--detect-vacuity doesn't work with the MIR backend

[sauclovian-g]

saw --detect-vacuity foo.saw doesn't detect unsatisfiable preconditions (such as a == 0 /\ b == 1 /\ a == b) when using the MIR (Rust) backend.

[RyanGlScott]

Here is a test case:

// test.c
void fun_c() {}

// test.rs
pub fn fun_rs() {}

// test.saw
enable_experimental;

let fun_c_spec = do {
  x <- llvm_fresh_var "x" (llvm_int 32);
  llvm_precond {{ x != x }};
  llvm_execute_func [];
};
llvm_mod <- llvm_load_module "test.bc";
llvm_verify llvm_mod "fun_c" [] false fun_c_spec z3;

let fun_rs_spec = do {
  x <- mir_fresh_var "x" mir_u32;
  mir_precond {{ x != x }};
  mir_execute_func [];
};
mir_mod <- mir_load_module "test.linked-mir.json";
mir_verify mir_mod "test::fun_rs" [] false fun_rs_spec z3;

$ clang -g -emit-llvm -c test.c
$ saw-rustc test.rs
$ ~/Software/saw-1.1/bin/saw test.saw --detect-vacuity
[00:07:29.925] Loading file "test.saw"
[00:07:29.963] Verifying fun_c ...
[00:07:29.982] Contradiction detected! Computing minimal core of contradictory assumptions:
[00:07:30.017] ConditionMetadata {conditionLoc = ProgramLoc {plFunction = llvm_precond, plSourceLoc = /home/ryanscott/Documents/Hacking/SAW/test.saw:6:3}, conditionTags = fromList [], conditionType = "specification assertion", conditionContext = ""}: precondition
[00:07:30.017] Because of the contradiction, the following proofs may be vacuous.
[00:07:30.017] Simulating fun_c ...
[00:07:30.017] Checking proof obligations fun_c ...
[00:07:30.017] Proof succeeded! fun_c
[00:07:30.057] Verifying test/569fd098::fun_rs[0] ...
[00:07:30.068] Simulating test/569fd098::fun_rs[0] ...
[00:07:30.068] Checking proof obligations test/569fd098::fun_rs[0] ...
[00:07:30.068] Proof succeeded! test/569fd098::fun_rs[0]

Note that SAW prints Contradiction detected! for the llvm_verify invocation, but not the mir_verify one.

[RyanGlScott]

The reason this happens is because --detect-vacuity only does anything in the LLVM backend:

saw-script/src/SAWScript/Crucible/LLVM/Builtins.hs

Lines 638 to 639 in 2a3ca89

	when (detectVacuity opts)
	$ checkAssumptionsForContradictions cc methodSpec tactic assumes

The MIR backend (as well as the JVM backend) simply don't perform this check. Most of the code in the checkAssumptionsForContradictions function is not LLVM-specific, and we could reasonably port it over to other backends:

saw-script/src/SAWScript/Crucible/LLVM/Builtins.hs

Lines 1030 to 1042 in 2a3ca89

	-- | Checks whether the given list of assumptions contains a contradiction, and
	-- if so, computes and displays a minimal set of contradictory assumptions.
	checkAssumptionsForContradictions ::
	(Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
	LLVMCrucibleContext arch ->
	MS.CrucibleMethodSpecIR (LLVM arch) ->
	ProofScript () ->
	[Crucible.LabeledPred Term AssumptionReason] ->
	TopLevel ()
	checkAssumptionsForContradictions cc methodSpec tactic assumes =
	whenM
	(assumptionsContainContradiction cc methodSpec tactic assumes)
	(computeMinimalContradictingCore cc methodSpec tactic assumes)

We'd need to perform some mild refactoring to get rid of the LLVMCrucibleContext argument, but I don't expect that to be difficult.

[sand7000]

Pull request:

#2339

resolves this. I added an a java version of the test case given above:

cat Test.java 
public class Test {
    public static void fun_jvm() {
    }
}

and appended this to test.saw:

let fun_jvm_spec = do {
  x <- jvm_fresh_var "x" java_int;
  jvm_precond {{ x != x }};  // Always false
  jvm_execute_func [];
};

cls <- java_load_class "Test";
jvm_verify cls "fun_jvm" [] false fun_jvm_spec z3;

and I see Contradiction detected! printed for all 3 now:

[18:44:05.617] Loading file "test.saw"
[18:44:05.653] Verifying fun_c ...
[18:44:05.664] Contradiction detected! Computing minimal core of contradictory assumptions:
[18:44:05.687] ConditionMetadata {conditionLoc = ProgramLoc {plFunction = llvm_precond, plSourceLoc = test.saw:6:3}, conditionTags = fromList [], conditionType = "specification assertion", conditionContext = ""}: precondition
[18:44:05.687] Because of the contradiction, the following proofs may be vacuous.
[18:44:05.687] Simulating fun_c ...
[18:44:05.688] Checking proof obligations fun_c ...
[18:44:05.688] Proof succeeded! fun_c
[18:44:05.725] Verifying test/648686db::fun_rs[0] ...
[18:44:05.749] Contradiction detected! Computing minimal core of contradictory assumptions:
[18:44:05.772] ConditionMetadata {conditionLoc = ProgramLoc {plFunction = mir_precond, plSourceLoc = test.saw:14:3}, conditionTags = fromList [], conditionType = "specification assertion", conditionContext = ""}: precondition
[18:44:05.772] Because of the contradiction, the following proofs may be vacuous.
[18:44:05.772] Simulating test/648686db::fun_rs[0] ...
starting executeCrucibleMIR
[18:44:05.773] Checking proof obligations test/648686db::fun_rs[0] ...
[18:44:05.773] Proof succeeded! test/648686db::fun_rs[0]
[18:44:05.861] Contradiction detected! Computing minimal core of contradictory assumptions:
[18:44:05.881] ConditionMetadata {conditionLoc = ProgramLoc {plFunction = jvm_precond, plSourceLoc = test.saw:22:3}, conditionTags = fromList [], conditionType = "specification assertion", conditionContext = ""}: precondition
[18:44:05.881] Because of the contradiction, the following proofs may be vacuous.
starting executeCrucibleJVM
registering standard overrides
registering user-provided overrides
registering assumptions
simulating function
[18:44:05.892] Proof succeeded! fun_jvm