state: use DisjointExpr to keep track of return value
MODIFY
ir/state.cpp
ir/state.cpp
@@ -15,9 +15,7 @@ namespace IR {
State::State(const Function &f, bool source)
: f(f), source(source), memory(*this, f.isLittleEndian()),
- return_domain(false) {
- return_val.first = f.getType().getDummyValue(false);
-}
+ return_domain(false), return_val(f.getType().getDummyValue(false)) {}
void State::resetGlobals() {
Memory::resetGlobalData();
@@ -151,14 +149,10 @@ void State::addCondJump(const StateValue &cond, const BasicBlock &dst_true,
}
void State::addReturn(const StateValue &val) {
- if (return_domain.isFalse()) {
- return_val.first = val;
- } else {
- return_val.first = StateValue::mkIf(domain.first, val, return_val.first);
- }
+ return_val.add(StateValue(val), expr(domain.first));
return_domain |= domain.first;
- return_val.second.insert(undef_vars.begin(), undef_vars.end());
- return_val.second.insert(domain.second.begin(), domain.second.end());
+ return_undef_vars.insert(undef_vars.begin(), undef_vars.end());
+ return_undef_vars.insert(domain.second.begin(), domain.second.end());
undef_vars.clear();
domain.first = false;
}

MODIFY
ir/state.h
ir/state.h
#include "ir/memory.h"
#include "ir/state_value.h"
#include "smt/expr.h"
+#include "smt/exprs.h"
#include <array>
#include <ostream>
#include <set>
@@ -60,8 +61,8 @@ private:
// return_domain: a boolean expression describing return condition
smt::expr return_domain;
- // FIXME: replace with disjoint expr builder
- ValTy return_val;
+ smt::DisjointExpr<StateValue> return_val;
+ std::set<smt::expr> return_undef_vars;
public:
State(const Function &f, bool source);
@@ -99,7 +100,10 @@ public:
const auto& getQuantVars() const { return quantified_vars; }
auto& returnDomain() const { return return_domain; }
- auto& returnVal() const { return return_val; }
+
+ std::pair<StateValue, const std::set<smt::expr>&> returnVal() const {
+ return { return_val(), return_undef_vars };
+ }
void startParsingPre() { disable_undef_rewrite = true; }

MODIFY
ir/state_value.cpp
ir/state_value.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/state_value.h"
+#include <tuple>
using namespace smt;
using namespace std;
@@ -46,6 +47,10 @@ StateValue StateValue::subst(const vector<pair<expr, expr>> &repls) const {
return { value.subst(repls), non_poison.subst(repls) };
}
+bool StateValue::operator<(const StateValue &rhs) const {
+ return tie(value, non_poison) < tie(rhs.value, rhs.non_poison);
+}
+
ostream& operator<<(ostream &os, const StateValue &val) {
return os << val.value << " / " << val.non_poison;
}

MODIFY
ir/state_value.h
ir/state_value.h
@@ -35,6 +35,9 @@ struct StateValue {
StateValue
subst(const std::vector<std::pair<smt::expr, smt::expr>> &repls) const;
+ // for container use only
+ bool operator<(const StateValue &rhs) const;
+
friend std::ostream& operator<<(std::ostream &os, const StateValue &val);
};

MODIFY
smt/exprs.cpp
smt/exprs.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "smt/exprs.h"
+#include "ir/state_value.h"
#include "util/compiler.h"
using namespace std;
namespace smt {
-void DisjointExpr::add(expr &&val, expr &&domain) {
+template <typename T>
+void DisjointExpr<T>::add(T &&val, expr &&domain) {
if (domain.isFalse())
return;
if (domain.isTrue())
@@ -19,14 +21,15 @@ void DisjointExpr::add(expr &&val, expr &&domain) {
I->second |= move(domain);
}
-expr DisjointExpr::operator()() const {
- expr ret;
+template <typename T>
+T DisjointExpr<T>::operator()() const {
+ T ret;
bool first = true;
for (auto &[val, domain] : vals) {
if (domain.isTrue())
return val;
- ret = first ? val : expr::mkIf(domain, val, ret);
+ ret = first ? val : T::mkIf(domain, val, ret);
first = false;
}
if (first)
@@ -34,6 +37,9 @@ expr DisjointExpr::operator()() const {
return ret;
}
+template class DisjointExpr<expr>;
+template class DisjointExpr<IR::StateValue>;
+
void FunctionExpr::add(expr &&key, expr &&val) {
ENSURE(fn.emplace(move(key), move(val)).second);

MODIFY
smt/exprs.h
smt/exprs.h
namespace smt {
+template <typename T>
class DisjointExpr {
- std::map<expr, expr> vals; // val -> domain
- expr default_val;
+ std::map<T, expr> vals; // val -> domain
+ T default_val;
public:
DisjointExpr() {}
- DisjointExpr(const expr &default_val)
- : default_val(default_val) {}
+ DisjointExpr(const T &default_val) : default_val(default_val) {}
+ DisjointExpr(T &&default_val) : default_val(std::move(default_val)) {}
- void add(expr &&val, expr &&domain);
- expr operator()() const;
+ void add(T &&val, expr &&domain);
+ T operator()() const;
};

state: use DisjointExpr to keep track of return value