Measure contract symbolic coverage

One of the arguments against property testing as an approach to formal verification is about the coverage of the approach. In order to fix that, we want to demonstrate that we are able to achieve full 100% coverage of a smart contract with property testing (or at least, show the user where their property tests are deficient). To do so, we'll provide a "symbolic coverage" metric for people's smart contracts.

Supposed we have two tests:

function test_f_1(uint x) {
  vm.assume(x <= 10);
  // point 1
  uint y = MyContract.f(x);
  vm.assert(y == 0);
}

function test_f_2(uint x) {
  vm.assume(10 < x);
  // point 2
  uint y = MyContract.f(x);
  vm.assert(y != 0);
}

function test_f_3() {
  // point 3
  uint y = MyContract.f(238);
  vm.assert(y != 0);
}

Have we covered all the possible inputs that MyContract can take? teh answer here is "No", because we have not covered the cases of illformed calldata (calling a function that doesn't exist, or calling f with bad calldata). How can we tell the user that?

We need to extract from the KCFGs of the executions of test_f_{1,2} the states at point 1 and point 2, and union those states together. Then we negate that union of those states, and check that the negation is empty.

For example, if we did not have test_f_2 above, we would want the backend to construct the state MyContract.f(x) #And #Not (x <= 10), and that would detect a case MyContract.f(x) #And (10 < x), and it should report back: "You need to have a property test for case f(x) #And (10 < x).".

Start by examining the KCFGs for executions of test_f_1 and test_f_2, focusing on the states at point 1 and point 2. The work is done when those states can be unioned and negated to detect uncovered inputs, including ill-formed calldata, and report a missing property-test case such as f(x) #And (10 < x).