You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Here is described the syntax and semantics of the "assigns" clause as implemented in CBMC. This construct allows the user to specify a list of memory locations which may be written within a particular scope. While an assigns clause may, in general, be interpreted with either "writes" or "modifies" semantics, this design is based on the former.
5
-
This means that memory not captured by the assigns clause must not be written within the given scope, even if the value(s) therein are not modified.
5
+
The _assigns_ clause allows the user to specify a list of memory
6
+
locations which may be written within a particular scope. While an assigns
7
+
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
9
+
captured by the assigns clause must not be written within the given scope, even
10
+
if the value(s) therein are not modified.
11
+
6
12
7
13
### Scalar Variables
8
-
The initial iteration of this design focuses on specifying an assigns clause for simple variable types and their pointers. Arrays, structured data, and pointers are left to future contributions.
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.
9
17
10
18
11
19
##### Syntax
12
-
A special construct is introduced to specify assigns clauses. Its syntax is defined as follows.
20
+
A special construct is introduced to specify assigns clauses. Its syntax is
@@ -24,28 +33,57 @@ A special construct is introduced to specify assigns clauses. Its syntax is defi
24
33
```
25
34
26
35
27
-
The `<assigns_clause>` states that only the memory identified by the dereference expressions and identifiers listed in the contained `<target_list>` may be written within the associated scope, as follows.
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.
39
+
28
40
29
41
##### Semantics
30
-
The semantics of an assigns clause *c* of some function *f* can be understood in two contexts. First, one may consider how the expressions in *c* are treated when a call to *f* is replaced by its contract specification, assuming the contract specification is a sound characterization of the behavior of *f*. Second, one may consider how *c* is applied the function body of *f* in order to determine whether *c* is a sound characterization of the behavior of *f*. We begin by exploring these two perspectives for assigns clauses which contain only scalar expressions.
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.
50
+
51
+
Let the i<sup>th</sup> expression in some assigns clause *c* be denoted
52
+
*exprs*<sub>*c*</sub>[i], the j<sup>th</sup> formal parameter of some function
53
+
*f* be denoted *params*<sub>*f*</sub>[j], and the k<sup>th</sup> argument passed
54
+
in a call to function *f* be denoted *args*<sub>*f*</sub>[k] (an identifying
55
+
index may be added to distinguish a *particular* call to *f*, but for simplicity
56
+
it is omitted here).
31
57
32
-
Let the i<sup>th</sup> expression in some assigns clause *c* be denoted *exprs*<sub>*c*</sub>[i], the j<sup>th</sup> formal parameter of some function *f* be denoted *params*<sub>*f*</sub>[j], and the k<sup>th</sup> argument passed in a call to function *f* be denoted *args*<sub>*f*</sub>[k] (an identifying index may be added to distinguish a *particular* call to *f*, but for simplicity it is omitted here).
33
58
34
59
###### Replacement
35
-
Assuming an assigns clause *c* is a sound characterization of the behavior of the function *f*, a call to *f* may be replaced a series of non-deterministic assignments. For each expression *e*∈*exprs*<sub>*c*</sub>, let there be an assignment ɸ := ∗, where ɸ is *args*<sub>*f*</sub>[i] if *e* is identical to some *params*<sub>*f*</sub>[i], and *e* otherwise.
36
-
37
-
###### Enforcement
38
-
In order to determine whether an assigns clause *c* is a sound characterization of the behavior of a function *f*, the body of the function should be instrumented with additional statements as follows.
39
-
40
-
- For each expression *e*∈*exprs*<sub>*c*</sub>, create a temporary variable *tmp*<sub>*e*</sub> to store \&(*e*), the address of *e*, at the start of *f*.
41
-
- Before each assignment statement, *lhs* := *rhs*, add an assertion (structured as a disjunction)
- Before each function call with an assigns clause *a*, add an assertion for each *e*<sub>*a*</sub> ∈*exprs*<sub>*a*</sub> (also formulated as a disjunction)
Here, __CPROVER_same_object is a predicate indicating that the two pointers reference the same object in the CBMC memory model. Additionally, for each function call without an assigns clause, add an assertion assert(*false*) to ensure that the assigns contract will only hold if all called functions have an assigns clause which is compatible with that of the calling function.
49
-
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*∈*exprs*<sub>*c*</sub>, let there be
63
+
an assignment ɸ := ∗, where ɸ is *args*<sub>*f*</sub>[i] if *e*
64
+
is identical to some *params*<sub>*f*</sub>[i], and *e* otherwise.
50
65
51
66
67
+
###### 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*∈*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
0 commit comments