memory: skip generating axioms if memory is not used in function
MODIFY
ir/constant.h
ir/constant.h
@@ -46,6 +46,7 @@ class AggregateConst final : public Constant {
std::vector<Value*> vals;
public:
AggregateConst(Type &type, std::vector<Value*> &&vals);
+ auto& getVals() const { return vals; }
StateValue toSMT(State &s) const override;
smt::expr getTypeConstraints() const override;

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -442,12 +442,20 @@ expr Memory::mk_liveness_array() const {
static unsigned last_local_bid = 0;
static unsigned last_nonlocal_bid = 1;
+static bool memory_unused() {
+ // +1 for the null block
+ return num_locals == 0 && num_nonlocals == 1 && !nullptr_is_used;
+}
+
Memory::Memory(State &state, bool little_endian)
: state(&state), little_endian(little_endian),
local_blk_addr(expr::mkUInt(0, bits_size_t - 1)),
local_blk_size(expr::mkUInt(0, bits_size_t - 1)),
local_blk_kind(expr::mkUInt(0, 2)) {
+ if (memory_unused())
+ return;
+
non_local_block_val = mk_val_array();
non_local_block_liveness = mk_liveness_array();
{
@@ -494,12 +502,12 @@ Memory::Memory(State &state, bool little_endian)
// 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) {
+ 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);
- for (unsigned bid2 = bid + 1; bid2 <= non_local_bid_upperbound; ++bid2) {
+ for (unsigned bid2 = bid + 1; bid2 < non_local_bid_upperbound; ++bid2) {
Pointer p2(*this, bid2, false);
disj &= p2.is_block_alive()
.implies(disjoint(p1.get_address(), p1.block_size(),
@@ -552,6 +560,8 @@ pair<expr, expr> Memory::mkUndefInput() const {
expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
optional<unsigned> bidopt, unsigned *bid_out,
const expr &precond) {
+ assert(!memory_unused());
+
// Produce a local block if blockKind is heap or stack.
bool is_local = blockKind != GLOBAL && blockKind != CONSTGLOBAL;
@@ -635,6 +645,7 @@ expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,
}
void Memory::free(const expr &ptr) {
+ assert(!memory_unused());
Pointer p(*this, ptr);
state->addUB(p.isNull() || (p.get_offset() == 0 &&
p.is_block_alive() &&
@@ -652,6 +663,7 @@ void Memory::free(const expr &ptr) {
void Memory::store(const expr &p, const StateValue &v, const Type &type,
unsigned align) {
+ assert(!memory_unused());
vector<Byte> bytes = valueToBytes(v, type, *this);
Pointer ptr(*this, p);
@@ -663,6 +675,7 @@ void Memory::store(const expr &p, const StateValue &v, const Type &type,
}
StateValue Memory::load(const expr &p, const Type &type, unsigned align) {
+ assert(!memory_unused());
auto bitsize = type.isPtrType() ? bitsPtrSize() : type.bits();
unsigned bytesize = divide_up(bitsize, 8);
@@ -680,6 +693,7 @@ StateValue Memory::load(const expr &p, const Type &type, unsigned align) {
void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
unsigned align) {
+ assert(!memory_unused());
assert(!val.isValid() || val.bits() == 8);
Pointer ptr(*this, p);
ptr.is_dereferenceable(bytesize, align, true);
@@ -701,6 +715,7 @@ void Memory::memset(const expr &p, const StateValue &val, const expr &bytesize,
void Memory::memcpy(const expr &d, const expr &s, const expr &bytesize,
unsigned align_dst, unsigned align_src, bool is_move) {
+ assert(!memory_unused());
Pointer dst(*this, d), src(*this, s);
dst.is_dereferenceable(bytesize, align_dst, true);
src.is_dereferenceable(bytesize, align_src, false);
@@ -725,15 +740,20 @@ void Memory::memcpy(const expr &d, const expr &s, const expr &bytesize,
}
expr Memory::ptr2int(const expr &ptr) {
+ assert(!memory_unused());
return Pointer(*this, ptr).get_address();
}
expr Memory::int2ptr(const expr &val) {
+ assert(!memory_unused());
// TODO
return {};
}
expr Memory::refined(const Memory &other) const {
+ if (memory_unused())
+ return true;
+
Pointer p(*this, "#idx");
Pointer q(other, p());
return p.block_refined(q);

MODIFY
ir/state.cpp
ir/state.cpp
@@ -18,14 +18,17 @@ unsigned num_locals;
unsigned num_nonlocals;
unsigned bits_for_bid;
unsigned bits_for_offset;
+bool nullptr_is_used;
void initConstants(unsigned num_globals, unsigned num_ptrinputs,
- unsigned num_max_nonlocals_inst, unsigned num_locals) {
+ unsigned num_max_nonlocals_inst, unsigned num_locals,
+ bool nullptr_is_used) {
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;
unsigned maxblks = max(num_locals, num_nonlocals);
if (maxblks == 1)

MODIFY
ir/state.h
ir/state.h
@@ -28,9 +28,11 @@ extern unsigned num_nonlocals;
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;
void initConstants(unsigned num_globals, unsigned num_ptrinputs,
- unsigned num_max_nonlocals_inst, unsigned num_locals);
+ unsigned num_max_nonlocals_inst, unsigned num_locals,
+ bool nullptr_is_used);
class Value;

MODIFY
ir/value.h
ir/value.h
@@ -80,23 +80,22 @@ public:
class GlobalVariable final : public Value {
// The size of this global variable (in bytes)
- int allocsize;
- // Alignment of this global variable
- int align;
+ uint64_t allocsize;
+ unsigned align;
// Initial value stored at this global variable.
// This is initialized only if the global is constant.
// If it has no initial value, this is nullptr.
Value *initval;
- // Is this global variable constant?
// initval can be null even if isconst is true if this is an external const.
bool isconst;
public:
- GlobalVariable(Type &type, std::string &&name, int allocsize, int align,
- Value *initval, bool isconst) :
+ GlobalVariable(Type &type, std::string &&name, uint64_t allocsize,
+ unsigned align, Value *initval, bool isconst) :
Value(type, std::move(name)), allocsize(allocsize), align(align),
initval(initval), isconst(isconst) {}
- int size() const { return allocsize; }
- int isConst() const { return isconst; }
+ uint64_t size() const { return allocsize; }
+ bool isConst() const { return isconst; }
+ const Value* initVal() const { return initval; }
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
};

MODIFY
tests/alive-tv/memory/glb-1.src.ll
tests/alive-tv/memory/glb-1.src.ll
@@ -4,3 +4,5 @@ define i32 @f() {
%v = load i32, i32* @x
ret i32 %v
}
+
+; XFAIL: Mismatch in memory

MODIFY
tests/alive-tv/memory/glb-1.tgt.ll
tests/alive-tv/memory/glb-1.tgt.ll
@x = constant i32 5, align 4
define i32 @f() {
- %v = load i32, i32* @x ; relieves memory mismatch check
ret i32 5
}

MODIFY
tests/unit/fshl/folds32.opt
tests/unit/fshl/folds32.opt
-; TEST-ARGS: -root-only -smt-to:30000
-
Name: single shift by masked value
%c_mod_width = urem i32 %c, i32 32
%t = shl i32 %a, i32 %c_mod_width

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -136,16 +136,16 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
}
set<string> seen_vars;
- for (auto &st : { src_state, tgt_state }) {
+ for (auto st : { &src_state, &tgt_state }) {
if (!check_each_var) {
- if (st.isSource()) {
+ if (st->isSource()) {
s << "\nSource:\n";
} else {
s << "\nTarget:\n";
}
}
- for (auto &[var, val, used] : st.getValues()) {
+ for (auto &[var, val, used] : st->getValues()) {
(void)used;
auto &name = var->getName();
if (name == var_name)
@@ -157,7 +157,7 @@ static void error(Errors &errs, State &src_state, State &tgt_state,
continue;
s << *var << " = ";
- print_varval(s, const_cast<State&>(st), m, var, var->getType(),
+ print_varval(s, const_cast<State&>(*st), m, var, var->getType(),
val.first);
s << '\n';
}
@@ -306,6 +306,20 @@ static void check_refinement(Errors &errs, Transform &t,
}
}
+static bool has_nullptr(const Value *v) {
+ if (dynamic_cast<const NullPointerValue*>(v))
+ return true;
+
+ if (auto agg = dynamic_cast<const AggregateConst*>(v)) {
+ for (auto val : agg->getVals()) {
+ if (has_nullptr(val))
+ return true;
+ }
+ }
+
+ return false;
+}
+
static void calculateAndInitConstants(Transform &t) {
const auto &globals_tgt = t.tgt.getGlobalVars();
const auto &globals_src = t.src.getGlobalVars();
@@ -364,8 +378,35 @@ static void calculateAndInitConstants(Transform &t) {
});
}
+ bool nullptr_is_used = 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;
+ }
+ }
+ }
+ }
+ }
+
+ if (!nullptr_is_used) {
+ 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;
+ }
+ }
+ }
+ }
+ }
+
initConstants(num_globals, num_ptrinputs, num_inst_nonlocals,
- max(num_locals_src, num_locals_tgt));
+ max(num_locals_src, num_locals_tgt), nullptr_is_used);
}

memory: skip generating axioms if memory is not used in function