Support introduction of global constants in target
MODIFY
ir/globals.cpp
ir/globals.cpp
@@ -13,6 +13,7 @@ namespace IR {
unsigned num_max_nonlocals_inst;
unsigned num_locals;
unsigned num_nonlocals;
+unsigned num_nonlocals_src;
unsigned bits_for_ptrattrs;
unsigned bits_for_bid;
unsigned bits_for_offset;

MODIFY
ir/globals.h
ir/globals.h
@@ -16,6 +16,9 @@ extern unsigned num_locals;
// Upperbound of the number of nonlocal blocks
extern unsigned num_nonlocals;
+// Upperbound of the number of nonlocal blocks in src (<= num_nonlocals)
+extern unsigned num_nonlocals_src;
+
/// Number of bits needed for attributes of pointers (e.g. nocapture).
extern unsigned bits_for_ptrattrs;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -366,7 +366,7 @@ unsigned Pointer::total_bits() {
expr Pointer::is_local() const {
if (num_locals == 0)
return false;
- if (num_nonlocals == 0)
+ if (m.num_nonlocals() == 0)
return true;
auto bit = total_bits() - 1;
return p.extract(bit, bit) == 1;
@@ -823,6 +823,7 @@ void Pointer::strip_attrs() {
}
Pointer Pointer::mkNullPointer(const Memory &m) {
+ // Null pointer exists if either source or target uses it.
assert(num_nonlocals > 0);
// A null pointer points to block 0 without any attribute.
return { m, 0, false };
@@ -879,6 +880,10 @@ static vector<expr> extract_possible_local_bids(Memory &m, const Byte &b) {
return ret;
}
+unsigned Memory::num_nonlocals() const {
+ return state->isSource() ? num_nonlocals_src : IR::num_nonlocals;
+}
+
void Memory::store(const Pointer &p, const expr &val, expr &local,
expr &non_local, bool index_bid) {
if (!index_bid && num_locals > 0) {
@@ -946,7 +951,7 @@ static void mk_nonlocal_val_axioms(State &s, Memory &m, expr &val) {
auto idx = Pointer(m, "#idx", false, false, expr()).short_ptr();
#if 0
- if (num_nonlocals > 0) {
+ if (m.num_nonlocals() > 0) {
expr is_ptr = does_int_mem_access
? expr::mkUF("blk_init_isptr", { idx }, true)
: true;
@@ -965,7 +970,7 @@ static void mk_nonlocal_val_axioms(State &s, Memory &m, expr &val) {
val = expr::mkLambda({ idx }, expr::mkIf(is_ptr, ptr_val(), int_val));
s.addAxiom(expr::mkForAll({ idx },
- ptr_val.ptr().get_short_bid().ule(num_nonlocals - 1)));
+ ptr_val.ptr().get_short_bid().ule(m.num_nonlocals() - 1)));
} else {
Byte byte(m, val.load(idx));
s.addAxiom(expr::mkForAll({ idx }, !byte.is_ptr()));
@@ -978,7 +983,7 @@ static void mk_nonlocal_val_axioms(State &s, Memory &m, expr &val) {
expr::mkForAll({ idx },
byte.is_ptr().implies(!loadedptr.is_local() &&
!loadedptr.is_nocapture() &&
- bid.ule(num_nonlocals - 1))));
+ bid.ule(m.num_nonlocals() - 1))));
#endif
}
@@ -1013,7 +1018,7 @@ Memory::Memory(State &state) : state(&state) {
// the block) should not overflow.
// Initialize a memory block for null pointer.
- if (num_nonlocals > 0)
+ if (IR::num_nonlocals > 0)
alloc(expr::mkUInt(0, bits_size_t), bits_program_pointer, GLOBAL, false,
false, 0);
@@ -1032,7 +1037,7 @@ void Memory::mkAxioms(const Memory &other) const {
return;
// transformation can increase alignment
- for (unsigned bid = 1; bid < num_nonlocals; ++bid) {
+ for (unsigned bid = 1; bid < IR::num_nonlocals; ++bid) {
state->addAxiom(Pointer(*this, bid, false).block_alignment().ule(
Pointer(other, bid, false).block_alignment()));
}
@@ -1040,12 +1045,12 @@ void Memory::mkAxioms(const Memory &other) const {
if (!observes_addresses())
return;
- if (num_nonlocals > 0)
+ if (IR::num_nonlocals > 0)
state->addAxiom(Pointer::mkNullPointer(*this).get_address(false) == 0);
// Non-local blocks are disjoint.
// Ignore null pointer block
- for (unsigned bid = 1; bid < num_nonlocals; ++bid) {
+ for (unsigned bid = 1; bid < IR::num_nonlocals; ++bid) {
Pointer p1(*this, bid, false);
expr disj = p1.get_address() != 0;
@@ -1054,7 +1059,7 @@ void Memory::mkAxioms(const Memory &other) const {
disj &= (p1.get_address() + p1.block_size()).extract(bit, bit) == 0;
// disjointness constraint
- for (unsigned bid2 = bid + 1; bid2 < num_nonlocals; ++bid2) {
+ for (unsigned bid2 = bid + 1; bid2 < IR::num_nonlocals; ++bid2) {
Pointer p2(*this, bid2, false);
disj &= p2.is_block_alive()
.implies(disjoint(p1.get_address(), p1.block_size(),
@@ -1082,12 +1087,8 @@ void Memory::mkAxioms(const Memory &other) const {
locals_fit(other);
}
-void Memory::resetGlobalData() {
- resetLocalBids();
- last_nonlocal_bid = 1;
-}
-
-void Memory::resetLocalBids() {
+void Memory::resetBids(unsigned last_nonlocal) {
+ last_nonlocal_bid = last_nonlocal;
last_local_bid = 0;
ptr_next_idx = 0;
}
@@ -1100,7 +1101,7 @@ expr Memory::mkInput(const char *name, unsigned attributes) const {
Pointer p(*this, name, false, false, attr_to_bitvec(attributes));
if (attributes & Input::NonNull)
state->addAxiom(p.isNonZero());
- state->addAxiom(p.get_short_bid().ule(num_nonlocals - 1));
+ state->addAxiom(p.get_short_bid().ule(num_nonlocals() - 1));
return p.release();
}
@@ -1144,7 +1145,7 @@ Memory::mkFnRet(const char *name, const vector<StateValue> &ptr_inputs) const {
state->addAxiom(expr::mkIf(p.is_local(),
expr::mk_or(local),
- p.get_short_bid().ule(num_nonlocals - 1)));
+ p.get_short_bid().ule(num_nonlocals() - 1)));
return { p.release(), move(var) };
}
@@ -1255,7 +1256,8 @@ 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));
+ assert((is_local && bid < num_locals) ||
+ (!is_local && bid < num_nonlocals()));
if (!bidopt)
++last_bid;
assert(bid < last_bid);
@@ -1524,7 +1526,7 @@ expr Memory::int2ptr(const expr &val) {
pair<expr,Pointer> Memory::refined(const Memory &other,
const vector<StateValue> *set_ptrs) const {
- if (num_nonlocals <= 1)
+ if (IR::num_nonlocals <= 1)
return { true, Pointer(*this, expr()) };
assert(!memory_unused());
@@ -1533,7 +1535,7 @@ pair<expr,Pointer> Memory::refined(const Memory &other,
expr offset = ptr.get_offset();
expr ret(true);
- for (unsigned bid = 1; bid < num_nonlocals; ++bid) {
+ for (unsigned bid = 1; bid < IR::num_nonlocals_src; ++bid) {
expr bid_expr = expr::mkUInt(bid, bits_for_bid);
Pointer p(*this, bid_expr, offset);
Pointer q(other, p());
@@ -1542,6 +1544,16 @@ pair<expr,Pointer> Memory::refined(const Memory &other,
ret &= (ptr_bid == bid_expr).implies(p.block_refined(q));
}
+ 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 = IR::num_nonlocals_src; bid < IR::num_nonlocals; ++bid)
+ assert(!is_constglb(*this, bid) && is_constglb(other, bid));
+
// restrict refinement check to set of request blocks
if (set_ptrs) {
expr c(false);
@@ -1562,7 +1574,7 @@ expr Memory::check_nocapture() const {
auto ofs = expr::mkVar(name.c_str(), bits_for_offset);
expr res(true);
- for (unsigned bid = 1; bid < num_nonlocals; ++bid) {
+ for (unsigned bid = 1; bid < num_nonlocals(); ++bid) {
Pointer p(*this, expr::mkUInt(bid, bits_for_bid), ofs);
Byte b(*this, non_local_block_val.load(p.short_ptr()));
Pointer loadp(*this, b.ptr_value());

MODIFY
ir/memory.h
ir/memory.h
@@ -231,8 +231,7 @@ public:
void finishInitialization();
void mkAxioms(const Memory &other) const;
- static void resetGlobalData();
- static void resetLocalBids();
+ static void resetBids(unsigned last_nonlocal);
void markByVal(unsigned bid);
smt::expr mkInput(const char *name, unsigned attributes) const;
@@ -286,6 +285,8 @@ public:
// Returns true if a nocapture pointer byte is not in the memory.
smt::expr check_nocapture() const;
+ unsigned num_nonlocals() const;
+
static Memory mkIf(const smt::expr &cond, const Memory &then,
const Memory &els);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -19,7 +19,7 @@ State::State(Function &f, bool source)
return_val(f.getType().getDummyValue(false)), return_memory(memory) {}
void State::resetGlobals() {
- Memory::resetGlobalData();
+ Memory::resetBids(1);
}
const StateValue& State::exec(const Value &v) {
@@ -338,7 +338,8 @@ void State::syncSEdataWithSrc(const State &src) {
fn_call_data = src.fn_call_data;
- Memory::resetLocalBids();
+ // The bid of tgt global starts with num_nonlocals_src
+ Memory::resetBids(num_nonlocals_src);
}
void State::mkAxioms(State &tgt) {

ADD
tests/alive-tv/refinement/const-introduce.src.ll
+define i32 @f() {
+ ret i32 0
+}

ADD
tests/alive-tv/refinement/const-introduce.tgt.ll
+@g = constant i32 0
+define i32 @f() {
+ %x = load i32, i32* @g
+ ret i32 %x
+}

ADD
tests/alive-tv/refinement/const-unused.src.ll
+define i32 @f(i32* %p) {
+ %v = load i32, i32* %p
+ ret i32 %v
+}

ADD
tests/alive-tv/refinement/const-unused.tgt.ll
+@c = constant i32 0
+define i32 @f(i32* %p) {
+ load i32, i32* @c
+ %v = load i32, i32* %p
+ ret i32 %v
+}

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -592,7 +592,8 @@ static uint64_t get_access_size(const Instr &inst) {
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();
+ unsigned num_globals_src = globals_src.size();
+ unsigned num_globals = num_globals_src;
// TODO: get this from data layout, varies among address spaces
bits_program_pointer = 64;
@@ -697,14 +698,16 @@ static void calculateAndInitConstants(Transform &t) {
}
}
- num_nonlocals = num_globals + num_ptrinputs + num_max_nonlocals_inst;
+ num_nonlocals_src = num_globals_src + num_ptrinputs + num_max_nonlocals_inst;
// check if null block is needed
- if (num_nonlocals > 0 || nullptr_is_used || has_malloc || has_load ||
+ if (num_nonlocals_src > 0 || nullptr_is_used || has_malloc || has_load ||
has_fncall)
- ++num_nonlocals;
+ ++num_nonlocals_src;
// Allow at least one non-const global for calls to change
- num_nonlocals += has_fncall;
+ num_nonlocals_src += has_fncall;
+
+ num_nonlocals = num_nonlocals_src + num_globals - num_globals_src;
if (!does_int_mem_access && !does_ptr_mem_access && has_fncall)
does_int_mem_access = true;
@@ -768,6 +771,7 @@ static void calculateAndInitConstants(Transform &t) {
if (config::debug)
config::dbg() << "num_max_nonlocals_inst: " << num_max_nonlocals_inst << "\n"
"num_locals: " << num_locals << "\n"
+ "num_nonlocals_src: " << num_nonlocals_src << "\n"
"num_nonlocals: " << num_nonlocals << "\n"
"bits_for_bid: " << bits_for_bid << "\n"
"bits_for_offset: " << bits_for_offset << "\n"

Support introduction of global constants in target (#212) (#283)