change undef pointers to have block_id=0
this helps efficiency (since block_id becomes constant and NULL),
and it doesn't affect correctness since undef block_id in the worst case would be 0, so non-deref
MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -518,14 +518,19 @@ void Memory::resetLocalBids() {
last_local_bid = 0;
}
-pair<expr, vector<expr>> Memory::mkInput(const char *name) {
+expr Memory::mkInput(const char *name) const {
unsigned bits = bits_for_bid - 1 + bits_for_offset;
expr var = expr::mkVar(name, bits);
expr offset = var.extract(bits_for_offset - 1, 0);
expr bid = var.extract(bits - 1, bits_for_offset);
expr is_local = expr::mkUInt(0, 1);
- return { Pointer(*this, is_local.concat(bid), offset).release(),
- { move(var) } };
+ return Pointer(*this, is_local.concat(bid), offset).release();
+}
+
+pair<expr, expr> Memory::mkUndefInput() const {
+ expr offset = expr::mkFreshVar("undef", expr::mkUInt(0, bits_for_offset));
+ Pointer p(*this, expr::mkUInt(0, bits_for_bid), offset);
+ return { p.release(), move(offset) };
}
expr Memory::alloc(const expr &size, unsigned align, BlockKind blockKind,

MODIFY
ir/memory.h
ir/memory.h
#include <ostream>
#include <string>
#include <utility>
-#include <vector>
namespace smt { class FunctionExpr; }
@@ -145,7 +144,8 @@ public:
static void resetGlobalData();
static void resetLocalBids();
- std::pair<smt::expr, std::vector<smt::expr>> mkInput(const char *name);
+ smt::expr mkInput(const char *name) const;
+ std::pair<smt::expr, smt::expr> mkUndefInput() const;
// Allocates a new memory block.
// If bid is not specified, it creates a fresh block id by increasing

MODIFY
ir/state.cpp
ir/state.cpp
@@ -174,8 +174,8 @@ void State::addQuantVar(const expr &var) {
quantified_vars.emplace(var);
}
-void State::addUndefVar(const expr &var) {
- undef_vars.emplace(var);
+void State::addUndefVar(expr &&var) {
+ undef_vars.emplace(move(var));
}
void State::resetUndefVars() {

MODIFY
ir/state.h
ir/state.h
@@ -90,7 +90,7 @@ public:
void addUB(const smt::expr &ub);
void addQuantVar(const smt::expr &var);
- void addUndefVar(const smt::expr &var);
+ void addUndefVar(smt::expr &&var);
void resetUndefVars();
auto& getFn() const { return f; }

MODIFY
ir/type.cpp
ir/type.cpp
@@ -221,6 +221,11 @@ expr Type::combine_poison(const expr &boolean, const expr &orig) const {
return expr::mkIf(boolean, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) | orig;
}
+pair<expr, vector<expr>> Type::mkUndefInput(State &s) const {
+ auto var = expr::mkFreshVar("undef", mkInput(s, ""));
+ return { var, { var } };
+}
+
ostream& operator<<(ostream &os, const Type &t) {
t.print(os);
return os;
@@ -257,7 +262,7 @@ VoidType::refines(State &src_s, State &tgt_s, const StateValue &src,
return { true, true };
}
-pair<expr, vector<expr>> VoidType::mkInput(State &s, const char *name) const {
+expr VoidType::mkInput(State &s, const char *name) const {
UNREACHABLE();
}
@@ -315,9 +320,8 @@ IntType::refines(State &src_s, State &tgt_s, const StateValue &src,
(src.non_poison && tgt.non_poison).implies(src.value == tgt.value) };
}
-pair<expr, vector<expr>> IntType::mkInput(State &s, const char *name) const {
- auto var = expr::mkVar(name, bits());
- return { var, { var } };
+expr IntType::mkInput(State &s, const char *name) const {
+ return expr::mkVar(name, bits());
}
void IntType::printVal(ostream &os, State &s, const expr &e) const {
@@ -428,15 +432,14 @@ FloatType::refines(State &src_s, State &tgt_s, const StateValue &src,
(non_poison && !src.value.isNaN()).implies(src.value == tgt.value) };
}
-pair<expr, vector<expr>> FloatType::mkInput(State &s, const char *name) const {
- expr var;
+expr FloatType::mkInput(State &s, const char *name) const {
switch (fpType) {
- case Half: var = expr::mkHalfVar(name); break;
- case Float: var = expr::mkFloatVar(name); break;
- case Double: var = expr::mkDoubleVar(name); break;
+ case Half: return expr::mkHalfVar(name);
+ case Float: return expr::mkFloatVar(name);
+ case Double: return expr::mkDoubleVar(name);
case Unknown: UNREACHABLE();
}
- return { var, { var } };
+ UNREACHABLE();
}
void FloatType::printVal(ostream &os, State &s, const expr &e) const {
@@ -526,10 +529,15 @@ PtrType::refines(State &src_s, State &tgt_s, const StateValue &src,
(src.non_poison && tgt.non_poison).implies(p.refined(q)) };
}
-pair<expr, vector<expr>> PtrType::mkInput(State &s, const char *name) const {
+expr PtrType::mkInput(State &s, const char *name) const {
return s.getMemory().mkInput(name);
}
+pair<expr, vector<expr>> PtrType::mkUndefInput(State &s) const {
+ auto [val, var] = s.getMemory().mkUndefInput();
+ return { move(val), { move(var) } };
+}
+
void PtrType::printVal(ostream &os, State &s, const expr &e) const {
os << Pointer(s.getMemory(), e);
}
@@ -685,14 +693,23 @@ AggregateType::refines(State &src_s, State &tgt_s, const StateValue &src,
return { expr::mk_and(poison), expr::mk_and(value) };
}
-pair<expr, vector<expr>>
-AggregateType::mkInput(State &s, const char *name) const {
+expr AggregateType::mkInput(State &s, const char *name) const {
+ expr val;
+ for (unsigned i = 0; i < elements; ++i) {
+ string c_name = string(name) + "#" + to_string(i);
+ auto v = children[i]->mkInput(s, c_name.c_str());
+ v = children[i]->toBV(move(v));
+ val = i == 0 ? move(v) : val.concat(v);
+ }
+ return val;
+}
+
+pair<expr, vector<expr>> AggregateType::mkUndefInput(State &s) const {
expr val;
vector<expr> vars;
for (unsigned i = 0; i < elements; ++i) {
- string c_name = string(name) + "#" + to_string(i);
- auto [v, vs] = children[i]->mkInput(s, c_name.c_str());
+ auto [v, vs] = children[i]->mkUndefInput(s);
v = children[i]->toBV(move(v));
val = i == 0 ? move(v) : val.concat(v);
vars.insert(vars.end(), vs.begin(), vs.end());
@@ -1025,11 +1042,15 @@ SymbolicType::refines(State &src_s, State &tgt_s, const StateValue &src,
DISPATCH(refines(src_s, tgt_s, src, tgt), UNREACHABLE());
}
-pair<expr, vector<expr>>
-SymbolicType::mkInput(State &st, const char *name) const {
+expr SymbolicType::mkInput(State &st, const char *name) const {
DISPATCH(mkInput(st, name), UNREACHABLE());
}
+pair<expr, vector<expr>> SymbolicType::mkUndefInput(State &st) const {
+ DISPATCH(mkUndefInput(st), UNREACHABLE());
+}
+
+
void SymbolicType::printVal(ostream &os, State &st, const expr &e) const {
DISPATCH(printVal(os, st, e), UNREACHABLE());
}

MODIFY
ir/type.h
ir/type.h
@@ -101,8 +101,10 @@ public:
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const = 0;
+ virtual smt::expr mkInput(State &s, const char *name) const = 0;
virtual std::pair<smt::expr, std::vector<smt::expr>>
- mkInput(State &s, const char *name) const = 0;
+ mkUndefInput(State &s) const;
+
virtual void printVal(std::ostream &os, State &s,
const smt::expr &e) const = 0;
@@ -126,8 +128,7 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
- std::pair<smt::expr, std::vector<smt::expr>>
- mkInput(State &s, const char *name) const override;
+ smt::expr mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -153,8 +154,7 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
- std::pair<smt::expr, std::vector<smt::expr>>
- mkInput(State &s, const char *name) const override;
+ smt::expr mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -191,8 +191,7 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
- std::pair<smt::expr, std::vector<smt::expr>>
- mkInput(State &s, const char *name) const override;
+ smt::expr mkInput(State &s, const char *name) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -218,8 +217,9 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
+ smt::expr mkInput(State &s, const char *name) const override;
std::pair<smt::expr, std::vector<smt::expr>>
- mkInput(State &s, const char *name) const override;
+ mkUndefInput(State &s) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};
@@ -259,8 +259,9 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
+ smt::expr mkInput(State &s, const char *name) const override;
std::pair<smt::expr, std::vector<smt::expr>>
- mkInput(State &s, const char *name) const override;
+ mkUndefInput(State &s) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
const AggregateType* getAsAggregateType() const override;
};
@@ -353,8 +354,9 @@ public:
std::pair<smt::expr, smt::expr>
refines(State &src_s, State &tgt_s, const StateValue &src,
const StateValue &tgt) const override;
+ smt::expr mkInput(State &s, const char *name) const override;
std::pair<smt::expr, std::vector<smt::expr>>
- mkInput(State &s, const char *name) const override;
+ mkUndefInput(State &s) const override;
void printVal(std::ostream &os, State &s, const smt::expr &e) const override;
void print(std::ostream &os) const override;
};

MODIFY
ir/value.cpp
ir/value.cpp
@@ -44,7 +44,7 @@ void UndefValue::print(ostream &os) const {
StateValue UndefValue::toSMT(State &s) const {
auto val = getType().getDummyValue(true);
expr var = expr::mkFreshVar("undef", val.value);
- s.addUndefVar(var);
+ s.addUndefVar(expr(var));
return { move(var), move(val.non_poison) };
}
@@ -119,16 +119,14 @@ StateValue Input::toSMT(State &s) const {
// 00: normal, 01: undef, else: poison
expr type = getTyVar();
- auto [val, vars] = getType().mkInput(s, smt_name.c_str());
+ auto val = getType().mkInput(s, smt_name.c_str());
if (!config::disable_undef_input) {
- vector<pair<expr, expr>> repls;
-
+ auto [undef, vars] = getType().mkUndefInput(s);
for (auto &v : vars) {
- s.addUndefVar(repls.emplace_back(v, expr::mkFreshVar("undef", v)).second);
+ s.addUndefVar(move(v));
}
-
- val = expr::mkIf(type.extract(0, 0) == 0, val, val.subst(repls));
+ val = expr::mkIf(type.extract(0, 0) == 0, val, undef);
}
expr poison = getType().getDummyValue(false).non_poison;

change undef pointers to have block_id=0
this helps efficiency (since block_id becomes constant and NULL),
and it doesn't affect correctness since undef block_id in the worst case would be 0, so non-deref