Explain why no overrides matched (Crucible LLVM)

[langston-barrett]

When no override matches (after structural matching, for that case see #391), SAW prints

Symbolic execution failed.
Abort due to false assumption:
  no override specification applies for SHA256_Init
  in overrideBranches at /build/fizz-hkdf/main.saw:192:1

This isn't very informative! It would be much better to record and print the reasons that each override failed to apply and present this to the user.

[langston-barrett]

It seems that what's going on when the user sees

"no override specification applies for " ++ fnName

is that there are a collection of overrides, each of which has an attached Pred sym which summarizes its preconditions, and all of these Preds are evaluating to false.

The problem, then, is that a single Pred can't really provide meaningful information on why an override failed to match (e.g. which precondition failed to hold?). This is probably a good place to apply the techniques and datastructures introduced in GaloisInc/crucible#151, as they solve essentially the same problem as it arises during symbolic simulation.

[langston-barrett]

Results from an offline conversation with @robdockins:

Observations

The way we end up selecting an override is by building up a somewhat complex continuation structure inside Crucible that symbolically branches on each precondition predicate, effectively trying each override's preconditions in order and selecting the first one that succeds. This information doesn't propagate back up to the SAW level, i.e. we don't learn which predicates succeeded or failed.

Now, we do have a list of conjoined, labeled predicates that make up the preconditions for each override. However, this isn't quite as helpful as it seems: an override's preconditions fail when the conjunction of the preconditions is false, which may not result from any individual conjuncts being false, but perhaps from an inconsistency among them.

Possible solutions

A first step which is both simple and generally useful (might improve performance) is to check if any overrides' preconditions are concretely false with asConstantPred. If all overrides failed to match, we can print out which conditions failed concretely.

A possible next step would be to narrow down why the conjoined symbolic predicates failed. The best tool for that job is likely the "unsatisfiable core" feature of some SMT solvers. However, this could be excessively detailed for the current problem.

A halfway point between the above options would be to go through the preconditions one at a time and use considerSatisfiability to determine if it is indeed a single conjunct that is failing. This is a kind of homespun version of computing certain unsatisfiable cores.