From 5ac80921bc95846804006a64699070d7145d0e1a Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Fri, 20 Dec 2024 08:39:48 +0100 Subject: [PATCH 1/6] copilot-c99: Add specific `Trigger` representation. 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. Consequently, the code generator assumes that trigger names are unique. To allow for multiple triggers that trigger the same handler, we need to introduce a separate construct in triggers that acts as a unique identifier. This commit introduces an internal datatype to represent a `Trigger` with a unique name that is different from that of the function called when triggered. --- copilot-c99/copilot-c99.cabal | 1 + .../src/Copilot/Compile/C99/Representation.hs | 21 +++++++++++++++++++ 2 files changed, 22 insertions(+) create mode 100644 copilot-c99/src/Copilot/Compile/C99/Representation.hs diff --git a/copilot-c99/copilot-c99.cabal b/copilot-c99/copilot-c99.cabal index f6a196b8..4e441d31 100644 --- a/copilot-c99/copilot-c99.cabal +++ b/copilot-c99/copilot-c99.cabal @@ -59,6 +59,7 @@ library , Copilot.Compile.C99.External , Copilot.Compile.C99.Compile , Copilot.Compile.C99.Settings + , Copilot.Compile.C99.Representation test-suite unit-tests type: diff --git a/copilot-c99/src/Copilot/Compile/C99/Representation.hs b/copilot-c99/src/Copilot/Compile/C99/Representation.hs new file mode 100644 index 00000000..886808a8 --- /dev/null +++ b/copilot-c99/src/Copilot/Compile/C99/Representation.hs @@ -0,0 +1,21 @@ +-- | C99 backend specific versions of selected `Copilot.Core` datatypes. +module Copilot.Compile.C99.Representation + ( UniqueTrigger (..) + , UniqueTriggerId + , mkUniqueTriggers + ) + where + +import Copilot.Core ( Trigger (..) ) + +-- | Internal unique name for a trigger. +type UniqueTriggerId = String + +-- | A `Copilot.Core.Trigger` with an unique name. +data UniqueTrigger = UniqueTrigger UniqueTriggerId Trigger + +-- | Given a list of triggers, make their names unique. +mkUniqueTriggers :: [Trigger] -> [UniqueTrigger] +mkUniqueTriggers ts = zipWith mkUnique ts [0..] + where + mkUnique t@(Trigger name _ _) n = UniqueTrigger (name ++ "_" ++ show n) t From e6356ef260524abbaf5891e2822bcb0ef5d3d3cf Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Fri, 20 Dec 2024 08:39:48 +0100 Subject: [PATCH 2/6] copilot-c99: Adapt `mkStep` to use unique triggers. 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. A prior commit has introduced a representation of triggers with unique IDs, allowing us to distinguish between a monitor for one condition within a Copilot spec vs the external C function being called when the condition becomes true. This commit updates the generation of the `step` function to use unique names for the triggers. --- .../src/Copilot/Compile/C99/CodeGen.hs | 33 +++++++++++-------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs index e71e7a0d..ce822e55 100644 --- a/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs +++ b/copilot-c99/src/Copilot/Compile/C99/CodeGen.hs @@ -36,14 +36,17 @@ import Copilot.Core ( Expr (..), Id, Stream (..), Struct (..), Trigger (..), Type (..), UExpr (..), Value (..), fieldName, typeSize ) -- Internal imports -import Copilot.Compile.C99.Error ( impossible ) -import Copilot.Compile.C99.Expr ( constArray, transExpr ) -import Copilot.Compile.C99.External ( External (..) ) -import Copilot.Compile.C99.Name ( argNames, argTempNames, generatorName, - guardName, indexName, streamAccessorName, - streamName ) -import Copilot.Compile.C99.Settings ( CSettings, cSettingsStepFunctionName ) -import Copilot.Compile.C99.Type ( transType ) +import Copilot.Compile.C99.Error ( impossible ) +import Copilot.Compile.C99.Expr ( constArray, transExpr ) +import Copilot.Compile.C99.External ( External (..) ) +import Copilot.Compile.C99.Name ( argNames, argTempNames, + generatorName, guardName, + indexName, streamAccessorName, + streamName ) +import Copilot.Compile.C99.Settings ( CSettings, + cSettingsStepFunctionName ) +import Copilot.Compile.C99.Type ( transType ) +import Copilot.Compile.C99.Representation ( UniqueTrigger (..) ) -- * Externs @@ -162,7 +165,7 @@ mkGenFunArray _name _nameArg _expr _ty = -- * Monitor processing -- | Define the step function that updates all streams. -mkStep :: CSettings -> [Stream] -> [Trigger] -> [External] -> C.FunDef +mkStep :: CSettings -> [Stream] -> [UniqueTrigger] -> [External] -> C.FunDef mkStep cSettings streams triggers exts = C.FunDef Nothing void (cSettingsStepFunctionName cSettings) [] declns stmts where @@ -271,8 +274,8 @@ mkStep cSettings streams triggers exts = -- 2. Assigning a struct to a temporary variable defensively ensures that -- any modifications that the handler called makes to the struct argument -- will not affect the internals of the monitoring code. - mkTriggerCheck :: Trigger -> ([C.Decln], C.Stmt) - mkTriggerCheck (Trigger name _guard args) = + mkTriggerCheck :: UniqueTrigger -> ([C.Decln], C.Stmt) + mkTriggerCheck (UniqueTrigger uniqueName (Trigger name _guard args)) = (aTmpDeclns, triggerCheckStmt) where aTmpDeclns :: [C.Decln] @@ -285,12 +288,14 @@ mkStep cSettings streams triggers exts = triggerCheckStmt :: C.Stmt triggerCheckStmt = C.If guard' fireTrigger where - guard' = C.Funcall (C.Ident $ guardName name) [] + guard' = C.Funcall (C.Ident $ guardName uniqueName) [] -- The body of the if-statement. This consists of statements that -- assign the values of the temporary variables, following by a -- final statement that passes the temporary variables to the -- handler function. + -- Note that we call 'name' here instead of 'uniqueName', as 'name' + -- is the name of the actual external function. fireTrigger = map C.Expr argAssigns ++ [C.Expr $ C.Funcall (C.Ident name) @@ -305,7 +310,7 @@ mkStep cSettings streams triggers exts = updateVar aTempName aArgName ty aArgNames :: [C.Ident] - aArgNames = take (length args) (argNames name) + aArgNames = take (length args) (argNames uniqueName) -- Build an expression to pass a temporary variable as argument -- to a trigger handler. @@ -323,7 +328,7 @@ mkStep cSettings streams triggers exts = _ -> C.Ident aTempName aTempNames :: [String] - aTempNames = take (length args) (argTempNames name) + aTempNames = take (length args) (argTempNames uniqueName) -- * Auxiliary functions From c1f273817e166e134b2e937579d63f327bb72c4d Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Fri, 20 Dec 2024 08:39:48 +0100 Subject: [PATCH 3/6] copilot-c99: Adapt top-level compilation functions to use unique triggers. 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 introduced a representation of triggers with unique IDs (allowing us to distinguish between a monitor for one condition within a Copilot spec vs the external C function being called when the condition becomes true), and have adapted low-level functions accordingly. This commit adapts the top-level compilation functions in the same way, by generating trigger guards and argument functions using the unique names. --- .../src/Copilot/Compile/C99/Compile.hs | 47 ++++++++++--------- 1 file changed, 26 insertions(+), 21 deletions(-) diff --git a/copilot-c99/src/Copilot/Compile/C99/Compile.hs b/copilot-c99/src/Copilot/Compile/C99/Compile.hs index 51507825..b7e676a3 100644 --- a/copilot-c99/src/Copilot/Compile/C99/Compile.hs +++ b/copilot-c99/src/Copilot/Compile/C99/Compile.hs @@ -23,17 +23,21 @@ import Copilot.Core ( Expr (..), Spec (..), Stream (..), Struct (..), Value (..) ) -- Internal imports -import Copilot.Compile.C99.CodeGen ( mkAccessDecln, mkBuffDecln, mkExtCpyDecln, - mkExtDecln, mkGenFun, mkGenFunArray, - mkIndexDecln, mkStep, mkStructDecln, - mkStructForwDecln ) -import Copilot.Compile.C99.External ( External, gatherExts ) -import Copilot.Compile.C99.Name ( argNames, generatorName, - generatorOutputArgName, guardName ) -import Copilot.Compile.C99.Settings ( CSettings, cSettingsOutputDirectory, - cSettingsStepFunctionName, - mkDefaultCSettings ) -import Copilot.Compile.C99.Type ( transType ) +import Copilot.Compile.C99.CodeGen ( mkAccessDecln, mkBuffDecln, + mkExtCpyDecln, mkExtDecln, + mkGenFun, mkGenFunArray, + mkIndexDecln, mkStep, + mkStructDecln, mkStructForwDecln ) +import Copilot.Compile.C99.External ( External, gatherExts ) +import Copilot.Compile.C99.Name ( argNames, generatorName, + generatorOutputArgName, guardName ) +import Copilot.Compile.C99.Settings ( CSettings, + cSettingsOutputDirectory, + cSettingsStepFunctionName, + mkDefaultCSettings ) +import Copilot.Compile.C99.Type ( transType ) +import Copilot.Compile.C99.Representation ( UniqueTrigger (..), + mkUniqueTriggers ) -- | Compile a specification to a .h and a .c file. -- @@ -90,12 +94,13 @@ compileC cSettings spec = C.TransUnit declns funs declns = mkExts exts ++ mkGlobals streams - funs = mkGenFuns streams triggers - ++ [mkStep cSettings streams triggers exts] + funs = mkGenFuns streams uniqueTriggers + ++ [mkStep cSettings streams uniqueTriggers exts] - streams = specStreams spec - triggers = specTriggers spec - exts = gatherExts streams triggers + streams = specStreams spec + triggers = specTriggers spec + uniqueTriggers = mkUniqueTriggers triggers + exts = gatherExts streams triggers -- Make declarations for copies of external variables. mkExts :: [External] -> [C.Decln] @@ -110,7 +115,7 @@ compileC cSettings spec = C.TransUnit declns funs indexDecln (Stream sId _ _ _ ) = mkIndexDecln sId -- Make generator functions, including trigger arguments. - mkGenFuns :: [Stream] -> [Trigger] -> [C.FunDef] + mkGenFuns :: [Stream] -> [UniqueTrigger] -> [C.FunDef] mkGenFuns streamList triggerList = map accessDecln streamList ++ map streamGen streamList ++ concatMap triggerGen triggerList @@ -122,11 +127,11 @@ compileC cSettings spec = C.TransUnit declns funs streamGen (Stream sId _ expr ty) = exprGen (generatorName sId) (generatorOutputArgName sId) expr ty - triggerGen :: Trigger -> [C.FunDef] - triggerGen (Trigger name guard args) = guardDef : argDefs + triggerGen :: UniqueTrigger -> [C.FunDef] + triggerGen (UniqueTrigger uniqueName (Trigger _name guard args)) = guardDef : argDefs where - guardDef = mkGenFun (guardName name) guard Bool - argDefs = zipWith argGen (argNames name) args + guardDef = mkGenFun (guardName uniqueName) guard Bool + argDefs = zipWith argGen (argNames uniqueName) args argGen :: String -> UExpr -> C.FunDef argGen argName (UExpr ty expr) = From 3f866c8bfea320ff43afda403b8e470af0caf9de Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Fri, 20 Dec 2024 08:39:48 +0100 Subject: [PATCH 4/6] copilot-c99: Remove duplicate trigger declarations in .h output. Refs #296. The current implementation of Copilot's C99 backend produces multiple repeated declarations when the same trigger is used multiple times, which is invalid C code. This commit modifies the code that generates the header file to prevent the same trigger from being declared multiple times. --- .../src/Copilot/Compile/C99/Compile.hs | 25 +++++++++++++++++-- 1 file changed, 23 insertions(+), 2 deletions(-) diff --git a/copilot-c99/src/Copilot/Compile/C99/Compile.hs b/copilot-c99/src/Copilot/Compile/C99/Compile.hs index b7e676a3..7ee08396 100644 --- a/copilot-c99/src/Copilot/Compile/C99/Compile.hs +++ b/copilot-c99/src/Copilot/Compile/C99/Compile.hs @@ -6,8 +6,9 @@ module Copilot.Compile.C99.Compile ) where -- External imports -import Data.List ( nub, union ) +import Data.List ( nub, nubBy, union ) import Data.Maybe ( mapMaybe ) +import Data.Type.Equality ( testEquality, (:~:)(Refl) ) import Data.Typeable ( Typeable ) import Language.C99.Pretty ( pretty ) import qualified Language.C99.Simple as C @@ -160,7 +161,9 @@ compileH cSettings spec = C.TransUnit declns [] exprs = gatherExprs streams triggers exts = gatherExts streams triggers streams = specStreams spec - triggers = specTriggers spec + + -- Remove duplicates due to multiple guards for the same trigger. + triggers = nubBy compareTrigger (specTriggers spec) mkStructForwDeclns :: [UExpr] -> [C.Decln] mkStructForwDeclns es = mapMaybe mkDecln uTypes @@ -261,3 +264,21 @@ gatherExprs streams triggers = map streamUExpr streams where streamUExpr (Stream _ _ expr ty) = UExpr ty expr triggerUExpr (Trigger _ guard args) = UExpr Bool guard : args + +-- | We consider triggers to be equal, if their names match and the number and +-- types of arguments. +compareTrigger :: Trigger -> Trigger -> Bool +compareTrigger (Trigger name1 _ args1) (Trigger name2 _ args2) + = name1 == name2 && compareArguments args1 args2 + + where + compareArguments :: [UExpr] -> [UExpr] -> Bool + compareArguments [] [] = True + compareArguments [] _ = False + compareArguments _ [] = False + compareArguments (x:xs) (y:ys) = compareUExpr x y && compareArguments xs ys + + compareUExpr :: UExpr -> UExpr -> Bool + compareUExpr (UExpr ty1 _) (UExpr ty2 _) + | Just Refl <- testEquality ty1 ty2 = True + | otherwise = False From 4cd80053f7a5bec550b11c379c156fb8866fa413 Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Fri, 20 Dec 2024 08:39:48 +0100 Subject: [PATCH 5/6] 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. -- From 1d389490d6e1017932679bb7a639dd9856bd04f8 Mon Sep 17 00:00:00 2001 From: Frank Dedden Date: Fri, 20 Dec 2024 09:02:26 +0100 Subject: [PATCH 6/6] copilot-c99: Document changes in CHANGELOG. Refs #296. --- copilot-c99/CHANGELOG | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/copilot-c99/CHANGELOG b/copilot-c99/CHANGELOG index 50c704f2..635e0021 100644 --- a/copilot-c99/CHANGELOG +++ b/copilot-c99/CHANGELOG @@ -1,5 +1,6 @@ -2024-11-14 +2024-12-20 * Remove uses of Copilot.Core.Expr.UExpr.uExprType. (#565) + * Allow using same trigger name in multiple declarations. (#296) 2024-11-07 * Version bump (4.1). (#561)