Allow the user to skip safety proofs that arise during

symbolic execution.  This is generally unsound, but may
be useful in proof exploration and construction to focus
in on just the stated correcness specifications.

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -725,6 +725,13 @@ verifyPoststate cc mspec env0 globals ret =
      poststateLoc <- SS.toW4Loc "_SAW_verify_poststate" <$> getPosition
      io $ W4.setCurrentProgramLoc sym poststateLoc
 
+     -- This discards all the obligations generated during
+     -- symbolic execution itself, i.e., which are not directly
+     -- generated from specification postconditions. This
+     -- is, in general, unsound.
+     skipSafetyProofs <- gets rwSkipSafetyProofs
+     when skipSafetyProofs (io (Crucible.clearProofObligations bak))
+
      let ecs0 = Map.fromList
            [ (ecVarIndex ec, ec)
            | tt <- mspec ^. MS.csPreState . MS.csFreshVars

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -1372,6 +1372,13 @@ verifyPoststate cc mspec env0 globals ret =
      opts <- getOptions
      io $ W4.setCurrentProgramLoc sym poststateLoc
 
+     -- This discards all the obligations generated during
+     -- symbolic execution itself, i.e., which are not directly
+     -- generated from specification postconditions. This
+     -- is, in general, unsound.
+     skipSafetyProofs <- gets rwSkipSafetyProofs
+     when skipSafetyProofs (io (Crucible.clearProofObligations bak))
+
      let ecs0 = Map.fromList
            [ (ecVarIndex ec, ec)
            | tt <- mspec ^. MS.csPreState . MS.csFreshVars
@@ -1397,9 +1404,12 @@ verifyPoststate cc mspec env0 globals ret =
      io $ for_ (view osAsserts st) $ \(W4.LabeledPred p r) ->
        Crucible.addAssertion bak (Crucible.LabeledPred p r)
 
-     obligations <- io $ Crucible.getProofObligations bak
-     io $ Crucible.clearProofObligations bak
-     sc_obligations <- io $ mapM (verifyObligation sc) (maybe [] Crucible.goalsToList obligations)
+     obligations <- io $
+       do obls <- Crucible.getProofObligations bak
+          Crucible.clearProofObligations bak
+          return (maybe [] Crucible.goalsToList obls)
+
+     sc_obligations <- io $ mapM (verifyObligation sc) obligations
      return (sc_obligations, st)
 
   where

src/SAWScript/Interpreter.hs

@@ -454,6 +454,7 @@ buildTopLevelEnv proxy opts =
                    , rwAllocSymInitCheck = True
                    , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout
                    , rwPathSatSolver = CC.PathSat_Z3
+                   , rwSkipSafetyProofs = False
                    }
        return (bic, ro0, rw0)
 
@@ -489,6 +490,18 @@ add_primitives lc bic opts = do
   , rwPrimsAvail = Set.insert lc (rwPrimsAvail rw)
   }
 
+enable_safety_proofs :: TopLevel ()
+enable_safety_proofs = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw{ rwSkipSafetyProofs = False }
+
+disable_safety_proofs :: TopLevel ()
+disable_safety_proofs = do
+  opts <- getOptions
+  io $ printOutLn opts Warn "Safety proofs disabled! This is unsound!"
+  rw <- getTopLevelRW
+  putTopLevelRW rw{ rwSkipSafetyProofs = True }
+
 enable_smt_array_memory_model :: TopLevel ()
 enable_smt_array_memory_model = do
   rw <- getTopLevelRW
@@ -825,6 +838,22 @@ primitives = Map.fromList
     Current
     [ "Disable the SMT array memory model." ]
 
+  , prim "enable_safety_proofs" "TopLevel ()"
+    (pureVal enable_safety_proofs)
+    Experimental
+    [ "Restore the default state, where safety obligations"
+    , "encountered during symbolic execution are proofed normally."
+    ]
+
+  , prim "disable_safety_proofs" "TopLevel ()"
+    (pureVal disable_safety_proofs)
+    Experimental
+    [ "Disable checking of safety obligations encountered during symbolic"
+    , "execution. This is unsound! However, it can be useful during"
+    , "initial proof construction to focus only on the stated correcness"
+    , "specifications."
+    ]
+
  , prim "enable_crucible_assert_then_assume" "TopLevel ()"
     (pureVal enable_crucible_assert_then_assume)
     Current

src/SAWScript/Value.hs

@@ -520,6 +520,7 @@ data TopLevelRW =
   , rwCrucibleTimeout :: Integer
 
   , rwPathSatSolver :: Common.PathSatSolver
+  , rwSkipSafetyProofs :: Bool
   }
 
 newtype TopLevel a =