Skip to content

Reject multiple triggers with the same name. Refs #74. #75

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
RyanGlScott merged 2 commits into from
Jan 20, 2025
Merged

Reject multiple triggers with the same name. Refs #74. #75

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f694d21
Reject multiple triggers with the same name. Refs #74.
RyanGlScott Jan 20, 2025
67b270e
Document changes in the CHANGELOG. Refs #74.
RyanGlScott Jan 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions copilot-verifier/CHANGELOG
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
2025-01-20
* Reject specs that use multiple triggers with the same name. (#74)

2024-11-08
* Version bump (4.1). (#72)

Expand Down
24 changes: 20 additions & 4 deletions copilot-verifier/src/Copilot/Verifier.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ module Copilot.Verifier
) 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)
Expand All @@ -33,7 +33,7 @@ import qualified Data.Text as Text
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
Expand Down Expand Up @@ -511,10 +511,26 @@ verifyStepBisimulation opts cruxOpts adapters csettings clRefs simctx llvmMod mo
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
Expand Down