Skip to content

Commit 74c89b3

Browse files
author
Remi Delmas
committed
CONTRACTS: Add __CPROVER_frees clauses
Add the following to the front-end: - add `__CPROVER_frees` clause for function contracts - add `__CPROVER_freeable` built-in function - add `__CPROVER_is_freeable` built-in predicate - add `__CPROVER_is_freed` built-in predicate Effective support for the new clause type and related predicates will come in a later PR.
1 parent af8e924 commit 74c89b3

File tree

40 files changed

+622
-42
lines changed

40 files changed

+622
-42
lines changed

doc/cprover-manual/contracts-frees.md

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
[CPROVER Manual TOC](../../)
2+
3+
# Frees Clauses
4+
5+
A _frees clause_ allows the user to specify a set of pointers that may be freed
6+
by a function. A function contract may have zero or more frees clauses.
7+
When no clause is provided the empty set is used as default.
8+
When more than one frees clause is given, the sets of pointers they contain are
9+
unioned together to yield a single set of pointers.
10+
11+
## Syntax
12+
13+
The clause has the following syntax:
14+
```c
15+
__CPROVER_frees(targets)
16+
```
17+
18+
Where `targets` has the following syntax:
19+
```
20+
targets ::= cond-target-group (';' cond-target-group)* ';'?
21+
cond-target-group ::= (condition ':')? target (',' target)*
22+
target ::= lvalue-expr
23+
| __CPROVER_freeable(lvalue-expr)
24+
```
25+
26+
A frees clause target must be eiter:
27+
- an lvalue expression with a pointer type,
28+
- a call to the built-in function `__CPROVER_freeable`
29+
- a call to a user-defined side effect free and deterministic function returning
30+
the type `void` (itself containing direct or indirect calls to
31+
`__CPROVER_freeable` or to functions that call `__CPROVER_freeable`);
32+
33+
### Example
34+
35+
```c
36+
int foo(char *arr1, char *arr2, size_t size)
37+
__CPROVER_frees(
38+
// `arr1` is freeable only if the condition `size > 0 && arr1` holds
39+
size > 0 && arr1: arr1;
40+
41+
// `arr2` is always freeable
42+
arr2;
43+
)
44+
{
45+
if(size > 0 && arr1)
46+
free(arr1);
47+
free(arr2);
48+
return 0;
49+
}
50+
```
51+
52+
## Semantics
53+
54+
The set of pointers specified by the frees clause of the contract is interpreted
55+
at the function call-site.
56+
57+
### For contract checking
58+
59+
When checking a contract against a function, each pointer that the
60+
function attempts to free gets checked for membership in the set of
61+
pointers specified by the _frees clause_.
62+
63+
### For replacement of function calls by contracts
64+
65+
When replacing a function call by a contract, each pointer of the
66+
_frees clause_ is non-deterministically freed after the function call.
67+
68+
## Specifying parametric sets of freeable pointers using C functions
69+
70+
Users can define parametric sets of freeable pointers by writing functions that
71+
return the built-in type void and call the built-in function
72+
`__CPROVER_freeable` (directly or indirectly through some other user-defined
73+
function):
74+
75+
```c
76+
void my_freeable_set(char **arr, size_t size)
77+
{
78+
// The first 3 pointers are freeable
79+
// if the array is at least of size 3.
80+
if (arr && size > 3) {
81+
__CPROVER_freeable(arr[0]);
82+
__CPROVER_freeable(arr[1]);
83+
__CPROVER_freeable(arr[2]);
84+
}
85+
}
86+
```
87+
88+
The built-in function:
89+
```c
90+
void __CPROVER_freeable(void *ptr);
91+
```
92+
adds the given pointer to the freeable set described by the enclosing function.
93+
94+
Calls to such functions can be used as targets in `__CPROVER_frees` clauses:
95+
```c
96+
void my_function(char **arr, size_t size)
97+
__CPROVER_frees(my_freeable_set(arr, size))
98+
{
99+
...
100+
}
101+
```
102+
103+
## Frees clause related predicates
104+
105+
The predicate:
106+
```c
107+
__CPROVER_bool __CPROVER_is_freeable(void *ptr);
108+
```
109+
can only be used in pre and post conditions, in contract checking or replacement
110+
modes. It returns `true` if and only if the pointer satisfies the preconditions
111+
of the `free` function from `stdlib.h`
112+
([see here](https://github.com/diffblue/cbmc/blob/cf00a53bbcc388748be9668f393276f6d84b1a60/src/ansi-c/library/stdlib.c#L269)),
113+
that is if and only if the pointer points to a valid dynamically allocated object and has offset zero.
114+
115+
The predicate:
116+
```c
117+
__CPROVER_bool __CPROVER_is_freed(void *ptr);
118+
```
119+
can only be used in post conditions and returns `true` if and only if the
120+
pointer was freed during the execution of the function under analysis.

regression/contracts/assigns_enforce_address_of/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
6+
^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
77
^CONVERSION ERROR$
88
--
99
--

regression/contracts/assigns_enforce_conditional_non_lvalue_target/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--enforce-contract foo
4-
^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
4+
^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
55
^CONVERSION ERROR
66
^EXIT=(1|64)$
77
^SIGNAL=0$

regression/contracts/assigns_enforce_conditional_non_lvalue_target_list/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
main.c
33
--enforce-contract foo
4-
^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
4+
^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
55
^CONVERSION ERROR
66
^EXIT=(1|64)$
77
^SIGNAL=0$

regression/contracts/assigns_enforce_function_calls/main.c

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,5 +13,4 @@ int main()
1313
{
1414
int x;
1515
foo(&x);
16-
baz(&x);
1716
}

regression/contracts/assigns_enforce_function_calls/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
6+
^.*error: expecting void return type for function 'bar' called in assigns clause$
77
^CONVERSION ERROR$
88
--
99
--
10-
Check that function call expressions are rejected in assigns clauses.
10+
Check that non-void function call expressions are rejected in assigns clauses.
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
void bar(int *x)
2+
{
3+
if(x)
4+
__CPROVER_typed_target(x);
5+
}
6+
7+
int foo(int *x) __CPROVER_assigns(bar(x))
8+
{
9+
*x = 0;
10+
return 0;
11+
}
12+
13+
int main()
14+
{
15+
int x;
16+
foo(&x);
17+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
CORE
2+
main.c
3+
--enforce-contract foo
4+
^call to function 'bar' in assigns clause not supported yet$
5+
^EXIT=(127|134)$
6+
^SIGNAL=0$
7+
--
8+
--
9+
Check that void function call expressions in assigns clauses make
10+
instrumentation fail.

regression/contracts/assigns_enforce_literal/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
6+
^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
77
^CONVERSION ERROR$
88
--
99
--

regression/contracts/assigns_enforce_side_effects_2/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--enforce-contract foo
44
^EXIT=(1|64)$
55
^SIGNAL=0$
6-
^.*error: assigns clause target must be a non-void lvalue or a call to one of __CPROVER_POINTER_OBJECT, __CPROVER_assignable, __CPROVER_object_whole, __CPROVER_object_upto, __CPROVER_object_from$
6+
^.*error: assigns clause target must be a non-void lvalue, a call to __CPROVER_POINTER_OBJECT or a call to a function returning void$
77
^CONVERSION ERROR$
88
--
99
--

0 commit comments

Comments
 (0)