uc-crux-llvm: Improve data model

[langston-barrett]

Today, UC-Crux works like this:

• Symbolically execute a function
• Maybe hit an error
• Classify the error as:
  • A likely bug
  • A missing precondition that it knows how to work around (i.e., generate new data conforming to)
  • A missing precondition that it doesn't know how to work around
  • Unknown
• Generate per-function reports/summaries of how errors were classified

This has worked OK so far, but there are a few issues:

1. Errors aren't deduplicated - If exploration of two functions encounters the same issue on the same line, the user sees it counted twice in reports
2. UC-Crux basically just gives up on all of the "unknowns", which is probably where any actual bugs are buried

Focusing on (2): Since there are always going to be issues/errors that are too complicated to work around by explicitly deducing new preconditions on the function's inputs (see e.g., "Inability to Infer Relations Between Arguments" in the blog post), to do better on these errors will require a more advanced strategy than exploring one function at a time and drawing all the conclusions about what's a bug or not on the spot.

One example of such a strategy would be to explore whether a given error is reachable from the callers of the function that it's contained in, or their callers, etc. all the way back to the program's entry point(s). Data like this could be combined with simple heuristics such as the ones currently implemented or other information when considering how/if to describe the error in reports.

To make use of strategies like this, "possible errors" will need to be explicitly reified as a concept in UC-Crux, perhaps along these lines:

data ProgErrorType
  = UninitializedStackRead
  | OOBHeapWrite
  | SignedAdditionOverflow
  -- ... see also Lang.Crucible.LLVM.Errors 

-- | A possible error encountered while exploring the target program
data ProgError
  = ProgError
      { progErrorType :: !ProgErrorType
      , progErrorLoc :: !ProgramLocation
      }
  deriving (Eq, Ord)

Fuzzers also have the problem of deduplicating errors, so there might be valuable insights from that community on how to model "a bug".

[langston-barrett]

Another wart is in the Uncertainty datatype, which captures both uncertain results due to the failure of the precondition-deducing heuristic, and failure due to other issues such as solver timeouts or hitting loop bounds. These should be distinguished and put into separate types.

[langston-barrett]

UC-Crux basically just gives up on all of the "unknowns", which is probably where any actual bugs are buried

We could do better than this without doing any kind of callgraph-based/reachability analysis, but instead by integrating the heuristics identified in the original UC-KLEE paper: must-fail, belief-fail, and concrete-fail (concrete-fail is mostly there already).