add a couple of optimizations to memory refinement
now bypasses the solver more often
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -797,10 +797,12 @@ expr Pointer::blockValRefined(const Pointer &other) const {
// refinement if offset had non-ptr value
expr np1 = val.nonptrNonpoison();
+ expr np2 = val2.nonptrNonpoison();
+ bool np_eqs = np1.eq(np2);
expr int_cnstr = does_sub_byte_access
- ? (val2.nonptrNonpoison() | np1) == np1 &&
+ ? (np2 | np1) == np1 &&
(val.nonptrValue() | np1) == (val2.nonptrValue() | np1)
- : val2.nonptrNonpoison() == 0 &&
+ : (np_eqs ? true : np2 == 0) &&
val.nonptrValue() == val2.nonptrValue();
// fast path: if we didn't do any ptr store, then all ptrs in memory were

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -330,7 +330,8 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
auto tgt_mem = tgt_state.returnMemory();
auto [memory_cnstr0, ptr_refinement0] = src_mem.refined(tgt_mem, false);
auto &ptr_refinement = ptr_refinement0;
- auto memory_cnstr = value_cnstr && memory_cnstr0;
+ auto memory_cnstr = memory_cnstr0.isTrue() ? memory_cnstr0
+ : value_cnstr && memory_cnstr0;
if (check_expr(axioms_expr && (pre_src && pre_tgt)).isUnsat()) {
errs.add("Precondition is always false", false);

add a couple of optimizations to memory refinement
now bypasses the solver more often