Skip to content

Commit ecfea14

Browse files
feliperodrifeliperodri
committed
Updates assigns clause description in CPROVER manual
Signed-off-by: Felipe R. Monteiro <[email protected]>
1 parent 2f04407 commit ecfea14

File tree

1 file changed

+226
-50
lines changed

1 file changed

+226
-50
lines changed

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

Lines changed: 226 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,17 @@
11
## CBMC Assigns Clause
22

3-
43
### Introduction
4+
55
The _assigns_ clause allows the user to specify a list of memory
66
locations which may be written within a particular scope. While an assigns
77
clause may, in general, be interpreted with either _writes_ or _modifies_
8-
semantics, this design is based on the former. This means that memory not
8+
semantics, this design is based on the former. This means that memory not
99
captured by the assigns clause must not be written within the given scope, even
1010
if the value(s) therein are not modified.
1111

12-
13-
### Scalar Variables
14-
The initial iteration of this design focuses on specifying an assigns clause for
15-
primitive types and their pointers. Arrays, structured data, and pointers are
16-
left to future contributions.
12+
Assigns clauses currently support simple variable types and their pointers,
13+
structs, and arrays. Recursive pointer structures are left to future work,
14+
as their support would require changes to CBMC's memory model.
1715

1816

1917
##### Syntax
@@ -24,29 +22,82 @@ defined as follows.
2422
<assigns_clause> := __CPROVER_assigns ( <target_list> )
2523
```
2624
```
27-
<target_list> := <target>
28-
| <target> , <target_list>
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>
2940
```
3041
```
31-
<target> := <identifier>
32-
| * <target>
42+
<member_target> := <primary_target>
43+
| <member_target> . <member_name>
44+
| <member_target> -> <member_name>
45+
```
46+
```
47+
<primary_target> := <identifier>
48+
| ( <target> )
3349
```
3450

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.
3557

36-
The `<assigns_clause>` states that only the memory identified by the dereference
37-
expressions and identifiers listed in the contained `<target_list>` may be
38-
written within the associated scope, as follows.
58+
For example, consider the following declarations.
3959

60+
```
61+
struct pair
62+
{
63+
int x;
64+
int y;
65+
};
66+
67+
void foo(int *myInt1, int *myInt2, struct pair *myPair, int myArr[], int lastIdx)
68+
__CPROVER_assigns(*myInt1, myPair->y, myArr[5, lastIdx]);
69+
```
70+
71+
This code declares a struct type, called `pair` with 2 members `x` and `y`,
72+
as well as a function `foo` which takes two integer pointer arguments
73+
`myInt1` and `myInt2`, one pair struct pointer `myPair`, and an array
74+
argument `myArr` with an associated last index `lastIdx`. The assigns
75+
clause attached to this definition states that most of the arguments
76+
can be assigned. However, `myInt2`, `myPair->x`, and the first four
77+
elements of `myArr` should not be assigned in the body of `foo`.
4078

4179
##### Semantics
42-
The semantics of an assigns clause *c* of some function *f* can be understood in
43-
two contexts. First, one may consider how the expressions in *c* are treated
44-
when a call to *f* is replaced by its contract specification, assuming the
45-
contract specification is a sound characterization of the behavior of *f*.
46-
Second, one may consider how *c* is applied to the function body of *f* in order
47-
to determine whether *c* is a sound characterization of the behavior of *f*. We
48-
begin by exploring these two perspectives for assigns clauses which contain only
49-
scalar expressions.
80+
The semantics of an assigns clause *c* of some function *f* can
81+
be understood in two contexts. First, one may consider how the expressions in
82+
*c* are treated when a call to *f* is replaced by its contract specification,
83+
assuming the contract specification is a sound characterization of the behavior
84+
of *f*. Second, one may consider how *c* is applied to the function body of *f*
85+
in order to determine whether *c* is a sound characterization of the behavior of
86+
*f*. To illustrate these two perspectives, consider the following definition of
87+
`foo`.
88+
89+
90+
```
91+
void foo(int *myInt1, int *myInt2, struct pair *myPair, int myArr[], int lastIdx)
92+
{
93+
*myInt1 = 34;
94+
myPair->y = 55;
95+
myArr[5] = 89;
96+
}
97+
```
98+
99+
We begin by exploring these two perspectives with a formal definition, and then
100+
an example.
50101

51102
Let the i<sup>th</sup> expression in some assigns clause *c* be denoted
52103
*exprs*<sub>*c*</sub>[i], the j<sup>th</sup> formal parameter of some function
@@ -55,35 +106,160 @@ in a call to function *f* be denoted *args*<sub>*f*</sub>[k] (an identifying
55106
index may be added to distinguish a *particular* call to *f*, but for simplicity
56107
it is omitted here).
57108

58-
59109
###### Replacement
60-
Assuming an assigns clause *c* is a sound characterization of the behavior of
61-
the function *f*, a call to *f* may be replaced a series of non-deterministic
62-
assignments. For each expression *e* &#8712; *exprs*<sub>*c*</sub>, let there be
63-
an assignment &#632; := &#8727;, where &#632; is *args*<sub>*f*</sub>[i] if *e*
64-
is identical to some *params*<sub>*f*</sub>[i], and *e* otherwise.
110+
Assuming an assigns clause *c* is a sound characterization of
111+
the behavior of the function *f*, a call to *f* may be replaced a series of
112+
non-deterministic assignments. For each expression *e* &#8712;
113+
*exprs*<sub>*c*</sub>, let there be an assignment &#632; := &#8727;, where
114+
&#632; is *args*<sub>*f*</sub>[i] if *e* is identical to some
115+
*params*<sub>*f*</sub>[i], and *e* otherwise. For array ranges, create an
116+
assignment for each element in the array range.
117+
118+
In the case where *f* is `foo`, and some function `bar` calls `foo`
119+
120+
```
121+
void bar()
122+
{
123+
int a, b;
124+
int arr[8];
125+
struct pair p;
126+
127+
foo(&a, &b, &p, arr, 7);
128+
}
129+
```
130+
131+
the call to `foo` is replaced by the following series of assignments.
65132

133+
```
134+
void bar()
135+
{
136+
int a, b;
137+
int arr[10];
138+
struct pair p;
139+
140+
a = *;
141+
p.y = *;
142+
arr[5] = *;
143+
arr[6] = *;
144+
arr[7] = *;
145+
}
146+
```
66147

67148
###### Enforcement
68-
In order to determine whether an assigns clause *c* is a sound characterization
69-
of the behavior of a function *f*, the body of the function should be
70-
instrumented with additional statements as follows.
71-
72-
- For each expression *e* &#8712; *exprs*<sub>*c*</sub>, create a temporary
73-
variable *tmp*<sub>*e*</sub> to store \&(*e*), the address of *e*, at the
74-
start of *f*.
75-
- Before each assignment statement, *lhs* := *rhs*, add an assertion (structured
76-
as a disjunction)
77-
assert(&#8707; *tmp*<sub>*e*</sub>. \_\_CPROVER\_same\_object(\&(*lhs*),
78-
*tmp*<sub>*e*</sub>)
79-
- Before each function call with an assigns clause *a*, add an assertion for
80-
each *e*<sub>*a*</sub> &#8712; *exprs*<sub>*a*</sub> (also formulated as a
81-
disjunction)
82-
assert(&#8707; *tmp*<sub>*e*</sub>.
83-
\_\_CPROVER\_same\_object(\&(*e*<sub>*a*</sub>), *tmp*<sub>*e*</sub>)
84-
85-
Here, \_\_CPROVER\_same\_object returns true if two pointers
86-
reference the same object in the CBMC memory model. Additionally, for each
87-
function call without an assigns clause, CBMC adds an assertion assert(*false*)
88-
to ensure that the assigns contract will only hold if all called functions
89-
have an assigns clause which is compatible with that of the calling function.
149+
In order to determine whether an assigns clause *c* is a
150+
sound characterization of the behavior of a function *f*, the body of the
151+
function is instrumented with assertion statements before each statement which
152+
may write to memory (e.g. an assignment). These assertions are based on the
153+
assignable targets *exprs*<sub>*c*</sub> identified in the assigns clause.
154+
155+
While sequentially traversing the function body, CBMC instruments statements
156+
that might modify memory a preceding assertion to ensure that they only
157+
modify assignable memory. These assertions consist of a disjunction
158+
where each disjunct depends on the type of the assignable target.
159+
160+
- For an assignable target expression *e* of scalar type:
161+
162+
```
163+
__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(&e) &&
164+
__CPROVER_POINTER_OFFSET(&lhs) == __CPROVER_POINTER_OFFSET(&e)
165+
```
166+
167+
- For an assignable target expression *e* of struct type, a similar disjunct is
168+
created, with an additional size comparison:
169+
170+
```
171+
__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(&e) &&
172+
__CPROVER_POINTER_OFFSET(&lhs) == __CPROVER_POINTER_OFFSET(&e) &&
173+
sizeof(lhs) == sizeof(e)
174+
```
175+
176+
Additionally, for each member m of *e*, we add an extra disjunct:
177+
178+
```
179+
__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(&(e->m)) &&
180+
__CPROVER_POINTER_OFFSET(&lhs) == __CPROVER_POINTER_OFFSET(&(e->m)) &&
181+
sizeof(lhs) == sizeof(e->m)
182+
```
183+
184+
This extension is performed recursively in the
185+
case that some member of a struct is also a struct.
186+
187+
- For an assignable target expression *e* of array range type, `a[lo, hi]`, a
188+
disjunct is created using the array pointer `a` and the range bounds `lo` and
189+
`hi`:
190+
191+
```
192+
__CPROVER_POINTER_OBJECT(&lhs) == __CPROVER_POINTER_OBJECT(a) &&
193+
__CPROVER_POINTER_OFFSET(&lhs) >= lo * sizeof(a[0]) &&
194+
__CPROVER_POINTER_OFFSET(&lhs) <= hi * sizeof(a[0])
195+
```
196+
197+
This effectively creates an assertion that the memory location being assigned
198+
falls within the assignable memory identified by the assigns clause. In
199+
practice, temporary variables are used to ensure that the assignable memory
200+
doesn't change during function execution, but here we have used the assignable
201+
targets directly for readability. Function calls are handled similarly, based
202+
on the memory their assigns clause indicates that they can modify.
203+
Additionally, for each function call without an assigns clause, we add an
204+
assertion assert(*false*) to ensure that the assigns contract will only hold if
205+
all called functions have an assigns clause which is compatible with that of the
206+
calling function.
207+
208+
For the earlier example, `foo` would be instrumented as follows:
209+
210+
211+
```
212+
void foo(int *myInt1, int *myInt2, struct pair *myPair, int myArr[], int lastIdx)
213+
{
214+
int *temp1 = myInt1;
215+
int *temp2 = &(myPair->y);
216+
int *temp3 = myArr;
217+
int temp4 = 5 * sizeof(iint);
218+
int temp5 = lastIdx * sizeof(int);
219+
220+
assert((__CPROVER_POINTER_OBJECT(myInt1) == __CPROVER_POINTER_OBJECT(temp1) &&
221+
__CPROVER_POINTER_OFFSET(myInt1) == __CPROVER_POINTER_OFFSET(temp1)) ||
222+
(__CPROVER_POINTER_OBJECT(myInt1) == __CPROVER_POINTER_OBJECT(temp2) &&
223+
__CPROVER_POINTER_OFFSET(myInt1) == __CPROVER_POINTER_OFFSET(temp2)) ||
224+
(__CPROVER_POINTER_OBJECT(myInt1) == __CPROVER_POINTER_OBJECT(temp3) &&
225+
__CPROVER_POINTER_OFFSET(myInt1) >= temp4 &&
226+
__CPROVER_POINTER_OFFSET(myInt1) <= temp5)
227+
);
228+
*myInt1 = 34;
229+
230+
assert((__CPROVER_POINTER_OBJECT(&(myPair->y)) == __CPROVER_POINTER_OBJECT(temp1) &&
231+
__CPROVER_POINTER_OFFSET(&(myPair->y)) == __CPROVER_POINTER_OFFSET(temp1)) ||
232+
(__CPROVER_POINTER_OBJECT(&(myPair->y)) == __CPROVER_POINTER_OBJECT(temp2) &&
233+
__CPROVER_POINTER_OFFSET(&(myPair->y)) == __CPROVER_POINTER_OFFSET(temp2)) ||
234+
(__CPROVER_POINTER_OBJECT(&(myPair->y)) == __CPROVER_POINTER_OBJECT(temp3) &&
235+
__CPROVER_POINTER_OFFSET(&(myPair->y)) >= temp4 &&
236+
__CPROVER_POINTER_OFFSET(&(myPair->y)) <= temp5)
237+
);
238+
myPair->y = 55;
239+
240+
assert((__CPROVER_POINTER_OBJECT(&(myArr[5])) == __CPROVER_POINTER_OBJECT(temp1) &&
241+
__CPROVER_POINTER_OFFSET(&(myArr[5])) == __CPROVER_POINTER_OFFSET(temp1)) ||
242+
(__CPROVER_POINTER_OBJECT(&(myArr[5])) == __CPROVER_POINTER_OBJECT(temp2) &&
243+
__CPROVER_POINTER_OFFSET(&(myArr[5])) == __CPROVER_POINTER_OFFSET(temp2)) ||
244+
(__CPROVER_POINTER_OBJECT(&(myArr[5])) == __CPROVER_POINTER_OBJECT(temp3) &&
245+
__CPROVER_POINTER_OFFSET(&(myArr[5])) >= temp4 &&
246+
__CPROVER_POINTER_OFFSET(&(myArr[5])) <= temp5)
247+
);
248+
myArr[5] = 89;
249+
}
250+
```
251+
252+
Additionally, the set of assignable target expressions is updated while
253+
traversing the function body when new memory is allocated. For example, the
254+
statement `x = (int *)malloc(sizeof(int))` would create a pointer, stored in
255+
`x`, to assignable memory. Since the memory is allocated within the current
256+
function, there is no way an assignment to this memory can affect the memory of
257+
the calling context. If memory is allocated for a struct, the subcomponents are
258+
considered assignable as well.
259+
260+
Finally, a set of freely-assignable symbols *free* is tracked during the
261+
traversal of the function body. These are locally-defined variables and formal
262+
parameters without dereferences. For example, in a variable declaration `<type>
263+
x = <initial_value>`, `x` would be added to *free*. Assignment statements (i.e.,
264+
where the left-hand-side is in *free*) are not instrumented with
265+
the above assertions.

0 commit comments

Comments
 (0)