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

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(..), proveCurrentObligations)
 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
@@ -180,19 +180,13 @@ simulateProgramWithExtension mkExt fn theInput outh profh opts hooks =
 
                        getProofObligations bak >>= \case
                          Nothing -> hPutStrLn outh "==== No proof obligations ===="
-                         Just gs ->
-                           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"
-                                     )
-                                )
+                         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"
 
                   _ -> hPutStrLn outh "No suitable main function found"
 

crucible-cli/test-data/simulate/override-nondet-test-both.out.good

@@ -29,8 +29,8 @@ Assuming:
      in not (and v7 v12 (not (and v7 v12)))
 * The branch in nondetBranchesTest from after branch 0 to second branch
     let -- test-data/simulate/override-nondet-test-both.cbl:10:5
-        v43 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i)))
-     in not v43
+        v47 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i)))
+     in not v47
 * The branch in main from test-data/simulate/override-nondet-test-both.cbl:7:12 to first branch
     let -- test-data/simulate/override-nondet-test-both.cbl:7:12
         v7 = eq 0 cw@0:i
@@ -55,8 +55,8 @@ Assuming:
      in not (and v7 v12 (not (and v7 v12)))
 * The branch in nondetBranchesTest from after branch 0 to second branch
     let -- test-data/simulate/override-nondet-test-both.cbl:10:5
-        v54 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i)))
-     in not v54
+        v58 = and (not (and (eq 0 cw@0:i) (eq 0 cnondetBranchesZ@11:i))) (not (and (eq 1 cw@0:i) (eq 1 cnondetBranchesZ@11:i)))
+     in not v58
 * The branch in main from test-data/simulate/override-nondet-test-both.cbl:7:12 to first branch
     let -- test-data/simulate/override-nondet-test-both.cbl:7:12
         v7 = eq 0 cw@0:i

crucible-cli/test-data/simulate/override-test2.out.good

@@ -17,8 +17,8 @@ COUNTEREXAMPLE
 Assuming:
 * The branch in symbolicBranchesTest from after branch 1 to third branch
     let -- test-data/simulate/override-test2.cbl:7:5
-        v30 = and (not (eq 1 cx@0:i)) (not (eq 2 cx@0:i)) (not (eq 3 cx@0:i))
-     in not v30
+        v37 = and (not (eq 1 cx@0:i)) (not (eq 2 cx@0:i)) (not (eq 3 cx@0:i))
+     in not v37
 Prove:
   test-data/simulate/override-test2.cbl:6:5: error: in main
   bogus!

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
@@ -56,7 +57,6 @@ import qualified What4.Expr as WE
 import qualified What4.Config as W4C
 import qualified What4.Solver.Yices as W4Y
 import qualified What4.Solver.Adapter as WSA
-import qualified What4.SatResult as W4R
 import qualified What4.Partial as W4
 
 import qualified What4.CachedArray as CA
@@ -133,26 +133,15 @@ 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 $ \obligation ->
+    \case
+      CB.Proved {} -> return ()
+      CB.Unknown {} -> T.assertFailure "Inconclusive"
+      CB.Disproved  _ _ -> do
+        CB.ProofGoal asms goal <- pure obligation
+        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