Skip to content

Commit e5a11d2

Browse files
tautschnigtautschnig
committed
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.
1 parent 8c229d7 commit e5a11d2

File tree

14 files changed

+183
-53
lines changed

14 files changed

+183
-53
lines changed

‎regression/cbmc/real-assignments1/main.c

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
int main()
2+
{
3+
__CPROVER_real a, b;
4+
a = 0;
5+
b = a;
6+
b++;
7+
b *= 100;
8+
__CPROVER_assert(0, "");
9+
}

‎regression/cbmc/real-assignments1/test.desc

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE smt-backend broken-cprover-smt-backend no-new-smt
2+
main.c
3+
--trace --smt2
4+
^EXIT=10$
5+
^SIGNAL=0$
6+
^ b=100 \(0b1100100\)$
7+
--

‎regression/cbmc/real-assignments1/typecheck.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--show-goto-functions
4+
^[[:space:]]*ASSIGN main::1::b := main::1::b \* cast\(100, ℝ\)$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^[[:space:]]*ASSIGN main::1::b := main::1::b \* 100$

‎src/ansi-c/ansi_c_internal_additions.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,7 +135,9 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
135135
" " CPROVER_PREFIX "ssize_t;\n"
136136
"const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
137137
"typedef void " CPROVER_PREFIX "integer;\n"
138+
"typedef void " CPROVER_PREFIX "natural;\n"
138139
"typedef void " CPROVER_PREFIX "rational;\n"
140+
"typedef void " CPROVER_PREFIX "real;\n"
139141
"extern unsigned char " CPROVER_PREFIX "memory["
140142
CPROVER_PREFIX "constant_infinity_uint];\n"
141143

‎src/ansi-c/c_typecast.cpp

Lines changed: 23 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -102,29 +102,23 @@ bool check_c_implicit_typecast(
102102

103103
if(src_type_id==ID_natural)
104104
{
105-
if(dest_type.id()==ID_bool ||
106-
dest_type.id()==ID_c_bool ||
107-
dest_type.id()==ID_integer ||
108-
dest_type.id()==ID_real ||
109-
dest_type.id()==ID_complex ||
110-
dest_type.id()==ID_unsignedbv ||
111-
dest_type.id()==ID_signedbv ||
112-
dest_type.id()==ID_floatbv ||
113-
dest_type.id()==ID_complex)
105+
if(
106+
dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
107+
dest_type.id() == ID_integer || dest_type.id() == ID_rational ||
108+
dest_type.id() == ID_real || dest_type.id() == ID_complex ||
109+
dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv ||
110+
dest_type.id() == ID_floatbv || dest_type.id() == ID_complex)
114111
return false;
115112
}
116113
else if(src_type_id==ID_integer)
117114
{
118-
if(dest_type.id()==ID_bool ||
119-
dest_type.id()==ID_c_bool ||
120-
dest_type.id()==ID_real ||
121-
dest_type.id()==ID_complex ||
122-
dest_type.id()==ID_unsignedbv ||
123-
dest_type.id()==ID_signedbv ||
124-
dest_type.id()==ID_floatbv ||
125-
dest_type.id()==ID_fixedbv ||
126-
dest_type.id()==ID_pointer ||
127-
dest_type.id()==ID_complex)
115+
if(
116+
dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
117+
dest_type.id() == ID_rational || dest_type.id() == ID_real ||
118+
dest_type.id() == ID_complex || dest_type.id() == ID_unsignedbv ||
119+
dest_type.id() == ID_signedbv || dest_type.id() == ID_floatbv ||
120+
dest_type.id() == ID_fixedbv || dest_type.id() == ID_pointer ||
121+
dest_type.id() == ID_complex)
128122
return false;
129123
}
130124
else if(src_type_id==ID_real)
@@ -139,12 +133,11 @@ bool check_c_implicit_typecast(
139133
}
140134
else if(src_type_id==ID_rational)
141135
{
142-
if(dest_type.id()==ID_bool ||
143-
dest_type.id()==ID_c_bool ||
144-
dest_type.id()==ID_complex ||
145-
dest_type.id()==ID_floatbv ||
146-
dest_type.id()==ID_fixedbv ||
147-
dest_type.id()==ID_complex)
136+
if(
137+
dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
138+
dest_type.id() == ID_real || dest_type.id() == ID_complex ||
139+
dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
140+
dest_type.id() == ID_complex)
148141
return false;
149142
}
150143
else if(src_type_id==ID_bool)
@@ -415,6 +408,8 @@ c_typecastt::c_typet c_typecastt::get_c_type(
415408
}
416409
else if(type.id() == ID_integer)
417410
return INTEGER;
411+
else if(type.id() == ID_natural)
412+
return NATURAL;
418413

419414
return OTHER;
420415
}
@@ -454,6 +449,9 @@ void c_typecastt::implicit_typecast_arithmetic(
454449
case RATIONAL: new_type=rational_typet(); break;
455450
case REAL: new_type=real_typet(); break;
456451
case INTEGER: new_type=integer_typet(); break;
452+
case NATURAL:
453+
new_type = natural_typet();
454+
break;
457455
case COMPLEX:
458456
case OTHER:
459457
case VOIDPTR:

‎src/ansi-c/c_typecast.h

Lines changed: 29 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -75,19 +75,35 @@ class c_typecastt
7575

7676
// these are in promotion order
7777

78-
enum c_typet { BOOL,
79-
CHAR, UCHAR,
80-
SHORT, USHORT,
81-
INT, UINT,
82-
LONG, ULONG,
83-
LONGLONG, ULONGLONG,
84-
LARGE_SIGNED_INT, LARGE_UNSIGNED_INT,
85-
INTEGER, // these are unbounded integers, non-standard
86-
FIXEDBV, // fixed-point, non-standard
87-
SINGLE, DOUBLE, LONGDOUBLE, FLOAT128, // float
88-
RATIONAL, REAL, // infinite precision, non-standard
89-
COMPLEX,
90-
VOIDPTR, PTR, OTHER };
78+
enum c_typet
79+
{
80+
BOOL,
81+
CHAR,
82+
UCHAR,
83+
SHORT,
84+
USHORT,
85+
INT,
86+
UINT,
87+
LONG,
88+
ULONG,
89+
LONGLONG,
90+
ULONGLONG,
91+
LARGE_SIGNED_INT,
92+
LARGE_UNSIGNED_INT,
93+
INTEGER, // these are unbounded integers, non-standard
94+
NATURAL, // these are unbounded natural numbers, non-standard
95+
FIXEDBV, // fixed-point, non-standard
96+
SINGLE,
97+
DOUBLE,
98+
LONGDOUBLE,
99+
FLOAT128, // float
100+
RATIONAL,
101+
REAL, // infinite precision, non-standard
102+
COMPLEX,
103+
VOIDPTR,
104+
PTR,
105+
OTHER
106+
};
91107

92108
c_typet get_c_type(const typet &type) const;
93109

‎src/ansi-c/c_typecheck_type.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1626,6 +1626,14 @@ void c_typecheck_baset::typecheck_typedef_type(typet &type)
16261626
{
16271627
type=integer_typet();
16281628
}
1629+
else if(symbol.base_name == CPROVER_PREFIX "natural")
1630+
{
1631+
type = natural_typet();
1632+
}
1633+
else if(symbol.base_name == CPROVER_PREFIX "real")
1634+
{
1635+
type = real_typet();
1636+
}
16291637
}
16301638

16311639
void c_typecheck_baset::adjust_function_parameter(typet &type) const

‎src/ansi-c/expr2c.cpp

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -246,11 +246,11 @@ std::string expr2ct::convert_rec(
246246
{
247247
return q + CPROVER_PREFIX + "string" + d;
248248
}
249-
else if(src.id()==ID_natural ||
250-
src.id()==ID_integer ||
251-
src.id()==ID_rational)
249+
else if(
250+
src.id() == ID_natural || src.id() == ID_integer ||
251+
src.id() == ID_rational || src.id() == ID_real)
252252
{
253-
return q+src.id_string()+d;
253+
return q + CPROVER_PREFIX + src.id_string() + d;
254254
}
255255
else if(src.id()==ID_empty)
256256
{
@@ -1780,9 +1780,9 @@ std::string expr2ct::convert_constant(
17801780
const irep_idt value=src.get_value();
17811781
std::string dest;
17821782

1783-
if(type.id()==ID_integer ||
1784-
type.id()==ID_natural ||
1785-
type.id()==ID_rational)
1783+
if(
1784+
type.id() == ID_integer || type.id() == ID_natural ||
1785+
type.id() == ID_rational || type.id() == ID_real)
17861786
{
17871787
dest=id2string(value);
17881788
}
@@ -1821,8 +1821,6 @@ std::string expr2ct::convert_constant(
18211821
else
18221822
return "/*enum*/" + value_as_string;
18231823
}
1824-
else if(type.id()==ID_rational)
1825-
return convert_norep(src, precedence);
18261824
else if(type.id()==ID_bv)
18271825
{
18281826
// not C

‎src/util/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ SRC = arith_tools.cpp \
6666
prefix_filter.cpp \
6767
rational.cpp \
6868
rational_tools.cpp \
69+
real.cpp \
6970
ref_expr_set.cpp \
7071
refined_string_type.cpp \
7172
rename.cpp \

‎src/util/arith_tools.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -103,7 +103,7 @@ constant_exprt from_integer(
103103
{
104104
const irep_idt &type_id=type.id();
105105

106-
if(type_id==ID_integer)
106+
if(type_id == ID_integer || type_id == ID_rational || type_id == ID_real)
107107
{
108108
return constant_exprt(integer2string(int_value), type);
109109
}

‎src/util/format_type.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -100,6 +100,8 @@ std::ostream &format_rec(std::ostream &os, const typet &type)
100100
return os << "\xe2\x84\x95"; // u+2115, 'N'
101101
else if(id == ID_rational)
102102
return os << "\xe2\x84\x9a"; // u+211A, 'Q'
103+
else if(id == ID_real)
104+
return os << "\xe2\x84\x9d"; // u+211D, 'R'
103105
else if(id == ID_mathematical_function)
104106
{
105107
const auto &mathematical_function = to_mathematical_function_type(type);

‎src/util/real.cpp

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
/*******************************************************************\
2+
3+
Module: Real Numbers
4+
5+
Author: Michael Tautschnig
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Real Numbers
11+
12+
#include "real.h"
13+
14+
realt &realt::operator-()
15+
{
16+
integral.negate();
17+
return *this;
18+
}
19+
20+
std::ostream &operator<<(std::ostream &out, const realt &a)
21+
{
22+
return out << a.get_integral() << '.' << a.get_fractional();
23+
}

‎src/util/real.h

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,53 @@
1+
/*******************************************************************\
2+
3+
Module: Real Numbers
4+
5+
Author: Michael Tautschnig
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_UTIL_REAL_H
10+
#define CPROVER_UTIL_REAL_H
11+
12+
#include "mp_arith.h"
13+
14+
class realt
15+
{
16+
protected:
17+
mp_integer integral, fractional;
18+
19+
public:
20+
// constructors
21+
realt() : integral(0), fractional(0)
22+
{
23+
}
24+
explicit realt(const mp_integer &i) : integral(i), fractional(0)
25+
{
26+
}
27+
28+
realt &operator-();
29+
30+
bool operator==(const realt &n) const
31+
{
32+
return integral == n.integral && fractional == n.fractional;
33+
}
34+
35+
bool operator!=(const realt &n) const
36+
{
37+
return integral != n.integral || fractional != n.fractional;
38+
}
39+
40+
const mp_integer &get_integral() const
41+
{
42+
return integral;
43+
}
44+
45+
const mp_integer &get_fractional() const
46+
{
47+
return fractional;
48+
}
49+
};
50+
51+
std::ostream &operator<<(std::ostream &out, const realt &a);
52+
53+
#endif // CPROVER_UTIL_REAL_H

‎src/util/simplify_expr.cpp

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1035,11 +1035,11 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
10351035
return make_boolean_expr(int_value != 0);
10361036
}
10371037

1038-
if(expr_type_id==ID_unsignedbv ||
1039-
expr_type_id==ID_signedbv ||
1040-
expr_type_id==ID_c_enum ||
1041-
expr_type_id==ID_c_bit_field ||
1042-
expr_type_id==ID_integer)
1038+
if(
1039+
expr_type_id == ID_unsignedbv || expr_type_id == ID_signedbv ||
1040+
expr_type_id == ID_c_enum || expr_type_id == ID_c_bit_field ||
1041+
expr_type_id == ID_integer || expr_type_id == ID_natural ||
1042+
expr_type_id == ID_rational || expr_type_id == ID_real)
10431043
{
10441044
return from_integer(int_value, expr_type);
10451045
}
@@ -1189,6 +1189,11 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
11891189
rationalt r(int_value);
11901190
return from_rational(r);
11911191
}
1192+
1193+
if(expr_type_id == ID_real)
1194+
{
1195+
return from_integer(int_value, expr_type);
1196+
}
11921197
}
11931198
else if(op_type_id==ID_fixedbv)
11941199
{

0 commit comments

Comments
 (0)