Merge pull request #4074 from diffblue/fix-smt2-binary

Fix use of binary irep in smt2_conv

Author: tautschnig

src/solvers/smt2/smt2_conv.cpp

@@ -275,11 +275,15 @@ constant_exprt smt2_convt::parse_literal(
         parse_literal(src.get_sub()[2], unsignedbv_typet(floatbv_type.get_e()));
       constant_exprt s3 =
         parse_literal(src.get_sub()[3], unsignedbv_typet(floatbv_type.get_f()));
+
+      const auto s1_int = numeric_cast_v<mp_integer>(s1);
+      const auto s2_int = numeric_cast_v<mp_integer>(s2);
+      const auto s3_int = numeric_cast_v<mp_integer>(s3);
+
       // stitch the bits together
-      std::string bits=id2string(s1.get_value())+
-                       id2string(s2.get_value())+
-                       id2string(s3.get_value());
-      value=binary2integer(bits, false);
+      value = bitwise_or(
+        s1_int << (floatbv_type.get_e() + floatbv_type.get_f()),
+        bitwise_or((s2_int << floatbv_type.get_f()), s3_int));
     }
     else
       value=0;
@@ -318,10 +322,12 @@ constant_exprt smt2_convt::parse_literal(
   }
   else if(type.id()==ID_c_enum_tag)
   {
-    return
-      from_integer(
-        value,
-        ns.follow_tag(to_c_enum_tag_type(type)));
+    constant_exprt result =
+      from_integer(value, ns.follow_tag(to_c_enum_tag_type(type)));
+
+    // restore the c_enum_tag type
+    result.type() = type;
+    return result;
   }
   else if(type.id()==ID_fixedbv ||
           type.id()==ID_floatbv)
@@ -331,7 +337,9 @@ constant_exprt smt2_convt::parse_literal(
   }
   else if(type.id()==ID_integer ||
           type.id()==ID_range)
+  {
     return from_integer(value, type);
+  }
   else
     INVARIANT(
       false,
@@ -384,25 +392,24 @@ exprt smt2_convt::parse_union(
   return union_exprt(first.get_name(), converted, type);
 }
 
-exprt smt2_convt::parse_struct(
-  const irept &src,
-  const struct_typet &type)
+struct_exprt
+smt2_convt::parse_struct(const irept &src, const struct_typet &type)
 {
   const struct_typet::componentst &components =
     type.components();
 
   struct_exprt result(exprt::operandst(components.size(), nil_exprt()), type);
 
   if(components.empty())
-    return std::move(result);
+    return result;
 
   if(use_datatypes)
   {
     // Structs look like:
     //  (mk-struct.1 <component0> <component1> ... <componentN>)
 
     if(src.get_sub().size()!=components.size()+1)
-      return std::move(result); // give up
+      return result; // give up
 
     for(std::size_t i=0; i<components.size(); i++)
     {
@@ -414,13 +421,12 @@ exprt smt2_convt::parse_struct(
   {
     // These are just flattened, i.e., we expect to see a monster bit vector.
     std::size_t total_width=boolbv_width(type);
-    exprt l = parse_literal(src, unsignedbv_typet(total_width));
-    if(!l.is_constant())
-      return nil_exprt();
+    const auto l = parse_literal(src, unsignedbv_typet(total_width));
 
-    irep_idt binary=to_constant_expr(l).get_value();
-    if(binary.size()!=total_width)
-      return nil_exprt();
+    const irep_idt binary =
+      integer2binary(numeric_cast_v<mp_integer>(l), total_width);
+
+    CHECK_RETURN(binary.size() == total_width);
 
     std::size_t offset=0;
 
@@ -443,20 +449,17 @@ exprt smt2_convt::parse_struct(
     }
   }
 
-  return std::move(result);
+  return result;
 }
 
-exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
+exprt smt2_convt::parse_rec(const irept &src, const typet &type)
 {
-  const typet &type=ns.follow(_type);
-
-  if(type.id()==ID_signedbv ||
-     type.id()==ID_unsignedbv ||
-     type.id()==ID_integer ||
-     type.id()==ID_rational ||
-     type.id()==ID_real ||
-     type.id()==ID_fixedbv ||
-     type.id()==ID_floatbv)
+  if(
+    type.id() == ID_signedbv || type.id() == ID_unsignedbv ||
+    type.id() == ID_integer || type.id() == ID_rational ||
+    type.id() == ID_real || type.id() == ID_c_enum ||
+    type.id() == ID_c_enum_tag || type.id() == ID_fixedbv ||
+    type.id() == ID_floatbv)
   {
     return parse_literal(src, type);
   }
@@ -486,10 +489,25 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
   {
     return parse_struct(src, to_struct_type(type));
   }
+  else if(type.id() == ID_struct_tag)
+  {
+    auto struct_expr =
+      parse_struct(src, ns.follow_tag(to_struct_tag_type(type)));
+    // restore the tag type
+    struct_expr.type() = type;
+    return std::move(struct_expr);
+  }
   else if(type.id()==ID_union)
   {
     return parse_union(src, to_union_type(type));
   }
+  else if(type.id() == ID_union_tag)
+  {
+    auto union_expr = parse_union(src, ns.follow_tag(to_union_tag_type(type)));
+    // restore the tag type
+    union_expr.type() = type;
+    return union_expr;
+  }
   else if(type.id()==ID_array)
   {
     return parse_array(src, to_array_type(type));
@@ -2371,15 +2389,15 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       significand = 1;
       exponent = 0;
       a.build(significand, exponent);
-      val.set(ID_value, integer2binary(a.pack(), a.spec.width()));
+      val.set_value(integer2bvrep(a.pack(), a.spec.width()));
 
       convert_constant(val);
       out << " ";
 
       significand = 0;
       exponent = 0;
       a.build(significand, exponent);
-      val.set(ID_value, integer2binary(a.pack(), a.spec.width()));
+      val.set_value(integer2bvrep(a.pack(), a.spec.width()));
 
       convert_constant(val);
       out << ")";
@@ -2780,7 +2798,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
   }
   else if(expr_type.id()==ID_pointer)
   {
-    const irep_idt &value=expr.get(ID_value);
+    const irep_idt &value = expr.get_value();
 
     if(value==ID_NULL)
     {
@@ -3110,7 +3128,7 @@ void smt2_convt::convert_rounding_mode_FPA(const exprt &expr)
   {
     const constant_exprt &cexpr=to_constant_expr(expr);
 
-    mp_integer value=binary2integer(id2string(cexpr.get_value()), false);
+    mp_integer value = numeric_cast_v<mp_integer>(cexpr);
 
     if(value==0)
       out << "roundNearestTiesToEven";

src/solvers/smt2/smt2_conv.h

@@ -237,7 +237,7 @@ class smt2_convt:public prop_convt
 
   // Parsing solver responses
   constant_exprt parse_literal(const irept &, const typet &type);
-  exprt parse_struct(const irept &s, const struct_typet &type);
+  struct_exprt parse_struct(const irept &s, const struct_typet &type);
   exprt parse_union(const irept &s, const union_typet &type);
   exprt parse_array(const irept &s, const array_typet &type);
   exprt parse_rec(const irept &s, const typet &type);

src/solvers/smt2/smt2_parser.cpp

@@ -394,6 +394,25 @@ exprt smt2_parsert::binary(irep_idt id, const exprt::operandst &op)
   return binary_exprt(op[0], id, op[1], op[0].type());
 }
 
+exprt smt2_parsert::function_application_ieee_float_eq(
+  const exprt::operandst &op)
+{
+  if(op.size() != 2)
+    throw error() << "FloatingPoint equality takes two operands";
+
+  if(op[0].type().id() != ID_floatbv || op[1].type().id() != ID_floatbv)
+    throw error() << "FloatingPoint equality takes FloatingPoint operands";
+
+  if(op[0].type() != op[1].type())
+  {
+    throw error() << "FloatingPoint equality takes FloatingPoint operands with "
+                  << "matching sort, but got " << smt2_format(op[0].type())
+                  << " vs " << smt2_format(op[1].type());
+  }
+
+  return ieee_float_equal_exprt(op[0], op[1]);
+}
+
 exprt smt2_parsert::function_application_ieee_float_op(
   const irep_idt &id,
   const exprt::operandst &op)
@@ -745,6 +764,16 @@ exprt smt2_parsert::function_application()
 
         return unary_predicate_exprt(ID_isinf, op[0]);
       }
+      else if(id == "fp.isNormal")
+      {
+        if(op.size() != 1)
+          throw error("fp.isNormal takes one operand");
+
+        if(op[0].type().id() != ID_floatbv)
+          throw error("fp.isNormal takes FloatingPoint operand");
+
+        return isnormal_exprt(op[0]);
+      }
       else if(id == "fp")
       {
         return function_application_fp(op);
@@ -754,6 +783,30 @@ exprt smt2_parsert::function_application()
       {
         return function_application_ieee_float_op(id, op);
       }
+      else if(id == "fp.eq")
+      {
+        return function_application_ieee_float_eq(op);
+      }
+      else if(id == "fp.leq")
+      {
+        return binary_predicate(ID_le, op);
+      }
+      else if(id == "fp.lt")
+      {
+        return binary_predicate(ID_lt, op);
+      }
+      else if(id == "fp.geq")
+      {
+        return binary_predicate(ID_ge, op);
+      }
+      else if(id == "fp.gt")
+      {
+        return binary_predicate(ID_gt, op);
+      }
+      else if(id == "fp.neg")
+      {
+        return unary(ID_unary_minus, op);
+      }
       else
       {
         // rummage through id_map

src/solvers/smt2/smt2_parser.h

@@ -122,6 +122,7 @@ class smt2_parsert
   exprt function_application_ieee_float_op(
     const irep_idt &,
     const exprt::operandst &);
+  exprt function_application_ieee_float_eq(const exprt::operandst &);
   exprt function_application_fp(const exprt::operandst &);
   typet sort();
   exprt::operandst operands();