copilot-verifier 4.1 → 4.2

raw patch · 3 files changed

+31/−11 lines, 3 filesdep ~copilotdep ~copilot-c99dep ~copilot-corePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: copilot, copilot-c99, copilot-core, copilot-language, copilot-prettyprinter, copilot-theorem

API changes (from Hackage documentation)

Files

• CHANGELOG +4/−0
• copilot-verifier.cabal +7/−7
• src/Copilot/Verifier.hs +20/−4

@@ -1,3 +1,7 @@+2025-01-20+        * Version bump (4.2). (#76)+        * Reject specs that use multiple triggers with the same name. (#74)+ 2024-11-08         * Version bump (4.1). (#72) 

@@ -1,6 +1,6 @@ Cabal-version: 2.2 Name:          copilot-verifier-Version:       4.1+Version:       4.2 Author:        Galois Inc. Maintainer:    rscott@galois.com Copyright:     (c) Galois, Inc 2021-2024@@ -45,9 +45,9 @@     bv-sized >= 1.0.0 && < 1.1,     bytestring,     containers >= 0.5.9.0,-    copilot-c99 >= 4.1 && < 4.2,-    copilot-core >= 4.1 && < 4.2,-    copilot-theorem >= 4.1 && < 4.2,+    copilot-c99 >= 4.2 && < 4.3,+    copilot-core >= 4.2 && < 4.3,+    copilot-theorem >= 4.2 && < 4.3,     crucible >= 0.7.1 && < 0.8,     crucible-llvm >= 0.7 && < 0.8,     crux >= 0.7.1 && < 0.8,@@ -78,9 +78,9 @@   hs-source-dirs: examples   build-depends:     case-insensitive,-    copilot >= 4.1 && < 4.2,-    copilot-language >= 4.1 && < 4.2,-    copilot-prettyprinter >= 4.1 && < 4.2,+    copilot >= 4.2 && < 4.3,+    copilot-language >= 4.2 && < 4.3,+    copilot-prettyprinter >= 4.2 && < 4.3,     copilot-verifier   exposed-modules:     Copilot.Verifier.Examples

@@ -23,7 +23,7 @@   ) where  import Control.Lens (view, (^.), to)-import Control.Monad (foldM, forM_, when)+import Control.Monad (foldM, forM_, unless, when) import Control.Monad.IO.Class (liftIO) import Control.Monad.State (execStateT, lift, StateT(..)) import Data.Aeson (ToJSON)@@ -33,7 +33,7 @@ import qualified Data.Map.Strict as Map import Data.IORef (newIORef, modifyIORef', readIORef, IORef) import qualified Text.LLVM.AST as L-import Data.List (genericLength)+import Data.List (genericLength, sort) import Data.List.NonEmpty (NonEmpty(..)) import qualified Data.List.NonEmpty as NE import qualified Data.Vector as V@@ -511,10 +511,26 @@         let prepTrigger (nm, guard, _) =               do gv <- freshGlobalVar halloc (Text.pack (nm ++ "_called")) NatRepr                  return (nm, gv, guard)-        triggerGlobals <- mapM prepTrigger (CW4.triggerState prfbundle) +            checkDuplicateTriggerNames :: [Name] -> IO ()+            checkDuplicateTriggerNames triggers =+              traverse_ checkDuplicateTriggerName $ NE.group $ sort triggers++            checkDuplicateTriggerName :: NonEmpty Name -> IO ()+            checkDuplicateTriggerName (trig :| dupTrigs) =+              unless (null dupTrigs) $+                fail $ unlines+                  [ "The specification invokes the `" ++ trig +++                    "` trigger function multiple times,"+                  , "which copilot-verifier does not currently support."+                  , "See https://github.com/Copilot-Language/copilot-verifier/issues/74."+                  ]+        let triggerState = CW4.triggerState prfbundle+        checkDuplicateTriggerNames $ map (\(nm,_,_) -> nm) triggerState+        triggerGlobals <- mapM prepTrigger triggerState+         -- execute the step function-        let overrides = zipWith (triggerOverride clRefs) triggerGlobals (CW4.triggerState prfbundle)+        let overrides = zipWith (triggerOverride clRefs) triggerGlobals triggerState         mem'' <- executeStep opts csettings clRefs simctx memVar mem' llvmMod modTrans triggerGlobals overrides (CW4.assumptions prfbundle) (CW4.sideConds prfbundle)          -- assert the poststate is in the relation