memory: add axioms only after global allocation to enable const folding of block attributes
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -514,15 +514,15 @@ Memory::Memory(State &state)
non_local_block_val = mk_val_array();
non_local_block_liveness = mk_liveness_array();
{
- Pointer ptr(*this, "#idx");
- auto idx = ptr.short_ptr();
+ auto idx = Pointer(*this, "#idx").short_ptr();
if (state.isSource()) {
// All non-local blocks cannot initially contain pointers to local blocks.
auto byte = Byte(*this, non_local_block_val.load(idx));
Pointer loadedptr(*this, byte.ptr_value());
expr cond = (byte.is_ptr() && byte.ptr_nonpoison())
- .implies(!loadedptr.is_local());
+ .implies(!loadedptr.is_local() &&
+ loadedptr.get_bid().ult(num_nonlocals));
state.addAxiom(expr::mkForAll({ idx }, move(cond)));
}
@@ -551,14 +551,19 @@ Memory::Memory(State &state)
// Initialize a memory block for null pointer.
alloc(expr::mkUInt(0, bits_size_t), 1, GLOBAL, 0, nullptr, false);
- if (state.isSource() && observes_addresses()) {
- state.addAxiom(Pointer::mkNullPointer(*this).get_address(false) == 0);
+ assert(bits_for_offset <= bits_size_t);
+}
+
+void Memory::mkAxioms() const {
+ if (memory_unused() || !state->isSource())
+ return;
+
+ if (observes_addresses()) {
+ state->addAxiom(Pointer::mkNullPointer(*this).get_address(false) == 0);
- if (num_nonlocals > 1) {
// Non-local blocks are disjoint.
// Ignore null pointer block
- unsigned non_local_bid_upperbound = 1 << (bits_for_bid - 1);
- for (unsigned bid = 1; bid < non_local_bid_upperbound; ++bid) {
+ for (unsigned bid = 1; bid < num_nonlocals; ++bid) {
Pointer p1(*this, bid, false);
expr disj = p1.get_address() != 0;
@@ -567,33 +572,29 @@ Memory::Memory(State &state)
disj &= (p1.get_address() + p1.block_size()).extract(bit, bit) == 0;
// disjointness constraint
- for (unsigned bid2 = bid + 1; bid2 < non_local_bid_upperbound; ++bid2) {
+ for (unsigned bid2 = bid + 1; bid2 < num_nonlocals; ++bid2) {
Pointer p2(*this, bid2, false);
disj &= p2.is_block_alive()
.implies(disjoint(p1.get_address(), p1.block_size(),
p2.get_address(), p2.block_size()));
}
- state.addAxiom(p1.is_block_alive().implies(disj));
- }
+ state->addAxiom(p1.is_block_alive().implies(disj));
}
}
// ensure globals fit in their reserved space
- if (state.isSource() && num_nonlocals > 1) {
+ {
auto sum_globals = expr::mkUInt(0, bits_size_t - 1);
- unsigned non_local_bid_upperbound = 1 << (bits_for_bid - 1);
- for (unsigned bid = 1; bid < non_local_bid_upperbound; ++bid) {
+ for (unsigned bid = 1; bid < num_nonlocals; ++bid) {
Pointer p(*this, bid, false);
auto sz = p.block_size().extract(bits_size_t - 2, 0);
- state.addAxiom(p.is_block_alive()
+ state->addAxiom(p.is_block_alive()
.implies(sum_globals.add_no_uoverflow(sz)));
sum_globals = expr::mkIf(p.is_block_alive(), sum_globals + sz,
sum_globals);
}
}
-
- assert(bits_for_offset <= bits_size_t);
}
void Memory::resetGlobalData() {
@@ -615,6 +616,7 @@ expr Memory::mkInput(const char *name) const {
expr offset = var.extract(bits_for_offset - 1, 0);
expr bid = var.extract(bits - 1, bits_for_offset);
expr is_local = expr::mkUInt(0, 1);
+ state->addAxiom(bid.ule(num_nonlocals - 1));
return Pointer(*this, is_local.concat(bid), offset).release();
}

MODIFY
ir/memory.h
ir/memory.h
@@ -143,6 +143,8 @@ public:
Memory(State &state);
+ void mkAxioms() const;
+
static void resetGlobalData();
static void resetLocalBids();

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1049,6 +1049,9 @@ expr expr::ule(const expr &rhs) const {
if (rhs.isZero())
return *this == rhs;
+ if (rhs.isAllOnes())
+ return true;
+
return binop_fold(rhs, Z3_mk_bvule);
}
@@ -1322,10 +1325,14 @@ expr expr::mkIf(const expr &cond, const expr &then, const expr &els) {
if (cond.isFalse())
return els;
- if (then.isTrue() && els.isFalse())
- return cond;
- if (then.isFalse() && els.isTrue())
- return !cond;
+ if (then.isTrue())
+ return cond || els;
+ if (then.isFalse())
+ return !cond && els;
+ if (els.isTrue())
+ return !cond || then;
+ if (els.isFalse())
+ return cond && then;
expr notcond;
Z3_ast c, t = then(), e = els();

MODIFY
smt/exprs.cpp
smt/exprs.cpp
@@ -9,6 +9,7 @@ using namespace std;
namespace smt {
void AndExpr::add(expr &&e) {
+ if (!e.isTrue())
exprs.insert(move(e));
}
@@ -26,6 +27,7 @@ ostream &operator<<(ostream &os, const AndExpr &e) {
void OrExpr::add(expr &&e) {
+ if (!e.isFalse())
exprs.insert(move(e));
}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -438,7 +438,8 @@ static void calculateAndInitConstants(Transform &t) {
has_int2ptr = false;
has_ptr2int = false;
// Mininum access size (in bytes)
- uint64_t min_access_size = 512;
+ uint64_t min_access_size = 16;
+ bool does_mem_access = false;
for (auto fn : { &t.src, &t.tgt }) {
for (auto BB : fn->getBBs()) {
@@ -452,8 +453,10 @@ static void calculateAndInitConstants(Transform &t) {
}
auto accsz = get_access_size(I);
- if (accsz != NO_ACCESS)
+ if (accsz != NO_ACCESS) {
min_access_size = gcd(min_access_size, accsz);
+ does_mem_access = true;
+ }
}
}
}
@@ -469,7 +472,7 @@ static void calculateAndInitConstants(Transform &t) {
bits_for_offset = 64;
// size of byte
- bits_byte = 8 * (unsigned)min_access_size;
+ bits_byte = 8 * (does_mem_access ? (unsigned)min_access_size : 1);
little_endian = t.src.isLittleEndian();

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -23,6 +23,7 @@ void sym_exec(State &s) {
}
s.exec(Value::voidVal);
+ s.getMemory().mkAxioms();
bool first = true;
if (f.getFirstBB().getName() != "__globalvars_init") {

memory: add axioms only after global allocation to enable const folding of block attributes