alive: add preliminary support for -root-only
MODIFY
ir/function.cpp
ir/function.cpp
@@ -33,6 +33,7 @@ ostream& operator<<(ostream &os, const BasicBlock &bb) {
for (auto &i : bb.instrs()) {
os << " ";
i.print(os);
+ os << '\n';
}
return os;
}

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -10,6 +10,13 @@ using namespace std;
namespace IR {
+void Instr::printType(ostream &os) const {
+ auto t = getType().toString();
+ if (!t.empty())
+ os << t << ' ';
+}
+
+
BinOp::BinOp(unique_ptr<Type> &&type, string &&name, Value &lhs, Value &rhs,
Op op, Flags flags)
: Instr(move(type), move(name)), lhs(lhs), rhs(rhs), op(op), flags(flags) {
@@ -50,10 +57,8 @@ void BinOp::print(ostream &os) const {
}
os << getName() << " = " << str << flag;
- auto t = getType().toString();
- if (!t.empty())
- os << t << ' ';
- os << lhs.getName() << ", " << rhs.getName() << '\n';
+ printType(os);
+ os << lhs.getName() << ", " << rhs.getName();
}
StateValue BinOp::toSMT(State &s) const {
@@ -153,6 +158,26 @@ expr BinOp::getTypeConstraints() const {
BinOp::~BinOp() {}
+
+void Return::print(ostream &os) const {
+ os << "return ";
+ printType(os);
+ os << val.getName();
+}
+
+StateValue Return::toSMT(State &s) const {
+ s.addReturn(s[val]);
+ return {};
+}
+
+expr Return::getTypeConstraints() const {
+ return getType().getTypeConstraints() &&
+ getType() == val.getType();
+}
+
+Return::~Return() {}
+
+
void Unreachable::print(ostream &os) const {
os << "unreachable";
}

MODIFY
ir/instr.h
ir/instr.h
@@ -9,8 +9,10 @@ namespace IR {
class Instr : public Value {
protected:
- Instr(std::unique_ptr<Type> &&type, std::string &&name)
- : Value(std::move(type), std::move(name)) {}
+ Instr(std::unique_ptr<Type> &&type, std::string &&name,
+ bool mk_unique_name = false)
+ : Value(std::move(type), std::move(name), mk_unique_name) {}
+ void printType(std::ostream &os) const;
};
@@ -35,6 +37,19 @@ public:
};
+class Return final : public Instr {
+ Value &val;
+public:
+ Return(std::unique_ptr<Type> &&type, Value &val) :
+ Instr(std::move(type), "return", true), val(val) {}
+
+ void print(std::ostream &os) const override;
+ StateValue toSMT(State &s) const override;
+ smt::expr getTypeConstraints() const override;
+ ~Return();
+};
+
+
class Unreachable final : public Instr {
public:
Unreachable() : Instr(std::make_unique<VoidType>(), "") {}

MODIFY
ir/state.cpp
ir/state.cpp
@@ -11,8 +11,8 @@ using namespace std;
namespace IR {
-StateValue StateValue::mkIf(const expr &cond, StateValue &&then,
- StateValue &&els) {
+StateValue StateValue::mkIf(const expr &cond, const StateValue &then,
+ const StateValue &els) {
return { expr::mkIf(cond, then.value, els.value),
expr::mkIf(cond, then.non_poison, els.non_poison) };
}
@@ -49,15 +49,14 @@ void State::addJump(const BasicBlock &bb) {
p.first->second |= domain;
}
-void State::addReturn(StateValue &&val) {
+void State::addReturn(const StateValue &val) {
if (returned) {
return_domain |= domain;
- return_val =
- StateValue::mkIf(domain, move(val), move(return_val));
+ return_val = StateValue::mkIf(domain, val, return_val);
} else {
returned = true;
return_domain = domain;
- return_val = move(val);
+ return_val = val;
}
}

MODIFY
ir/state.h
ir/state.h
@@ -17,8 +17,8 @@ struct StateValue {
StateValue(smt::expr &&value, smt::expr &&non_poison)
: value(std::move(value)), non_poison(std::move(non_poison)) {}
- static StateValue mkIf(const smt::expr &cond, StateValue &&then,
- StateValue &&els);
+ static StateValue mkIf(const smt::expr &cond, const StateValue &then,
+ const StateValue &els);
friend std::ostream& operator<<(std::ostream &os, const StateValue &val);
};
@@ -47,14 +47,17 @@ public:
bool startBB(const BasicBlock &bb);
void addJump(const BasicBlock &bb);
- void addReturn(StateValue &&val);
+ void addReturn(const StateValue &val);
void addUB(smt::expr &&ub) { domain &= std::move(ub); }
void addUB(const smt::expr &ub) { domain &= ub; }
void addQuantVar(const smt::expr &var);
auto& getFn() const { return f; }
const auto& getValues() const { return values; }
+
bool fnReturned() const { return returned; }
+ const smt::expr& returnDomain() const { return return_domain; }
+ const StateValue& returnVal() const { return return_val; }
};
}

MODIFY
ir/value.cpp
ir/value.cpp
@@ -16,8 +16,11 @@ static string fresh_id() {
namespace IR {
-Value::Value(unique_ptr<Type> &&type, string &&name)
+Value::Value(unique_ptr<Type> &&type, string &&name, bool mk_unique_name)
: type(move(type)), name(move(name)) {
+ if (mk_unique_name)
+ this->type->setName(getName() + '_' + fresh_id());
+ else
this->type->setName(getName());
}
@@ -36,8 +39,7 @@ ostream& operator<<(ostream &os, const Value &val) {
IntConst::IntConst(unique_ptr<Type> &&type, uint64_t val)
- : Value(move(type), to_string(val)), val(val) {
- getWType().setName(getName() + '_' + fresh_id());
+ : Value(move(type), to_string(val), true), val(val) {
getWType().enforceIntType();
}

MODIFY
ir/value.h
ir/value.h
@@ -19,7 +19,8 @@ class Value {
std::string name;
protected:
- Value(std::unique_ptr<Type> &&type, std::string &&name);
+ Value(std::unique_ptr<Type> &&type, std::string &&name,
+ bool mk_unique_name = false);
Type& getWType() { return *type.get(); }
public:

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -302,13 +302,21 @@ expr expr::operator*(const expr &rhs) const {
expr expr::sdiv(const expr &rhs) const {
C(rhs);
- // TODO: optimize
+
+ expr r;
+ if (binop_sfold(rhs, [](auto a, auto b) { return a / b; }, r))
+ return r;
+
return Z3_mk_bvsdiv(ctx(), ast(), rhs());
}
expr expr::udiv(const expr &rhs) const {
C(rhs);
- // TODO: optimize
+
+ expr r;
+ if (binop_ufold(rhs, [](auto a, auto b) { return a / b; }, r))
+ return r;
+
return Z3_mk_bvudiv(ctx(), ast(), rhs());
}

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -20,6 +20,7 @@ static void show_help() {
cerr <<
"Usage: alive2 <options> <files.opt>\n"
"Options:\n"
+ " -root-only:\tCheck the expression's root only\n"
" -v:\t\tverbose mode\n"
" -smt-stats:\tshow SMT statistics\n"
" -skip-smt:\tassume all SMT queries are UNSAT\n"
@@ -31,13 +32,18 @@ int main(int argc, char **argv) {
bool verbose = false;
bool show_smt_stats = false;
+ TransformVerifyOpts transform_opts;
+
int argc_i = 1;
for (; argc_i < argc; ++argc_i) {
if (argv[argc_i][0] != '-')
break;
string_view arg(argv[argc_i]);
- if (arg == "-v")
+ if (arg == "-root-only")
+ // FIXME: add a return instruction to each transform as needed
+ transform_opts.check_each_var = false;
+ else if (arg == "-v")
verbose = true;
else if (arg == "-smt-stats")
show_smt_stats = true;
@@ -87,7 +93,7 @@ int main(int argc, char **argv) {
unsigned i = 0;
for (; types; ++types) {
t.fixupTypes(types);
- if (auto errs = t.verify()) {
+ if (auto errs = t.verify(transform_opts)) {
cerr << errs;
++num_errors;
break;

MODIFY
tools/alive_lexer.re
tools/alive_lexer.re
@@ -135,6 +135,7 @@ re2c:yyfill:check = 0;
"nsw" { return NSW; }
"nuw" { return NUW; }
"exact" { return EXACT; }
+"return" { return RETURN; }
"unreachable" { return UNREACH; }
* { error("couldn't parse: '" + string((char*)YYTEXT, 16) + '\''); }

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -227,21 +227,32 @@ static unique_ptr<Instr> parse_instr(string_view name) {
UNREACHABLE();
}
+static unique_ptr<Instr> parse_return() {
+ auto type = parse_type(/*optional=*/true);
+ auto &val = parse_operand(type.get());
+ return make_unique<Return>(move(type), val);
+}
+
static void parse_fn(Function &f) {
fn = &f;
+ identifiers.clear();
BasicBlock *bb = &f.getBB("");
while (true) {
switch (auto t = *tokenizer) {
case IDENTIFIER: {
- auto i = parse_instr(yylval.str);
- identifiers.emplace(yylval.str, i.get());
+ string name(yylval.str);
+ auto i = parse_instr(name);
+ identifiers.emplace(move(name), i.get());
bb->addIntr(move(i));
break;
}
case LABEL:
bb = &f.getBB(yylval.str);
break;
+ case RETURN:
+ bb->addIntr(parse_return());
+ break;
case UNREACH:
bb->addIntr(make_unique<Unreachable>());
break;
@@ -270,6 +281,7 @@ vector<Transform> parse(string_view buf) {
parse_fn(t.tgt);
}
+ identifiers.clear();
return ret;
}

MODIFY
tools/tokens.h
tools/tokens.h
@@ -18,6 +18,7 @@ TOKEN(NSW)
TOKEN(NUM)
TOKEN(NUW)
TOKEN(PRE)
+TOKEN(RETURN)
TOKEN(SDIV)
TOKEN(SHL)
TOKEN(SUB)

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -15,9 +15,27 @@ using namespace smt;
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
+ // TODO: improve error messages
+ s.check({
+ { 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"); } },
+
+ { dom_a && a.non_poison && a.value != b.value, [&](const Model &m) {
+ errs.add("value mismatch");
+ } }
+ });
+}
+
namespace tools {
-Errors Transform::verify() const {
+Errors Transform::verify(const TransformVerifyOpts &opts) const {
Errors errs;
unordered_map<string, const Value*> tgt_vals;
@@ -30,26 +48,16 @@ Errors Transform::verify() const {
sym_exec(tgt_state);
Solver s;
+
+ if (opts.check_each_var) {
for (auto &[var, val] : src_state.getValues()) {
auto &name = var->getName();
- if (name.empty() || name[0] != '%')
+ if (name[0] != '%')
continue;
- auto &[srcv, srcp] = val;
- auto &[tgtv, tgtp] = tgt_state[*tgt_vals.at(name)];
-
- // TODO
- // add data-flow domain tracking for Alive, but not for TV?
- // finish these proof obligations
- // handle quantified vars
- s.check({
-// { srcd.notImplies(tgtd), "Source is more defined than target" },
- // { srcd && srcp.notImplies(tgtd), "foo" },
- { srcp && srcv != tgtv, [&](const Model &m) {
- errs.add("value mismatch");
- }}
+ // 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)]);
}
- );
}
if (src_state.fnReturned() != tgt_state.fnReturned()) {
@@ -59,7 +67,9 @@ Errors Transform::verify() const {
errs.add("Target returns but source doesn't");
} else if (src_state.fnReturned()) {
- // FIXME
+ check_refinement(s, errs,
+ src_state.returnDomain(), src_state.returnVal(),
+ tgt_state.returnDomain(), tgt_state.returnVal());
}
return errs;

MODIFY
tools/transform.h
tools/transform.h
@@ -30,11 +30,15 @@ public:
};
+struct TransformVerifyOpts {
+ bool check_each_var = true;
+};
+
struct Transform {
std::string name;
IR::Function src, tgt;
- util::Errors verify() const;
+ util::Errors verify(const TransformVerifyOpts &opts) const;
TypingAssignments getTypings() const;
void fixupTypes(const TypingAssignments &t);

MODIFY
util/symexec.cpp
util/symexec.cpp
@@ -31,9 +31,11 @@ void sym_exec(State &s) {
for (auto &i : bb->instrs()) {
auto val = i.toSMT(s);
- if (!i.getName().empty()) {
+ auto &name = i.getName();
+
+ if (name[0] == '%') {
if (config::symexec_print_each_value)
- cout << i.getName() << " = " << val << '\n';
+ cout << name << " = " << val << '\n';
s.add(i, move(val));
}
}

alive: add preliminary support for -root-only