Add vacuity detection in MIR and JVM backends.

[sand7000]

• Extracted vacuity logic (checkAssumptionsForContradictions, etc.) into a new backend independent module: SAWCentral.Crucible.Common.Vacuity.
• Hooked vacuity checks into:
  • mir_verify in SAWCentral.Crucible.MIR.Builtins
  • jvm_verify in SAWCentral.Crucible.JVM.Builtins
  • verifyMethodSpec and refineMethodSpec in SAWCentral.Crucible.LLVM.Builtins

Fixes #2028

[sand7000]

This PR addresses all prior review feedback:

• Restored original comments. I had temporarily removed them while reviewing the code to better understand it, but preserving them is preferable.
• Removed GenericCrucibleContext. Passing sym directly is sufficient, as suggested.
• Added an integration test covering vacuity detection across LLVM, MIR, and JVM backends.
• Added an entry to the changelog.

I opted to open a new PR with a single additional commit rather than rewriting commit history to include the issue reference (#2028), to avoid disrupting references from the original PR.

[RyanGlScott]

This is looking nice!

Do you know what is causing this test failure?

  test2028_vacuity_detect:             Expected 3 contradictions, found 0

test.sh: line 3: eval saw  -j '/home/runner/work/saw-script/saw-script/intTests/jars/bcprov-jdk16-145.jar:/home/runner/work/saw-script/saw-script/intTests/jars/galois.jar:/home/runner/work/saw-script/saw-script/intTests/jars/org.sat4j.core.jar': No such file or directory

FAIL
    intTests/IntegrationTest.hs:185:
    expected: ExitSuccess
     but got: ExitFailure 1
    Use -p '/test2028_vacuity_detect/' to rerun this test only.

[RyanGlScott]

Note that --detect-vacuity is already tested in the LLVM backend as part of the test0064_detect_vacuity test case. I'd favor removing the LLVM-specific parts from test2028_vacuity_detect to avoid redundancy. (It might be worth referring to test0064_detect_vacuity from test2028_vacuity_detect/README.)

[sand7000]

I'll make the suggested changes to avoid redundancy.

As for the test failure, I haven't figured out exactly why the runner fails. I tested the case manually in a SAW Docker container built from my changes, and it worked as expected (see below). I suspect the test runner doesn't like how I invoke the SAW command in the script, maybe due to how $SAW is formatted or evaluated.

Unless you have a better suggestion, I'll split the test into two shell scripts (JVM and MIR) and rely on the existing LLVM test to cover that backend.

docker run -it --rm   --entrypoint /bin/bash   -v "$PWD":/workdir   -v "$PWD/cryptol-specs":/cryptol-specs   -v "$HOME/jdk8-classes":/jdk   -w /workdir   -e CRYPTOLPATH=/cryptol-specs   -e CLASSPATH=/jdk:/workdir -e SAW=saw  saw:vacuity
saw@194779f19baa:/workdir$ bash test.sh 
[21:17:24.843] Loading file "test.saw"
[21:17:24.877] Verifying fun_c ...
[21:17:24.887] Contradiction detected! Computing minimal core of contradictory assumptions:
[21:17:24.902] ConditionMetadata {conditionLoc = ProgramLoc {plFunction = llvm_precond, plSourceLoc = test.saw:6:3}, conditionTags = fromList [], conditionType = "specification assertion", conditionContext = ""}: precondition
[21:17:24.902] Because of the contradiction, the following proofs may be vacuous.
[21:17:24.902] Simulating fun_c ...
[21:17:24.903] Checking proof obligations fun_c ...
[21:17:24.903] Proof succeeded! fun_c
[21:17:24.936] Verifying test/648686db::fun_rs[0] ...
[21:17:24.953] Contradiction detected! Computing minimal core of contradictory assumptions:
[21:17:24.967] ConditionMetadata {conditionLoc = ProgramLoc {plFunction = mir_precond, plSourceLoc = test.saw:14:3}, conditionTags = fromList [], conditionType = "specification assertion", conditionContext = ""}: precondition
[21:17:24.968] Because of the contradiction, the following proofs may be vacuous.
[21:17:24.968] Simulating test/648686db::fun_rs[0] ...
[21:17:24.968] Checking proof obligations test/648686db::fun_rs[0] ...
[21:17:24.968] Proof succeeded! test/648686db::fun_rs[0]
[21:17:25.050] Contradiction detected! Computing minimal core of contradictory assumptions:
[21:17:25.064] ConditionMetadata {conditionLoc = ProgramLoc {plFunction = jvm_precond, plSourceLoc = test.saw:22:3}, conditionTags = fromList [], conditionType = "specification assertion", conditionContext = ""}: precondition
[21:17:25.064] Because of the contradiction, the following proofs may be vacuous.
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[21:17:25.073] Proof succeeded! fun_jvm
Found 3 expected contradictions

[RyanGlScott]

Ah, I see what is going on now. You can reproduce the issue by running ./build.sh followed by:

$ PATH=$(pwd)/bin:$PATH cabal run integration_tests -- -p test2028_vacuity_detect

Which is how the CI invokes the test suite.

The problem is this line of the test case:

saw-script/intTests/test2028_vacuity_detect/test.sh

Line 3 in 03e1382

n=$( "$SAW" --detect-vacuity test.saw 2>&1 | tee /dev/stderr | grep -c "Contradiction detected" )

This quotes the SAW environment variable. When run through the integration_tests test suite, SAW is defined to be saw -j '/home/runner/work/saw-script/saw-script/intTests/jars/bcprov-jdk16-145.jar:/home/runner/work/saw-script/saw-script/intTests/jars/galois.jar:/home/runner/work/saw-script/saw-script/intTests/jars/org.sat4j.core.jar'. This means that when you invoke "$SAW", you are actually invoking "saw -j ...", which causes the shell to treat everything between the double-quotes as one giant command name. This isn't what you want, since SAW is intentionally including both the command and its arguments.

The simplest fix would be to remove the double quotes around "$SAW", I think.

[sand7000]

Thanks! I fixed and tested it this morning. If all tests pass in github I will merge.

[RyanGlScott]

Suggested change

	LLVM as that is already tested in test0064.
	LLVM as that is already tested in test0064_detect_vacuity.