memory: change encoding of writability of blocks
MODIFY
ir/function.cpp
ir/function.cpp
@@ -122,7 +122,7 @@ vector<string_view> Function::getGlobalVarNames() const {
vector<string_view> gvnames;
auto gvs = getGlobalVars();
transform(gvs.begin(), gvs.end(), back_inserter(gvnames),
- [](auto itm) { return string_view(itm->getName()).substr(1); });
+ [](auto &itm) { return string_view(itm->getName()).substr(1); });
return gvnames;
}

MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -10,9 +10,10 @@ using namespace std;
namespace IR {
-unsigned num_max_nonlocals_inst;
unsigned num_locals_src;
unsigned num_locals_tgt;
+unsigned num_consts_src;
+unsigned num_extra_nonconst_tgt;
unsigned num_nonlocals;
unsigned num_nonlocals_src;
unsigned bits_for_ptrattrs;

MODIFY
ir/globals.h
ir/globals.h
@@ -7,12 +7,15 @@ namespace smt { class expr; }
namespace IR {
-/// Upperbound of the number of non-local pointers returned by instructions
-extern unsigned num_max_nonlocals_inst;
-
/// Upperbound of the number of local blocks
extern unsigned num_locals_src, num_locals_tgt;
+/// Number of constant global variables in src
+extern unsigned num_consts_src;
+
+/// Number of non-constant globals introduced in tgt
+extern unsigned num_extra_nonconst_tgt;
+
// Upperbound of the number of nonlocal blocks
extern unsigned num_nonlocals;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -859,11 +859,12 @@ expr Pointer::blockRefined(const Pointer &other) const {
}
expr Pointer::isWritable() const {
- auto this_bid = getShortBid();
- expr non_local(true);
- for (auto bid : m.non_local_blk_nonwritable) {
- non_local &= this_bid != bid;
- }
+ auto bid = getShortBid();
+ expr non_local
+ = num_consts_src == 1 ? bid != has_null_block :
+ (num_consts_src ? bid.ugt(has_null_block + num_consts_src - 1) : true);
+ if (m.numNonlocals() > num_nonlocals_src + num_extra_nonconst_tgt)
+ non_local &= bid.ult(num_nonlocals_src + num_extra_nonconst_tgt);
return isLocal() || non_local;
}
@@ -1424,8 +1425,11 @@ Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
if (align_bits && observes_addresses())
state->addAxiom(p.getAddress().extract(align_bits - 1, 0) == 0);
- if (blockKind == CONSTGLOBAL)
- non_local_blk_nonwritable.emplace(bid);
+ bool cond = (has_null_block && bid == 0) ||
+ (bid >= has_null_block + num_consts_src &&
+ bid < num_nonlocals_src + num_extra_nonconst_tgt);
+ if (blockKind == CONSTGLOBAL) assert(!cond); else assert(cond);
+ (void)cond;
}
store_bv(p, allocated, local_block_liveness, non_local_block_liveness);
@@ -1660,18 +1664,8 @@ Memory::refined(const Memory &other, bool skip_constants,
expr offset = ptr.getOffset();
expr ret(true);
- auto is_constglb = [](const Memory &m, unsigned bid) {
- return
- find(m.non_local_blk_nonwritable.begin(),
- m.non_local_blk_nonwritable.end(), bid) !=
- m.non_local_blk_nonwritable.end();
- };
-
- for (unsigned bid = has_null_block; bid < num_nonlocals_src; ++bid) {
- if (skip_constants && is_constglb(*this, bid)) {
- assert(is_constglb(other, bid));
- continue;
- }
+ unsigned bid = has_null_block + skip_constants * num_consts_src;
+ for (; bid < num_nonlocals_src; ++bid) {
expr bid_expr = expr::mkUInt(bid, bits_for_bid);
Pointer p(*this, bid_expr, offset);
Pointer q(other, p());
@@ -1729,8 +1723,6 @@ Memory Memory::mkIf(const expr &cond, const Memory &then, const Memory &els) {
ret.local_blk_size.add(els.local_blk_size);
ret.local_blk_align.add(els.local_blk_align);
ret.local_blk_kind.add(els.local_blk_kind);
- ret.non_local_blk_nonwritable.insert(els.non_local_blk_nonwritable.begin(),
- els.non_local_blk_nonwritable.end());
ret.non_local_blk_size.add(els.non_local_blk_size);
ret.non_local_blk_align.add(els.non_local_blk_align);
ret.non_local_blk_kind.add(els.non_local_blk_kind);
@@ -1752,13 +1744,13 @@ bool Memory::operator<(const Memory &rhs) const {
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_size, non_local_blk_align,
non_local_blk_kind, byval_blks, escaped_local_blks, undef_vars) <
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,
+ 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.undef_vars);
@@ -1837,13 +1829,6 @@ ostream& operator<<(ostream &os, const Memory &m) {
}
os << "\nLOCAL BLOCK ADDR: " << m.local_blk_addr << '\n';
}
- if (!m.non_local_blk_nonwritable.empty()) {
- os << "CONST NON-LOCALS:";
- for (auto bid : m.non_local_blk_nonwritable) {
- os << ' ' << bid;
- }
- os << '\n';
- }
return os;
}

MODIFY
ir/memory.h
ir/memory.h
@@ -205,7 +205,6 @@ class Memory {
smt::FunctionExpr local_blk_align;
smt::FunctionExpr local_blk_kind;
- std::set<unsigned> non_local_blk_nonwritable;
smt::FunctionExpr non_local_blk_size;
smt::FunctionExpr non_local_blk_align;
smt::FunctionExpr non_local_blk_kind;

MODIFY
llvm_util/llvm2alive.cpp
llvm_util/llvm2alive.cpp
@@ -1068,7 +1068,7 @@ public:
auto storedval = get_operand(gv->getInitializer());
if (!storedval) {
*out << "ERROR: Unsupported constant: " << *gv->getInitializer()
- << "\n";
+ << '\n';
return {};
}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -494,11 +494,22 @@ static void calculateAndInitConstants(Transform &t) {
assert(bits_program_pointer == t.tgt.bitsPointers());
heap_block_alignment = 8;
+ num_consts_src = 0;
+ num_extra_nonconst_tgt = 0;
+
+ for (auto GV : globals_src) {
+ if (GV->isConst())
+ ++num_consts_src;
+ }
+
for (auto GVT : globals_tgt) {
auto I = find_if(globals_src.begin(), globals_src.end(),
[GVT](auto *GV) -> bool { return GVT->getName() == GV->getName(); });
- if (I == globals_src.end())
+ if (I == globals_src.end()) {
++num_globals;
+ if (!GVT->isConst())
+ ++num_extra_nonconst_tgt;
+ }
}
unsigned num_ptrinputs = 0;
@@ -507,7 +518,7 @@ static void calculateAndInitConstants(Transform &t) {
}
// The number of instructions that can return a pointer to a non-local block.
- num_max_nonlocals_inst = 0;
+ unsigned num_max_nonlocals_inst = 0;
// The number of local blocks.
num_locals_src = 0;
num_locals_tgt = 0;

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -15,9 +15,22 @@ namespace util {
void sym_exec(State &s) {
Function &f = const_cast<Function&>(s.getFn());
+ // global constants need to be created in the right order so they get the
+ // first bids in source, and the last in target
+ set<const Value*> seen_inits;
+ for (const auto &v : f.getConstants()) {
+ if (auto gv = dynamic_cast<const GlobalVariable*>(&v)) {
+ if (gv->isConst() == s.isSource()) {
+ s.exec(v);
+ seen_inits.emplace(&v);
+ }
+ }
+ }
+
// add constants & inputs to State table first of all
for (auto &l : { f.getConstants(), f.getInputs(), f.getUndefs() }) {
for (const auto &v : l) {
+ if (!seen_inits.count(&v))
s.exec(v);
}
}

memory: change encoding of writability of blocks