fix bitcast of floats<->ints
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -492,7 +492,15 @@ StateValue ConversionOp::toSMT(State &s) const {
newval = v.trunc(to_bw);
break;
case BitCast:
+ if ((getType().isIntType() && val.getType().isIntType()) ||
+ (getType().isFloatType() && val.getType().isFloatType()))
newval = v;
+ else if (getType().isIntType() && val.getType().isFloatType())
+ newval = v.float2BV();
+ else if (getType().isFloatType() && val.getType().isIntType())
+ newval = v.BV2float(getType().getDummyValue());
+ else
+ UNREACHABLE();
break;
case Ptr2Int:
newval = s.getMemory().ptr2int(v);

MODIFY
ir/type.cpp
ir/type.cpp
@@ -97,6 +97,14 @@ expr Type::sameType(const Type &b) const {
return false;
}
+bool Type::isIntType() const {
+ return false;
+}
+
+bool Type::isFloatType() const {
+ return false;
+}
+
expr Type::enforceIntType(unsigned bits) const {
return false;
}
@@ -210,6 +218,10 @@ void IntType::fixup(const Model &m) {
bitwidth = m.getUInt(sizeVar());
}
+bool IntType::isIntType() const {
+ return true;
+}
+
expr IntType::enforceIntType(unsigned bits) const {
return bits ? sizeVar() == bits : true;
}
@@ -304,6 +316,10 @@ void FloatType::fixup(const Model &m) {
fpType = FpType(fp_typ);
}
+bool FloatType::isFloatType() const {
+ return true;
+}
+
expr FloatType::enforceFloatType() const {
return true;
}
@@ -760,6 +776,14 @@ void SymbolicType::fixup(const Model &m) {
}
}
+bool SymbolicType::isIntType() const {
+ return typ == Int;
+}
+
+bool SymbolicType::isFloatType() const {
+ return typ == Float;
+}
+
expr SymbolicType::enforceIntType(unsigned bits) const {
return isInt() && i.enforceIntType(bits);
}

MODIFY
ir/type.h
ir/type.h
@@ -45,6 +45,9 @@ public:
smt::expr sameType(const Type &rhs) const;
virtual void fixup(const smt::Model &m) = 0;
+ virtual bool isIntType() const;
+ virtual bool isFloatType() const;
+
virtual smt::expr enforceIntType(unsigned bits = 0) const;
virtual smt::expr enforceIntOrVectorType() const;
virtual smt::expr enforceIntOrPtrOrVectorType() const;
@@ -100,6 +103,7 @@ public:
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;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;
@@ -132,6 +136,7 @@ public:
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;
const FloatType* getAsFloatType() const override;
std::pair<smt::expr, std::vector<smt::expr>>
@@ -252,6 +257,8 @@ public:
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;
smt::expr enforceIntType(unsigned bits = 0) const override;
smt::expr enforceIntOrVectorType() const override;
smt::expr enforceIntOrPtrOrVectorType() const override;

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -1053,6 +1053,16 @@ expr expr::toBVBool() const {
return mkIf(*this, mkUInt(1, sort), mkUInt(0, sort));
}
+expr expr::float2BV() const {
+ C();
+ return Z3_mk_fpa_to_ieee_bv(ctx(), ast());
+}
+
+expr expr::BV2float(const expr &type) const {
+ C(type);
+ return Z3_mk_fpa_to_fp_bv(ctx(), ast(), type.sort());
+}
+
expr expr::mkUF(const char *name, const vector<expr> &args, const expr &range) {
C2(range);
auto num_args = args.size();

MODIFY
smt/expr.h
smt/expr.h
@@ -154,6 +154,12 @@ public:
expr ctlz() const;
expr ctpop() const;
+ expr fadd(const expr &rhs) const;
+ expr fsub(const expr &rhs) const;
+ expr fmul(const expr &rhs) const;
+ expr fdiv(const expr &rhs) const;
+ expr frem(const expr &rhs) const;
+
expr operator&(const expr &rhs) const;
expr operator|(const expr &rhs) const;
expr operator^(const expr &rhs) const;
@@ -199,11 +205,8 @@ public:
expr extract(unsigned high, unsigned low) const;
expr toBVBool() const;
- expr fadd(const expr &rhs) const;
- expr fsub(const expr &rhs) const;
- expr fmul(const expr &rhs) const;
- expr fdiv(const expr &rhs) const;
- expr frem(const expr &rhs) const;
+ expr float2BV() const;
+ expr BV2float(const expr &type) const;
// we don't expose SMT expr types, so range must be passed as a dummy value
// of the desired type

fix bitcast of floats<->ints