two fixes to fpto*i (#733)

As mentioned in https://reviews.llvm.org/D106053#2885236 , Alive2 had a bug in fptoui/si encoding.

`fptoui float 31.5 to i32' was yielding poison because np was `(float)(i32)31.5 == 31.5' which is alway false.
The rhs is fixed to round towards zero so that it becomes `(float)(i32)31.5 == round_towards_zero(31.5)'.

Also, fptoui should round towards zero according to LangRef, but it was using nearest ties to even.
This is fixed as well.

ir/instr.cpp

@@ -1253,14 +1253,14 @@ StateValue ConversionOp::toSMT(State &s) const {
       expr bv  = val.fp2sint(to_type.bits());
       expr fp2 = bv.sint2fp(val);
       // -0.0 is converted to 0 and then to 0.0, though -0.0 is ok to convert
-      return { move(bv), val.isFPZero() || fp2 == val };
+      return { move(bv), val.isFPZero() || fp2 == val.roundtz() };
     };
     break;
   case FPToUInt:
     fn = [](auto &&val, auto &to_type) -> StateValue {
       expr bv  = val.fp2uint(to_type.bits());
       expr fp2 = bv.uint2fp(val);
-      return { move(bv), fp2 == val };
+      return { move(bv), fp2 == val.roundtz() };
     };
     break;
   case FPExt:

smt/expr.cpp

@@ -1720,7 +1720,7 @@ expr expr::fp2sint(unsigned bits) const {
 
 expr expr::fp2uint(unsigned bits) const {
   C();
-  auto rm = Z3_mk_fpa_round_nearest_ties_to_even(ctx());
+  auto rm = Z3_mk_fpa_rtz(ctx());
   return simplify_const(Z3_mk_fpa_to_ubv(ctx(), rm, ast(), bits), *this);
 }
 

tests/alive-tv/fp/fptosi-nonpoison.srctgt.ll

@@ -0,0 +1,10 @@
+define i32 @src() {
+	%v = fptosi float 31.5 to i32
+	ret i32 %v
+}
+
+define i32 @tgt() {
+	ret i32 poison
+}
+
+; ERROR: Target is more poisonous than source

tests/alive-tv/fp/fptoui-nonpoison.srctgt.ll

@@ -0,0 +1,12 @@
+; https://reviews.llvm.org/D106053#2885236
+
+define i32 @src() {
+	%v = fptoui float 31.5 to i32
+	ret i32 %v
+}
+
+define i32 @tgt() {
+	ret i32 poison
+}
+
+; ERROR: Target is more poisonous than source

tests/alive-tv/fp/fptoui-rtz.srctgt.ll

@@ -0,0 +1,10 @@
+; fptoui does rounding towards zero conversion when it ties
+
+define i32 @src() {
+	%v = fptoui float 31.5 to i32
+	ret i32 %v
+}
+
+define i32 @tgt() {
+	ret i32 31
+}