memory: skip disjointness constraints if addresses aren't observed
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -158,6 +158,10 @@ StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
}
}
+static bool observes_addresses() {
+ return IR::has_ptr2int || IR::has_int2ptr;
+}
+
namespace IR {
@@ -493,19 +497,20 @@ Memory::Memory(State &state, bool little_endian)
// value.
local_avail_space = expr::mkVar("local_avail_space", bitsPtrSize() - 1);
- if (state.isSource()) {
+ if (state.isSource())
+ state.addAxiom(Pointer::mkNullPointer(*this).block_size(false) == 0);
+
+ if (state.isSource() && observes_addresses()) {
// Initialize a memory block for null pointer.
// TODO: in twin memory model, this is not needed.
- auto nullPtr = Pointer::mkNullPointer(*this);
- state.addAxiom(nullPtr.get_address(false) == 0);
- state.addAxiom(nullPtr.block_size(false) == 0);
+ state.addAxiom(Pointer::mkNullPointer(*this).get_address(false) == 0);
// 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) {
Pointer p1(*this, bid, false);
- expr disj(true);
+ expr disj = p1.get_address() != 0;
for (unsigned bid2 = bid + 1; bid2 < non_local_bid_upperbound; ++bid2) {
Pointer p2(*this, bid2, false);
@@ -522,6 +527,21 @@ Memory::Memory(State &state, bool little_endian)
}
}
+ // ensure globals fit in their reserved space
+ if (state.isSource()) {
+ auto sum_globals = expr::mkUInt(0, bitsPtrSize() - 1);
+
+ unsigned non_local_bid_upperbound = 1 << (bits_for_bid - 1);
+ for (unsigned bid = 1; bid < non_local_bid_upperbound; ++bid) {
+ Pointer p(*this, bid, false);
+ auto sz = p.block_size().extract(bitsPtrSize() - 2, 0);
+ 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);
}
@@ -603,6 +623,7 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
allocated &= size_upperbound.ule(local_avail_space.zext(1));
// Disjointness of block's address range with other local blocks
+ if (observes_addresses()) {
auto zero = expr::mkUInt(0, bitsOffset());
auto one = expr::mkUInt(1, 1);
expr disj(true);
@@ -614,6 +635,7 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
p2.block_size()));
}
state->addPre(allocated.implies(disj));
+ }
local_blk_addr.add(expr(short_bid), move(blk_addr));
local_blk_size.add(expr(short_bid), size_zext.trunc(bits_size_t - 1));
@@ -629,6 +651,7 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
local_avail_space);
// addr + size does not overflow.
+ if (observes_addresses())
state->addPre(p.get_address().add_no_uoverflow(p.block_size()));
} else {
@@ -637,8 +660,7 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
// The memory block was initially alive.
state->addAxiom(allocated.implies(mk_liveness_array().load(short_bid) &&
p.is_aligned(align) &&
- p.block_size() == size_zext &&
- p.get_address() != 0));
+ p.block_size() == size_zext));
state->addAxiom(p.get_alloc_type() == alloc_ty);
}
return expr::mkIf(allocated, p(), Pointer::mkNullPointer(*this)());

MODIFY
ir/state.cpp
ir/state.cpp
@@ -19,16 +19,21 @@ unsigned num_nonlocals;
unsigned bits_for_bid;
unsigned bits_for_offset;
bool nullptr_is_used;
+bool has_int2ptr;
+bool has_ptr2int;
void initConstants(unsigned num_globals, unsigned num_ptrinputs,
unsigned num_max_nonlocals_inst, unsigned num_locals,
- bool nullptr_is_used) {
+ bool nullptr_is_used, bool has_int2ptr, bool has_ptr2int) {
IR::bits_for_offset = 64;
IR::num_max_nonlocals_inst = num_max_nonlocals_inst;
IR::num_locals = num_locals;
// Include null block
IR::num_nonlocals = num_globals + num_ptrinputs + num_max_nonlocals_inst + 1;
+
IR::nullptr_is_used = nullptr_is_used;
+ IR::has_int2ptr = has_int2ptr;
+ IR::has_ptr2int = has_ptr2int;
unsigned maxblks = max(num_locals, num_nonlocals);
if (maxblks == 1)

MODIFY
ir/state.h
ir/state.h
@@ -29,10 +29,12 @@ extern unsigned bits_for_bid;
// The number of bits needed for encoding pointer's offset.
extern unsigned bits_for_offset;
extern bool nullptr_is_used;
+extern bool has_int2ptr;
+extern bool has_ptr2int;
void initConstants(unsigned num_globals, unsigned num_ptrinputs,
unsigned num_max_nonlocals_inst, unsigned num_locals,
- bool nullptr_is_used);
+ bool nullptr_is_used, bool has_int2ptr, bool has_ptr2int);
class Value;

MODIFY
tests/alive-tv/memory/freshbid-malloc-2.src.ll
tests/alive-tv/memory/freshbid-malloc-2.src.ll
-; TEST-ARGS: -disable-undef-input
+; TEST-ARGS: -smt-to=10000
; target: 64 bits ptr addr
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"

MODIFY
tests/alive-tv/memory/pre-bigendian.src.ll
tests/alive-tv/memory/pre-bigendian.src.ll
+; TEST-ARGS: -disable-undef-input
+
; This was excerpted from GVN/PRE/rle.ll
target datalayout = "E-p:32:32:32-p1:16:16:16-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:32:64-f32:32:32-f64:64:64-n32"

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -379,14 +379,18 @@ static void calculateAndInitConstants(Transform &t) {
}
bool nullptr_is_used = false;
+ bool has_int2ptr = false;
+ bool has_ptr2int = false;
+
for (auto fn : { &t.src, &t.tgt }) {
for (auto BB : fn->getBBs()) {
for (auto &I : BB->instrs()) {
for (auto op : I.operands()) {
- if (has_nullptr(op)) {
- nullptr_is_used = true;
- break;
+ nullptr_is_used |= has_nullptr(op);
}
+ if (auto conv = dynamic_cast<const ConversionOp*>(&I)) {
+ has_int2ptr |= conv->getOp() == ConversionOp::Int2Ptr;
+ has_ptr2int |= conv->getOp() == ConversionOp::Ptr2Int;
}
}
}
@@ -396,17 +400,17 @@ static void calculateAndInitConstants(Transform &t) {
for (auto gvs : { &globals_src , &globals_tgt }) {
for (auto gv : *gvs) {
if (auto init = gv->initVal()) {
- if (has_nullptr(init)) {
- nullptr_is_used = true;
- break;
- }
+ if (nullptr_is_used |= has_nullptr(init))
+ goto exit_gv_loop;
}
}
}
}
+exit_gv_loop:
initConstants(num_globals, num_ptrinputs, num_inst_nonlocals,
- max(num_locals_src, num_locals_tgt), nullptr_is_used);
+ max(num_locals_src, num_locals_tgt), nullptr_is_used,
+ has_int2ptr, has_ptr2int);
}

memory: skip disjointness constraints if addresses aren't observed