Add vacuity detection in MIR and JVM backends.

CHANGES.md

@@ -36,6 +36,11 @@ Note that build.sh is in any case the recommended way to build.
 
 * Support `bmux` gates in exported Yosys directly to avoid reliance on `bmuxmap`
 
+* Vacuity checking (`--detect-vacuity`) now correctly reports contradictions in specifications
+  for all Crucible backends: LLVM, MIR, and JVM. Previously, vacuous proofs in MIR and JVM
+  code could go undetected.
+
+
 ## Bug fixes
 
 * The `head` and `tail` primitives are now implemented in the SAW-Core

intTests/test2028_vacuity_detect/Makefile

@@ -0,0 +1,7 @@
+all: test.linked-mir.json Test.class
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+
+Test.class: Test.java
+	javac -g $<

intTests/test2028_vacuity_detect/README

@@ -0,0 +1,8 @@
+This test checks for vacuous proofs in the MIR, and JVM backends. It skips
+LLVM as that is already tested in test0064.
+
+It corresponds to issue https://github.com/GaloisInc/saw-script/issues/2028
+
+Each function includes a contradictory precondition (e.g., x != x), and SAW
+should detect this and emit a vacuity warning before successfully proving the
+function.

intTests/test2028_vacuity_detect/Test.java

@@ -0,0 +1,4 @@
+public class Test {
+    public static void fun_jvm() {
+    }
+}

intTests/test2028_vacuity_detect/test.linked-mir.json

@@ -0,0 +1 @@
+{"version":1,"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:2:19: 2:19"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/648686db::fun_rs","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/648686db::fun_rs","kind":"Item","substs":[]},"name":"test/648686db::fun_rs"}],"tys":[{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}}],"roots":["test/648686db::fun_rs"]}

intTests/test2028_vacuity_detect/test.rs

@@ -0,0 +1,2 @@
+// test.rs
+pub fn fun_rs() {}

intTests/test2028_vacuity_detect/test.saw

@@ -0,0 +1,19 @@
+// test.saw
+enable_experimental;
+
+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;
+
+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;

intTests/test2028_vacuity_detect/test.sh

@@ -0,0 +1,11 @@
+#!/bin/bash
+
+n=$( $SAW --detect-vacuity test.saw 2>&1 | tee /dev/stderr | grep -c "Contradiction detected" )
+
+if [ "$n" -eq 2 ]; then
+  echo "Found 2 expected contradictions"
+  exit 0
+else
+  echo "Expected 2 contradictions, found $n"
+  exit 1
+fi

saw-central/src/SAWCentral/Crucible/Common/Vacuity.hs

@@ -0,0 +1,110 @@
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+
+module SAWCentral.Crucible.Common.Vacuity (
+  checkAssumptionsForContradictions
+) where
+
+import Prelude hiding (fail)
+
+import           Control.Lens
+import           Control.Monad (forM_)
+import           Control.Monad.Extra (findM, whenM)
+import           Data.Function
+import           Data.List
+import qualified What4.ProgramLoc as W4
+import qualified What4.Interface as W4
+import qualified Lang.Crucible.Backend as Crucible
+import SAWCore.SharedTerm
+import SAWCoreWhat4.ReturnTrip
+import SAWCentral.Proof
+import SAWCentral.TopLevel
+import SAWCentral.Value
+import SAWCentral.Options
+import qualified SAWCentral.Crucible.Common as Common
+import           SAWCentral.Crucible.Common.MethodSpec (CrucibleMethodSpecIR)
+import qualified SAWCentral.Crucible.Common.MethodSpec as MS
+
+type AssumptionReason = (MS.ConditionMetadata, String)
+
+-- | Checks whether the given list of assumptions contains a contradiction, and
+-- if so, computes and displays a minimal set of contradictory assumptions.
+checkAssumptionsForContradictions ::
+  Show (MS.MethodId ext) =>
+  Common.Sym ->
+  CrucibleMethodSpecIR ext ->
+  ProofScript () ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
+  TopLevel ()
+checkAssumptionsForContradictions sym methodSpec tactic assumptions =
+  whenM
+    (assumptionsContainContradiction sym methodSpec tactic assumptions)
+    (computeMinimalContradictingCore sym methodSpec tactic assumptions)
+
+-- | Checks for contradictions within the given list of assumptions, by asking
+-- the solver about whether their conjunction entails falsehood.
+assumptionsContainContradiction ::
+  Show (MS.MethodId ext) =>
+  Common.Sym ->
+  CrucibleMethodSpecIR ext ->
+  ProofScript () ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
+  TopLevel Bool
+assumptionsContainContradiction sym methodSpec tactic assumptions = 
+  do
+     st <- io $ Common.sawCoreState sym
+     let sc  = saw_ctx st
+     let ploc = methodSpec^.MS.csLoc
+     (goal',pgl) <- io $
+      do
+         -- conjunction of all assumptions
+         assume <- scAndList sc (toListOf (folded . Crucible.labeledPred) assumptions)
+         -- implies falsehood
+         goal  <- scImplies sc assume =<< toSC sym st (W4.falsePred sym)
+         goal' <- boolToProp sc [] goal
+         return $ (goal',
+                  ProofGoal
+                  { goalNum  = 0
+                  , goalType = "vacuousness check"
+                  , goalName = show (methodSpec^.MS.csMethod)
+                  , goalLoc  = show (W4.plSourceLoc ploc) ++ " in " ++ show (W4.plFunction ploc)
+                  , goalDesc = "vacuousness check"
+                  , goalSequent = propToSequent goal'
+                  , goalTags = mempty
+                  })
+     res <- runProofScript tactic goal' pgl Nothing
+              "vacuousness check" False False
+     case res of
+       ValidProof _ _     -> return True
+       InvalidProof _ _ _ -> return False
+       UnfinishedProof _  ->
+         -- TODO? is this the right behavior?
+         do printOutLnTop Warn "Could not determine if preconditions are vacuous"
+            return True
+
+-- | Given a list of assumptions, computes and displays a smallest subset of
+-- them that are contradictory among each themselves.  This is **not**
+-- implemented efficiently.
+computeMinimalContradictingCore ::
+  Show (MS.MethodId ext) =>
+  Common.Sym ->
+  CrucibleMethodSpecIR ext ->
+  ProofScript () ->
+  [Crucible.LabeledPred Term AssumptionReason] ->
+  TopLevel ()
+computeMinimalContradictingCore sym methodSpec tactic assumes =
+  do
+     printOutLnTop Warn "Contradiction detected! Computing minimal core of contradictory assumptions:"
+     -- test subsets of assumptions of increasing sizes until we find a
+     -- contradictory one
+     let cores = sortBy (compare `on` length) (subsequences assumes)
+     findM (assumptionsContainContradiction sym methodSpec tactic) cores >>= \case
+      Nothing -> 
+        printOutLnTop Warn "No minimal core: the assumptions did not contains a contradiction."
+      Just core ->
+        forM_ core $ \assume ->
+          case assume^.Crucible.labeledPredMsg of
+            (loc, reason) -> printOutLnTop Warn (show loc ++ ": " ++ reason)
+     printOutLnTop Warn "Because of the contradiction, the following proofs may be vacuous."

saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs

@@ -133,6 +133,7 @@ import qualified SAWCentral.Crucible.Common as Common
 import           SAWCentral.Crucible.Common
 import           SAWCentral.Crucible.Common.Override (MetadataMap)
 import           SAWCentral.Crucible.Common.MethodSpec (AllocIndex(..), nextAllocIndex, PrePost(..))
+import qualified SAWCentral.Crucible.Common.Vacuity as Vacuity
 
 import qualified SAWCentral.Crucible.Common.MethodSpec as MS
 import qualified SAWCentral.Crucible.Common.Setup.Type as Setup
@@ -247,6 +248,14 @@ jvm_verify cls nm lemmas checkSat setup tactic =
      -- construct the initial state for verifications
      (args, assumes, env, globals2) <- io $ verifyPrestate cc methodSpec globals1
 
+     -- check for contradictory preconditions
+     when (detectVacuity opts) $
+       Vacuity.checkAssumptionsForContradictions
+         sym
+         methodSpec
+         tactic
+         assumes
+
      -- save initial path conditions
      frameIdent <- io $ Crucible.pushAssumptionFrame bak
 

saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs

@@ -94,8 +94,7 @@ import Prelude hiding (fail)
 import qualified Control.Exception as X
 import           Control.Lens
 
-import           Control.Monad (foldM, forM, forM_, replicateM, unless, when)
-import           Control.Monad.Extra (findM, whenM)
+import           Control.Monad (foldM, forM, replicateM, unless, when)
 import           Control.Monad.Fail (MonadFail(..))
 import           Control.Monad.IO.Class (MonadIO(..))
 import           Control.Monad.Reader (runReaderT)
@@ -104,7 +103,6 @@ import           Control.Monad.Trans.Class (MonadTrans(..))
 import qualified Data.Bimap as Bimap
 import           Data.Char (isDigit)
 import           Data.Foldable (for_, toList, fold)
-import           Data.Function
 import           Data.Functor (void)
 import           Data.IORef
 import           Data.List
@@ -212,6 +210,7 @@ import           SAWCentral.Crucible.Common.MethodSpec (SetupValue(..))
 import           SAWCentral.Crucible.Common.Override
 import qualified SAWCentral.Crucible.Common.Setup.Builtins as Setup
 import qualified SAWCentral.Crucible.Common.Setup.Type as Setup
+import qualified SAWCentral.Crucible.Common.Vacuity as Vacuity
 
 import SAWCentral.Crucible.LLVM.Override
 import SAWCentral.Crucible.LLVM.ResolveSetupValue
@@ -654,7 +653,7 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp =
        io $ verifyPrestate opts cc methodSpec globals1
 
      when (detectVacuity opts)
-       $ checkAssumptionsForContradictions cc methodSpec tactic assumes
+       $ Vacuity.checkAssumptionsForContradictions sym methodSpec tactic assumes
 
      -- save initial path conditions
      frameIdent <- io $ Crucible.pushAssumptionFrame bak
@@ -755,7 +754,7 @@ refineMethodSpec cc methodSpec lemmas tactic =
        io $ verifyPrestate opts cc methodSpec globals1
 
      when (detectVacuity opts)
-       $ checkAssumptionsForContradictions cc methodSpec tactic assumes
+       $ Vacuity.checkAssumptionsForContradictions sym methodSpec tactic assumes
 
      -- save initial path conditions
      frameIdent <- io $ Crucible.pushAssumptionFrame bak
@@ -981,86 +980,6 @@ verifyPrestate opts cc mspec globals =
 
      return (args, cs, env, globals2)
 
--- | Checks for contradictions within the given list of assumptions, by asking
--- the solver about whether their conjunction entails falsehood.
-assumptionsContainContradiction ::
-  (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
-  LLVMCrucibleContext arch ->
-  MS.CrucibleMethodSpecIR (LLVM arch) ->
-  ProofScript () ->
-  [Crucible.LabeledPred Term AssumptionReason] ->
-  TopLevel Bool
-assumptionsContainContradiction cc methodSpec tactic assumptions =
-  do
-     let sym = cc^.ccSym
-     st <- io $ Common.sawCoreState sym
-     let sc  = saw_ctx st
-     let ploc = methodSpec^.MS.csLoc
-     (goal',pgl) <- io $
-      do
-         -- conjunction of all assumptions
-         assume <- scAndList sc (toListOf (folded . Crucible.labeledPred) assumptions)
-         -- implies falsehood
-         goal  <- scImplies sc assume =<< toSC sym st (W4.falsePred sym)
-         goal' <- boolToProp sc [] goal
-         return $ (goal',
-                  ProofGoal
-                  { goalNum  = 0
-                  , goalType = "vacuousness check"
-                  , goalName = show (methodSpec^.MS.csMethod)
-                  , goalLoc  = show (W4.plSourceLoc ploc) ++ " in " ++ show (W4.plFunction ploc)
-                  , goalDesc = "vacuousness check"
-                  , goalSequent = propToSequent goal'
-                  , goalTags = mempty
-                  })
-     res <- runProofScript tactic goal' pgl Nothing
-              "vacuousness check" False False
-     case res of
-       ValidProof _ _     -> return True
-       InvalidProof _ _ _ -> return False
-       UnfinishedProof _  ->
-         -- TODO? is this the right behavior?
-         do printOutLnTop Warn "Could not determine if preconditions are vacuous"
-            return True
-
--- | Given a list of assumptions, computes and displays a smallest subset of
--- them that are contradictory among each themselves.  This is **not**
--- implemented efficiently.
-computeMinimalContradictingCore ::
-  (Crucible.HasPtrWidth (Crucible.ArchWidth arch), Crucible.HasLLVMAnn Sym) =>
-  LLVMCrucibleContext arch ->
-  MS.CrucibleMethodSpecIR (LLVM arch) ->
-  ProofScript () ->
-  [Crucible.LabeledPred Term AssumptionReason] ->
-  TopLevel ()
-computeMinimalContradictingCore cc methodSpec tactic assumes =
-  do
-     printOutLnTop Warn "Contradiction detected! Computing minimal core of contradictory assumptions:"
-     -- test subsets of assumptions of increasing sizes until we find a
-     -- contradictory one
-     let cores = sortBy (compare `on` length) (subsequences assumes)
-     findM (assumptionsContainContradiction cc methodSpec tactic) cores >>= \case
-      Nothing -> printOutLnTop Warn "No minimal core: the assumptions did not contains a contradiction."
-      Just core ->
-        forM_ core $ \assume ->
-          case assume^.Crucible.labeledPredMsg of
-            (loc, reason) -> printOutLnTop Warn (show loc ++ ": " ++ reason)
-     printOutLnTop Warn "Because of the contradiction, the following proofs may be vacuous."
-
--- | 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)
-
 -- | Check two MemTypes for register compatiblity.  This is a stricter
 --   check than the memory compatiblity check that is done for points-to
 --   assertions.

saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs

@@ -132,6 +132,7 @@ import qualified SAWCentral.Crucible.Common.MethodSpec as MS
 import SAWCentral.Crucible.Common.Override
 import qualified SAWCentral.Crucible.Common.Setup.Builtins as Setup
 import qualified SAWCentral.Crucible.Common.Setup.Type as Setup
+import qualified SAWCentral.Crucible.Common.Vacuity as Vacuity
 import SAWCentral.Crucible.MIR.MethodSpecIR
 import SAWCentral.Crucible.MIR.Override
 import SAWCentral.Crucible.MIR.ResolveSetupValue
@@ -710,6 +711,14 @@ mir_verify rm nm lemmas checkSat setup tactic =
      -- save initial path conditions
      frameIdent <- io $ Crucible.pushAssumptionFrame bak
 
+     -- check for contradictory preconditions
+     when (detectVacuity opts) $
+       Vacuity.checkAssumptionsForContradictions
+         sym
+         methodSpec
+         tactic
+         assumes
+
      -- run the symbolic execution
      printOutLnTop Info $
        unwords ["Simulating", show (methodSpec ^. MS.csMethod), "..."]

saw.cabal

@@ -641,6 +641,7 @@ library saw-central
     SAWCentral.Crucible.Common.Setup.Builtins
     SAWCentral.Crucible.Common.Setup.Type
     SAWCentral.Crucible.Common.Setup.Value
+    SAWCentral.Crucible.Common.Vacuity
 
     SAWCentral.Crucible.LLVM.Builtins
     SAWCentral.Crucible.LLVM.Boilerplate