Call to scGeneralizeExts in crucible_llvm_verify is a performance bottleneck

[brianhuffman]

Profiling shows that on some proof goals (some of the s2n proofs in particular), the following call to scGeneralizeExts takes up a significant portion of the total runtime of crucible_llvm_verify:

saw-script/src/SAWScript/Crucible/LLVM/Builtins.hs

Line 403 in faf2dee

goal' <- io $ scGeneralizeExts sc (getAllExts goal) =<< scEqTrue sc goal

There is also similar call to scGeneralizeExts in crucible_jvm_verify:

saw-script/src/SAWScript/Crucible/JVM/Builtins.hs

Line 276 in faf2dee

goal' <- io $ scGeneralizeExts sc (getAllExts goal) =<< scEqTrue sc goal

The purpose of scGeneralizeExts is simply to convert external constants into local variables, which the saw backends were initially designed to handle. Instead of doing this possibly-expensive pre-processing step, we should just make sure that the various saw-core simulator backends can handle external constants in the same way that they handle local variables.

[robdockins]

Indeed, there are some places where we close over all the external constants, only to immediately open them up again with fresh constants, or vice versa. We should change the convention so that provers accept external constants also (or, maybe better, instead of) lambda-bound variables.

This would also make it significantly easier to do some of the things we want to do with counterexamples. I ran into trouble trying to work on this before because tracking the identity of the free variables is very difficult when they get abstracted into lambdas.