SMT2 floating point encoding fix

regression/cbmc/Float-div3/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --floatbv
 ^EXIT=0$

regression/cbmc/Float-smt2-1/test.desc

@@ -1,4 +1,4 @@
-CORE smt-backend broken-smt-backend
+CORE smt-backend
 main.c
 --smt2
 ^EXIT=10$

regression/cbmc/Float-to-double2/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 --floatbv --no-simplify
 ^EXIT=0$

src/solvers/smt2/smt2_conv.cpp

@@ -2280,12 +2280,13 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
     // adding the rounding mode.  See
     // smt2_convt::convert_floatbv_typecast.
     // The exception is bool and c_bool to float.
+    const auto &dest_floatbv_type = to_floatbv_type(dest_type);
 
     if(src_type.id()==ID_bool)
     {
       constant_exprt val(irep_idt(), dest_type);
 
-      ieee_floatt a(to_floatbv_type(dest_type));
+      ieee_floatt a(dest_floatbv_type);
 
       mp_integer significand;
       mp_integer exponent;
@@ -2316,6 +2317,23 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       const typecast_exprt tmp(src, bool_typet());
       convert_typecast(typecast_exprt(tmp, dest_type));
     }
+    else if(src_type.id() == ID_bv)
+    {
+      if(to_bv_type(src_type).get_width() != dest_floatbv_type.get_width())
+      {
+        UNEXPECTEDCASE("Typecast bv -> float with wrong width");
+      }
+
+      if(use_FPA_theory)
+      {
+        out << "((_ to_fp " << dest_floatbv_type.get_e() << " "
+            << dest_floatbv_type.get_f() + 1 << ") ";
+        convert_expr(src);
+        out << ')';
+      }
+      else
+        convert_expr(src);
+    }
     else
       UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float");
   }

src/solvers/smt2/smt2_dec.cpp

@@ -143,7 +143,12 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
 
   while(in)
   {
-    irept parsed = smt2irep(in, get_message_handler());
+    auto parsed_opt = smt2irep(in, get_message_handler());
+
+    if(!parsed_opt.has_value())
+      break;
+
+    const auto &parsed = parsed_opt.value();
 
     if(parsed.id()=="sat")
       res=resultt::D_SATISFIABLE;

src/solvers/smt2/smt2irep.cpp

@@ -22,41 +22,33 @@ class smt2irept:public smt2_tokenizert
   {
   }
 
-  inline irept operator()()
-  {
-    parse();
-    return result;
-  }
-
-  bool parse();
+  optionalt<irept> operator()();
 
 protected:
   messaget log;
-  irept result;
 };
 
-bool smt2irept::parse()
+optionalt<irept> smt2irept::operator()()
 {
   try
   {
     std::stack<irept> stack;
-    result.clear();
 
     while(true)
     {
       switch(next_token())
       {
       case END_OF_FILE:
-        throw error("unexpected end of file");
+        if(stack.empty())
+          return {};
+        else
+          throw error("unexpected end of file");
 
       case STRING_LITERAL:
       case NUMERAL:
       case SYMBOL:
         if(stack.empty())
-        {
-          result = irept(buffer);
-          return false; // all done!
-        }
+          return irept(buffer); // all done!
         else
           stack.top().get_sub().push_back(irept(buffer));
         break;
@@ -76,10 +68,7 @@ bool smt2irept::parse()
           stack.pop();
 
           if(stack.empty())
-          {
-            result = tmp;
-            return false; // all done!
-          }
+            return tmp; // all done!
 
           stack.top().get_sub().push_back(tmp);
           break;
@@ -94,11 +83,11 @@ bool smt2irept::parse()
   {
     log.error().source_location.set_line(e.get_line_no());
     log.error() << e.what() << messaget::eom;
-    return true;
+    return {};
   }
 }
 
-irept smt2irep(std::istream &in, message_handlert &message_handler)
+optionalt<irept> smt2irep(std::istream &in, message_handlert &message_handler)
 {
   return smt2irept(in, message_handler)();
 }

src/solvers/smt2/smt2irep.h

@@ -13,9 +13,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <iosfwd>
 
 #include <util/irep.h>
+#include <util/optional.h>
 
 class message_handlert;
 
-irept smt2irep(std::istream &, message_handlert &);
+/// returns an irep for an SMT-LIB2 expression read from a given stream
+/// returns {} when EOF is encountered before reading non-whitespace input
+optionalt<irept> smt2irep(std::istream &, message_handlert &);
 
 #endif // CPROVER_SOLVERS_SMT2_SMT2IREP_H