Add static analysis to count the max number of local/non-local memory blocks
MODIFY
ir/instr.h
ir/instr.h
@@ -113,6 +113,7 @@ public:
ConversionOp(Type &type, std::string &&name, Value &val, Op op)
: Instr(type, std::move(name)), val(&val), op(op) {}
+ Op getOp() const { return op; }
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
@@ -166,16 +166,16 @@ Pointer::Pointer(const Memory &m, const char *var_name)
expr::mkFreshVar(var_name, expr::mkUInt(0, total_bits()-1)))) {}
Pointer::Pointer(const Memory &m, unsigned bid, bool local) : m(m) {
- expr bid_expr = expr::mkUInt(bid, m.bitsBid() - 1);
+ expr bid_expr = expr::mkUInt(bid, bits_for_bid - 1);
p = expr::mkUInt(local, 1).concat(bid_expr)
- .concat(expr::mkUInt(0, m.bits_for_offset));
+ .concat(expr::mkUInt(0, bits_for_offset));
}
Pointer::Pointer(const Memory &m, const expr &bid, const expr &offset)
: m(m), p(bid.concat(offset)) {}
unsigned Pointer::total_bits() const {
- return m.bitsBid() + m.bitsOffset();
+ return bits_for_bid + m.bitsOffset();
}
expr Pointer::is_local() const {
@@ -237,11 +237,11 @@ expr Pointer::short_ptr() const {
Pointer Pointer::operator+(const expr &bytes) const {
expr off = (get_offset() + bytes.zextOrTrunc(m.bits_size_t));
- return { m, get_bid(), off.trunc(m.bits_for_offset) };
+ return { m, get_bid(), off.trunc(bits_for_offset) };
}
Pointer Pointer::operator+(unsigned bytes) const {
- return *this + expr::mkUInt(bytes, m.bits_for_offset);
+ return *this + expr::mkUInt(bytes, bits_for_offset);
}
void Pointer::operator+=(const expr &bytes) {
@@ -309,7 +309,7 @@ void Pointer::is_dereferenceable(const expr &bytes0, unsigned align,
}
void Pointer::is_dereferenceable(unsigned bytes, unsigned align, bool iswrite) {
- is_dereferenceable(expr::mkUInt(bytes, m.bits_for_offset), align, iswrite);
+ is_dereferenceable(expr::mkUInt(bytes, bits_for_offset), align, iswrite);
}
// general disjoint check for unsigned integer
@@ -429,12 +429,12 @@ static expr load(const Pointer &p, expr &local, expr &non_local) {
expr Memory::mk_val_array() const {
return expr::mkArray("blk_val",
- expr::mkUInt(0, bitsBid() - 1 + bits_for_offset),
+ expr::mkUInt(0, bits_for_bid - 1 + bits_for_offset),
expr::mkUInt(0, bitsByte()));
}
expr Memory::mk_liveness_array() const {
- return expr::mkArray("blk_liveness", expr::mkUInt(0, bitsBid() - 1), true);
+ return expr::mkArray("blk_liveness", expr::mkUInt(0, bits_for_bid - 1), true);
}
// last_bid stores 1 + the last memory block id.
@@ -470,7 +470,7 @@ Memory::Memory(State &state, bool little_endian)
// all local blocks are dead in the beginning
local_block_liveness
- = expr::mkLambda({ expr::mkVar("#bid0", bitsBid() - 1) }, false);
+ = expr::mkLambda({ expr::mkVar("#bid0", bits_for_bid - 1) }, false);
// A memory space is separated into non-local area / local area.
// Non-local area is the lower half of memory (to include null pointer),
@@ -492,11 +492,9 @@ Memory::Memory(State &state, bool little_endian)
state.addAxiom(nullPtr.get_address(false) == 0);
state.addAxiom(nullPtr.block_size(false) == 0);
- // TODO: replace the magic number 2 with the result of analysis.
- // This is just set as 2 to make existing unit tests run with less timeout.
- unsigned non_local_bid_upperbound = 2;
// Non-local blocks are disjoint.
// Ignore null pointer block
+ unsigned non_local_bid_upperbound = (1 << ilog2(2 * num_nonlocals - 1)) - 1;
for (unsigned bid = 1; bid <= non_local_bid_upperbound; ++bid) {
Pointer p1(*this, bid, false);
expr disj(true);
@@ -528,6 +526,14 @@ void Memory::resetLocalBids() {
last_local_bid = 0;
}
+unsigned Memory::bitsOffset() const {
+ return bits_for_offset;
+}
+
+unsigned Memory::bitsByte() const {
+ return 1 + 1 + bits_for_bid + bitsOffset() + 3;
+}
+
expr Memory::mkInput(const char *name) const {
unsigned bits = bits_for_bid - 1 + bits_for_offset;
expr var = expr::mkVar(name, bits);
@@ -551,6 +557,7 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
auto &last_bid = is_local ? last_local_bid : last_nonlocal_bid;
unsigned bid = bidopt ? *bidopt : last_bid;
+ assert((is_local && bid < num_locals) || (!is_local && bid < num_nonlocals));
if (!bidopt)
++last_bid;
assert(bid < last_bid);

MODIFY
ir/memory.h
ir/memory.h
@@ -108,9 +108,6 @@ public:
class Memory {
State *state;
- // FIXME: these should be tuned per function
- unsigned bits_for_offset = 64;
- unsigned bits_for_bid = 12;
// bits_size_t is equivalent to the size of a pointer.
unsigned bits_size_t = 64;
@@ -176,9 +173,8 @@ public:
static Memory mkIf(const smt::expr &cond, const Memory &then,
const Memory &els);
- unsigned bitsOffset() const { return bits_for_offset; }
- unsigned bitsBid() const { return bits_for_bid; }
- unsigned bitsByte() const { return 1 + 1 + bitsBid() + bitsOffset() + 3; }
+ unsigned bitsOffset() const;
+ unsigned bitsByte() const;
unsigned bitsPtrSize() const { return bits_size_t; }
// for container use only

MODIFY
ir/state.cpp
ir/state.cpp
@@ -13,6 +13,29 @@ using namespace std;
namespace IR {
+unsigned num_max_nonlocals_inst;
+unsigned num_locals;
+unsigned num_nonlocals;
+unsigned bits_for_bid;
+unsigned bits_for_offset;
+
+void initConstants(unsigned num_globals, unsigned num_ptrinputs,
+ unsigned num_max_nonlocals_inst, unsigned num_locals) {
+ 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;
+
+ unsigned maxblks = max(num_locals, num_nonlocals);
+ if (maxblks == 1)
+ IR::bits_for_bid = 2; // local/non-local bit + one bit for bid
+ else {
+ unsigned n = ilog2(2 * maxblks - 1); // floor(log2(maxblks))
+ IR::bits_for_bid = 1 + n;
+ }
+}
+
State::State(const Function &f, bool source)
: f(f), source(source), memory(*this, f.isLittleEndian()),
return_domain(false), return_val(f.getType().getDummyValue(false)),

MODIFY
ir/state.h
ir/state.h
namespace IR {
+// The upperbound of # of non-local pointers that are returned by instructions.
+extern unsigned num_max_nonlocals_inst;
+// The upperbound of # of local blocks (max(src, tgt))
+extern unsigned num_locals;
+// The upperbound of # of nonlocal blocks
+extern unsigned num_nonlocals;
+// The number of bits needed for encoding block id.
+extern unsigned bits_for_bid;
+// The number of bits needed for encoding pointer's offset.
+extern unsigned bits_for_offset;
+
+void initConstants(unsigned num_globals, unsigned num_ptrinputs,
+ unsigned num_max_nonlocals_inst, unsigned num_locals);
+
+
class Value;
class BasicBlock;
class Function;

MODIFY
ir/type.cpp
ir/type.cpp
@@ -485,8 +485,7 @@ expr PtrType::ASVar() const {
}
unsigned PtrType::bits() const {
- // TODO: make this configurable
- return 64 + 12;
+ return bits_for_offset + bits_for_bid;
}
StateValue PtrType::getDummyValue(bool non_poison) const {

MODIFY
tests/alive-tv/memory/alloca-malloc-fail.src.ll
tests/alive-tv/memory/alloca-malloc-fail.src.ll
; target: 64 bits ptr addr
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
-define i8 @alloca_malloc(i8* %ptr0) {
+define i8 @alloca_malloc() {
%ptr = call noalias i8* @malloc(i64 1)
%i = ptrtoint i8* %ptr to i64
%cmp = icmp eq i64 %i, 0

MODIFY
tests/alive-tv/memory/alloca-malloc-fail.tgt.ll
tests/alive-tv/memory/alloca-malloc-fail.tgt.ll
; target: 64 bits ptr addr
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
-define i8 @alloca_malloc(i8* %ptr0) {
+define i8 @alloca_malloc() {
%ptr = alloca i8
store i8 20, i8* %ptr
%v = load i8, i8* %ptr

MODIFY
tests/alive-tv/memory/alloca-malloc.src.ll
tests/alive-tv/memory/alloca-malloc.src.ll
; target: 64 bits ptr addr
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
-define i8 @alloca_malloc(i8* %ptr0) {
+define i8 @alloca_malloc() {
%ptr = call noalias i8* @malloc(i64 1)
; If there is '%ptr == null` check guard, this optimization is invalid
; because source can safely return whereas alloca may raise OOM (which is UB).

MODIFY
tests/alive-tv/memory/alloca-malloc.tgt.ll
tests/alive-tv/memory/alloca-malloc.tgt.ll
; target: 64 bits ptr addr
target datalayout = "e-m:o-i64:64-f80:128-n8:16:32:64-S128"
-define i8 @alloca_malloc(i8* %ptr0) {
+define i8 @alloca_malloc() {
%ptr = alloca i8
store i8 20, i8* %ptr
%v = load i8, i8* %ptr

MODIFY
tests/alive-tv/memory/gep-struct2.src.ll
tests/alive-tv/memory/gep-struct2.src.ll
+; TEST-ARGS: -smt-to=2000
target datalayout = "e-i32:32-i128:32-i8:8"
%0 = type [10 x { i32, i128, [5 x { i32, i8, i8 }] }]

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -306,6 +306,69 @@ static void check_refinement(Errors &errs, Transform &t,
}
}
+static void calculateAndInitConstants(Transform &t) {
+ const auto &globals_tgt = t.tgt.getGlobalVars();
+ const auto &globals_src = t.src.getGlobalVars();
+ unsigned num_globals = globals_src.size();
+
+ 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())
+ ++num_globals;
+ }
+
+ unsigned num_ptrinputs = 0;
+ const auto &inputs = t.src.getInputs();
+ for (auto &arg : inputs) {
+ // An argument with aggregate type with pointer member isn't regarded
+ // as a source of non-local pointer, because its member should be extracted
+ // with extractelement / extractvalue instructions, which are also counted
+ // as source of non-local blocks.
+ num_ptrinputs += arg.getType().isPtrType();
+ }
+
+ auto returns_local = [](const Instr &inst) {
+ return dynamic_cast<const Alloc *>(&inst) != nullptr ||
+ dynamic_cast<const Malloc *>(&inst) != nullptr ||
+ dynamic_cast<const Calloc *>(&inst) != nullptr;
+ };
+ auto returns_nonlocal = [](const Instr &inst) {
+ if (!inst.getType().isPtrType())
+ return false;
+ if (auto conv = dynamic_cast<const ConversionOp *>(&inst)) {
+ if (conv->getOp() == ConversionOp::BitCast)
+ return false;
+ }
+ if (dynamic_cast<const GEP *>(&inst))
+ return false;
+ return true;
+ };
+
+ // The number of instructions that can return a pointer to a non-local block.
+ unsigned num_inst_nonlocals = 0;
+ // The number of local blocks.
+ unsigned num_locals_src = 0, num_locals_tgt = 0;
+ for (auto BB : t.src.getBBs()) {
+ const auto &instrs = BB->instrs();
+ for_each(instrs.begin(), instrs.end(), [&](const auto &i) {
+ num_locals_src += returns_local(i);
+ num_inst_nonlocals += returns_nonlocal(i);
+ });
+ }
+ for (auto BB : t.tgt.getBBs()) {
+ const auto &instrs = BB->instrs();
+ for_each(instrs.begin(), instrs.end(), [&](const auto &i) {
+ num_locals_tgt += returns_local(i);
+ num_inst_nonlocals += returns_nonlocal(i);
+ });
+ }
+
+ initConstants(num_globals, num_ptrinputs, num_inst_nonlocals,
+ max(num_locals_src, num_locals_tgt));
+}
+
+
namespace tools {
@@ -355,6 +418,7 @@ Errors TransformVerify::verify() const {
}
}
+ ::calculateAndInitConstants(t);
State::resetGlobals();
State src_state(t.src, true), tgt_state(t.tgt, false);

Add static analysis to count the max number of local/non-local memory blocks (#182)