| | 1 | == Comparison == |
| | 2 | |
| | 3 | Here is a sketch of combining ASTs of a spec and impl in order to form a composite program. In compare mode, CIVL will take two programs as arguments. We treat the first program as the "spec" and the second as the "impl." |
| | 4 | |
| | 5 | 1. Parse individual programs |
| | 6 | 2. Examine input variables, check that spec inputs are a subset of impl inputs. |
| | 7 | - It's ok for the impl to have extra inputs. |
| | 8 | 3. Examine output variables, check that sets of spec and input output variables are the same. |
| | 9 | 4. Rename output variables in both programs. (maybe we should just do this in the spec? e.g. for $output int x;, have $output int x_spec; and $output int x; ?) |
| | 10 | - We're going to need to compare output variables, and so will need the outputs for each program moved to the new artificial "file" scope. |
| | 11 | 5. Check that assumptions are consistent in spec and impl. (Is it sufficient to check assumptions in the file scope only?) |
| | 12 | - Need to check that assumptions in the impl don't prevent any of the valid inputs to the spec from occurring. e.g. suppose spec inputs are `x,y` and impl inputs are `x,y,z`. If `x=0,y=1` is a legal input for the spec, then there must exist some value `z_0` of `z` such that `x=0,y=1,z=z_0` is a legal input to the impl. |
| | 13 | - Let `X` be the set of inputs to the spec and `Y` be the set of inputs in the impl not corresponding to inputs in the spec (i.e. `X` and `Y` are disjoint and `X` union `Y` is the full set of inputs to the impl). |
| | 14 | - Let `p(X)` be the conjunction of assumptions in the spec and `q(X,Y)` be the conjunction of assumptions in the impl. |
| | 15 | - Check that `p(X)` implies there exists an assignment to all variables in `Y` such that `q(X,Y)` is valid. |
| | 16 | - If the prover can't answer, provide a warning. |
| | 17 | - If assumptions involving input variables are located outside of the file scope, provide a warning. |
| | 18 | 6. Create functions for the spec and impl that wrap the sequence of nodes at the file scopes. |
| | 19 | 7. Create a new sequence node. Add the following to it: |
| | 20 | i. The union of the set of input variables. Remove inputs from spec and impl |
| | 21 | ii. All (renamed) output variables. Remove outputs from spec and impl |
| | 22 | iii. The functions for spec and impl |
| | 23 | iv. One copy of each of the civlc.h functions (remove from spec and impl) |
| | 24 | v. Spawn statements for spec and impl |
| | 25 | vi. Wait statements for spec and impl |
| | 26 | vii. Assertions checking equality of each pair of output variables. e.g. suppose `x` is an output variable. If the variables are renamed `x_spec` and `x_impl`, an assertion `$assert(x_spec==x_impl);` will be added. |
