arithmetic promotion for fix-point arithmetic; issue #435

Author: Daniel Kroening

regression/cbmc/Fixedbv1/main.c

@@ -1,5 +1,5 @@
 int main() {
-  double x;
+  __CPROVER_fixedbv[64][32] x;
   int y;
 
   x=2;

regression/cbmc/Fixedbv1/test.desc

@@ -1,6 +1,6 @@
-CORE
+KNOWNBUG
 main.c
---fixedbv
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Fixedbv2/main.c

@@ -1,10 +1,10 @@
 main() {
-        float a;
-        double b;
+  __CPROVER_fixedbv[32][16] a;
+  __CPROVER_fixedbv[64][32] b;
 
-        a=1.25L;
-        assert(a==1.25);
+  a=1.25L;
+  assert(a==1.25);
 
-        b=1.250;
-        assert(b==1.25);
+  b=1.250;
+  assert(b==1.25);
 }

regression/cbmc/Fixedbv2/test.desc

@@ -1,6 +1,6 @@
-CORE
+KNOWNBUG
 main.c
---fixedbv
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Fixedbv3/main.c

@@ -1,6 +1,6 @@
 int nondet_int();
 
-double d = 0.0;
+__CPROVER_fixedbv[64][32] d = 0.0;
 
 void f1()
 {

regression/cbmc/Fixedbv3/test.desc

@@ -1,6 +1,6 @@
-CORE
+KNOWNBUG
 main.c
---fixedbv
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc/Fixedbv5/main.c

@@ -1,10 +1,11 @@
 int main()
 {
-  float a, b;
+  typedef __CPROVER_fixedbv[32][16] ft;
+  ft a, b;
 
-  __CPROVER_assume(a==1 || a==0.5 || a==2 || a==3 || a==0.1);
+  __CPROVER_assume(a==1 || a==(ft)0.5 || a==2 || a==3 || a==(ft)0.1);
   b=a;
   a/=2;
   a*=2;
-  __CPROVER_assert(a==b, "float div works");
+  __CPROVER_assert(a==b, "fixedbv div works");
 }

regression/cbmc/Fixedbv5/test.desc

@@ -1,6 +1,6 @@
-CORE
+KNOWNBUG
 main.c
---fixedbv
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

src/ansi-c/c_typecast.cpp

@@ -383,8 +383,7 @@ c_typecastt::c_typet c_typecastt::get_c_type(
     return BOOL;
   else if(type.id()==ID_c_bool)
     return BOOL;
-  else if(type.id()==ID_floatbv ||
-          type.id()==ID_fixedbv)
+  else if(type.id()==ID_floatbv)
   {
     if(width<=config.ansi_c.single_width)
       return SINGLE;
@@ -395,6 +394,10 @@ c_typecastt::c_typet c_typecastt::get_c_type(
     else if(width<=128)
       return FLOAT128;
   }
+  else if(type.id()==ID_fixedbv)
+  {
+    return FIXEDBV;
+  }
   else if(type.id()==ID_pointer)
   {
     if(type.subtype().id()==ID_empty)
@@ -728,8 +731,8 @@ void c_typecastt::implicit_typecast_arithmetic(
   if(max_type==LARGE_SIGNED_INT || max_type==LARGE_UNSIGNED_INT)
   {
     // get the biggest width of both
-    unsigned width1=type1.get_int(ID_width);
-    unsigned width2=type2.get_int(ID_width);
+    std::size_t width1=type1.get_size_t(ID_width);
+    std::size_t width2=type2.get_size_t(ID_width);
 
     // produce type
     typet result_type;
@@ -751,6 +754,30 @@ void c_typecastt::implicit_typecast_arithmetic(
 
     return;
   }
+  else if(max_type==FIXEDBV)
+  {
+    typet result_type;
+    
+    if(c_type1==FIXEDBV && c_type2==FIXEDBV)
+    {
+      // get bigger of both
+      std::size_t width1=to_fixedbv_type(type1).get_width();
+      std::size_t width2=to_fixedbv_type(type2).get_width();
+      if(width1>=width2)
+        result_type=type1;
+      else
+        result_type=type2;
+    }
+    else if(c_type1==FIXEDBV)
+      result_type=type1;
+    else
+      result_type=type2;
+
+    do_typecast(expr1, result_type);
+    do_typecast(expr2, result_type);
+    
+    return;
+  }
   else if(max_type==COMPLEX)
   {
     if(c_type1==COMPLEX && c_type2==COMPLEX)

src/ansi-c/c_typecast.h

@@ -72,9 +72,10 @@ class c_typecastt
                  LONG, ULONG,
                  LONGLONG, ULONGLONG,
                  LARGE_SIGNED_INT, LARGE_UNSIGNED_INT,
-                 INTEGER, // these are unbounded integers
+                 INTEGER, // these are unbounded integers, non-standard
+                 FIXEDBV, // fixed-point, non-standard
                  SINGLE, DOUBLE, LONGDOUBLE, FLOAT128, // float
-                 RATIONAL, REAL, // these are infinite precision
+                 RATIONAL, REAL, // infinite precision, non-standard
                  COMPLEX,
                  VOIDPTR, PTR, OTHER };