From ef329e3ed04d4b49ea68c894e46f651c1d1c8607 Mon Sep 17 00:00:00 2001 From: Adam Sampson Date: Wed, 26 Mar 2008 14:20:35 +0000 Subject: [PATCH] Check SpecTypes. --- common/Types.hs | 7 +- frontends/OccamTypes.hs | 189 ++++++++++++++++++++++++++---------- frontends/OccamTypesTest.hs | 125 +++++++++++++++++++++++- 3 files changed, 266 insertions(+), 55 deletions(-) diff --git a/common/Types.hs b/common/Types.hs index 65ca201..4791b22 100644 --- a/common/Types.hs +++ b/common/Types.hs @@ -20,7 +20,7 @@ with this program. If not, see . module Types ( specTypeOfName, typeOfSpec, abbrevModeOfName, typeOfName, typeOfExpression, typeOfVariable, underlyingType, stripArrayType, abbrevModeOfVariable, abbrevModeOfSpec - , isRealType, isIntegerType, isNumericType, isCaseableType, isScalarType, isCommunicableType, isSequenceType + , isRealType, isIntegerType, isNumericType, isCaseableType, isScalarType, isDataType, isCommunicableType, isSequenceType , resolveUserType, isSafeConversion, isPreciseConversion, isImplicitConversionRain , returnTypesOfFunction , BytesInResult(..), bytesInType, countReplicator, countStructured, computeStructured @@ -504,6 +504,11 @@ isScalarType :: A.Type -> Bool isScalarType A.Bool = True isScalarType t = isIntegerType t || isRealType t +-- | Types that can be used to define 'DataType's. +isDataType :: A.Type -> Bool +-- This may change in the future. +isDataType = isCommunicableType + -- | Types that can be communicated across a channel. isCommunicableType :: A.Type -> Bool isCommunicableType (A.Array _ t) = isCommunicableType t diff --git a/frontends/OccamTypes.hs b/frontends/OccamTypes.hs index a9a400e..cf784c9 100644 --- a/frontends/OccamTypes.hs +++ b/frontends/OccamTypes.hs @@ -21,6 +21,7 @@ module OccamTypes (checkTypes) where import Control.Monad.State import Data.Generics +import Data.List import qualified AST as A import CompState @@ -113,17 +114,27 @@ checkCaseable = checkTypeClass isCaseableType "case-selectable" checkScalar :: Meta -> A.Type -> PassM () checkScalar = checkTypeClass isScalarType "scalar" +-- | Check that a type is usable as a 'DataType' +checkDataType :: Meta -> A.Type -> PassM () +checkDataType = checkTypeClass isDataType "data" + -- | Check that a type is communicable. checkCommunicable :: Meta -> A.Type -> PassM () -checkCommunicable = checkTypeClass isCommunicableType "communicable" +checkCommunicable m (A.Counted ct rawAT) + = do checkInteger m ct + at <- underlyingType m rawAT + case at of + A.Array (A.UnknownDimension:ds) t -> + do checkCommunicable m t + mapM_ (checkFullDimension m) ds + _ -> dieP m "Expected array type with unknown first dimension" +checkCommunicable m t = checkTypeClass isCommunicableType "communicable" m t -- | Check that a type is a sequence. checkSequence :: Meta -> A.Type -> PassM () checkSequence = checkTypeClass isSequenceType "array or list" -- | Check that a type is an array. --- (This also gets used elsewhere where we *know* the argument isn't an array, --- so that we get a consistent error message.) checkArray :: Meta -> A.Type -> PassM () checkArray m rawT = do t <- underlyingType m rawT @@ -131,8 +142,13 @@ checkArray m rawT A.Array _ _ -> ok _ -> diePC m $ formatCode "Expected array type; found %" t +-- | Check that a dimension isn't unknown. +checkFullDimension :: Meta -> A.Dimension -> PassM () +checkFullDimension m A.UnknownDimension + = dieP m $ "Type contains unknown dimensions" +checkFullDimension _ _ = ok + -- | Check that a type is a list. --- Return the element type of the list. checkList :: Meta -> A.Type -> PassM () checkList m rawT = do t <- underlyingType m rawT @@ -152,10 +168,6 @@ checkExpressionInt e = checkExpressionType A.Int e checkExpressionBool :: A.Expression -> PassM () checkExpressionBool e = checkExpressionType A.Bool e --- | Check the type of a variable. -checkVariableType :: Meta -> A.Type -> A.Variable -> PassM () -checkVariableType m et v = typeOfVariable v >>= checkType m et - --}}} --{{{ more complex checks @@ -342,7 +354,7 @@ checkAllocMobile m rawT me case t of A.Mobile innerT -> do case innerT of - A.Array ds _ -> sequence_ $ map checkFullDimension ds + A.Array ds _ -> mapM_ (checkFullDimension m) ds _ -> ok case me of Just e -> @@ -350,11 +362,6 @@ checkAllocMobile m rawT me checkType (findMeta e) innerT et Nothing -> ok _ -> diePC m $ formatCode "Expected mobile type in allocation; found %" t - where - checkFullDimension :: A.Dimension -> PassM () - checkFullDimension A.UnknownDimension - = dieP m $ "Type in allocation contains unknown dimensions" - checkFullDimension _ = ok -- | Check that a variable is writable. checkWritable :: A.Variable -> PassM () @@ -465,6 +472,39 @@ checkExpressionList ets el checkType (findMeta e) et rt | (e, et) <- zip es ets] +-- | Check a set of names are distinct. +checkNamesDistinct :: Meta -> [A.Name] -> PassM () +checkNamesDistinct m ns + = when (dupes /= []) $ + diePC m $ formatCode "List contains duplicate names: %" dupes + where + dupes :: [A.Name] + dupes = nub (ns \\ nub ns) + +-- | Check a 'Replicator'. +checkReplicator :: A.Replicator -> PassM () +checkReplicator (A.For _ _ start count) + = do checkExpressionInt start + checkExpressionInt count +checkReplicator (A.ForEach _ _ e) + = do t <- typeOfExpression e + checkSequence (findMeta e) t + +-- | Check a 'Structured', applying the given check to each item found inside +-- it. This assumes that processes and specifications will be checked +-- elsewhere. +checkStructured :: Data t => (t -> PassM ()) -> A.Structured t -> PassM () +checkStructured doInner (A.Rep _ rep s) + = checkReplicator rep >> checkStructured doInner s +checkStructured doInner (A.Spec _ spec s) + = checkStructured doInner s +checkStructured doInner (A.ProcThen _ p s) + = checkStructured doInner s +checkStructured doInner (A.Only _ i) + = doInner i +checkStructured doInner (A.Several _ ss) + = mapM_ (checkStructured doInner) ss + --}}} -- | Check the AST for type consistency. @@ -472,20 +512,11 @@ checkExpressionList ets el -- inside the AST, but it doesn't really make sense to split it up. checkTypes :: Data t => t -> PassM t checkTypes t = - checkSpecTypes t >>= - checkVariables >>= + checkVariables t >>= checkExpressions >>= + checkSpecTypes >>= 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 @@ -562,6 +593,82 @@ checkExpressions = checkDepthM doExpression sequence_ $ map (doArrayElem m t') aes doArrayElem _ t (A.ArrayElemExpr e) = checkExpressionType t e +--}}} +--{{{ checkSpecTypes + +checkSpecTypes :: Data t => t -> PassM t +checkSpecTypes = checkDepthM doSpecType + where + doSpecType :: A.SpecType -> PassM () + doSpecType (A.Place _ e) = checkExpressionInt e + doSpecType (A.Is m am t v) + = do tv <- typeOfVariable v + checkType (findMeta v) t tv + when (am /= A.Abbrev) $ unexpectedAM m + amv <- abbrevModeOfVariable v + checkAbbrev m amv am + doSpecType (A.IsExpr m am t e) + = do te <- typeOfExpression e + checkType (findMeta e) t te + when (am /= A.ValAbbrev) $ unexpectedAM m + checkAbbrev m A.ValAbbrev am + doSpecType (A.IsChannelArray m rawT cs) + = do t <- underlyingType m rawT + case t of + A.Array [d] et@(A.Chan _ _ _) -> + do sequence_ [do rt <- typeOfVariable c + checkType (findMeta c) et rt + am <- abbrevModeOfVariable c + checkAbbrev m am A.Abbrev + | c <- cs] + case d of + A.UnknownDimension -> ok + A.Dimension e -> + do v <- evalIntExpression e + when (v /= length cs) $ + dieP m $ "Wrong number of elements in channel array abbreviation: found " ++ (show $ length cs) ++ ", expected " ++ show v + _ -> dieP m "Expected 1D channel array type" + doSpecType (A.DataType m rawT) + = do t <- underlyingType m rawT + checkDataType m t + doSpecType (A.RecordType m _ nts) + = do sequence_ [checkDataType (findMeta n) t + | (n, t) <- nts] + checkNamesDistinct m (map fst nts) + doSpecType (A.Protocol m ts) + = do when (length ts == 0) $ + dieP m "A protocol cannot be empty" + mapM_ (checkCommunicable m) ts + doSpecType (A.ProtocolCase m ntss) + = do sequence_ [mapM_ (checkCommunicable (findMeta n)) ts + | (n, ts) <- ntss] + checkNamesDistinct m (map fst ntss) + doSpecType (A.Proc m _ fs _) + = sequence_ [when (am == A.Original) $ unexpectedAM m + | A.Formal am _ n <- fs] + doSpecType (A.Function m _ rs fs body) + = do when (length rs == 0) $ + dieP m "A function must have at least one return type" + sequence_ [do when (am /= A.ValAbbrev) $ + diePC (findMeta n) $ formatCode "Argument % is not a value abbreviation" n + checkDataType (findMeta n) t + | A.Formal am t n <- fs] + -- FIXME: Run this test again after free name removal + doFunctionBody rs body + where + doFunctionBody :: [A.Type] + -> Either (A.Structured A.ExpressionList) A.Process + -> PassM () + doFunctionBody rs (Left s) = checkStructured (checkExpressionList rs) s + -- FIXME: Need to know the name of the function to do this + doFunctionBody rs (Right p) = dieP m "Cannot check function process body" + -- FIXME: Retypes/RetypesExpr is checked elsewhere + doSpecType _ = ok + + unexpectedAM :: Meta -> PassM () + unexpectedAM m = dieP m "Unexpected abbreviation mode" + + --}}} --{{{ checkProcesses @@ -584,16 +691,16 @@ checkProcesses = checkDepthM doProcess checkWritable v doProcess (A.Skip _) = ok doProcess (A.Stop _) = ok - doProcess (A.Seq _ s) = doStructured (\p -> ok) s - doProcess (A.If _ s) = doStructured doChoice s + doProcess (A.Seq _ s) = checkStructured (\p -> ok) s + doProcess (A.If _ s) = checkStructured doChoice s doProcess (A.Case _ e s) = do t <- typeOfExpression e checkCaseable (findMeta e) t - doStructured (doOption t) s + checkStructured (doOption t) s doProcess (A.While _ e _) = checkExpressionBool e - doProcess (A.Par _ _ s) = doStructured (\p -> ok) s + doProcess (A.Par _ _ s) = checkStructured (\p -> ok) s doProcess (A.Processor _ e _) = checkExpressionInt e - doProcess (A.Alt _ _ s) = doStructured doAlternative s + doProcess (A.Alt _ _ s) = checkStructured doAlternative s doProcess (A.ProcCall m n as) = do st <- specTypeOfName n case st of @@ -628,7 +735,7 @@ checkProcesses = checkDepthM doProcess checkProtocol m t Nothing iis doInputItem doInput c (A.InputCase _ s) = do t <- checkChannel A.DirInput c - doStructured (doVariant t) s + checkStructured (doVariant t) s where doVariant :: A.Type -> A.Variant -> PassM () doVariant t (A.Variant m tag iis _) @@ -689,25 +796,5 @@ checkProcesses = checkDepthM doProcess = do t <- typeOfExpression e checkType (findMeta e) wantT t - doReplicator :: A.Replicator -> PassM () - doReplicator (A.For _ _ start count) - = do checkExpressionInt start - checkExpressionInt count - doReplicator (A.ForEach _ _ e) - = do t <- typeOfExpression e - checkSequence (findMeta e) t - - 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 b889ad1..c25c344 100644 --- a/frontends/OccamTypesTest.hs +++ b/frontends/OccamTypesTest.hs @@ -84,6 +84,7 @@ 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 @@ -205,8 +206,10 @@ 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] @@ -369,6 +372,105 @@ testOccamTypes = TestList , testFail 1913 $ A.IntrinsicProcCall m "RESCHEDULE" [A.ActualExpression A.Bool boolE] , testFail 1914 $ A.IntrinsicProcCall m "HERRING" [] + + --}}} + --{{{ specifications + + , testOK 2000 $ A.Place m intE + , testFail 2001 $ A.Place m twoIntsE + + , testOK 2010 $ A.Declaration m A.Int + , testOK 2011 $ A.Declaration m twoIntsT + + , testOK 2020 $ A.Is m A.Abbrev A.Int intV + , testFail 2021 $ A.Is m A.ValAbbrev A.Int intV + , testFail 2022 $ A.Is m A.Original A.Int intV + , testFail 2023 $ A.Is m A.Abbrev A.Real32 intV + , testOK 2024 $ A.Is m A.Abbrev chanIntT intC + , testFail 2025 $ A.Is m A.ValAbbrev chanIntT intC + , testOK 2026 $ A.Is m A.Abbrev (A.Timer A.OccamTimer) tim + , testFail 2027 $ A.Is m A.ValAbbrev (A.Timer A.OccamTimer) tim + + , testOK 2030 $ A.IsExpr m A.ValAbbrev A.Int intE + , testFail 2031 $ A.IsExpr m A.Abbrev A.Int intE + , testFail 2032 $ A.IsExpr m A.Original A.Int intE + , testFail 2033 $ A.IsExpr m A.ValAbbrev A.Real32 intE + + , testOK 2040 $ A.IsChannelArray m chansIntT [intC, intC] + , testOK 2041 $ A.IsChannelArray m uchansIntT [intC, intC] + , testOK 2042 $ A.IsChannelArray m uchansIntT [] + , testFail 2043 $ A.IsChannelArray m chansIntT [intC] + , testFail 2044 $ A.IsChannelArray m chansIntT [iirC, intC] + , testFail 2045 $ A.IsChannelArray m chansIntT [intC, intC, intC] + , testFail 2046 $ A.IsChannelArray m chansIntT [intV, intV] + + , testOK 2050 $ A.DataType m A.Int + , testOK 2051 $ A.DataType m twoIntsT + , testOK 2052 $ A.DataType m myTwoIntsT + , testFail 2053 $ A.DataType m chanIntT + , testFail 2054 $ A.DataType m $ A.Timer A.OccamTimer + + , testOK 2060 $ A.RecordType m True [] + , testOK 2061 $ A.RecordType m False [] + , testOK 2062 $ A.RecordType m False [ (simpleName "x", A.Int) + , (simpleName "y", A.Int) + , (simpleName "z", A.Int) + ] + , testFail 2063 $ A.RecordType m False [(simpleName "c", chanIntT)] + , testOK 2064 $ A.RecordType m False [(simpleName "c", A.Mobile A.Int)] + , testFail 2065 $ A.RecordType m False [ (simpleName "x", A.Int) + , (simpleName "x", A.Real32) + ] + + , testOK 2070 $ A.Protocol m [A.Int] + , testOK 2071 $ A.Protocol m [A.Int, A.Real32, twoIntsT] + , testOK 2072 $ A.Protocol m [A.Mobile A.Int] + , testFail 2073 $ A.Protocol m [] + , testFail 2074 $ A.Protocol m [chanIntT] + , testOK 2075 $ A.Protocol m [A.Counted A.Int unknownIntsT] + , testFail 2076 $ A.Protocol m [A.Counted A.Real32 unknownIntsT] + , testFail 2077 $ A.Protocol m [A.Counted A.Int A.Int] + , testFail 2078 $ A.Protocol m [A.Counted A.Int twoIntsT] + + , testOK 2080 $ A.ProtocolCase m [ (simpleName "one", [A.Int]) + , (simpleName "two", [A.Real32]) + , (simpleName "three", []) + ] + , testFail 2081 $ A.ProtocolCase m [ (simpleName "one", [A.Int]) + , (simpleName "one", [A.Real32]) + ] + + , testOK 2090 $ A.Proc m A.PlainSpec [] skip + , testOK 2091 $ A.Proc m A.InlineSpec [] skip + , testOK 2092 $ A.Proc m A.PlainSpec + [ A.Formal A.Abbrev A.Int (simpleName "x") + , A.Formal A.ValAbbrev A.Int (simpleName "y") + , A.Formal A.Abbrev chanIntT (simpleName "c") + ] + skip + , testFail 2093 $ A.Proc m A.PlainSpec + [ A.Formal A.Original A.Int (simpleName "x") + ] + skip + + , testOK 2100 $ A.Function m A.PlainSpec [A.Int] [] returnOne + , testOK 2110 $ A.Function m A.InlineSpec [A.Int] [] returnOne + , testFail 2120 $ A.Function m A.PlainSpec [] [] returnNone + , testOK 2130 $ A.Function m A.PlainSpec [A.Int] + [ A.Formal A.ValAbbrev A.Int (simpleName "x") + , A.Formal A.ValAbbrev A.Bool (simpleName "b") + , A.Formal A.ValAbbrev A.Int (simpleName "q") + ] + returnOne + , testFail 2140 $ A.Function m A.PlainSpec [A.Int] + [A.Formal A.Abbrev A.Int (simpleName "x")] + returnOne + , testFail 2150 $ A.Function m A.PlainSpec [A.Int] + [A.Formal A.ValAbbrev chanIntT (simpleName "c")] + returnOne + , testFail 2160 $ A.Function m A.PlainSpec [A.Int] [] returnNone + , testFail 2170 $ A.Function m A.PlainSpec [A.Int] [] returnTwo + --}}} ] where @@ -384,7 +486,8 @@ testOccamTypes = TestList (OccamTypes.checkTypes orig) startState - --{{{ definitions for tests + --{{{ expression fragments + subex sub = A.SubscriptedExpr m sub twoIntsE intV = variable "varInt" intE = intLiteral 42 @@ -415,6 +518,10 @@ testOccamTypes = TestList coord2E = A.Literal m coord2T coord2 coord3T = A.Record (simpleName "COORD3") coord3 = A.RecordLiteral m [realE, realE, realE] + chanT t = A.Chan A.DirUnknown (A.ChanAttributes False False) t + chanIntT = chanT A.Int + chansIntT = A.Array [dimension 2] $ chanT A.Int + uchansIntT = A.Array [A.UnknownDimension] $ chanT A.Int intC = variable "chanInt" intCE = A.ExprVariable m intC intsC = variable "chansInt" @@ -430,11 +537,15 @@ testOccamTypes = TestList listT = A.List A.Int 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" + + --}}} + --{{{ process fragments + + skip = A.Skip m + sskip = A.Only m skip insim iis = A.InputSimple m iis inputSimple c iis = A.Input m c $ insim iis inputCase c vs = A.Input m c @@ -450,6 +561,14 @@ testOccamTypes = TestList tim = variable "tim" testAlt a = A.Alt m True $ A.Only m a proccall n = A.ProcCall m (simpleName n) + + --}}} + --{{{ specification fragments + + returnNone = Left $ A.Only m $ A.ExpressionList m [] + returnOne = Left $ A.Only m $ A.ExpressionList m [intE] + returnTwo = Left $ A.Only m $ A.ExpressionList m [intE, intE] + --}}} tests :: Test