search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
437 stars 63 forks source link

Use a single persistent solver connection for typechecking cryptol #953

Open brianhuffman opened 3 years ago

brianhuffman commented 3 years ago

For testing purposes I recently tried running examples/ecdsa/ecdsa-crucible.saw using crucible_jvm_unsafe_assume_spec instead of crucible_jvm_verify throughout. I expected everything to run really fast, but it was not nearly as fast as I had hoped to see. Some specs took well over a second to process:

[14:43:20.749] Skipping verification of ec_twin_mul_init
[14:43:21.593] Time: 0.843762s

[14:43:21.594] Skipping verification of ec_twin_mul
[14:43:22.231] Time: 0.637015s

[14:43:22.235] Skipping verification of signHash
[14:43:23.920] Time: 1.685543s

[14:43:23.924] Skipping verification of verifySignature
[14:43:25.364] Time: 1.440212s

I was surprised to see these specs take so long because crucible_jvm_unsafe_assume_spec doesn't really do much, other than check to see that everything in the spec is type-correct and otherwise well-formed.

Using unsafe_assume_spec, the entire file takes a bit over 15 seconds to run. (For comparison, the file takes about 4:30 or so with all the symbolic simulation and proofs turned on.)

Profiling shows that crucible_jvm_unsafe_assume_spec takes up about half of the total runtime. Of that, practically all of it is taken up by running parseTypedTerm on the embedded cryptol syntax {{ }}. parseTypedTerm appears to be called several hundred times in total.

We should see what we can do to reduce the cost of running parseTypedTerm lots of times.

brianhuffman commented 3 years ago

The profiling output shows that within parseTypedTerm, the function loadTcPrelude takes up a fifth of the runtime and 2/3 of the memory allocation. We could probably speed this up a lot with some pre-processing, because currently it seems to be taking the raw String contents of CryptolTC.z3, stripping comments, parsing S-expressions, and then prettyprinting SMT output over and over.

brianhuffman commented 3 years ago

Instead of making the processing of CryptolTC.z3 faster, a much more promising solution would be to just process CryptolTC.z3 and send it to the solver once. Apparently the Cryptol library interface will need to be modified to support this (see GaloisInc/cryptol#996).

brianhuffman commented 3 years ago

PR GaloisInc/saw-core#197 adapts cryptol-saw-core to work with GaloisInc/cryptol#1128, which adds support for maintaining a single persistent connection to z3 for typechecking purposes instead of opening a separate connection each time a term is typechecked. As suggested in the comment thread for #197, we could take advantage of this by storing the solver instance inside the CryptolEnv.