From f694d21e8621b9928787a3156f8125280ffbd01f Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 20 Jan 2025 15:24:44 -0500
Subject: [PATCH 1/2] Reject multiple triggers with the same name. Refs #74.

Although `copilot-c99` added the ability to invoke multiple triggers with the
same name in https://github.com/Copilot-Language/copilot/pull/572, it is not
yet clear how best to support this in `copilot-verifier`.

In the meantime, this adds an explicit check that rules out specifications that
use multiple triggers with the same name to prevent the verifier from becoming
confused by them. The remaining task of fully supporting such specifications is
tracked in https://github.com/Copilot-Language/copilot-verifier/issues/74.
---
 copilot-verifier/src/Copilot/Verifier.hs | 24 ++++++++++++++++++++----
 1 file changed, 20 insertions(+), 4 deletions(-)

diff --git a/copilot-verifier/src/Copilot/Verifier.hs b/copilot-verifier/src/Copilot/Verifier.hs
index d4df725..3196bdf 100644
--- a/copilot-verifier/src/Copilot/Verifier.hs
+++ b/copilot-verifier/src/Copilot/Verifier.hs
@@ -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)
@@ -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
@@ -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

From 67b270e71bcf624b46f69790b61011b8bfac2eb0 Mon Sep 17 00:00:00 2001
From: Ryan Scott <rscott@galois.com>
Date: Mon, 20 Jan 2025 15:26:48 -0500
Subject: [PATCH 2/2] Document changes in the CHANGELOG. Refs #74.

---
 copilot-verifier/CHANGELOG | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/copilot-verifier/CHANGELOG b/copilot-verifier/CHANGELOG
index a5a01b8..74f1dc6 100644
--- a/copilot-verifier/CHANGELOG
+++ b/copilot-verifier/CHANGELOG
@@ -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)