More evaluation for crucible_term and friends

[robdockins]

When processing SAWCore terms that will be injected into the symbolic simulator, the current default behavior is to generate a fresh What4 symbolic variable to represent that term and record this binding in a lookup table (except in very limited special cases where we can easily recognize literal values). Then, when the simulator is finished, the resulting What4 terms are interpreted back into SAWCore; the freshly-created variables are replaced with their original SAWCore meanings.

This process is sound, but prevents the symbolic simulator from accessing the meanings of terms in most cases. This can be very problematic, as it may prevent symbolic termination, interferes with path-sat checking, and may cause necessary "potential" override matches and generally results in less-precise-than-possible results.

On the other hand, we cannot just evaluate every single SAWCore term destined for the simulator. Some constructs cannot be faithfully represented in What4; and in many cases full evaluation is undesirable anyway, as it would lead to a large amount of wasted work translating terms back and forth from SAWCore. This is especially true for compositional verification, where subcomponents of the computation are explicitly intended to be treated as black boxes for later stages of verification.

Instead, we will likely need a more flexible system for determining which terms should be "transparent" to this translation and which should be "opaque". As a first approximation, we will treat functions defined in the SAWCore and Cryptol preludes as being transparent, and other terms as being opaque. We will probably want a UI to allow users to override these defaults at some point, but I believe this is a good starting point.

This ticket is intended to track design discussions and ongoing work regarding this general issue.

[robdockins]

Some initial experiments have validated my concerns that simply fully evaluating SAWCore to be sent to the simulator results in unacceptable space and time usage in even fairly simple examples. Some changes will be needed to the saw-core simulator to handle cases where we want evaluation to "block" on function calls we can't or don't want to unfold.

[brianhuffman]

I've done experiments with similar things in the past (see for example the commit message for 2673178). For small, closed expressions like 1 << 7 we definitely want to evaluate them, but if the expression contains a strong cryptographic algorithm it might be quite expensive to evaluate, so I've also found that evaluating everything is not the right approach.

It seems like the two reasonable choices are either relying on heuristics to decide whether/how much to evaluate, or else give more control to saw-script users. One idea I had was making two variants of the saw-script function crucible_term, one that evaluates its argument and one that doesn't.

[robdockins]

Status: PR #887 adds evaluation of SAWCore terms to What4 values at bitvector and boolean types during the "setup value resolution" phase for LLVM verification. It will abandon evaluation if it must unfold the definition of any Cryptol function that is not part of the prelude and not a locally let-bound definition, falling back on the previous behavior (which treats the whole value as uninterpreted during symbolic evaluation). This heuristic largely seems to have the "expected" effects, and allows better path-satisfiability checking, etc.

However, it also causes significant (around %200) slowdowns in some of our benchmark proofs, for reasons I don't yet understand.