type refactoring: values don't own types anymore
this avoids copies and simplifies constraints for solver (due to sharing)
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -11,11 +11,11 @@ using namespace std;
namespace IR {
-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) {
- getWType().enforceIntOrPtrOrVectorType();
+VoidType Instr::voidTy("void");
+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) {
switch (op) {
case Add:
case Sub:
@@ -184,20 +184,14 @@ StateValue BinOp::toSMT(State &s) const {
}
expr BinOp::getTypeConstraints() const {
- return getType().getTypeConstraints() &&
+ return Value::getTypeConstraints() &&
+ getType().enforceIntOrPtrOrVectorType() &&
getType() == lhs.getType() &&
getType() == rhs.getType();
}
-ConversionOp::ConversionOp(unique_ptr<Type> &&type, string &&name, Value &val,
- Op op) :
- Instr(move(type), move(name)), val(val), op(op) {
- getWType().enforceIntOrPtrOrVectorType();
- val.getWType().enforceIntOrPtrOrVectorType();
-}
-
-void ConversionOp::print(std::ostream &os) const {
+void ConversionOp::print(ostream &os) const {
const char *str = nullptr;
switch (op) {
case SExt: str = "sext "; break;
@@ -243,22 +237,15 @@ expr ConversionOp::getTypeConstraints() const {
break;
}
// TODO: missing constraint comparing ty and to_ty (e.g. both ints)
- return getType().getTypeConstraints() &&
+ return Value::getTypeConstraints() &&
+ getType().enforceIntOrPtrOrVectorType() &&
val.getTypeConstraints() &&
+ val.getType().enforceIntOrPtrOrVectorType() && // FIXME: remove
move(sizeconstr);
}
-Select::Select(unique_ptr<Type> &&type, string &&name, Value &cond, Value &a,
- Value &b)
- : Instr(move(type), move(name)), cond(cond), a(a), b(b) {
- getWType().enforceIntOrPtrOrVectorType();
- cond.getWType().enforceIntType();
- a.getWType().enforceIntOrPtrOrVectorType();
- b.getWType().enforceIntOrPtrOrVectorType();
-}
-
-void Select::print(std::ostream &os) const {
+void Select::print(ostream &os) const {
os << getName() << " = select " << cond << ", " << a << ", " << b;
}
@@ -273,18 +260,17 @@ StateValue Select::toSMT(State &s) const {
expr Select::getTypeConstraints() const {
return cond.getTypeConstraints() &&
+ cond.getType().enforceIntType() &&
cond.getType().sizeVar() == 1u &&
- getType().getTypeConstraints() &&
+ Value::getTypeConstraints() &&
+ getType().enforceIntOrPtrOrVectorType() &&
getType() == a.getType() &&
getType() == b.getType();
}
-ICmp::ICmp(std::string &&name, Cond cond, Value &a, Value &b) :
- Instr(make_unique<IntType>(1), move(name)), a(a), b(b), cond(cond) {
- a.getWType().enforceIntOrPtrOrVectorType();
- b.getWType().enforceIntOrPtrOrVectorType();
-
+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";
cond_var = expr::mkVar(str.c_str(), 4);
}
@@ -329,8 +315,11 @@ StateValue ICmp::toSMT(State &s) const {
}
expr ICmp::getTypeConstraints() const {
- return getType().getTypeConstraints() &&
+ return 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));
@@ -364,7 +353,7 @@ StateValue Freeze::toSMT(State &s) const {
}
expr Freeze::getTypeConstraints() const {
- return getType().getTypeConstraints() &&
+ return Value::getTypeConstraints() &&
getType() == val.getType();
}
@@ -378,7 +367,7 @@ StateValue CopyOp::toSMT(State &s) const {
}
expr CopyOp::getTypeConstraints() const {
- return getType().getTypeConstraints() &&
+ return Value::getTypeConstraints() &&
getType() == val.getType();
}
@@ -393,7 +382,7 @@ StateValue Return::toSMT(State &s) const {
}
expr Return::getTypeConstraints() const {
- return getType().getTypeConstraints() &&
+ return Value::getTypeConstraints() &&
getType() == val.getType();
}

MODIFY
ir/instr.h
ir/instr.h
@@ -9,9 +9,8 @@ namespace IR {
class Instr : public Value {
protected:
- Instr(std::unique_ptr<Type> &&type, std::string &&name,
- bool mk_unique_name = false)
- : Value(std::move(type), std::move(name), mk_unique_name) {}
+ static VoidType voidTy;
+ Instr(Type &type, std::string &&name) : Value(type, std::move(name)) {}
};
@@ -27,8 +26,8 @@ private:
Flags flags;
public:
- BinOp(std::unique_ptr<Type> &&type, std::string &&name, Value &lhs,
- Value &rhs, Op op, Flags flags = None);
+ BinOp(Type &type, std::string &&name, Value &lhs, Value &rhs, Op op,
+ Flags flags = None);
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
@@ -45,8 +44,8 @@ private:
Op op;
public:
- ConversionOp(std::unique_ptr<Type> &&type, std::string &&name, Value &val,
- Op op);
+ ConversionOp(Type &type, std::string &&name, Value &val, Op op)
+ : 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;
@@ -56,8 +55,8 @@ public:
class Select final : public Instr {
Value &cond, &a, &b;
public:
- Select(std::unique_ptr<Type> &&type, std::string &&name, Value &cond,
- Value &a, Value &b);
+ Select(Type &type, std::string &&name, Value &cond, Value &a, Value &b)
+ : 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;
@@ -74,7 +73,7 @@ private:
Cond cond;
public:
- ICmp(std::string &&name, Cond cond, Value &a, Value &b);
+ 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;
@@ -85,8 +84,8 @@ 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) {}
+ Freeze(Type &type, std::string &&name, Value &val)
+ : Instr(type, std::move(name)), val(val) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
@@ -97,8 +96,8 @@ public:
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) {}
+ CopyOp(Type &type, std::string &&name, Value &val)
+ : Instr(type, std::move(name)), val(val) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
@@ -109,8 +108,7 @@ 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) {}
+ Return(Type &type, Value &val) : Instr(type, "return"), val(val) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
@@ -120,7 +118,7 @@ public:
class Unreachable final : public Instr {
public:
- Unreachable() : Instr(std::make_unique<VoidType>(), "") {}
+ Unreachable() : Instr(Instr::voidTy, "") {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;

MODIFY
ir/type.cpp
ir/type.cpp
@@ -17,8 +17,7 @@ static constexpr unsigned var_bw_bits = 10;
namespace IR {
expr Type::var(const char *var, unsigned bits) const {
- assert(!opname.empty());
- auto str = opname + '_' + var;
+ auto str = name + '_' + var;
return expr::mkVar(str.c_str(), bits);
}
@@ -40,10 +39,6 @@ expr Type::isPtr() const { return is(SymbolicType::Ptr); }
expr Type::isArray() const { return is(SymbolicType::Array); }
expr Type::isVector() const { return is(SymbolicType::Vector); }
-void Type::setName(const string &name) {
- opname = name;
-}
-
unsigned Type::bits() const {
UNREACHABLE();
}
@@ -76,12 +71,12 @@ expr Type::operator==(const Type &b) const {
return false;
}
-void Type::enforceIntType() {
- UNREACHABLE();
+expr Type::enforceIntType() const {
+ return false;
}
-void Type::enforceIntOrPtrOrVectorType() {
- UNREACHABLE();
+expr Type::enforceIntOrPtrOrVectorType() const {
+ return false;
}
string Type::toString() const {
@@ -101,10 +96,6 @@ void VoidType::fixup(const Model &m) {
// do nothing
}
-unique_ptr<Type> VoidType::dup() const {
- return make_unique<VoidType>();
-}
-
void VoidType::print(ostream &os) const {
os << "void";
}
@@ -135,16 +126,12 @@ void IntType::fixup(const Model &m) {
bitwidth = m.getUInt(sizeVar());
}
-void IntType::enforceIntType() {
- // do nothing
-}
-
-void IntType::enforceIntOrPtrOrVectorType() {
- // do nothing
+expr IntType::enforceIntType() const {
+ return true;
}
-unique_ptr<Type> IntType::dup() const {
- return make_unique<IntType>(*this);
+expr IntType::enforceIntOrPtrOrVectorType() const {
+ return true;
}
void IntType::print(ostream &os) const {
@@ -167,10 +154,6 @@ void FloatType::fixup(const Model &m) {
// TODO
}
-unique_ptr<Type> FloatType::dup() const {
- return make_unique<FloatType>(*this);
-}
-
void FloatType::print(ostream &os) const {
os << "TODO";
}
@@ -190,12 +173,8 @@ void PtrType::fixup(const Model &m) {
// TODO
}
-void PtrType::enforceIntOrPtrOrVectorType() {
- // do nothing
-}
-
-unique_ptr<Type> PtrType::dup() const {
- return make_unique<PtrType>(*this);
+expr PtrType::enforceIntOrPtrOrVectorType() const {
+ return true;
}
void PtrType::print(ostream &os) const {
@@ -217,10 +196,6 @@ void ArrayType::fixup(const Model &m) {
// TODO
}
-unique_ptr<Type> ArrayType::dup() const {
- return make_unique<ArrayType>(*this);
-}
-
void ArrayType::print(ostream &os) const {
os << "TODO";
}
@@ -240,12 +215,8 @@ void VectorType::fixup(const Model &m) {
// TODO
}
-void VectorType::enforceIntOrPtrOrVectorType() {
- // do nothing
-}
-
-unique_ptr<Type> VectorType::dup() const {
- return make_unique<VectorType>(*this);
+expr VectorType::enforceIntOrPtrOrVectorType() const {
+ return true;
}
void VectorType::print(ostream &os) const {
@@ -253,35 +224,9 @@ void VectorType::print(ostream &os) const {
}
-expr SymbolicType::isInt() const {
- return expr(enabled & (1 << Int)) && Type::isInt();
-}
-
-expr SymbolicType::isFloat() const {
- return expr(enabled & (1 << Float)) && Type::isFloat();
-}
-
-expr SymbolicType::isPtr() const {
- return expr(enabled & (1 << Ptr)) && Type::isPtr();
-}
-
-expr SymbolicType::isVector() const {
- return expr(enabled & (1 << Vector)) && Type::isVector();
-}
-
-expr SymbolicType::isArray() const {
- return expr(enabled & (1 << Array)) && Type::isArray();
-}
-
-void SymbolicType::setName(const string &opname) {
- auto &str = name.empty() ? opname : name;
- i.setName(str);
- f.setName(str);
- p.setName(str);
- a.setName(str);
- v.setName(str);
- Type::setName(str);
-}
+SymbolicType::SymbolicType(string &&name)
+ : Type(string(name)), i(string(name)), f(string(name)), p(string(name)),
+ a(string(name)), v(string(name)) {}
unsigned SymbolicType::bits() const {
switch (typ) {
@@ -307,6 +252,9 @@ expr SymbolicType::getTypeConstraints() const {
}
expr SymbolicType::operator==(const Type &b) const {
+ if (this == &b)
+ return true;
+
if (auto rhs = dynamic_cast<const IntType*>(&b))
return isInt() && i == *rhs;
if (auto rhs = dynamic_cast<const FloatType*>(&b))
@@ -334,7 +282,6 @@ expr SymbolicType::operator==(const Type &b) const {
void SymbolicType::fixup(const Model &m) {
unsigned smt_typ = m.getUInt(typeVar());
assert(smt_typ >= Int && smt_typ <= Vector);
- assert((1 << smt_typ) & enabled);
typ = TypeNum(smt_typ);
switch (typ) {
@@ -348,16 +295,12 @@ void SymbolicType::fixup(const Model &m) {
}
}
-void SymbolicType::enforceIntType() {
- enabled &= (1 << Int);
-}
-
-void SymbolicType::enforceIntOrPtrOrVectorType() {
- enabled &= (1 << Int) | (1 << Ptr) | (1 << Vector);
+expr SymbolicType::enforceIntType() const {
+ return isInt();
}
-unique_ptr<Type> SymbolicType::dup() const {
- return make_unique<SymbolicType>(*this);
+expr SymbolicType::enforceIntOrPtrOrVectorType() const {
+ return isInt() || isPtr() || isVector();
}
void SymbolicType::print(ostream &os) const {

MODIFY
ir/type.h
ir/type.h
@@ -13,10 +13,8 @@ namespace smt { class Model; }
namespace IR {
class Type {
- // name of associated operand
- std::string opname;
-
protected:
+ std::string name;
smt::expr var(const char *var, unsigned bits) const;
smt::expr typeVar() const;
smt::expr is(unsigned t) const;
@@ -27,7 +25,7 @@ protected:
smt::expr isVector() const;
public:
- virtual void setName(const std::string &name);
+ Type(std::string &&name) : name(std::move(name)) {}
virtual unsigned bits() const;
virtual smt::expr getTypeConstraints() const = 0;
@@ -35,10 +33,9 @@ public:
smt::expr operator==(const Type &rhs) const;
virtual void fixup(const smt::Model &m) = 0;
- virtual void enforceIntType();
- virtual void enforceIntOrPtrOrVectorType();
+ virtual smt::expr enforceIntType() const;
+ virtual smt::expr enforceIntOrPtrOrVectorType() const;
- virtual std::unique_ptr<Type> dup() const = 0;
virtual void print(std::ostream &os) const = 0;
std::string toString() const;
@@ -48,10 +45,9 @@ public:
class VoidType final : public Type {
public:
- VoidType() {}
+ VoidType(std::string &&name) : Type(std::move(name)) {}
smt::expr getTypeConstraints() const override;
void fixup(const smt::Model &m) override;
- std::unique_ptr<Type> dup() const override;
void print(std::ostream &os) const override;
};
@@ -61,62 +57,59 @@ class IntType final : public Type {
bool defined = false;
public:
- IntType() {}
- IntType(unsigned bitwidth) : bitwidth(bitwidth), defined(true) {}
+ IntType(std::string &&name) : Type(std::move(name)) {}
+ IntType(std::string &&name, unsigned bitwidth)
+ : Type(std::move(name)), 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;
- void enforceIntOrPtrOrVectorType() override;
- std::unique_ptr<Type> dup() const override;
+ smt::expr enforceIntType() const override;
+ smt::expr enforceIntOrPtrOrVectorType() const override;
void print(std::ostream &os) const override;
};
class FloatType final : public Type {
public:
- FloatType() {}
+ FloatType(std::string &&name) : Type(std::move(name)) {}
smt::expr getTypeConstraints() const override;
smt::expr operator==(const FloatType &rhs) const;
void fixup(const smt::Model &m) override;
- std::unique_ptr<Type> dup() const override;
void print(std::ostream &os) const override;
};
class PtrType final : public Type {
public:
- PtrType() {}
+ PtrType(std::string &&name) : Type(std::move(name)) {}
smt::expr getTypeConstraints() const override;
smt::expr operator==(const PtrType &rhs) const;
void fixup(const smt::Model &m) override;
- void enforceIntOrPtrOrVectorType() override;
- std::unique_ptr<Type> dup() const override;
+ smt::expr enforceIntOrPtrOrVectorType() const override;
void print(std::ostream &os) const override;
};
class ArrayType final : public Type {
public:
- ArrayType() {}
+ ArrayType(std::string &&name) : Type(std::move(name)) {}
smt::expr getTypeConstraints() const override;
smt::expr operator==(const ArrayType &rhs) const;
void fixup(const smt::Model &m) override;
- std::unique_ptr<Type> dup() const override;
void print(std::ostream &os) const override;
};
class VectorType final : public Type {
public:
- VectorType() {}
+ VectorType(std::string &&name) : Type(std::move(name)) {}
smt::expr getTypeConstraints() const override;
smt::expr operator==(const VectorType &rhs) const;
void fixup(const smt::Model &m) override;
- void enforceIntOrPtrOrVectorType() override;
- std::unique_ptr<Type> dup() const override;
+ smt::expr enforceIntOrPtrOrVectorType() const override;
void print(std::ostream &os) const override;
};
@@ -126,33 +119,21 @@ public:
enum TypeNum { Int, Float, Ptr, Array, Vector, Undefined };
private:
- std::string name;
TypeNum typ = Undefined;
- unsigned enabled = (1 << Int) | (1 << Float) | (1 << Ptr) | (1 << Array) |
- (1 << Vector);
IntType i;
FloatType f;
PtrType p;
ArrayType a;
VectorType v;
- smt::expr isInt() const;
- smt::expr isFloat() const;
- smt::expr isPtr() const;
- smt::expr isArray() const;
- smt::expr isVector() const;
-
public:
- SymbolicType() {}
- SymbolicType(std::string &&name) : name(std::move(name)) {}
- void setName(const std::string &name) override;
+ SymbolicType(std::string &&name);
unsigned bits() const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const Type &rhs) const;
void fixup(const smt::Model &m) override;
- void enforceIntType() override;
- void enforceIntOrPtrOrVectorType() override;
- std::unique_ptr<Type> dup() const override;
+ smt::expr enforceIntType() const override;
+ smt::expr enforceIntOrPtrOrVectorType() const override;
void print(std::ostream &os) const override;
};

MODIFY
ir/value.cpp
ir/value.cpp
@@ -21,20 +21,14 @@ 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)
- this->type->setName(getName() + '_' + fresh_id());
- else
- this->type->setName(getName());
+expr Value::getTypeConstraints() const {
+ return getType().getTypeConstraints();
}
void Value::fixupTypes(const Model &m) {
- type->fixup(m);
+ type.fixup(m);
}
-Value::~Value() {}
-
ostream& operator<<(ostream &os, const Value &val) {
auto t = val.getType().toString();
if (!t.empty())
@@ -43,10 +37,8 @@ ostream& operator<<(ostream &os, const Value &val) {
}
-IntConst::IntConst(unique_ptr<Type> &&type, int64_t val)
- : Value(move(type), to_string(val), true), val(val) {
- getWType().enforceIntType();
-}
+IntConst::IntConst(Type &type, int64_t val)
+ : Value(type, to_string(val)), val(val) {}
void IntConst::print(ostream &os) const {
UNREACHABLE();
@@ -58,16 +50,14 @@ StateValue IntConst::toSMT(State &s) const {
expr IntConst::getTypeConstraints() const {
unsigned min_bits = (val >= 0 ? 63 : 64) - num_sign_bits(val);
- return getType().getTypeConstraints() &&
+ return Value::getTypeConstraints() &&
+ getType().enforceIntType() &&
getType().sizeVar().uge(min_bits);
}
-UndefValue::UndefValue(unique_ptr<Type> &&type)
- : Value(std::move(type), "undef", true) {}
-
void UndefValue::print(ostream &os) const {
- os << "undef";
+ UNREACHABLE();
}
StateValue UndefValue::toSMT(State &s) const {
@@ -77,33 +67,22 @@ StateValue UndefValue::toSMT(State &s) const {
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";
+ UNREACHABLE();
}
StateValue PoisonValue::toSMT(State &s) const {
return { {}, false };
}
-expr PoisonValue::getTypeConstraints() const {
- return getType().getTypeConstraints();
-}
-
void Input::print(std::ostream &os) const {
- os << getName();
+ UNREACHABLE();
}
StateValue Input::toSMT(State &s) const {
@@ -122,8 +101,4 @@ StateValue Input::toSMT(State &s) const {
type.extract(1,1) == expr::mkUInt(0, 1) };
}
-expr Input::getTypeConstraints() const {
- return getType().getTypeConstraints();
-}
-
}

MODIFY
ir/value.h
ir/value.h
#include "ir/state.h"
#include "ir/type.h"
#include "smt/expr.h"
-#include <memory>
#include <ostream>
#include <string>
@@ -15,26 +14,24 @@ namespace smt { class Model; }
namespace IR {
class Value {
- std::unique_ptr<Type> type;
+ Type &type;
std::string name;
protected:
- Value(std::unique_ptr<Type> &&type, std::string &&name,
- bool mk_unique_name = false);
+ Value(Type &type, std::string &&name)
+ : type(type), name(std::move(name)) {}
static std::string fresh_id();
public:
- unsigned bits() const { return type->bits(); }
- const std::string& getName() const { return name; }
- const Type& getType() const { return *type.get(); }
- Type& getWType() { return *type.get(); }
+ auto bits() const { return type.bits(); }
+ auto& getName() const { return name; }
+ auto& getType() const { return type; }
virtual void print(std::ostream &os) const = 0;
virtual StateValue toSMT(State &s) const = 0;
- virtual smt::expr getTypeConstraints() const = 0;
+ virtual smt::expr getTypeConstraints() const;
virtual void fixupTypes(const smt::Model &m);
- virtual ~Value();
static void reset_gbl_id();
@@ -46,7 +43,7 @@ class IntConst final : public Value {
int64_t val;
public:
- IntConst(std::unique_ptr<Type> &&type, int64_t val);
+ IntConst(Type &type, int64_t val);
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
smt::expr getTypeConstraints() const override;
@@ -55,10 +52,9 @@ public:
class UndefValue final : public Value {
public:
- UndefValue(std::unique_ptr<Type> &&type);
+ UndefValue(Type &type) : Value(type, "undef") {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
static std::string getFreshName();
};
@@ -66,20 +62,18 @@ public:
class PoisonValue final : public Value {
public:
- PoisonValue(std::unique_ptr<Type> &&type);
+ PoisonValue(Type &type) : Value(type, "poison") {}
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) :
- Value(std::move(type), std::move(name)) {}
+ Input(Type &type, std::string &&name) :
+ Value(type, std::move(name)) {}
void print(std::ostream &os) const override;
StateValue toSMT(State &s) const override;
- smt::expr getTypeConstraints() const override;
};
}

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -68,6 +68,7 @@ int main(int argc, char **argv) {
}
smt::smt_initializer smt_init;
+ init_parser();
TransformPrintOpts print_opts;
print_opts.print_fn_header = false;

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
#include "tools/alive_lexer.h"
#include "util/compiler.h"
#include <cassert>
-#include <iostream>
-#include <string>
-#include <string_view>
+#include <memory>
+#include <unordered_map>
#define YYDEBUG 0
+#if YYDEBUG
+#include <iostream>
+#endif
+
using namespace IR;
using namespace tools;
using namespace std;
@@ -27,8 +30,8 @@ static void error(string &&s) {
static unordered_map<string, Value*> identifiers;
static Function *fn;
-static Value& get_constant(uint64_t n, Type *t) {
- auto c = make_unique<IntConst>(t->dup(), n);
+static Value& get_constant(uint64_t n, Type &t) {
+ auto c = make_unique<IntConst>(t, n);
auto ret = c.get();
fn->addConstant(move(c));
return *ret;
@@ -113,14 +116,23 @@ static void parse_comma() {
tokenizer.ensure(COMMA);
}
-static unique_ptr<Type> parse_type(bool optional = true) {
+
+static vector<unique_ptr<IntType>> int_types;
+static vector<unique_ptr<SymbolicType>> sym_types;
+static unsigned sym_num;
+
+static Type& parse_type(bool optional = true) {
switch (auto t = *tokenizer) {
case INT_TYPE:
- return make_unique<IntType>(yylval.num);
+ if (yylval.num <= 64)
+ return *int_types[yylval.num].get();
+ error("Int type too long: " + to_string(yylval.num));
+ break;
default:
if (optional) {
tokenizer.unget(t);
- return make_unique<SymbolicType>();
+ auto t = make_unique<SymbolicType>("symty_" + to_string(sym_num++));
+ return *sym_types.emplace_back(move(t)).get();
} else {
error(string("Expecting a type, got: ") + token_name[t]);
}
@@ -128,7 +140,7 @@ static unique_ptr<Type> parse_type(bool optional = true) {
UNREACHABLE();
}
-static Value& parse_operand(Type *type) {
+static Value& parse_operand(Type &type) {
switch (auto t = *tokenizer) {
case NUM:
// FIXME: constraint type to int
@@ -139,13 +151,13 @@ static Value& parse_operand(Type *type) {
case FALSE:
return get_constant(0, type);
case UNDEF: {
- auto val = make_unique<UndefValue>(type->dup());
+ auto val = make_unique<UndefValue>(type);
auto ret = val.get();
fn->addUndef(move(val));
return *ret;
}
case POISON: {
- auto val = make_unique<PoisonValue>(type->dup());
+ auto val = make_unique<PoisonValue>(type);
auto ret = val.get();
fn->addConstant(move(val));
return *ret;
@@ -156,7 +168,7 @@ static Value& parse_operand(Type *type) {
I != identifiers.end())
return *I->second;
- auto input = make_unique<Input>(type->dup(), string(id));
+ auto input = make_unique<Input>(type, string(id));
auto ret = input.get();
fn->addInput(move(input));
identifiers.emplace(move(id), ret);
@@ -213,10 +225,10 @@ static BinOp::Flags parse_binop_flags(token op_token) {
static unique_ptr<Instr> parse_binop(string_view name, token op_token) {
BinOp::Flags flags = parse_binop_flags(op_token);
- auto type = parse_type();
- auto &a = parse_operand(type.get());
+ auto &type = parse_type();
+ auto &a = parse_operand(type);
parse_comma();
- auto &b = parse_operand(type.get());
+ auto &b = parse_operand(type);
BinOp::Op op;
switch (op_token) {
@@ -236,14 +248,14 @@ static unique_ptr<Instr> parse_binop(string_view name, token op_token) {
default:
UNREACHABLE();
}
- return make_unique<BinOp>(move(type), string(name), a, b, op, flags);
+ return make_unique<BinOp>(type, string(name), a, b, op, flags);
}
static unique_ptr<Instr> parse_conversionop(string_view name, token op_token) {
// op ty %op to ty2
- auto opty = parse_type();
- auto &val = parse_operand(opty.get());
- unique_ptr<Type> ty2 = parse_type(/*optional=*/!tokenizer.consumeIf(TO));
+ auto &opty = parse_type();
+ auto &val = parse_operand(opty);
+ auto &ty2 = parse_type(/*optional=*/!tokenizer.consumeIf(TO));
ConversionOp::Op op;
switch (op_token) {
@@ -253,20 +265,20 @@ static unique_ptr<Instr> parse_conversionop(string_view name, token op_token) {
default:
UNREACHABLE();
}
- return make_unique<ConversionOp>(move(ty2), string(name), val, op);
+ return make_unique<ConversionOp>(ty2, string(name), val, op);
}
static unique_ptr<Instr> parse_select(string_view name) {
// select condty %cond, ty %a, ty %b
- auto condty = parse_type();
- auto &cond = parse_operand(condty.get());
+ auto &condty = parse_type();
+ auto &cond = parse_operand(condty);
parse_comma();
- auto aty = parse_type();
- auto &a = parse_operand(aty.get());
+ auto &aty = parse_type();
+ auto &a = parse_operand(aty);
parse_comma();
- auto bty = parse_type();
- auto &b = parse_operand(bty.get());
- return make_unique<Select>(move(aty), string(name), cond, a, b);
+ auto &bty = parse_type();
+ auto &b = parse_operand(bty);
+ return make_unique<Select>(aty, string(name), cond, a, b);
}
static ICmp::Cond parse_icmp_cond() {
@@ -290,25 +302,25 @@ static ICmp::Cond parse_icmp_cond() {
static unique_ptr<Instr> parse_icmp(string_view name) {
// icmp cond ty %a, &b
auto cond = parse_icmp_cond();
- auto ty = parse_type();
- auto &a = parse_operand(ty.get());
+ auto &ty = parse_type();
+ auto &a = parse_operand(ty);
parse_comma();
- auto &b = parse_operand(ty.get());
- return make_unique<ICmp>(string(name), cond, a, b);
+ auto &b = parse_operand(ty);
+ return make_unique<ICmp>(*int_types[1].get(), 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);
+ auto &ty = parse_type();
+ auto &op = parse_operand(ty);
+ return make_unique<Freeze>(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);
+ auto &ty = parse_type();
+ auto &op = parse_operand(ty);
+ return make_unique<CopyOp>(ty, string(name), op);
}
static unique_ptr<Instr> parse_instr(string_view name) {
@@ -354,9 +366,9 @@ static unique_ptr<Instr> parse_instr(string_view name) {
}
static unique_ptr<Instr> parse_return() {
- auto type = parse_type();
- auto &val = parse_operand(type.get());
- return make_unique<Return>(move(type), val);
+ auto &type = parse_type();
+ auto &val = parse_operand(type);
+ return make_unique<Return>(type, val);
}
static void parse_fn(Function &f) {
@@ -397,6 +409,7 @@ vector<Transform> parse(string_view buf) {
vector<Transform> ret;
yylex_init(buf);
+ sym_num = 0;
while (!tokenizer.empty()) {
auto &t = ret.emplace_back();
@@ -411,4 +424,12 @@ vector<Transform> parse(string_view buf) {
return ret;
}
+void init_parser() {
+ int_types.emplace_back(nullptr);
+
+ for (unsigned i = 1; i <= 64; ++i) {
+ int_types.emplace_back(make_unique<IntType>("i" + to_string(i), i));
+ }
+}
+
}

MODIFY
tools/alive_parser.h
tools/alive_parser.h
namespace tools {
std::vector<tools::Transform> parse(std::string_view buf);
+void init_parser();
struct ParseException {
std::string str;

type refactoring: values don't own types anymore
this avoids copies and simplifies constraints for solver (due to sharing)