Fix and demonstrate support for __CPROVER_rational

Author: polgreen

regression/cbmc/rational1/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  __CPROVER_rational x;
+  __CPROVER_rational y;
+  x = 6 / 10;
+  y = 3 / 5;
+
+  __CPROVER_assert(y != x, "should fail");
+}

regression/cbmc/rational1/test.desc

@@ -0,0 +1,6 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--trace --smt2
+^EXIT=10$
+^SIGNAL=0$
+--

regression/cbmc/rational1/typecheck.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--show-goto-functions
+^[[:space:]]*ASSIGN main::1::x := cast\(6 / 10, ℚ\)
+^EXIT=0$
+^SIGNAL=0$
+--

src/solvers/flattening/boolbv_width.cpp

@@ -206,6 +206,10 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
   {
     cache_entry = defined_entryt{0};
   }
+  else if(type_id == ID_rational)
+  {
+    cache_entry = defined_entryt{1};
+  }
   else
   {
     UNIMPLEMENTED_FEATURE(

src/solvers/smt2/smt2_conv.cpp

@@ -29,6 +29,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/pointer_predicates.h>
 #include <util/prefix.h>
 #include <util/range.h>
+#include <util/rational.h>
+#include <util/rational_tools.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 #include <util/string2int.h>
@@ -416,8 +418,7 @@ constant_exprt smt2_convt::parse_literal(
 
   if(!src.id().empty())
   {
-    const std::string &s=src.id_string();
-
+    const std::string &s = src.id_string();
     if(s.size()>=2 && s[0]=='#' && s[1]=='b')
     {
       // Binary #b010101
@@ -430,8 +431,29 @@ constant_exprt smt2_convt::parse_literal(
     }
     else
     {
+      std::size_t pos = s.find(".");
+      if(pos != std::string::npos)
+      {
+        // Decimal, return as rational
+        mp_integer first = string2integer(s.substr(0, pos));
+        mp_integer second = string2integer(s.substr(pos, std::string::npos));
+        if(type.id() == ID_rational)
+        {
+          rationalt rational_value(first);
+          rationalt second_rational(second);
+          rationalt tmp = rational_value + second_rational / rationalt(100);
+          return from_rational(tmp);
+        }
+        else
+        {
+          UNREACHABLE_BECAUSE(
+            "smt2_convt::parse_literal parsed a number with a decimal point "
+            "in, which cannot be converted to type " +
+            type.id_string());
+        }
+      }
       // Numeral
-      value=string2integer(s);
+      value = string2integer(s);
     }
   }
   else if(src.get_sub().size()==2 &&
@@ -527,6 +549,11 @@ constant_exprt smt2_convt::parse_literal(
   {
     return from_integer(value + to_range_type(type).get_from(), type);
   }
+  else if(type.id() == ID_rational)
+  {
+    // TODO parse this literal back correctly.
+    return from_integer(value, type);
+  }
   else
     UNREACHABLE_BECAUSE(
       "smt2_convt::parse_literal should not be of unsupported type " +
@@ -3167,6 +3194,19 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr)
       convert_typecast(tmp);
     }
   }
+  else if(dest_type.id() == ID_rational)
+  {
+    if(src_type.id() == ID_signedbv)
+    {
+      // TODO: negative numbers
+      out << "(/ ";
+      convert_expr(src);
+      out << " 1)";
+    }
+    else
+      UNEXPECTEDCASE(
+        "Unknown typecast " + src_type.id_string() + " -> rational");
+  }
   else
     UNEXPECTEDCASE(
       "TODO typecast8 "+src_type.id_string()+" -> "+dest_type.id_string());
@@ -3588,7 +3628,10 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
     const bool negative = has_prefix(value, "-");
 
     if(negative)
+    {
       out << "(- ";
+      value = value.substr(1);
+    }
 
     size_t pos=value.find("/");
 
@@ -4190,6 +4233,16 @@ void smt2_convt::convert_div(const div_exprt &expr)
     // the rounding mode.  See smt2_convt::convert_floatbv_div.
     UNREACHABLE;
   }
+  else if(
+    expr.type().id() == ID_rational || expr.type().id() == ID_integer ||
+    expr.type().id() == ID_real)
+  {
+    out << "(/ ";
+    convert_expr(expr.op0());
+    out << " ";
+    convert_expr(expr.op1());
+    out << ")";
+  }
   else
     UNEXPECTEDCASE("unsupported type for /: "+expr.type().id_string());
 }

src/util/arith_tools.cpp

@@ -177,6 +177,10 @@ constant_exprt from_integer(
     ieee_float.from_integer(int_value);
     return ieee_float.to_expr();
   }
+  else if(type_id == ID_rational)
+  {
+    return constant_exprt(integer2string(int_value), type);
+  }
   else
     PRECONDITION(false);
 }

src/util/expr.cpp

@@ -59,8 +59,10 @@ bool exprt::is_zero() const
     {
       rationalt rat_value;
       if(to_rational(*this, rat_value))
-        CHECK_RETURN(false);
-      return rat_value.is_zero();
+      {
+        // CHECK_RETURN(false);
+        return rat_value.is_zero();
+      }
     }
     else if(
       type_id == ID_unsignedbv || type_id == ID_signedbv ||

src/util/pointer_expr.cpp

@@ -26,6 +26,7 @@ unsigned int dynamic_object_exprt::get_instance() const
   return std::stoul(id2string(to_constant_expr(op0()).get_value()));
 }
 
+#include <iostream>
 /// Build an object_descriptor_exprt from a given expr
 static void build_object_descriptor_rec(
   const namespacet &ns,
@@ -39,6 +40,11 @@ static void build_object_descriptor_rec(
     build_object_descriptor_rec(ns, index.array(), dest);
 
     auto sub_size = size_of_expr(expr.type(), ns);
+    if(!sub_size.has_value())
+    {
+      std::cout << "no value for " << id2string(expr.type().id()) << std::endl;
+    }
+    CHECK_RETURN(sub_size.has_value());
 
     if(sub_size.has_value())
     {

src/util/pointer_offset_size.cpp

@@ -488,6 +488,11 @@ std::optional<exprt> size_of_expr(const typet &type, const namespacet &ns)
   {
     return from_integer(32 / config.ansi_c.char_width, size_type());
   }
+  else if(type.id() == ID_rational)
+  {
+    // these shouldn't really have sizes but this will do
+    return from_integer(1, size_type());
+  }
   else
     return {};
 }

src/util/rational_tools.cpp

@@ -29,11 +29,18 @@ bool to_rational(const exprt &expr, rationalt &rational_value)
   if(!expr.is_constant())
     return true;
 
-  const std::string &value=expr.get_string(ID_value);
+  std::string value = expr.get_string(ID_value);
 
   std::string no1, no2;
   char mode=0;
 
+  bool is_negative = false;
+  if(value[0] == '-')
+  {
+    is_negative = true;
+    value = value.substr(1, value.size() - 1);
+  }
+
   for(const char ch : value)
   {
     if(isdigit(ch))
@@ -54,20 +61,23 @@ bool to_rational(const exprt &expr, rationalt &rational_value)
       return true;
   }
 
+  if(is_negative)
+    rational_value = rationalt(-string2integer(no1));
+  else
+    rational_value = rationalt(string2integer(no1));
+
   switch(mode)
   {
   case 0:
-    rational_value=rationalt(string2integer(no1));
+    // do nothing
     break;
 
   case '.':
-    rational_value=rationalt(string2integer(no1));
-    rational_value+=
-      rationalt(string2integer(no2))/rationalt(power10(no2.size()));
+    rational_value +=
+      rationalt(string2integer(no2)) / rationalt(power10(no2.size()));
     break;
 
   case '/':
-    rational_value=rationalt(string2integer(no1));
     rational_value/=rationalt(string2integer(no2));
     break;