|
| 1 | +# Generating GOTO Functions From Contract Clauses {#contracts-dev-spec-codegen} |
| 2 | + |
| 3 | +Back to top @ref contracts-dev-spec |
| 4 | + |
| 5 | +@tableofcontents |
| 6 | + |
| 7 | +## Translating Assigns Clauses to GOTO Functions {#contracts-dev-spec-codegen-assigns} |
| 8 | + |
| 9 | + |
| 10 | +Let's consider a contract `foo` (with corresponding pure contract |
| 11 | +`contract::foo`) with a `__CPROVER_assigns(A)` clause. |
| 12 | + |
| 13 | +```c |
| 14 | +ret_t foo(foo-parameters) __CPROVER_assigns(A); |
| 15 | +``` |
| 16 | +We know the elements of A only depend on `foo-parameters` and global variables. |
| 17 | +
|
| 18 | +A new GOTO function with the following signature is generated: |
| 19 | +
|
| 20 | +```c |
| 21 | +void contract::foo::assigns(foo-parameters); |
| 22 | +``` |
| 23 | + |
| 24 | +The body of the function generated from the elements of A as follows: |
| 25 | +- For each target `cond: target` where the target is an lvalue expression: |
| 26 | + ```c |
| 27 | + DECL __cond: bool; |
| 28 | + ASSIGN __cond = <result of goto_convert(cond)>; |
| 29 | + IF !__cond GOTO SKIP_TARGET; |
| 30 | + CALL __CPROVER_assignable(&target, sizeof(target), has_ptr_type(target)); |
| 31 | + SKIP_TARGET: SKIP; |
| 32 | + DEAD __cond; |
| 33 | + ``` |
| 34 | + where `has_ptr_type(target)` returns true if the target has a pointer-type; |
| 35 | +- For each target `cond: f(parameters)`, where `f` is a void-typed function: |
| 36 | + ```c |
| 37 | + DECL __cond: bool; |
| 38 | + ASSIGN __cond = <result of goto_convert(cond)>; |
| 39 | + IF !__cond GOTO SKIP_TARGET; |
| 40 | + CALL f(parameters); |
| 41 | + SKIP_TARGET: SKIP; |
| 42 | + DEAD __cond; |
| 43 | + ``` |
| 44 | + |
| 45 | +Remark: The condition expressions needs to be goto_converted during translation |
| 46 | +since they come directly from the front-end and are allowed to contain function |
| 47 | +calls. |
| 48 | + |
| 49 | +The rewriting pass @ref contracts-dev-spec-spec-rewriting-assigns is applied |
| 50 | +to transform the function into a function that accepts two |
| 51 | +write set parameters: The first one is the write set that gets populated with |
| 52 | +assignable locations specified by the function, the second is a write set that |
| 53 | +is used by the function to check its side effects. |
| 54 | + |
| 55 | +```c |
| 56 | +void contract::foo::assigns( |
| 57 | + |
| 58 | + // function parameters |
| 59 | + foo-parameters, |
| 60 | + |
| 61 | + // write set to populate with new targets |
| 62 | + __CPROVER_contracts_write_set_ptr_t __write_set_to_fill, |
| 63 | + |
| 64 | + // write set against which to check itself for unwanted side effects |
| 65 | + __CPROVER_contracts_write_set_ptr_t __write_set_to_check); |
| 66 | +``` |
| 67 | +
|
| 68 | +The rewriting step @ref contracts-dev-spec-spec-rewriting-havoc is also applied |
| 69 | +to the function in order to generate a havoc function that can be used to model |
| 70 | +contract replacement: |
| 71 | +
|
| 72 | +```c |
| 73 | +void contract::foo::havoc(__CPROVER_contracts_write_set_ptr_t __write_set_to_havoc); |
| 74 | +``` |
| 75 | + |
| 76 | +## Translating Frees Clauses to GOTO Functions {#contracts-dev-spec-codegen-frees} |
| 77 | + |
| 78 | +Let's consider a contract `foo` (with corresponding pure contract |
| 79 | +`contract::foo`) with a `__CPROVER_frees(F)` clause. |
| 80 | + |
| 81 | +```c |
| 82 | +ret_t foo(foo-parameters) __CPROVER_frees(F); |
| 83 | +``` |
| 84 | +We know the elements of F only depend on `foo-parameters` and global variables. |
| 85 | +
|
| 86 | +A new GOTO function with the following signature is generated: |
| 87 | +
|
| 88 | +```c |
| 89 | +void contract::foo::frees(foo-parameters); |
| 90 | +``` |
| 91 | + |
| 92 | +The body of the function generated from the elements of F as follows: |
| 93 | +- For each element of the form `cond: expr` where `expr` is a pointer-typed |
| 94 | + expression: |
| 95 | + ```c |
| 96 | + DECL __cond: bool; |
| 97 | + ASSIGN __cond = <result of goto_convert(cond)>; |
| 98 | + IF !__cond GOTO SKIP_TARGET; |
| 99 | + CALL __CPROVER_freeable(expr); |
| 100 | + SKIP_TARGET: SKIP; |
| 101 | + DEAD __cond; |
| 102 | + ``` |
| 103 | +- For each target of the form `cond: f(params)` where `f` is a void-typed |
| 104 | + function: |
| 105 | + ```c |
| 106 | + DECL __cond: bool; |
| 107 | + ASSIGN __cond = <result of goto_convert(cond)>; |
| 108 | + IF !__cond GOTO SKIP_TARGET; |
| 109 | + CALL f(params); |
| 110 | + SKIP_TARGET: SKIP; |
| 111 | + DEAD __cond; |
| 112 | + ``` |
| 113 | + |
| 114 | +Remark: The condition expressions needs to be goto_converted during translation |
| 115 | +since they come directly from the front-end and are allowed to contain function |
| 116 | +calls. |
| 117 | + |
| 118 | +The resulting function is declarative, in the sense that it describes the |
| 119 | +contents of the frees clause but does not have any runtime effects. |
| 120 | + |
| 121 | +The rewriting pass @ref contracts-dev-spec-spec-rewriting-frees is applied |
| 122 | +to transform the function into a function that accepts two |
| 123 | +write set parameters: The first one is the write set that gets populated with |
| 124 | +freeable pointers specified by the function, the second is a write set that is |
| 125 | +used by the function to check its side effects. |
| 126 | + |
| 127 | +```c |
| 128 | +void contract::foo::frees( |
| 129 | + |
| 130 | + // function parameters |
| 131 | + foo-parameters, |
| 132 | + |
| 133 | + // write set to populate with new targets |
| 134 | + __CPROVER_contracts_write_set_ptr_t __write_set_to_fill, |
| 135 | + |
| 136 | + // write set against which to check itself for unwanted side effects |
| 137 | + __CPROVER_contracts_write_set_ptr_t __write_set_to_check); |
| 138 | +``` |
| 139 | +
|
| 140 | +--- |
| 141 | + Prev | Next |
| 142 | +:-----|:------ |
| 143 | + @ref contracts-dev-spec-transfo-params | @ref contracts-dev-spec-spec-rewriting |
0 commit comments