further work on StructType
still missing support for symbolic instantiations
MODIFY
ir/constant.cpp
ir/constant.cpp
@@ -45,15 +45,6 @@ expr IntConst::getTypeConstraints() const {
getType().sizeVar().uge(min_bits);
}
-bool IntConst::isIntConst(int64_t &n) const {
- if (auto v = get_if<int64_t>(&val))
- n = *v;
- else if (auto v = get_if<string>(&val))
- n = std::stoll(*v);
-
- return true;
-}
-
pair<expr, expr> ConstantInput::toSMT_cnst() const {
return { expr::mkVar(getName().c_str(), bits()), true };
}

MODIFY
ir/constant.h
ir/constant.h
#include <string>
#include <string_view>
#include <utility>
+#include <variant>
#include <vector>
namespace IR {
@@ -29,7 +30,7 @@ public:
IntConst(Type &type, std::string &&val);
virtual std::pair<smt::expr, smt::expr> toSMT_cnst() const override;
smt::expr getTypeConstraints() const override;
- bool isIntConst(int64_t &n) const override;
+ auto getInt() const { return std::get_if<int64_t>(&val); }
};

MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -39,6 +39,10 @@ BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
case LShr:
assert((flags & Exact) == flags);
break;
+ case ExtractValue:
+ assert(dynamic_cast<IntConst*>(&rhs));
+ assert(dynamic_cast<IntConst&>(rhs).getInt());
+ [[fallthrough]];
case SRem:
case URem:
case SAdd_Sat:
@@ -51,7 +55,6 @@ BinOp::BinOp(Type &type, string &&name, Value &lhs, Value &rhs, Op op,
case Cttz:
case Ctlz:
case SAdd_Overflow:
- case ExtractValue:
assert(flags == 0);
break;
}
@@ -234,17 +237,14 @@ StateValue BinOp::toSMT(State &s) const {
case SAdd_Overflow:
val = a + b;
- val = val.concat(expr::mkIf(a.add_no_soverflow(b),
- expr::mkUInt(0, 1),
- expr::mkUInt(1, 1)));
+ val = val.concat(expr::toBVBool(!a.add_no_soverflow(b)));
break;
case ExtractValue:
{
- auto &structType = static_cast<StructureType&>(lhs.getType());
- uint64_t index;
- ENSURE(b.isUInt(index));
- val = structType.extract(a, index);
+ auto structType = lhs.getType().getAsStructType();
+ auto idx = *static_cast<IntConst&>(rhs).getInt();
+ val = structType->extract(a, idx);
break;
}
}
@@ -257,40 +257,42 @@ expr BinOp::getTypeConstraints(const Function &f) const {
switch (op) {
case ExtractValue:
{
- int64_t n;
- instrconstr = lhs.getType().enforceStructureType() &&
- rhs.isIntConst(n);
- auto structType = dynamic_cast<StructureType*>(&lhs.getType());
- if (structType &&
- n >= 0 && n < static_cast<int64_t>(structType->numElements())) {
- instrconstr = instrconstr &&
- structType->getChildType(n) == getType();
- } else {
- instrconstr = false;
+ instrconstr = lhs.getType().enforceAggregateType() &&
+ rhs.getType().enforceIntType();
+
+ // TODO: add support for arrays
+ if (auto ty = lhs.getType().getAsStructType()) {
+ auto idx = *static_cast<IntConst&>(rhs).getInt();
+ instrconstr &= ty->numElements().ugt(idx) &&
+ ty->getChild(idx) == getType();
}
break;
}
case SAdd_Overflow:
- instrconstr = lhs.getType() == rhs.getType() &&
+ instrconstr = getType().enforceStructType() &&
lhs.getType().enforceIntType() &&
- getType().enforceStructureType();
+ lhs.getType() == rhs.getType();
+
+ if (auto ty = getType().getAsStructType()) {
+ instrconstr &= ty->numElements() == 2 &&
+ ty->getChild(0) == lhs.getType() &&
+ ty->getChild(1).enforceIntType(1);
+ }
break;
case Cttz:
case Ctlz:
- instrconstr = rhs.getType().enforceIntType() &&
- rhs.getType().sizeVar() == 1u &&
- getType().enforceIntOrPtrOrVectorType() &&
- getType() == lhs.getType();
+ instrconstr = getType().enforceIntOrPtrOrVectorType() &&
+ getType() == lhs.getType() &&
+ rhs.getType().enforceIntType() &&
+ rhs.getType().sizeVar() == 1u;
break;
default:
- instrconstr = getType() == rhs.getType() &&
- getType().enforceIntOrPtrOrVectorType() &&
- getType() == lhs.getType();
+ instrconstr = getType().enforceIntOrPtrOrVectorType() &&
+ getType() == lhs.getType() &&
+ getType() == rhs.getType();
break;
}
-
- return Value::getTypeConstraints() &&
- move(instrconstr);
+ return Value::getTypeConstraints() && move(instrconstr);
}
unique_ptr<Instr> BinOp::dup(const string &suffix) const {

MODIFY
ir/type.cpp
ir/type.cpp
@@ -40,7 +40,7 @@ expr Type::isFloat() const { return is(SymbolicType::Float); }
expr Type::isPtr() const { return is(SymbolicType::Ptr); }
expr Type::isArray() const { return is(SymbolicType::Array); }
expr Type::isVector() const { return is(SymbolicType::Vector); }
-expr Type::isStructure() const { return is(SymbolicType::Structure); }
+expr Type::isStruct() const { return is(SymbolicType::Struct); }
unsigned Type::bits() const {
UNREACHABLE();
@@ -64,6 +64,7 @@ expr Type::operator==(const Type &b) const {
CMP(PtrType)
CMP(ArrayType)
CMP(VectorType)
+ CMP(StructType)
#undef CMP
@@ -74,7 +75,7 @@ expr Type::operator==(const Type &b) const {
return false;
}
-expr Type::enforceIntType() const {
+expr Type::enforceIntType(unsigned bits) const {
return false;
}
@@ -86,10 +87,18 @@ expr Type::enforceIntOrPtrOrVectorType() const {
return false;
}
-expr Type::enforceStructureType() const {
+expr Type::enforceStructType() const {
return false;
}
+expr Type::enforceAggregateType() const {
+ return false;
+}
+
+const StructType* Type::getAsStructType() const {
+ UNREACHABLE();
+}
+
ostream& operator<<(ostream &os, const Type &t) {
t.print(os);
return os;
@@ -143,8 +152,8 @@ void IntType::fixup(const Model &m) {
bitwidth = m.getUInt(sizeVar());
}
-expr IntType::enforceIntType() const {
- return true;
+expr IntType::enforceIntType(unsigned bits) const {
+ return bits ? sizeVar() == bits : true;
}
expr IntType::enforceIntOrVectorType() const {
@@ -221,6 +230,10 @@ void ArrayType::fixup(const Model &m) {
// TODO
}
+expr ArrayType::enforceAggregateType() const {
+ return true;
+}
+
void ArrayType::print(ostream &os) const {
os << "TODO";
}
@@ -252,68 +265,77 @@ void VectorType::print(ostream &os) const {
os << "TODO";
}
-expr StructureType::getTypeConstraints() const {
+expr StructType::getTypeConstraints() const {
expr res(true);
- for (auto type : children) {
- res &= type->enforceIntType();
+ for (auto c : children) {
+ res &= c->getTypeConstraints();
}
-
return res;
}
-expr StructureType::operator==(const StructureType &rhs) const {
+expr StructType::operator==(const StructType &rhs) const {
if (children.size() != rhs.children.size())
return false;
- expr res(false);
- for (unsigned i = 0; i < children.size(); i++) {
- res = res || *children[i] == *rhs.children[i];
+ expr res(true);
+ for (unsigned i = 0, e = children.size(); i != e; ++i) {
+ res &= *children[i] == *rhs.children[i];
}
-
return res;
}
-expr StructureType::enforceStructureType() const {
- return !children.empty();
+expr StructType::enforceStructType() const {
+ return true;
+}
+
+expr StructType::enforceAggregateType() const {
+ return true;
}
-void StructureType::fixup(const Model &m) {
- // TODO
+const StructType* StructType::getAsStructType() const {
+ return this;
}
-expr StructureType::enforceIntOrPtrOrVectorType() const {
- return false;
+void StructType::fixup(const Model &m) {
+ for (auto c : children) {
+ c->fixup(m);
+ }
}
-unsigned StructureType::bits() const {
+unsigned StructType::bits() const {
unsigned res = 0;
- for (unsigned i = 0; i < children.size(); i++) {
- res += children[i]->bits();
+ for (auto c : children) {
+ res += c->bits();
}
-
return res;
}
-void StructureType::print(ostream &os) const {
- assert(children.size() > 0);
+void StructType::print(ostream &os) const {
os << '{';
- children[0]->print(os);
- for (unsigned i = 1; i < children.size(); i++) {
+ bool first = true;
+ for (auto c : children) {
+ if (!first)
os << ", ";
- children[i]->print(os);
+ first = false;
+ c->print(os);
}
os << '}';
}
-Type& StructureType::getChildType(unsigned index) const {
- assert(index < children.size());
+smt::expr StructType::numElements() const {
+ // TODO: fix symbolic struct type
+ return expr::mkUInt(children.size(), 8);
+}
+
+Type& StructType::getChild(unsigned index) const {
+ // TODO: fix symbolic struct type
return *children[index];
}
-expr StructureType::extract(const expr &struct_val, unsigned index) const {
+expr StructType::extract(const expr &struct_val, unsigned index) const {
unsigned total_till_now = 0;
assert(index < children.size());
- for (unsigned i = 0; i <= index; i++) {
+ for (unsigned i = 0; i <= index; ++i) {
total_till_now += children[i]->bits();
}
unsigned low = struct_val.bits() - total_till_now;
@@ -323,7 +345,7 @@ expr StructureType::extract(const expr &struct_val, unsigned index) const {
SymbolicType::SymbolicType(string &&name, bool named)
: Type(string(name)), i(string(name)), f(string(name)), p(string(name)),
- a(string(name)), v(string(name)), st(string(name)), named(named) {}
+ a(string(name)), v(string(name)), s(string(name)), named(named) {}
unsigned SymbolicType::bits() const {
switch (typ) {
@@ -332,7 +354,7 @@ unsigned SymbolicType::bits() const {
case Ptr: return p.bits();
case Array: return a.bits();
case Vector: return v.bits();
- case Structure: return st.bits();
+ case Struct: return s.bits();
case Undefined:
assert(0 && "undefined at SymbolicType::bits()");
}
@@ -346,6 +368,7 @@ expr SymbolicType::getTypeConstraints() const {
c |= isPtr() && p.getTypeConstraints();
c |= isArray() && a.getTypeConstraints();
c |= isVector() && v.getTypeConstraints();
+ c |= isStruct() && s.getTypeConstraints();
return c;
}
@@ -363,8 +386,8 @@ expr SymbolicType::operator==(const Type &b) const {
return isArray() && a == *rhs;
if (auto rhs = dynamic_cast<const VectorType*>(&b))
return isVector() && v == *rhs;
- if (auto rhs = dynamic_cast<const StructureType*>(&b))
- return isStructure() && st == *rhs;
+ if (auto rhs = dynamic_cast<const StructType*>(&b))
+ return isStruct() && s == *rhs;
if (auto rhs = dynamic_cast<const SymbolicType*>(&b)) {
expr c(false);
@@ -373,7 +396,7 @@ expr SymbolicType::operator==(const Type &b) const {
c |= isPtr() && p == rhs->p;
c |= isArray() && a == rhs->a;
c |= isVector() && v == rhs->v;
- c |= isStructure() && st == rhs->st;
+ // FIXME: add support for this: c |= isStruct() && s == rhs->s;
return move(c) && typeVar() == rhs->typeVar();
}
assert(0 && "unhandled case in SymbolicType::operator==");
@@ -382,7 +405,7 @@ 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(smt_typ >= Int && smt_typ <= Struct);
typ = TypeNum(smt_typ);
switch (typ) {
@@ -391,14 +414,14 @@ void SymbolicType::fixup(const Model &m) {
case Ptr: p.fixup(m); break;
case Array: a.fixup(m); break;
case Vector: v.fixup(m); break;
- case Structure: st.fixup(m); break;
+ case Struct: s.fixup(m); break;
case Undefined:
UNREACHABLE();
}
}
-expr SymbolicType::enforceIntType() const {
- return isInt();
+expr SymbolicType::enforceIntType(unsigned bits) const {
+ return isInt() && i.enforceIntType(bits);
}
expr SymbolicType::enforceIntOrVectorType() const {
@@ -409,8 +432,16 @@ expr SymbolicType::enforceIntOrPtrOrVectorType() const {
return isInt() || isPtr() || isVector();
}
-expr SymbolicType::enforceStructureType() const {
- return isStructure();
+expr SymbolicType::enforceStructType() const {
+ return isStruct();
+}
+
+expr SymbolicType::enforceAggregateType() const {
+ return isArray() || isStruct();
+}
+
+const StructType* SymbolicType::getAsStructType() const {
+ return &s;
}
void SymbolicType::print(ostream &os) const {
@@ -425,7 +456,7 @@ void SymbolicType::print(ostream &os) const {
case Ptr: p.print(os); break;
case Array: a.print(os); break;
case Vector: v.print(os); break;
- case Structure: st.print(os); break;
+ case Struct: s.print(os); break;
case Undefined: break;
}
}

MODIFY
ir/type.h
ir/type.h
@@ -13,6 +13,7 @@ namespace smt { class Model; }
namespace IR {
+class StructType;
class VoidType;
class Type {
@@ -26,7 +27,7 @@ protected:
smt::expr isPtr() const;
smt::expr isArray() const;
smt::expr isVector() const;
- smt::expr isStructure() const;
+ smt::expr isStruct() const;
public:
Type(std::string &&name) : name(std::move(name)) {}
@@ -37,10 +38,13 @@ public:
smt::expr operator==(const Type &rhs) const;
virtual void fixup(const smt::Model &m) = 0;
- virtual smt::expr enforceIntType() const;
+ virtual smt::expr enforceIntType(unsigned bits = 0) const;
virtual smt::expr enforceIntOrVectorType() const;
virtual smt::expr enforceIntOrPtrOrVectorType() const;
- virtual smt::expr enforceStructureType() const;
+ virtual smt::expr enforceStructType() const;
+ virtual smt::expr enforceAggregateType() const;
+
+ virtual const StructType* getAsStructType() const;
virtual void print(std::ostream &os) const = 0;
friend std::ostream& operator<<(std::ostream &os, const Type &t);
@@ -75,7 +79,7 @@ public:
smt::expr sizeVar() const override;
smt::expr operator==(const IntType &rhs) const;
void fixup(const smt::Model &m) override;
- smt::expr enforceIntType() const override;
+ smt::expr enforceIntType(unsigned bits = 0) const override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
void print(std::ostream &os) const override;
@@ -110,6 +114,7 @@ public:
smt::expr getTypeConstraints() const override;
smt::expr operator==(const ArrayType &rhs) const;
void fixup(const smt::Model &m) override;
+ smt::expr enforceAggregateType() const override;
void print(std::ostream &os) const override;
};
@@ -126,23 +131,25 @@ public:
};
-class StructureType final : public Type {
+class StructType final : public Type {
const std::vector<Type*> children;
public:
- StructureType(std::string &&name) : Type(std::move(name)) {}
- StructureType(std::string &&name, std::vector<Type*> &&children)
- : Type(std::move(name)), children(children) { }
+ StructType(std::string &&name) : Type(std::move(name)) {}
+ StructType(std::string &&name, std::vector<Type*> &&children)
+ : Type(std::move(name)), children(std::move(children)) {}
unsigned bits() const override;
- smt::expr enforceStructureType() const override;
smt::expr getTypeConstraints() const override;
- smt::expr operator==(const StructureType &rhs) const;
+ smt::expr operator==(const StructType &rhs) const;
void fixup(const smt::Model &m) override;
- smt::expr enforceIntOrPtrOrVectorType() const override;
+ smt::expr enforceStructType() const override;
+ smt::expr enforceAggregateType() const override;
+ const StructType* getAsStructType() const override;
void print(std::ostream &os) const override;
- auto numElements() const { return children.size(); }
- Type& getChildType(unsigned index) const;
+
+ smt::expr numElements() const;
+ Type& getChild(unsigned index) const;
// Extracts the type located at \p index from \p struct_val
smt::expr extract(const smt::expr &struct_val, unsigned index) const;
};
@@ -150,7 +157,7 @@ public:
class SymbolicType final : public Type {
public:
- enum TypeNum { Int, Float, Ptr, Array, Vector, Structure, Undefined };
+ enum TypeNum { Int, Float, Ptr, Array, Vector, Struct, Undefined };
private:
TypeNum typ = Undefined;
@@ -159,7 +166,7 @@ private:
PtrType p;
ArrayType a;
VectorType v;
- StructureType st;
+ StructType s;
bool named;
public:
@@ -168,10 +175,12 @@ public:
smt::expr getTypeConstraints() const override;
smt::expr operator==(const Type &rhs) const;
void fixup(const smt::Model &m) override;
- smt::expr enforceIntType() const override;
+ smt::expr enforceIntType(unsigned bits = 0) const override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
- smt::expr enforceStructureType() const override;
+ smt::expr enforceStructType() const override;
+ smt::expr enforceAggregateType() const override;
+ const StructType* getAsStructType() const override;
void print(std::ostream &os) const override;
};

MODIFY
ir/value.h
ir/value.h
@@ -42,8 +42,6 @@ public:
static void reset_gbl_id();
- virtual bool isIntConst(int64_t &n) const { return false; }
-
friend std::ostream& operator<<(std::ostream &os, const Value &val);
virtual ~Value() {}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -178,6 +178,11 @@ expr expr::mkBoolVar(const char *name) {
return ::mkVar(name, Z3_mk_bool_sort(ctx()));
}
+expr expr::toBVBool(const expr &e) {
+ auto sort = mkBVSort(1);
+ return mkIf(e, mkUInt(1, sort), mkUInt(0, sort));
+}
+
expr expr::IntSMin(unsigned bits) {
assert(bits > 0);
static_assert(sizeof(unsigned long long) == 8);

MODIFY
smt/expr.h
smt/expr.h
@@ -73,6 +73,7 @@ public:
static expr mkInt(const char *n, unsigned bits);
static expr mkVar(const char *name, unsigned bits);
static expr mkBoolVar(const char *name);
+ static expr toBVBool(const expr &e);
static expr IntSMin(unsigned bits);
static expr IntSMax(unsigned bits);

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -220,17 +220,17 @@ static void parse_comma() {
}
-static unordered_map<Type*, unique_ptr<StructureType>> overflow_aggregate_types;
+static unordered_map<Type*, unique_ptr<StructType>> overflow_aggregate_types;
static vector<unique_ptr<SymbolicType>> sym_types;
static unsigned sym_num;
static Type& get_overflow_type(Type &type) {
- auto t = make_unique<StructureType>("oaggty",
- std::initializer_list<Type*>(
- { &type,
- int_types[1].get()}));
- auto res = overflow_aggregate_types.emplace(&type, move(t));
- return *res.first->second.get();
+ auto p = overflow_aggregate_types.try_emplace(&type);
+ auto &st = p.first->second;
+ if (p.second)
+ st = make_unique<StructType>("structty",
+ initializer_list<Type*>({ &type, int_types[1].get() }));
+ return *st.get();
}
static Type& get_sym_type() {
@@ -242,9 +242,11 @@ static Type& get_sym_type() {
}
static Type& get_int_type(unsigned size) {
+ if (size >= int_types.size())
+ int_types.resize(size + 1);
+
if (!int_types[size])
- int_types[size] =
- make_unique<IntType>("i" + to_string(size), size);
+ int_types[size] = make_unique<IntType>("i" + to_string(size), size);
return *int_types[size].get();
}
@@ -254,10 +256,6 @@ static Type& parse_type(bool optional = true) {
case INT_TYPE:
if (yylval.num > 4 * 1024)
error("Int type too long: " + to_string(yylval.num));
-
- if (yylval.num >= int_types.size())
- int_types.resize(yylval.num + 1);
-
return get_int_type(yylval.num);
default:
@@ -415,11 +413,12 @@ static unique_ptr<Instr> parse_binop(string_view name, token op_token) {
auto &a = parse_operand(type);
parse_comma();
- // 2nd binop argument handling
- Type *type2 = &try_parse_type(type);
- if (op_token == EXTRACTVALUE)
- type2 = &get_int_type(64);
- auto &b = parse_operand(*type2);
+ // RHS handling
+ // for extractvalue it isn't important to try multiple types
+ // so we use a default of i8
+ Type &default_rhs_type = op_token == EXTRACTVALUE ? get_int_type(8) : type;
+ Type &type_rhs = try_parse_type(default_rhs_type);
+ auto &b = parse_operand(type_rhs);
Type *rettype = &type;
BinOp::Op op;

MODIFY
tools/tokens.h
tools/tokens.h
@@ -49,8 +49,8 @@ TOKEN(PRE)
TOKEN(REGISTER)
TOKEN(RETURN)
TOKEN(RPAREN)
-TOKEN(SADD_SAT)
TOKEN(SADD_OVERFLOW)
+TOKEN(SADD_SAT)
TOKEN(SDIV)
TOKEN(SELECT)
TOKEN(SEXT)

further work on StructType
still missing support for symbolic instantiations