crucible-symio 0.1 → 0.1.1

raw patch · 3 files changed

+25/−23 lines, 3 filesdep ~basedep ~cruciblenew-uploaderPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, crucible

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• crucible-symio.cabal +3/−3
• tests/TestMain.hs +18/−20

@@ -1,5 +1,9 @@ # Revision history for crucible-symio +## 0.1.1 -- 2024-08-30++* Add support for GHC 9.8+ ## 0.1 -- 2024-02-05  * First version. Released on an unsuspecting world.

@@ -6,7 +6,7 @@   reading and writing symbolic data. An example use case would be to support verifying   programs that e.g., use configuration files or accept input from files. name:                crucible-symio-version:             0.1+version:             0.1.1 license:             BSD-3-Clause license-file:        LICENSE author:              Daniel Matichuk@@ -21,7 +21,7 @@   subdir:   crucible-symio  common shared-  build-depends:       base >=4.12 && <4.19,+  build-depends:       base >=4.12 && <4.20,                        aeson,                        bv-sized,                        bytestring,@@ -63,7 +63,7 @@   main-is: TestMain.hs   hs-source-dirs: tests, src   ghc-options: -Wall -Wcompat-  build-depends: base >=4.12 && <4.19,+  build-depends: base >=4.12 && <4.20,                  what4,                  crucible,                  crucible-symio,

@@ -27,6 +27,7 @@ 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@@ -42,6 +43,7 @@ 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@@ -50,13 +52,14 @@ 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 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,29 +136,24 @@         _ -> 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+  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"+      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"+  case merr of+    Left CTO.TimedOut -> T.assertFailure "Timeout"+    Right () -> pure ()  showAbortedResult :: CS.AbortedResult c d -> String showAbortedResult ar = case ar of