memory: skip dereferenceability constraints for init stores
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -2606,7 +2606,8 @@ void Store::print(std::ostream &os) const {
StateValue Store::toSMT(State &s) const {
auto &[p, np] = s[*ptr];
s.addUB(np);
- s.getMemory().store(p, s[*val], val->getType(), align, s.getUndefVars());
+ auto &v = s[*val];
+ s.getMemory().store(p, v, val->getType(), align, s.getUndefVars());
return {};
}

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -1497,9 +1497,9 @@ void Memory::store(const expr &p, const StateValue &v, const Type &type,
undef_vars.insert(undef_vars0.begin(), undef_vars0.end());
- if (deref_check)
- state->addUB(ptr.isDereferenceable(getStoreByteSize(type), align,
- !state->isInitializationPhase()));
+ // initializer stores are ok by construction
+ if (deref_check && !state->isInitializationPhase())
+ state->addUB(ptr.isDereferenceable(getStoreByteSize(type), align, true));
auto aty = type.getAsAggregateType();
if (aty && !isNonPtrVector(type)) {

MODIFY
ir/memory.h
ir/memory.h
@@ -307,6 +307,8 @@ public:
const std::vector<PtrInput> *set_ptrs = nullptr)
const;
+ auto& getUndefVars() const { return undef_vars; }
+
// Returns true if a nocapture pointer byte is not in the memory.
smt::expr checkNocapture() const;

MODIFY
ir/state.cpp
ir/state.cpp
@@ -190,8 +190,9 @@ void State::addReturn(const StateValue &val) {
}
void State::addUB(expr &&ub) {
+ bool isconst = ub.isConst();
domain.UB.add(move(ub));
- if (!ub.isConst())
+ if (!isconst)
domain.undef_vars.insert(undef_vars.begin(), undef_vars.end());
}
@@ -202,7 +203,9 @@ void State::addUB(const expr &ub) {
}
void State::addUB(AndExpr &&ubs) {
+ bool isconst = ubs.isTrue();
domain.UB.add(move(ubs));
+ if (!isconst)
domain.undef_vars.insert(undef_vars.begin(), undef_vars.end());
}

MODIFY
smt/exprs.h
smt/exprs.h
@@ -28,6 +28,7 @@ public:
bool contains(const expr &e) const;
expr operator()() const;
operator bool() const;
+ bool isTrue() const { return exprs.empty(); }
friend std::ostream &operator<<(std::ostream &os, const AndExpr &e);
};

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -333,6 +333,11 @@ check_refinement(Errors &errs, Transform &t, State &src_state, State &tgt_state,
auto memory_cnstr = memory_cnstr0.isTrue() ? memory_cnstr0
: value_cnstr && memory_cnstr0;
+ if (!memory_cnstr.isConst()) {
+ auto &undef = src_mem.getUndefVars();
+ qvars.insert(undef.begin(), undef.end());
+ }
+
if (check_expr(axioms_expr && (pre_src && pre_tgt)).isUnsat()) {
errs.add("Precondition is always false", false);
return;

memory: skip dereferenceability constraints for init stores