search

GaloisInc / saw-script

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

`resolveSAWTerm` is a performance bottleneck #897

Open brianhuffman opened 4 years ago

brianhuffman commented 4 years ago

Function resolveSAWTerm in module SAWScript.Crucible.JVM.ResolveSetupValue, which is used to implement points_to declarations when running method overrides, can cause extreme slowdowns in symbolic simulation runs where overrides are used many times.

For example, the verification of method ec_mul in ecdsa-crucible.saw uses ec_mul_aux in a loop, and the symbolic simulation run takes over 2 minutes on my machine. For comparison, the same subproof in the old-style ecdsa.saw takes only 9 seconds, including prover time. https://github.com/GaloisInc/saw-script/blob/d7a335d32db4ad4044c346e4bd42c6e51fc27f0d/examples/ecdsa/ecdsa-crucible.saw#L1476

Profiling shows that the more than 90% of the symbolic simulation time is spent in resolveSAWTerm. Of this, about 70% is spent computing the set of free variables (which GaloisInc/saw-core#100 helps with) and the other 30% is spent in bindSAWTerm from Lang.Crucible.Backend.SAWCore in the crucible-saw package.

I expect that the corresponding function is similarly slow in LLVM verification as well, as it is implemented the same way.

brianhuffman commented 4 years ago

GaloisInc/crucible#581 helps to speed up bindSAWTerm a fair amount.

brianhuffman commented 3 years ago

Here's another more recent data point: With the current master (a9e13c2dc94725c69aec04a9b800a09684e5b51c) I just ran a profiling build on the keygen.saw proof script from blst-verification, which is run as part of saw-script CI. The profiling results show that about half of the total runtime is spent on calls to sbvSolveBasic on this one line in resolveSAWSymBV: https://github.com/GaloisInc/saw-script/blob/0297c1fe7e614b58f68a08e22ea4d896658ab125/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs#L400-L401