Skip to content

Commit b683850

Browse files
tautschnigtautschnig
committed
Make CPROVER intrinsics proper prototypes
Forward declarations without arguments are deprecated in C. Polymorphic built-ins now have dummy declarations that are only in effect when running library checks. Our own C front-end will type check them properly and won't rely on forward declarations.
1 parent 4c967ad commit b683850

File tree

3 files changed

+110
-92
lines changed

3 files changed

+110
-92
lines changed

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 78 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -2118,6 +2118,77 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
21182118

21192119
return;
21202120
}
2121+
else if(identifier == CPROVER_PREFIX "equal")
2122+
{
2123+
if(expr.arguments().size() != 2)
2124+
{
2125+
error().source_location = f_op.source_location();
2126+
error() << "equal expects two operands" << eom;
2127+
throw 0;
2128+
}
2129+
2130+
equal_exprt equality_expr(
2131+
expr.arguments().front(), expr.arguments().back());
2132+
equality_expr.add_source_location() = expr.source_location();
2133+
2134+
if(equality_expr.lhs().type() != equality_expr.rhs().type())
2135+
{
2136+
error().source_location = f_op.source_location();
2137+
error() << "equal expects two operands of same type" << eom;
2138+
throw 0;
2139+
}
2140+
2141+
expr.swap(equality_expr);
2142+
return;
2143+
}
2144+
else if(
2145+
identifier == CPROVER_PREFIX "overflow_minus" ||
2146+
identifier == CPROVER_PREFIX "overflow_mult" ||
2147+
identifier == CPROVER_PREFIX "overflow_plus" ||
2148+
identifier == CPROVER_PREFIX "overflow_shl")
2149+
{
2150+
exprt overflow{identifier, typet{}, exprt::operandst{expr.arguments()}};
2151+
overflow.add_source_location() = f_op.source_location();
2152+
2153+
if(identifier == CPROVER_PREFIX "overflow_minus")
2154+
{
2155+
overflow.id(ID_minus);
2156+
typecheck_expr_binary_arithmetic(overflow);
2157+
}
2158+
else if(identifier == CPROVER_PREFIX "overflow_mult")
2159+
{
2160+
overflow.id(ID_mult);
2161+
typecheck_expr_binary_arithmetic(overflow);
2162+
}
2163+
else if(identifier == CPROVER_PREFIX "overflow_plus")
2164+
{
2165+
overflow.id(ID_plus);
2166+
typecheck_expr_binary_arithmetic(overflow);
2167+
}
2168+
else if(identifier == CPROVER_PREFIX "overflow_shl")
2169+
{
2170+
overflow.id(ID_shl);
2171+
typecheck_expr_shifts(to_shift_expr(overflow));
2172+
}
2173+
2174+
binary_overflow_exprt of{
2175+
overflow.operands()[0], overflow.id(), overflow.operands()[1]};
2176+
of.add_source_location() = overflow.source_location();
2177+
expr.swap(of);
2178+
return;
2179+
}
2180+
else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
2181+
{
2182+
exprt tmp{ID_unary_minus, typet{}, exprt::operandst{expr.arguments()}};
2183+
tmp.add_source_location() = f_op.source_location();
2184+
2185+
typecheck_expr_unary_arithmetic(tmp);
2186+
2187+
unary_minus_overflow_exprt overflow{tmp.operands().front()};
2188+
overflow.add_source_location() = tmp.source_location();
2189+
expr.swap(overflow);
2190+
return;
2191+
}
21212192
else if(identifier == CPROVER_PREFIX "enum_is_in_range")
21222193
{
21232194
// Check correct number of arguments
@@ -2563,11 +2634,15 @@ exprt c_typecheck_baset::do_special_functions(
25632634

25642635
typecheck_function_call_arguments(expr);
25652636

2637+
exprt::operandst args_no_cast;
2638+
args_no_cast.reserve(expr.arguments().size());
25662639
for(const auto &argument : expr.arguments())
25672640
{
2641+
args_no_cast.push_back(skip_typecast(argument));
25682642
if(
2569-
argument.type().id() != ID_pointer ||
2570-
to_pointer_type(argument.type()).base_type().id() != ID_struct_tag)
2643+
args_no_cast.back().type().id() != ID_pointer ||
2644+
to_pointer_type(args_no_cast.back().type()).base_type().id() !=
2645+
ID_struct_tag)
25712646
{
25722647
error().source_location = expr.arguments()[0].source_location();
25732648
error() << "is_sentinel_dll_node expects struct-pointer operands"
@@ -2577,7 +2652,7 @@ exprt c_typecheck_baset::do_special_functions(
25772652
}
25782653

25792654
predicate_exprt is_sentinel_dll_expr("is_sentinel_dll");
2580-
is_sentinel_dll_expr.operands() = expr.arguments();
2655+
is_sentinel_dll_expr.operands() = args_no_cast;
25812656
is_sentinel_dll_expr.add_source_location() = source_location;
25822657

25832658
return std::move(is_sentinel_dll_expr);
@@ -3353,30 +3428,6 @@ exprt c_typecheck_baset::do_special_functions(
33533428

33543429
return std::move(ffs);
33553430
}
3356-
else if(identifier==CPROVER_PREFIX "equal")
3357-
{
3358-
if(expr.arguments().size()!=2)
3359-
{
3360-
error().source_location = f_op.source_location();
3361-
error() << "equal expects two operands" << eom;
3362-
throw 0;
3363-
}
3364-
3365-
typecheck_function_call_arguments(expr);
3366-
3367-
equal_exprt equality_expr(
3368-
expr.arguments().front(), expr.arguments().back());
3369-
equality_expr.add_source_location()=source_location;
3370-
3371-
if(equality_expr.lhs().type() != equality_expr.rhs().type())
3372-
{
3373-
error().source_location = f_op.source_location();
3374-
error() << "equal expects two operands of same type" << eom;
3375-
throw 0;
3376-
}
3377-
3378-
return std::move(equality_expr);
3379-
}
33803431
else if(identifier=="__builtin_expect")
33813432
{
33823433
// This is a gcc extension to provide branch prediction.
@@ -3562,52 +3613,6 @@ exprt c_typecheck_baset::do_special_functions(
35623613

35633614
return tmp;
35643615
}
3565-
else if(
3566-
identifier == CPROVER_PREFIX "overflow_minus" ||
3567-
identifier == CPROVER_PREFIX "overflow_mult" ||
3568-
identifier == CPROVER_PREFIX "overflow_plus" ||
3569-
identifier == CPROVER_PREFIX "overflow_shl")
3570-
{
3571-
exprt overflow{identifier, typet{}, exprt::operandst{expr.arguments()}};
3572-
overflow.add_source_location() = f_op.source_location();
3573-
3574-
if(identifier == CPROVER_PREFIX "overflow_minus")
3575-
{
3576-
overflow.id(ID_minus);
3577-
typecheck_expr_binary_arithmetic(overflow);
3578-
}
3579-
else if(identifier == CPROVER_PREFIX "overflow_mult")
3580-
{
3581-
overflow.id(ID_mult);
3582-
typecheck_expr_binary_arithmetic(overflow);
3583-
}
3584-
else if(identifier == CPROVER_PREFIX "overflow_plus")
3585-
{
3586-
overflow.id(ID_plus);
3587-
typecheck_expr_binary_arithmetic(overflow);
3588-
}
3589-
else if(identifier == CPROVER_PREFIX "overflow_shl")
3590-
{
3591-
overflow.id(ID_shl);
3592-
typecheck_expr_shifts(to_shift_expr(overflow));
3593-
}
3594-
3595-
binary_overflow_exprt of{
3596-
overflow.operands()[0], overflow.id(), overflow.operands()[1]};
3597-
of.add_source_location() = overflow.source_location();
3598-
return std::move(of);
3599-
}
3600-
else if(identifier == CPROVER_PREFIX "overflow_unary_minus")
3601-
{
3602-
exprt tmp{ID_unary_minus, typet{}, exprt::operandst{expr.arguments()}};
3603-
tmp.add_source_location() = f_op.source_location();
3604-
3605-
typecheck_expr_unary_arithmetic(tmp);
3606-
3607-
unary_minus_overflow_exprt overflow{tmp.operands().front()};
3608-
overflow.add_source_location() = tmp.source_location();
3609-
return std::move(overflow);
3610-
}
36113616
else if(
36123617
identifier == "__builtin_add_overflow" ||
36133618
identifier == "__builtin_sadd_overflow" ||

‎src/ansi-c/cprover_builtin_headers.h

Lines changed: 7 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -6,21 +6,17 @@ void __CPROVER_precondition(__CPROVER_bool precondition, const char *description
66
void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
77
void __CPROVER_havoc_object(void *);
88
void __CPROVER_havoc_slice(void *, __CPROVER_size_t);
9-
__CPROVER_bool __CPROVER_equal();
109
__CPROVER_bool __CPROVER_same_object(const void *, const void *);
1110
__CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
1211
_Bool __CPROVER_is_zero_string(const void *);
1312
__CPROVER_size_t __CPROVER_zero_string_length(const void *);
1413
__CPROVER_size_t __CPROVER_buffer_size(const void *);
15-
__CPROVER_bool __CPROVER_r_ok();
16-
__CPROVER_bool __CPROVER_w_ok();
17-
__CPROVER_bool __CPROVER_rw_ok();
1814

1915
// experimental features for CHC encodings -- do not use
20-
__CPROVER_bool __CPROVER_is_list(); // a singly-linked null-terminated dynamically-allocated list
21-
__CPROVER_bool __CPROVER_is_dll();
22-
__CPROVER_bool __CPROVER_is_cyclic_dll();
23-
__CPROVER_bool __CPROVER_is_sentinel_dll();
16+
__CPROVER_bool __CPROVER_is_list(const void *); // a singly-linked null-terminated dynamically-allocated list
17+
__CPROVER_bool __CPROVER_is_dll(const void *);
18+
__CPROVER_bool __CPROVER_is_cyclic_dll(const void *);
19+
__CPROVER_bool __CPROVER_is_sentinel_dll(const void *, ...);
2420
__CPROVER_bool __CPROVER_is_cstring(const char *);
2521
__CPROVER_size_t __CPROVER_cstrlen(const char *);
2622
__CPROVER_bool __CPROVER_separate(const void *, const void *, ...);
@@ -41,8 +37,8 @@ void __CPROVER_output(const char *id, ...);
4137
void __CPROVER_cover(__CPROVER_bool condition);
4238

4339
// concurrency-related
44-
void __CPROVER_atomic_begin();
45-
void __CPROVER_atomic_end();
40+
void __CPROVER_atomic_begin(void);
41+
void __CPROVER_atomic_end(void);
4642
void __CPROVER_fence(const char *kind, ...);
4743

4844
// contract-related functions
@@ -124,19 +120,11 @@ void __CPROVER_array_replace(const void *dest, const void *src);
124120
void __CPROVER_array_set(const void *dest, ...);
125121

126122
// k-induction
127-
void __CPROVER_k_induction_hint(unsigned min, unsigned max,
128-
unsigned step, unsigned loop_free);
123+
void __CPROVER_k_induction_hint(unsigned min, unsigned max, unsigned step, unsigned loop_free);
129124

130125
// format string-related
131126
int __CPROVER_scanf(const char *, ...);
132127

133-
// detect overflow
134-
__CPROVER_bool __CPROVER_overflow_minus();
135-
__CPROVER_bool __CPROVER_overflow_mult();
136-
__CPROVER_bool __CPROVER_overflow_plus();
137-
__CPROVER_bool __CPROVER_overflow_shl();
138-
__CPROVER_bool __CPROVER_overflow_unary_minus();
139-
140128
// contracts
141129
void __CPROVER_assignable(void *ptr, __CPROVER_size_t size,
142130
__CPROVER_bool is_ptr_to_ptr);

‎src/ansi-c/library/cprover.h

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,10 +40,35 @@ struct __CPROVER_pipet {
4040
short next_unread;
4141
};
4242

43+
// __CPROVER_equal expects two arguments of the same type -- any type is
44+
// permitted, unsigned long long is just used for the benefit of running syntax
45+
// checks using system compilers
46+
__CPROVER_bool __CPROVER_equal(unsigned long long, unsigned long long);
47+
48+
// The following built-ins are type checked by our C front-end and do not
49+
// require declarations. They work with any types as described below. unsigned
50+
// long long is just used to enable checks using system compilers.
51+
52+
// detect overflow
53+
// the following expect two numeric arguments
54+
__CPROVER_bool __CPROVER_overflow_minus(unsigned long long, unsigned long long);
55+
__CPROVER_bool __CPROVER_overflow_mult(unsigned long long, unsigned long long);
56+
__CPROVER_bool __CPROVER_overflow_plus(unsigned long long, unsigned long long);
57+
__CPROVER_bool __CPROVER_overflow_shl(unsigned long long, unsigned long long);
58+
// expects one numeric argument
59+
__CPROVER_bool __CPROVER_overflow_unary_minus(unsigned long long);
60+
4361
// enumerations
4462
// expects one enum-typed argument
4563
__CPROVER_bool __CPROVER_enum_is_in_range(unsigned long long);
4664

65+
// The following have an optional second parameter (the width), and are
66+
// polymorphic in the first parameter: if the second argument is omitted, then
67+
// the width of the subtype of the pointer-typed first argument is used.
68+
__CPROVER_bool __CPROVER_r_ok(const void *, ...);
69+
__CPROVER_bool __CPROVER_w_ok(const void *, ...);
70+
__CPROVER_bool __CPROVER_rw_ok(const void *, ...);
71+
4772
#include "../cprover_builtin_headers.h"
4873

4974
#endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H

0 commit comments

Comments
 (0)