misc type fixes & add vector support to select
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -749,8 +749,10 @@ expr ConversionOp::getTypeConstraints(const Function &f) const {
getType().sizeVar().ult(val->getType().sizeVar());
break;
case BitCast:
- // FIXME: input can only be ptr if result is a ptr as well
- c = (getType().enforceIntOrPtrType() || getType().enforceFloatType()) &&
+ c = ((getType().enforcePtrType() && val->getType().enforcePtrType()) ||
+ ((getType().enforceIntType() || getType().enforceFloatType()) &&
+ (val->getType().enforceIntType() ||
+ val->getType().enforceFloatType()))) &&
getType().sizeVar() == val->getType().sizeVar();
break;
case SIntToFP:
@@ -796,19 +798,41 @@ void Select::print(ostream &os) const {
}
StateValue Select::toSMT(State &s) const {
- auto &[c, cp] = s[*cond];
- auto &[av, ap] = s[*a];
- auto &[bv, bp] = s[*b];
- auto cond = c == 1u;
- return { expr::mkIf(cond, av, bv),
- cp && expr::mkIf(cond, ap, bp) };
+ auto &cv = s[*cond];
+ auto &av = s[*a];
+ auto &bv = s[*b];
+
+ auto scalar = [](const auto &a, const auto &b, const auto &c) -> StateValue {
+ auto cond = c.value == 1;
+ return { expr::mkIf(cond, a.value, b.value),
+ c.non_poison && expr::mkIf(cond, a.non_poison, b.non_poison) };
+ };
+
+ if (auto agg = getType().getAsAggregateType()) {
+ vector<StateValue> vals;
+ auto cond_agg = cond->getType().getAsAggregateType();
+
+ for (unsigned i = 0, e = agg->numElementsConst(); i != e; ++i) {
+ vals.emplace_back(scalar(agg->extract(av, i), agg->extract(bv, i),
+ cond_agg ? cond_agg->extract(cv, i) : cv));
+ }
+ return agg->aggregateVals(vals);
+ }
+ return scalar(av, bv, cv);
}
expr Select::getTypeConstraints(const Function &f) const {
- // TODO: vector support
- return cond->getType().enforceIntType(1) &&
+ expr elems_sz = false;
+ if (auto cond_agg = cond->getType().getAsAggregateType())
+ if (auto agg = getType().getAsAggregateType())
+ elems_sz = cond_agg->numElements() == agg->numElements();
+
+ return (cond->getType().enforceIntType(1) ||
+ (cond->getType().enforceIntOrVectorType(1) &&
+ getType().enforceVectorType() &&
+ elems_sz)) &&
Value::getTypeConstraints() &&
- getType().enforceIntOrPtrType() &&
+ getType().enforceIntOrFloatOrPtrOrVectorType() &&
getType() == a->getType() &&
getType() == b->getType();
}
@@ -984,7 +1008,13 @@ StateValue FnCall::toSMT(State &s) const {
expr FnCall::getTypeConstraints(const Function &f) const {
// TODO : also need to name each arg type smt var uniquely
- return Value::getTypeConstraints();
+ auto r = Value::getTypeConstraints();
+ // TODO: add aggregate support
+ for (auto arg : args) {
+ r &= !arg->getType().enforceStructType();
+ r &= !arg->getType().enforceVectorType();
+ }
+ return r;
}
unique_ptr<Instr> FnCall::dup(const string &suffix) const {

MODIFY
ir/memory.cpp
ir/memory.cpp
@@ -144,8 +144,8 @@ StateValue bytesToValue(const vector<Byte> &bytes, const Type &toType) {
IntType i8Ty("", 8);
for (auto &b: bytes) {
- expr ptr_np = i8Ty.toBV({ b.nonptr_nonpoison(), !b.is_ptr() }).non_poison;
- StateValue v(b.nonptr_value(), ptr_np | b.nonptr_nonpoison());
+ StateValue v(b.nonptr_value(),
+ i8Ty.combine_poison(!b.is_ptr(), b.nonptr_nonpoison()));
val = first ? move(v) : v.concat(val);
first = false;
}

MODIFY
ir/type.cpp
ir/type.cpp
@@ -150,6 +150,10 @@ expr Type::enforceFloatType() const {
return false;
}
+expr Type::enforceVectorType() const {
+ return enforceVectorType([](auto &ty) { return true; });
+}
+
expr
Type::enforceVectorType(const function<expr(const Type&)> &enforceElem) const {
return false;
@@ -165,6 +169,11 @@ expr Type::enforceIntOrVectorType(unsigned bits) const {
[&](auto &ty) { return ty.enforceIntType(bits); });
}
+expr Type::enforceIntOrFloatOrPtrOrVectorType() const {
+ return enforceScalarOrVectorType(
+ [&](auto &ty) { return ty.enforceIntOrPtrType() || ty.enforceFloatType();});
+}
+
expr Type::enforceIntOrPtrOrVectorType() const {
return enforceScalarOrVectorType(
[&](auto &ty) { return ty.enforceIntOrPtrType(); });
@@ -192,7 +201,7 @@ expr Type::toBV(expr e) const {
}
StateValue Type::toBV(StateValue v) const {
- expr val = toBV(v.value);
+ expr val = toBV(move(v.value));
auto bw = val.bits();
return { move(val),
expr::mkIf(v.non_poison, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) };
@@ -206,6 +215,14 @@ StateValue Type::fromBV(StateValue v) const {
return { fromBV(v.value), v.non_poison == 0 };
}
+expr Type::combine_poison(const expr &boolean, const expr &orig) const {
+ if (orig.isBool())
+ return boolean && orig;
+
+ auto bw = orig.bits();
+ return expr::mkIf(boolean, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) | orig;
+}
+
ostream& operator<<(ostream &os, const Type &t) {
t.print(os);
return os;

MODIFY
ir/type.h
ir/type.h
@@ -67,12 +67,14 @@ public:
std::vector<Type*> *element_types = nullptr) const;
virtual smt::expr enforceFloatType() const;
+ smt::expr enforceVectorType() const;
virtual smt::expr enforceVectorType(
const std::function<smt::expr(const Type&)> &enforceElem) const;
smt::expr enforceScalarOrVectorType(
const std::function<smt::expr(const Type&)> &enforceElem) const;
smt::expr enforceIntOrVectorType(unsigned bits = 0) const;
+ smt::expr enforceIntOrFloatOrPtrOrVectorType() const;
smt::expr enforceIntOrPtrOrVectorType() const;
smt::expr enforceFloatOrVectorType() const;
@@ -85,6 +87,10 @@ public:
virtual smt::expr fromBV(smt::expr e) const;
virtual IR::StateValue fromBV(IR::StateValue v) const;
+ // combine existing poison value in BV repr with a new boolean expr
+ smt::expr combine_poison(const smt::expr &boolean,
+ const smt::expr &orig) const;
+
// returns pair of refinement constraints for <poison, !poison && value>
virtual std::pair<smt::expr, smt::expr>
refines(const IR::StateValue &src, const IR::StateValue &tgt) const = 0;

misc type fixes & add vector support to select