Comparison

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

1. Parse individual programs
2. Examine input variables, check that spec inputs are a subset of impl inputs.
   • It's ok for the impl to have extra inputs.
3. Examine output variables, check that sets of spec and input output variables are the same.
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; ?)
   • 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.
5. Check that assumptions are consistent in spec and impl. (Is it sufficient to check assumptions in the file scope only?)
   • 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.
   • 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).
   • Let p(X) be the conjunction of assumptions in the spec and q(X,Y) be the conjunction of assumptions in the impl.
   • Check that p(X) implies there exists an assignment to all variables in Y such that q(X,Y) is valid.
   • If the prover can't answer, provide a warning.
   • If assumptions involving input variables are located outside of the file scope, provide a warning.
6. Create functions for the spec and impl that wrap the sequence of nodes at the file scopes.
7. Create a new sequence node. Add the following to it:
   1. The union of the set of input variables. Remove inputs from spec and impl
   2. All (renamed) output variables. Remove outputs from spec and impl
   3. The functions for spec and impl
   4. One copy of each of the civlc.h functions (remove from spec and impl)
   5. Spawn statements for spec and impl
   6. Wait statements for spec and impl
   7. 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. Maybe we need to have a flag indicating that this assertion is special and can read output variables without error? Or, make a system function for comparing output variables that doesn't have this restriction and can directly compare symbolic expressions for arrays, etc.