Skip to content

Commit 19a8310

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 587e5ef commit 19a8310

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
@@ -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: 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
@@ -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/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
@@ -102,7 +102,7 @@ constant_exprt from_integer(
102102
{
103103
const irep_idt &type_id=type.id();
104104

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

0 commit comments

Comments
 (0)