allow function calls to write to global vars
still missing code to write to escaped locals
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -20,6 +20,7 @@ bool has_int2ptr;
bool has_ptr2int;
bool has_malloc;
bool has_free;
+bool has_fncall;
bool has_nocapture;
bool has_readonly;
bool has_dead_allocas;

MODIFY
ir/globals.h
ir/globals.h
@@ -45,6 +45,8 @@ extern bool has_ptr2int;
extern bool has_malloc;
extern bool has_free;
+extern bool has_fncall;
+
/// Whether any function argument (not function call arg) has the attribute
extern bool has_nocapture;
extern bool has_readonly;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -146,7 +146,7 @@ Byte Byte::mkPtrByte(const Memory &m, const expr &val) {
byte = expr::mkUInt(1, 1);
if (padding)
byte = concat_if(byte, expr::mkUInt(0, padding));
- return { m, concat_if(byte, expr(val)) };
+ return { m, concat_if(byte, expr(val)).concat_zeros(bits_for_ptrattrs) };
}
Byte Byte::mkNonPtrByte(const Memory &m, const expr &val) {
@@ -574,7 +574,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 && !has_dead_allocas)
+ if (!has_free && !has_fncall && !has_dead_allocas)
return true;
auto bid = get_short_bid();
@@ -818,24 +818,28 @@ static bool memory_unused() {
!observes_addresses();
}
-Memory::Memory(State &state) : state(&state) {
- if (memory_unused())
- return;
-
- non_local_block_val
- = expr::mkArray("blk_val",
+static expr mk_block_val_array() {
+ return expr::mkArray("blk_val",
expr::mkUInt(0, bits_shortbid() + bits_for_offset),
expr::mkUInt(0, Byte::bitsByte()));
+}
- // Non-local blocks cannot initially contain pointers to local blocks
- // and no-capture pointers.
- if (does_ptr_mem_access) {
- auto idx = Pointer(*this, "#idx", false, false, expr()).short_ptr();
+static expr mk_liveness_array() {
+ return expr::mkArray("blk_liveness", expr::mkUInt(0, bits_shortbid()), true);
+}
+
+static void mk_nonlocal_val_axioms(State &s, Memory &m, expr &val) {
+ if (!does_ptr_mem_access)
+ return;
+
+ auto idx = Pointer(m, "#idx", false, false, expr()).short_ptr();
#if 0
if (num_nonlocals > 0) {
- expr is_ptr = expr::mkUF("blk_init_isptr", { idx }, true);
+ expr is_ptr = does_int_mem_access
+ ? expr::mkUF("blk_init_isptr", { idx }, true)
+ : true;
expr int_val
- = Byte::mkNonPtrByte(*this, expr::mkUF("blk_init_nonptr", { idx },
+ = Byte::mkNonPtrByte(m, expr::mkUF("blk_init_nonptr", { idx },
expr::mkUInt(0, bits_byte * 2)))();
expr np = expr::mkUF("blk_init_ptr_np", { idx }, expr::mkUInt(0, 1));
@@ -843,35 +847,39 @@ Memory::Memory(State &state) : state(&state) {
expr::mkUInt(0, bits_shortbid() + bits_for_offset + 3));
bid_off = prepend_if(expr::mkUInt(0, 1), move(bid_off),
ptr_has_local_bit());
- Byte ptr_val = Byte::mkPtrByte(*this, np.concat(bid_off));
+ Byte ptr_val = Byte::mkPtrByte(m, np.concat(bid_off));
assert(ptr_val.ptr().is_local().isFalse());
- non_local_block_val =
- expr::mkLambda({ idx }, expr::mkIf(is_ptr, ptr_val(), int_val));
+ val = expr::mkLambda({ idx }, expr::mkIf(is_ptr, ptr_val(), int_val));
- if (state.isSource())
- state.addAxiom(expr::mkForAll({ idx },
+ s.addAxiom(expr::mkForAll({ idx },
ptr_val.ptr().get_short_bid().ule(num_nonlocals - 1)));
} else {
- Byte byte(*this, non_local_block_val.load(idx));
- state.addAxiom(expr::mkForAll({ idx }, !byte.is_ptr()));
+ Byte byte(m, val.load(idx));
+ s.addAxiom(expr::mkForAll({ idx }, !byte.is_ptr()));
}
#else
- if (state.isSource()) {
- Byte byte(*this, non_local_block_val.load(idx));
+ Byte byte(m, val.load(idx));
Pointer loadedptr = byte.ptr();
expr bid = loadedptr.get_short_bid();
- state.addAxiom(
+ s.addAxiom(
expr::mkForAll({ idx },
byte.is_ptr().implies(!loadedptr.is_local() &&
!loadedptr.is_nocapture() &&
bid.ule(num_nonlocals - 1))));
- }
#endif
}
- non_local_block_liveness
- = expr::mkArray("blk_liveness", expr::mkUInt(0, bits_shortbid()), true);
+Memory::Memory(State &state) : state(&state) {
+ if (memory_unused())
+ return;
+
+ non_local_block_val = mk_block_val_array();
+ non_local_block_liveness = mk_liveness_array();
+
+ // Non-local blocks cannot initially contain pointers to local blocks
+ // and no-capture pointers.
+ mk_nonlocal_val_axioms(state, *this, non_local_block_val);
// initialize all local blocks as non-pointer, poison value
// This is okay because loading a pointer as non-pointer is also poison.
@@ -899,6 +907,10 @@ Memory::Memory(State &state) : state(&state) {
assert(bits_for_offset <= bits_size_t);
}
+void Memory::finishInitialization() {
+ initial_non_local_block_val = non_local_block_val;
+}
+
void Memory::mkAxioms(const Memory &other) const {
assert(state->isSource() && !other.state->isSource());
if (memory_unused())
@@ -1020,6 +1032,39 @@ pair<expr,expr> Memory::mkFnRet(const char *name) const {
return { p.release(), move(var) };
}
+expr Memory::CallState::operator==(const CallState &st) const {
+ if (empty || st.empty)
+ return true;
+ return block_val_var == st.block_val_var &&
+ liveness_var == st.liveness_var;
+}
+
+Memory::CallState Memory::mkCallState() const {
+ Memory::CallState st;
+ st.empty = false;
+
+ auto blk_val = mk_block_val_array();
+ st.block_val_var = expr::mkFreshVar("blk_val", blk_val);
+ st.non_local_block_val
+ = initial_non_local_block_val.subst(blk_val, st.block_val_var);
+
+ // functions can free an object, but cannot bring a dead one back to live
+ auto idx = expr::mkFreshVar("#idx", expr::mkUInt(0, bits_shortbid()));
+ st.liveness_var = expr::mkFreshVar("blk_liveness", mk_liveness_array());
+ st.non_local_block_liveness
+ = expr::mkLambda( { idx }, non_local_block_liveness.load(idx) &&
+ st.liveness_var.load(idx));
+ return st;
+}
+
+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;
+ mk_nonlocal_val_axioms(*state, *this, non_local_block_val);
+}
+
static expr disjoint_local_blocks(const Memory &m, const expr &addr,
const expr &sz, FunctionExpr &blk_addr) {
expr disj = true;
@@ -1379,13 +1424,16 @@ Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
bool Memory::operator<(const Memory &rhs) const {
// FIXME: remove this once we move to C++20
+ // NOTE: we don't compare field state so that memories from src/tgt can
+ // compare equal
return
- tie(non_local_block_val, local_block_val,
+ tie(non_local_block_val, local_block_val, initial_non_local_block_val,
non_local_block_liveness, local_block_liveness, local_blk_addr,
local_blk_size, local_blk_align, local_blk_kind,
non_local_blk_nonwritable, non_local_blk_size, non_local_blk_align,
non_local_blk_kind, byval_blks) <
tie(rhs.non_local_block_val, rhs.local_block_val,
+ rhs.initial_non_local_block_val,
rhs.non_local_block_liveness, rhs.local_block_liveness,
rhs.local_blk_addr, rhs.local_blk_size, rhs.local_blk_align,
rhs.local_blk_kind, rhs.non_local_blk_nonwritable,

MODIFY
ir/memory.h
ir/memory.h
@@ -185,6 +185,7 @@ class Memory {
smt::expr non_local_block_val; // array: (bid, offset) -> Byte
smt::expr local_block_val;
+ smt::expr initial_non_local_block_val;
smt::expr non_local_block_liveness; // array: bid -> bool
smt::expr local_block_liveness;
@@ -206,8 +207,22 @@ public:
HEAP, STACK, GLOBAL, CONSTGLOBAL
};
+ // TODO: missing local_* equivalents
+ class CallState {
+ smt::expr non_local_block_val;
+ smt::expr block_val_var;
+ smt::expr non_local_block_liveness;
+ smt::expr liveness_var;
+ bool empty = true;
+
+ public:
+ smt::expr operator==(const CallState &st) const;
+ friend class Memory;
+ };
+
Memory(State &state);
+ void finishInitialization();
void mkAxioms(const Memory &other) const;
static void resetGlobalData();
@@ -216,7 +231,10 @@ public:
void markByVal(unsigned bid);
smt::expr mkInput(const char *name, unsigned attributes) const;
std::pair<smt::expr, smt::expr> mkUndefInput(unsigned attributes) const;
+
std::pair<smt::expr, smt::expr> mkFnRet(const char *name) const;
+ CallState mkCallState() const;
+ void setState(const CallState &st);
// Allocates a new memory block and returns (pointer expr, allocated).
// If bid is not specified, it creates a fresh block id by increasing

MODIFY
ir/state.cpp
ir/state.cpp
@@ -195,6 +195,7 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
return vector<StateValue>(out_types.size());
}
+ // TODO: this doesn't need to compare the full memory, just a subset of fields
auto [I, inserted]
= fn_call_data[name].try_emplace({ move(inputs), move(ptr_inputs),
memory, reads_memory, argmemonly });
@@ -217,19 +218,24 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
}
string ub_name = string(name) + "#ub";
- I->second = { move(values), expr::mkFreshVar(ub_name.c_str(), false) };
+ I->second = { move(values), expr::mkFreshVar(ub_name.c_str(), false),
+ writes_memory ? memory.mkCallState() : Memory::CallState() };
}
- addUB(I->second.second);
+ addUB(get<1>(I->second));
+
+ if (writes_memory)
+ memory.setState(get<2>(I->second));
+
if (all_args_np.isTrue())
- return I->second.first;
+ return get<0>(I->second);
// if any of the arguments is poison, yield an arbitrary value, such that
// f(poison) -> f(42) works
vector<StateValue> ret;
auto T = out_types.begin();
auto var_name = name + "#pval";
- for (auto &[v, np] : I->second.first) {
+ for (auto &[v, np] : get<0>(I->second)) {
auto [val_poison, var] = mk_val(**T, var_name);
ret.emplace_back(expr::mkIf(all_args_np, v, val_poison), expr(np));
addQuantVar(move(var));
@@ -278,6 +284,11 @@ StateValue State::rewriteUndef(StateValue &&val) {
return { val.value.subst(repls), val.non_poison.subst(repls) };
}
+void State::finishInitializer() {
+ is_initialization_phase = false;
+ memory.finishInitialization();
+}
+
void State::addGlobalVarBid(const string &glbvar, unsigned bid) {
ENSURE(glbvar_bids.emplace(glbvar, make_pair(bid, true)).second);
}
@@ -320,12 +331,12 @@ void State::mkAxioms(State &tgt) {
(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] = I->second;
+ auto &[rets, ub, mem_state] = I->second;
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, argmem2] = I2->first;
- auto &[rets2, ub2] = I2->second;
+ auto &[rets2, ub2, mem_state2] = I2->second;
expr refines(true), is_val_eq(true);
for (unsigned i = 0, e = ins.size(); i != e; ++i) {
@@ -356,7 +367,8 @@ 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)));
+ tgt.addPre(refines.implies(ref_expr && ub.implies(ub2) &&
+ mem_state == mem_state2));
}
}
}

MODIFY
ir/state.h
ir/state.h
@@ -70,11 +70,12 @@ private:
// store data for function calls:
// inputs: non-ptr arguments, ptr arguments, memory, reads memory?, argmemonly
- // outputs: values, UB
+ // outputs: values, UB, memory state
std::map<std::string,
std::map<std::tuple<std::vector<StateValue>, std::vector<StateValue>,
Memory, bool, bool>,
- std::pair<std::vector<StateValue>, smt::expr>>>
+ std::tuple<std::vector<StateValue>, smt::expr,
+ Memory::CallState>>>
fn_call_data;
public:
@@ -114,7 +115,7 @@ public:
StateValue rewriteUndef(StateValue &&val);
bool isInitializationPhase() const { return is_initialization_phase; }
- void finishInitializer() { is_initialization_phase = false; }
+ void finishInitializer();
auto& getFn() const { return f; }
auto& getMemory() { return memory; }

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -620,6 +620,7 @@ static void calculateAndInitConstants(Transform &t) {
has_ptr2int = false;
has_malloc = false;
has_free = false;
+ has_fncall = false;
does_ptr_store = false;
does_ptr_mem_access = false;
does_int_mem_access = false;
@@ -648,6 +649,7 @@ static void calculateAndInitConstants(Transform &t) {
has_malloc |= dynamic_cast<const Calloc*>(&I) != nullptr;
has_free |= dynamic_cast<const Free*>(&I) != nullptr;
has_load |= dynamic_cast<const Load*>(&I) != nullptr;
+ has_fncall |= dynamic_cast<const FnCall*>(&I) != nullptr;
auto accsz = get_access_size(I);
if (accsz != NO_ACCESS) {
@@ -660,9 +662,13 @@ static void calculateAndInitConstants(Transform &t) {
num_nonlocals = num_globals + num_ptrinputs + num_max_nonlocals_inst;
// check if null block is needed
- if (num_nonlocals > 0 || nullptr_is_used || has_malloc || has_load)
+ if (num_nonlocals > 0 || nullptr_is_used || has_malloc || has_load ||
+ has_fncall)
++num_nonlocals;
+ // Allow at least one non-const global for calls to change
+ num_nonlocals += has_fncall;
+
auto has_attr = [&](Input::Attribute a) -> bool {
for (auto fn : { &t.src, &t.tgt }) {
for (auto &v : fn->getInputs()) {

allow function calls to write to global vars
still missing code to write to escaped locals