Vacuity checking added to JVM and MIR Backends #2338
Conversation
- Introduce SAWCentral.Crucible.Common.Vacuity for backend-independent detection of contradictory assumptions. - Adapt LLVM/Builtins.hs to use the new GenericCrucibleContext abstraction. - Preserve existing vacuity behavior under --detect-vacuity for LLVM backend. - No change for other backends yet. - Register new module in saw.cabal.
Hooks vacuity checking into mir_verify using the new GenericCrucibleContext abstraction.
Hooks vacuity checking into jvm_verify using the new GenericCrucibleContext abstraction.
|
This is related to #2028 |
There was a problem hiding this comment.
Thanks for working on this, @sand7000!
Some general observations:
- Please make a note of --detect-vacuity doesn't work with the MIR backend #2028 in the relevant commits that fix the issue so that GitHub links the commits back to the issue.
- Make sure mention this improvement in the SAW changelog.
- Please add at least one test case under
intTestsso that we can verify that the bug remains fixed going forward.
| -- | Minimal backend-independent context | ||
| data GenericCrucibleContext sym = GenericCrucibleContext | ||
| { gccSym :: sym -- What4 symbolic backend | ||
| } |
There was a problem hiding this comment.
I don't understand what the purpose of this data type is. Why not just pass Sym directly instead?
| (assumptionsContainContradiction gcc methodSpec tactic assumptions) | ||
| (computeMinimalContradictingCore gcc methodSpec tactic assumptions) | ||
|
|
||
| -- | Check if the assumptions are contradictory |
There was a problem hiding this comment.
Any reason not to use the same Haddock comments that were originally present in SAWCentral.Crucible.LLVM.Builtins?
| -- | Check if the assumptions are contradictory | |
| -- | Checks for contradictions within the given list of assumptions, by asking | |
| -- the solver about whether their conjunction entails falsehood. |
These are more detailed, so I would prefer using these.
| do printOutLnTop Warn "Could not determine if preconditions are vacuous" | ||
| return True | ||
|
|
||
| -- | Try to find the smallest contradictory subset |
There was a problem hiding this comment.
Similarly:
| -- | Try to find the smallest contradictory subset | |
| -- | Given a list of assumptions, computes and displays a smallest subset of | |
| -- them that are contradictory among each themselves. This is **not** | |
| -- implemented efficiently. |
| TopLevel () | ||
| computeMinimalContradictingCore gcc methodSpec tactic assumes = do | ||
| printOutLnTop Warn "Contradiction detected! Computing minimal core of contradictory assumptions:" | ||
| let cores = sortBy (compare `on` length) (subsequences assumes) |
There was a problem hiding this comment.
This is missing a comment from the original code in SAWCrucible.Crucible.Builtins.LLVM, which would be nice to include:
| let cores = sortBy (compare `on` length) (subsequences assumes) | |
| -- test subsets of assumptions of increasing sizes until we find a | |
| -- contradictory one | |
| let cores = sortBy (compare `on` length) (subsequences assumes) |
| { gccSym :: sym -- What4 symbolic backend | ||
| } | ||
|
|
||
| -- | Top-level check and minimal core reporter |
There was a problem hiding this comment.
Consider using the Haddocks comments from the function of the same name in SAWCentral.Crucible.LLVM.Builtins, which are more detailed:
| -- | Top-level check and minimal core reporter | |
| -- | Checks whether the given list of assumptions contains a contradiction, and | |
| -- if so, computes and displays a minimal set of contradictory assumptions. |
| -- | Checks whether the given list of assumptions contains a contradiction, and | ||
| -- if so, computes and displays a minimal set of contradictory assumptions. | ||
| checkAssumptionsForContradictions :: |
There was a problem hiding this comment.
Now that checkAssumptionsForContradictions has been moved to SAWCentral.Crucible.Common.Vacuity, I would favor removing this function here, as it is essentially a duplicate.
Changes
I verified the with test cases demonstrating vacuous and non-vacuous proofs across all three backends.