Refactoring of goal-proving helpers, more use in crucible-cli

GaloisInc · Jun 20, 2024 · ee97a5d · ee97a5d
1 parent 672f0a0
commit ee97a5d
Show file tree

Hide file tree

Showing 5 changed files with 29 additions and 35 deletions.
diff --git a/crucible-cli/src/Lang/Crucible/CLI.hs b/crucible-cli/src/Lang/Crucible/CLI.hs
@@ -49,7 +49,7 @@ 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.Prove (ProofResult(..), proveCurrentObligations)
 import Lang.Crucible.Backend.Simple
 import Lang.Crucible.FunctionHandle
 import Lang.Crucible.Simulator
@@ -180,16 +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
-                                   proveProofGoal sym defaultLogData z3Adapter g $
-                                     \case
-                                       Proved {} -> hPutStrLn outh "PROVED"
-                                       Disproved {} -> hPutStrLn outh "COUNTEREXAMPLE"
-                                       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"
 

diff --git a/crucible-cli/test-data/simulate/override-nondet-test-both.out.good b/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

diff --git a/crucible-cli/test-data/simulate/override-test2.out.good b/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!

diff --git a/crucible-symio/tests/TestMain.hs b/crucible-symio/tests/TestMain.hs
@@ -57,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
@@ -135,11 +134,12 @@ runFSTest' bak (FSTest fsTest) = do
           putStrLn $ showF p
           T.assertFailure "Partial Result"
 
-  CB.proveCurrentObligations bak WSA.defaultLogData W4Y.yicesAdapter $
+  CB.proveCurrentObligations bak WSA.defaultLogData W4Y.yicesAdapter $ \obligation ->
     \case
       CB.Proved {} -> return ()
       CB.Unknown {} -> T.assertFailure "Inconclusive"
-      CB.Disproved (CB.ProofGoal asms goal) _ _ -> do
+      CB.Disproved  _ _ -> do
+        CB.ProofGoal asms goal <- pure obligation
         asmsPred <- CB.assumptionsPred sym asms
         let goalPred = goal ^. CB.labeledPred
         putStrLn (showF asmsPred)

diff --git a/crucible/src/Lang/Crucible/Backend/Prove.hs b/crucible/src/Lang/Crucible/Backend/Prove.hs
@@ -30,24 +30,22 @@ import qualified Lang.Crucible.Backend as CB
 import           Lang.Crucible.Backend.Assumptions (Assumptions)
 import           Lang.Crucible.Backend.ProofGoals (traverseGoalsWithAssumptions)
 
-type Goal sym = CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym)
-
 -- | The result of attempting to prove a goal with an SMT solver.
 --
 -- The constructors of this type correspond to those of 'W4R.SatResult'.
 data ProofResult sym t
    = -- | The goal was proved
      --
      -- Corresponds to 'W4R.Unsat'.
-     Proved (Goal sym)
+     Proved
      -- | The goal was disproved, and a model that falsifies it is available.
      --
      -- Corresponds to 'W4R.Sat'.
-   | Disproved (Goal sym) (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t))
+   | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t))
      -- | The SMT solver returned \"unknown\".
      --
      -- Corresponds to 'W4R.Unknown'.
-   | Unknown (Goal sym)
+   | Unknown
 
 -- | Prove a single goal.
 proveGoal ::
@@ -59,19 +57,18 @@ proveGoal ::
   Assumptions sym ->
   CB.Assertion sym ->
   -- | Continuation to process the 'ProofResult'.
-  (ProofResult sym t -> IO r) ->
+  (CB.ProofObligation sym -> ProofResult sym t -> IO r) ->
   IO r
 proveGoal sym ld adapter asms goal k = do
   let goalPred = goal ^. CB.labeledPred
   asmsPred <- CB.assumptionsPred sym asms
   notGoal <- W4.notPred sym goalPred
-  let goal' = CB.ProofGoal asms goal
   WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $
-    k .
+    k (CB.ProofGoal asms goal) .
       \case
-        W4R.Sat (gfn, binds) -> Disproved goal' gfn binds
-        W4R.Unsat () -> Proved goal'
-        W4R.Unknown -> Unknown goal'
+        W4R.Sat (gfn, binds) -> Disproved gfn binds
+        W4R.Unsat () -> Proved
+        W4R.Unknown -> Unknown
 
 -- | Prove a single 'CB.ProofGoal'.
 proveProofGoal ::
@@ -82,7 +79,7 @@ proveProofGoal ::
   WSA.SolverAdapter st ->
   CB.ProofGoal (CB.Assumptions sym) (CB.Assertion sym) ->
   -- | Continuation to process the 'ProofResult'.
-  (ProofResult sym t -> IO r) ->
+  (CB.ProofObligation sym -> ProofResult sym t -> IO r) ->
   IO r
 proveProofGoal sym ld adapter (CB.ProofGoal asms goal) =
   proveGoal sym ld adapter asms goal
@@ -96,7 +93,7 @@ proveGoals ::
   WSA.SolverAdapter st ->
   CB.Goals (CB.Assumptions sym) (CB.Assertion sym) ->
   -- | Continuation to process the 'ProofResult'.
-  (ProofResult sym t -> IO m) ->
+  (CB.ProofObligation sym -> ProofResult sym t -> IO m) ->
   IO m
 proveGoals sym ld adapter goals k =
   getConst $
@@ -112,7 +109,7 @@ proveObligations ::
   WSA.SolverAdapter st ->
   CB.ProofObligations sym ->
   -- | Continuation to process the 'ProofResult'.
-  (ProofResult sym t -> IO m) ->
+  (CB.ProofObligation sym -> ProofResult sym t -> IO m) ->
   IO m
 proveObligations sym ld adapter obligations k =
   case obligations of
@@ -127,7 +124,7 @@ proveCurrentObligations ::
   WSA.LogData ->
   WSA.SolverAdapter st ->
   -- | Continuation to process the 'ProofResult'.
-  (ProofResult sym t -> IO m) ->
+  (CB.ProofObligation sym -> ProofResult sym t -> IO m) ->
   IO m
 proveCurrentObligations bak ld adapter k = do
   obligations <- CB.getProofObligations bak