memory: fix bug in fncall where globals weren't being havoced because there were no globals
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1021,9 +1021,11 @@ pair<expr,expr> Memory::mkFnRet(const char *name) const {
return { p.release(), move(var) };
}
-expr Memory::CallState::operator==(const CallState &st) const {
+expr Memory::CallState::implies(const CallState &st) const {
if (empty || st.empty)
return true;
+ // NOTE: using equality here is an approximation.
+ // TODO: benchmark using quantifiers to state implication
return block_val_var == st.block_val_var &&
liveness_var == st.liveness_var;
}
@@ -1048,9 +1050,7 @@ Memory::CallState Memory::mkCallState() const {
void Memory::setState(const Memory::CallState &st) {
non_local_block_val = st.non_local_block_val;
- // TODO: missing condition that if fn calls are refined, so is the liveness
- // data
- //non_local_block_liveness = st.non_local_block_liveness;
+ non_local_block_liveness = st.non_local_block_liveness;
mk_nonlocal_val_axioms(*state, *this, non_local_block_val);
}

MODIFY
ir/memory.h
ir/memory.h
@@ -216,7 +216,7 @@ public:
bool empty = true;
public:
- smt::expr operator==(const CallState &st) const;
+ smt::expr implies(const CallState &st) const;
friend class Memory;
};

MODIFY
ir/state.cpp
ir/state.cpp
@@ -327,8 +327,10 @@ void State::mkAxioms(State &tgt) {
memory.mkAxioms(tgt.memory);
// axioms for function calls
+ // We would potentially need to do refinement check of tgt x tgt, but it
+ // doesn't seem to be needed in practice for optimizations
+ // since there's no introduction of calls in tgt
for (auto &[fn, data] : fn_call_data) {
- (void)fn;
for (auto I = data.begin(), E = data.end(); I != E; ++I) {
auto &[ins, ptr_ins, mem, reads, argmem] = I->first;
auto &[rets, ub, mem_state] = I->second;
@@ -367,8 +369,9 @@ void State::mkAxioms(State &tgt) {
ref_expr &= rets[i].non_poison.implies(rets2[i].non_poison);
}
tgt.addPre(is_val_eq.implies(eq_expr));
- tgt.addPre(refines.implies(ref_expr && ub.implies(ub2) &&
- mem_state == mem_state2));
+ tgt.addPre(refines.implies(ref_expr &&
+ ub.implies(ub2) &&
+ mem_state.implies(mem_state2)));
}
}
}

MODIFY
tests/unit/call-error3.opt
tests/unit/call-error3.opt
-; ERROR: Value mismatch
+; ERROR: Target is more poisonous
%c = call i32 @f(i32 3)
%d = call i32 @f(i32 poison)

ADD
tests/unit/call-error4.opt
+; TEST-ARGS: -root-only
+; ERROR: Value mismatch
+
+ %c = call i32 @f(i32 3)
+ %d = call i32 @f(i32 3)
+ %r = icmp eq i32 %c, %d
+ ret %r
+=>
+ ret true

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -672,6 +672,9 @@ static void calculateAndInitConstants(Transform &t) {
// Allow at least one non-const global for calls to change
num_nonlocals += has_fncall;
+ if (!does_int_mem_access && !does_ptr_mem_access && has_fncall)
+ does_int_mem_access = true;
+
auto has_attr = [&](Input::Attribute a) -> bool {
for (auto fn : { &t.src, &t.tgt }) {
for (auto &v : fn->getInputs()) {

memory: fix bug in fncall where globals weren't being havoced because there were no globals