bitcast: add initial support for casts between vectors and scalars
not correct for little endian?
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -739,53 +739,42 @@ void ConversionOp::print(ostream &os) const {
}
StateValue ConversionOp::toSMT(State &s) const {
- auto &v = s[*val];
- function<StateValue(const expr &, const Type &, const Type &)> fn;
+ auto v = s[*val];
+ function<StateValue(const expr &, const Type &)> fn;
switch (op) {
case SExt:
- fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ fn = [](auto &val, auto &to_type) -> StateValue {
return { val.sext(to_type.bits() - val.bits()), true };
};
break;
case ZExt:
- fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ fn = [](auto &val, auto &to_type) -> StateValue {
return { val.zext(to_type.bits() - val.bits()), true };
};
break;
case Trunc:
- fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ fn = [](auto &val, auto &to_type) -> StateValue {
return { val.trunc(to_type.bits()), true };
};
break;
case BitCast:
- fn = [&s](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 = from_type.getAsFloatType()->toInt(s, val);
- else if (to_type.isFloatType() && from_type.isIntType())
- newval = val.BV2float(to_type.getDummyValue(true).value);
- else
- UNREACHABLE();
- return { move(newval), true };
+ fn = [&s](auto &val, auto &to_type) -> StateValue {
+ return { to_type.fromBV(val), true };
};
break;
case SIntToFP:
- fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ fn = [](auto &val, auto &to_type) -> StateValue {
return { val.sint2fp(to_type.getDummyValue(false).value), true };
};
break;
case UIntToFP:
- fn = [](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ fn = [](auto &val, auto &to_type) -> StateValue {
return { val.uint2fp(to_type.getDummyValue(false).value), true };
};
break;
case FPToSInt:
- fn = [&](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ fn = [&](auto &val, 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)) &&
@@ -793,7 +782,7 @@ StateValue ConversionOp::toSMT(State &s) const {
};
break;
case FPToUInt:
- fn = [&](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ fn = [&](auto &val, auto &to_type) -> StateValue {
return { val.fp2uint(to_type.bits()),
val.foge(expr::mkFloat(0, val)) &&
val.fole(expr::IntUMax(getType().bits()).uint2fp(val)) &&
@@ -801,34 +790,47 @@ StateValue ConversionOp::toSMT(State &s) const {
};
break;
case Ptr2Int:
- fn = [&](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ fn = [&](auto &val, auto &to_type) -> StateValue {
return { s.getMemory().ptr2int(val).zextOrTrunc(to_type.bits()), true };
};
break;
case Int2Ptr:
- fn = [&](auto &val, auto &from_type, auto &to_type) -> StateValue {
+ fn = [&](auto &val, auto &to_type) -> StateValue {
return { s.getMemory().int2ptr(val), true };
};
break;
}
- auto scalar = [&](const StateValue &sv, const Type &from_type,
- const Type &to_type) -> StateValue {
- auto [v, np] = fn(sv.value, from_type, to_type);
+ auto scalar = [&](const StateValue &sv, const Type &to_type) -> StateValue {
+ auto [v, np] = fn(sv.value, to_type);
return { move(v), sv.non_poison && np };
};
+ if (op == BitCast)
+ v = val->getType().toInt(s, move(v));
+
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)));
+ auto elems = retty->numElementsConst();
+
+ // bitcast vect elems size may vary, so create a new data type whose
+ // element size is aligned with the output vector elem size
+ IntType elem_ty("int", retty->bits() / elems);
+ VectorType int_ty("vec", elems, elem_ty);
+ auto valty = op == BitCast ? &int_ty : val->getType().getAsAggregateType();
+
+ for (unsigned i = 0; i != elems; ++i) {
+ vals.emplace_back(scalar(valty->extract(v, i), retty->getChild(i)));
}
return retty->aggregateVals(vals);
}
- return scalar(v, val->getType(), getType());
+
+ // turn poison data into boolean, while keeping value in BV
+ if (op == BitCast)
+ v = IntType("int", getType().bits()).fromBV(v);
+
+ return scalar(v, getType());
}
expr ConversionOp::getTypeConstraints(const Function &f) const {
@@ -838,22 +840,17 @@ expr ConversionOp::getTypeConstraints(const Function &f) const {
case ZExt:
c = getType().enforceIntOrVectorType() &&
val->getType().enforceIntOrVectorType() &&
- val->getType().sizeVar().ult(getType().sizeVar());
+ val->getType().scalarSize().ult(getType().scalarSize());
break;
case Trunc:
c = getType().enforceIntOrVectorType() &&
val->getType().enforceIntOrVectorType() &&
- getType().sizeVar().ult(val->getType().sizeVar());
+ getType().scalarSize().ult(val->getType().scalarSize());
break;
case BitCast:
- c = (getType().enforcePtrOrVectorType() &&
- val->getType().enforcePtrOrVectorType()) ||
- ((getType().enforceIntOrVectorType() ||
- getType().enforceFloatOrVectorType()) &&
- (val->getType().enforceIntOrVectorType() ||
- val->getType().enforceFloatOrVectorType()));
-
- c &= getType().sizeVar() == val->getType().sizeVar();
+ c = getType().enforceIntOrFloatOrPtrOrVectorType() &&
+ val->getType().enforceIntOrFloatOrPtrOrVectorType() &&
+ getType().sizeVar() == val->getType().sizeVar();
break;
case SIntToFP:
case UIntToFP:
@@ -874,9 +871,11 @@ expr ConversionOp::getTypeConstraints(const Function &f) const {
val->getType().enforceIntOrVectorType();
break;
}
- return Value::getTypeConstraints() &&
- move(c) &&
- getType().enforceVectorTypeEquiv(val->getType());
+
+ c &= Value::getTypeConstraints();
+ if (op != BitCast)
+ c &= getType().enforceVectorTypeEquiv(val->getType());
+ return c;
}
unique_ptr<Instr> ConversionOp::dup(const string &suffix) const {

MODIFY
ir/type.cpp
ir/type.cpp
@@ -35,6 +35,10 @@ expr Type::sizeVar() const {
return var("bw", var_bw_bits);
}
+expr Type::scalarSize() const {
+ return sizeVar();
+}
+
expr Type::is(unsigned t) const {
return typeVar() == t;
}
@@ -206,6 +210,17 @@ StateValue Type::toBV(StateValue v) const {
expr::mkIf(v.non_poison, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) };
}
+expr Type::toInt(State &s, expr v) const {
+ return toBV(move(v));
+}
+
+StateValue Type::toInt(State &s, StateValue v) const {
+ expr val = toInt(s, move(v.value));
+ auto bw = val.bits();
+ return { move(val),
+ expr::mkIf(v.non_poison, expr::mkUInt(0, bw), expr::mkInt(-1, bw)) };
+}
+
expr Type::fromBV(expr e) const {
return e;
}
@@ -354,7 +369,7 @@ unsigned FloatType::bits() const {
return float_sizes[fpType].first;
}
-expr FloatType::toInt(State &s, const expr &fp) const {
+expr FloatType::toInt(State &s, expr fp) const {
expr isnan = fp.isNaN();
expr val = fp.float2BV();
@@ -378,6 +393,10 @@ expr FloatType::toInt(State &s, const expr &fp) const {
return expr::mkIf(isnan, nan, val);
}
+StateValue FloatType::toInt(State &s, StateValue v) const {
+ return Type::toInt(s, move(v));
+}
+
const FloatType* FloatType::getAsFloatType() const {
return this;
}
@@ -656,6 +675,16 @@ expr AggregateType::getTypeConstraints() const {
return r;
}
+expr AggregateType::sizeVar() const {
+ expr elems = numElements();
+ expr sz = expr::mkUInt(0, var_bw_bits);
+
+ for (unsigned i = 0; i < elements; ++i) {
+ sz = expr::mkIf(elems.ugt(i), sz + children[i]->sizeVar(), sz);
+ }
+ return sz;
+}
+
expr AggregateType::operator==(const AggregateType &rhs) const {
expr elems = numElements();
expr res = elems == rhs.numElements();
@@ -697,6 +726,23 @@ StateValue AggregateType::toBV(StateValue v) const {
return v;
}
+expr AggregateType::toInt(State &s, expr v) const {
+ UNREACHABLE();
+}
+
+StateValue AggregateType::toInt(State &s, StateValue v) const {
+ // structs can be empty
+ if (elements == 0)
+ return { expr::mkUInt(0, 1), true };
+
+ StateValue ret;
+ for (unsigned i = 0; i < elements; ++i) {
+ auto vv = children[i]->toInt(s, extract(v, i));
+ ret = i == 0 ? move(vv) : ret.concat(vv);
+ }
+ return ret;
+}
+
expr AggregateType::fromBV(expr e) const {
return Type::fromBV(move(e));
}
@@ -829,7 +875,7 @@ expr VectorType::getTypeConstraints() const {
return r;
}
-expr VectorType::sizeVar() const {
+expr VectorType::scalarSize() const {
return children[0]->sizeVar();
}
@@ -1060,6 +1106,14 @@ StateValue SymbolicType::toBV(StateValue val) const {
DISPATCH(toBV(move(val)), UNREACHABLE());
}
+expr SymbolicType::toInt(State &st, expr e) const {
+ DISPATCH(toInt(st, move(e)), UNREACHABLE());
+}
+
+StateValue SymbolicType::toInt(State &st, StateValue val) const {
+ DISPATCH(toInt(st, move(val)), UNREACHABLE());
+}
+
expr SymbolicType::fromBV(expr e) const {
DISPATCH(fromBV(move(e)), UNREACHABLE());
}

MODIFY
ir/type.h
ir/type.h
@@ -48,6 +48,7 @@ public:
virtual smt::expr getTypeConstraints() const = 0;
virtual smt::expr sizeVar() const;
+ virtual smt::expr scalarSize() const;
smt::expr operator==(const Type &rhs) const;
virtual void fixup(const smt::Model &m) = 0;
@@ -89,6 +90,8 @@ public:
virtual smt::expr toBV(smt::expr e) const;
virtual IR::StateValue toBV(IR::StateValue v) const;
+ virtual smt::expr toInt(State &s, smt::expr v) const;
+ virtual IR::StateValue toInt(State &s, IR::StateValue v) const;
virtual smt::expr fromBV(smt::expr e) const;
virtual IR::StateValue fromBV(IR::StateValue v) const;
@@ -176,7 +179,6 @@ public:
: Type(std::move(name)), fpType(fpType), defined(true) {}
unsigned bits() const override;
FpType getFpType() const { return fpType; };
- smt::expr toInt(State &s, const smt::expr &fp) const;
IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
@@ -188,6 +190,8 @@ public:
const FloatType* getAsFloatType() const override;
smt::expr toBV(smt::expr e) const override;
IR::StateValue toBV(IR::StateValue v) const override;
+ smt::expr toInt(State &s, smt::expr v) const override;
+ IR::StateValue toInt(State &s, 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>
@@ -250,12 +254,15 @@ public:
unsigned bits() const override;
IR::StateValue getDummyValue(bool non_poison) const override;
smt::expr getTypeConstraints() const override;
+ smt::expr sizeVar() const override;
smt::expr operator==(const AggregateType &rhs) const;
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 toInt(State &s, smt::expr v) const override;
+ IR::StateValue toInt(State &s, 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>
@@ -289,7 +296,7 @@ public:
const IR::StateValue &val,
const smt::expr &idx) const;
smt::expr getTypeConstraints() const override;
- smt::expr sizeVar() const override;
+ smt::expr scalarSize() const override;
bool isVectorType() const override;
smt::expr enforceVectorType(
const std::function<smt::expr(const Type&)> &enforceElem) const override;
@@ -351,6 +358,8 @@ public:
const StructType* getAsStructType() const override;
smt::expr toBV(smt::expr e) const override;
IR::StateValue toBV(IR::StateValue v) const override;
+ smt::expr toInt(State &s, smt::expr v) const override;
+ IR::StateValue toInt(State &s, 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>

bitcast: add initial support for casts between vectors and scalars
not correct for little endian?