add vector support for conversion ops
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -738,103 +738,144 @@ void ConversionOp::print(ostream &os) const {
}
StateValue ConversionOp::toSMT(State &s) const {
- auto &[v, vp] = s[*val];
- expr newval, np = vp;
- auto to_bw = getType().bits();
+ auto &v = s[*val];
+ function<StateValue(const expr &, const Type &, const Type &)> fn;
switch (op) {
case SExt:
- newval = v.sext(to_bw - val->bits());
+ fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ return { val.sext(to_type.bits() - val.bits()), true };
+ };
break;
case ZExt:
- newval = v.zext(to_bw - val->bits());
+ fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ return { val.zext(to_type.bits() - val.bits()), true };
+ };
break;
case Trunc:
- newval = v.trunc(to_bw);
+ fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ return { val.trunc(to_type.bits()), true };
+ };
break;
case BitCast:
- if ((getType().isIntType() && val->getType().isIntType()) ||
- (getType().isFloatType() && val->getType().isFloatType()) ||
- (getType().isPtrType() && val->getType().isPtrType()))
- newval = v;
- else if (getType().isIntType() && val->getType().isFloatType())
- newval = v.float2BV();
- else if (getType().isFloatType() && val->getType().isIntType())
- newval = v.BV2float(getType().getDummyValue(true).value);
+ fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ expr newval;
+ if ((to_type.isIntType() && from_type.isIntType()) ||
+ (to_type.isFloatType() && from_type.isFloatType()) ||
+ (to_type.isPtrType() && from_type.isPtrType()))
+ newval = val;
+ else if (to_type.isIntType() && from_type.isFloatType())
+ newval = val.float2BV();
+ else if (to_type.isFloatType() && from_type.isIntType())
+ newval = val.BV2float(to_type.getDummyValue(true).value);
else
UNREACHABLE();
+ return { move(newval), true };
+ };
break;
case SIntToFP:
- newval = v.sint2fp(getType().getDummyValue(false).value);
+ fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ return { val.sint2fp(to_type.getDummyValue(false).value), true };
+ };
break;
case UIntToFP:
- newval = v.uint2fp(getType().getDummyValue(false).value);
+ fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ return { val.uint2fp(to_type.getDummyValue(false).value), true };
+ };
break;
case FPToSInt:
- newval = v.fp2sint(to_bw);
- np &= v.foge(expr::IntSMin(getType().bits()).sint2fp(v));
- np &= v.fole(expr::IntSMax(getType().bits()).sint2fp(v));
- np &= !v.isInf();
+ fn = [&](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ return { val.fp2sint(to_type.bits()),
+ val.foge(expr::IntSMin(getType().bits()).sint2fp(val)) &&
+ val.fole(expr::IntSMax(getType().bits()).sint2fp(val)) &&
+ !val.isInf() };
+ };
break;
case FPToUInt:
- newval = v.fp2uint(to_bw);
- np &= v.foge(expr::mkFloat(0, v));
- np &= v.fole(expr::IntUMax(getType().bits()).uint2fp(v));
- np &= !v.isInf();
+ fn = [&](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ return { val.fp2uint(to_type.bits()),
+ val.foge(expr::mkFloat(0, val)) &&
+ val.fole(expr::IntUMax(getType().bits()).uint2fp(val)) &&
+ !val.isInf() };
+ };
break;
case Ptr2Int:
- newval = s.getMemory().ptr2int(v).zextOrTrunc(getType().bits());
+ fn = [&](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ return { s.getMemory().ptr2int(val).zextOrTrunc(to_type.bits()), true };
+ };
break;
case Int2Ptr:
- newval = s.getMemory().int2ptr(v);
+ fn = [&](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ return { s.getMemory().int2ptr(val), true };
+ };
break;
}
- return { move(newval), move(np) };
+
+ auto scalar = [&](const StateValue &sv, const Type &from_type,
+ const Type &to_type) -> StateValue {
+ auto [v, np] = fn(sv.value, from_type, to_type);
+ return { move(v), sv.non_poison && np };
+ };
+
+ if (getType().isVectorType()) {
+ vector<StateValue> vals;
+ auto valty = val->getType().getAsAggregateType();
+ auto retty = getType().getAsAggregateType();
+ for (unsigned i = 0, e = valty->numElementsConst(); i != e; ++i) {
+ vals.emplace_back(scalar(valty->extract(v, i), valty->getChild(i),
+ retty->getChild(i)));
+ }
+ return retty->aggregateVals(vals);
+ }
+ return scalar(v, val->getType(), getType());
}
expr ConversionOp::getTypeConstraints(const Function &f) const {
expr c;
- // TODO: add vector support
switch (op) {
case SExt:
case ZExt:
- c = getType().enforceIntType() &&
- getType().sameType(val->getType()) &&
+ c = getType().enforceIntOrVectorType() &&
+ val->getType().enforceIntOrVectorType() &&
val->getType().sizeVar().ult(getType().sizeVar());
break;
case Trunc:
- c = getType().enforceIntType() &&
- getType().sameType(val->getType()) &&
+ c = getType().enforceIntOrVectorType() &&
+ val->getType().enforceIntOrVectorType() &&
getType().sizeVar().ult(val->getType().sizeVar());
break;
case BitCast:
- c = ((getType().enforcePtrType() && val->getType().enforcePtrType()) ||
- ((getType().enforceIntType() || getType().enforceFloatType()) &&
- (val->getType().enforceIntType() ||
- val->getType().enforceFloatType()))) &&
- getType().sizeVar() == val->getType().sizeVar();
+ c = (getType().enforcePtrOrVectorType() &&
+ val->getType().enforcePtrOrVectorType()) ||
+ ((getType().enforceIntOrVectorType() ||
+ getType().enforceFloatOrVectorType()) &&
+ (val->getType().enforceIntOrVectorType() ||
+ val->getType().enforceFloatOrVectorType()));
+
+ c &= getType().sizeVar() == val->getType().sizeVar();
break;
case SIntToFP:
case UIntToFP:
- // FIXME: output is vector iff input is vector
- c = getType().enforceFloatType() &&
- val->getType().enforceIntType();
+ c = getType().enforceFloatOrVectorType() &&
+ val->getType().enforceIntOrVectorType();
break;
case FPToSInt:
case FPToUInt:
- c = getType().enforceIntType() &&
- val->getType().enforceFloatType();
+ c = getType().enforceIntOrVectorType() &&
+ val->getType().enforceFloatOrVectorType();
break;
case Ptr2Int:
- c = getType().enforceIntType() &&
- val->getType().enforcePtrType();
+ c = getType().enforceIntOrVectorType() &&
+ val->getType().enforcePtrOrVectorType();
break;
case Int2Ptr:
- c = getType().enforcePtrType() &&
- val->getType().enforceIntType();
+ c = getType().enforcePtrOrVectorType() &&
+ val->getType().enforceIntOrVectorType();
break;
}
- return Value::getTypeConstraints() && move(c);
+ return Value::getTypeConstraints() &&
+ move(c) &&
+ getType().enforceVectorTypeEquiv(val->getType());
}
unique_ptr<Instr> ConversionOp::dup(const string &suffix) const {

MODIFY
ir/type.cpp
ir/type.cpp
@@ -71,33 +71,6 @@ expr Type::operator==(const Type &b) const {
return false;
}
-expr Type::sameType(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)) \
- return lhs->sameType(*rhs); \
- }
-
- CMP(IntType)
- CMP(FloatType)
- CMP(PtrType)
- CMP(ArrayType)
- CMP(VectorType)
- CMP(StructType)
-#undef CMP
-
- if (auto lhs = dynamic_cast<const SymbolicType*>(this))
- return lhs->sameType(b);
-
- if (auto rhs = dynamic_cast<const SymbolicType*>(&b))
- return rhs->sameType(*this);
-
- return false;
-}
-
bool Type::isIntType() const {
return false;
}
@@ -203,6 +176,11 @@ expr Type::enforceFloatOrVectorType() const {
[&](auto &ty) { return ty.enforceFloatType(); });
}
+expr Type::enforcePtrOrVectorType() const {
+ return enforceScalarOrVectorType(
+ [&](auto &ty) { return ty.enforcePtrType(); });
+}
+
const FloatType* Type::getAsFloatType() const {
return nullptr;
}
@@ -315,10 +293,6 @@ expr IntType::operator==(const IntType &rhs) const {
return sizeVar() == rhs.sizeVar();
}
-expr IntType::sameType(const IntType &rhs) const {
- return true;
-}
-
void IntType::fixup(const Model &m) {
if (!defined)
bitwidth = m.getUInt(sizeVar());
@@ -419,10 +393,6 @@ expr FloatType::operator==(const FloatType &rhs) const {
return sizeVar() == rhs.sizeVar();
}
-expr FloatType::sameType(const FloatType &rhs) const {
- return true;
-}
-
void FloatType::fixup(const Model &m) {
if (defined)
return;
@@ -520,10 +490,6 @@ expr PtrType::operator==(const PtrType &rhs) const {
ASVar() == rhs.ASVar();
}
-expr PtrType::sameType(const PtrType &rhs) const {
- return *this == rhs;
-}
-
void PtrType::fixup(const Model &m) {
if (!defined)
addr_space = m.getUInt(ASVar());
@@ -647,16 +613,6 @@ expr AggregateType::operator==(const AggregateType &rhs) const {
return res;
}
-expr AggregateType::sameType(const AggregateType &rhs) const {
- expr elems = numElements();
- expr res = elems == rhs.numElements();
- for (unsigned i = 0, e = min(children.size(), rhs.children.size());
- i != e; ++i) {
- res &= elems.ugt(i).implies(children[i]->sameType(*rhs.children[i]));
- }
- return res;
-}
-
void AggregateType::fixup(const Model &m) {
if (!defined)
elements = m.getUInt(numElements());
@@ -802,6 +758,10 @@ expr VectorType::getTypeConstraints() const {
return r;
}
+expr VectorType::sizeVar() const {
+ return children[0]->sizeVar();
+}
+
bool VectorType::isVectorType() const {
return true;
}
@@ -931,37 +891,6 @@ expr SymbolicType::operator==(const Type &b) const {
UNREACHABLE();
}
-expr SymbolicType::sameType(const Type &b) const {
- if (this == &b)
- return true;
-
- if (auto rhs = dynamic_cast<const IntType*>(&b))
- return isInt() && (i ? i->sameType(*rhs) : false);
- if (auto rhs = dynamic_cast<const FloatType*>(&b))
- return isFloat() && (f ? f->sameType(*rhs) : false);
- if (auto rhs = dynamic_cast<const PtrType*>(&b))
- return isPtr() && (p ? p->sameType(*rhs) : false);
- if (auto rhs = dynamic_cast<const ArrayType*>(&b))
- return isArray() && (a ? a->sameType(*rhs) : false);
- if (auto rhs = dynamic_cast<const VectorType*>(&b))
- return isVector() && (v ? v->sameType(*rhs) : false);
- if (auto rhs = dynamic_cast<const StructType*>(&b))
- return isStruct() && (s ? s->sameType(*rhs) : false);
-
- if (auto rhs = dynamic_cast<const SymbolicType*>(&b)) {
- expr c(false);
- if (i && rhs->i) c |= isInt() && i->sameType(*rhs->i);
- if (f && rhs->f) c |= isFloat() && f->sameType(*rhs->f);
- 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);
- if (s && rhs->s) c |= isStruct() && s->sameType(*rhs->s);
- return move(c) && typeVar() == rhs->typeVar();
- }
- assert(0 && "unhandled case in SymbolicType::sameType");
- UNREACHABLE();
-}
-
void SymbolicType::fixup(const Model &m) {
unsigned smt_typ = m.getUInt(typeVar());
assert(smt_typ >= Int && smt_typ <= Struct);

MODIFY
ir/type.h
ir/type.h
@@ -49,7 +49,6 @@ public:
virtual smt::expr getTypeConstraints() const = 0;
virtual smt::expr sizeVar() const;
smt::expr operator==(const Type &rhs) const;
- smt::expr sameType(const Type &rhs) const;
virtual void fixup(const smt::Model &m) = 0;
virtual bool isIntType() const;
@@ -82,6 +81,7 @@ public:
smt::expr enforceIntOrFloatOrPtrOrVectorType() const;
smt::expr enforceIntOrPtrOrVectorType() const;
smt::expr enforceFloatOrVectorType() const;
+ smt::expr enforcePtrOrVectorType() const;
virtual const FloatType* getAsFloatType() const;
virtual const AggregateType* getAsAggregateType() const;
@@ -145,7 +145,6 @@ public:
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;
smt::expr operator==(const IntType &rhs) const;
- smt::expr sameType(const IntType &rhs) const;
void fixup(const smt::Model &m) override;
bool isIntType() const override;
smt::expr enforceIntType(unsigned bits = 0) const override;
@@ -178,7 +177,6 @@ public:
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;
smt::expr operator==(const FloatType &rhs) const;
- smt::expr sameType(const FloatType &rhs) const;
void fixup(const smt::Model &m) override;
bool isFloatType() const override;
smt::expr enforceFloatType() const override;
@@ -210,7 +208,6 @@ public:
smt::expr getTypeConstraints() const override;
smt::expr sizeVar() const override;
smt::expr operator==(const PtrType &rhs) const;
- smt::expr sameType(const PtrType &rhs) const;
void fixup(const smt::Model &m) override;
bool isPtrType() const override;
smt::expr enforcePtrType() const override;
@@ -247,7 +244,6 @@ public:
IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const AggregateType &rhs) const;
- smt::expr sameType(const AggregateType &rhs) const;
void fixup(const smt::Model &m) override;
smt::expr enforceAggregateType(
std::vector<Type *> *element_types) const override;
@@ -284,6 +280,7 @@ public:
const IR::StateValue &n,
const smt::expr &idx) const;
smt::expr getTypeConstraints() const override;
+ smt::expr sizeVar() const override;
bool isVectorType() const override;
smt::expr enforceVectorType(
const std::function<smt::expr(const Type&)> &enforceElem) const override;
@@ -325,7 +322,6 @@ public:
IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
smt::expr operator==(const Type &rhs) const;
- smt::expr sameType(const Type &rhs) const;
void fixup(const smt::Model &m) override;
bool isIntType() const override;
bool isFloatType() const override;

add vector support for conversion ops