memory/fncall: skip checking of constants
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1562,7 +1562,7 @@ expr Memory::int2ptr(const expr &val) const {
}
pair<expr,Pointer>
-Memory::refined(const Memory &other,
+Memory::refined(const Memory &other, bool skip_constants,
const vector<pair<StateValue, bool>> *set_ptrs) const {
if (IR::num_nonlocals <= 1)
return { true, Pointer(*this, expr()) };
@@ -1573,7 +1573,18 @@ Memory::refined(const Memory &other,
expr offset = ptr.get_offset();
expr ret(true);
+ auto is_constglb = [](const Memory &m, unsigned bid) {
+ return
+ find(m.non_local_blk_nonwritable.begin(),
+ m.non_local_blk_nonwritable.end(), bid) !=
+ m.non_local_blk_nonwritable.end();
+ };
+
for (unsigned bid = 1; bid < IR::num_nonlocals_src; ++bid) {
+ if (skip_constants && is_constglb(*this, bid)) {
+ assert(is_constglb(other, bid));
+ continue;
+ }
expr bid_expr = expr::mkUInt(bid, bits_for_bid);
Pointer p(*this, bid_expr, offset);
Pointer q(other, p());
@@ -1583,13 +1594,6 @@ Memory::refined(const Memory &other,
}
#ifndef NDEBUG
- auto is_constglb = [](const Memory &m, unsigned bid) {
- return
- find(m.non_local_blk_nonwritable.begin(),
- m.non_local_blk_nonwritable.end(), bid) !=
- m.non_local_blk_nonwritable.end();
- };
-
if (state->isSource() && !other.state->isSource()) {
for (unsigned bid = IR::num_nonlocals_src; bid < IR::num_nonlocals; ++bid)
assert(!is_constglb(*this, bid) && is_constglb(other, bid));

MODIFY
ir/memory.h
ir/memory.h
@@ -285,6 +285,7 @@ public:
std::pair<smt::expr,Pointer>
refined(const Memory &other,
+ bool skip_constants,
const std::vector<std::pair<StateValue, bool>> *set_ptrs = nullptr)
const;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -412,7 +412,7 @@ void State::mkAxioms(State &tgt) {
if (reads2) {
auto restrict_ptrs = argmem2 ? &ptr_ins2 : nullptr;
- expr mem_refined = mem.refined(mem2, restrict_ptrs).first;
+ expr mem_refined = mem.refined(mem2, true, restrict_ptrs).first;
is_val_eq &= mem_refined;
refines &= mem_refined;
}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -322,7 +322,7 @@ static void check_refinement(Errors &errs, Transform &t,
auto src_mem = src_state.returnMemory();
auto tgt_mem = tgt_state.returnMemory();
- auto [memory_cnstr, ptr_refinement0] = src_mem.refined(tgt_mem);
+ auto [memory_cnstr, ptr_refinement0] = src_mem.refined(tgt_mem, false);
auto &ptr_refinement = ptr_refinement0;
if (check_expr(axioms_expr && (pre_src && pre_tgt)).isUnsat()) {

memory/fncall: skip checking of constants