memory: fix assorted bugs related with lifetime management
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -19,6 +19,7 @@ bool has_int2ptr;
bool has_ptr2int;
bool has_malloc;
bool has_free;
+bool has_dead_allocas;
bool does_int_mem_access;
bool does_ptr_mem_access;

MODIFY
ir/globals.h
ir/globals.h
@@ -41,6 +41,9 @@ extern bool has_ptr2int;
extern bool has_malloc;
extern bool has_free;
+/// Whether there are allocas that are initially dead (need start_lifetime)
+extern bool has_dead_allocas;
+
/// Whether the programs do memory accesses that load/store int/ptrs
extern bool does_int_mem_access;
extern bool does_ptr_mem_access;

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1817,9 +1817,8 @@ void StartLifetime::print(std::ostream &os) const {
StateValue StartLifetime::toSMT(State &s) const {
auto &[p, np] = s[*ptr];
- expr allocated = s.getMemory().start_lifetime(p);
- // This should be coherent with Alloc's OOM semantics
- s.addUB(np && allocated);
+ s.addUB(np);
+ s.getMemory().start_lifetime(p);
return {};
}

MODIFY
ir/instr.h
ir/instr.h
@@ -384,6 +384,7 @@ public:
: Instr(type, std::move(name)), size(&size), align(align),
initially_dead(initially_dead) {}
+ bool initDead() const { return initially_dead; }
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;
void print(std::ostream &os) const override;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -510,7 +510,7 @@ expr Pointer::is_block_alive() const {
// If programs have no free(), we assume all blocks are always live.
// For non-local blocks, there's enough non-determinism through block size,
// that can be 0 or non-0
- if (!has_free)
+ if (!has_free && !has_dead_allocas)
return true;
auto bid = get_short_bid();
@@ -970,30 +970,25 @@ pair<expr, expr> Memory::alloc(const expr &size, unsigned align, BlockKind block
return { p.release(), move(allocated) };
}
-expr Memory::start_lifetime(const expr &ptr_local) {
+void Memory::start_lifetime(const expr &ptr_local) {
assert(!memory_unused());
Pointer p(*this, ptr_local);
auto align = *local_blk_align(p.get_short_bid());
- auto size_upperbound = p.block_size() + align.zextOrTrunc(bits_size_t) -
- expr::mkUInt(1, bits_size_t);
- auto allocated = size_upperbound.ule(local_avail_space.zext(1));
+ auto one = expr::mkUInt(1, bits_size_t);
+ auto size_upperbound = p.block_size() +
+ (one << align.zextOrTrunc(bits_size_t)) - one;
+ state->addUB(size_upperbound.ule(local_avail_space.zext(1)));
- if (observes_addresses()) {
- // Disjointness of block's address range with other local blocks
- state->addPre(
- allocated.implies(disjoint_local_blocks(*this, p.get_address(),
- p.block_size(), local_blk_addr)));
- }
- auto size_upperbound_trunc = size_upperbound.trunc(bits_size_t - 1);
- // Reduces memory usage even if the alloca was alive before lifetime.start
+ if (observes_addresses())
+ state->addPre(disjoint_local_blocks(*this, p.get_address(), p.block_size(),
+ local_blk_addr));
+
+ // Reduces available space even if the alloca was alive before lifetime.start
// for performance
- local_avail_space = expr::mkIf(allocated,
- local_avail_space - size_upperbound_trunc,
- local_avail_space);
- // alloca is always alive after lifetime.start(), otherwise it should be UB
+ local_avail_space = local_avail_space - size_upperbound.trunc(bits_size_t-1);
+
local_block_liveness = local_block_liveness.store(p.get_short_bid(), true);
- return allocated;
}
void Memory::free(const expr &ptr, bool unconstrained) {

MODIFY
ir/memory.h
ir/memory.h
@@ -132,7 +132,7 @@ public:
StateValue ugt(const Pointer &rhs) const;
smt::expr inbounds() const;
- smt::expr block_alignment() const;
+ smt::expr block_alignment() const; // log(bits)
smt::expr is_block_aligned(unsigned align, bool exact = false) const;
smt::expr is_aligned(unsigned align) const;
void is_dereferenceable(unsigned bytes, unsigned align, bool iswrite);
@@ -212,8 +212,7 @@ public:
unsigned *bid_out = nullptr, const smt::expr &precond = true);
// Start lifetime of a local block.
- // Returns whether it is successfully allocated.
- smt::expr start_lifetime(const smt::expr &ptr_local);
+ void start_lifetime(const smt::expr &ptr_local);
// If unconstrained is true, the pointer offset, liveness, and block kind
// are not checked.

MODIFY
ir/state.cpp
ir/state.cpp
@@ -195,13 +195,9 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
return vector<StateValue>(out_types.size());
}
- optional<Memory> mem_in;
- if (reads_memory)
- mem_in = memory;
-
auto [I, inserted]
= fn_call_data[name].try_emplace({ move(inputs), move(ptr_inputs),
- move(mem_in)});
+ memory, reads_memory });
if (inserted) {
vector<StateValue> values;
@@ -311,33 +307,34 @@ void State::mkAxioms(State &tgt) {
memory.mkAxioms();
// axioms for function calls
- for (auto &[fn, data] : tgt.fn_call_data) {
+ 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] = I->first;
+ auto &[ins, ptr_ins, mem, reads] = I->first;
auto &[rets, ub] = I->second;
- for (auto I2 = data.begin(); I2 != E; ++I2) {
- auto &[ins2, ptr_ins2, mem2] = I2->first;
+ auto &data2 = tgt.fn_call_data.at(fn);
+ for (auto I2 = data2.begin(), E2 = data2.end(); I2 != E2; ++I2) {
+ auto &[ins2, ptr_ins2, mem2, reads2] = I2->first;
auto &[rets2, ub2] = I2->second;
expr refines(true), is_val_eq(true);
for (unsigned i = 0, e = ins.size(); i != e; ++i) {
expr eq_val = ins[i].value == ins2[i].value;
is_val_eq &= eq_val;
- refines &= !ins[i].non_poison || (eq_val && ins2[i].non_poison);
+ refines &= ins[i].non_poison.implies(eq_val && ins2[i].non_poison);
}
for (unsigned i = 0, e = ptr_ins.size(); i != e; ++i) {
- expr eq_val = Pointer(memory, ptr_ins[i].value)
- .fninput_refined(Pointer(memory, ptr_ins2[i].value));
+ expr eq_val = Pointer(mem, ptr_ins[i].value)
+ .fninput_refined(Pointer(mem2, ptr_ins2[i].value));
is_val_eq &= eq_val;
refines &= ptr_ins[i].non_poison
.implies(eq_val && ptr_ins2[i].non_poison);
}
- if (mem && mem2) {
- expr mem_refined = mem->refined(*mem2).first;
+ if (reads && reads2) {
+ expr mem_refined = mem.refined(mem2).first;
is_val_eq &= mem_refined;
refines &= mem_refined;
}

MODIFY
ir/state.h
ir/state.h
#include "smt/exprs.h"
#include <array>
#include <map>
-#include <optional>
#include <ostream>
#include <set>
#include <string>
@@ -70,11 +69,11 @@ private:
std::set<smt::expr> return_undef_vars;
// store data for function calls:
- // inputs: non-ptr arguments, ptr arguments, optinal memory
+ // inputs: non-ptr arguments, ptr arguments, memory, reads memory?
// outputs: values, UB
std::map<std::string,
std::map<std::tuple<std::vector<StateValue>, std::vector<StateValue>,
- std::optional<Memory>>,
+ Memory, bool>,
std::pair<std::vector<StateValue>, smt::expr>>>
fn_call_data;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -503,6 +503,9 @@ static void calculateAndInitConstants(Transform &t) {
has_ptr2int |= conv->getOp() == ConversionOp::Ptr2Int;
}
+ if (auto alloc = dynamic_cast<const Alloc*>(&I))
+ has_dead_allocas |= alloc->initDead();
+
has_malloc |= dynamic_cast<const Malloc*>(&I) != nullptr;
has_free |= dynamic_cast<const Free *>(&I) != nullptr;

memory: fix assorted bugs related with lifetime management