Add a notion of OOM
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -955,8 +955,11 @@ void Memory::mkAxioms(const Memory &other) const {
Pointer p(m, bid, true);
if (auto sz = m.local_blk_size.lookup(p.get_short_bid())) {
auto size = sz->extract(bits_size_t - 2, 0);
- m.state->addPre(sum.add_no_uoverflow(size));
- sum = sum + size;
+ auto align = expr::mkUInt(1, bits_size_t - 1) << p.block_alignment();
+ align = align - expr::mkUInt(1, align.bits());
+ m.state->addOOM(size.add_no_uoverflow(align));
+ m.state->addOOM(sum.add_no_uoverflow(size + align));
+ sum = sum + size + align;
}
}
};

MODIFY
ir/state.h
ir/state.h
@@ -37,6 +37,7 @@ private:
bool is_initialization_phase = true;
smt::AndExpr precondition;
smt::AndExpr axioms;
+ smt::AndExpr ooms;
const BasicBlock *current_bb;
std::set<smt::expr> quantified_vars;
@@ -101,6 +102,7 @@ public:
void addPre(smt::expr &&cond) { precondition.add(std::move(cond)); }
void addUB(smt::expr &&ub);
void addUB(const smt::expr &ub);
+ void addOOM(smt::expr &&oom) { ooms.add(std::move(oom)); }
const std::vector<StateValue>
addFnCall(const std::string &name, std::vector<StateValue> &&inputs,
@@ -121,6 +123,7 @@ 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; }

ADD
tests/alive-tv/memory/alloca-removal-fail.src.ll
+; TEST-ARGS: -disable-undef-input
+define i8* @f_observed(i64 %size) {
+entry:
+ %items.addr = alloca i32, align 4
+ %call = call noalias i8* @malloc(i64 %size)
+ %i = ptrtoint i8* %call to i64
+ ret i8* %call
+}
+
+; ERROR: Value mismatch
+declare dso_local noalias i8* @malloc(i64)

ADD
tests/alive-tv/memory/alloca-removal-fail.tgt.ll
+define i8* @f_observed(i64 %size) {
+entry:
+ ret i8* null
+}
+
+declare dso_local noalias i8* @malloc(i64)

ADD
tests/alive-tv/memory/alloca-removal.src.ll
+; TEST-ARGS: -disable-undef-input
+define i8* @f(i64 %size) {
+entry:
+ %items.addr = alloca i32, align 4
+ %call = call noalias i8* @malloc(i64 %size)
+ ret i8* %call
+}
+
+define i8* @f_observed(i64 %size) {
+entry:
+ %items.addr = alloca i32, align 8
+ %call = call noalias i8* @malloc(i64 %size)
+ %unused = ptrtoint i8* %call to i64
+ ret i8* %call
+}
+
+declare dso_local noalias i8* @malloc(i64)

ADD
tests/alive-tv/memory/alloca-removal.tgt.ll
+; TEST-ARGS: -disable-undef-input
+define i8* @f(i64 %size) {
+entry:
+ %call = call noalias i8* @malloc(i64 %size)
+ ret i8* %call
+}
+
+define i8* @f_observed(i64 %size) {
+entry:
+ %call = call noalias i8* @malloc(i64 %size)
+ %unused = ptrtoint i8* %call to i64
+ ret i8* %call
+}
+
+declare dso_local noalias i8* @malloc(i64)

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

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -316,6 +316,8 @@ static void check_refinement(Errors &errs, Transform &t,
expr axioms_expr = axioms();
expr dom = dom_a && dom_b;
+ expr oom_src = src_state.getOOM()();
+
auto [poison_cnstr, value_cnstr] = type.refines(src_state, tgt_state, a, b);
auto src_mem = src_state.returnMemory();
@@ -323,7 +325,8 @@ static void check_refinement(Errors &errs, Transform &t,
auto [memory_cnstr, ptr_refinement0] = src_mem.refined(tgt_mem);
auto &ptr_refinement = ptr_refinement0;
- if (check_expr(axioms_expr && (pre_src && pre_tgt)).isUnsat()) {
+ if (check_expr(axioms_expr && (oom_src && pre_src && pre_tgt))
+ .isUnsat()) {
errs.add("Precondition is always false", false);
return;
}
@@ -338,8 +341,8 @@ static void check_refinement(Errors &errs, Transform &t,
if (refines.isFalse())
return move(refines);
- return axioms_expr &&
- preprocess(t, qvars, uvars, pre_tgt && pre_src.implies(refines));
+ auto fml = pre_tgt && oom_src && pre_src.implies(refines);
+ return axioms_expr && preprocess(t, qvars, uvars, move(fml));
};
auto print_ptr_load = [&](ostream &s, const Model &m) {

Add a notion of OOM (#261)