Skip to content

Commit cebcc43

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 b471b78 commit cebcc43

File tree

18 files changed

+292
-99
lines changed

18 files changed

+292
-99
lines changed

‎regression/cbmc/rational1/test.desc‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,8 @@ CORE smt-backend broken-cprover-smt-backend no-new-smt
22
main.c
33
--trace --smt2
44
^\[main.assertion.2\] line 9 should fail: FAILURE$
5+
^\s*x=3/5
6+
^\s*y=3/5
57
^\*\* 1 of 2 failed
68
^EXIT=10$
79
^SIGNAL=0$

‎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
@@ -144,7 +144,9 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
144144
" " CPROVER_PREFIX "ssize_t;\n"
145145
"const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
146146
"typedef void " CPROVER_PREFIX "integer;\n"
147+
"typedef void " CPROVER_PREFIX "natural;\n"
147148
"typedef void " CPROVER_PREFIX "rational;\n"
149+
"typedef void " CPROVER_PREFIX "real;\n"
148150
"extern unsigned char " CPROVER_PREFIX "memory["
149151
CPROVER_PREFIX "constant_infinity_uint];\n"
150152

‎src/ansi-c/c_typecast.cpp‎

Lines changed: 49 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -104,30 +104,28 @@ bool check_c_implicit_typecast(
104104

105105
if(src_type_id==ID_natural)
106106
{
107-
if(dest_type.id()==ID_bool ||
108-
dest_type.id()==ID_c_bool ||
109-
dest_type.id()==ID_integer ||
110-
dest_type.id()==ID_real ||
111-
dest_type.id()==ID_complex ||
112-
dest_type.id()==ID_unsignedbv ||
113-
dest_type.id()==ID_signedbv ||
114-
dest_type.id()==ID_floatbv ||
115-
dest_type.id()==ID_complex)
107+
if(
108+
dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
109+
dest_type.id() == ID_integer || dest_type.id() == ID_rational ||
110+
dest_type.id() == ID_real || dest_type.id() == ID_complex ||
111+
dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv ||
112+
dest_type.id() == ID_floatbv || dest_type.id() == ID_complex)
113+
{
116114
return false;
115+
}
117116
}
118117
else if(src_type_id==ID_integer)
119118
{
120-
if(dest_type.id()==ID_bool ||
121-
dest_type.id()==ID_c_bool ||
122-
dest_type.id()==ID_real ||
123-
dest_type.id()==ID_complex ||
124-
dest_type.id()==ID_unsignedbv ||
125-
dest_type.id()==ID_signedbv ||
126-
dest_type.id()==ID_floatbv ||
127-
dest_type.id()==ID_fixedbv ||
128-
dest_type.id()==ID_pointer ||
129-
dest_type.id()==ID_complex)
119+
if(
120+
dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
121+
dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
122+
dest_type.id() == ID_real || dest_type.id() == ID_complex ||
123+
dest_type.id() == ID_unsignedbv || dest_type.id() == ID_signedbv ||
124+
dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
125+
dest_type.id() == ID_pointer || dest_type.id() == ID_complex)
126+
{
130127
return false;
128+
}
131129
}
132130
else if(src_type_id==ID_real)
133131
{
@@ -141,49 +139,46 @@ bool check_c_implicit_typecast(
141139
}
142140
else if(src_type_id==ID_rational)
143141
{
144-
if(dest_type.id()==ID_bool ||
145-
dest_type.id()==ID_c_bool ||
146-
dest_type.id()==ID_complex ||
147-
dest_type.id()==ID_floatbv ||
148-
dest_type.id()==ID_fixedbv ||
149-
dest_type.id()==ID_complex)
142+
if(
143+
dest_type.id() == ID_bool || dest_type.id() == ID_c_bool ||
144+
dest_type.id() == ID_real || dest_type.id() == ID_complex ||
145+
dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
146+
dest_type.id() == ID_complex)
147+
{
150148
return false;
149+
}
151150
}
152151
else if(src_type_id==ID_bool)
153152
{
154-
if(dest_type.id()==ID_c_bool ||
155-
dest_type.id()==ID_integer ||
156-
dest_type.id()==ID_real ||
157-
dest_type.id()==ID_unsignedbv ||
158-
dest_type.id()==ID_signedbv ||
159-
dest_type.id()==ID_pointer ||
160-
dest_type.id()==ID_floatbv ||
161-
dest_type.id()==ID_fixedbv ||
162-
dest_type.id()==ID_c_enum ||
163-
dest_type.id()==ID_c_enum_tag ||
164-
dest_type.id()==ID_complex)
153+
if(
154+
dest_type.id() == ID_c_bool || dest_type.id() == ID_integer ||
155+
dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
156+
dest_type.id() == ID_real || dest_type.id() == ID_unsignedbv ||
157+
dest_type.id() == ID_signedbv || dest_type.id() == ID_pointer ||
158+
dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
159+
dest_type.id() == ID_c_enum || dest_type.id() == ID_c_enum_tag ||
160+
dest_type.id() == ID_complex)
161+
{
165162
return false;
163+
}
166164
}
167165
else if(src_type_id==ID_unsignedbv ||
168166
src_type_id==ID_signedbv ||
169167
src_type_id==ID_c_enum ||
170168
src_type_id==ID_c_enum_tag ||
171169
src_type_id==ID_c_bool)
172170
{
173-
if(dest_type.id()==ID_unsignedbv ||
174-
dest_type.id()==ID_bool ||
175-
dest_type.id()==ID_c_bool ||
176-
dest_type.id()==ID_integer ||
177-
dest_type.id()==ID_real ||
178-
dest_type.id()==ID_rational ||
179-
dest_type.id()==ID_signedbv ||
180-
dest_type.id()==ID_floatbv ||
181-
dest_type.id()==ID_fixedbv ||
182-
dest_type.id()==ID_pointer ||
183-
dest_type.id()==ID_c_enum ||
184-
dest_type.id()==ID_c_enum_tag ||
185-
dest_type.id()==ID_complex)
171+
if(
172+
dest_type.id() == ID_unsignedbv || dest_type.id() == ID_bool ||
173+
dest_type.id() == ID_c_bool || dest_type.id() == ID_integer ||
174+
dest_type.id() == ID_natural || dest_type.id() == ID_rational ||
175+
dest_type.id() == ID_real || dest_type.id() == ID_signedbv ||
176+
dest_type.id() == ID_floatbv || dest_type.id() == ID_fixedbv ||
177+
dest_type.id() == ID_pointer || dest_type.id() == ID_c_enum ||
178+
dest_type.id() == ID_c_enum_tag || dest_type.id() == ID_complex)
179+
{
186180
return false;
181+
}
187182
}
188183
else if(src_type_id==ID_floatbv ||
189184
src_type_id==ID_fixedbv)
@@ -417,6 +412,8 @@ c_typecastt::c_typet c_typecastt::get_c_type(
417412
}
418413
else if(type.id() == ID_integer)
419414
return INTEGER;
415+
else if(type.id() == ID_natural)
416+
return NATURAL;
420417

421418
return OTHER;
422419
}
@@ -456,6 +453,9 @@ void c_typecastt::implicit_typecast_arithmetic(
456453
case RATIONAL: new_type=rational_typet(); break;
457454
case REAL: new_type=real_typet(); break;
458455
case INTEGER: new_type=integer_typet(); break;
456+
case NATURAL:
457+
new_type = natural_typet();
458+
break;
459459
case COMPLEX:
460460
case OTHER:
461461
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, // infinite precision, non-standard
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
@@ -1686,6 +1686,14 @@ void c_typecheck_baset::typecheck_typedef_type(typet &type)
16861686
{
16871687
type=integer_typet();
16881688
}
1689+
else if(symbol.base_name == CPROVER_PREFIX "natural")
1690+
{
1691+
type = natural_typet();
1692+
}
1693+
else if(symbol.base_name == CPROVER_PREFIX "real")
1694+
{
1695+
type = real_typet();
1696+
}
16891697
}
16901698

16911699
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
@@ -245,11 +245,11 @@ std::string expr2ct::convert_rec(
245245
{
246246
return q + CPROVER_PREFIX + "string" + d;
247247
}
248-
else if(src.id()==ID_natural ||
249-
src.id()==ID_integer ||
250-
src.id()==ID_rational)
248+
else if(
249+
src.id() == ID_natural || src.id() == ID_integer ||
250+
src.id() == ID_rational || src.id() == ID_real)
251251
{
252-
return q+src.id_string()+d;
252+
return q + CPROVER_PREFIX + src.id_string() + d;
253253
}
254254
else if(src.id()==ID_empty)
255255
{
@@ -1796,9 +1796,9 @@ std::string expr2ct::convert_constant(
17961796
const irep_idt value=src.get_value();
17971797
std::string dest;
17981798

1799-
if(type.id()==ID_integer ||
1800-
type.id()==ID_natural ||
1801-
type.id()==ID_rational)
1799+
if(
1800+
type.id() == ID_integer || type.id() == ID_natural ||
1801+
type.id() == ID_rational || type.id() == ID_real)
18021802
{
18031803
dest=id2string(value);
18041804
}
@@ -1837,8 +1837,6 @@ std::string expr2ct::convert_constant(
18371837
else
18381838
return "/*enum*/" + value_as_string;
18391839
}
1840-
else if(type.id()==ID_rational)
1841-
return convert_norep(src, precedence);
18421840
else if(type.id()==ID_bv)
18431841
{
18441842
// used for _BitInt

‎src/solvers/flattening/boolbv_width.cpp‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -206,8 +206,12 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
206206
{
207207
cache_entry = defined_entryt{0};
208208
}
209-
else if(type_id == ID_rational)
209+
else if(
210+
type_id == ID_rational || type_id == ID_real || type_id == ID_integer ||
211+
type_id == ID_natural)
210212
{
213+
// these have unbounded width, but we warn about this elsewhere and
214+
// shouldn't fail in get_entry
211215
cache_entry = defined_entryt{1};
212216
}
213217
else

0 commit comments

Comments
 (0)