fix poison semantics of fp2[su]int
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -680,7 +680,7 @@ void ConversionOp::print(ostream &os) const {
StateValue ConversionOp::toSMT(State &s) const {
auto &[v, vp] = s[*val];
- expr newval;
+ expr newval, np = vp;
auto to_bw = getType().bits();
switch (op) {
@@ -713,9 +713,15 @@ StateValue ConversionOp::toSMT(State &s) const {
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();
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();
break;
case Ptr2Int:
newval = s.getMemory().ptr2int(v).zextOrTrunc(getType().bits());
@@ -724,7 +730,7 @@ StateValue ConversionOp::toSMT(State &s) const {
newval = s.getMemory().int2ptr(v);
break;
}
- return { move(newval), expr(vp) };
+ return { move(newval), move(np) };
}
expr ConversionOp::getTypeConstraints(const Function &f) const {

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -175,6 +175,11 @@ expr expr::mkInt(const char *n, unsigned bits) {
return bits ? Z3_mk_numeral(ctx(), n, mkBVSort(bits)) : expr();
}
+expr expr::mkFloat(double n, const expr &type) {
+ C2(type);
+ return Z3_mk_fpa_numeral_double(ctx(), n, type.sort());
+}
+
expr expr::mkHalf(float n) {
return Z3_mk_fpa_numeral_float(ctx(), n, Z3_mk_fpa_sort_half(ctx()));
}
@@ -223,13 +228,19 @@ expr expr::mkFreshVar(const char *prefix, const expr &type) {
expr expr::IntSMin(unsigned bits) {
if (bits == 0)
return {};
- return mkUInt(1, 1).concat(mkUInt(0, bits-1));
+ expr v = mkUInt(1, 1);
+ if (bits > 1)
+ v = v.concat(mkUInt(0, bits - 1));
+ return v;
}
expr expr::IntSMax(unsigned bits) {
if (bits == 0)
return {};
- return mkUInt(0, 1).concat(mkInt(-1, bits-1));
+ expr v = mkUInt(0, 1);
+ if (bits > 1)
+ v = v.concat(mkInt(-1, bits - 1));
+ return v;
}
expr expr::IntUMax(unsigned bits) {

MODIFY
smt/expr.h
smt/expr.h
@@ -79,6 +79,7 @@ public:
static expr mkUInt(uint64_t n, unsigned bits);
static expr mkInt(int64_t n, unsigned bits);
static expr mkInt(const char *n, unsigned bits);
+ static expr mkFloat(double n, const expr &type);
static expr mkHalf(float n);
static expr mkFloat(float n);
static expr mkDouble(double n);

MODIFY
tests/unit/fp-casts.opt
tests/unit/fp-casts.opt
@@ -8,12 +8,22 @@ Name: uitofp
=>
%r = 255.0
-Name: sitofp
+Name: fp2si
%r = fptosi -1.0
=>
%r = -1
-Name: sitofp
+Name: fp2si 2
+%r = fptosi -200.0 to i2
+ =>
+%r = poison
+
+Name: fp2ui
%r = fptoui 255.0 to i8
=>
%r = -1
+
+Name: fp2ui 2
+%r = fptoui -1.0 to i8
+ =>
+%r = poison

fix poison semantics of fp2[su]int