Changes between Version 34 and Version 35 of ContractReduction
- Timestamp:
- 12/09/15 11:52:29 (10 years ago)
Legend:
- Unmodified
- Added
- Removed
- Modified
-
ContractReduction
v34 v35 3 3 == ACSL function contract grammar with CIVL-C extension (starting with `$`) == 4 4 The CIVL-C function contract extends ACSL function contract with the following elements: 5 * ` $guards` clause: specify the guard of a function, i.e., the specified predicate should hold in order to enable the execution of the function body6 * ` $depends` clause: specify the dependency relation of the function, usually used for partial order reduction (POR) or other analysis7 * ` $reads` clause: specify memory locations read by the function, the syntax of which is similar to `assigns` clause5 * `guards` clause: specify the guard of a function, i.e., the specified predicate should hold in order to enable the execution of the function body 6 * `depends` clause: specify the dependency relation of the function, usually used for partial order reduction (POR) or other analysis 7 * `reads` clause: specify memory locations read by the function, the syntax of which is similar to `assigns` clause 8 8 * additional parameter for `allocates` clause: specify the scope of the heap for allocation; if absent then the root scope `$root` is used 9 9 … … 14 14 terminates-clause ::= terminates pred ; 15 15 decreases-clause ::= decreases term (for id)? ; 16 guards-clause ::= $guards pred ;16 guards-clause ::= guards pred ; 17 17 simple-clause ::= assigns-clause | ensures-clause 18 18 | allocation-clause | abrupt-clause-fn … … 22 22 ensures-clause ::= ensures pred ; 23 23 allocation-clause ::= allocates tsets (, scope)? ; | frees tsets ; 24 reads-clause ::= $reads tsets;25 depends-clause := $depends event (, event)*;24 reads-clause ::= reads tsets; 25 depends-clause := depends event (, event)*; 26 26 named-behavior ::= behavior id : behavior-body 27 27 behavior-body ::= assumes-clause∗ requires-clause∗ simple-clause∗ … … 29 29 completeness-clause ::= complete behaviors (id (, id)∗)? ; 30 30 | disjoint behaviors (id (, id)∗)? ; 31 term ::= \old ( term ) | \result | \nothing | $everything31 term ::= \old ( term ) | \result | \nothing | \everything 32 32 pred ::= \old ( pred ) 33 33 }}} … … 54 54 * a left-hand-side expression, when used in certain contexts, is automatically converted to `$memory`. The contexts are: arguments to the built-in functions `$access`, `$read`, and `$write` described below, or occurrence in the list of an `$assigns` clause 55 55 * `a[dom]`, where `a` is an expression of array type and `dom` is an expression of `$domain` type. The dimension of the array must match the dimension of the domain. This represents all memory units which are the cells in the array indexed by a tuple in `dom`. 56 * ` $region(ptr)`, where `ptr` is an expression with a pointer type. This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself.56 * `\region(ptr)`, where `ptr` is an expression with a pointer type. This represents the set of all memory units reachable from `ptr`, including the memory unit pointed to by `ptr` itself. 57 57 58 58 [[* `mem1+mem2`, where `mem1` and `mem2` are expressions of type `$memory`. This is the union of the two sets.]] Problem this is ambiguous with numeric +, as in x+y. … … 68 68 Example: 69 69 {{{ 70 assigns x,a[i][j], $region(list->head),b[dom];71 }}} 72 73 74 == ` $depends` clause ==70 assigns x,a[i][j],\region(list->head),b[dom]; 71 }}} 72 73 74 == `depends` clause == 75 75 76 76 This contractual clause specifies part of the dependence relation used in POR. 77 77 {{{ 78 $depends event (, event)*78 depends event (, event)* 79 79 }}} 80 80 where `event` is a memory event represented as a boolean expression. For each process `p`, the `event ` can be evaluated in the context of `p`. If `event ` evaluates to `true`, then `p` must be included in an ample set containing a call to this function. … … 84 84 {{{ 85 85 EventSetExpression 86 ::= $read(MemorySetExpression) 87 | $write(MemorySetExpression) 88 | $access(MemorySetExpression) 89 | $calls(FunctionCallExpression) 86 ::= \read(MemorySetExpression) 87 | \write(MemorySetExpression) 88 | \calls(FunctionCallExpression) 90 89 | \nothing 91 | $everything90 | \everything 92 91 | ‘(’ EventSetExpression ‘)’ 93 92 | EventSetExpression + EventSetExpression … … 102 101 The following built-in functions may be used as constituents in the boolean expression `e`: 103 102 104 * `_Bool $access(<memory-list>)` 105 * holds if any memory unit in the list may be read or modified by `p` at some point now or in the future. 106 * `_Bool $write(<memory-list>)` 103 * `_Bool \write(<memory-list>)` 107 104 * holds if any memory unit in the list may be modified by `p` at some point now or in the future. 108 * `_Bool $read(<memory-list>)`105 * `_Bool \read(<memory-list>)` 109 106 * holds if any memory unit in the list may be read by `p` at some point now or in the future. 110 107 111 Default: if there is no ` $depends` clause present, the dependency information will be obtained from Java code in the library enabler. If the library enabler does not specify anything for this function, the default rules will be used, which are sound:108 Default: if there is no `depends` clause present, the dependency information will be obtained from Java code in the library enabler. If the library enabler does not specify anything for this function, the default rules will be used, which are sound: 112 109 * if the body of the function is not provided, i.e., the function is a system function, the verifier will assume that execution of the function may read and/or modify any memory unit that it can reach, and decide on the partial order reduction appropriately, else 113 110 * if the body of the function is present, the statements comprising the body may be analyzed to further restrict the reduction. … … 176 173 === Use of `$depends` === 177 174 178 In the case where S is a function call, the ` $depends` clause in the function contract specifies the175 In the case where S is a function call, the `depends` clause in the function contract specifies the 179 176 set A(s,S,p) as follows: first the depends clause specifies a predicate d(s,q) where s is a state and 180 177 q is a proc. Then … … 204 201 - The following means that any process that can reach the memory unit of `comm` should be in the ample set if the current process (`$self`) is to be chosen in the ample set. 205 202 {{{ 206 /*@ $depends $access(*comm); */203 /*@ depends \access(*comm); */ 207 204 void comm_dequeue($comm comm, ....); 208 205 }}} … … 216 213 /*@ requires scope <= $root; 217 214 @ requires size >= 0; 218 @ $depends \nothing;219 @ $guards $true;215 @ depends \nothing; 216 @ guards true; 220 217 @ assigns \nothing; 221 218 @ */ … … 226 223 /* Destroys the gbarrier */ 227 224 /*@ requires barrier != \null; 228 @ $guards $true;229 @ $depends \nothing;225 @ guards true; 226 @ depends \nothing; 230 227 @ assigns barrier;//barrier has pointer type, and is converted into $memory type automatically 231 228 @ */
