From 4cd80053f7a5bec550b11c379c156fb8866fa413 Mon Sep 17 00:00:00 2001
From: Frank Dedden <frank@systemf.dev>
Date: Fri, 20 Dec 2024 08:39:48 +0100
Subject: [PATCH] copilot-c99: Disallow conflicting trigger definitions. Refs
 #296.

The current implementation of Copilot does not allow using the same
trigger handler name multiple times, since the C99 backend produces
multiple repeated declarations, which is invalid.

Prior commits have modified the C99 backend to now allow for
multiple triggers with the same handler. However, the resulting code
is only valid in C if the triggers always have the same type signatures,
since C does not support polymorphism.

This commit adds a check to the compilation step to ensure that triggers
used multiple times are always used with the same types (and,
consequently, the same arity).
---
 .../src/Copilot/Compile/C99/Compile.hs        | 28 ++++++++++++++++++-
 1 file changed, 27 insertions(+), 1 deletion(-)

diff --git a/copilot-c99/src/Copilot/Compile/C99/Compile.hs b/copilot-c99/src/Copilot/Compile/C99/Compile.hs
index 7ee08396..1467af40 100644
--- a/copilot-c99/src/Copilot/Compile/C99/Compile.hs
+++ b/copilot-c99/src/Copilot/Compile/C99/Compile.hs
@@ -47,12 +47,20 @@ import Copilot.Compile.C99.Representation ( UniqueTrigger (..),
 -- The second argument is used as prefix for the .h and .c files generated.
 compileWith :: CSettings -> String -> Spec -> IO ()
 compileWith cSettings prefix spec
-  | null (specTriggers spec)
+  | null triggers
   = do hPutStrLn stderr $
          "Copilot error: attempt at compiling empty specification.\n"
          ++ "You must define at least one trigger to generate C monitors."
        exitFailure
 
+  | incompatibleTriggers triggers
+  = do hPutStrLn stderr $
+         "Copilot error: attempt at compiling specification with conflicting "
+         ++ "trigger definitions.\n"
+         ++ "Multiple triggers have the same name, but different argument "
+         ++ "types.\n"
+       exitFailure
+
   | otherwise
   = do let cFile = render $ pretty $ C.translate $ compileC cSettings spec
            hFile = render $ pretty $ C.translate $ compileH cSettings spec
@@ -74,6 +82,24 @@ compileWith cSettings prefix spec
        writeFile (dir </> prefix ++ ".c") $ cMacros ++ cFile
        writeFile (dir </> prefix ++ ".h") hFile
        writeFile (dir </> prefix ++ "_types.h") typeDeclnsFile
+  where
+    triggers = specTriggers spec
+
+    -- Check that two triggers do no conflict, that is: if their names are
+    -- equal, the types of their arguments should be equal as well.
+    incompatibleTriggers :: [Trigger] -> Bool
+    incompatibleTriggers = pairwiseAny conflict
+      where
+        conflict :: Trigger -> Trigger -> Bool
+        conflict t1@(Trigger name1 _ _) t2@(Trigger name2 _ _) =
+          name1 == name2 && not (compareTrigger t1 t2)
+
+        -- True if the function holds for any pair of elements. We assume that
+        -- the function is commutative.
+        pairwiseAny :: (a -> a -> Bool) -> [a] -> Bool
+        pairwiseAny _ []     = False
+        pairwiseAny _ (_:[]) = False
+        pairwiseAny f (x:xs) = any (f x) xs || pairwiseAny f xs
 
 -- | Compile a specification to a .h and a .c file.
 --