Add --pointer-encoding-via-maps: solver-level array maps for pointer encoding#8953

Draft

tautschnig wants to merge 30 commits intodiffblue:developfrom

tautschnig:feature/pointer-encoding-via-maps

Commits on Apr 8, 2026

Skip Ackermann constraints for derived arrays (weak equivalence)

tautschnig
and
kiro-agent
committed
Accept member expressions with arbitrary struct operands in array solver

tautschnig
and
kiro-agent
committed
Simplify expressions after lowering byte operators for array theory

tautschnig
and
kiro-agent
committed
Handle array typecast with different element sizes in array theory

tautschnig
and
kiro-agent
committed
Document Array_operations2 union-find conflation bug with --arrays-uf-always

tautschnig
and
kiro-agent
committed
Handle simplified equality in array theory byte operator lowering

tautschnig
and
kiro-agent
committed
Add regression test target for --arrays-uf-always

tautschnig
and
kiro-agent
committed
Make with and if array constraints lazy for --refine-arrays

tautschnig
and
kiro-agent
committed
Add regression test for --refine-arrays with --arrays-uf-always

tautschnig
and
kiro-agent
committed
Add regression test target for --arrays-uf-always --refine-arrays

tautschnig
and
kiro-agent
committed
Disable SAT simplifier when --refine-arrays is used

tautschnig
and
kiro-agent
committed
Keep with/if array constraints eager, only Ackermann lazy

tautschnig
and
kiro-agent
committed
Use array comprehension for large byte_extract lowering

tautschnig
and
kiro-agent
committed
Promote arrays-uf-always-member-crash test from KNOWNBUG to CORE

tautschnig
and
kiro-agent
committed
Fix --arrays-uf-always soundness for member-of-index array expressions

tautschnig
and
kiro-agent
committed
Regression test: --arrays-uf-always soundness issue with large struct arrays

tautschnig
and
kiro-agent
committed
Connect array symbol map literals to element-wise constraints

tautschnig
and
kiro-agent
committed
Fix array theory: add with-constraints for SSA-renamed indices

tautschnig
and
kiro-agent
committed
Mark Array_UF23 as KNOWNBUG: refinement non-convergence

tautschnig
and
kiro-agent
committed
Add map-based pointer encoding via --pointer-encoding-via-maps
tautschnig
committed
Fix pointer equality and pointer-to-integer casts in map encoding

tautschnig
and
kiro-agent
committed
Lower byte operations on pointer types and cache encode()

tautschnig
and
kiro-agent
committed
Bypass array theory for constant pointer indices and add offset inequalities

tautschnig
and
kiro-agent
committed
Fix pointer arithmetic overflow checks and constrain address range

tautschnig
and
kiro-agent
committed
Improve pointer equality and subtraction for map encoding

tautschnig
and
kiro-agent
committed
Templatize bv_refinementt on pointer encoding base class

tautschnig
and
kiro-agent
committed
Add alternative test descriptors for map encoding

tautschnig
and
kiro-agent
committed
Constrain I2P object to known objects

tautschnig
and
kiro-agent
committed
Add backward I2P constraint: address in range implies object identity

tautschnig
and
kiro-agent
committed
Add test tagging for maps-based pointer encoding

tautschnig
and
kiro-agent
committed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add --pointer-encoding-via-maps: solver-level array maps for pointer encoding#8953

Add --pointer-encoding-via-maps: solver-level array maps for pointer encoding#8953
tautschnig wants to merge 30 commits intodiffblue:developfrom
tautschnig:feature/pointer-encoding-via-maps

Commits on Apr 8, 2026

Skip Ackermann constraints for derived arrays (weak equivalence)

Accept member expressions with arbitrary struct operands in array solver

Simplify expressions after lowering byte operators for array theory

Handle array typecast with different element sizes in array theory

Document Array_operations2 union-find conflation bug with --arrays-uf-always

Handle simplified equality in array theory byte operator lowering

Add regression test target for --arrays-uf-always

Make with and if array constraints lazy for --refine-arrays

Add regression test for --refine-arrays with --arrays-uf-always

Add regression test target for --arrays-uf-always --refine-arrays

Disable SAT simplifier when --refine-arrays is used

Keep with/if array constraints eager, only Ackermann lazy

Use array comprehension for large byte_extract lowering

Promote arrays-uf-always-member-crash test from KNOWNBUG to CORE

Fix --arrays-uf-always soundness for member-of-index array expressions

Regression test: --arrays-uf-always soundness issue with large struct arrays

Connect array symbol map literals to element-wise constraints

Fix array theory: add with-constraints for SSA-renamed indices

Mark Array_UF23 as KNOWNBUG: refinement non-convergence

Add map-based pointer encoding via --pointer-encoding-via-maps

Fix pointer equality and pointer-to-integer casts in map encoding

Lower byte operations on pointer types and cache encode()

Bypass array theory for constant pointer indices and add offset inequalities

Fix pointer arithmetic overflow checks and constrain address range

Improve pointer equality and subtraction for map encoding

Templatize bv_refinementt on pointer encoding base class

Add alternative test descriptors for map encoding

Constrain I2P object to known objects

Add backward I2P constraint: address in range implies object identity

Add test tagging for maps-based pointer encoding