Fix support for mathematical types

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,10 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--trace --smt2
+^\[main.assertion.2\] line 9 should fail: FAILURE$
+^\s*x=3/5
+^\s*y=3/5
+^\*\* 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/cbmc/real-assignments1/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  __CPROVER_real a, b;
+  a = 0;
+  b = a;
+  b++;
+  b *= 100;
+  __CPROVER_assert(0, "");
+}

regression/cbmc/real-assignments1/test.desc

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

regression/cbmc/real-assignments1/typecheck.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--show-goto-functions
+^[[:space:]]*ASSIGN main::1::b := main::1::b \* cast\(100, ℝ\)$
+^EXIT=0$
+^SIGNAL=0$
+--
+^[[:space:]]*ASSIGN main::1::b := main::1::b \* 100$

regression/cbmc/real-irrational1/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  __CPROVER_real a;
+  __CPROVER_real a2 = a * a;
+  __CPROVER_assert(a2 != 2, "");
+}

regression/cbmc/real-irrational1/test.desc

@@ -0,0 +1,8 @@
+CORE smt-backend broken-cprover-smt-backend no-new-smt
+main.c
+--trace --smt2
+^  a=x ∈ ℝ\.\(x\^2 \+ -2 = 0\)
+^EXIT=10$
+^SIGNAL=0$
+--
+--

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

@@ -29,7 +29,9 @@
     ['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'],
+    ['real-assignments1', 'typecheck.desc'],
     ['saturating_arithmetric', 'output-goto.desc'],
     # this one wants show-properties instead producing a trace
     ['show_properties1', 'test.desc'],
@@ -80,7 +82,9 @@
     ['integer-assignments1', 'test.desc'],
     # this test is expected to abort, thus producing invalid XML
     ['String_Abstraction17', 'test.desc'],
-    ['Quantifiers1', 'quantifier-with-side-effect.desc']
+    ['Quantifiers1', 'quantifier-with-side-effect.desc'],
+    # this test produces unicode output that cannot be decoded as ASCII
+    ['real-irrational1', 'test.desc']
 ]))
 
 # TODO maybe consider looking them up on PATH, but direct paths are

src/ansi-c/ansi_c_internal_additions.cpp

@@ -144,7 +144,9 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
       " " CPROVER_PREFIX "ssize_t;\n"
     "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
     "typedef void " CPROVER_PREFIX "integer;\n"
+    "typedef void " CPROVER_PREFIX "natural;\n"
     "typedef void " CPROVER_PREFIX "rational;\n"
+    "typedef void " CPROVER_PREFIX "real;\n"
     "extern unsigned char " CPROVER_PREFIX "memory["
       CPROVER_PREFIX "constant_infinity_uint];\n"
 

src/ansi-c/c_typecast.cpp

@@ -8,20 +8,22 @@ Author: Daniel Kroening, [email protected]
 
 #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,
@@ -102,30 +104,28 @@ bool check_c_implicit_typecast(
 
   if(src_type_id==ID_natural)
   {
-    if(dest_type.id()==ID_bool ||
-       dest_type.id()==ID_c_bool ||
-       dest_type.id()==ID_integer ||
-       dest_type.id()==ID_real ||
-       dest_type.id()==ID_complex ||
-       dest_type.id()==ID_unsignedbv ||
-       dest_type.id()==ID_signedbv ||
-       dest_type.id()==ID_floatbv ||
-       dest_type.id()==ID_complex)
+    if(
+      dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
+      dest_type.id() == ID_integer || dest_type.id() == ID_rational ||
+      dest_type.id() == ID_real || dest_type.id() == ID_complex ||
+      dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv ||
+      dest_type.id() == ID_floatbv || dest_type.id() == ID_complex)
+    {
       return false;
+    }
   }
   else if(src_type_id==ID_integer)
   {
-    if(dest_type.id()==ID_bool ||
-       dest_type.id()==ID_c_bool ||
-       dest_type.id()==ID_real ||
-       dest_type.id()==ID_complex ||
-       dest_type.id()==ID_unsignedbv ||
-       dest_type.id()==ID_signedbv ||
-       dest_type.id()==ID_floatbv ||
-       dest_type.id()==ID_fixedbv ||
-       dest_type.id()==ID_pointer ||
-       dest_type.id()==ID_complex)
+    if(
+      dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
+      dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
+      dest_type.id() == ID_real || dest_type.id() == ID_complex ||
+      dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv ||
+      dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
+      dest_type.id() == ID_pointer || dest_type.id() == ID_complex)
+    {
       return false;
+    }
   }
   else if(src_type_id==ID_real)
   {
@@ -139,49 +139,46 @@ bool check_c_implicit_typecast(
   }
   else if(src_type_id==ID_rational)
   {
-    if(dest_type.id()==ID_bool ||
-       dest_type.id()==ID_c_bool ||
-       dest_type.id()==ID_complex ||
-       dest_type.id()==ID_floatbv ||
-       dest_type.id()==ID_fixedbv ||
-       dest_type.id()==ID_complex)
+    if(
+      dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
+      dest_type.id() == ID_real || dest_type.id() == ID_complex ||
+      dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
+      dest_type.id() == ID_complex)
+    {
       return false;
+    }
   }
   else if(src_type_id==ID_bool)
   {
-    if(dest_type.id()==ID_c_bool ||
-       dest_type.id()==ID_integer ||
-       dest_type.id()==ID_real ||
-       dest_type.id()==ID_unsignedbv ||
-       dest_type.id()==ID_signedbv ||
-       dest_type.id()==ID_pointer ||
-       dest_type.id()==ID_floatbv ||
-       dest_type.id()==ID_fixedbv ||
-       dest_type.id()==ID_c_enum ||
-       dest_type.id()==ID_c_enum_tag ||
-       dest_type.id()==ID_complex)
+    if(
+      dest_type.id() == ID_c_bool || dest_type.id() == ID_integer ||
+      dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
+      dest_type.id() == ID_real || dest_type.id() == ID_unsignedbv ||
+      dest_type.id() == ID_signedbv || dest_type.id() == ID_pointer ||
+      dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
+      dest_type.id() == ID_c_enum || dest_type.id() == ID_c_enum_tag ||
+      dest_type.id() == ID_complex)
+    {
       return false;
+    }
   }
   else if(src_type_id==ID_unsignedbv ||
           src_type_id==ID_signedbv ||
           src_type_id==ID_c_enum ||
           src_type_id==ID_c_enum_tag ||
           src_type_id==ID_c_bool)
   {
-    if(dest_type.id()==ID_unsignedbv ||
-       dest_type.id()==ID_bool ||
-       dest_type.id()==ID_c_bool ||
-       dest_type.id()==ID_integer ||
-       dest_type.id()==ID_real ||
-       dest_type.id()==ID_rational ||
-       dest_type.id()==ID_signedbv ||
-       dest_type.id()==ID_floatbv ||
-       dest_type.id()==ID_fixedbv ||
-       dest_type.id()==ID_pointer ||
-       dest_type.id()==ID_c_enum ||
-       dest_type.id()==ID_c_enum_tag ||
-       dest_type.id()==ID_complex)
+    if(
+      dest_type.id() == ID_unsignedbv || dest_type.id() == ID_bool ||
+      dest_type.id() == ID_c_bool || dest_type.id() == ID_integer ||
+      dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
+      dest_type.id() == ID_real || dest_type.id() == ID_signedbv ||
+      dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
+      dest_type.id() == ID_pointer || dest_type.id() == ID_c_enum ||
+      dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_complex)
+    {
       return false;
+    }
   }
   else if(src_type_id==ID_floatbv ||
           src_type_id==ID_fixedbv)
@@ -415,6 +412,8 @@ c_typecastt::c_typet c_typecastt::get_c_type(
   }
   else if(type.id() == ID_integer)
     return INTEGER;
+  else if(type.id() == ID_natural)
+    return NATURAL;
 
   return OTHER;
 }
@@ -454,6 +453,9 @@ void c_typecastt::implicit_typecast_arithmetic(
   case RATIONAL:   new_type=rational_typet(); break;
   case REAL:       new_type=real_typet(); break;
   case INTEGER:    new_type=integer_typet(); break;
+  case NATURAL:
+    new_type = natural_typet();
+    break;
   case COMPLEX:
   case OTHER:
   case VOIDPTR:
@@ -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/ansi-c/c_typecast.h

@@ -75,19 +75,35 @@ class c_typecastt
 
   // these are in promotion order
 
-  enum c_typet { BOOL,
-                 CHAR, UCHAR,
-                 SHORT, USHORT,
-                 INT, UINT,
-                 LONG, ULONG,
-                 LONGLONG, ULONGLONG,
-                 LARGE_SIGNED_INT, LARGE_UNSIGNED_INT,
-                 INTEGER, // these are unbounded integers, non-standard
-                 FIXEDBV, // fixed-point, non-standard
-                 SINGLE, DOUBLE, LONGDOUBLE, FLOAT128, // float
-                 RATIONAL, REAL, // infinite precision, non-standard
-                 COMPLEX,
-                 VOIDPTR, PTR, OTHER };
+  enum c_typet
+  {
+    BOOL,
+    CHAR,
+    UCHAR,
+    SHORT,
+    USHORT,
+    INT,
+    UINT,
+    LONG,
+    ULONG,
+    LONGLONG,
+    ULONGLONG,
+    LARGE_SIGNED_INT,
+    LARGE_UNSIGNED_INT,
+    INTEGER, // these are unbounded integers, non-standard
+    NATURAL, // these are unbounded natural numbers, non-standard
+    FIXEDBV, // fixed-point, non-standard
+    SINGLE,
+    DOUBLE,
+    LONGDOUBLE,
+    FLOAT128, // float
+    RATIONAL, // infinite precision, non-standard
+    REAL,     // infinite precision, non-standard
+    COMPLEX,
+    VOIDPTR,
+    PTR,
+    OTHER
+  };
 
   c_typet get_c_type(const typet &type) const;
 

src/ansi-c/c_typecheck_type.cpp

@@ -1686,6 +1686,14 @@ void c_typecheck_baset::typecheck_typedef_type(typet &type)
   {
     type=integer_typet();
   }
+  else if(symbol.base_name == CPROVER_PREFIX "natural")
+  {
+    type = natural_typet();
+  }
+  else if(symbol.base_name == CPROVER_PREFIX "real")
+  {
+    type = real_typet();
+  }
 }
 
 void c_typecheck_baset::adjust_function_parameter(typet &type) const