Use goal-proving helpers in crucible-symio test suite

GaloisInc · Jun 18, 2024 · 625051d · 625051d
1 parent b0fe72b
commit 625051d
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 20 deletions.
diff --git a/crucible-symio/tests/TestMain.hs b/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
+  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"

diff --git a/crucible/crucible.cabal b/crucible/crucible.cabal
@@ -74,7 +74,6 @@ library
 
   other-modules:
     Lang.Crucible.Backend.Assumptions
-    Lang.Crucible.Backend.Prove
 
   exposed-modules:
     Lang.Crucible.Analysis.DFS
@@ -87,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