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) 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/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 diff --git a/copilot-c99/src/Copilot/Compile/C99/Compile.hs b/copilot-c99/src/Copilot/Compile/C99/Compile.hs index 51507825..1467af40 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 @@ -23,17 +24,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. -- @@ -42,12 +47,20 @@ import Copilot.Compile.C99.Type ( transType ) -- 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 @@ -69,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. -- @@ -90,12 +121,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 +142,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 +154,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) = @@ -155,7 +187,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 @@ -256,3 +290,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 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