SAW simulator backend performance regressions

[brianhuffman]

Some uses of SAW simulator backends have slowed down by a factor of about 6x since the saw-0.7 release in Dec 2020. I noticed the regression in a proof script that proved a bunch of rewrite rules using prove_print with the rme tactic. (Unlike many calls to external provers, the actual solver time here is fast enough that the simulator overhead is the dominant factor in the total time.)

The slowdown did not happen all at once; saw-0.8 was about 3x slower that 0.7, and then the current master version of saw is another 2x slower than 0.8. I did a series of bisections and identified a few points where the proof times jumped by noticeable amounts:

• b0df5ea bumped saw-core to include Switch from GlobalDef to Constant for definitions in .sawcore files. saw-core#118 (of which GaloisInc/saw-core@9dfb209 is the important commit). ~3x slowdown
• e360dcc "Add type information to the simulator evaluation environment", ~30% slowdown
• 4270bae "Implement a new Prim type, which is used for implementing primitives", ~40% slowdown
• c446e1f "Bump cryptol submodule, update withSolver calls", ~10% slowdown

[brianhuffman]

Currently the saw-core simulator is implemented in such a way that it makes two passes over each term. We should reimplement it such that it only requires a single pass.