popFrameUnchecked changes cause regression in SAW AWS-LC proof

[RyanGlScott]

While working on GaloisInc/saw-script#2037, I discovered that the changes in commit c1f3800 (part of #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 c1f3800 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]

Looking at c1f3800 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]

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