Helpers for checking proof obligations

crucible-cli/src/Lang/Crucible/CLI.hs

@@ -20,7 +20,6 @@ module Lang.Crucible.CLI
   , execCommand
   ) where
 
-import Control.Lens (view)
 import Control.Monad
 
 import Data.Foldable
@@ -50,18 +49,19 @@ import Lang.Crucible.Syntax.SExpr
 
 import Lang.Crucible.Analysis.Postdom
 import Lang.Crucible.Backend
+import Lang.Crucible.Backend.Prove (ProofResult(..), proveProofGoal)
 import Lang.Crucible.Backend.Simple
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
 import Lang.Crucible.Simulator.Profiling
 
 import What4.Config
-import What4.Interface (getConfiguration,notPred)
+import What4.Interface (getConfiguration)
 import What4.Expr (ExprBuilder, newExprBuilder, EmptyExprBuilderState(..))
 import What4.FunctionName
 import What4.ProgramLoc
-import What4.SatResult
-import What4.Solver (defaultLogData, runZ3InOverride, z3Options)
+import What4.Solver (defaultLogData)
+import What4.Solver.Z3 (z3Adapter, z3Options)
 
 -- | Allows users to hook into the various stages of 'simulateProgram'.
 data SimulateProgramHooks ext = SimulateProgramHooks
@@ -184,14 +184,11 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
                            do hPutStrLn outh "==== Proof obligations ===="
                               forM_ (goalsToList gs) (\g ->
                                 do hPrint outh =<< ppProofObligation sym g
-                                   neggoal <- notPred sym (view labeledPred (proofGoal g))
-                                   asms <- assumptionsPred sym (proofAssumptions g)
-                                   let bs = [neggoal, asms]
-                                   runZ3InOverride sym defaultLogData bs (\case
-                                     Sat _   -> hPutStrLn outh "COUNTEREXAMPLE"
-                                     Unsat _ -> hPutStrLn outh "PROVED"
-                                     Unknown -> hPutStrLn outh "UNKNOWN"
-                                     )
+                                   proveProofGoal sym defaultLogData z3Adapter g $
+                                     \case
+                                       Proved {} -> hPutStrLn outh "PROVED"
+                                       Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE"
+                                       Unknown {} -> hPutStrLn outh "UNKNOWN"
                                 )
 
                   _ -> hPutStrLn outh "No suitable main function found"

crucible-symio/tests/TestMain.hs

@@ -42,6 +42,7 @@ import qualified Data.BitVector.Sized as BVS
 import qualified Test.Tasty as T
 import qualified Test.Tasty.HUnit as T
 
+import qualified Lang.Crucible.Backend.Prove as CB
 import qualified Lang.Crucible.Backend.Simple as CB
 import qualified Lang.Crucible.Backend as CB
 import qualified Lang.Crucible.CFG.Core as CC
@@ -133,26 +134,14 @@ runFSTest' bak (FSTest fsTest) = do
         _ -> do
           putStrLn $ showF p
           T.assertFailure "Partial Result"
-  obligations <- CB.getProofObligations bak
-  mapM_ (proveGoal sym W4Y.yicesAdapter) (maybe [] CB.goalsToList obligations)
 
-
-proveGoal ::
-  (sym ~ WE.ExprBuilder t st fs) =>
-  CB.IsSymInterface sym =>
-  sym ->
-  WSA.SolverAdapter st ->
-  CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) ->
-  IO ()
-proveGoal sym adapter (CB.ProofGoal asms goal) = do
-  let goalPred = goal ^. CB.labeledPred
-  asmsPred <- CB.assumptionsPred sym asms
-  notgoal <- W4.notPred sym goalPred
-  WSA.solver_adapter_check_sat adapter sym WSA.defaultLogData [notgoal, asmsPred] $ \sr ->
-    case sr of
-      W4R.Unsat _ -> return ()
-      W4R.Unknown -> T.assertFailure "Inconclusive"
-      W4R.Sat _ -> do
+  CB.proveCurrentObligations bak WSA.defaultLogData W4Y.yicesAdapter $
+    \case
+      CB.Proved {} -> return ()
+      CB.Unknown {} -> T.assertFailure "Inconclusive"
+      CB.Disproved (CB.ProofGoal asms goal) _ _ -> do
+        asmsPred <- CB.assumptionsPred sym asms
+        let goalPred = goal ^. CB.labeledPred
         putStrLn (showF asmsPred)
         putStrLn (showF goalPred)
         T.assertFailure "Assertion Failure"

crucible/crucible.cabal

@@ -72,6 +72,9 @@ library
 
   hs-source-dirs: src
 
+  other-modules:
+    Lang.Crucible.Backend.Assumptions
+
   exposed-modules:
     Lang.Crucible.Analysis.DFS
     Lang.Crucible.Analysis.ForwardDataflow
@@ -83,6 +86,7 @@ library
     Lang.Crucible.Backend.AssumptionStack
     Lang.Crucible.Backend.ProofGoals
     Lang.Crucible.Backend.Online
+    Lang.Crucible.Backend.Prove
     Lang.Crucible.Backend.Simple
     Lang.Crucible.Concretize
     Lang.Crucible.CFG.Common