memory: fix load of undef value
bug found & reported by Juneyoung Lee
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -861,6 +861,7 @@ StateValue Memory::load(const expr &p, const Type &type, unsigned align,
if (deref_check)
ptr.is_dereferenceable(bytecount, align, false);
+ StateValue ret;
if (auto aty = type.getAsAggregateType()) {
vector<StateValue> member_vals;
unsigned byteofs = 0;
@@ -870,7 +871,7 @@ StateValue Memory::load(const expr &p, const Type &type, unsigned align,
byteofs += getStoreByteSize(aty->getChild(i));
}
assert(byteofs == bytecount);
- return aty->aggregateVals(member_vals);
+ ret = aty->aggregateVals(member_vals);
} else {
vector<Byte> loadedBytes;
@@ -881,8 +882,9 @@ StateValue Memory::load(const expr &p, const Type &type, unsigned align,
loadedBytes.emplace_back(*this, ::load(ptr_i, local_block_val,
non_local_block_val));
}
- return bytesToValue(loadedBytes, type);
+ ret = bytesToValue(loadedBytes, type);
}
+ return state->rewriteUndef(move(ret));
}
Byte Memory::load(const Pointer &p) {

MODIFY
ir/state.cpp
ir/state.cpp
#include "smt/smt.h"
#include "util/errors.h"
#include <cassert>
+#include <sstream>
+#include <string_view>
using namespace smt;
using namespace util;
@@ -182,6 +184,33 @@ void State::resetUndefVars() {
undef_vars.clear();
}
+static void collectUndefVars(State &s, set<expr> &undef_vars,
+ vector<pair<expr,expr>> &repls, const expr &val) {
+ for (auto &var : val.vars()) {
+ ostringstream ss;
+ ss << var;
+ auto name = ss.str();
+ if (string_view(name).substr(0, 6) == "undef!" &&
+ undef_vars.emplace(var).second) {
+ auto newvar = expr::mkFreshVar("undef", var);
+ repls.emplace_back(var, newvar);
+ s.addUndefVar(move(newvar));
+ }
+ }
+}
+
+StateValue State::rewriteUndef(StateValue &&val) {
+ set<expr> undef_vars;
+ vector<pair<expr, expr>> repls;
+ collectUndefVars(*this, undef_vars, repls, val.value);
+ collectUndefVars(*this, undef_vars, repls, val.non_poison);
+ if (undef_vars.empty())
+ return val;
+ if (hit_half_memory_limit())
+ throw AliveException("Out of memory; skipping function.", false);
+ return { val.value.subst(repls), val.non_poison.subst(repls) };
+}
+
void State::addGlobalVarBid(const string &glbvar, unsigned bid) {
ENSURE(glbvar_bids.emplace(glbvar, make_pair(bid, true)).second);
}

MODIFY
ir/state.h
ir/state.h
@@ -94,6 +94,8 @@ public:
void addUndefVar(smt::expr &&var);
void resetUndefVars();
+ StateValue rewriteUndef(StateValue &&val);
+
bool isInitializationPhase() const { return is_initialization_phase; }
void finishInitializer() { is_initialization_phase = false; }

ADD
tests/alive-tv/memory/load-undef.src.ll
+@gv = global i8 0
+
+define void @fn(i8 %v) {
+entry:
+ %v.addr = alloca i8
+ store i8 %v, i8* %v.addr
+ %0 = load i8, i8* %v.addr
+
+ %cmp = icmp eq i8 %0, 1
+ br i1 %cmp, label %if.then, label %if.end
+
+if.then:
+ %1 = load i8, i8* %v.addr
+ store i8 %1, i8* @gv
+ br label %if.end
+
+if.end:
+ ret void
+}
+
+
+define i8 @fn2() {
+entry:
+ %v.addr = alloca i8
+ store i8 undef, i8* %v.addr
+
+ %0 = load i8, i8* %v.addr
+ %1 = load i8, i8* %v.addr
+ %2 = add i8 %0, %1
+ ret i8 %2
+}

ADD
tests/alive-tv/memory/load-undef.tgt.ll
+@gv = global i8 0
+
+define void @fn(i8 %v) {
+entry:
+ %cmp = icmp eq i8 %v, 1
+ br i1 %cmp, label %if.then, label %if.end
+
+if.then:
+ store i8 %v, i8* @gv
+ br label %if.end
+
+if.end:
+ ret void
+}
+
+define i8 @fn2() {
+entry:
+ ret i8 undef
+}

memory: fix load of undef value
bug found & reported by Juneyoung Lee