From 499112e376dc9984102e7488430fae4187794972 Mon Sep 17 00:00:00 2001
From: Robert Dockins <rdockins@galois.com>
Date: Thu, 19 May 2022 15:28:56 -0700
Subject: [PATCH] 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  |  7 ++++++
 src/SAWScript/Crucible/LLVM/Builtins.hs | 16 +++++++++++---
 src/SAWScript/Interpreter.hs            | 29 +++++++++++++++++++++++++
 src/SAWScript/Value.hs                  |  1 +
 4 files changed, 50 insertions(+), 3 deletions(-)

diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
index 47eddaa93a..8f33a31d35 100644
--- a/src/SAWScript/Crucible/JVM/Builtins.hs
+++ b/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
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index 6b51a45673..3dce24fc8f 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/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
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 66a3b4cc4d..ef9c6b3111 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/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
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index f7eb7a361e..b5880395af 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -520,6 +520,7 @@ data TopLevelRW =
   , rwCrucibleTimeout :: Integer
 
   , rwPathSatSolver :: Common.PathSatSolver
+  , rwSkipSafetyProofs :: Bool
   }
 
 newtype TopLevel a =