fix OOM formula in refinement constraints
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1543,8 +1543,8 @@ void Memory::mkAxioms(const Memory &tgt) const {
auto align = one << p.blockAlignment().zextOrTrunc(bits_size_t - 1);
align = align - one;
auto sz_align = size + align;
- m.state->addOOM(size.add_no_uoverflow(align));
- m.state->addOOM(sum.add_no_uoverflow(sz_align));
+ m.state->addPre(size.add_no_uoverflow(align));
+ m.state->addPre(sum.add_no_uoverflow(sz_align));
sum = sum + sz_align;
}
}

MODIFY
ir/state.h
ir/state.h
@@ -54,7 +54,6 @@ private:
bool is_initialization_phase = true;
smt::AndExpr precondition;
smt::AndExpr axioms;
- smt::AndExpr ooms;
const BasicBlock *current_bb = nullptr;
std::set<smt::expr> quantified_vars;
@@ -137,7 +136,6 @@ public:
void addUB(const smt::expr &ub);
void addUB(smt::AndExpr &&ubs);
void addNoReturn();
- void addOOM(smt::expr &&oom) { ooms.add(std::move(oom)); }
std::vector<StateValue>
addFnCall(const std::string &name, std::vector<StateValue> &&inputs,
@@ -159,7 +157,6 @@ public:
auto& getMemory() { return memory; }
auto& getAxioms() const { return axioms; }
auto& getPre() const { return precondition; }
- auto& getOOM() const { return ooms; }
const auto& getValues() const { return values; }
const auto& getQuantVars() const { return quantified_vars; }

MODIFY
tests/alive-tv/memory/malloc-undef.src.ll
tests/alive-tv/memory/malloc-undef.src.ll
-; NOTE: This should fail, but malloc of quantified variable is not supported.
-; (it spuriously succeeds)
+; ERROR: Value mismatch
define i8 @malloc_undef() {
%ptr = call i8* @malloc(i64 undef)

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -316,7 +316,6 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
expr axioms_expr = axioms();
expr dom = dom_a && dom_b;
- pre_tgt &= src_state.getOOM()();
pre_tgt &= !tgt_state.sinkDomain();
expr pre_src_exists = pre_src, pre_src_forall = true;

fix OOM formula in refinement constraints