Skip to content

Commit 11d0b0c

Browse files
feliperodrifeliperodri
committed
Adds documentation about function contracts
Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 0ae6010 commit 11d0b0c

File tree

6 files changed

+405
-47
lines changed

6 files changed

+405
-47
lines changed

‎doc/cprover-manual/assigns-clause.md

Lines changed: 11 additions & 47 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,10 @@
1-
# CBMC Assigns Clause
1+
# Assigns Clause
22

3-
## Introduction
3+
### Definition
4+
5+
```c
6+
void __CPROVER_assigns(...)
7+
```
48
59
The _assigns_ clause allows the user to specify a list of memory
610
locations which may be written within a particular scope. While an assigns
@@ -9,52 +13,12 @@ semantics, this design is based on the former. This means that memory not
913
captured by the assigns clause must not be written within the given scope, even
1014
if the value(s) therein are not modified.
1115
16+
### Parameters
17+
1218
Assigns clauses currently support simple variable types and their pointers,
1319
structs, and arrays. Recursive pointer structures are left to future work,
1420
as their support would require changes to CBMC's memory model.
1521
16-
17-
## Syntax
18-
A special construct is introduced to specify assigns clauses. Its syntax is
19-
defined as follows.
20-
21-
```
22-
<assigns_clause> := __CPROVER_assigns ( <target_list> )
23-
```
24-
```
25-
<target_list> := __CPROVER_nothing
26-
| <target>
27-
| <target_list> , <target>
28-
```
29-
```
30-
<target> := <deref_target>
31-
| <target> [ array_index ]
32-
| <target> [ array_range ]
33-
34-
<array_index> := <identifier> | <integer>
35-
<array_range> := <array_index> , <array_index>
36-
```
37-
```
38-
<deref_target> := <member_target>
39-
| * <deref_target>
40-
```
41-
```
42-
<member_target> := <primary_target>
43-
| <member_target> . <member_name>
44-
| <member_target> -> <member_name>
45-
```
46-
```
47-
<primary_target> := <identifier>
48-
| ( <target> )
49-
```
50-
51-
The assigns clause identifies a list of targets, which may be an identifier
52-
(e.g. `x`), a member of a struct (e.g. `myStruct.someMember` or
53-
`myStructPtr->otherMember`), a dereferenced pointer (e.g. `*myPtr`), or an
54-
array range (e.g. `myArr[5, lastIdx]`). The `<assigns_clause>` states that only
55-
memory identified in the target list may be written within the function, as
56-
described in the next section.
57-
5822
For example, consider the following declarations.
5923
6024
```c
@@ -76,7 +40,7 @@ clause attached to this definition states that most of the arguments
7640
can be assigned. However, `myInt2`, `myPair->x`, and the first four
7741
elements of `myArr` should not be assigned in the body of `foo`.
7842

79-
## Semantics
43+
### Semantics
8044
The semantics of an assigns clause *c* of some function *f* can
8145
be understood in two contexts. First, one may consider how the expressions in
8246
*c* are treated when a call to *f* is replaced by its contract specification,
@@ -106,7 +70,7 @@ in a call to function *f* be denoted *args*<sub>*f*</sub>[k] (an identifying
10670
index may be added to distinguish a *particular* call to *f*, but for simplicity
10771
it is omitted here).
10872
109-
## Replacement
73+
#### Replacement
11074
Assuming an assigns clause *c* is a sound characterization of
11175
the behavior of the function *f*, a call to *f* may be replaced a series of
11276
non-deterministic assignments. For each expression *e* &#8712;
@@ -145,7 +109,7 @@ void bar()
145109
}
146110
```
147111

148-
## Enforcement
112+
#### Enforcement
149113
In order to determine whether an assigns clause *c* is a
150114
sound characterization of the behavior of a function *f*, the body of the
151115
function is instrumented with assertion statements before each statement which

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

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
# Function Contracts
2+
3+
CBMC offers support for function contracts, which includes three basic
4+
clauses: _requires_, _ensures_, and _assigns_. These clauses
5+
accept either symbols or Boolean predicates that formally describe the
6+
specification of a function, but they might need more expressive constructs to
7+
fully specify these operations. Therefore, CBMC also provides a series of
8+
built-in constructus to be used with functions contracts (e.g., _history
9+
variables_, _quantifiers_, and _memory predicates_).
10+
11+
To learn more about contracts, take a look at the chapter [Design by Contract](http://se.inf.ethz.ch/~meyer/publications/old/dbc_chapter.pdf) from the book Object-Oriented Software Construction by Bertrand Meyer or check it out the notes [Contract-based Design](https://www.georgefairbanks.com/york-university-contract-based-design-2021) by George Fairbanks.
12+
13+
## Overview
14+
15+
Take a look at the example below.
16+
17+
```c
18+
#include <stdlib.h>
19+
#include <stdint.h>
20+
21+
#define SUCCESS 0
22+
#define FAILURE -1
23+
24+
int sum(uint32_t* a, uint32_t* b, uint32_t* out)
25+
{
26+
const uint64_t result = ((uint64_t) *a) + ((uint64_t) *b);
27+
if (result > UINT32_MAX) return FAILURE;
28+
*out = (uint32_t) result;
29+
return SUCCESS;
30+
}
31+
32+
int foo()
33+
{
34+
uint32_t* a = malloc(sizeof(*a));
35+
uint32_t* b = malloc(sizeof(*a));
36+
uint32_t out;
37+
int rval = sum(a, b, &out);
38+
if (rval == SUCCESS)
39+
return out;
40+
return rval;
41+
}
42+
```
43+
44+
Function `sum` writes the sum of `a` and `b` to `out`, and returns `SUCCESS`; unless there is overflows, in which case it returns `FAILURE`. Let's write a function contract for this function.
45+
46+
A function contract has three parts:
47+
48+
- **Precondition** - describes what the function requires of the arguments supplied by the caller and global variables;
49+
- **Postcondition** - describes the effects of the function;
50+
- **Writable Set** - describes the set of locations outside the function that might be written to;
51+
52+
In our example, the developer may require from the caller to properly allocate all
53+
arguments, thus, pointers must be valid. We can specify the preconditions of a function using `__CPROVER_requires` (see [Requires \& Ensures Clauses](requires-and-ensures-clauses.md) Section for details) and we can specify an allocated object using a predicate called `__CPROVER_is_fresh` (see [Memory Predicate]() Section for details). Thus, for the `sum` function, the set of preconditions are
54+
55+
```c
56+
/* Precondition */
57+
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(*a)))
58+
__CPROVER_requires(__CPROVER_is_fresh(b, sizeof(*b)))
59+
__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out)))
60+
```
61+
62+
We can use `__CPROVER_ensures` to specify postconditions (see [Requires \& Ensures Clauses](requires-and-ensures-clauses.md) Section for details).
63+
In our example, developers can use the built-in construct
64+
`__CPROVER_return_value`, which represents the return value of a function. As
65+
postconditions, one may list possible return values (in this
66+
case, either `SUCCESS` or `FAILURE`) as well as describe the main property of
67+
this function: if the function returns `SUCCESS`, then `*out` stores the
68+
result of `*a + *b`.
69+
We can also check that the value in `out` will be preserved in case of failure by using `__CPROVER_old`, which refers to the value of a given object in the pre-state of a function (see [History Varaibles]() Section for details). Thus, for the `sum` function, the set of postconditions are
70+
71+
72+
```c
73+
/* Postconditions */
74+
__CPROVER_ensures(__CPROVER_return_value == SUCCESS || __CPROVER_return_value == FAILURE)
75+
__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (*a + *b)))
76+
__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == __CPROVER_old(*out)))
77+
```
78+
79+
Finally, the _assigns_ clause allows developers to define a frame condition (see [Assigns Clauses](assigns-clause.md) Section for details).
80+
in general, be interpreted with either _writes_ or _modifies_ semantics, this
81+
design is based on the former. This means that memory not specified by the
82+
assigns clause must not be written within the given function scope, even if the
83+
value(s) therein are not modified. In our example, since we only expect
84+
that the value pointed by `out` may be modified, we annotate the function using
85+
`__CPROVER_assigns(*out)`.
86+
87+
```c
88+
/* Writable Set */
89+
__CPROVER_assigns(*out)
90+
```
91+
92+
Here is the whole function with its contract.
93+
94+
```c
95+
int sum(uint32_t* a, uint32_t* b, uint32_t* out)
96+
/* Precondition */
97+
__CPROVER_requires(__CPROVER_is_fresh(a, sizeof(*a)))
98+
__CPROVER_requires(__CPROVER_is_fresh(b, sizeof(*b)))
99+
__CPROVER_requires(__CPROVER_is_fresh(out, sizeof(*out)))
100+
/* Postconditions */
101+
__CPROVER_ensures(__CPROVER_return_value == SUCCESS || __CPROVER_return_value == FAILURE)
102+
__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (*a + *b)))
103+
__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == __CPROVER_old(*out)))
104+
/* Writable Set */
105+
__CPROVER_assigns(*out)
106+
{
107+
const uint64_t result = ((uint64_t) *a) + ((uint64_t) *b);
108+
if (result > UINT32_MAX) return FAILURE;
109+
*out = (uint32_t) result;
110+
return SUCCESS;
111+
}
112+
```
113+
114+
First, we have to prove the function contract is correct.
115+
116+
```shell
117+
goto-cc -o main.goto *.c
118+
goto-instrument --enforce-contract sum main.goto main-checking-contracts.goto
119+
cbmc main-checking-contracts.goto
120+
```
121+
122+
The first command just compiles the GOTO program as usual, the second command instruments the code to check the function contract, and the third one runs CBMC to do the checking.
123+
124+
Now that we proved the function contract is correct, we can use the function contract in place of the function implementation wherever the function is called.
125+
126+
```shell
127+
goto-cc -o main.goto *.c
128+
goto-instrument --replace-contract sum main.goto main-using-contracts.goto
129+
cbmc main-using-contracts.goto
130+
```
131+
132+
The first command just compiles the goto program as usual, the second command instruments the code to use the function contract in place of the function implementation wherever is invoked, and the third one runs CBMC to check the program using contracts.
133+
134+
## Additional Resources
135+
136+
- [Requires \& Ensures Clauses](requires-and-ensures-clauses.md)
137+
- [Assigns Clauses](assigns-clause.md)
138+
- [Memory Predicates](memory-predicates.md)
139+
- [History Variables](history-variables.md)
140+
- [Quantifiers](quantifiers.md)

‎doc/cprover-manual/history-variables.md

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
# Historic variables
2+
3+
### Denfinition
4+
5+
`__CPROVER_old()` refers to the value of a given object
6+
in the pre-state of a function within the _ensures_ clause. It only supports
7+
scalars, structs and pointers.
8+
9+
```c
10+
int add_overflow(uint32_t a, uint32_t b, uint32_t* out)
11+
/* ... */
12+
__CPROVER_ensures((__CPROVER_return_value == FAILURE) ==> (*out == __CPROVER_old(*out)))
13+
/* ... */
14+
{
15+
/* ... */
16+
}
17+
```
18+
19+
### Semantics

‎doc/cprover-manual/memory-predicates.md

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,54 @@
1+
# Memory Predicates
2+
3+
4+
### Definition
5+
`__CPROVER_is_fresh` specifies freshly allocated objects.
6+
This allows us to use function contracts without wrapping the function around
7+
harnesses to perform allocations (e.g., using malloc). Let's improve our first
8+
example `add_overflow`. Instead of simply requesting `out != NULL`, we can
9+
specify a fresh allocated object.
10+
11+
```c
12+
int add_overflow(uint32_t a, uint32_t b, uint32_t* out)
13+
__CPROVER_requires(__CPROVER_is_fresh(out))
14+
__CPROVER_ensures(__CPROVER_return_value == SUCCESS || __CPROVER_return_value == FAILURE)
15+
__CPROVER_ensures((__CPROVER_return_value == SUCCESS) ==> (*out == (a + b)))
16+
{
17+
/* ... */
18+
}
19+
```
20+
21+
### Parameters
22+
23+
### Semantics
24+
25+
**Enforcement.** It creates an infinite map that records the allocated elements
26+
in _requires_ clauses and a function for each type used in a function contract
27+
that returns an object or array of that type. For _ensures_ clauses, it ensures
28+
that an object is *fresh* (e.g., not previously allocated).
29+
30+
```c
31+
/* Declarations */
32+
static uint8_t __<fn_name>_memory_map[__CPROVER_constant_infinity_uint];
33+
34+
/* For each referenced type */
35+
static bool __<fn_name>_<type>_requires_is_fresh(<type> *elem, size_t size);
36+
static bool __<fn_name>_<type>_ensures_is_fresh(<type> *elem, size_t size);
37+
```
38+
39+
**Replacement.** CBMC needs to create dual declarations. For the _requires_
40+
clauses, CBMC needs to check that all objects mapped to *fresh* objects are
41+
distinct. For the _ensures_ clauses, if an object is *fresh*, we need to create
42+
a new object to represent it.
43+
44+
```c
45+
/* Declarations (per call) */
46+
static uint8_t <fn_name>_memory_map[__CPROVER_constant_infinity_uint];
47+
48+
/* For each referenced type */
49+
static bool __call_<fn_name>_<type>_requires_is_fresh(<type> *elem, size_t size);
50+
static bool __call_<fn_name>_<type>_ensures_is_fresh(<type> *elem, size_t size);
51+
```
52+
53+
Note that for a given context, we may have multiple calls to the same function,
54+
so we have to be sure to create unique identifiers for the declarations.

‎doc/cprover-manual/quantifiers.md

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
# Quantifiers
2+
3+
### Definition
4+
5+
`__CPROVER_forall{}` and `__CPROVER_exists{}` are both supported in function-contracts context.
6+
7+
```
8+
__CPROVER_forall { *type identifier* : range; *expression* }
9+
__CPROVER_exists { *type identifier* : range; *expression* }
10+
```
11+
12+
13+
### Semantics
14+
15+
These expressions support quantification in CBMC. They have meaning both for
16+
bounded and unbounded verification by virtue of the range predicate, which
17+
defines minimum and maximum values for quantification. These can be arbitrarily
18+
small and large, within the limits of the C type that is quantified over.
19+
20+
```c
21+
int foo(int *arr, int len)
22+
/* ... */
23+
__CPROVER_ensures(__CPROVER_forall {
24+
int i;
25+
(0 <= i && i < len) ==> arr[i] == i
26+
})
27+
{
28+
/* ... */
29+
}
30+
31+
int bar(int *arr, int len)
32+
__CPROVER_requires(__CPROVER_exists {
33+
int i;
34+
(0 <= i && i < len) && arr[i] == 1
35+
})
36+
/* ... */
37+
{
38+
/* ... */
39+
}
40+
```

0 commit comments

Comments
 (0)