Skip to content

Commit 86a9ce0

Browse files
ivanperez-keeraivanperez-keera
committed
Merge remote-tracking branch 'fdedden/develop-multiple-triggers'. Close #296.
**Description** 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. So long as the types do not change, or so long as the target language allows for method/function overloading, then the Copilot spec should accept them. **Type** - Feature: extend valid specifications to allow multiple triggers with the same handler. **Additional context** None. **Requester** - Antanas Kalkauskas (Sensemtry). **Method to check presence of bug** Not applicable (not a bug). **Expected result** Copilot accepts specs where there are two triggers with the same name, so long as the types of the arguments (and their arity) is the same. The following dockerfile checks that a spec with the same trigger name used multiple times can be compiled correctly, and the resulting C code also compiles, after which it prints the message "Success": ``` --- Dockerfile-verify-296 FROM ubuntu:trusty RUN apt-get update RUN apt-get install --yes software-properties-common RUN add-apt-repository ppa:hvr/ghc RUN apt-get update RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4 RUN apt-get install --yes libz-dev ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH RUN cabal update RUN cabal v1-sandbox init RUN cabal v1-install alex happy RUN apt-get install --yes git ADD MultipleTriggers.hs /tmp/MultipleTriggers.hs SHELL ["/bin/bash", "-c"] CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \ && cabal v1-install $NAME/copilot**/ \ && cabal v1-exec -- runhaskell /tmp/MultipleTriggers.hs \ && gcc -c triggers.c \ && echo "Success" --- MultipleTriggers.hs import Language.Copilot import Copilot.Compile.C99 import Prelude hiding ((>), (<), div) -- External temperature as a byte, range of -50C to 100C temp :: Stream Word8 temp = extern "temperature" Nothing spec = do -- Triggers that fire when the temp is too low or too high, pass the current -- temp as an argument. trigger "adjust" (temp < 18) [arg temp] trigger "adjust" (temp > 21) [arg temp] -- Compile the spec main = reify spec >>= compile "triggers" ``` Command (substitute variables based on new path after merge): ``` $ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-296 ``` **Solution implemented** Introduce a new type to represent triggers with a unique name in the generated C code. The unique trigger names are local to the C implementation and are not visible in the generated C header file. Modify implementation to use the unique triggers instead of the pre-existing triggers, assigning them unique names. Modify C header file generator to remove duplicate handler declarations. Modify top-level checks run prior to code generation to check that multiple triggers referring to the same handler pass arguments with the same types in both cases (since C does not support function polymorphism). **Further notes** None.
2 parents 5380279 + 1d38949 commit 86a9ce0

File tree

5 files changed

+119
-39
lines changed

5 files changed

+119
-39
lines changed

‎copilot-c99/CHANGELOG‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1-
2024-11-14
1+
2024-12-20
22
* Remove uses of Copilot.Core.Expr.UExpr.uExprType. (#565)
3+
* Allow using same trigger name in multiple declarations. (#296)
34

45
2024-11-07
56
* Version bump (4.1). (#561)

‎copilot-c99/copilot-c99.cabal‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,7 @@ library
5959
, Copilot.Compile.C99.External
6060
, Copilot.Compile.C99.Compile
6161
, Copilot.Compile.C99.Settings
62+
, Copilot.Compile.C99.Representation
6263

6364
test-suite unit-tests
6465
type:

‎copilot-c99/src/Copilot/Compile/C99/CodeGen.hs‎

Lines changed: 19 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -36,14 +36,17 @@ import Copilot.Core ( Expr (..), Id, Stream (..), Struct (..), Trigger (..),
3636
Type (..), UExpr (..), Value (..), fieldName, typeSize )
3737

3838
-- Internal imports
39-
import Copilot.Compile.C99.Error ( impossible )
40-
import Copilot.Compile.C99.Expr ( constArray, transExpr )
41-
import Copilot.Compile.C99.External ( External (..) )
42-
import Copilot.Compile.C99.Name ( argNames, argTempNames, generatorName,
43-
guardName, indexName, streamAccessorName,
44-
streamName )
45-
import Copilot.Compile.C99.Settings ( CSettings, cSettingsStepFunctionName )
46-
import Copilot.Compile.C99.Type ( transType )
39+
import Copilot.Compile.C99.Error ( impossible )
40+
import Copilot.Compile.C99.Expr ( constArray, transExpr )
41+
import Copilot.Compile.C99.External ( External (..) )
42+
import Copilot.Compile.C99.Name ( argNames, argTempNames,
43+
generatorName, guardName,
44+
indexName, streamAccessorName,
45+
streamName )
46+
import Copilot.Compile.C99.Settings ( CSettings,
47+
cSettingsStepFunctionName )
48+
import Copilot.Compile.C99.Type ( transType )
49+
import Copilot.Compile.C99.Representation ( UniqueTrigger (..) )
4750

4851
-- * Externs
4952

@@ -162,7 +165,7 @@ mkGenFunArray _name _nameArg _expr _ty =
162165
-- * Monitor processing
163166

164167
-- | Define the step function that updates all streams.
165-
mkStep :: CSettings -> [Stream] -> [Trigger] -> [External] -> C.FunDef
168+
mkStep :: CSettings -> [Stream] -> [UniqueTrigger] -> [External] -> C.FunDef
166169
mkStep cSettings streams triggers exts =
167170
C.FunDef Nothing void (cSettingsStepFunctionName cSettings) [] declns stmts
168171
where
@@ -271,8 +274,8 @@ mkStep cSettings streams triggers exts =
271274
-- 2. Assigning a struct to a temporary variable defensively ensures that
272275
-- any modifications that the handler called makes to the struct argument
273276
-- will not affect the internals of the monitoring code.
274-
mkTriggerCheck :: Trigger -> ([C.Decln], C.Stmt)
275-
mkTriggerCheck (Trigger name _guard args) =
277+
mkTriggerCheck :: UniqueTrigger -> ([C.Decln], C.Stmt)
278+
mkTriggerCheck (UniqueTrigger uniqueName (Trigger name _guard args)) =
276279
(aTmpDeclns, triggerCheckStmt)
277280
where
278281
aTmpDeclns :: [C.Decln]
@@ -285,12 +288,14 @@ mkStep cSettings streams triggers exts =
285288
triggerCheckStmt :: C.Stmt
286289
triggerCheckStmt = C.If guard' fireTrigger
287290
where
288-
guard' = C.Funcall (C.Ident $ guardName name) []
291+
guard' = C.Funcall (C.Ident $ guardName uniqueName) []
289292

290293
-- The body of the if-statement. This consists of statements that
291294
-- assign the values of the temporary variables, following by a
292295
-- final statement that passes the temporary variables to the
293296
-- handler function.
297+
-- Note that we call 'name' here instead of 'uniqueName', as 'name'
298+
-- is the name of the actual external function.
294299
fireTrigger = map C.Expr argAssigns
295300
++ [C.Expr $
296301
C.Funcall (C.Ident name)
@@ -305,7 +310,7 @@ mkStep cSettings streams triggers exts =
305310
updateVar aTempName aArgName ty
306311

307312
aArgNames :: [C.Ident]
308-
aArgNames = take (length args) (argNames name)
313+
aArgNames = take (length args) (argNames uniqueName)
309314

310315
-- Build an expression to pass a temporary variable as argument
311316
-- to a trigger handler.
@@ -323,7 +328,7 @@ mkStep cSettings streams triggers exts =
323328
_ -> C.Ident aTempName
324329

325330
aTempNames :: [String]
326-
aTempNames = take (length args) (argTempNames name)
331+
aTempNames = take (length args) (argTempNames uniqueName)
327332

328333
-- * Auxiliary functions
329334

‎copilot-c99/src/Copilot/Compile/C99/Compile.hs‎

Lines changed: 76 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,9 @@ module Copilot.Compile.C99.Compile
66
) where
77

88
-- External imports
9-
import Data.List ( nub, union )
9+
import Data.List ( nub, nubBy, union )
1010
import Data.Maybe ( mapMaybe )
11+
import Data.Type.Equality ( testEquality, (:~:)(Refl) )
1112
import Data.Typeable ( Typeable )
1213
import Language.C99.Pretty ( pretty )
1314
import qualified Language.C99.Simple as C
@@ -23,17 +24,21 @@ import Copilot.Core ( Expr (..), Spec (..), Stream (..), Struct (..),
2324
Value (..) )
2425

2526
-- Internal imports
26-
import Copilot.Compile.C99.CodeGen ( mkAccessDecln, mkBuffDecln, mkExtCpyDecln,
27-
mkExtDecln, mkGenFun, mkGenFunArray,
28-
mkIndexDecln, mkStep, mkStructDecln,
29-
mkStructForwDecln )
30-
import Copilot.Compile.C99.External ( External, gatherExts )
31-
import Copilot.Compile.C99.Name ( argNames, generatorName,
32-
generatorOutputArgName, guardName )
33-
import Copilot.Compile.C99.Settings ( CSettings, cSettingsOutputDirectory,
34-
cSettingsStepFunctionName,
35-
mkDefaultCSettings )
36-
import Copilot.Compile.C99.Type ( transType )
27+
import Copilot.Compile.C99.CodeGen ( mkAccessDecln, mkBuffDecln,
28+
mkExtCpyDecln, mkExtDecln,
29+
mkGenFun, mkGenFunArray,
30+
mkIndexDecln, mkStep,
31+
mkStructDecln, mkStructForwDecln )
32+
import Copilot.Compile.C99.External ( External, gatherExts )
33+
import Copilot.Compile.C99.Name ( argNames, generatorName,
34+
generatorOutputArgName, guardName )
35+
import Copilot.Compile.C99.Settings ( CSettings,
36+
cSettingsOutputDirectory,
37+
cSettingsStepFunctionName,
38+
mkDefaultCSettings )
39+
import Copilot.Compile.C99.Type ( transType )
40+
import Copilot.Compile.C99.Representation ( UniqueTrigger (..),
41+
mkUniqueTriggers )
3742

3843
-- | Compile a specification to a .h and a .c file.
3944
--
@@ -42,12 +47,20 @@ import Copilot.Compile.C99.Type ( transType )
4247
-- The second argument is used as prefix for the .h and .c files generated.
4348
compileWith :: CSettings -> String -> Spec -> IO ()
4449
compileWith cSettings prefix spec
45-
| null (specTriggers spec)
50+
| null triggers
4651
= do hPutStrLn stderr $
4752
"Copilot error: attempt at compiling empty specification.\n"
4853
++ "You must define at least one trigger to generate C monitors."
4954
exitFailure
5055

56+
| incompatibleTriggers triggers
57+
= do hPutStrLn stderr $
58+
"Copilot error: attempt at compiling specification with conflicting "
59+
++ "trigger definitions.\n"
60+
++ "Multiple triggers have the same name, but different argument "
61+
++ "types.\n"
62+
exitFailure
63+
5164
| otherwise
5265
= do let cFile = render $ pretty $ C.translate $ compileC cSettings spec
5366
hFile = render $ pretty $ C.translate $ compileH cSettings spec
@@ -69,6 +82,24 @@ compileWith cSettings prefix spec
6982
writeFile (dir </> prefix ++ ".c") $ cMacros ++ cFile
7083
writeFile (dir </> prefix ++ ".h") hFile
7184
writeFile (dir </> prefix ++ "_types.h") typeDeclnsFile
85+
where
86+
triggers = specTriggers spec
87+
88+
-- Check that two triggers do no conflict, that is: if their names are
89+
-- equal, the types of their arguments should be equal as well.
90+
incompatibleTriggers :: [Trigger] -> Bool
91+
incompatibleTriggers = pairwiseAny conflict
92+
where
93+
conflict :: Trigger -> Trigger -> Bool
94+
conflict t1@(Trigger name1 _ _) t2@(Trigger name2 _ _) =
95+
name1 == name2 && not (compareTrigger t1 t2)
96+
97+
-- True if the function holds for any pair of elements. We assume that
98+
-- the function is commutative.
99+
pairwiseAny :: (a -> a -> Bool) -> [a] -> Bool
100+
pairwiseAny _ [] = False
101+
pairwiseAny _ (_:[]) = False
102+
pairwiseAny f (x:xs) = any (f x) xs || pairwiseAny f xs
72103

73104
-- | Compile a specification to a .h and a .c file.
74105
--
@@ -90,12 +121,13 @@ compileC cSettings spec = C.TransUnit declns funs
90121
declns = mkExts exts
91122
++ mkGlobals streams
92123

93-
funs = mkGenFuns streams triggers
94-
++ [mkStep cSettings streams triggers exts]
124+
funs = mkGenFuns streams uniqueTriggers
125+
++ [mkStep cSettings streams uniqueTriggers exts]
95126

96-
streams = specStreams spec
97-
triggers = specTriggers spec
98-
exts = gatherExts streams triggers
127+
streams = specStreams spec
128+
triggers = specTriggers spec
129+
uniqueTriggers = mkUniqueTriggers triggers
130+
exts = gatherExts streams triggers
99131

100132
-- Make declarations for copies of external variables.
101133
mkExts :: [External] -> [C.Decln]
@@ -110,7 +142,7 @@ compileC cSettings spec = C.TransUnit declns funs
110142
indexDecln (Stream sId _ _ _ ) = mkIndexDecln sId
111143

112144
-- Make generator functions, including trigger arguments.
113-
mkGenFuns :: [Stream] -> [Trigger] -> [C.FunDef]
145+
mkGenFuns :: [Stream] -> [UniqueTrigger] -> [C.FunDef]
114146
mkGenFuns streamList triggerList = map accessDecln streamList
115147
++ map streamGen streamList
116148
++ concatMap triggerGen triggerList
@@ -122,11 +154,11 @@ compileC cSettings spec = C.TransUnit declns funs
122154
streamGen (Stream sId _ expr ty) =
123155
exprGen (generatorName sId) (generatorOutputArgName sId) expr ty
124156

125-
triggerGen :: Trigger -> [C.FunDef]
126-
triggerGen (Trigger name guard args) = guardDef : argDefs
157+
triggerGen :: UniqueTrigger -> [C.FunDef]
158+
triggerGen (UniqueTrigger uniqueName (Trigger _name guard args)) = guardDef : argDefs
127159
where
128-
guardDef = mkGenFun (guardName name) guard Bool
129-
argDefs = zipWith argGen (argNames name) args
160+
guardDef = mkGenFun (guardName uniqueName) guard Bool
161+
argDefs = zipWith argGen (argNames uniqueName) args
130162

131163
argGen :: String -> UExpr -> C.FunDef
132164
argGen argName (UExpr ty expr) =
@@ -155,7 +187,9 @@ compileH cSettings spec = C.TransUnit declns []
155187
exprs = gatherExprs streams triggers
156188
exts = gatherExts streams triggers
157189
streams = specStreams spec
158-
triggers = specTriggers spec
190+
191+
-- Remove duplicates due to multiple guards for the same trigger.
192+
triggers = nubBy compareTrigger (specTriggers spec)
159193

160194
mkStructForwDeclns :: [UExpr] -> [C.Decln]
161195
mkStructForwDeclns es = mapMaybe mkDecln uTypes
@@ -256,3 +290,21 @@ gatherExprs streams triggers = map streamUExpr streams
256290
where
257291
streamUExpr (Stream _ _ expr ty) = UExpr ty expr
258292
triggerUExpr (Trigger _ guard args) = UExpr Bool guard : args
293+
294+
-- | We consider triggers to be equal, if their names match and the number and
295+
-- types of arguments.
296+
compareTrigger :: Trigger -> Trigger -> Bool
297+
compareTrigger (Trigger name1 _ args1) (Trigger name2 _ args2)
298+
= name1 == name2 && compareArguments args1 args2
299+
300+
where
301+
compareArguments :: [UExpr] -> [UExpr] -> Bool
302+
compareArguments [] [] = True
303+
compareArguments [] _ = False
304+
compareArguments _ [] = False
305+
compareArguments (x:xs) (y:ys) = compareUExpr x y && compareArguments xs ys
306+
307+
compareUExpr :: UExpr -> UExpr -> Bool
308+
compareUExpr (UExpr ty1 _) (UExpr ty2 _)
309+
| Just Refl <- testEquality ty1 ty2 = True
310+
| otherwise = False

‎copilot-c99/src/Copilot/Compile/C99/Representation.hs‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
-- | C99 backend specific versions of selected `Copilot.Core` datatypes.
2+
module Copilot.Compile.C99.Representation
3+
( UniqueTrigger (..)
4+
, UniqueTriggerId
5+
, mkUniqueTriggers
6+
)
7+
where
8+
9+
import Copilot.Core ( Trigger (..) )
10+
11+
-- | Internal unique name for a trigger.
12+
type UniqueTriggerId = String
13+
14+
-- | A `Copilot.Core.Trigger` with an unique name.
15+
data UniqueTrigger = UniqueTrigger UniqueTriggerId Trigger
16+
17+
-- | Given a list of triggers, make their names unique.
18+
mkUniqueTriggers :: [Trigger] -> [UniqueTrigger]
19+
mkUniqueTriggers ts = zipWith mkUnique ts [0..]
20+
where
21+
mkUnique t@(Trigger name _ _) n = UniqueTrigger (name ++ "_" ++ show n) t

0 commit comments

Comments
 (0)