Skip to content

Commit 62a0609

Browse files
author
Remi Delmas
committed
CONTRACTS: Front-end: frees clause improvements
Add the following to the front-end: - add `__CPROVER_freeable_t` built-in type - add `__CPROVER_freeable` built-in function - allow calls to `__CPROVER_freeable_t` functions in frees clauses - add `__CPROVER_is_freeable` built-in predicate - add `__CPROVER_is_freed` built-in predicate The predicates are not yet supported in the back-end.
1 parent d53d826 commit 62a0609

File tree

17 files changed

+327
-4
lines changed

17 files changed

+327
-4
lines changed

‎doc/cprover-manual/contracts-frees.md‎

Lines changed: 56 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,3 +78,59 @@ When replacing a function call or a loop by a contract, each pointer of the
7878
_frees_ clause is non-deterministically freed after the function call
7979
or after the loop.
8080

81+
# Using functions to specify parametric sets of freeable pointers
82+
83+
Users can define parametric sets of freeable pointers by writing functions that
84+
return the built-in type `__CPROVER_freeable_t` and call the built-in function
85+
`__CPROVER_freeable` or any user-defined function returning
86+
`__CPROVER_freeable_t`:
87+
88+
```c
89+
__CPROVER_freeable_t my_freeable_set(char **arr, size_t size)
90+
{
91+
if (arr && size > 3) {
92+
__CPROVER_freeable(arr[0]);
93+
__CPROVER_freeable(arr[1]);
94+
__CPROVER_freeable(arr[2]);
95+
}
96+
}
97+
```
98+
99+
The built-in function:
100+
101+
```c
102+
__CPROVER_freeable_t __CPROVER_freeable(void *ptr);
103+
```
104+
adds the given pointer to the freeable set described by the enclosing function.
105+
106+
Calls to functions returning `__CPROVER_freeable_t` can then be used as targets
107+
in `__CPROVER_frees` clauses:
108+
109+
```c
110+
void my_function(char **arr, size_t size)
111+
__CPROVER_frees(my_freeable_set(arr, size))
112+
{
113+
...
114+
}
115+
```
116+
117+
# Frees clause related predicates
118+
119+
The predicate:
120+
121+
```c
122+
__CPROVER_bool __CPROVER_is_freeable(void *ptr);
123+
```
124+
can only be used in pre and post conditions, in contract checking or replacement
125+
modes. It returns `true` if and only if the pointer satisfies the preconditions
126+
of the `free` function from `stdlib.h`, that is if and only if the pointer
127+
points to a valid dynamically allocated object and has offset zero.
128+
129+
The predicate:
130+
131+
```c
132+
__CPROVER_bool __CPROVER_is_freed(void *ptr);
133+
```
134+
can only be used in post conditions and returns `true` if and only if the
135+
pointer was freed during the execution of the function or the loop under
136+
analysis.

‎regression/contracts/frees-clause-and-predicates-fail/main.c‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
#include <stdlib.h>
2+
3+
// A function defining a conditionally freeable target
4+
__CPROVER_freeable_t
5+
foo_frees(char *arr, const size_t size, const size_t new_size)
6+
{
7+
__CPROVER_freeable(arr);
8+
}
9+
10+
char *foo(char *arr, const size_t size, const size_t new_size)
11+
// clang-format off
12+
// error is_freed cannot be used in preconditions
13+
__CPROVER_requires(!__CPROVER_is_freed(arr))
14+
__CPROVER_requires(__CPROVER_is_freeable(arr))
15+
__CPROVER_assigns(__CPROVER_whole_object(arr))
16+
__CPROVER_frees(foo_frees(arr, size, new_size))
17+
__CPROVER_ensures(
18+
(arr && new_size > size) ==>
19+
__CPROVER_is_fresh(__CPROVER_return_value, new_size))
20+
__CPROVER_ensures(
21+
(arr && new_size > size) ==>
22+
__CPROVER_is_freed(__CPROVER_old(arr)))
23+
__CPROVER_ensures(
24+
!(arr && new_size > size) ==>
25+
__CPROVER_return_value == __CPROVER_old(arr))
26+
// clang-format on
27+
{
28+
if(arr && new_size > size)
29+
{
30+
free(arr);
31+
return malloc(new_size);
32+
}
33+
else
34+
{
35+
return arr;
36+
}
37+
}
38+
39+
int main()
40+
{
41+
size_t size;
42+
size_t new_size;
43+
char *arr = malloc(size);
44+
arr = foo(arr, size, new_size);
45+
return 0;
46+
}

‎regression/contracts/frees-clause-and-predicates-fail/test.desc‎

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+
^main.c.* error: __CPROVER_is_freed is not allowed in preconditions.$
5+
^CONVERSION ERROR$
6+
^EXIT=(1|64)$
7+
^SIGNAL=0$
8+
--
9+
--
10+
This test checks that the front end rejects __CPROVER_is_freed in preconditions.

‎regression/contracts/frees-clause-and-predicates-fail2/main.c‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
#include <stdlib.h>
2+
3+
// A function defining a conditionally freeable target
4+
void
5+
foo_frees(char *arr, const size_t size, const size_t new_size)
6+
{
7+
__CPROVER_freeable(arr);
8+
}
9+
10+
char *foo(char *arr, const size_t size, const size_t new_size)
11+
// clang-format off
12+
__CPROVER_requires(__CPROVER_is_freeable(arr))
13+
__CPROVER_assigns(__CPROVER_whole_object(arr))
14+
__CPROVER_frees(foo_frees(arr, size, new_size))
15+
__CPROVER_ensures(
16+
(arr && new_size > size) ==>
17+
__CPROVER_is_fresh(__CPROVER_return_value, new_size))
18+
__CPROVER_ensures(
19+
(arr && new_size > size) ==>
20+
__CPROVER_is_freed(__CPROVER_old(arr)))
21+
__CPROVER_ensures(
22+
!(arr && new_size > size) ==>
23+
__CPROVER_return_value == __CPROVER_old(arr))
24+
// clang-format on
25+
{
26+
if(arr && new_size > size)
27+
{
28+
free(arr);
29+
return malloc(new_size);
30+
}
31+
else
32+
{
33+
return arr;
34+
}
35+
}
36+
37+
int main()
38+
{
39+
size_t size;
40+
size_t new_size;
41+
char *arr = malloc(size);
42+
arr = foo(arr, size, new_size);
43+
return 0;
44+
}

‎regression/contracts/frees-clause-and-predicates-fail2/test.desc‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--enforce-contract foo
4+
^main.c.* error: expecting __CPROVER_freeable_t return type for function foo_frees called in frees clause$
5+
^CONVERSION ERROR$
6+
^EXIT=(1|64)$
7+
^SIGNAL=0$
8+
--
9+
--
10+
This test checks that the front-end rejects non-__CPROVER_freeable_t-typed
11+
function calls in frees clauses.

‎regression/contracts/frees-clause-and-predicates/main.c‎

Lines changed: 44 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,44 @@
1+
#include <stdlib.h>
2+
3+
// A function defining a conditionally freeable target
4+
__CPROVER_freeable_t
5+
foo_frees(char *arr, const size_t size, const size_t new_size)
6+
{
7+
__CPROVER_freeable(arr);
8+
}
9+
10+
char *foo(char *arr, const size_t size, const size_t new_size)
11+
// clang-format off
12+
__CPROVER_requires(__CPROVER_is_freeable(arr))
13+
__CPROVER_assigns(__CPROVER_whole_object(arr))
14+
__CPROVER_frees(foo_frees(arr, size, new_size))
15+
__CPROVER_ensures(
16+
(arr && new_size > size) ==>
17+
__CPROVER_is_fresh(__CPROVER_return_value, new_size))
18+
__CPROVER_ensures(
19+
(arr && new_size > size) ==>
20+
__CPROVER_is_freed(__CPROVER_old(arr)))
21+
__CPROVER_ensures(
22+
!(arr && new_size > size) ==>
23+
__CPROVER_return_value == __CPROVER_old(arr))
24+
// clang-format on
25+
{
26+
if(arr && new_size > size)
27+
{
28+
free(arr);
29+
return malloc(new_size);
30+
}
31+
else
32+
{
33+
return arr;
34+
}
35+
}
36+
37+
int main()
38+
{
39+
size_t size;
40+
size_t new_size;
41+
char *arr = malloc(size);
42+
arr = foo(arr, size, new_size);
43+
return 0;
44+
}

‎regression/contracts/frees-clause-and-predicates/test.desc‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
CORE
2+
main.c
3+
--enforce-contract foo
4+
^\[foo.postcondition.\d+\] line \d+ Check ensures clause: FAILURE$
5+
^VERIFICATION FAILED$
6+
^EXIT=10$
7+
^SIGNAL=0$
8+
--
9+
--
10+
This test checks that the front end parses and typchecks correct uses of:
11+
- __CPROVER_freeable_t function calls as frees clause targets
12+
- the predicate __CPROVER_freeable
13+
- the predicate __CPROVER_is_freeable
14+
- the predicate __CPROVER_is_freed
15+
16+
The post condition of the contract is expected to fail because the predicates
17+
have no interpretation in the back-end yet.

‎regression/contracts/frees-clause-for-loop-fail/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
--apply-loop-contracts
4-
^main.c.*: error: frees clause target must be a pointer-typed expression$
4+
^main.c.* error: frees clause target must be a pointer-typed expression or a call to a function returning __CPROVER_freeable_t$
55
^CONVERSION ERROR$
66
^EXIT=(1|64)$
77
^SIGNAL=0$

‎regression/contracts/frees-clause-function-fail/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-
^main.c.*: error: frees clause target must be a pointer-typed expression$
4+
^main.c.* error: frees clause target must be a pointer-typed expression or a call to a function returning __CPROVER_freeable_t$
55
^CONVERSION ERROR$
66
^EXIT=(1|64)$
77
^SIGNAL=0$

‎regression/contracts/frees-clause-while-loop-fail/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
--apply-loop-contracts
4-
^main.c.*: error: frees clause target must be a pointer-typed expression$
4+
^main.c.* error: frees clause target must be a pointer-typed expression or a call to a function returning __CPROVER_freeable_t$
55
^CONVERSION ERROR$
66
^EXIT=(1|64)$
77
^SIGNAL=0$

0 commit comments

Comments
 (0)