From d5766c5fe54e68a8aa33a9a2083a0b5f9277166a Mon Sep 17 00:00:00 2001 From: Adam Sampson Date: Wed, 16 May 2007 19:34:10 +0000 Subject: [PATCH] Implement arrays inside records. ... which required a bunch of stuff: - Record handling in the literal evaluator (to solve a nasty problem with record literals documented in the code). - Splitting abbrevModeOfVariable into two functions which do the two (different) things it was previously used for. - Clean up how arrays are handled in GenerateC. - Fix the pullup rules for record literals containing arrays. --- fco2/EvalConstants.hs | 4 + fco2/EvalLiterals.hs | 5 + fco2/GenerateC.hs | 205 +++++++++++++++++----- fco2/SimplifyExprs.hs | 23 ++- fco2/TODO | 16 ++ fco2/Types.hs | 10 +- fco2/Utils.hs | 6 + fco2/testcases/nonconst-array-literal.occ | 16 ++ fco2/testcases/record-literals.occ | 40 +++++ 9 files changed, 269 insertions(+), 56 deletions(-) create mode 100644 fco2/testcases/nonconst-array-literal.occ diff --git a/fco2/EvalConstants.hs b/fco2/EvalConstants.hs index bfa0ce7..6748ff6 100644 --- a/fco2/EvalConstants.hs +++ b/fco2/EvalConstants.hs @@ -63,6 +63,8 @@ evalLiteral (A.Literal _ _ (A.ArrayLiteral _ [])) = throwError "empty array" evalLiteral (A.Literal _ _ (A.ArrayLiteral _ aes)) = liftM OccArray (mapM evalLiteralArray aes) +evalLiteral (A.Literal _ (A.Record n) (A.RecordLiteral _ es)) + = liftM (OccRecord n) (mapM evalExpression es) evalLiteral l = evalSimpleLiteral l evalLiteralArray :: A.ArrayElem -> EvalM OccValue @@ -222,6 +224,8 @@ renderLiteral m (OccArray vs) where t = makeArrayType (A.Dimension $ length vs) (head ts) (ts, aes) = unzip $ map (renderLiteralArray m) vs +renderLiteral m (OccRecord n vs) + = (A.Record n, A.RecordLiteral m (map (snd . renderValue m) vs)) renderChar :: Char -> String renderChar '\'' = "*'" diff --git a/fco2/EvalLiterals.hs b/fco2/EvalLiterals.hs index 92d3c5a..7a323b8 100644 --- a/fco2/EvalLiterals.hs +++ b/fco2/EvalLiterals.hs @@ -29,13 +29,18 @@ data OccValue = | OccInt16 Int16 | OccInt32 Int32 | OccInt64 Int64 + -- FIXME This should include the type of the elements, so we can handle + -- empty arrays. | OccArray [OccValue] + | OccRecord A.Name [OccValue] deriving (Show, Eq, Typeable, Data) -- | Is an expression a constant literal? isConstant :: A.Expression -> Bool isConstant (A.Literal _ _ (A.ArrayLiteral _ aes)) = and $ map isConstantArray aes +isConstant (A.Literal _ _ (A.RecordLiteral _ es)) + = and $ map isConstant es isConstant (A.Literal _ _ _) = True isConstant (A.True _) = True isConstant (A.False _) = True diff --git a/fco2/GenerateC.hs b/fco2/GenerateC.hs index e4bdd30..38c597f 100644 --- a/fco2/GenerateC.hs +++ b/fco2/GenerateC.hs @@ -19,6 +19,7 @@ import Pass import Errors import TLP import Types +import Utils --{{{ monad definition type CGen = WriterT [String] PassM @@ -55,11 +56,21 @@ genTopLevel p missing :: String -> CGen () missing s = tell ["\n#error Unimplemented: ", s, "\n"] +--{{{ simple punctuation genComma :: CGen () genComma = tell [", "] +genLeftB :: CGen () +genLeftB = tell ["{ "] + +genRightB :: CGen () +genRightB = tell [" }"] +--}}} + +-- | A function that applies a subscript to a variable. type SubscripterFunction = A.Variable -> A.Variable +-- | Map an operation over every item of an occam array. overArray :: Meta -> A.Variable -> (SubscripterFunction -> Maybe (CGen ())) -> CGen () overArray m var func = do A.Array ds _ <- typeOfVariable var @@ -93,6 +104,7 @@ genStructured s def = def s data InputType = ITTimerRead | ITTimerAfter | ITOther +-- | Given an input mode, figure out what sort of input it's actually doing. inputType :: A.Variable -> A.InputMode -> CGen InputType inputType c im = do t <- typeOfVariable c @@ -105,6 +117,8 @@ inputType c im --}}} --{{{ metadata +-- | Turn a Meta into a string literal that can be passed to a function +-- expecting a const char * argument. genMeta :: Meta -> CGen () genMeta m = tell ["\"", show m, "\""] --}}} @@ -115,6 +129,7 @@ genName n = tell [[if c == '.' then '_' else c | c <- A.nameName n]] --}}} --{{{ types +-- | If a type maps to a simple C type, return Just that; else return Nothing. scalarType :: A.Type -> Maybe String scalarType A.Bool = Just "bool" scalarType A.Byte = Just "uint8_t" @@ -303,13 +318,65 @@ genLiteralRepr (A.IntLiteral m s) = genDecimal s genLiteralRepr (A.HexLiteral m s) = tell ["0x", s] genLiteralRepr (A.ByteLiteral m s) = tell ["'"] >> genByteLiteral s >> tell ["'"] genLiteralRepr (A.ArrayLiteral m aes) - = do tell ["{"] + = do genLeftB genArrayLiteralElems aes - tell ["}"] -genLiteralRepr (A.RecordLiteral m es) - = do tell ["{"] - sequence_ $ intersperse genComma $ map genExpression es - tell ["}"] + genRightB +genLiteralRepr (A.RecordLiteral _ es) + = do genLeftB + sequence_ $ intersperse genComma $ map genUnfoldedExpression es + genRightB + +-- | Generate an expression inside a record literal. +-- +-- This is awkward: the sort of literal that this produces when there's a +-- variable in here cannot always be compiled at the top level of a C99 program +-- -- because in C99, an array subscript is not a constant, even if it's a +-- constant subscript of a constant array. So we need to be sure that when we +-- use this at the top level, the thing we're unfolding only contains literals. +-- Yuck! +genUnfoldedExpression :: A.Expression -> CGen () +genUnfoldedExpression (A.Literal _ t lr) + = do genLiteralRepr lr + case t of + A.Array ds _ -> + do genComma + genLeftB + genArraySizesLiteral ds + genRightB + _ -> return () +genUnfoldedExpression (A.ExprVariable m var) = genUnfoldedVariable m var +genUnfoldedExpression e = genExpression e + +-- | Generate a variable inside a record literal. +genUnfoldedVariable :: Meta -> A.Variable -> CGen () +genUnfoldedVariable m var + = do t <- typeOfVariable var + case t of + A.Array ds _ -> + do genLeftB + unfoldArray ds var + genRightB + genComma + genLeftB + genArraySizesLiteral ds + genRightB + A.Record _ -> + do genLeftB + fs <- recordFields m t + sequence_ $ intersperse genComma [genUnfoldedVariable m (A.SubscriptedVariable m (A.SubscriptField m n) var) + | (n, t) <- fs] + genRightB + -- We can defeat the usage check here because we know it's safe; *we're* + -- generating the subscripts. + -- FIXME Is that actually true for something like [a[x]]? + _ -> genVariable' False var + where + unfoldArray :: [A.Dimension] -> A.Variable -> CGen () + unfoldArray [] v = genUnfoldedVariable m v + unfoldArray (A.Dimension n:ds) v + = sequence_ $ intersperse genComma $ [unfoldArray ds (A.SubscriptedVariable m (A.Subscript m $ makeConstant m i) v) + | i <- [0..(n - 1)]] + unfoldArray _ _ = dieP m "trying to unfold array with unknown dimension" -- | Generate a decimal literal -- removing leading zeroes to avoid producing -- an octal literal! @@ -325,7 +392,7 @@ genArrayLiteralElems aes where genElem :: A.ArrayElem -> CGen () genElem (A.ArrayElemArray aes) = genArrayLiteralElems aes - genElem (A.ArrayElemExpr e) = genExpression e + genElem (A.ArrayElemExpr e) = genUnfoldedExpression e genByteLiteral :: String -> CGen () genByteLiteral s @@ -399,9 +466,13 @@ genVariable = genVariable' True genVariableUnchecked :: A.Variable -> CGen () genVariableUnchecked = genVariable' False +-- FIXME This needs to detect when we've "gone through" a record and revert to +-- the Original prefixing behaviour. (Can do the same for arrays?) +-- Best way to do this is probably to make inner return a reference and a prefix, +-- so that we can pass prefixes upwards... genVariable' :: Bool -> A.Variable -> CGen () genVariable' checkValid v - = do am <- abbrevModeOfVariable v + = do am <- accessAbbrevMode v t <- typeOfVariable v let isSub = case v of A.Variable _ _ -> False @@ -420,6 +491,19 @@ genVariable' checkValid v inner v when (prefix /= "") $ tell [")"] where + -- | Find the effective abbreviation mode for the variable we're looking at. + -- This differs from abbrevModeOfVariable in that it will return Original + -- for array and record elements (because when we're generating C, we can + -- treat c->x as if it's just x). + accessAbbrevMode :: A.Variable -> CGen A.AbbrevMode + accessAbbrevMode (A.Variable _ n) = abbrevModeOfName n + accessAbbrevMode (A.SubscriptedVariable _ sub v) + = do am <- accessAbbrevMode v + return $ case (am, sub) of + (_, A.Subscript _ _) -> A.Original + (_, A.SubscriptField _ _) -> A.Original + _ -> am + inner :: A.Variable -> CGen () inner (A.Variable _ n) = genName n inner sv@(A.SubscriptedVariable _ (A.Subscript _ _) _) @@ -798,9 +882,6 @@ genRetypeSizes m am destT destN srcT srcV tell ["}\n"] _ -> return () - tell ["const int "] - genName destN - tell ["_sizes[] = { "] let dims = [case d of A.UnknownDimension -> -- Unknown dimension -- insert it. @@ -810,8 +891,7 @@ genRetypeSizes m am destT destN srcT srcV die "genRetypeSizes expecting free dimension" A.Dimension n -> tell [show n] | d <- destDS] - sequence_ $ intersperse genComma dims - tell ["};\n"] + genArraySize False (sequence_ $ intersperse genComma dims) destN -- Not array; just check the size is 1. _ -> @@ -824,18 +904,10 @@ abbrevExpression :: A.AbbrevMode -> A.Type -> A.Expression -> (CGen (), A.Name - abbrevExpression am t@(A.Array _ _) e = case e of A.ExprVariable _ v -> abbrevVariable am t v - A.Literal _ litT r -> (genExpression e, genTypeSize litT) + A.Literal _ (A.Array ds _) r -> (genExpression e, declareArraySizes ds) _ -> bad where bad = (missing "array expression abbreviation", noSize) - - genTypeSize :: A.Type -> (A.Name -> CGen ()) - genTypeSize (A.Array ds _) - = genArraySize False $ sequence_ $ intersperse genComma dims - where dims = [case d of - A.Dimension n -> tell [show n] - _ -> die "unknown dimension in literal array type" - | d <- ds] abbrevExpression am _ e = (genExpression e, noSize) --}}} @@ -853,13 +925,7 @@ declareType :: A.Type -> CGen () declareType (A.Chan _) = tell ["Channel *"] declareType t = genType t -genDimensions :: [A.Dimension] -> CGen () -genDimensions ds - = do tell ["["] - sequence $ intersperse (tell [" * "]) - [case d of A.Dimension n -> tell [show n] | d <- ds] - tell ["]"] - +-- | Generate a declaration of a new variable. genDeclaration :: A.Type -> A.Name -> CGen () genDeclaration (A.Chan _) n = do tell ["Channel "] @@ -869,21 +935,47 @@ genDeclaration (A.Array ds t) n = do declareType t tell [" "] genName n - genDimensions ds + genFlatArraySize ds tell [";\n"] + declareArraySizes ds n genDeclaration t n = do declareType t tell [" "] genName n tell [";\n"] -declareArraySizes :: [A.Dimension] -> CGen () -> CGen () +-- | Generate the size of the C array that an occam array of the given +-- dimensions maps to. +genFlatArraySize :: [A.Dimension] -> CGen () +genFlatArraySize ds + = do tell ["["] + sequence $ intersperse (tell [" * "]) + [case d of A.Dimension n -> tell [show n] | d <- ds] + tell ["]"] + +-- | Generate the size of the _sizes C array for an occam array. +genArraySizesSize :: [A.Dimension] -> CGen () +genArraySizesSize ds + = do tell ["["] + tell [show $ length ds] + tell ["]"] + +-- | Declare an _sizes array for a variable. +declareArraySizes :: [A.Dimension] -> A.Name -> CGen () declareArraySizes ds name - = do tell ["const int "] - name - tell ["_sizes[] = { "] - sequence_ $ intersperse genComma [tell [show n] | A.Dimension n <- ds] - tell [" };\n"] + = genArraySize False (genArraySizesLiteral ds) name + +-- | Generate a C literal to initialise an _sizes array with, where all the +-- dimensions are fixed. +genArraySizesLiteral :: [A.Dimension] -> CGen () +genArraySizesLiteral ds + = sequence_ $ intersperse genComma dims + where + dims :: [CGen ()] + dims = [case d of + A.Dimension n -> tell [show n] + _ -> die "unknown dimension in array type" + | d <- ds] -- | Initialise an item being declared. declareInit :: Meta -> A.Type -> A.Variable -> Maybe (CGen ()) @@ -898,16 +990,29 @@ declareInit m t@(A.Array ds t') var let storeV = A.Variable m store tell ["Channel "] genName store - genDimensions ds + genFlatArraySize ds tell [";\n"] - declareArraySizes ds (genName store) + declareArraySizes ds store return (\sub -> Just $ do genVariable (sub var) tell [" = &"] genVariable (sub storeV) tell [";\n"] - fromJust $ declareInit m t' (sub var)) + doMaybe $ declareInit m t' (sub var)) _ -> return (\sub -> declareInit m t' (sub var)) overArray m var init +declareInit m rt@(A.Record _) var + = Just $ do fs <- recordFields m rt + sequence_ [initField t (A.SubscriptedVariable m (A.SubscriptField m n) var) + | (n, t) <- fs] + where + initField :: A.Type -> A.Variable -> CGen () + -- An array as a record field; we must initialise the sizes. + initField t@(A.Array ds _) v + = do sequence_ [do genVariable v + tell ["_sizes[", show i, "] = ", show n, ";\n"] + | (i, A.Dimension n) <- zip [0..(length ds - 1)] ds] + doMaybe $ declareInit m t v + initField t v = doMaybe $ declareInit m t v declareInit _ _ _ = Nothing -- | Free a declared item that's going out of scope. @@ -932,9 +1037,6 @@ CHAN OF INT c IS d: Channel *c = d; introduceSpec :: A.Specification -> CGen () introduceSpec (A.Specification m n (A.Declaration _ t)) = do genDeclaration t n - case t of - A.Array ds _ -> declareArraySizes ds (genName n) - _ -> return () case declareInit m t (A.Variable m n) of Just p -> p Nothing -> return () @@ -983,16 +1085,24 @@ introduceSpec (A.Specification _ n (A.IsChannelArray _ t cs)) tell ["[] = {"] sequence_ $ intersperse genComma (map genVariable cs) tell ["};\n"] - declareArraySizes [A.Dimension $ length cs] (genName n) + declareArraySizes [A.Dimension $ length cs] n introduceSpec (A.Specification _ _ (A.DataType _ _)) = return () introduceSpec (A.Specification _ n (A.RecordType _ b fs)) = do tell ["typedef struct {\n"] sequence_ [case t of - _ -> - do declareType t + -- Arrays need the corresponding _sizes array. + A.Array ds t' -> + do genType t' tell [" "] genName n + genFlatArraySize ds tell [";\n"] + tell ["int "] + genName n + tell ["_sizes"] + genArraySizesSize ds + tell [";\n"] + _ -> genDeclaration t n | (n, t) <- fs] tell ["} "] when b $ tell ["occam_struct_packed "] @@ -1139,6 +1249,11 @@ genAssign m [v] el doAssign :: A.Type -> A.Variable -> A.Expression -> CGen () doAssign t@(A.Array _ subT) toV (A.ExprVariable m fromV) = overArray m fromV (\sub -> Just $ doAssign subT (sub toV) (A.ExprVariable m (sub fromV))) + doAssign rt@(A.Record _) toV (A.ExprVariable m fromV) + = do fs <- recordFields m rt + sequence_ [let subV v = A.SubscriptedVariable m (A.SubscriptField m n) v + in doAssign t (subV toV) (A.ExprVariable m $ subV fromV) + | (n, t) <- fs] doAssign t v e = case scalarType t of Just _ -> diff --git a/fco2/SimplifyExprs.hs b/fco2/SimplifyExprs.hs index 7bf0757..de329de 100644 --- a/fco2/SimplifyExprs.hs +++ b/fco2/SimplifyExprs.hs @@ -104,7 +104,14 @@ expandArrayLiterals = doGeneric `extM` doArrayElem -- | Find things that need to be moved up to their enclosing Structured, and do -- so. pullUp :: Data t => t -> PassM t -pullUp = doGeneric `extM` doStructured `extM` doProcess `extM` doSpecification `extM` doExpression `extM` doVariable `extM` doExpressionList +pullUp = doGeneric + `extM` doStructured + `extM` doProcess + `extM` doSpecification + `extM` doLiteralRepr + `extM` doExpression + `extM` doVariable + `extM` doExpressionList where doGeneric :: Data t => t -> PassM t doGeneric = makeGeneric pullUp @@ -133,8 +140,7 @@ pullUp = doGeneric `extM` doStructured `extM` doProcess `extM` doSpecification ` popPullContext return p'' - -- | *Don't* pull anything that's already an abbreviation -- but do convert - -- RetypesExpr into Retypes (of a variable). + -- | Filter what can be pulled in Specifications. doSpecification :: A.Specification -> PassM A.Specification -- Iss might be SubscriptedVars -- which is fine; the backend can deal with that. doSpecification (A.Specification m n (A.Is m' am t v)) @@ -144,6 +150,7 @@ pullUp = doGeneric `extM` doStructured `extM` doProcess `extM` doSpecification ` doSpecification (A.Specification m n (A.IsExpr m' am t e)) = do e' <- doExpression' e -- note doExpression' rather than pullUp return $ A.Specification m n (A.IsExpr m' am t e') + -- Convert RetypesExpr into Retypes of a variable. doSpecification (A.Specification m n (A.RetypesExpr m' am toT e)) = do e' <- doExpression e fromT <- typeOfExpression e' @@ -152,6 +159,16 @@ pullUp = doGeneric `extM` doStructured `extM` doProcess `extM` doSpecification ` return $ A.Specification m n (A.Retypes m' am toT (A.Variable m' n')) doSpecification s = doGeneric s + -- | Filter what can be pulled in LiteralReprs. + doLiteralRepr :: A.LiteralRepr -> PassM A.LiteralRepr + -- FIXME: We could do away with ArrayElem and have a rule like the below + -- for nested array literals. + -- Don't pull up array expressions that are fields of record literals. + doLiteralRepr (A.RecordLiteral m es) + = do es' <- mapM doExpression' es -- note doExpression' rather than pullUp + return $ A.RecordLiteral m es' + doLiteralRepr lr = doGeneric lr + -- | Pull array expressions that aren't already non-subscripted variables. doExpression :: A.Expression -> PassM A.Expression doExpression e diff --git a/fco2/TODO b/fco2/TODO index f219387..17c242f 100644 --- a/fco2/TODO +++ b/fco2/TODO @@ -15,6 +15,10 @@ The show instance for types should produce occam-looking types. ParseState should be called something more sensible, since most of it has nothing to do with parsing. +Eventually (not yet), channel formals should take a direction; this should +either be given directly using decorators, or inferred from the code that uses +them. + ## Support code Types needs cleaning up and Haddocking. @@ -77,6 +81,8 @@ Pullups don't work properly for this at the moment, because index changes after the pullup: c ? index; [array FROM index] (Tested in cgtest12.) +The sensible fix would probably be to make input items Structured, so we can +insert extra stuff into them. ## tock_support @@ -84,6 +90,16 @@ No overflow checking is done on most operations. Real-to-integer conversions don't work correctly. +## Usage checker + +Not written yet, obviously... + +Use a separation logic idea -- at any point in the program, we have a set of +resources. When you go parallel, you have to divide up the resources among the +parallel branches -- e.g. splitting a channel into read and write ends, carving +up an array, and so on. The safety check is done by making sure the resources +are actually divided up. + ## Long-term If we have constant folding, we're three-quarters of the way towards having an diff --git a/fco2/Types.hs b/fco2/Types.hs index 449c08c..d37df61 100644 --- a/fco2/Types.hs +++ b/fco2/Types.hs @@ -139,16 +139,10 @@ typeOfVariable (A.Variable m n) = typeOfName n typeOfVariable (A.SubscriptedVariable m s v) = typeOfVariable v >>= subscriptType s +-- | Get the abbreviation mode of a variable. abbrevModeOfVariable :: (PSM m, Die m) => A.Variable -> m A.AbbrevMode abbrevModeOfVariable (A.Variable _ n) = abbrevModeOfName n -abbrevModeOfVariable (A.SubscriptedVariable _ sub v) - = do am <- abbrevModeOfVariable v - return $ case (am, sub) of - (A.ValAbbrev, A.Subscript _ _) -> A.ValAbbrev - (_, A.Subscript _ _) -> A.Original - (A.ValAbbrev, A.SubscriptField _ _) -> A.ValAbbrev - (_, A.SubscriptField _ _) -> A.Original - _ -> am +abbrevModeOfVariable (A.SubscriptedVariable _ sub v) = abbrevModeOfVariable v dyadicIsBoolean :: A.DyadicOp -> Bool dyadicIsBoolean A.Eq = True diff --git a/fco2/Utils.hs b/fco2/Utils.hs index 48a1b74..2bb3ee0 100644 --- a/fco2/Utils.hs +++ b/fco2/Utils.hs @@ -28,3 +28,9 @@ joinPath base new "." -> new dir -> dir ++ new +-- | Given a monadic action wrapped in a Maybe, run it if there's one there; +-- if it's Nothing, then do nothing. +doMaybe :: Monad m => Maybe (m ()) -> m () +doMaybe (Just a) = a +doMaybe Nothing = return () + diff --git a/fco2/testcases/nonconst-array-literal.occ b/fco2/testcases/nonconst-array-literal.occ new file mode 100644 index 0000000..4820b89 --- /dev/null +++ b/fco2/testcases/nonconst-array-literal.occ @@ -0,0 +1,16 @@ +-- This tests an oddball case in occam-to-C translation: an array subscript is +-- not constant in C99 (even if it's a constant subscript of a constant). +-- We therefore have to avoid doing the "obvious" C translation of the code below +-- by constant-folding the subscript out of existance -- and making sure it +-- doesn't get pulled back out to a variable again! +VAL []INT xs IS [1, 2, 3, 4]: +VAL []INT ys IS [12, xs[2], 34]: +VAL [][]INT yss IS [[xs[0], xs[1]]]: +DATA TYPE ONE.REC + RECORD + [1]INT a: +: +VAL ONE.REC rec IS [[xs[2]]]: +PROC P () + SKIP +: diff --git a/fco2/testcases/record-literals.occ b/fco2/testcases/record-literals.occ index 9b8dbfb..b041ccb 100644 --- a/fco2/testcases/record-literals.occ +++ b/fco2/testcases/record-literals.occ @@ -1,4 +1,5 @@ -- Need to test that list literals inside record literals are not collapsed. +-- Need to test that arrays of records work. DATA TYPE ONE RECORD @@ -16,11 +17,26 @@ DATA TYPE SAME INT y: INT z: : +DATA TYPE WITH.ARRAY + RECORD + INT x: + [4]INT xs: +: +DATA TYPE WITH.RECORD + RECORD + INT q: + WITH.ARRAY wa: + BOOL w: +: PROC P () VAL INT x IS 42: VAL ONE one IS [42]: VAL DIFF diff IS [42, '**', 3.141]: VAL SAME same IS [42, 43, 44]: + VAL WITH.ARRAY val.wa IS [99, [44, 33, 22, 11]]: + WITH.ARRAY wa: + VAL WITH.RECORD val.wr IS [123, val.wa, TRUE]: + WITH.RECORD wr: SEQ ASSERT (one[i] = 42) ASSERT (diff[i] = 42) @@ -30,4 +46,28 @@ PROC P () ASSERT (same[x] = 42) ASSERT (same[y] = 43) ASSERT (same[z] = 44) + PROC check.wa (VAL WITH.ARRAY wa) + SEQ + ASSERT (wa[x] = 99) + ASSERT ((SIZE wa[xs]) = 4) + ASSERT (wa[xs][0] = 44) + ASSERT (wa[xs][1] = 33) + ASSERT (wa[xs][2] = 22) + ASSERT (wa[xs][3] = 11) + : + PROC check.wr (VAL WITH.RECORD wr) + SEQ + ASSERT (wr[q] = 123) + check.wa (wr[wa]) + ASSERT (wr[w]) + : + SEQ + check.wa (val.wa) + wa := val.wa + check.wa (wa) + check.wr (val.wr) + wr := val.wr + check.wr (wr) + wr[wa] := wa + check.wr (wr) :