Fix and demonstrate support for __CPROVER_rational

Author: polgreen

regression/cbmc/rational1/main.c

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

regression/cbmc/rational1/test.desc

@@ -0,0 +1,8 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--trace --smt2
+^\[main.assertion.2\] line 9 should fail: FAILURE$
+^\*\* 1 of 2 failed
+^EXIT=10$
+^SIGNAL=0$
+--

regression/cbmc/rational1/typecheck.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+^[[:space:]]*ASSIGN main::1::x := 3/5
+^[[:space:]]*ASSIGN main::1::y := 3/5
+^EXIT=0$
+^SIGNAL=0$
+--

regression/validate-trace-xml-schema/check.py

@@ -29,6 +29,7 @@
     ['enum_is_in_range', 'enum_test3-simplified.desc'],
     ['enum_is_in_range', 'format.desc'],
     ['r_w_ok9', 'simplify.desc'],
+    ['rational1', 'typecheck.desc'],
     ['reachability-slice-interproc2', 'test.desc'],
     ['saturating_arithmetric', 'output-goto.desc'],
     # this one wants show-properties instead producing a trace

src/ansi-c/c_typecast.cpp

@@ -8,20 +8,22 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "c_typecast.h"
 
-#include <algorithm>
-
 #include <util/arith_tools.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_util.h>
 #include <util/mathematical_types.h>
 #include <util/namespace.h>
 #include <util/pointer_expr.h>
+#include <util/rational.h>
+#include <util/rational_tools.h>
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
 #include "c_qualifiers.h"
 
+#include <algorithm>
+
 bool c_implicit_typecast(
   exprt &expr,
   const typet &dest_type,
@@ -776,6 +778,27 @@ void c_typecastt::do_typecast(exprt &expr, const typet &dest_type)
     {
       expr=is_not_zero(expr, ns);
     }
+    else if(dest_type.id() == ID_rational)
+    {
+      if(auto div_expr = expr_try_dynamic_cast<div_exprt>(expr))
+      {
+        auto op1 = numeric_cast<mp_integer>(div_expr->lhs());
+        auto op2 = numeric_cast<mp_integer>(div_expr->rhs());
+        if(op1.has_value() && op2.has_value())
+        {
+          rationalt numerator{*op1};
+          expr = from_rational(rationalt{*op1} / rationalt{*op2});
+          return;
+        }
+      }
+      else if(auto int_const = numeric_cast<mp_integer>(expr))
+      {
+        expr = from_integer(*int_const, dest_type);
+        return;
+      }
+
+      expr = typecast_exprt(expr, dest_type);
+    }
     else
     {
       expr = typecast_exprt(expr, dest_type);

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>
@@ -430,6 +432,26 @@ constant_exprt smt2_convt::parse_literal(
     }
     else
     {
+      std::size_t pos = s.find(".");
+      if(pos != std::string::npos)
+      {
+        // Decimal, return as rational
+        if(type.id() == ID_rational)
+        {
+          rationalt rational_value;
+          bool failed = to_rational(
+            constant_exprt{src.id(), rational_typet{}}, rational_value);
+          CHECK_RETURN(!failed);
+          return from_rational(rational_value);
+        }
+        else
+        {
+          UNREACHABLE_BECAUSE(
+            "smt2_convt::parse_literal parsed a number with a decimal point "
+            "as type " +
+            type.id_string());
+        }
+      }
       // Numeral
       value=string2integer(s);
     }
@@ -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/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,19 @@ 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);
+  PRECONDITION(!value.empty());
 
   std::string no1, no2;
   char mode=0;
 
+  bool is_negative = false;
+  if(value[0] == '-')
+  {
+    is_negative = true;
+    value = value.substr(1);
+  }
+
   for(const char ch : value)
   {
     if(isdigit(ch))
@@ -54,20 +62,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()));
     break;
 
   case '/':
-    rational_value=rationalt(string2integer(no1));
     rational_value/=rationalt(string2integer(no2));
     break;