conversion of floatbv constants to fixedbv constants

Author: Daniel Kroening

regression/cbmc/Fixedbv1/main.c

@@ -1,3 +1,5 @@
+#include <assert.h>
+
 int main() {
   __CPROVER_fixedbv[64][32] x;
   int y;

regression/cbmc/Fixedbv1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Fixedbv2/main.c

@@ -1,10 +1,12 @@
+#include <assert.h>
+
 main() {
   __CPROVER_fixedbv[32][16] a;
   __CPROVER_fixedbv[64][32] b;
 
   a=1.25L;
-  assert(a==1.25);
+  assert(a==(__CPROVER_fixedbv[32][16])1.25);
 
   b=1.250;
-  assert(b==1.25);
+  assert(b==(__CPROVER_fixedbv[64][32])1.25);
 }

regression/cbmc/Fixedbv2/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Fixedbv3/main.c

@@ -1,3 +1,5 @@
+#include <assert.h>
+
 int nondet_int();
 
 __CPROVER_fixedbv[64][32] d = 0.0;
@@ -20,5 +22,5 @@ int main()
 
   d += (x > 3);
 
-  assert(d == 2.0);
+  assert(d == (__CPROVER_fixedbv[64][32])2.0);
 }

regression/cbmc/Fixedbv3/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

regression/cbmc/Fixedbv5/main.c

@@ -3,7 +3,7 @@ int main()
   typedef __CPROVER_fixedbv[32][16] ft;
   ft a, b;
 
-  __CPROVER_assume(a==1 || a==(ft)0.5 || a==2 || a==3 || a==(ft)0.1);
+  __CPROVER_assume(a==1 || a==(ft)0.5 || a==2 || a==3 || a==(ft)0.25);
   b=a;
   a/=2;
   a*=2;

regression/cbmc/Fixedbv5/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

src/util/simplify_expr.cpp

@@ -657,14 +657,14 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
       if(expr_type_id==ID_unsignedbv ||
          expr_type_id==ID_signedbv)
       {
-        // cast from float to int
+        // cast from fixedbv to int
         fixedbvt f(to_constant_expr(expr.op0()));
         expr=from_integer(f.to_integer(), expr_type);
         return false;
       }
       else if(expr_type_id==ID_fixedbv)
       {
-        // float to double or double to float
+        // fixedbv to fixedbv
         fixedbvt f(to_constant_expr(expr.op0()));
         f.round(to_fixedbv_type(expr_type));
         expr=f.to_expr();
@@ -673,22 +673,33 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
     }
     else if(op_type_id==ID_floatbv)
     {
+      ieee_floatt f(to_constant_expr(expr.op0()));
+
       if(expr_type_id==ID_unsignedbv ||
          expr_type_id==ID_signedbv)
       {
         // cast from float to int
-        ieee_floatt f(to_constant_expr(expr.op0()));
         expr=from_integer(f.to_integer(), expr_type);
         return false;
       }
       else if(expr_type_id==ID_floatbv)
       {
         // float to double or double to float
-        ieee_floatt f(to_constant_expr(expr.op0()));
         f.change_spec(to_floatbv_type(expr_type));
         expr=f.to_expr();
         return false;
       }
+      else if(expr_type_id==ID_fixedbv)
+      {
+        fixedbvt fixedbv;
+        fixedbv.spec=fixedbv_spect(to_fixedbv_type(expr_type));
+        ieee_floatt factor(f.spec);
+        factor.from_integer(power(2, fixedbv.spec.get_fraction_bits()));
+        f*=factor;
+        fixedbv.set_value(f.to_integer());
+        expr=fixedbv.to_expr();
+        return false;
+      }
     }
     else if(op_type_id==ID_bv)
     {