type checking: simplify constraints sent to SMT solver
MODIFY
ir/type.cpp
ir/type.cpp
@@ -49,6 +49,9 @@ unsigned Type::bits() const {
}
expr Type::operator==(const Type &b) const {
+ if (this == &b)
+ return true;
+
#define CMP(Ty) \
if (auto lhs = dynamic_cast<const Ty*>(this)) { \
if (auto rhs = dynamic_cast<const Ty*>(&b)) \
@@ -108,22 +111,19 @@ void VoidType::print(ostream &os) const {
unsigned IntType::bits() const {
- assert(defined);
return bitwidth;
}
expr IntType::getTypeConstraints() const {
- auto c = isInt();
+ // limit ints to be between 1 and 64 bits
+ // TODO: lift 64-bit restriction
auto bw = sizeVar();
- if (defined) {
- c &= bw == expr::mkUInt(bitwidth, var_bw_bits);
+ return bw != expr::mkUInt(0, var_bw_bits) &&
+ bw.ule(expr::mkUInt(64, var_bw_bits));
}
- // limit ints to be between 1 and 64 bits
- // TODO: lift 64-bit restriction
- c &= bw.uge(expr::mkUInt(1, var_bw_bits));
- c &= bw.ule(expr::mkUInt(64, var_bw_bits));
- return c;
+expr IntType::sizeVar() const {
+ return defined ? expr::mkUInt(bits(), var_bw_bits) : Type::sizeVar();
}
expr IntType::operator==(const IntType &rhs) const {
@@ -131,9 +131,8 @@ expr IntType::operator==(const IntType &rhs) const {
}
void IntType::fixup(const Model &m) {
- assert(m.getUInt(typeVar()) == SymbolicType::Int);
+ if (!defined)
bitwidth = m.getUInt(sizeVar());
- defined = true;
}
void IntType::enforceIntType() {
@@ -156,16 +155,15 @@ void IntType::print(ostream &os) const {
expr FloatType::getTypeConstraints() const {
// TODO
- return isFloat() && false;
+ return false;
}
expr FloatType::operator==(const FloatType &rhs) const {
// TODO
- return true;
+ return false;
}
void FloatType::fixup(const Model &m) {
- assert(m.getUInt(typeVar()) == SymbolicType::Float);
// TODO
}
@@ -180,7 +178,7 @@ void FloatType::print(ostream &os) const {
expr PtrType::getTypeConstraints() const {
// TODO
- return isPtr() && false;
+ return false;
}
expr PtrType::operator==(const PtrType &rhs) const {
@@ -189,7 +187,6 @@ expr PtrType::operator==(const PtrType &rhs) const {
}
void PtrType::fixup(const Model &m) {
- assert(m.getUInt(typeVar()) == SymbolicType::Ptr);
// TODO
}
@@ -208,16 +205,15 @@ void PtrType::print(ostream &os) const {
expr ArrayType::getTypeConstraints() const {
// TODO
- return isArray() && false;
+ return false;
}
expr ArrayType::operator==(const ArrayType &rhs) const {
// TODO
- return true;
+ return false;
}
void ArrayType::fixup(const Model &m) {
- assert(m.getUInt(typeVar()) == SymbolicType::Array);
// TODO
}
@@ -232,16 +228,15 @@ void ArrayType::print(ostream &os) const {
expr VectorType::getTypeConstraints() const {
// TODO
- return isVector() && false;
+ return false;
}
expr VectorType::operator==(const VectorType &rhs) const {
// TODO
- return true;
+ return false;
}
void VectorType::fixup(const Model &m) {
- assert(m.getUInt(typeVar()) == SymbolicType::Vector);
// TODO
}

MODIFY
ir/type.h
ir/type.h
@@ -31,7 +31,7 @@ public:
virtual unsigned bits() const;
virtual smt::expr getTypeConstraints() const = 0;
- smt::expr sizeVar() const;
+ virtual smt::expr sizeVar() const;
smt::expr operator==(const Type &rhs) const;
virtual void fixup(const smt::Model &m) = 0;
@@ -57,7 +57,7 @@ public:
class IntType final : public Type {
- unsigned bitwidth = 0;
+ unsigned bitwidth;
bool defined = false;
public:
@@ -65,6 +65,7 @@ public:
IntType(unsigned bitwidth) : bitwidth(bitwidth), defined(true) {}
unsigned bits() const override;
smt::expr getTypeConstraints() const override;
+ smt::expr sizeVar() const override;
smt::expr operator==(const IntType &rhs) const;
void fixup(const smt::Model &m) override;
void enforceIntType() override;

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -31,8 +31,7 @@ static void show_help() {
int main(int argc, char **argv) {
bool verbose = false;
bool show_smt_stats = false;
-
- TransformVerifyOpts transform_opts;
+ bool check_each_var = true;
int argc_i = 1;
for (; argc_i < argc; ++argc_i) {
@@ -42,7 +41,7 @@ int main(int argc, char **argv) {
string_view arg(argv[argc_i]);
if (arg == "-root-only")
// FIXME: add a return instruction to each transform as needed
- transform_opts.check_each_var = false;
+ check_each_var = false;
else if (arg == "-v")
verbose = true;
else if (arg == "-smt-stats")
@@ -83,7 +82,8 @@ int main(int argc, char **argv) {
t.print(cout, print_opts);
cout << '\n';
- auto types = t.getTypings();
+ TransformVerify tv(t, check_each_var);
+ auto types = tv.getTypings();
if (!types) {
cerr << "Doesn't type check!\n";
++num_errors;
@@ -92,8 +92,8 @@ int main(int argc, char **argv) {
unsigned i = 0;
for (; types; ++types) {
- t.fixupTypes(types);
- if (auto errs = t.verify(transform_opts)) {
+ tv.fixupTypes(types);
+ if (auto errs = tv.verify()) {
cerr << errs;
++num_errors;
break;

MODIFY
tools/transform.cpp
tools/transform.cpp
#include "smt/solver.h"
#include "util/errors.h"
#include "util/symexec.h"
-#include <string>
-#include <unordered_map>
using namespace IR;
using namespace smt;
@@ -40,21 +38,25 @@ static void check_refinement(Solver &s, Errors &errs,
namespace tools {
-Errors Transform::verify(const TransformVerifyOpts &opts) const {
- unordered_map<string, const Value*> tgt_vals;
- for (auto &i : tgt.instrs()) {
+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);
}
+ }
+}
+Errors TransformVerify::verify() const {
Value::reset_gbl_id();
- State src_state(src), tgt_state(tgt);
+ State src_state(t.src), tgt_state(t.tgt);
sym_exec(src_state);
sym_exec(tgt_state);
Errors errs;
Solver s;
- if (opts.check_each_var) {
+ if (check_each_var) {
for (auto &[var, val] : src_state.getValues()) {
auto &name = var->getName();
if (name[0] != '%' || !dynamic_cast<const Instr*>(var))
@@ -95,15 +97,22 @@ void TypingAssignments::operator++(void) {
assert(!r.isUnknown());
}
-TypingAssignments Transform::getTypings() const {
+TypingAssignments TransformVerify::getTypings() const {
// TODO: missing cross-program type constraints
// e.g. for inputs and return values
- return { src.getTypeConstraints() && tgt.getTypeConstraints() };
+ auto c = t.src.getTypeConstraints() && t.tgt.getTypeConstraints();
+
+ if (check_each_var) {
+ for (auto &i : t.src.instrs()) {
+ c &= i.getType() == tgt_vals.at(i.getName())->getType();
+ }
+ }
+ return { move(c) };
}
-void Transform::fixupTypes(const TypingAssignments &t) {
- src.fixupTypes(t.r.getModel());
- tgt.fixupTypes(t.r.getModel());
+void TransformVerify::fixupTypes(const TypingAssignments &ty) {
+ t.src.fixupTypes(ty.r.getModel());
+ t.tgt.fixupTypes(ty.r.getModel());
}
void Transform::print(ostream &os, const TransformPrintOpts &opt) const {

MODIFY
tools/transform.h
tools/transform.h
#include "util/errors.h"
#include <string>
#include <ostream>
+#include <unordered_map>
namespace tools {
@@ -16,6 +17,15 @@ struct TransformPrintOpts {
};
+struct Transform {
+ std::string name;
+ IR::Function src, tgt;
+
+ void print(std::ostream &os, const TransformPrintOpts &opt) const;
+ friend std::ostream& operator<<(std::ostream &os, const Transform &t);
+};
+
+
class TypingAssignments {
smt::Solver s;
smt::Result r;
@@ -26,24 +36,20 @@ public:
operator bool() const { return r.isSat(); }
void operator++(void);
- friend struct Transform;
+ friend struct TransformVerify;
};
-struct TransformVerifyOpts {
- bool check_each_var = true;
-};
-
-struct Transform {
- std::string name;
- IR::Function src, tgt;
+class TransformVerify {
+ Transform &t;
+ std::unordered_map<std::string, const IR::Value*> tgt_vals;
+ bool check_each_var;
- util::Errors verify(const TransformVerifyOpts &opts) const;
+public:
+ TransformVerify(Transform &t, bool check_each_var);
+ util::Errors verify() const;
TypingAssignments getTypings() const;
- void fixupTypes(const TypingAssignments &t);
-
- void print(std::ostream &os, const TransformPrintOpts &opt) const;
- friend std::ostream& operator<<(std::ostream &os, const Transform &t);
+ void fixupTypes(const TypingAssignments &ty);
};
}

type checking: simplify constraints sent to SMT solver