memory: shrink number of bits for block size whenever posssible
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -11,6 +11,7 @@ unsigned num_nonlocals;
unsigned bits_for_ptrattrs;
unsigned bits_for_bid;
unsigned bits_for_offset;
+unsigned bits_program_pointer;
unsigned bits_size_t;
unsigned bits_byte;
bool little_endian;

MODIFY
ir/globals.h
ir/globals.h
@@ -23,7 +23,10 @@ extern unsigned bits_for_bid;
// Number of bits needed for encoding a pointer's offset
extern unsigned bits_for_offset;
-/// sizeof(size_t). This is assume to be equal to pointer size
+/// Size of a program pointer in bytes
+extern unsigned bits_program_pointer;
+
+/// sizeof(size_t)
extern unsigned bits_size_t;
/// Number of bits for a byte.

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -1926,6 +1926,7 @@ StateValue GEP::toSMT(State &s) const {
auto inc = multiplier * val;
if (inbounds) {
+ if (sz != 0)
non_poison &= val.sextOrTrunc(v.bits()) == v;
non_poison &= multiplier.mul_no_soverflow(val);
non_poison &= ptr.add_no_overflow(inc);

MODIFY
ir/instr.h
ir/instr.h
@@ -386,6 +386,7 @@ public:
: Instr(type, std::move(name)), size(&size), align(align),
initially_dead(initially_dead) {}
+ Value& getSize() const { return *size; }
bool initDead() const { return initially_dead; }
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;
@@ -405,6 +406,7 @@ public:
Malloc(Type &type, std::string &&name, Value &size, bool isNonNull)
: Instr(type, std::move(name)), size(&size), isNonNull(isNonNull) {}
+ Value& getSize() const { return *size; }
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;
void print(std::ostream &os) const override;
@@ -420,6 +422,8 @@ public:
Calloc(Type &type, std::string &&name, Value &num, Value &size)
: Instr(type, std::move(name)), num(&num), size(&size) {}
+ Value& getNum() const { return *num; }
+ Value& getSize() const { return *size; }
std::vector<Value*> operands() const override;
void rauw(const Value &what, Value &with) override;
void print(std::ostream &os) const override;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -37,7 +37,7 @@ Byte::Byte(const Memory &m, expr &&byterepr) : m(m), p(move(byterepr)) {
Byte::Byte(const Pointer &ptr, unsigned i, const expr &non_poison)
: m(ptr.getMemory()) {
// TODO: support pointers larger than 64 bits.
- assert(bits_size_t <= 64 && bits_size_t % 8 == 0);
+ assert(bits_program_pointer <= 64 && bits_program_pointer % 8 == 0);
if (!does_ptr_mem_access) {
p = expr::mkUInt(0, bitsByte());
@@ -195,7 +195,7 @@ static vector<Byte> valueToBytes(const StateValue &val, const Type &fromType,
vector<Byte> bytes;
if (fromType.isPtrType()) {
Pointer p(mem, val.value);
- unsigned bytesize = bits_size_t / bits_byte;
+ unsigned bytesize = bits_program_pointer / bits_byte;
for (unsigned i = 0; i < bytesize; ++i)
bytes.emplace_back(p, i, val.non_poison);
@@ -221,7 +221,7 @@ static StateValue bytesToValue(const Memory &m, const vector<Byte> &bytes,
assert(!bytes.empty());
if (toType.isPtrType()) {
- assert(bytes.size() == bits_size_t / bits_byte);
+ assert(bytes.size() == bits_program_pointer / bits_byte);
auto nullp = Pointer::mkNullPointer(m);
expr loaded_ptr;
// The result is not poison if all of these hold:
@@ -903,7 +903,10 @@ void Memory::mkAxioms(const Memory &other) const {
Pointer(other, bid, false).block_alignment()));
}
- if (observes_addresses() && num_nonlocals > 0) {
+ if (!observes_addresses())
+ return;
+
+ if (num_nonlocals > 0)
state->addAxiom(Pointer::mkNullPointer(*this).get_address(false) == 0);
// Non-local blocks are disjoint.
@@ -925,7 +928,6 @@ void Memory::mkAxioms(const Memory &other) const {
}
state->addAxiom(p1.is_block_alive().implies(disj));
}
- }
// ensure globals fit in their reserved space
{
@@ -1138,7 +1140,7 @@ void Memory::free(const expr &ptr, bool unconstrained) {
unsigned Memory::getStoreByteSize(const Type &ty) {
if (ty.isPtrType())
- return divide_up(bits_size_t, 8);
+ return divide_up(bits_program_pointer, 8);
if (auto aty = ty.getAsAggregateType()) {
unsigned sz = 0;

MODIFY
tests/alive-tv/memory/memset-fn.src.ll
tests/alive-tv/memory/memset-fn.src.ll
-; TEST-ARGS: -smt-to=10000
-
target datalayout = "e-m:e-p270:32:32-p271:32:32-p272:64:64-i64:64-f80:128-n8:16:32:64-S128"
define i32* @f(i32* %ptr, i32 %val, i64 %len) {

MODIFY
tests/alive-tv/memory/punning-intptr.src.ll
tests/alive-tv/memory/punning-intptr.src.ll
+; TEST-ARGS: -smt-to=10000
+
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
define i8* @int_ptr_punning(i8* %ptr, i64 %n) {

MODIFY
tests/alive-tv/memory/store-removal.src.ll
tests/alive-tv/memory/store-removal.src.ll
-; TEST-ARGS: -disable-poison-input
-
define void @f(i8* %p) {
%v = load i8, i8* %p
store i8 %v, i8* %p

MODIFY
tests/alive-tv/memory/storeptr.src.ll
tests/alive-tv/memory/storeptr.src.ll
+; TEST-ARGS: -smt-to=10000 -disable-undef-input
+
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
define i64 @f(i64** %pptr) {

MODIFY
tests/alive-tv/memory/zeroinit-memset.src.ll
tests/alive-tv/memory/zeroinit-memset.src.ll
; From Transforms/MemCpyOpt/fca2memcpy.ll
-; TEST-ARGS: -smt-to=15000 -disable-poison-input
target datalayout = "e-i64:64-f80:128-n8:16:32:64"
%S = type { i8*, i8, i32 }

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -454,12 +454,14 @@ static optional<int64_t> get_int(const Value &val) {
return {};
}
+static uint64_t max_mem_access, max_alloc_size;
+
static uint64_t max_gep(const Instr &inst) {
if (auto conv = dynamic_cast<const ConversionOp*>(&inst)) {
// if addresses are observed, then expose full ptr range
if (conv->getOp() == ConversionOp::Int2Ptr ||
conv->getOp() == ConversionOp::Ptr2Int)
- return UINT64_MAX;
+ return max_mem_access = max_alloc_size = UINT64_MAX;
}
if (auto gep = dynamic_cast<const GEP*>(&inst)) {
@@ -474,20 +476,52 @@ static uint64_t max_gep(const Instr &inst) {
return abs(off);
}
if (auto load = dynamic_cast<const Load*>(&inst)) {
- return Memory::getStoreByteSize(load->getType());
+ max_mem_access = max(max_mem_access,
+ (uint64_t)Memory::getStoreByteSize(load->getType()));
+ return 0;
}
if (auto store = dynamic_cast<const Store*>(&inst)) {
- return Memory::getStoreByteSize(store->getValue().getType());
+ max_mem_access
+ = max(max_mem_access,
+ (uint64_t)Memory::getStoreByteSize(store->getValue().getType()));
+ return 0;
}
if (auto cpy = dynamic_cast<const Memcpy*>(&inst)) {
if (auto bytes = get_int(cpy->getBytes()))
- return *bytes;
- return UINT64_MAX;
+ max_mem_access = max(max_mem_access, (uint64_t)abs(*bytes));
+ else
+ max_mem_access = UINT64_MAX;
+ return 0;
}
if (auto memset = dynamic_cast<const Memset *>(&inst)) {
if (auto bytes = get_int(memset->getBytes()))
- return *bytes;
- return UINT64_MAX;
+ max_mem_access = max(max_mem_access, (uint64_t)abs(*bytes));
+ else
+ max_mem_access = UINT64_MAX;
+ return 0;
+ }
+
+ Value *size;
+ uint64_t mul = 1;
+ if (auto alloc = dynamic_cast<const Alloc*>(&inst)) {
+ size = &alloc->getSize();
+ } else if (auto alloc = dynamic_cast<const Malloc*>(&inst)) {
+ size = &alloc->getSize();
+ } else if (auto alloc = dynamic_cast<const Calloc*>(&inst)) {
+ size = &alloc->getSize();
+ if (auto n = get_int(alloc->getNum())) {
+ mul = *n;
+ } else {
+ max_alloc_size = UINT64_MAX;
+ }
+ } else {
+ return 0;
+ }
+
+ if (auto bytes = get_int(*size)) {
+ max_alloc_size = max(max_alloc_size, mul * abs(*bytes));
+ } else {
+ max_alloc_size = UINT64_MAX;
}
return 0;
}
@@ -498,7 +532,7 @@ static void calculateAndInitConstants(Transform &t) {
unsigned num_globals = globals_src.size();
// TODO: get this from data layout, varies among address spaces
- bits_size_t = 64;
+ bits_program_pointer = 64;
for (auto GVT : globals_tgt) {
auto I = find_if(globals_src.begin(), globals_src.end(),
@@ -552,6 +586,8 @@ static void calculateAndInitConstants(Transform &t) {
// The number of local blocks.
unsigned num_locals_src = 0, num_locals_tgt = 0;
uint64_t max_gep_src = 0, max_gep_tgt = 0;
+ max_alloc_size = 0;
+ max_mem_access = 0;
for (auto BB : t.src.getBBs()) {
for (auto &i : BB->instrs()) {
@@ -644,8 +680,14 @@ static void calculateAndInitConstants(Transform &t) {
// reserve a multiple of 4 for the number of offset bits to make SMT &
// counterexamples more readable
// Allow an extra bit for the sign
- auto max_geps = ilog2_ceil(max(max_gep_src, max_gep_tgt), true) + 1;
- bits_for_offset = min(round_up(max_geps, 4), (uint64_t)bits_size_t);
+ auto max_geps
+ = ilog2_ceil(add_saturate(max(max_gep_src, max_gep_tgt), max_mem_access),
+ true) + 1;
+ bits_for_offset = min(round_up(max_geps, 4), (uint64_t)bits_program_pointer);
+
+ // we need an extra bit because 1st bit of size is always 0
+ bits_size_t = ilog2_ceil(max_alloc_size, true);
+ bits_size_t = min(max(bits_for_offset, bits_size_t)+1, bits_program_pointer);
// size of byte
bits_byte = 8 * (does_mem_access ? (unsigned)min_access_size : 1);
@@ -658,6 +700,9 @@ static void calculateAndInitConstants(Transform &t) {
"num_nonlocals: " << num_nonlocals << "\n"
"bits_for_bid: " << bits_for_bid << "\n"
"bits_for_offset: " << bits_for_offset << "\n"
+ "bits_program_pointer: " << bits_program_pointer << "\n"
+ "max_alloc_size: " << max_alloc_size << "\n"
+ "max_mem_access: " << max_mem_access << "\n"
"bits_size_t: " << bits_size_t << "\n"
"bits_byte: " << bits_byte << "\n"
"little_endian: " << little_endian << "\n"

memory: shrink number of bits for block size whenever posssible