Structured assertions

[langston-barrett]

Motivation

Execution of syntax extensions produces values whose validity depends on the
truth of certain (symbolic) predicates (call such predicates "safety
assertions"). The values are often operated on further, compounding and
combining their paired safety assertions. When these safety assertions are
actually discharged, it would be nice to be able to explain to users why
symbolic simulation failed.

The current state of affairs

Assertions arise both at runtime, when instructions are being executed, and
as expressions at translation time. The way these are dealt with right now
is:

• Runtime: use What4's PartExpr datatype (isomorphic to
  Maybe (Value, Predicate)) with the predicate summing up all the
  assertions made
• Translation time: use the AddSideCondition constructor of Crucible's
  Expr with a pair of (Predicate, Explanation)

The downsides of this approach are:

• these are totally disparate approaches, even though the same kinds of
  assertions are being made
• the information contained in the error messages varies widely
• there is no ability to programatically select which assertions should
  be made

Design

There are a few observations that influce the design here:

1. The type of safety assertions is specific to the syntax extension in
   operation. Java and LLVM have different things to assert.
2. Some operations on safety assertions can be shared between extensions,
   and so should go in Crucible proper.
3. Assertions need to be constructed both at CFG-building time and at
   symbolic execution time.

These lead to the following design decisions:

1. The open type family AssertionClassifier, keyed on the syntax extension
2. The implementation of the HasStructuredAssertions class

For runtime assertions, the new idea is that partial values should be
(isomorphic to) a pair (Value sym, AssertionTree sym) where
AssertionTree sym is a tree which has boolean connectives (and, or, ite)
as non-leaf vertices and predicates together with classifiers and
explanations as leaves.

Since assertions can also come up at translation time, the type family is
parameterized over a type of expressions e :: CrucibleType -> Type that gets
converted from Expr ext s f at translation time to RegValue sym ty at
runtime. This allows for predicates to be constructed using Crucible syntax at
translation time. The safety assertions will participate in the translation
process so they can be asserted at runtime.

Possible next steps

• Allow for programatic filtering of exceptions in the HasStructuredAssertions class
• Simplify assertion trees using asConstantPred
• Allow for a sliding scale of verbosity
• Merge the modes of expression-level and statement-level assertions
• Implement in other syntax extensions (JVM, Macaw)
  • More highly structured assertions for JVM
• Implement some kind of flag around whether the value has the semantics of undef
  or poison when the assertion fails

[langston-barrett]

I think this would be most useful (and reduce most duplication) if I try to get rid of What4.PartExpr altogether (at least in crucible-llvm). I'm going to look into doing that in this PR.

[robdockins]

Can we avoid this unsafeCoerce? I don't understand the correctness argument you're making here in this comment, and it seems like it depends on the OrdC instance in a nontrivial way that makes me uneasy.

[langston-barrett]

Yeah, the issue is that we don't have the type-level evidence we need in this branch, but we can't say these things are unequal. This is a pretty fundamental issue because of the shift from PartExr p v ~= Maybe (p, v) to a type more like (p, Maybe v). I wonder if we can get rid of the Maybe altogether, there should be reasonable "zero" values for each type... I'll look into that.

[langston-barrett]

I've done away with the Maybe here, see "What4.Partial". This actually led me to combine the ideas from a few different types expressing partiality, and I think leads to a better overall solution.

[robdockins]

FYI, I did a merge with master and pushed into branch partllvmval, you'll probably want to pull from there

[langston-barrett]

I think this is generally ready for review, with the caveat that it might be hard to get Crucible to exhibit these structured messages, because the way memory reads work is to calll a "fallback" function readPrev whenever what you're currently trying fails. It's sort of a backtracking algorithm

[robdockins]

There's a pretty big merge conflict with the refactoring related to registering intrinsics. Can you take a look @siddharthist? I can't tell if there are changes that need to be preserved.

[langston-barrett]

Yep!

[langston-barrett]

@robdockins This is current again.