From 8691c5af381d1b2d6a812266304a53757fe82950 Mon Sep 17 00:00:00 2001 From: Elizabeth Polgreen Date: Tue, 8 Oct 2024 16:48:14 +0100 Subject: [PATCH 1/2] Fix and demonstrate support for __CPROVER_rational --- regression/cbmc/rational1/main.c | 10 ++++ regression/cbmc/rational1/test.desc | 8 +++ regression/cbmc/rational1/typecheck.desc | 8 +++ regression/validate-trace-xml-schema/check.py | 1 + src/ansi-c/c_typecast.cpp | 27 +++++++++- src/solvers/flattening/boolbv_width.cpp | 4 ++ src/solvers/smt2/smt2_conv.cpp | 53 +++++++++++++++++++ src/util/arith_tools.cpp | 4 ++ src/util/pointer_offset_size.cpp | 5 ++ src/util/rational_tools.cpp | 19 +++++-- 10 files changed, 133 insertions(+), 6 deletions(-) create mode 100644 regression/cbmc/rational1/main.c create mode 100644 regression/cbmc/rational1/test.desc create mode 100644 regression/cbmc/rational1/typecheck.desc diff --git a/regression/cbmc/rational1/main.c b/regression/cbmc/rational1/main.c new file mode 100644 index 00000000000..2c4766de72d --- /dev/null +++ b/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"); +} diff --git a/regression/cbmc/rational1/test.desc b/regression/cbmc/rational1/test.desc new file mode 100644 index 00000000000..45aaa49c8cf --- /dev/null +++ b/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$ +-- diff --git a/regression/cbmc/rational1/typecheck.desc b/regression/cbmc/rational1/typecheck.desc new file mode 100644 index 00000000000..a35e97d54ba --- /dev/null +++ b/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$ +-- diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index d544778fc37..f284d760b16 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/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 diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index 873e857af8f..685299d38df 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -8,8 +8,6 @@ Author: Daniel Kroening, kroening@kroening.com #include "c_typecast.h" -#include - #include #include #include @@ -17,11 +15,15 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include #include #include #include "c_qualifiers.h" +#include + 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(expr)) + { + auto op1 = numeric_cast(div_expr->lhs()); + auto op2 = numeric_cast(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(expr)) + { + expr = from_integer(*int_const, dest_type); + return; + } + + expr = typecast_exprt(expr, dest_type); + } else { expr = typecast_exprt(expr, dest_type); diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index 41885c469c8..afc2596ca69 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/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( diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index 80a9b973847..a4891dc516b 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -29,6 +29,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include +#include #include #include #include @@ -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()); } diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index 7d40b77b60d..d8a518228ff 100644 --- a/src/util/arith_tools.cpp +++ b/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); } diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 9e60faf8047..b4062e8a93e 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -488,6 +488,11 @@ std::optional 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 {}; } diff --git a/src/util/rational_tools.cpp b/src/util/rational_tools.cpp index 8806ba35017..637e015b35a 100644 --- a/src/util/rational_tools.cpp +++ b/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; From fb0495e10ba535bcd125546d9c0a6fb8770eb9c8 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 11 Jun 2024 19:44:12 +0000 Subject: [PATCH 2/2] Fix support for mathematical types We were missing front-end support for reals and did not consistently support all of integers, naturals, rationals, reals but instead would only handle varying subsets in each place. --- regression/cbmc/rational1/test.desc | 2 + regression/cbmc/real-assignments1/main.c | 9 ++ regression/cbmc/real-assignments1/test.desc | 7 ++ .../cbmc/real-assignments1/typecheck.desc | 8 ++ regression/cbmc/real-irrational1/main.c | 6 ++ regression/cbmc/real-irrational1/test.desc | 11 +++ regression/validate-trace-xml-schema/check.py | 1 + src/ansi-c/ansi_c_internal_additions.cpp | 2 + src/ansi-c/c_typecast.cpp | 98 +++++++++---------- src/ansi-c/c_typecast.h | 42 +++++--- src/ansi-c/c_typecheck_type.cpp | 8 ++ src/ansi-c/expr2c.cpp | 16 ++- src/solvers/flattening/boolbv_width.cpp | 6 +- src/solvers/smt2/smt2_conv.cpp | 82 +++++++++++----- src/util/Makefile | 1 + src/util/arith_tools.cpp | 2 +- src/util/format_expr.cpp | 6 +- src/util/format_type.cpp | 2 + src/util/real.cpp | 33 +++++++ src/util/real.h | 62 ++++++++++++ src/util/simplify_expr.cpp | 15 ++- 21 files changed, 315 insertions(+), 104 deletions(-) create mode 100644 regression/cbmc/real-assignments1/main.c create mode 100644 regression/cbmc/real-assignments1/test.desc create mode 100644 regression/cbmc/real-assignments1/typecheck.desc create mode 100644 regression/cbmc/real-irrational1/main.c create mode 100644 regression/cbmc/real-irrational1/test.desc create mode 100644 src/util/real.cpp create mode 100644 src/util/real.h diff --git a/regression/cbmc/rational1/test.desc b/regression/cbmc/rational1/test.desc index 45aaa49c8cf..11083ff19a1 100644 --- a/regression/cbmc/rational1/test.desc +++ b/regression/cbmc/rational1/test.desc @@ -2,6 +2,8 @@ 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$ diff --git a/regression/cbmc/real-assignments1/main.c b/regression/cbmc/real-assignments1/main.c new file mode 100644 index 00000000000..36101d3b4e0 --- /dev/null +++ b/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, ""); +} diff --git a/regression/cbmc/real-assignments1/test.desc b/regression/cbmc/real-assignments1/test.desc new file mode 100644 index 00000000000..8ccdf3ca863 --- /dev/null +++ b/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 +-- diff --git a/regression/cbmc/real-assignments1/typecheck.desc b/regression/cbmc/real-assignments1/typecheck.desc new file mode 100644 index 00000000000..c06ed82f381 --- /dev/null +++ b/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$ diff --git a/regression/cbmc/real-irrational1/main.c b/regression/cbmc/real-irrational1/main.c new file mode 100644 index 00000000000..40cadc3cd6f --- /dev/null +++ b/regression/cbmc/real-irrational1/main.c @@ -0,0 +1,6 @@ +int main() +{ + __CPROVER_real a; + __CPROVER_real a2 = a * a; + __CPROVER_assert(a2 != 2, ""); +} diff --git a/regression/cbmc/real-irrational1/test.desc b/regression/cbmc/real-irrational1/test.desc new file mode 100644 index 00000000000..ec7cf51433e --- /dev/null +++ b/regression/cbmc/real-irrational1/test.desc @@ -0,0 +1,11 @@ +KNOWNBUG +main.c +--trace --smt2 +^EXIT=10$ +^SIGNAL=0$ +-- +-- +This currently fails an invariant in parse_literal, but really requires +adjusting the implementation of realt to be coefficients of a polynomial. We can +then parse, e.g., (root-obj (+ (^ x 2) (- 2)) 1), which Z3 returns as part of +the model. diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py index f284d760b16..9b77df11c50 100644 --- a/regression/validate-trace-xml-schema/check.py +++ b/regression/validate-trace-xml-schema/check.py @@ -31,6 +31,7 @@ ['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'], diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 0f0e11c759a..14d7cf52a9c 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/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" diff --git a/src/ansi-c/c_typecast.cpp b/src/ansi-c/c_typecast.cpp index 685299d38df..ea6a13848cd 100644 --- a/src/ansi-c/c_typecast.cpp +++ b/src/ansi-c/c_typecast.cpp @@ -104,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) { @@ -141,28 +139,28 @@ 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 || @@ -170,20 +168,17 @@ bool check_c_implicit_typecast( 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) @@ -417,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; } @@ -456,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: diff --git a/src/ansi-c/c_typecast.h b/src/ansi-c/c_typecast.h index 9585d99b7cb..ab06f04df60 100644 --- a/src/ansi-c/c_typecast.h +++ b/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; diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp index d80669f5f42..6de21fe222d 100644 --- a/src/ansi-c/c_typecheck_type.cpp +++ b/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 diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 6cf0f170abc..796466a1390 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -245,11 +245,11 @@ std::string expr2ct::convert_rec( { return q + CPROVER_PREFIX + "string" + d; } - else if(src.id()==ID_natural || - src.id()==ID_integer || - src.id()==ID_rational) + else if( + src.id() == ID_natural || src.id() == ID_integer || + src.id() == ID_rational || src.id() == ID_real) { - return q+src.id_string()+d; + return q + CPROVER_PREFIX + src.id_string() + d; } else if(src.id()==ID_empty) { @@ -1796,9 +1796,9 @@ std::string expr2ct::convert_constant( const irep_idt value=src.get_value(); std::string dest; - if(type.id()==ID_integer || - type.id()==ID_natural || - type.id()==ID_rational) + if( + type.id() == ID_integer || type.id() == ID_natural || + type.id() == ID_rational || type.id() == ID_real) { dest=id2string(value); } @@ -1837,8 +1837,6 @@ std::string expr2ct::convert_constant( else return "/*enum*/" + value_as_string; } - else if(type.id()==ID_rational) - return convert_norep(src, precedence); else if(type.id()==ID_bv) { // used for _BitInt diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp index afc2596ca69..998312fd37e 100644 --- a/src/solvers/flattening/boolbv_width.cpp +++ b/src/solvers/flattening/boolbv_width.cpp @@ -206,8 +206,12 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const { cache_entry = defined_entryt{0}; } - else if(type_id == ID_rational) + else if( + type_id == ID_rational || type_id == ID_real || type_id == ID_integer || + type_id == ID_natural) { + // these have unbounded width, but we warn about this elsewhere and + // shouldn't fail in get_entry cache_entry = defined_entryt{1}; } else diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index a4891dc516b..b78ae63a25a 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -31,6 +31,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include #include @@ -435,7 +436,7 @@ constant_exprt smt2_convt::parse_literal( std::size_t pos = s.find("."); if(pos != std::string::npos) { - // Decimal, return as rational + // Decimal, return as rational or real if(type.id() == ID_rational) { rationalt rational_value; @@ -444,6 +445,13 @@ constant_exprt smt2_convt::parse_literal( CHECK_RETURN(!failed); return from_rational(rational_value); } + else if(type.id() == ID_real) + { + mp_integer first = string2integer(s.substr(0, pos)); + mp_integer second = string2integer(s.substr(pos, std::string::npos)); + realt real{first, second}; + return real.as_expr(); + } else { UNREACHABLE_BECAUSE( @@ -468,6 +476,18 @@ constant_exprt smt2_convt::parse_literal( { value=string2integer(src.get_sub()[1].id_string().substr(2)); } + else if( + type.id() == ID_rational && src.get_sub().size() == 3 && + src.get_sub()[0].id() == "/") + { + rationalt numerator; + rationalt denominator; + bool failed = + to_rational(parse_literal(src.get_sub()[1], type), numerator) || + to_rational(parse_literal(src.get_sub()[2], type), denominator); + CHECK_RETURN(!failed); + return from_rational(numerator / denominator); + } else if(src.get_sub().size()==4 && src.get_sub()[0].id()=="fp") // (fp signbv exponentbv significandbv) { @@ -541,7 +561,7 @@ constant_exprt smt2_convt::parse_literal( std::size_t width=boolbv_width(type); return constant_exprt(integer2bvrep(value, width), type); } - else if(type.id() == ID_integer) + else if(type.id() == ID_integer || type.id() == ID_natural) { return from_integer(value, type); } @@ -549,11 +569,6 @@ 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 " + @@ -753,7 +768,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &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_c_enum || + type.id() == ID_natural || type.id() == ID_real || type.id() == ID_c_enum || type.id() == ID_c_enum_tag || type.id() == ID_fixedbv || type.id() == ID_floatbv || type.id() == ID_c_bool || type.id() == ID_range) { @@ -1386,6 +1401,7 @@ void smt2_convt::convert_expr(const exprt &expr) } else { + PRECONDITION(type.id() != ID_natural); out << "(bvneg "; convert_expr(unary_minus_expr.op()); out << ")"; @@ -2672,12 +2688,12 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) if(dest_type.id()==ID_bool) { // this is comparison with zero - if(src_type.id()==ID_signedbv || - src_type.id()==ID_unsignedbv || - src_type.id()==ID_c_bool || - src_type.id()==ID_fixedbv || - src_type.id()==ID_pointer || - src_type.id()==ID_integer) + if( + src_type.id() == ID_signedbv || src_type.id() == ID_unsignedbv || + src_type.id() == ID_c_bool || src_type.id() == ID_fixedbv || + src_type.id() == ID_pointer || src_type.id() == ID_integer || + src_type.id() == ID_natural || src_type.id() == ID_rational || + src_type.id() == ID_real) { out << "(not (= "; convert_expr(src); @@ -2874,9 +2890,9 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) out << ")"; } } - else if(src_type.id()==ID_integer) // from integer to bit-vector + else if(src_type.id() == ID_integer || src_type.id() == ID_natural) { - // must be constant + // from integer to bit-vector, must be constant if(src.is_constant()) { mp_integer i = numeric_cast_v(to_constant_expr(src)); @@ -3169,7 +3185,7 @@ void smt2_convt::convert_typecast(const typecast_exprt &expr) else UNEXPECTEDCASE("Unknown typecast "+src_type.id_string()+" -> float"); } - else if(dest_type.id()==ID_integer) + else if(dest_type.id() == ID_integer || dest_type.id() == ID_natural) { if(src_type.id()==ID_bool) { @@ -3646,6 +3662,13 @@ void smt2_convt::convert_constant(const constant_exprt &expr) if(negative) out << ')'; } + else if(expr_type.id() == ID_real) + { + const std::string &value = id2string(expr.get_value()); + out << value; + if(value.find('.') == std::string::npos) + out << ".0"; + } else if(expr_type.id()==ID_integer) { const auto value = id2string(expr.get_value()); @@ -3656,6 +3679,10 @@ void smt2_convt::convert_constant(const constant_exprt &expr) else out << value; } + else if(expr_type.id() == ID_natural) + { + out << expr.get_value(); + } else if(expr_type.id() == ID_range) { auto &range_type = to_range_type(expr_type); @@ -3807,8 +3834,9 @@ void smt2_convt::convert_relation(const binary_relation_exprt &expr) else convert_floatbv(expr); } - else if(op_type.id()==ID_rational || - op_type.id()==ID_integer) + else if( + op_type.id() == ID_rational || op_type.id() == ID_integer || + op_type.id() == ID_natural || op_type.id() == ID_real) { out << "("; out << expr.id(); @@ -3853,7 +3881,7 @@ void smt2_convt::convert_plus(const plus_exprt &expr) { if( expr.type().id() == ID_rational || expr.type().id() == ID_integer || - expr.type().id() == ID_real) + expr.type().id() == ID_natural || expr.type().id() == ID_real) { // these are multi-ary in SMT-LIB2 out << "(+"; @@ -4080,7 +4108,9 @@ void smt2_convt::convert_floatbv_plus(const ieee_float_op_exprt &expr) void smt2_convt::convert_minus(const minus_exprt &expr) { - if(expr.type().id()==ID_integer) + if( + expr.type().id() == ID_integer || expr.type().id() == ID_natural || + expr.type().id() == ID_rational || expr.type().id() == ID_real) { out << "(- "; convert_expr(expr.op0()); @@ -4235,7 +4265,7 @@ void smt2_convt::convert_div(const div_exprt &expr) } else if( expr.type().id() == ID_rational || expr.type().id() == ID_integer || - expr.type().id() == ID_real) + expr.type().id() == ID_natural || expr.type().id() == ID_real) { out << "(/ "; convert_expr(expr.op0()); @@ -4324,9 +4354,9 @@ void smt2_convt::convert_mult(const mult_exprt &expr) out << "))"; // bvmul, extract } - else if(expr.type().id()==ID_rational || - expr.type().id()==ID_integer || - expr.type().id()==ID_real) + else if( + expr.type().id() == ID_rational || expr.type().id() == ID_integer || + expr.type().id() == ID_natural || expr.type().id() == ID_real) { out << "(*"; @@ -5859,6 +5889,8 @@ void smt2_convt::convert_type(const typet &type) out << "Real"; else if(type.id()==ID_integer) out << "Int"; + else if(type.id() == ID_natural) + out << "Nat"; else if(type.id()==ID_complex) { if(use_datatypes) diff --git a/src/util/Makefile b/src/util/Makefile index 1e33ebc73db..44d5d307fd9 100644 --- a/src/util/Makefile +++ b/src/util/Makefile @@ -66,6 +66,7 @@ SRC = arith_tools.cpp \ prefix_filter.cpp \ rational.cpp \ rational_tools.cpp \ + real.cpp \ ref_expr_set.cpp \ refined_string_type.cpp \ rename.cpp \ diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp index d8a518228ff..fff5eac4d4e 100644 --- a/src/util/arith_tools.cpp +++ b/src/util/arith_tools.cpp @@ -102,7 +102,7 @@ constant_exprt from_integer( { const irep_idt &type_id=type.id(); - if(type_id==ID_integer) + if(type_id == ID_integer || type_id == ID_rational || type_id == ID_real) { return constant_exprt(integer2string(int_value), type); } diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp index 55118640c91..90d56372e60 100644 --- a/src/util/format_expr.cpp +++ b/src/util/format_expr.cpp @@ -202,8 +202,12 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src) result += ']'; return os << result; } - else if(type == ID_integer || type == ID_natural || type == ID_range) + else if( + type == ID_integer || type == ID_natural || type == ID_rational || + type == ID_real || type == ID_range) + { return os << src.get_value(); + } else if(type == ID_string) return os << '"' << escape(id2string(src.get_value())) << '"'; else if(type == ID_floatbv) diff --git a/src/util/format_type.cpp b/src/util/format_type.cpp index f2b495521c5..394ef7ca7ac 100644 --- a/src/util/format_type.cpp +++ b/src/util/format_type.cpp @@ -106,6 +106,8 @@ std::ostream &format_rec(std::ostream &os, const typet &type) } else if(id == ID_rational) return os << "\xe2\x84\x9a"; // u+211A, 'Q' + else if(id == ID_real) + return os << "\xe2\x84\x9d"; // u+211D, 'R' else if(id == ID_mathematical_function) { const auto &mathematical_function = to_mathematical_function_type(type); diff --git a/src/util/real.cpp b/src/util/real.cpp new file mode 100644 index 00000000000..8dbd74018e5 --- /dev/null +++ b/src/util/real.cpp @@ -0,0 +1,33 @@ +/*******************************************************************\ + +Module: Real Numbers + +Author: Michael Tautschnig + +\*******************************************************************/ + +/// \file +/// Real Numbers + +#include "real.h" + +#include "mathematical_types.h" + +constant_exprt realt::as_expr() const +{ + std::string d = integer2string(integral); + if(fractional != 0) + d += "." + integer2string(fractional); + return constant_exprt(d, real_typet()); +} + +realt &realt::operator-() +{ + integral.negate(); + return *this; +} + +std::ostream &operator<<(std::ostream &out, const realt &a) +{ + return out << a.get_integral() << '.' << a.get_fractional(); +} diff --git a/src/util/real.h b/src/util/real.h new file mode 100644 index 00000000000..9d55866aa32 --- /dev/null +++ b/src/util/real.h @@ -0,0 +1,62 @@ +/*******************************************************************\ + +Module: Real Numbers + +Author: Michael Tautschnig + +\*******************************************************************/ + +#ifndef CPROVER_UTIL_REAL_H +#define CPROVER_UTIL_REAL_H + +#include "mp_arith.h" +#include "std_expr.h" + +class realt +{ +protected: + // TODO: we will eventually need to move to a list of coefficients (of a + // polynomial) to be able to represent irrational numbers. See also the + // KNOWNBUG test cbmc/real-irrational1. + mp_integer integral, fractional; + +public: + // constructors + realt() : integral(0), fractional(0) + { + } + realt(const mp_integer &i, const mp_integer &f) : integral(i), fractional(f) + { + } + explicit realt(const mp_integer &i) : realt(i, 0) + { + } + + constant_exprt as_expr() const; + + realt &operator-(); + + bool operator==(const realt &n) const + { + return integral == n.integral && fractional == n.fractional; + } + + bool operator!=(const realt &n) const + { + return integral != n.integral || fractional != n.fractional; + } + + const mp_integer &get_integral() const + { + return integral; + } + + const mp_integer &get_fractional() const + { + return fractional; + } +}; + +std::ostream &operator<<(std::ostream &out, const realt &a); + +#endif // CPROVER_UTIL_REAL_H diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index c21b0d28250..3538ca3234f 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -1036,11 +1036,11 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) return make_boolean_expr(int_value != 0); } - if(expr_type_id==ID_unsignedbv || - expr_type_id==ID_signedbv || - expr_type_id==ID_c_enum || - expr_type_id==ID_c_bit_field || - expr_type_id==ID_integer) + if( + expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv || + expr_type_id == ID_c_enum || expr_type_id == ID_c_bit_field || + expr_type_id == ID_integer || expr_type_id == ID_natural || + expr_type_id == ID_rational || expr_type_id == ID_real) { return from_integer(int_value, expr_type); } @@ -1191,6 +1191,11 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) rationalt r(int_value); return from_rational(r); } + + if(expr_type_id == ID_real) + { + return from_integer(int_value, expr_type); + } } else if(op_type_id==ID_fixedbv) {