search

GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
617 stars 42 forks source link

`popFrameUnchecked` changes cause regression in SAW AWS-LC proof #1181

Open RyanGlScott opened 4 months ago

RyanGlScott commented 4 months ago

While working on https://github.com/GaloisInc/saw-script/pull/2037, I discovered that the changes in commit c1f38003465fd263fe2bb229adf123ee05197e80 (part of https://github.com/GaloisInc/crucible/pull/1169) caused a regression in the llvm_verify_fixpoint_x86 proof for sha512_data_block_order, which is part of the AWS-LC proofs that are run in SAW's CI. Here is the specific error:

[18:41:16.589] Finding symbol for "sha512_block_data_order"
[18:41:16.642] Found symbol at address 0x7066c0, building CFG
[18:41:17.326] Simulating function "sha512_block_data_order" (at address 0x7066c0)
[18:41:17.326] Examining specification to determine preconditions
[18:41:18.628] Simulating function
[18:41:26.002] Examining specification to determine postconditions
[18:41:27.170] Simulation finished, running solver on 35 goals
[18:41:28.429] Subgoal failed: 0x707ef8: error: in sha512_block_data_order
Error during memory load
[18:41:28.429] SolverStats {solverStatsSolvers = fromList ["W4 ->z3"], solverStatsGoalSize = 224}
[18:41:28.429] ----------Counterexample----------
[18:41:28.429]  num: 57578523786673063
[18:41:28.429]  reg_join_var: 7370051044694152064
[18:41:28.429] ----------------------------------
[18:41:28.430] Stack trace:
"include" (/saw-script/aws-lc-verification/SAW/proof/SHA512/verify-SHA512-384-quickcheck.saw:11:1-11:8)
"include" (/saw-script/aws-lc-verification/SAW/proof/SHA512/SHA512.saw:6:1-6:8)
"llvm_verify_fixpoint_x86" (/saw-script/aws-lc-verification/SAW/proof/SHA512/SHA512-common.saw:337:37-337:61)
Proof failed.

This is pretty surprising, given that the changes in c1f38003465fd263fe2bb229adf123ee05197e80 are almost all pure refactoring-related changes. I don't fully understand what caused the proof to change, but my current guess is that popFrameUnchecked now always completes an atomicModifyIORef' transaction rather than panicking halfway through the transaction, which may wreak havoc with exception-handling code somewhere.

For now, I am going to revert #1169. That being said, we should strive to better understand what is going on here.

kquick commented 4 months ago

Looking at https://github.com/GaloisInc/crucible/commit/c1f38003465fd263fe2bb229adf123ee05197e80 I see that in the second replacement, the original return was (poppedCollector frm, ...) and the updated version returns (collectPoppedGoals frm, ...). I have not looked at the difference between poppedCollector and collectPoppedGoals, but that may be one avenue to pursue in resolving this.

RyanGlScott commented 4 months ago

Ah, I had completely overlooked that. Indeed, that feels like a far more plausible explanation than what I came up with.