Merge pull request #1216 from langston-barrett/lb/prove-goals-faster

Make obligation checking more configurable
GaloisInc · Jul 16, 2024 · c310fcb · c310fcb
2 parents 376a1c0 + f6814fb
commit c310fcb
Show file tree

Hide file tree

Showing 7 changed files with 488 additions and 96 deletions.
diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -21,7 +21,7 @@ module Lang.Crucible.CLI
   ) where
 
 import Control.Monad
-
+import Control.Monad.Except (runExceptT)
 import Data.Foldable
 import Data.Map (Map)
 import Data.Text (Text)
@@ -49,11 +49,13 @@ import Lang.Crucible.Syntax.SExpr
 
 import Lang.Crucible.Analysis.Postdom
 import Lang.Crucible.Backend
-import Lang.Crucible.Backend.Prove (ProofResult(..), proveCurrentObligations)
+import qualified Lang.Crucible.Backend.Prove as Prove
 import Lang.Crucible.Backend.Simple
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
 import Lang.Crucible.Simulator.Profiling
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 import What4.Config
 import What4.Interface (getConfiguration)
@@ -181,12 +183,22 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                        getProofObligations bak >>= \case
                          Nothing -> hPutStrLn outh "==== No proof obligations ===="
                          Just {} -> hPutStrLn outh "==== Proof obligations ===="
-                       proveCurrentObligations bak defaultLogData z3Adapter $ \goal res -> do
-                         hPrint outh =<< ppProofObligation sym goal
-                         case res of
-                           Proved {} -> hPutStrLn outh "PROVED"
-                           Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE"
-                           Unknown {} -> hPutStrLn outh "UNKNOWN"
+                       -- TODO: Make this timeout configurable via the CLI
+                       let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+                       let prover = Prove.offlineProver timeout sym defaultLogData z3Adapter
+                       let strat = Prove.ProofStrategy prover Prove.keepGoing
+                       let ppResult =
+                             \case
+                               Prove.Proved {} ->  "PROVED"
+                               Prove.Disproved {} -> "COUNTEREXAMPLE"
+                               Prove.Unknown {} -> "UNKNOWN"
+                       let printer = Prove.ProofConsumer $ \goal res -> do
+                             hPrint outh =<< ppProofObligation sym goal
+                             hPutStrLn outh (ppResult res)
+                       runExceptT (Prove.proveCurrentObligations bak strat printer) >>=
+                         \case
+                           Left CTO.TimedOut -> hPutStrLn outh "TIMEOUT"
+                           Right () -> pure ()
 
                   _ -> hPutStrLn outh "No suitable main function found"
 

diff --git a/crucible-symio/tests/TestMain.hs b/crucible-symio/tests/TestMain.hs
@@ -27,6 +27,7 @@ import           GHC.TypeNats
 import           Control.Lens ( (^.) )
 
 import           Control.Monad (foldM )
+import           Control.Monad.Except (runExceptT)
 import           Control.Monad.IO.Class (liftIO)
 import qualified Data.Map as Map
 import qualified Data.Parameterized.Context as Ctx
@@ -51,6 +52,8 @@ import qualified Lang.Crucible.Simulator as CS
 import qualified Lang.Crucible.Simulator.OverrideSim as CSO
 import qualified Lang.Crucible.FunctionHandle as CFH
 import qualified Lang.Crucible.Simulator.GlobalState as CGS
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 import qualified What4.Interface as W4
 import qualified What4.Expr as WE
@@ -134,7 +137,10 @@ runFSTest' bak (FSTest fsTest) = do
           putStrLn $ showF p
           T.assertFailure "Partial Result"
 
-  CB.proveCurrentObligations bak WSA.defaultLogData W4Y.yicesAdapter $ \obligation ->
+  let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+  let prover = CB.offlineProver timeout sym WSA.defaultLogData W4Y.yicesAdapter
+  let strat = CB.ProofStrategy prover CB.failFast
+  merr <- runExceptT $ CB.proveCurrentObligations bak strat $ CB.ProofConsumer $ \obligation ->
     \case
       CB.Proved {} -> return ()
       CB.Unknown {} -> T.assertFailure "Inconclusive"
@@ -145,6 +151,9 @@ runFSTest' bak (FSTest fsTest) = do
         putStrLn (showF asmsPred)
         putStrLn (showF goalPred)
         T.assertFailure "Assertion Failure"
+  case merr of
+    Left CTO.TimedOut -> T.assertFailure "Timeout"
+    Right () -> pure ()
 
 showAbortedResult :: CS.AbortedResult c d -> String
 showAbortedResult ar = case ar of

diff --git a/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs b/crucible-syntax/src/Lang/Crucible/Syntax/Overrides.hs
@@ -10,23 +10,24 @@ module Lang.Crucible.Syntax.Overrides
   ) where
 
 import Control.Lens hiding ((:>), Empty)
-import Control.Monad (forM_)
+import Control.Monad.Except (runExceptT)
 import Control.Monad.IO.Class
 import System.IO
 
 import Data.Parameterized.Context hiding (view)
 
 import What4.Expr.Builder
-import What4.Interface
 import What4.ProgramLoc
-import What4.SatResult
 import What4.Solver (LogData(..), defaultLogData)
-import What4.Solver.Z3 (runZ3InOverride)
+import What4.Solver.Z3 (z3Adapter)
 
 import Lang.Crucible.Backend
+import qualified Lang.Crucible.Backend.Prove as CB
 import Lang.Crucible.Types
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
+import qualified Lang.Crucible.Utils.Seconds as Sec
+import qualified Lang.Crucible.Utils.Timeout as CTO
 
 
 setupOverrides ::
@@ -48,15 +49,20 @@ proveObligations =
      liftIO $ do
        hPutStrLn h "Attempting to prove all outstanding obligations!\n"
 
-       obls <- maybe [] goalsToList <$> getProofObligations bak
-       clearProofObligations bak
+       let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h
+                                    , logReason = "assertion proof" }
+       let timeout = CTO.Timeout (Sec.secondsFromInt 5)
+       let prover = CB.offlineProver timeout sym logData z3Adapter
+       let strat = CB.ProofStrategy prover CB.keepGoing
+       let ppResult o =
+             \case
+               CB.Proved {}  -> unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+               CB.Disproved {} -> unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+               CB.Unknown {} -> unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+       let printer = CB.ProofConsumer $ \o r -> hPutStrLn h (ppResult o r)
+       runExceptT (CB.proveCurrentObligations bak strat printer) >>=
+         \case
+           Left CTO.TimedOut -> hPutStrLn h "Proof timed out!"
+           Right () -> pure ()
 
-       forM_ obls $ \o ->
-         do asms <- assumptionsPred sym (proofAssumptions o)
-            gl <- notPred sym (o ^. to proofGoal.labeledPred)
-            let logData = defaultLogData { logCallbackVerbose = \_ -> hPutStrLn h
-                                         , logReason = "assertion proof" }
-            runZ3InOverride sym logData [asms,gl] $ \case
-              Unsat{}  -> hPutStrLn h $ unlines ["Proof Succeeded!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
-              Sat _mdl -> hPutStrLn h $ unlines ["Proof failed!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
-              Unknown  -> hPutStrLn h $ unlines ["Proof inconclusive!", show $ ppSimError $ (proofGoal o)^.labeledPredMsg]
+       clearProofObligations bak
diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal
@@ -44,6 +44,7 @@ common bldflags
 library
   import: bldflags
   build-depends:
+    async,
     base >= 4.13 && < 4.19,
     bimap,
     bv-sized >= 1.0.0 && < 1.1,
@@ -129,6 +130,8 @@ library
     Lang.Crucible.Utils.MuxTree
     Lang.Crucible.Utils.PrettyPrint
     Lang.Crucible.Utils.RegRewrite
+    Lang.Crucible.Utils.Seconds
+    Lang.Crucible.Utils.Timeout
     Lang.Crucible.Utils.StateContT
     Lang.Crucible.Utils.Structural