__CPROVER_floatbv[width][mantissa]

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@2908 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

doc/html-manual/api.shtml

@@ -211,6 +211,22 @@ can be applied. The usual arithmetic promotions will be
 applied to operands of this type.
 </p>
 
+<h4>__CPROVER_floatbv</h4>
+
+<hr>
+<code>
+__CPROVER_floatbv [ <i>expression</i> ] [ <i>expression</i> ]
+</code>
+<hr>
+
+<p class="justified">
+This type is only available in the C frontend.  It is used
+to specify an IEEE-754 floating point number with arbitrary
+but fixed size.  The first parameter is the total size (in bits)
+of the number, and the second is the size (in bits) of the
+mantissa, or significand.
+</p>
+
 <h4>__CPROVER_size_t</h4>
 
 <p class="justified">

src/ansi-c/ansi_c_convert_type.cpp

@@ -130,6 +130,50 @@ void ansi_c_convert_typet::read_rec(const typet &type)
     
     bv_width=integer2long(size_int);
   }
+  else if(type.id()==ID_floatbv &&
+          !type.find(ID_f).is_nil() &&
+          !type.find(ID_size).is_nil())
+  {
+    floatbv_cnt++;
+
+    const exprt &size_expr=
+      static_cast<const exprt &>(type.find(ID_size));
+    const exprt &fsize_expr=
+      static_cast<const exprt &>(type.find(ID_f));
+
+    mp_integer size_int;
+    if(to_integer(size_expr, size_int))
+    {
+      err_location(location);
+      error("floatbv width has to be constant (got " + size_expr.to_string() + ")");
+      throw 0;
+    }
+    
+    if(size_int<1 || size_int>1024)
+    {
+      err_location(location);
+      error("floatbv width invalid");
+      throw 0;
+    }
+
+    bv_width=integer2long(size_int);
+
+    if(to_integer(fsize_expr, size_int))
+    {
+      err_location(location);
+      error("floatbv mantissa size has to be constant");
+      throw 0;
+    }
+
+    if(size_int<1 || size_int>bv_width)
+    {
+      err_location(location);
+      error("floatbv mantissa size invalid");
+      throw 0;
+    }
+
+    mantissa_width=integer2long(size_int);
+  }
   else if(type.id()==ID_short)
     short_cnt++;
   else if(type.id()==ID_long)
@@ -429,6 +473,12 @@ void ansi_c_convert_typet::write(typet &type)
       
       // need to decide on ID_C_c_type to set
     }
+    else if(floatbv_cnt)
+    {
+      type.id(ID_floatbv);
+      type.set(ID_width, bv_width);
+      type.set(ID_f, mantissa_width);
+    }
     else if(short_cnt)
     {
       if(long_cnt || char_cnt)

src/ansi-c/ansi_c_convert_type.h

@@ -26,7 +26,8 @@ public:
   // extensions
   unsigned int8_cnt, int16_cnt, int32_cnt, int64_cnt,
            ptr32_cnt, ptr64_cnt,
-           gcc_float128_cnt, gcc_int128_cnt, bv_cnt, bv_width;
+           gcc_float128_cnt, gcc_int128_cnt, bv_cnt, bv_width,
+           floatbv_cnt, mantissa_width;
   bool gcc_mode_QI, gcc_mode_HI, gcc_mode_SI, gcc_mode_DI, gcc_mode_TI;
            
   bool packed, aligned;
@@ -56,7 +57,7 @@ public:
     long_cnt=double_cnt=float_cnt=c_bool_cnt=proper_bool_cnt=complex_cnt=
     int8_cnt=int16_cnt=int32_cnt=int64_cnt=
     ptr32_cnt=ptr64_cnt=
-    gcc_float128_cnt=gcc_int128_cnt=bv_cnt=0;
+    gcc_float128_cnt=gcc_int128_cnt=bv_cnt=floatbv_cnt=0;
     vector_size.make_nil();
     alignment.make_nil();
     bv_width=0;

src/ansi-c/c_typecheck_type.cpp

@@ -307,6 +307,14 @@ void c_typecheck_baset::typecheck_vector_type(vector_typet &type)
     throw 0;
   }
 
+  if(sub_size==0)
+  {
+    err_location(size_location);
+    str << "type had size 0: `"
+        << to_string(type.subtype()) << "'";
+    throw 0;
+  }
+  
   // adjust by width of base type
   if(s%sub_size!=0)
   {

src/ansi-c/expr2c.cpp

@@ -218,7 +218,11 @@ std::string expr2ct::convert_rec(
     else if(width==config.ansi_c.double_width)
       return q+"double"+d;
     else
-      assert(false);
+    {
+      std::string swidth=src.get_string(ID_width);
+      std::string fwidth=src.get_string(ID_f);
+      return q+"__CPROVER_floatbv["+swidth+"]["+fwidth+"]";
+    }
   }
   else if(src.id()==ID_fixedbv)
   {

src/ansi-c/parser.y

@@ -146,6 +146,7 @@ extern char *yyansi_ctext;
 %token TOK_ACSL_EXISTS "\\exists"
 %token TOK_ARRAY_OF    "array_of"
 %token TOK_CPROVER_BITVECTOR "__CPROVER_bitvector"
+%token TOK_CPROVER_FLOATBV "__CPROVER_floatbv"
 %token TOK_CPROVER_ATOMIC "__CPROVER_atomic"
 %token TOK_CPROVER_BOOL "__CPROVER_bool"
 %token TOK_CPROVER_THROW "__CPROVER_throw"
@@ -1270,6 +1271,13 @@ basic_type_name:
           set($$, ID_bv);
           stack($$).add(ID_size).swap(stack($3));
         }
+        | TOK_CPROVER_FLOATBV '[' comma_expression ']' '[' comma_expression ']'
+        {
+          $$=$1;
+          set($$, ID_floatbv);
+          stack($$).add(ID_size).swap(stack($3));
+          stack($$).add(ID_f).swap(stack($6));
+        }
         | TOK_CPROVER_BOOL { $$=$1; set($$, ID_proper_bool); }
         ;
 

src/ansi-c/scanner.l

@@ -899,6 +899,7 @@ __decltype          { if(PARSER.cpp && PARSER.mode==ansi_c_parsert::GCC)
 "__CPROVER_array_of"     { loc(); return TOK_ARRAY_OF; }
 "__CPROVER_thread_local" { loc(); return TOK_THREAD_LOCAL; }
 "__CPROVER_bitvector"    { loc(); return TOK_CPROVER_BITVECTOR; }
+"__CPROVER_floatbv"      { loc(); return TOK_CPROVER_FLOATBV; }
 "__CPROVER_bool"         { loc(); return TOK_CPROVER_BOOL; }
 "__CPROVER_throw"        { loc(); return TOK_CPROVER_THROW; }
 "__CPROVER_catch"        { loc(); return TOK_CPROVER_CATCH; }