Implement evaluation harness for specifications

[jyoo980]

We'll need a way to evaluate our specifications. There are two things we want to do.

Mutation-based Evaluation

This might help us evaluate whether the specifications generated by Avocado are actually helpful. The general idea is, given a verifying spec S for a function F.

• Mutate the body of F with standard mutation operators, resulting in mutants F_1, F_2, F_3, ..., F_n
• Attempt to verify each mutant with the spec S.
  • If a mutant still verifies under S, this implies that S isn't adequately capturing the underlying semantics of the program.
• Kill score is calculated as usual.

Metrics for specification characteristics

For each specification, we should calculate

• Number of atoms in a clause (e.g., __CPROVER_ensures(a || b || c) -> 3 atoms)
  • Proxy measure for complexity.
• Number of expressions that reduce to either True or False
  • Obviously, the lower this number the better.

Evaluating Specification Completeness

Try to generate the body of a function given the specification for it, and compare it to the original function.