typing: now does zero SMT queries if fully typed
MODIFY
ir/function.cpp
ir/function.cpp
@@ -9,10 +9,10 @@ using namespace std;
namespace IR {
-expr BasicBlock::getTypeConstraints() const {
+expr BasicBlock::getTypeConstraints(const Function &f) const {
expr t(true);
for (auto &i : instrs()) {
- t &= i.getTypeConstraints();
+ t &= i.getTypeConstraints(f);
}
return t;
}
@@ -42,7 +42,7 @@ ostream& operator<<(ostream &os, const BasicBlock &bb) {
expr Function::getTypeConstraints() const {
expr t(true);
for (auto bb : getBBs()) {
- t &= bb->getTypeConstraints();
+ t &= bb->getTypeConstraints(*this);
}
for (auto &l : { getConstants(), getInputs(), getUndefs() }) {
for (auto &v : l) {

MODIFY
ir/function.h
ir/function.h
@@ -18,6 +18,8 @@ namespace smt { class Model; }
namespace IR {
+class Function;
+
class BasicBlock {
std::string name;
std::vector<std::unique_ptr<Instr>> m_instrs;
@@ -26,7 +28,7 @@ public:
BasicBlock(std::string &&name) : name(std::move(name)) {}
BasicBlock(std::string_view name) : name(name) {}
- smt::expr getTypeConstraints() const;
+ smt::expr getTypeConstraints(const Function &f) const;
void fixupTypes(const smt::Model &m);
void addIntr(std::unique_ptr<Instr> &&i);
@@ -34,12 +36,14 @@ public:
util::const_strip_unique_ptr<decltype(m_instrs)> instrs() const {
return m_instrs;
}
+ Instr& back() { return *m_instrs.back(); }
friend std::ostream& operator<<(std::ostream &os, const BasicBlock &bb);
};
class Function {
+ IR::Type *type = nullptr;
std::string name;
std::unordered_map<std::string, BasicBlock> BBs;
std::vector<BasicBlock*> BB_order;
@@ -51,7 +55,11 @@ class Function {
public:
Function() {}
- Function(std::string &&name) : name(std::move(name)) {}
+ Function(Type &type, std::string &&name)
+ : type(&type), name(std::move(name)) {}
+
+ const IR::Type& getType() const { return *type; }
+ void setType(IR::Type &t) { type = &t; }
smt::expr getTypeConstraints() const;
void fixupTypes(const smt::Model &m);

MODIFY
ir/instr.cpp
ir/instr.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "ir/instr.h"
+#include "ir/function.h"
#include "smt/expr.h"
#include "smt/solver.h"
#include "util/compiler.h"
@@ -13,6 +14,16 @@ namespace IR {
VoidType Instr::voidTy("void");
+expr Instr::eqType(const Instr &i) const {
+ return getType() == i.getType();
+}
+
+expr Instr::getTypeConstraints() const {
+ UNREACHABLE();
+ return {};
+}
+
+
BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
Flags flags)
: Instr(type, move(name)), lhs(lhs), rhs(rhs), op(op), flags(flags) {
@@ -183,7 +194,7 @@ StateValue BinOp::toSMT(State &s) const {
return { move(val), move(not_poison) };
}
-expr BinOp::getTypeConstraints() const {
+expr BinOp::getTypeConstraints(const Function &f) const {
return Value::getTypeConstraints() &&
getType().enforceIntOrPtrOrVectorType() &&
getType() == lhs.getType() &&
@@ -225,7 +236,7 @@ StateValue ConversionOp::toSMT(State &s) const {
return { move(newval), expr(vp) };
}
-expr ConversionOp::getTypeConstraints() const {
+expr ConversionOp::getTypeConstraints(const Function &f) const {
expr sizeconstr;
switch (op) {
case SExt:
@@ -239,7 +250,6 @@ expr ConversionOp::getTypeConstraints() const {
// TODO: missing constraint comparing ty and to_ty (e.g. both ints)
return Value::getTypeConstraints() &&
getType().enforceIntOrPtrOrVectorType() &&
- val.getTypeConstraints() &&
val.getType().enforceIntOrPtrOrVectorType() && // FIXME: remove
move(sizeconstr);
}
@@ -258,9 +268,8 @@ StateValue Select::toSMT(State &s) const {
cp && expr::mkIf(cond, ap, bp) };
}
-expr Select::getTypeConstraints() const {
- return cond.getTypeConstraints() &&
- cond.getType().enforceIntType() &&
+expr Select::getTypeConstraints(const Function &f) const {
+ return cond.getType().enforceIntType() &&
cond.getType().sizeVar() == 1u &&
Value::getTypeConstraints() &&
getType().enforceIntOrPtrOrVectorType() &&
@@ -270,9 +279,13 @@ expr Select::getTypeConstraints() const {
ICmp::ICmp(Type &type, string &&name, Cond cond, Value &a, Value &b)
- : Instr(type, move(name)), a(a), b(b), cond(cond) {
- auto str = getName() + "_cond";
+ : Instr(type, move(name)), a(a), b(b), cond(cond), defined(cond != Any) {
+ if (!defined) {
+ auto str = getName() + "_cond" + fresh_id();
cond_var = expr::mkVar(str.c_str(), 4);
+ } else {
+ cond_var = expr::mkUInt(cond, 4);
+ }
}
void ICmp::print(ostream &os) const {
@@ -314,22 +327,33 @@ StateValue ICmp::toSMT(State &s) const {
return { expr::mkIf(val, expr::mkUInt(1,1), expr::mkUInt(0,1)), ap && bp };
}
-expr ICmp::getTypeConstraints() const {
- return Value::getTypeConstraints() &&
+expr ICmp::getTypeConstraints(const Function &f) const {
+ expr e = Value::getTypeConstraints() &&
getType().enforceIntType() &&
getType().sizeVar() == 1u &&
- a.getTypeConstraints() &&
a.getType().enforceIntOrPtrOrVectorType() &&
- a.getType() == b.getType() &&
- (cond == Any ? cond_var.ule(expr::mkUInt(9, 4))
- : cond_var == expr::mkUInt(cond, 4));
+ a.getType() == b.getType();
+ if (!defined)
+ e &= cond_var.ule(expr::mkUInt(9, 4));
+ return e;
}
void ICmp::fixupTypes(const Model &m) {
Value::fixupTypes(m);
+ if (!defined)
cond = (Cond)m.getUInt(cond_var);
}
+expr ICmp::eqType(const Instr &i) const {
+ expr eq = Instr::eqType(i);
+ if (auto rhs = dynamic_cast<const ICmp*>(&i)) {
+ if (!defined || !rhs->defined) {
+ eq &= cond_var == rhs->cond_var;
+ }
+ }
+ return eq;
+}
+
void Freeze::print(ostream &os) const {
os << getName() << " = freeze " << val;
@@ -352,7 +376,7 @@ StateValue Freeze::toSMT(State &s) const {
true };
}
-expr Freeze::getTypeConstraints() const {
+expr Freeze::getTypeConstraints(const Function &f) const {
return Value::getTypeConstraints() &&
getType() == val.getType();
}
@@ -366,7 +390,7 @@ StateValue CopyOp::toSMT(State &s) const {
return s[val];
}
-expr CopyOp::getTypeConstraints() const {
+expr CopyOp::getTypeConstraints(const Function &f) const {
return Value::getTypeConstraints() &&
getType() == val.getType();
}
@@ -381,9 +405,10 @@ StateValue Return::toSMT(State &s) const {
return {};
}
-expr Return::getTypeConstraints() const {
+expr Return::getTypeConstraints(const Function &f) const {
return Value::getTypeConstraints() &&
- getType() == val.getType();
+ getType() == val.getType() &&
+ f.getType() == getType();
}
@@ -396,7 +421,7 @@ StateValue Unreachable::toSMT(State &s) const {
return {};
}
-expr Unreachable::getTypeConstraints() const {
+expr Unreachable::getTypeConstraints(const Function &f) const {
return true;
}

MODIFY
ir/instr.h
ir/instr.h
namespace IR {
+class Function;
+
+
class Instr : public Value {
protected:
static VoidType voidTy;
Instr(Type &type, std::string &&name) : Value(type, std::move(name)) {}
+
+public:
+ virtual smt::expr eqType(const Instr &i) const;
+ smt::expr getTypeConstraints() const override;
+ virtual smt::expr getTypeConstraints(const Function &f) const = 0;
};
@@ -31,7 +39,7 @@ public:
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
};
@@ -48,7 +56,7 @@ public:
: Instr(type, std::move(name)), val(val), op(op) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
};
@@ -59,7 +67,7 @@ public:
: Instr(type, move(name)), cond(cond), a(a), b(b) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
};
@@ -71,13 +79,15 @@ private:
Value &a, &b;
smt::expr cond_var;
Cond cond;
+ bool defined;
public:
ICmp(Type &type, std::string &&name, Cond cond, Value &a, Value &b);
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
void fixupTypes(const smt::Model &m) override;
+ smt::expr eqType(const Instr &i) const override;
};
@@ -89,7 +99,7 @@ public:
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
};
@@ -101,7 +111,7 @@ public:
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
};
@@ -112,7 +122,7 @@ public:
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
};
@@ -122,7 +132,7 @@ public:
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
+ smt::expr getTypeConstraints(const Function &f) const override;
};
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -233,6 +233,7 @@ bool expr::isSMax() const {
}
unsigned expr::bits() const {
+ C();
return Z3_get_bv_sort_size(ctx(), sort());
}

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -375,6 +375,7 @@ static void parse_fn(Function &f) {
fn = &f;
identifiers.clear();
BasicBlock *bb = &f.getBB("");
+ bool has_return = false;
while (true) {
switch (auto t = *tokenizer) {
@@ -388,9 +389,13 @@ static void parse_fn(Function &f) {
case LABEL:
bb = &f.getBB(yylval.str);
break;
- case RETURN:
- bb->addIntr(parse_return());
+ case RETURN: {
+ auto instr = parse_return();
+ f.setType(instr->getType());
+ bb->addIntr(move(instr));
+ has_return = true;
break;
+ }
case UNREACH:
bb->addIntr(make_unique<Unreachable>());
break;
@@ -399,6 +404,13 @@ static void parse_fn(Function &f) {
return;
}
}
+
+ // FIXME: if target: copy relevant src instructions
+ // FIXME: add error checking
+ if (!has_return) {
+ auto &last = bb->back();
+ f.setType(last.getType());
+ }
}
static void parse_arrow() {

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -90,7 +90,7 @@ TransformVerify::TransformVerify(Transform &t, bool check_each_var) :
t(t), check_each_var(check_each_var) {
if (check_each_var) {
for (auto &i : t.tgt.instrs()) {
- tgt_vals.emplace(i.getName(), &i);
+ tgt_instrs.emplace(i.getName(), &i);
}
}
}
@@ -111,7 +111,7 @@ Errors TransformVerify::verify() const {
// TODO: add data-flow domain tracking for Alive, but not for TV
check_refinement(errs, t, src_state.getQuantVars(),
- true, val, true, tgt_state.at(*tgt_vals.at(name)));
+ true, val, true, tgt_state.at(*tgt_instrs.at(name)));
if (errs)
return errs;
}
@@ -159,13 +159,12 @@ void TypingAssignments::operator++(void) {
}
TypingAssignments TransformVerify::getTypings() const {
- // TODO: missing cross-program type constraints
- // e.g. for inputs and return values
auto c = t.src.getTypeConstraints() && t.tgt.getTypeConstraints();
+ c &= t.src.getType() == t.tgt.getType();
if (check_each_var) {
for (auto &i : t.src.instrs()) {
- c &= i.getType() == tgt_vals.at(i.getName())->getType();
+ c &= i.eqType(*tgt_instrs.at(i.getName()));
}
}
return { move(c) };

MODIFY
tools/transform.h
tools/transform.h
@@ -44,7 +44,7 @@ public:
class TransformVerify {
Transform &t;
- std::unordered_map<std::string, const IR::Value*> tgt_vals;
+ std::unordered_map<std::string, const IR::Instr*> tgt_instrs;
bool check_each_var;
public:

typing: now does zero SMT queries if fully typed