add initial support for poison, undef, freeze
MODIFY
ir/function.cpp
ir/function.cpp
@@ -44,11 +44,10 @@ expr Function::getTypeConstraints() const {
for (auto bb : getBBs()) {
t &= bb->getTypeConstraints();
}
- for (auto &c : constants) {
- t &= c->getTypeConstraints();
+ for (auto &l : { getConstants(), getInputs(), getUndefs() }) {
+ for (auto &v : l) {
+ t &= v.getTypeConstraints();
}
- for (auto &i : inputs) {
- t &= i->getTypeConstraints();
}
return t;
}
@@ -57,11 +56,10 @@ void Function::fixupTypes(const Model &m) {
for (auto bb : getBBs()) {
bb->fixupTypes(m);
}
- for (auto &c : constants) {
- c->fixupTypes(m);
+ for (auto &l : { getConstants(), getInputs(), getUndefs() }) {
+ for (auto &v : l) {
+ const_cast<Value&>(v).fixupTypes(m);
}
- for (auto &i : inputs) {
- i->fixupTypes(m);
}
}
@@ -80,8 +78,12 @@ void Function::addConstant(unique_ptr<Value> &&c) {
constants.emplace_back(move(c));
}
-void Function::addInput(unique_ptr<Input> &&c) {
- inputs.emplace_back(move(c));
+void Function::addUndef(unique_ptr<UndefValue> &&u) {
+ undefs.emplace_back(move(u));
+}
+
+void Function::addInput(unique_ptr<Input> &&i) {
+ inputs.emplace_back(move(i));
}
Function::instr_iterator::

MODIFY
ir/function.h
ir/function.h
@@ -45,6 +45,7 @@ class Function {
// constants used in this function
std::vector<std::unique_ptr<Value>> constants;
+ std::vector<std::unique_ptr<Value>> undefs;
std::vector<std::unique_ptr<Value>> inputs;
public:
@@ -62,6 +63,11 @@ public:
return constants;
}
+ void addUndef(std::unique_ptr<UndefValue> &&c);
+ util::const_strip_unique_ptr<decltype(undefs)> getUndefs() const {
+ return undefs;
+ }
+
void addInput(std::unique_ptr<Input> &&c);
util::const_strip_unique_ptr<decltype(inputs)> getInputs() const {
return inputs;

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -342,6 +342,47 @@ void ICmp::fixupTypes(const Model &m) {
}
+void Freeze::print(ostream &os) const {
+ os << getName() << " = freeze " << val;
+}
+
+StateValue Freeze::toSMT(State &s) const {
+ auto &[v, p] = s[val];
+ s.resetUndefVars();
+
+ if (p.isTrue())
+ return { expr(v), expr(p) };
+
+ auto name = "undet_" + fresh_id();
+ expr undet = expr::mkVar(name.c_str(), bits());
+ s.addQuantVar(undet);
+
+ return { p.isFalse() ?
+ move(undet) :
+ expr::mkIf(p, v, undet),
+ true };
+}
+
+expr Freeze::getTypeConstraints() const {
+ return getType().getTypeConstraints() &&
+ getType() == val.getType();
+}
+
+
+void CopyOp::print(ostream &os) const {
+ os << getName() << " = " << val;
+}
+
+StateValue CopyOp::toSMT(State &s) const {
+ return s[val];
+}
+
+expr CopyOp::getTypeConstraints() const {
+ return getType().getTypeConstraints() &&
+ getType() == val.getType();
+}
+
+
void Return::print(ostream &os) const {
os << "ret " << val;
}

MODIFY
ir/instr.h
ir/instr.h
@@ -82,6 +82,30 @@ public:
};
+class Freeze final : public Instr {
+ Value &val;
+public:
+ Freeze(std::unique_ptr<Type> &&type, std::string &&name, Value &val) :
+ Instr(std::move(type), std::move(name)), val(val) {}
+
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints() const override;
+};
+
+
+class CopyOp final : public Instr {
+ Value &val;
+public:
+ CopyOp(std::unique_ptr<Type> &&type, std::string &&name, Value &val) :
+ Instr(std::move(type), std::move(name)), val(val) {}
+
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints() const override;
+};
+
+
class Return final : public Instr {
Value &val;
public:

MODIFY
ir/state.cpp
ir/state.cpp
@@ -25,12 +25,62 @@ State::State(const Function &f) : f(f) {
domain_bbs.emplace(&f.getBB(""), true);
}
-void State::add(const Value &val, StateValue &&e) {
- auto p = values.emplace(&val, move(e));
+const StateValue& State::exec(const Value &v) {
+ assert(undef_vars.empty());
+ auto val = v.toSMT(*this);
+ auto p = values.try_emplace(&v, move(val), move(undef_vars));
assert(p.second);
+
+ // cleanup potentailly used temporary values due to undef rewriting
+ while (i_tmp_values > 0) {
+ tmp_values[--i_tmp_values] = StateValue();
+ }
+
+ return p.first->second.first;
+}
+
+const StateValue& State::operator[](const Value &val) {
+ auto &[sval, uvars] = values.at(&val);
+ if (uvars.empty())
+ return sval;
+
+ if (undef_vars.empty()) {
+ undef_vars = uvars;
+ return sval;
}
-const StateValue& State::operator[](const Value &val) const {
+ // if evaluated expr shares undef vars with previously evaluated expr, rename
+ // those undef vars
+ vector<pair<expr, expr>> repls;
+ auto VI = uvars.begin(), VE = uvars.end();
+ for (auto I = undef_vars.begin(), E = undef_vars.end(); I != E && VI != VE;) {
+ if (I->eq(*VI)) {
+ auto name = UndefValue::getFreshName();
+ repls.emplace_back(*I, expr::mkVar(name.c_str(), I->bits()));
+ ++I, ++VI;
+
+ } else if (*I < *VI) {
+ ++I;
+
+ } else {
+ undef_vars.emplace_hint(I, *VI);
+ ++VI;
+ }
+ }
+
+ if (repls.empty())
+ return sval;
+
+ for (auto &p : repls) {
+ undef_vars.emplace(p.second);
+ }
+
+ tmp_values[i_tmp_values] =
+ { sval.value.replace(repls), sval.non_poison.replace(repls) };
+ return tmp_values[i_tmp_values++];
+}
+
+const State::ValTy& State::at(const Value &val) const {
return values.at(&val);
}
@@ -52,11 +102,13 @@ void State::addJump(const BasicBlock &bb) {
void State::addReturn(const StateValue &val) {
if (returned) {
return_domain |= domain;
- return_val = StateValue::mkIf(domain, val, return_val);
+ // TODO: combine undef_vars
+ return_val = { StateValue::mkIf(domain, val, return_val.first),
+ move(undef_vars) };
} else {
returned = true;
return_domain = domain;
- return_val = val;
+ return_val = { val, move(undef_vars) };
}
}
@@ -64,4 +116,12 @@ void State::addQuantVar(const expr &var) {
quantified_vars.emplace(var);
}
+void State::addUndefVar(const expr &var) {
+ undef_vars.emplace(var);
+}
+
+void State::resetUndefVars() {
+ undef_vars.clear();
+}
+
}

MODIFY
ir/state.h
ir/state.h
// Distributed under the MIT license that can be found in the LICENSE file.
#include "smt/expr.h"
+#include <array>
#include <ostream>
#include <set>
#include <unordered_map>
+#include <utility>
namespace IR {
@@ -29,21 +31,33 @@ class BasicBlock;
class Function;
class State {
+public:
+ using ValTy = std::pair<StateValue, std::set<smt::expr>>;
+
+private:
const Function &f;
std::set<smt::expr> quantified_vars;
- // var -> ((value, not_poison), domain)
- std::unordered_map<const Value*, StateValue> values;
+ // var -> ((value, not_poison), undef_vars)
+ std::unordered_map<const Value*, ValTy> values;
std::unordered_map<const BasicBlock*, smt::expr> domain_bbs;
+
+ // temp state
smt::expr domain;
+ std::set<smt::expr> undef_vars;
+ std::array<StateValue, 4> tmp_values;
+ unsigned i_tmp_values = 0; // next available position in tmp_values
+
smt::expr return_domain;
// FIXME: replace with disjoint expr builder
- StateValue return_val;
+ ValTy return_val;
bool returned = false;
public:
State(const Function &f);
- void add(const Value &val, StateValue &&e);
- const StateValue& operator[](const Value &val) const;
+
+ const StateValue& exec(const Value &v);
+ const StateValue& operator[](const Value &val);
+ const ValTy& at(const Value &val) const;
bool startBB(const BasicBlock &bb);
void addJump(const BasicBlock &bb);
@@ -51,13 +65,16 @@ public:
void addUB(smt::expr &&ub) { domain &= std::move(ub); }
void addUB(const smt::expr &ub) { domain &= ub; }
void addQuantVar(const smt::expr &var);
+ void addUndefVar(const smt::expr &var);
+ void resetUndefVars();
auto& getFn() const { return f; }
const auto& getValues() const { return values; }
+ const auto& getQuantVars() const { return quantified_vars; }
bool fnReturned() const { return returned; }
- const smt::expr& returnDomain() const { return return_domain; }
- const StateValue& returnVal() const { return return_val; }
+ auto& returnDomain() const { return return_domain; }
+ auto& returnVal() const { return return_val; }
};
}

MODIFY
ir/value.cpp
ir/value.cpp
@@ -10,12 +10,17 @@ using namespace util;
using namespace std;
static unsigned gbl_fresh_id = 0;
-static string fresh_id() {
- return to_string(++gbl_fresh_id);
-}
namespace IR {
+void Value::reset_gbl_id() {
+ gbl_fresh_id = 0;
+}
+
+string Value::fresh_id() {
+ return to_string(++gbl_fresh_id);
+}
+
Value::Value(unique_ptr<Type> &&type, string &&name, bool mk_unique_name)
: type(move(type)), name(move(name)) {
if (mk_unique_name)
@@ -58,17 +63,63 @@ expr IntConst::getTypeConstraints() const {
}
+UndefValue::UndefValue(unique_ptr<Type> &&type)
+ : Value(std::move(type), "undef", true) {}
+
+void UndefValue::print(ostream &os) const {
+ os << "undef";
+}
+
+StateValue UndefValue::toSMT(State &s) const {
+ auto name = getFreshName();
+ expr var = expr::mkVar(name.c_str(), bits());
+ s.addUndefVar(var);
+ return { move(var), true };
+}
+
+expr UndefValue::getTypeConstraints() const {
+ return getType().getTypeConstraints();
+}
+
+string UndefValue::getFreshName() {
+ return "undef_" + fresh_id();
+}
+
+
+PoisonValue::PoisonValue(unique_ptr<Type> &&type)
+ : Value(std::move(type), "poison", true) {}
+
+void PoisonValue::print(ostream &os) const {
+ os << "poison";
+}
+
+StateValue PoisonValue::toSMT(State &s) const {
+ return { {}, false };
+}
+
+expr PoisonValue::getTypeConstraints() const {
+ return getType().getTypeConstraints();
+}
+
+
void Input::print(std::ostream &os) const {
os << getName();
}
StateValue Input::toSMT(State &s) const {
- string pname = getName() + "_np";
- auto poison = expr::mkBoolVar(pname.c_str());
- auto value = expr::mkVar(getName().c_str(), getType().bits());
- s.addQuantVar(poison);
- s.addQuantVar(value);
- return { move(value), move(poison) };
+ // 00: normal, 01: undef, else: poison
+ string tyname = "ty_" + getName();
+ expr type = expr::mkVar(tyname.c_str(), 2);
+
+ auto bw = bits();
+ string uname = UndefValue::getFreshName();
+ expr undef = expr::mkVar(uname.c_str(), bw);
+ s.addUndefVar(undef);
+
+ return { expr::mkIf(type == expr::mkUInt(0, 2),
+ expr::mkVar(getName().c_str(), bw),
+ move(undef)),
+ type.extract(1,1) == expr::mkUInt(0, 1) };
}
expr Input::getTypeConstraints() const {

MODIFY
ir/value.h
ir/value.h
@@ -22,6 +22,8 @@ protected:
Value(std::unique_ptr<Type> &&type, std::string &&name,
bool mk_unique_name = false);
+ static std::string fresh_id();
+
public:
unsigned bits() const { return type->bits(); }
const std::string& getName() const { return name; }
@@ -34,6 +36,8 @@ public:
virtual void fixupTypes(const smt::Model &m);
virtual ~Value();
+ static void reset_gbl_id();
+
friend std::ostream& operator<<(std::ostream &os, const Value &val);
};
@@ -49,6 +53,26 @@ public:
};
+class UndefValue final : public Value {
+public:
+ UndefValue(std::unique_ptr<Type> &&type);
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints() const override;
+
+ static std::string getFreshName();
+};
+
+
+class PoisonValue final : public Value {
+public:
+ PoisonValue(std::unique_ptr<Type> &&type);
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints() const override;
+};
+
+
class Input final : public Value {
public:
Input(std::unique_ptr<Type> &&type, std::string &&name) :

MODIFY
smt/expr.cpp
smt/expr.cpp
#include "smt/ctx.h"
#include "smt/expr.h"
#include <cassert>
+#include <memory>
#include <z3.h>
#define DEBUG_Z3_RC 0
@@ -714,10 +715,34 @@ expr expr::mkIf(const expr &cond, const expr &then, const expr &els) {
return Z3_mk_ite(ctx(), c, t, e);
}
+expr expr::mkForAll(const set<expr> &vars, expr &&val) {
+ if (vars.empty() || val.isTrue() || val.isFalse())
+ return move(val);
+
+ unique_ptr<Z3_app[]> vars_ast(new Z3_app[vars.size()]);
+ unsigned i = 0;
+ for (auto &v : vars) {
+ vars_ast[i++] = (Z3_app)v();
+ }
+ return Z3_mk_forall_const(ctx(), 0, vars.size(), vars_ast.get(), 0, nullptr,
+ val());
+}
+
+expr expr::replace(vector<pair<expr, expr>> &repls) const {
+ unique_ptr<Z3_ast[]> from(new Z3_ast[repls.size()]);
+ unique_ptr<Z3_ast[]> to(new Z3_ast[repls.size()]);
+
+ unsigned i = 0;
+ for (auto &p : repls) {
+ from[i] = p.first();
+ to[i] = p.second();
+ ++i;
+ }
+ return Z3_substitute(ctx(), ast(), repls.size(), from.get(), to.get());
+}
+
ostream& operator<<(ostream &os, const expr &e) {
- if (!e.isValid())
- return os << "(null)";
- return os << Z3_ast_to_string(ctx(), e());
+ return os << (e.isValid() ? Z3_ast_to_string(ctx(), e()) : "(null)");
}
bool expr::operator<(const expr &rhs) const {

MODIFY
smt/expr.h
smt/expr.h
#include <cstdint>
#include <ostream>
+#include <set>
#include <utility>
+#include <vector>
typedef struct _Z3_context* Z3_context;
typedef struct _Z3_app* Z3_app;
@@ -162,6 +164,10 @@ public:
expr extract(unsigned high, unsigned low) const;
static expr mkIf(const expr &cond, const expr &then, const expr &els);
+ static expr mkForAll(const std::set<expr> &vars, expr &&val);
+
+ // replace v1 -> v2
+ expr replace(std::vector<std::pair<expr, expr>> &repls) const;
friend std::ostream &operator<<(std::ostream &os, const expr &e);

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -126,6 +126,8 @@ re2c:yyfill:check = 0;
"true" { return TRUE; }
"false" { return FALSE; }
+"undef" { return UNDEF; }
+"poison" { return POISON; }
"add" { return ADD; }
"mul" { return MUL; }
"sub" { return SUB; }
@@ -158,6 +160,7 @@ re2c:yyfill:check = 0;
"ult" { return ULT; }
"uge" { return UGE; }
"ugt" { return UGT; }
+"freeze" { return FREEZE; }
"ret" { return RETURN; }
"unreachable" { return UNREACH; }

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -138,6 +138,18 @@ static Value& parse_operand(Type *type) {
return get_constant(1, type);
case FALSE:
return get_constant(0, type);
+ case UNDEF: {
+ auto val = make_unique<UndefValue>(type->dup());
+ auto ret = val.get();
+ fn->addUndef(move(val));
+ return *ret;
+ }
+ case POISON: {
+ auto val = make_unique<PoisonValue>(type->dup());
+ auto ret = val.get();
+ fn->addConstant(move(val));
+ return *ret;
+ }
case IDENTIFIER: {
string id(yylval.str);
if (auto I = identifiers.find(id);
@@ -285,6 +297,20 @@ static unique_ptr<Instr> parse_icmp(string_view name) {
return make_unique<ICmp>(string(name), cond, a, b);
}
+static unique_ptr<Instr> parse_freeze(string_view name) {
+ // freeze ty %op
+ auto ty = parse_type();
+ auto &op = parse_operand(ty.get());
+ return make_unique<Freeze>(move(ty), string(name), op);
+}
+
+static unique_ptr<Instr> parse_copyop(string_view name, token t) {
+ tokenizer.unget(t);
+ auto ty = parse_type();
+ auto &op = parse_operand(ty.get());
+ return make_unique<CopyOp>(move(ty), string(name), op);
+}
+
static unique_ptr<Instr> parse_instr(string_view name) {
// %name = instr arg1, arg2, ...
tokenizer.ensure(EQUALS);
@@ -311,6 +337,16 @@ static unique_ptr<Instr> parse_instr(string_view name) {
return parse_select(name);
case ICMP:
return parse_icmp(name);
+ case FREEZE:
+ return parse_freeze(name);
+ case INT_TYPE:
+ case NUM:
+ case TRUE:
+ case FALSE:
+ case UNDEF:
+ case POISON:
+ case IDENTIFIER:
+ return parse_copyop(name, t);
default:
error(string("Expected instruction name; got: ") + token_name[t]);
}

MODIFY
tools/tokens.h
tools/tokens.h
@@ -11,6 +11,7 @@ TOKEN(EQ)
TOKEN(EQUALS)
TOKEN(EXACT)
TOKEN(FALSE)
+TOKEN(FREEZE)
TOKEN(ICMP)
TOKEN(IDENTIFIER)
TOKEN(INT_TYPE)
@@ -23,6 +24,7 @@ TOKEN(NSW)
TOKEN(NUM)
TOKEN(NUW)
TOKEN(OR)
+TOKEN(POISON)
TOKEN(PRE)
TOKEN(RETURN)
TOKEN(SDIV)
@@ -43,6 +45,7 @@ TOKEN(UGE)
TOKEN(UGT)
TOKEN(ULE)
TOKEN(ULT)
+TOKEN(UNDEF)
TOKEN(UNREACH)
TOKEN(UREM)
TOKEN(XOR)

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -16,47 +16,53 @@ using namespace util;
using namespace std;
static void check_refinement(Solver &s, Errors &errs,
- const expr &dom_a, const StateValue &a,
- const expr &dom_b, const StateValue &b) {
- // TODO: handle quantified vars
+ const set<expr> &global_qvars,
+ const expr &dom_a, const State::ValTy &ap,
+ const expr &dom_b, const State::ValTy &bp) {
+ auto &a = ap.first;
+ auto &b = bp.first;
+
+ auto qvars = global_qvars;
+ qvars.insert(ap.second.begin(), ap.second.end());
+
// TODO: improve error messages
s.check({
- { dom_a.notImplies(dom_b), [&](const Model &m) {
- errs.add("Source is more defined than target"); } },
+ { expr::mkForAll(qvars, dom_a.notImplies(dom_b)),
+ [&](const Model &m) { errs.add("Source is more defined than target"); } },
- { dom_a && a.non_poison.notImplies(b.non_poison), [&](const Model &m) {
- errs.add("Target is more poisonous than source"); } },
+ { expr::mkForAll(qvars, dom_a && a.non_poison.notImplies(b.non_poison)),
+ [&](const Model &m) {errs.add("Target is more poisonous than source"); }},
- { dom_a && a.non_poison && a.value != b.value, [&](const Model &m) {
- errs.add("value mismatch");
- } }
+ { expr::mkForAll(qvars, dom_a && a.non_poison && a.value != b.value),
+ [&](const Model &m) { errs.add("value mismatch"); } }
});
}
namespace tools {
Errors Transform::verify(const TransformVerifyOpts &opts) const {
- Errors errs;
-
unordered_map<string, const Value*> tgt_vals;
for (auto &i : tgt.instrs()) {
tgt_vals.emplace(i.getName(), &i);
}
+ Value::reset_gbl_id();
State src_state(src), tgt_state(tgt);
sym_exec(src_state);
sym_exec(tgt_state);
+ Errors errs;
Solver s;
if (opts.check_each_var) {
for (auto &[var, val] : src_state.getValues()) {
auto &name = var->getName();
- if (name[0] != '%')
+ if (name[0] != '%' || !dynamic_cast<const Instr*>(var))
continue;
// TODO: add data-flow domain tracking for Alive, but not for TV
- check_refinement(s, errs, true, val, true, tgt_state[*tgt_vals.at(name)]);
+ check_refinement(s, errs, tgt_state.getQuantVars(),
+ true, val, true, tgt_state.at(*tgt_vals.at(name)));
}
}
@@ -67,7 +73,7 @@ Errors Transform::verify(const TransformVerifyOpts &opts) const {
errs.add("Target returns but source doesn't");
} else if (src_state.fnReturned()) {
- check_refinement(s, errs,
+ check_refinement(s, errs, tgt_state.getQuantVars(),
src_state.returnDomain(), src_state.returnVal(),
tgt_state.returnDomain(), tgt_state.returnVal());
}

MODIFY
util/compiler.h
util/compiler.h
@@ -36,8 +36,8 @@ struct const_strip_unique_ptr {
bool operator!=(const const_iterator &other) const { return I != other.I; }
};
- const_iterator begin() { return container.begin(); }
- const_iterator end() { return container.end(); }
+ const_iterator begin() const { return container.begin(); }
+ const_iterator end() const { return container.end(); }
};
unsigned ilog2(uint64_t n);

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -17,12 +17,10 @@ void sym_exec(State &s) {
Function &f = const_cast<Function&>(s.getFn());
// add constants & inputs to State table first of all
- for (auto &c : f.getConstants()) {
- s.add(c, c.toSMT(s));
+ for (auto &l : { f.getConstants(), f.getInputs(), f.getUndefs() }) {
+ for (const auto &v : l) {
+ s.exec(v);
}
-
- for (auto &i : f.getInputs()) {
- s.add(i, i.toSMT(s));
}
for (auto &bb : f.getBBs()) {
@@ -30,14 +28,11 @@ void sym_exec(State &s) {
continue;
for (auto &i : bb->instrs()) {
- auto val = i.toSMT(s);
+ auto val = s.exec(i);
auto &name = i.getName();
- if (name[0] == '%') {
- if (config::symexec_print_each_value)
+ if (config::symexec_print_each_value && name[0] == '%')
cout << name << " = " << val << '\n';
- s.add(i, move(val));
- }
}
}
}

add initial support for poison, undef, freeze