memory: implement partial order reduction for pointer loads
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -14,6 +14,7 @@ unsigned num_locals_src;
unsigned num_locals_tgt;
unsigned num_consts_src;
unsigned num_globals_src;
+unsigned num_ptrinputs;
unsigned num_extra_nonconst_tgt;
unsigned num_nonlocals;
unsigned num_nonlocals_src;

MODIFY
ir/globals.h
ir/globals.h
@@ -15,6 +15,8 @@ extern unsigned num_consts_src;
extern unsigned num_globals_src;
+extern unsigned num_ptrinputs;
+
/// Number of non-constant globals introduced in tgt
extern unsigned num_extra_nonconst_tgt;

MODIFY
ir/memory.cpp
ir/memory.cpp
#include "ir/value.h"
#include "smt/solver.h"
#include "util/compiler.h"
-#include <map>
#include <string>
using namespace IR;
@@ -19,9 +18,6 @@ static unsigned ptr_next_idx;
static unsigned next_local_bid;
static unsigned next_nonlocal_bid;
static unsigned next_ptr_input;
-static unsigned next_nonlocal_ptr;
-static map<expr, unsigned> max_nonlocal_bid;
-static map<expr, vector<bool>> local_bid_alias;
static bool observes_addresses() {
return IR::has_ptr2int || IR::has_int2ptr;
@@ -917,6 +913,10 @@ static vector<expr> extract_possible_local_bids(Memory &m, const expr &ptr) {
return ret;
}
+unsigned Memory::nextNonlocalPtr() {
+ return min(next_nonlocal_ptr++, num_nonlocals_src-1);
+}
+
unsigned Memory::numLocals() const {
return state->isSource() ? num_locals_src : num_locals_tgt;
}
@@ -970,7 +970,7 @@ bool Memory::mayalias(bool local, unsigned bid0, const expr &offset0,
template <typename Fn>
void Memory::access(const Pointer &ptr, unsigned bytes, unsigned align,
- bool write, Fn &fn) const {
+ bool write, Fn &fn) {
assert(bytes % (bits_byte/8) == 0);
vector<bool> access_local, access_nonlocal;
@@ -1073,7 +1073,7 @@ void Memory::access(const Pointer &ptr, unsigned bytes, unsigned align,
vector<Byte> Memory::load(const Pointer &ptr, unsigned bytes, set<expr> &undef,
unsigned align, bool left2right,
- DataType type) const {
+ DataType type) {
if (bytes == 0)
return {};
@@ -1267,6 +1267,9 @@ Memory::Memory(State &state) : state(&state) {
if (memory_unused())
return;
+ next_nonlocal_ptr
+ = has_null_block + num_globals_src + num_ptrinputs + has_fncall;
+
if (has_null_block)
non_local_block_val.emplace_back();
@@ -1306,22 +1309,27 @@ Memory::Memory(State &state) : state(&state) {
// Initialize a memory block for null pointer.
if (has_null_block)
- alloc(expr::mkUInt(0, bits_size_t), bits_program_pointer, GLOBAL, false,
- false, 0);
+ alloc(expr::mkUInt(0, bits_size_t), 1, GLOBAL, false, false, 0);
assert(bits_for_offset <= bits_size_t);
}
-void Memory::mkAxioms(const Memory &other) const {
- assert(state->isSource() && !other.state->isSource());
+void Memory::mkAxioms(const Memory &tgt) const {
+ assert(state->isSource() && !tgt.state->isSource());
if (memory_unused())
return;
+ auto nonlocal_used = [&](unsigned bid) {
+ return bid < tgt.next_nonlocal_ptr || bid >= num_nonlocals_src;
+ };
+
// transformation can increase alignment
- unsigned align = heap_block_alignment;
+ unsigned align = ilog2(heap_block_alignment);
for (unsigned bid = has_null_block; bid < num_nonlocals; ++bid) {
+ if (!nonlocal_used(bid))
+ continue;
Pointer p(*this, bid, false);
- Pointer q(other, bid, false);
+ Pointer q(tgt, bid, false);
auto p_align = p.blockAlignment();
auto q_align = q.blockAlignment();
state->addAxiom(expr::mkIf(p.isHeapAllocated(),
@@ -1338,6 +1346,9 @@ void Memory::mkAxioms(const Memory &other) const {
// Non-local blocks are disjoint.
// Ignore null pointer block
for (unsigned bid = has_null_block; bid < num_nonlocals; ++bid) {
+ if (!nonlocal_used(bid))
+ continue;
+
Pointer p1(*this, bid, false);
auto addr = p1.getAddress();
auto sz = p1.blockSize();
@@ -1350,6 +1361,8 @@ void Memory::mkAxioms(const Memory &other) const {
// disjointness constraint
for (unsigned bid2 = bid + 1; bid2 < num_nonlocals; ++bid2) {
+ if (!nonlocal_used(bid2))
+ continue;
Pointer p2(*this, bid2, false);
disj &= p2.isBlockAlive()
.implies(disjoint(addr, sz, p2.getAddress(), p2.blockSize()));
@@ -1375,23 +1388,30 @@ void Memory::mkAxioms(const Memory &other) const {
}
};
locals_fit(*this);
- locals_fit(other);
+ locals_fit(tgt);
}
-void Memory::resetBids(unsigned last_nonlocal, bool is_source) {
- next_nonlocal_bid = last_nonlocal;
+void Memory::resetGlobals() {
+ next_nonlocal_bid = has_null_block;
next_local_bid = 0;
ptr_next_idx = 0;
next_ptr_input = 0;
- if (is_source)
- next_nonlocal_ptr = 0;
+}
+
+void Memory::syncWithSrc(const Memory &src) {
+ assert(src.state->isSource() && !state->isSource());
+ resetGlobals();
+ // The bid of tgt global starts with num_nonlocals_src
+ next_nonlocal_bid = num_nonlocals_src;
+ max_nonlocal_bid = src.max_nonlocal_bid;
+ next_nonlocal_ptr = src.next_nonlocal_ptr;
}
void Memory::markByVal(unsigned bid) {
byval_blks.emplace_back(bid);
}
-expr Memory::mkInput(const char *name, const ParamAttrs &attrs) const {
+expr Memory::mkInput(const char *name, const ParamAttrs &attrs) {
unsigned max_bid = has_null_block + num_globals_src + next_ptr_input++;
assert(max_bid < num_nonlocals_src);
Pointer p(*this, name, false, false, false, attr_to_bitvec(attrs));
@@ -1425,8 +1445,7 @@ pair<expr, expr> Memory::mkUndefInput(const ParamAttrs &attrs) const {
}
pair<expr,expr>
-Memory::mkFnRet(const char *name,
- const vector<PtrInput> &ptr_inputs) const {
+Memory::mkFnRet(const char *name, const vector<PtrInput> &ptr_inputs) {
bool has_local = false;
auto escaped = escaped_local_blks;
@@ -1481,10 +1500,8 @@ Memory::mkFnRet(const char *name,
}
}
- unsigned max_bid
- = has_null_block + num_globals_src + next_ptr_input + next_nonlocal_ptr++;
-
- expr nonlocal = bid.ule(min(max_bid, num_nonlocals_src-1));
+ unsigned max_bid = nextNonlocalPtr();
+ expr nonlocal = bid.ule(max_bid);
max_nonlocal_bid.emplace(bid, max_bid);
state->addAxiom(expr::mkIf(p.isLocal(), expr::mk_or(local), nonlocal));
@@ -1662,8 +1679,10 @@ Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
}
} else {
state->addAxiom(p.blockSize() == size_zext);
+ if (!has_null_block || bid != 0) {
state->addAxiom(p.isBlockAligned(align, true));
state->addAxiom(p.getAllocType() == alloc_ty);
+ }
if (align_bits && observes_addresses())
state->addAxiom(p.getAddress().extract(align_bits - 1, 0) == 0);
@@ -1771,7 +1790,7 @@ void Memory::store(const expr &p, const StateValue &v, const Type &type,
}
StateValue Memory::load(const Pointer &ptr, const Type &type, set<expr> &undef,
- unsigned align) const {
+ unsigned align) {
unsigned bytecount = getStoreByteSize(type);
auto aty = type.getAsAggregateType();
@@ -1791,11 +1810,27 @@ StateValue Memory::load(const Pointer &ptr, const Type &type, set<expr> &undef,
bool is_ptr = type.isPtrType();
auto loadedBytes = load(ptr, bytecount, undef, align, little_endian,
is_ptr ? DATA_PTR : DATA_INT);
- return bytesToValue(*this, loadedBytes, type);
+ auto val = bytesToValue(*this, loadedBytes, type);
+
+ if (is_ptr && !val.non_poison.isFalse()) {
+ Pointer p(*this, val.value);
+ auto islocal = p.isLocal();
+ if (!islocal.isTrue()) {
+ auto bid = p.getShortBid();
+ auto [I, inserted] = max_nonlocal_bid.try_emplace(bid, 0);
+ if (inserted) {
+ unsigned max_bid = nextNonlocalPtr();
+ I->second = max_bid;
+ state->addAxiom(islocal || bid.ule(max_bid));
+ }
+ }
+ }
+
+ return val;
}
pair<StateValue, AndExpr>
-Memory::load(const expr &p, const Type &type, unsigned align) const {
+Memory::load(const expr &p, const Type &type, unsigned align) {
assert(!memory_unused());
Pointer ptr(*this, p);
@@ -1805,7 +1840,7 @@ Memory::load(const expr &p, const Type &type, unsigned align) const {
return { state->rewriteUndef(move(ret), undef_vars), move(ubs) };
}
-Byte Memory::load(const Pointer &p, set<expr> &undef, unsigned align) const {
+Byte Memory::load(const Pointer &p, set<expr> &undef, unsigned align) {
return move(load(p, bits_byte / 8, undef, align)[0]);
}
@@ -2013,8 +2048,15 @@ Memory::refined(const Memory &other, bool skip_constants,
expr ret(true);
set<expr> undef_vars;
+ auto nonlocal_used = [](const Memory &m, unsigned bid) {
+ return bid < m.next_nonlocal_ptr;
+ };
+
unsigned bid = has_null_block + skip_constants * num_consts_src;
for (; bid < num_nonlocals_src; ++bid) {
+ if (!nonlocal_used(*this, bid) && !nonlocal_used(other, bid))
+ continue;
+
expr bid_expr = expr::mkUInt(bid, bits_for_bid);
Pointer p(*this, bid_expr, offset);
Pointer q(other, p());
@@ -2111,12 +2153,20 @@ Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
if (els.escaped_local_blks[i])
ret.escaped_local_blks[i] = true;
}
- return ret;
+
+ for (const auto &[expr, vect] : els.local_bid_alias) {
+ auto [I, inserted] = ret.local_bid_alias.try_emplace(expr, vect);
+ if (!inserted)
+ merge_bool_vects(I->second, vect);
}
-void Memory::resetState() {
- max_nonlocal_bid.clear();
- local_bid_alias.clear();
+ for (const auto &[expr, bid] : els.max_nonlocal_bid) {
+ auto [I, inserted] = ret.max_nonlocal_bid.try_emplace(expr, bid);
+ if (!inserted && bid > I->second)
+ I->second = bid;
+ }
+ ret.next_nonlocal_ptr = max(then.next_nonlocal_ptr, els.next_nonlocal_ptr);
+ return ret;
}
bool Memory::operator<(const Memory &rhs) const {
@@ -2128,13 +2178,15 @@ bool Memory::operator<(const Memory &rhs) const {
non_local_block_liveness, local_block_liveness, local_blk_addr,
local_blk_size, local_blk_align, local_blk_kind,
non_local_blk_size, non_local_blk_align,
- non_local_blk_kind, byval_blks, escaped_local_blks) <
+ non_local_blk_kind, byval_blks, escaped_local_blks,
+ local_bid_alias, max_nonlocal_bid, next_nonlocal_ptr) <
tie(rhs.non_local_block_val, rhs.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_size, rhs.non_local_blk_align,
- rhs.non_local_blk_kind, rhs.byval_blks, rhs.escaped_local_blks);
+ rhs.non_local_blk_kind, rhs.byval_blks, rhs.escaped_local_blks,
+ rhs.local_bid_alias, rhs.max_nonlocal_bid, rhs.next_nonlocal_ptr);
}
#define P(name, expr) do { \

MODIFY
ir/memory.h
ir/memory.h
#include "ir/type.h"
#include "smt/expr.h"
#include "smt/exprs.h"
+#include <map>
#include <optional>
#include <ostream>
#include <set>
@@ -236,6 +237,12 @@ class Memory {
std::vector<unsigned> byval_blks;
std::vector<bool> escaped_local_blks;
+ std::map<smt::expr, std::vector<bool>> local_bid_alias;
+
+ std::map<smt::expr, unsigned> max_nonlocal_bid;
+ unsigned next_nonlocal_ptr;
+ unsigned nextNonlocalPtr();
+
unsigned numLocals() const;
unsigned numNonlocals() const;
@@ -246,14 +253,14 @@ class Memory {
template <typename Fn>
void access(const Pointer &ptr, unsigned btyes, unsigned align, bool write,
- Fn &fn) const;
+ Fn &fn);
std::vector<Byte> load(const Pointer &ptr, unsigned bytes,
std::set<smt::expr> &undef, unsigned align,
bool left2right = true,
- DataType type = DATA_ANY) const;
+ DataType type = DATA_ANY);
StateValue load(const Pointer &ptr, const Type &type,
- std::set<smt::expr> &undef, unsigned align) const;
+ std::set<smt::expr> &undef, unsigned align);
DataType data_type(const std::vector<std::pair<unsigned, smt::expr>> &data,
bool full_store) const;
@@ -295,10 +302,11 @@ public:
void mkAxioms(const Memory &other) const;
- static void resetBids(unsigned last_nonlocal, bool is_source);
+ static void resetGlobals();
+ void syncWithSrc(const Memory &src);
void markByVal(unsigned bid);
- smt::expr mkInput(const char *name, const ParamAttrs &attrs) const;
+ smt::expr mkInput(const char *name, const ParamAttrs &attrs);
std::pair<smt::expr, smt::expr> mkUndefInput(const ParamAttrs &attrs) const;
struct PtrInput {
@@ -315,8 +323,7 @@ public:
};
std::pair<smt::expr, smt::expr>
- mkFnRet(const char *name,
- const std::vector<PtrInput> &ptr_inputs) const;
+ mkFnRet(const char *name, const std::vector<PtrInput> &ptr_inputs);
CallState mkCallState(const std::vector<PtrInput> *ptr_inputs, bool nofree)
const;
void setState(const CallState &st);
@@ -342,12 +349,11 @@ public:
static unsigned getStoreByteSize(const Type &ty);
void store(const smt::expr &ptr, const StateValue &val, const Type &type,
unsigned align, const std::set<smt::expr> &undef_vars);
- std::pair<StateValue, smt::AndExpr> load(const smt::expr &ptr,
- const Type &type, unsigned align) const;
+ std::pair<StateValue, smt::AndExpr>
+ load(const smt::expr &ptr, const Type &type, unsigned align);
// raw load
- Byte load(const Pointer &p, std::set<smt::expr> &undef_vars,
- unsigned align) const;
+ Byte load(const Pointer &p, std::set<smt::expr> &undef_vars, unsigned align);
void memset(const smt::expr &ptr, const StateValue &val,
const smt::expr &bytesize, unsigned align,
@@ -375,8 +381,6 @@ public:
static Memory mkIf(const smt::expr &cond, const Memory &then,
const Memory &els);
- static void resetState();
-
// for container use only
bool operator<(const Memory &rhs) const;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -38,7 +38,7 @@ State::State(Function &f, bool source)
return_val(f.getType().getDummyValue(false)), return_memory(memory) {}
void State::resetGlobals() {
- Memory::resetBids(has_null_block, true);
+ Memory::resetGlobals();
}
const StateValue& State::exec(const Value &v) {
@@ -377,8 +377,7 @@ void State::syncSEdataWithSrc(const State &src) {
}
}
- // The bid of tgt global starts with num_nonlocals_src
- Memory::resetBids(num_nonlocals_src, false);
+ memory.syncWithSrc(src.memory);
}
void State::mkAxioms(State &tgt) {

MODIFY
ir/state.h
ir/state.h
@@ -191,10 +191,6 @@ public:
void mkAxioms(State &tgt);
smt::expr simplifyWithAxioms(smt::expr &&e) const;
- struct cleanup_state {
- ~cleanup_state() { Memory::resetState(); }
- };
-
private:
void addJump(const BasicBlock &dst, smt::expr &&domain);
};

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -540,7 +540,7 @@ static void calculateAndInitConstants(Transform &t) {
}
}
- unsigned num_ptrinputs = 0;
+ num_ptrinputs = 0;
for (auto &arg : t.src.getInputs()) {
num_ptrinputs += num_ptrs(arg.getType());
}
@@ -819,7 +819,6 @@ Errors TransformVerify::verify() const {
StopWatch symexec_watch;
calculateAndInitConstants(t);
State::resetGlobals();
- State::cleanup_state cleanup;
State src_state(t.src, true), tgt_state(t.tgt, false);
try {

MODIFY
util/compiler.cpp
util/compiler.cpp
# include <intrin.h>
#endif
+using namespace std;
+
namespace util {
unsigned ilog2(uint64_t n) {
@@ -83,4 +85,11 @@ uint64_t gcd(uint64_t n, uint64_t m) {
return gcd(m, n % m);
}
+void merge_bool_vects(vector<bool> &tgt, const vector<bool> &src) {
+ for (unsigned i = 0, e = tgt.size(); i != e; ++i) {
+ if (src[i])
+ tgt[i] = true;
+ }
+}
+
}

MODIFY
util/compiler.h
util/compiler.h
#include <cassert>
#include <cstdint>
+#include <vector>
#ifdef _MSC_VER
# define UNREACHABLE() __assume(0)
@@ -56,4 +57,6 @@ uint64_t add_saturate(uint64_t a, uint64_t b);
uint64_t divide_up(uint64_t n, uint64_t amount); // division with ceiling
uint64_t round_up(uint64_t n, uint64_t amount);
uint64_t gcd(uint64_t a, uint64_t b);
+
+void merge_bool_vects(std::vector<bool> &tgt, const std::vector<bool> &src);
}

memory: implement partial order reduction for pointer loads