Skip to content

Commit 34b8cbe

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 34b8cbe

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
}

0 commit comments

Comments
 (0)