work on vector support incl unop vector ops
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -171,7 +171,7 @@ static expr fm_poison(const expr &a, const expr &b, const expr &val,
StateValue BinOp::toSMT(State &s) const {
bool use_default_op = true;
- std::function<StateValue(const expr&, const expr&, const expr&, const expr&,
+ function<StateValue(const expr&, const expr&, const expr&, const expr&,
const Type&)> fn, scalar_op;
switch (op) {
@@ -444,8 +444,8 @@ StateValue BinOp::toSMT(State &s) const {
};
}
- auto a = s[*lhs];
- auto b = s[*rhs];
+ auto &a = s[*lhs];
+ auto &b = s[*rhs];
if (getType().isVectorType()) {
vector<StateValue> vals;
@@ -531,42 +531,58 @@ void UnaryOp::print(ostream &os) const {
}
StateValue UnaryOp::toSMT(State &s) const {
- auto &[v, vp] = s[*val];
- expr newval;
+ function<expr(const expr&)> fn;
switch (op) {
case Copy:
- newval = v;
+ fn = [](auto v) { return v; };
break;
case BitReverse:
- newval = v.bitreverse();
+ fn = [](auto v) { return v.bitreverse(); };
break;
case BSwap:
- newval = v.bswap();;
+ fn = [](auto v) { return v.bswap(); };
break;
case Ctpop:
- newval = v.ctpop();
+ fn = [](auto v) { return v.ctpop(); };
break;
case FNeg:
- newval = v.fneg();
+ fn = [](auto v) { return v.fneg(); };
break;
}
- return { move(newval), expr(vp) };
+
+ auto &v = s[*val];
+
+ if (getType().isVectorType()) {
+ vector<StateValue> vals;
+ auto ty = getType().getAsAggregateType();
+ for (unsigned i = 0, e = ty->numElementsConst(); i != e; ++i) {
+ auto vi = ty->extract(v, i);
+ vals.emplace_back(fn(vi.value), move(vi.non_poison));
+ }
+ return ty->aggregateVals(vals);
+ }
+ return { fn(v.value), expr(v.non_poison) };
}
expr UnaryOp::getTypeConstraints(const Function &f) const {
- expr instrconstr = true;
+ expr instrconstr;
switch(op) {
+ case Copy:
+ instrconstr = true;
+ break;
case BSwap:
- instrconstr = val->getType().sizeVar().urem(expr::mkUInt(16, 8)) == 0;
- [[fallthrough]];
+ instrconstr = getType().enforceScalarOrVectorType([](auto &scalar) {
+ return scalar.enforceIntType() &&
+ scalar.sizeVar().urem(expr::mkUInt(16, 8)) == 0;
+ });
+ break;
case BitReverse:
case Ctpop:
- instrconstr &= getType().enforceIntOrVectorType();
- case Copy:
+ instrconstr = getType().enforceIntOrVectorType();
break;
case FNeg:
- instrconstr = getType().enforceFloatType();
+ instrconstr = getType().enforceFloatOrVectorType();
break;
}
@@ -625,7 +641,7 @@ StateValue TernaryOp::toSMT(State &s) const {
expr TernaryOp::getTypeConstraints(const Function &f) const {
return Value::getTypeConstraints() &&
- getType().enforceIntOrVectorType() &&
+ getType().enforceIntType() && // FIXME: vectors
getType() == a->getType() &&
getType() == b->getType() &&
getType() == c->getType();
@@ -713,33 +729,34 @@ StateValue ConversionOp::toSMT(State &s) const {
expr ConversionOp::getTypeConstraints(const Function &f) const {
expr c;
+ // TODO: add vector support
switch (op) {
case SExt:
case ZExt:
- c = getType().enforceIntOrVectorType() &&
+ c = getType().enforceIntType() &&
getType().sameType(val->getType()) &&
val->getType().sizeVar().ult(getType().sizeVar());
break;
case Trunc:
- c = getType().enforceIntOrVectorType() &&
+ c = getType().enforceIntType() &&
getType().sameType(val->getType()) &&
getType().sizeVar().ult(val->getType().sizeVar());
break;
case BitCast:
// FIXME: input can only be ptr if result is a ptr as well
- c = getType().enforceIntOrPtrOrVectorType() &&
+ c = getType().enforceIntType() &&
getType().sizeVar() == val->getType().sizeVar();
break;
case SIntToFP:
case UIntToFP:
// FIXME: output is vector iff input is vector
- c = getType().enforceFloatOrVectorType() &&
- val->getType().enforceIntOrVectorType();
+ c = getType().enforceFloatType() &&
+ val->getType().enforceIntType();
break;
case FPToSInt:
case FPToUInt:
- c = getType().enforceIntOrVectorType() &&
- val->getType().enforceFloatOrVectorType();
+ c = getType().enforceIntType() &&
+ val->getType().enforceFloatType();
break;
case Ptr2Int:
c = getType().enforceIntType() &&
@@ -782,9 +799,10 @@ StateValue Select::toSMT(State &s) const {
}
expr Select::getTypeConstraints(const Function &f) const {
+ // TODO: vector support
return cond->getType().enforceIntType(1) &&
Value::getTypeConstraints() &&
- getType().enforceIntOrPtrOrVectorType() &&
+ getType().enforceIntOrPtrType() &&
getType() == a->getType() &&
getType() == b->getType();
}
@@ -1076,9 +1094,10 @@ StateValue ICmp::toSMT(State &s) const {
}
expr ICmp::getTypeConstraints(const Function &f) const {
+ // TODO: add vector support
return Value::getTypeConstraints() &&
getType().enforceIntType(1) &&
- a->getType().enforceIntOrPtrOrVectorType() &&
+ a->getType().enforceIntOrPtrType() &&
a->getType() == b->getType();
}
@@ -1369,7 +1388,7 @@ StateValue Switch::toSMT(State &s) const {
expr Switch::getTypeConstraints(const Function &f) const {
expr typ = value->getType().enforceIntType();
for (auto &p : targets) {
- typ &= p.first->getType().enforceIntType();
+ typ &= p.first->getType() == value->getType();
}
return typ;
}
@@ -1600,7 +1619,8 @@ StateValue GEP::toSMT(State &s) const {
}
expr GEP::getTypeConstraints(const Function &f) const {
- auto c = getType() == ptr->getType() &&
+ auto c = Value::getTypeConstraints() &&
+ getType() == ptr->getType() &&
getType().enforcePtrType();
for (auto &[sz, idx] : idxs) {
(void)sz;

MODIFY
ir/type.cpp
ir/type.cpp
@@ -34,7 +34,7 @@ expr Type::sizeVar() const {
}
expr Type::is(unsigned t) const {
- return typeVar() == expr::mkUInt(t, var_type_bits);
+ return typeVar() == t;
}
expr Type::isInt() const { return is(SymbolicType::Int); }
@@ -346,10 +346,18 @@ expr FloatType::toBV(expr e) const {
return e.float2BV();
}
+StateValue FloatType::toBV(StateValue v) const {
+ return Type::toBV(move(v));
+}
+
expr FloatType::fromBV(expr e) const {
return e.BV2float(getDummyValue(true).value);
}
+StateValue FloatType::fromBV(StateValue v) const {
+ return Type::fromBV(move(v));
+}
+
expr FloatType::sizeVar() const {
return defined ? expr::mkUInt(getFpType(), var_bw_bits) : Type::sizeVar();
}
@@ -523,7 +531,7 @@ AggregateType::AggregateType(string &&name, bool symbolic)
// FIXME: limitation below is for vectors; what about structs and arrays?
for (unsigned i = 0; i < num; ++i) {
- sym[i] = make_unique<SymbolicType>("v_" + name,
+ sym[i] = make_unique<SymbolicType>("v#" + to_string(i) + '_' + name,
(1 << SymbolicType::Int) |
(1 << SymbolicType::Float) |
(1 << SymbolicType::Ptr));
@@ -650,10 +658,18 @@ expr AggregateType::enforceAggregateType(vector<Type*> *element_types) const {
return r;
}
+expr AggregateType::toBV(expr e) const {
+ return Type::toBV(move(e));
+}
+
StateValue AggregateType::toBV(StateValue v) const {
return v;
}
+expr AggregateType::fromBV(expr e) const {
+ return Type::fromBV(move(e));
+}
+
StateValue AggregateType::fromBV(StateValue v) const {
return v;
}
@@ -663,8 +679,8 @@ AggregateType::refines(const StateValue &src, const StateValue &tgt) const {
set<expr> poison, value;
for (unsigned i = 0; i < elements; ++i) {
auto [p, v] = children[i]->refines(extract(src, i), extract(tgt, i));
- poison.insert(p);
- value.insert(v);
+ poison.insert(move(p));
+ value.insert(move(v));
}
return { expr::mk_and(poison), expr::mk_and(value) };
}
@@ -677,7 +693,7 @@ AggregateType::mkInput(State &s, const char *name) const {
for (unsigned i = 0; i < elements; ++i) {
string c_name = string(name) + "#" + to_string(i);
auto [v, vs] = children[i]->mkInput(s, c_name.c_str());
- v = children[i]->toBV(v);
+ v = children[i]->toBV(move(v));
val = i == 0 ? move(v) : val.concat(v);
vars.insert(vars.end(), vs.begin(), vs.end());
}
@@ -801,32 +817,24 @@ SymbolicType::SymbolicType(string &&name, unsigned type_mask)
s.emplace(string(name));
}
+#define DISPATCH(call, undef) \
+ switch (typ) { \
+ case Int: return i->call; \
+ case Float: return f->call; \
+ case Ptr: return p->call; \
+ case Array: return a->call; \
+ case Vector: return v->call; \
+ case Struct: return s->call; \
+ case Undefined: undef; \
+ } \
+ UNREACHABLE()
+
unsigned SymbolicType::bits() const {
- switch (typ) {
- case Int: return i->bits();
- case Float: return f->bits();
- case Ptr: return p->bits();
- case Array: return a->bits();
- case Vector: return v->bits();
- case Struct: return s->bits();
- case Undefined:
- assert(0 && "undefined at SymbolicType::bits()");
- }
- UNREACHABLE();
+ DISPATCH(bits(), UNREACHABLE());
}
StateValue SymbolicType::getDummyValue(bool non_poison) const {
- switch (typ) {
- case Int: return i->getDummyValue(non_poison);
- case Float: return f->getDummyValue(non_poison);
- case Ptr: return p->getDummyValue(non_poison);
- case Array: return a->getDummyValue(non_poison);
- case Vector: return v->getDummyValue(non_poison);
- case Struct: return s->getDummyValue(non_poison);
- case Undefined:
- break;
- }
- UNREACHABLE();
+ DISPATCH(getDummyValue(non_poison), UNREACHABLE());
}
expr SymbolicType::getTypeConstraints() const {
@@ -835,8 +843,7 @@ expr SymbolicType::getTypeConstraints() const {
if (f) c |= isFloat() && f->getTypeConstraints();
if (p) c |= isPtr() && p->getTypeConstraints();
if (a) c |= isArray() && a->getTypeConstraints();
- // FIXME: disabled temporarily until BinOps/etc support vectors
- //if (v) c |= isVector() && v->getTypeConstraints();
+ if (v) c |= isVector() && v->getTypeConstraints();
if (s) c |= isStruct() && s->getTypeConstraints();
return c;
}
@@ -865,7 +872,7 @@ expr SymbolicType::operator==(const Type &b) const {
if (p && rhs->p) c |= isPtr() && *p == *rhs->p;
if (a && rhs->a) c |= isArray() && *a == *rhs->a;
if (v && rhs->v) c |= isVector() && *v == *rhs->v;
- // FIXME: add support for this: c |= isStruct() && s == rhs->s;
+ if (s && rhs->s) c |= isStruct() && *s == *rhs->s;
return move(c) && typeVar() == rhs->typeVar();
}
assert(0 && "unhandled case in SymbolicType::operator==");
@@ -896,7 +903,7 @@ expr SymbolicType::sameType(const Type &b) const {
if (p && rhs->p) c |= isPtr() && p->sameType(*rhs->p);
if (a && rhs->a) c |= isArray() && a->sameType(*rhs->a);
if (v && rhs->v) c |= isVector() && v->sameType(*rhs->v);
- // FIXME: add support for this: c |= isStruct() && s.sameType(rhs->s);
+ if (s && rhs->s) c |= isStruct() && s->sameType(*rhs->s);
return move(c) && typeVar() == rhs->typeVar();
}
assert(0 && "unhandled case in SymbolicType::sameType");
@@ -976,64 +983,55 @@ const FloatType* SymbolicType::getAsFloatType() const {
}
const AggregateType* SymbolicType::getAsAggregateType() const {
- // TODO: needs a proxy or something
- return &*s;
+ switch (typ) {
+ case Int:
+ case Float:
+ case Ptr:
+ return nullptr;
+ case Array: return &*a;
+ case Vector: return &*v;
+ case Struct: return &*s;
+ case Undefined: return &*s; // FIXME: needs a proxy or something
+ }
+ UNREACHABLE();
}
const StructType* SymbolicType::getAsStructType() const {
return &*s;
}
+expr SymbolicType::toBV(expr e) const {
+ DISPATCH(toBV(move(e)), UNREACHABLE());
+}
+
+StateValue SymbolicType::toBV(StateValue val) const {
+ DISPATCH(toBV(move(val)), UNREACHABLE());
+}
+
+expr SymbolicType::fromBV(expr e) const {
+ DISPATCH(fromBV(move(e)), UNREACHABLE());
+}
+
+StateValue SymbolicType::fromBV(StateValue val) const {
+ DISPATCH(fromBV(move(val)), UNREACHABLE());
+}
+
pair<expr, expr>
SymbolicType::refines(const StateValue &src, const StateValue &tgt) const {
- switch (typ) {
- case Int: return i->refines(src, tgt);
- case Float: return f->refines(src, tgt);
- case Ptr: return p->refines(src, tgt);
- case Array: return a->refines(src, tgt);
- case Vector: return v->refines(src, tgt);
- case Struct: return s->refines(src, tgt);
- case Undefined: UNREACHABLE();
- }
- UNREACHABLE();
+ DISPATCH(refines(src, tgt), UNREACHABLE());
}
pair<expr, vector<expr>>
SymbolicType::mkInput(State &st, const char *name) const {
- switch (typ) {
- case Int: return i->mkInput(st, name);
- case Float: return f->mkInput(st, name);
- case Ptr: return p->mkInput(st, name);
- case Array: return a->mkInput(st, name);
- case Vector: return v->mkInput(st, name);
- case Struct: return s->mkInput(st, name);
- case Undefined: UNREACHABLE();
- }
- UNREACHABLE();
+ DISPATCH(mkInput(st, name), UNREACHABLE());
}
void SymbolicType::printVal(ostream &os, State &st, const expr &e) const {
- switch (typ) {
- case Int: i->printVal(os, st, e); break;
- case Float: f->printVal(os, st, e); break;
- case Ptr: p->printVal(os, st, e); break;
- case Array: a->printVal(os, st, e); break;
- case Vector: v->printVal(os, st, e); break;
- case Struct: s->printVal(os, st, e); break;
- case Undefined: UNREACHABLE();
- }
+ DISPATCH(printVal(os, st, e), UNREACHABLE());
}
void SymbolicType::print(ostream &os) const {
- switch (typ) {
- case Int: i->print(os); break;
- case Float: f->print(os); break;
- case Ptr: p->print(os); break;
- case Array: a->print(os); break;
- case Vector: v->print(os); break;
- case Struct: s->print(os); break;
- case Undefined: break;
- }
+ DISPATCH(print(os), return);
}
}

MODIFY
ir/type.h
ir/type.h
@@ -173,7 +173,9 @@ public:
smt::expr enforceFloatType() const override;
const FloatType* getAsFloatType() const override;
smt::expr toBV(smt::expr e) const override;
+ IR::StateValue toBV(IR::StateValue v) const override;
smt::expr fromBV(smt::expr e) const override;
+ IR::StateValue fromBV(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
std::pair<smt::expr, std::vector<smt::expr>>
@@ -239,7 +241,9 @@ public:
void fixup(const smt::Model &m) override;
smt::expr enforceAggregateType(
std::vector<Type *> *element_types) const override;
+ smt::expr toBV(smt::expr e) const override;
IR::StateValue toBV(IR::StateValue v) const override;
+ smt::expr fromBV(smt::expr e) const override;
IR::StateValue fromBV(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
refines(const IR::StateValue &src,const IR::StateValue &tgt) const override;
@@ -325,6 +329,10 @@ public:
const FloatType* getAsFloatType() const override;
const AggregateType* getAsAggregateType() const override;
const StructType* getAsStructType() const override;
+ smt::expr toBV(smt::expr e) const override;
+ IR::StateValue toBV(IR::StateValue v) const override;
+ smt::expr fromBV(smt::expr e) const override;
+ IR::StateValue fromBV(IR::StateValue v) const override;
std::pair<smt::expr, smt::expr>
refines(const IR::StateValue &a, const IR::StateValue &b) const override;
std::pair<smt::expr, std::vector<smt::expr>>

MODIFY
ir/value.cpp
ir/value.cpp
@@ -138,8 +138,13 @@ StateValue Input::toSMT(State &s) const {
val = expr::mkIf(type.extract(0, 0) == 0, val, val.subst(repls));
}
+ expr poison = getType().getDummyValue(false).non_poison;
+ expr non_poison = getType().getDummyValue(true).non_poison;
+
return { move(val),
- config::disable_poison_input ? true : type.extract(1, 1) == 0 };
+ config::disable_poison_input
+ ? move(non_poison)
+ : expr::mkIf(type.extract(1, 1) == 0, non_poison, poison) };
}
expr Input::getTyVar() const {

work on vector support incl unop vector ops