From b3e3308b3e19452b9ba09ec564c2d7c465044490 Mon Sep 17 00:00:00 2001 From: Adam Sampson Date: Tue, 25 Mar 2008 15:56:03 +0000 Subject: [PATCH] Implement channel IO checks, and refactor OccamTypes (again). --- common/TestUtils.hs | 10 ++ frontends/OccamTypes.hs | 208 ++++++++++++++++++++++++++++++------ frontends/OccamTypesTest.hs | 142 ++++++++++++++++++------ 3 files changed, 293 insertions(+), 67 deletions(-) diff --git a/common/TestUtils.hs b/common/TestUtils.hs index b7c2234..220a828 100644 --- a/common/TestUtils.hs +++ b/common/TestUtils.hs @@ -360,6 +360,16 @@ defineFunction s rs as st = A.Function emptyMeta A.PlainSpec rs fs (Right $ A.Skip emptyMeta) fs = [A.Formal A.ValAbbrev t (simpleName s) | (s, t) <- as] +-- | Define a protocol. +defineProtocol :: String -> [A.Type] -> State CompState () +defineProtocol s ts + = defineThing s A.ProtocolName (A.Protocol emptyMeta ts) A.Original + +-- | Define a variant protocol. +defineProtocolCase :: String -> [(A.Name, [A.Type])] -> State CompState () +defineProtocolCase s ntss + = defineThing s A.ProtocolName (A.ProtocolCase emptyMeta ntss) A.Original + --}}} --{{{ custom assertions diff --git a/frontends/OccamTypes.hs b/frontends/OccamTypes.hs index cf02d45..9a3070e 100644 --- a/frontends/OccamTypes.hs +++ b/frontends/OccamTypes.hs @@ -331,6 +331,76 @@ checkWritable v A.ValAbbrev -> dieP (findMeta v) $ "Expected a writable variable" _ -> ok +-- | Check that is a variable is a channel that can be used in the given +-- direction. +-- If the direction passed is 'DirUnknown', no direction or sharedness checks +-- will be performed. +-- Return the type carried by the channel. +checkChannel :: A.Direction -> A.Variable -> PassM A.Type +checkChannel wantDir c + = do -- Check it's a channel. + t <- typeOfVariable c >>= underlyingType m + case t of + A.Chan dir (A.ChanAttributes ws rs) innerT -> + do -- Check the direction is appropriate + case (wantDir, dir) of + (A.DirUnknown, _) -> ok + (_, A.DirUnknown) -> ok + (a, b) -> when (a /= b) $ + dieP m $ "Channel directions do not match" + + -- Check it's not shared in the direction we're using. + case (ws, rs, wantDir) of + (False, _, A.DirOutput) -> ok + (_, False, A.DirInput) -> ok + (_, _, A.DirUnknown) -> ok + _ -> dieP m $ "Shared channel must be claimed before use" + + return innerT + _ -> diePC m $ formatCode "Expected channel; found %" t + where + m = findMeta c + +-- | Return the list of types carried by a protocol. +-- For a variant protocol, the second argument should be 'Just' the tag. +-- For a non-variant protocol, the second argument should be 'Nothing'. +protocolTypes :: Meta -> A.Type -> Maybe A.Name -> PassM [A.Type] +protocolTypes m t tag + = case t of + -- A user-defined protocol. + A.UserProtocol n -> + do st <- specTypeOfName n + case (st, tag) of + -- A simple protocol. + (A.Protocol _ ts, Nothing) -> return ts + (A.Protocol _ _, Just tagName) -> + diePC m $ formatCode "Tag % specified for non-variant protocol %" tagName n + -- A variant protocol. + (A.ProtocolCase _ ntss, Just tagName) -> + case lookup tagName ntss of + Just ts -> return ts + Nothing -> diePC m $ formatCode "Tag % not found in protocol %; expected one of %" tagName n (map fst ntss) + (A.ProtocolCase _ _, Nothing) -> + diePC m $ formatCode "No tag specified for variant protocol %" n + -- Not actually a protocol. + _ -> diePC m $ formatCode "% is not a protocol" n + -- Not a protocol (e.g. CHAN INT); just return it. + _ -> return [t] + +-- | Check a protocol communication. +-- Figure out the types of the items that should be involved in a protocol +-- communication, and run the supplied check against each item with its type. +checkProtocol :: Meta -> A.Type -> Maybe A.Name + -> [t] -> (A.Type -> t -> PassM ()) -> PassM () +checkProtocol m t tag items doItem + = do its <- protocolTypes m t tag + when (length its /= length items) $ + dieP m $ "Wrong number of items in protocol communication; found " + ++ (show $ length items) ++ ", expected " + ++ (show $ length its) + sequence_ [doItem it item + | (it, item) <- zip its items] + --}}} -- | Check the AST for type consistency. @@ -338,12 +408,21 @@ checkWritable v -- inside the AST, but it doesn't really make sense to split it up. checkTypes :: Data t => t -> PassM t checkTypes t = - checkVariables t >>= + checkSpecTypes t >>= + checkVariables >>= checkExpressions >>= - checkInputItems >>= - checkOutputItems >>= - checkReplicators >>= - checkChoices + checkProcesses + +--{{{ checkSpecTypes + +checkSpecTypes :: Data t => t -> PassM t +checkSpecTypes = checkDepthM doSpecType + where + doSpecType :: A.SpecType -> PassM () + doSpecType _ = ok + +--}}} +--{{{ checkVariables checkVariables :: Data t => t -> PassM t checkVariables = checkDepthM doVariable @@ -364,6 +443,9 @@ checkVariables = checkDepthM doVariable _ -> dieP m $ "Dereference applied to non-mobile variable" doVariable _ = ok +--}}} +--{{{ checkExpressions + checkExpressions :: Data t => t -> PassM t checkExpressions = checkDepthM doExpression where @@ -414,40 +496,88 @@ checkExpressions = checkDepthM doExpression sequence_ $ map (doArrayElem m t') aes doArrayElem _ t (A.ArrayElemExpr e) = checkExpressionType (findMeta e) t e -checkInputItems :: Data t => t -> PassM t -checkInputItems = checkDepthM doInputItem +--}}} +--{{{ checkProcesses + +checkProcesses :: Data t => t -> PassM t +checkProcesses = checkDepthM doProcess where - doInputItem :: A.InputItem -> PassM () - doInputItem (A.InCounted m cv av) + doProcess :: A.Process -> PassM () + -- Assign + doProcess (A.Input _ v im) = doInput v im + doProcess (A.Output m v ois) = doOutput m v ois + doProcess (A.OutputCase m v tag ois) = doOutputCase m v tag ois + -- GetTime + -- Wait + -- ClearMobile + -- Skip + -- Stop + doProcess (A.Seq _ s) = doStructured (\p -> ok) s + doProcess (A.If _ s) = doStructured doChoice s + -- Case + -- While + -- Par + -- Processor + -- Alt + -- ProcCall + -- IntrinsicProcCall + doProcess _ = ok + + doChoice :: A.Choice -> PassM () + doChoice (A.Choice _ e _) = checkExpressionBool (findMeta e) e + + doInput :: A.Variable -> A.InputMode -> PassM () + doInput c (A.InputSimple m iis) + = do t <- checkChannel A.DirInput c + checkProtocol m t Nothing iis doInputItem + doInput c (A.InputCase _ s) + = do t <- checkChannel A.DirInput c + doStructured (doVariant t) s + where + doVariant :: A.Type -> A.Variant -> PassM () + doVariant t (A.Variant m tag iis _) + = checkProtocol m t (Just tag) iis doInputItem + -- InputTimerRead + -- InputTimerAfter + doInput _ _ = ok + + doInputItem :: A.Type -> A.InputItem -> PassM () + doInputItem (A.Counted wantCT wantAT) (A.InCounted m cv av) = do ct <- typeOfVariable cv - checkInteger (findMeta cv) ct + checkType (findMeta cv) wantCT ct checkWritable cv at <- typeOfVariable av - checkArray (findMeta av) at - checkCommunicable (findMeta av) at + checkType (findMeta cv) wantAT at checkWritable av - doInputItem (A.InVariable _ v) + doInputItem t@(A.Counted _ _) (A.InVariable m v) + = diePC m $ formatCode "Expected counted item of type %; found %" t v + doInputItem wantT (A.InVariable _ v) = do t <- typeOfVariable v - checkCommunicable (findMeta v) t + checkType (findMeta v) wantT t checkWritable v -checkOutputItems :: Data t => t -> PassM t -checkOutputItems = checkDepthM doOutputItem - where - doOutputItem :: A.OutputItem -> PassM () - doOutputItem (A.OutCounted m ce ae) - = do ct <- typeOfExpression ce - checkInteger (findMeta ce) ct - at <- typeOfExpression ae - checkArray (findMeta ae) at - checkCommunicable (findMeta ae) at - doOutputItem (A.OutExpression _ e) - = do t <- typeOfExpression e - checkCommunicable (findMeta e) t + doOutput :: Meta -> A.Variable -> [A.OutputItem] -> PassM () + doOutput m c ois + = do t <- checkChannel A.DirOutput c + checkProtocol m t Nothing ois doOutputItem + + doOutputCase :: Meta -> A.Variable -> A.Name -> [A.OutputItem] -> PassM () + doOutputCase m c tag ois + = do t <- checkChannel A.DirOutput c + checkProtocol m t (Just tag) ois doOutputItem + + doOutputItem :: A.Type -> A.OutputItem -> PassM () + doOutputItem (A.Counted wantCT wantAT) (A.OutCounted m ce ae) + = do ct <- typeOfExpression ce + checkType (findMeta ce) wantCT ct + at <- typeOfExpression ae + checkType (findMeta ae) wantAT at + doOutputItem t@(A.Counted _ _) (A.OutExpression m e) + = diePC m $ formatCode "Expected counted item of type %; found %" t e + doOutputItem wantT (A.OutExpression _ e) + = do t <- typeOfExpression e + checkType (findMeta e) wantT t -checkReplicators :: Data t => t -> PassM t -checkReplicators = checkDepthM doReplicator - where doReplicator :: A.Replicator -> PassM () doReplicator (A.For _ _ start count) = do checkExpressionInt (findMeta start) start @@ -456,9 +586,17 @@ checkReplicators = checkDepthM doReplicator = do t <- typeOfExpression e checkSequence (findMeta e) t -checkChoices :: Data t => t -> PassM t -checkChoices = checkDepthM doChoice - where - doChoice :: A.Choice -> PassM () - doChoice (A.Choice _ e _) = checkExpressionBool (findMeta e) e + doStructured :: Data t => (t -> PassM ()) -> A.Structured t -> PassM () + doStructured doInner (A.Rep _ rep s) + = doReplicator rep >> doStructured doInner s + doStructured doInner (A.Spec _ spec s) + = doStructured doInner s + doStructured doInner (A.ProcThen _ p s) + = doStructured doInner s + doStructured doInner (A.Only _ i) + = doInner i + doStructured doInner (A.Several _ ss) + = mapM_ (doStructured doInner) ss + +--}}} diff --git a/frontends/OccamTypesTest.hs b/frontends/OccamTypesTest.hs index 7b7ec1f..5181343 100644 --- a/frontends/OccamTypesTest.hs +++ b/frontends/OccamTypesTest.hs @@ -57,16 +57,29 @@ startState defineFunction "function2" [A.Int] [("x", A.Int), ("y", A.Int)] defineFunction "function22" [A.Int, A.Int] [("x", A.Int), ("y", A.Int)] + defineProtocol "countedInts" $ [A.Counted A.Int intsT] + defineChannel "chanCountedInts" countedIntsT + defineProtocol "iir" $ [A.Int, A.Int, A.Real32] + defineChannel "chanIIR" iirT + defineProtocolCase "caseProto" $ [ (simpleName "one", [A.Int]) + , (simpleName "two", [A.Real32]) + , (simpleName "three", []) + ] + defineChannel "chanCaseProto" caseProtoT where - ca = A.ChanAttributes False False intsT = A.Array [A.UnknownDimension] A.Int arrayLit = A.ArrayLiteral m [] - chanIntT = A.Chan A.DirUnknown ca A.Int + chanT t = A.Chan A.DirUnknown (A.ChanAttributes False False) t + chanIntT = chanT A.Int + countedIntsT = chanT $ A.UserProtocol (simpleName "countedInts") + iirT = chanT $ A.UserProtocol (simpleName "iir") + caseProtoT = chanT $ A.UserProtocol (simpleName "caseProto") -- | Test the typechecker. testOccamTypes :: Test testOccamTypes = TestList [ + --{{{ expressions -- Subscript expressions testOK 0 $ subex $ A.Subscript m A.NoCheck intE , testFail 1 $ subex $ A.Subscript m A.NoCheck byteE @@ -103,10 +116,10 @@ testOccamTypes = TestList -- Variables , testOK 50 $ intV , testOK 51 $ bytesV - , testOK 52 $ A.DirectedVariable m A.DirInput chanIntV + , testOK 52 $ A.DirectedVariable m A.DirInput intC , testFail 53 $ A.DirectedVariable m A.DirInput intV , testOK 54 $ A.DerefVariable m mobileIntV - , testFail 55 $ A.DerefVariable m chanIntV + , testFail 55 $ A.DerefVariable m intC -- Operators in expressions , testOK 100 $ A.Monadic m A.MonadicSubtr intE @@ -188,36 +201,85 @@ testOccamTypes = TestList , testOK 254 $ A.AllocMobile m (A.Mobile twoIntsT) (Just twoIntsE) , testFail 255 $ A.AllocMobile m (A.Mobile unknownIntsT) (Just twoIntsE) , testFail 256 $ A.AllocMobile m (A.Mobile unknownIntsT) Nothing + --}}} + --{{{ processes + -- Inputs + , testOK 1000 $ inputSimple countedIntsC [A.InCounted m intV intsV] + , testFail 1001 $ inputSimple countedIntsC [A.InCounted m realV intsV] + , testFail 1002 $ inputSimple countedIntsC [A.InCounted m intV intV] + , testFail 1003 $ inputSimple countedIntsC [A.InCounted m constIntV intsV] + , testFail 1004 $ inputSimple countedIntsC [A.InCounted m intV constIntsV] + , testFail 1005 $ inputSimple countedIntsC [A.InCounted m intV intsC] + , testOK 1010 $ inputSimple intC [inv intV] + , testFail 1011 $ inputSimple intC [inv constIntV] + , testFail 1012 $ inputSimple intC [inv intC] + , testFail 1013 $ inputSimple intV [inv intV] + , testFail 1014 $ inputSimple intV [] + , testFail 1015 $ inputSimple intV [inv intV, inv intV] + , testOK 1020 $ inputSimple iirC [inv intV, inv intV, inv realV] + , testFail 1021 $ inputSimple iirC [inv intV, inv realV, inv intV] + , testFail 1022 $ inputSimple iirC [inv realV, inv intV, inv intV] + , testFail 1023 $ inputSimple iirC [inv intV, inv intV] + , testFail 1024 $ inputSimple iirC [inv intV, inv intV, inv realV, inv intV] + , testOK 1030 $ inputCase caseC [ vari "one" [inv intV] + , vari "two" [inv realV] + , vari "three" [] + ] + , testFail 1031 $ inputCase caseC [ vari "one" [inv realV] + , vari "two" [inv realV] + , vari "three" [] + ] + , testFail 1032 $ inputCase caseC [ vari "one" [inv intV] + , vari "two" [inv intV] + , vari "three" [] + ] + , testFail 1033 $ inputCase caseC [ vari "one" [inv intV] + , vari "herring" [inv realV] + , vari "three" [] + ] + , testFail 1034 $ inputCase caseC [ vari "one" [inv intV, inv realV] + , vari "two" [inv realV] + , vari "three" [] + ] + , testFail 1035 $ inputCase caseC [ vari "one" [] + , vari "two" [] + , vari "three" [] + ] - -- Input items - , testOK 300 $ A.InCounted m intV intsV - , testFail 301 $ A.InCounted m realV intsV - , testFail 302 $ A.InCounted m intV intV - , testFail 303 $ A.InCounted m constIntV intsV - , testFail 304 $ A.InCounted m intV constIntsV - , testFail 305 $ A.InCounted m intV chansIntV - , testOK 306 $ A.InVariable m intV - , testFail 307 $ A.InVariable m constIntV - , testFail 308 $ A.InVariable m chanIntV - - -- Output items - , testOK 310 $ A.OutCounted m intE twoIntsE - , testFail 311 $ A.OutCounted m realE twoIntsE - , testFail 312 $ A.OutCounted m intE intE - , testOK 313 $ A.OutExpression m intE - , testFail 313 $ A.OutExpression m chanIntE + -- Outputs + , testOK 1100 $ outputSimple countedIntsC [A.OutCounted m intE twoIntsE] + , testFail 1101 $ outputSimple countedIntsC [A.OutCounted m realE twoIntsE] + , testFail 1102 $ outputSimple countedIntsC [A.OutCounted m intE intE] + , testOK 1110 $ outputSimple intC [oute intE] + , testFail 1111 $ outputSimple intC [oute intCE] + , testFail 1112 $ outputSimple intV [oute intE] + , testOK 1120 $ outputSimple iirC [oute intE, oute intE, oute realE] + , testFail 1121 $ outputSimple iirC [oute intE, oute realE, oute intE] + , testFail 1122 $ outputSimple iirC [oute realE, oute intE, oute intE] + , testFail 1123 $ outputSimple iirC [oute intE, oute intE] + , testFail 1124 $ outputSimple iirC [oute intE, oute intE, oute realE, + oute intE] + , testOK 1130 $ outputCase caseC "one" [oute intE] + , testOK 1131 $ outputCase caseC "two" [oute realE] + , testOK 1132 $ outputCase caseC "three" [] + , testFail 1133 $ outputCase caseC "three" [oute intE] + , testFail 1134 $ outputCase caseC "two" [oute realE, oute intE] + , testFail 1135 $ outputCase caseC "two" [] + , testFail 1136 $ outputCase caseC "two" [oute intE] + , testFail 1137 $ outputCase caseC "herring" [oute intE] -- Replicators - , testOK 320 $ A.For m i intE intE - , testFail 321 $ A.For m i realE intE - , testFail 322 $ A.For m i intE realE - , testOK 323 $ A.ForEach m i twoIntsE - , testOK 324 $ A.ForEach m i listE - , testFail 324 $ A.ForEach m i intE + , testOK 1200 $ testRep $ A.For m i intE intE + , testFail 1201 $ testRep $ A.For m i realE intE + , testFail 1202 $ testRep $ A.For m i intE realE + , testOK 1203 $ testRep $ A.ForEach m i twoIntsE + , testOK 1204 $ testRep $ A.ForEach m i listE + , testFail 1205 $ testRep $ A.ForEach m i intE -- Choices - , testOK 330 $ A.Choice m boolE skip - , testFail 331 $ A.Choice m intE skip + , testOK 1300 $ testChoice $ A.Choice m boolE skip + , testFail 1301 $ testChoice $ A.Choice m intE skip + --}}} ] where testOK :: (Show a, Data a) => Int -> a -> Test @@ -232,6 +294,7 @@ testOccamTypes = TestList (OccamTypes.checkTypes orig) startState + --{{{ definitions for tests subex sub = A.SubscriptedExpr m sub twoIntsE intV = variable "varInt" intE = intLiteral 42 @@ -262,9 +325,9 @@ testOccamTypes = TestList coord2E = A.Literal m coord2T coord2 coord3T = A.Record (simpleName "COORD3") coord3 = A.RecordLiteral m [realE, realE, realE] - chanIntV = variable "chanInt" - chanIntE = A.ExprVariable m chanIntV - chansIntV = variable "chanInt" + intC = variable "chanInt" + intCE = A.ExprVariable m intC + intsC = variable "chansInt" mobileIntV = variable "mobileInt" sub0 = A.Subscript m A.NoCheck (intLiteral 0) sub0E = A.SubscriptedExpr m sub0 @@ -278,6 +341,21 @@ testOccamTypes = TestList listE = A.Literal m listT (A.ListLiteral m [intE, intE, intE]) i = simpleName "i" skip = A.Skip m + sskip = A.Only m skip + countedIntsC = variable "chanCountedInts" + iirC = variable "chanIIR" + caseC = variable "chanCaseProto" + inputSimple c iis = A.Input m c $ A.InputSimple m iis + inputCase c vs = A.Input m c + $ A.InputCase m (A.Several m (map (A.Only m) vs)) + vari tag iis = A.Variant m (simpleName tag) iis skip + outputSimple c ois = A.Output m c ois + outputCase c tag ois = A.OutputCase m c (simpleName tag) ois + testRep r = A.Seq m (A.Rep m r sskip) + testChoice c = A.If m $ A.Only m c + inv = A.InVariable m + oute = A.OutExpression m + --}}} tests :: Test tests = TestLabel "OccamTypesTest" $ TestList