diff --git a/ssm.cabal b/ssm.cabal index 025e7c0b..65e8bdc2 100644 --- a/ssm.cabal +++ b/ssm.cabal @@ -4,7 +4,7 @@ cabal-version: 1.12 -- -- see: https://github.com/sol/hpack -- --- hash: a0f8bd48de2115636fda8c0f782dfcf3b71c53ec06ad80fd9bbef24a1a513322 +-- hash: 0ad0929e4602c4758fd406557510901ce0830bde9d2ee8f0ed2215c9aa709b01 name: ssm version: 0.1.0.0 @@ -27,6 +27,7 @@ source-repository head library exposed-modules: + SSM.Backend.C.Analysis.WaitAnalysis SSM.Backend.C.CodeGen SSM.Backend.C.Compile SSM.Backend.C.Exp @@ -47,7 +48,6 @@ library SSM.Language SSM.Pretty SSM.Pretty.Syntax - SSM.TestProgram SSM.Util.Default SSM.Util.HughesList SSM.Util.Operators diff --git a/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs b/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs new file mode 100644 index 00000000..c72e95a8 --- /dev/null +++ b/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs @@ -0,0 +1,87 @@ +{- | This module implements different strategies that are used to assign triggers to +sensitize/desensitize statements. The current strategy, `primitiveTriggerIDs`, work by +taking a naive approach and assigns a unique trigger to each reference that sensitizes +at least once. +-} +module SSM.Backend.C.Analysis.WaitAnalysis + ( primitiveTriggerIDs + ) where + +import SSM.Backend.C.Types ( CStm(..) ) +import SSM.Core.Syntax ( Procedure(body) + , Reference + , Stm + ( Desensitize + , If + , Sensitize + , While + ) + ) + +import Control.Monad.State ( State + , execState + , get + , gets + , modify + , put + , runState + ) + +import qualified Data.Map as Map + +-- | State for the primitive trigger scheme +type PrimSt + = ( Int + , Map.Map Reference Int + , Map.Map (Reference, Int) Int + , Map.Map (Reference, Int) Int + ) + +{- | Return a triple containing + + 1. How many unique triggers are used + 2. A map that associates @(Reference, Int)@ -pairs with trigger IDs to use when + sensitizing + 3. A map that associates @(Reference, Int)@ -pairs with trigger IDs to use when + desensitizing. +-} +primitiveTriggerIDs + :: [CStm] -> (Int, Map.Map (Reference, Int) Int, Map.Map (Reference, Int) Int) +primitiveTriggerIDs stmts = + let st = (0, Map.empty, Map.empty, Map.empty) + (ww, _, se, de) = + execState (go stmts) (0, Map.empty, Map.empty, Map.empty) + in (ww, se, de) + where + go :: [CStm] -> State PrimSt () + go stmts = flip mapM_ stmts $ \x -> case x of + Numbered n (Sensitize r) -> recordSensitize r n + Numbered n (Desensitize r) -> recordDesensitize r n + Numbered n stm -> return () + CWhile n c bdy -> go bdy + CIf n c thn els -> go thn >> go els + + {- | Look up the unique trigger associated with a reference. If none exist yet, + generate one and return that one. -} + lookupTrigID :: Reference -> State PrimSt Int + lookupTrigID r = do + (i, m1, m2, m3) <- get + case Map.lookup r m1 of + Just id -> return id + Nothing -> do + put (i + 1, Map.insert r (i + 1) m1, m2, m3) + return $ i + 1 + + -- | Record the information that the reference @r@ on statement @n@ is sensitized + recordSensitize :: Reference -> Int -> State PrimSt () + recordSensitize r n = do + tid <- lookupTrigID r + (i, m1, m2, m3) <- get + put (i, m1, Map.insert (r, n) tid m2, m3) + + -- | Record the information that the reference @r@ on statement @n@ is desensitized + recordDesensitize :: Reference -> Int -> State PrimSt () + recordDesensitize r n = do + tid <- lookupTrigID r + (i, m1, m2, m3) <- get + put (i, m1, m2, Map.insert (r, n) tid m3) diff --git a/ssm/SSM/Backend/C/CodeGen.hs b/ssm/SSM/Backend/C/CodeGen.hs index 11ae8a29..5475a80d 100644 --- a/ssm/SSM/Backend/C/CodeGen.hs +++ b/ssm/SSM/Backend/C/CodeGen.hs @@ -15,7 +15,10 @@ module SSM.Backend.C.CodeGen import Control.Monad.State.Lazy ( State , evalState + , runState , gets + , get + , put , modify ) @@ -30,6 +33,7 @@ import Data.List ( sortOn ) import SSM.Backend.C.Exp import SSM.Backend.C.Identifiers import SSM.Backend.C.Types +import SSM.Backend.C.Analysis.WaitAnalysis import SSM.Core.Syntax import qualified SSM.Interpret.Trace as T @@ -71,8 +75,7 @@ should be computed first, before this information is used to generate the act struct and enter definitions. -} data TRState = TRState - { procedure :: Procedure -- ^ Procedure we are compiling - , ncase :: Int -- ^ Which number has the next case? + { ncase :: Int -- ^ Which number has the next case? , numwaits :: Int -- ^ The size of the widest wait , locals :: [Reference] -- ^ Local references declared with var } @@ -81,8 +84,8 @@ data TRState = TRState type TR a = State TRState a -- | Run a TR computation on a procedure. -runTR :: Procedure -> TR a -> a -runTR p tra = evalState tra $ TRState p 0 0 [] +runTR :: TR a -> a +runTR tra = evalState tra $ TRState 0 0 [] -- | Read and increment the number of cases in a procedure, i.e., `ncase++`. nextCase :: TR Int @@ -127,15 +130,23 @@ genGlobals globals = globalvars genInitProgram :: Program -> [C.Definition] genInitProgram p = [cunit| void $id:initialize_program(void) { - $items:(map initGlobal $ globalReferences p) + $items:(concat $ map initGlobal $ globalReferences p) $id:fork($id:(enter_ $ identName $ entry p) (&ssm_top_parent, SSM_ROOT_PRIORITY, SSM_ROOT_DEPTH)); } |] where -- | Initialize global reference - initGlobal :: (Ident, Type) -> C.BlockItem - initGlobal (n, t) = [citem| $id:(initialize_ t)(&$id:(identName n));|] + initGlobal :: (Ident, Type) -> [C.BlockItem] + initGlobal (n, Ref TEvent) = + [ [citem| $id:(initialize_ TEvent)(&$id:(identName n));|] + , [citem| $id:(assign_ TEvent)(&$id:(identName n), 0);|] + ] + initGlobal (n, Ref t) = + [ [citem| $id:(initialize_ t)(&$id:(identName n));|] + , [citem| $id:(assign_ t)(&$id:(identName n), 0, 0);|] + ] + initGlobal (_, t) = error $ "error initializing global variable of type " ++ show t -- | Generate include statements, to be placed at the top of the generated C. genPreamble :: [C.Definition] @@ -179,19 +190,18 @@ function prototype declarations, while the snd element contains the function definitions. -} genProcedure :: Procedure -> ([C.Definition], [C.Definition]) -genProcedure p = runTR p $ do - (stepDecl , stepDefn ) <- genStep - (enterDecl, enterDefn) <- genEnter - structDefn <- genStruct +genProcedure p = runTR $ do + (stepDecl , stepDefn ) <- genStep p + (enterDecl, enterDefn) <- genEnter p + structDefn <- genStruct p return ([structDefn, enterDecl, stepDecl], [enterDefn, stepDefn]) {- | Generate struct definition for an SSM 'Procedure'. This is where local variables, triggers, and parameter values are stored. -} -genStruct :: TR C.Definition -genStruct = do - p <- gets procedure +genStruct :: Procedure -> TR C.Definition +genStruct p = do ts <- gets numwaits ls <- gets locals return [cedecl| @@ -224,9 +234,8 @@ genStruct = do Its struct is allocated and initialized (partially; local variables' values are left uninitialized). -} -genEnter :: TR (C.Definition, C.Definition) -genEnter = do - p <- gets procedure +genEnter :: Procedure -> TR (C.Definition, C.Definition) +genEnter p = do ts <- gets numwaits ls <- gets locals let actname = identName $ name p @@ -283,11 +292,17 @@ This function just defines the function definition and switch statement that wraps the statements of the procedure. The heavy lifting is performed by 'genCase'. -} -genStep :: TR (C.Definition, C.Definition) -genStep = do - p <- gets procedure +genStep :: Procedure -> TR (C.Definition, C.Definition) +genStep p = do + -- turn the statements that make up the body into uniquely numbered statements + let cstmts = toCStm $ body p + -- trigger assignment + let (widestwait, semap, demap) = primitiveTriggerIDs cstmts + + modify $ \st -> st { numwaits = widestwait } + _ <- nextCase -- Toss away 0th case - cases <- concat <$> mapM genCase (body p) + cases <- concat <$> mapM (genCase semap demap) cstmts locs <- gets locals final <- nextCase let @@ -355,128 +370,130 @@ genStep = do |] ) -{- | Generate the list of statements from each 'Stm' in an SSM 'Procedure'. +{- | Generate the list of statements. Note that this compilation scheme might not work if the language were to support return statements. This could be fixed by generating a break, and moving the leave call to outside of the switch statement in 'genStep'. -} -genCase :: Stm -> TR [C.Stm] -genCase (NewRef n t v) = do - locs <- gets locals - let lvar = identName n - lhs = [cexp|&$id:acts->$id:lvar|] - rhs = genExp locs v - addLocal $ makeDynamicRef n (mkReference t) - case baseType t of - TEvent -> return [[cstm|$id:(assign_ t)($exp:lhs, $id:actg->priority);|]] - _ -> - return [[cstm|$id:(assign_ t)($exp:lhs, $id:actg->priority, $exp:rhs);|]] -genCase (SetRef r e) = do - locs <- gets locals - let lvar = refIdent r - t = refType r - lhs = refPtr r locs - rhs = genExp locs e - case baseType t of - TEvent -> return [[cstm|$id:(assign_ t)($exp:lhs, $id:actg->priority);|]] - _ -> - return [[cstm|$id:(assign_ t)($exp:lhs, $id:actg->priority, $exp:rhs);|]] -genCase (SetLocal n t e) = do - locs <- gets locals - let lvar = identName n - lhs = [cexp|&$id:acts->$id:lvar|] - rhs = genExp locs e - return [[cstm| $id:acts->$id:(identName n) = $exp:rhs;|]] -genCase (If c t e) = do +genCase :: Map.Map (Reference, Int) Int -> Map.Map (Reference, Int) Int -> CStm -> TR [C.Stm] +genCase sensitizemap desensitizemap (Numbered n stm) = case stm of + + CreateRef n t -> do + addLocal $ makeDynamicRef n t + return [] + + SetRef r e -> do + locs <- gets locals + let lvar = refIdent r + t = refType r + lhs = refPtr r locs + rhs = genExp locs e + case baseType t of + TEvent -> return [[cstm|$id:(assign_ t)($exp:lhs, $id:actg->priority);|]] + _ -> + return [[cstm|$id:(assign_ t)($exp:lhs, $id:actg->priority, $exp:rhs);|]] + + SetLocal n t e -> do + locs <- gets locals + let lvar = identName n + lhs = [cexp|&$id:acts->$id:lvar|] + rhs = genExp locs e + return [[cstm| $id:acts->$id:(identName n) = $exp:rhs;|]] + + If c thn els -> error "error while generating C - wait analysis failed (found If)" + While c bdy -> error "error while generating C - wait analysis failed (found While)" + + Skip -> return [] + + After d r v -> do + locs <- gets locals + let lvar = refIdent r + t = refType r + del = genTimeDelay locs d + lhs = refPtr r locs + rhs = genExp locs v + -- Note that the semantics of 'After' and 'later_' differ---the former + -- expects a relative time, whereas the latter takes an absolute time. + -- Thus we add now() in the code we generate. + case baseType t of + TEvent -> return [[cstm| $id:(later_ t)($exp:lhs, $id:now() + $exp:del);|]] + _ -> return + [[cstm| $id:(later_ t)($exp:lhs, $id:now() + $exp:del, $exp:rhs);|]] + + Sensitize r -> do + -- fetch the id of the trigger to sensitize on + let trigid = case Map.lookup (r, n) sensitizemap of + Just id -> id + Nothing -> error $ + "wait analysis failed -- no trigger ID found for line " ++ show n ++ + " when sensitizing" + svvar <- refSV r <$> gets locals + return [ [cstm|$id:debug_trace($string:(show $ T.ActSensitize $ refName r)); |] + , [cstm|$id:sensitize($exp:svvar, &$id:acts->$id:(trig_ trigid)); |] + ] + + Desensitize r -> do + let trigid = case Map.lookup (r, n) desensitizemap of + Just id -> id + Nothing -> error $ + "wait analysis failed -- no trigger ID found for line " ++ show n ++ + " when desensitizing" + return [[cstm|$id:desensitize(&$id:acts->$id:(trig_ trigid));|]] + + Yield -> do + caseNum <- nextCase + return [ [cstm| $id:actg->pc = $int:caseNum; |] + , [cstm| return; |] + , [cstm| case $int:caseNum: ; |] + ] + + Fork cs -> do + locs <- gets locals + let + genCall :: Int -> (Ident, [Either SSMExp Reference]) -> C.Stm + genCall i (r, as) = + [cstm|$id:fork($id:(enter_ (identName r))($args:enterArgs));|] + where + enterArgs = + [ [cexp|actg|] + , [cexp|actg->priority + $int:i * (1 << $exp:newDepth)|] + , newDepth + ] + ++ map genArg as + genArg :: Either SSMExp Reference -> C.Exp + genArg (Left e) = genExp locs e + genArg (Right r) = refPtr r locs + + newDepth :: C.Exp + newDepth = [cexp|actg->depth - $int:depthSub|] + + depthSub :: Int + depthSub = + (ceiling $ logBase (2 :: Double) $ fromIntegral $ length cs) :: Int + + checkNewDepth :: C.Stm + checkNewDepth = [cstm| + if ($id:actg->depth < $int:depthSub) + $id:throw($exp:exhausted_priority); |] + + genTrace :: (Ident, [Either SSMExp Reference]) -> C.Stm + genTrace (r, _) = [cstm|$id:debug_trace($string:event);|] + where event = show $ T.ActActivate $ identName r + + return + $ checkNewDepth + : map genTrace cs + ++ zipWith genCall [0 :: Int ..] cs + +genCase sensitizemap desensitizemap (CIf n c thn els) = do locs <- gets locals let cnd = genExp locs c - thn <- concat <$> mapM genCase t - els <- concat <$> mapM genCase e - return [[cstm| if ($exp:cnd) { $stms:thn } else { $stms:els }|]] -genCase (While c b) = do - locs <- gets locals + thn' <- concat <$> mapM (genCase sensitizemap desensitizemap) thn + els' <- concat <$> mapM (genCase sensitizemap desensitizemap) els + return [[cstm| if ($exp:cnd) { $stms:thn' } else { $stms:els' } |]] +genCase sensitizemap desensitizemap (CWhile n c bdy) = do + locs <- gets locals let cnd = genExp locs c - bod <- concat <$> mapM genCase b + bod <- concat <$> mapM (genCase sensitizemap desensitizemap) bdy return [[cstm| while ($exp:cnd) { $id:debug_microtick(); $stms:bod } |]] -genCase (After d r v) = do - locs <- gets locals - let lvar = refIdent r - t = refType r - del = genTimeDelay locs d - lhs = refPtr r locs - rhs = genExp locs v - -- Note that the semantics of 'After' and 'later_' differ---the former - -- expects a relative time, whereas the latter takes an absolute time. - -- Thus we add now() in the code we generate. - case baseType t of - TEvent -> return [[cstm| $id:(later_ t)($exp:lhs, $id:now() + $exp:del);|]] - _ -> return - [[cstm| $id:(later_ t)($exp:lhs, $id:now() + $exp:del, $exp:rhs);|]] -genCase (Wait ts) = do - caseNum <- nextCase - maxWaits $ length ts - locs <- gets locals - let trigs = zip [1 ..] $ map (`refSV` locs) ts - return - $ map getTrace ts - ++ map sensitizeTrig trigs - ++ [ [cstm| $id:actg->pc = $int:caseNum; |] - , [cstm| return; |] - , [cstm| case $int:caseNum: ; |] - ] - ++ fmap desensitizeTrig trigs - where - sensitizeTrig :: (Int, C.Exp) -> C.Stm - sensitizeTrig (i, trig) = - [cstm|$id:sensitize($exp:trig, &$id:acts->$id:(trig_ i));|] - - desensitizeTrig :: (Int, C.Exp) -> C.Stm - desensitizeTrig (i, _) = [cstm|$id:desensitize(&$id:acts->$id:(trig_ i));|] - - getTrace :: Reference -> C.Stm - getTrace r = [cstm|$id:debug_trace($string:event);|] - where event = show $ T.ActSensitize $ refName r -genCase (Fork cs) = do - locs <- gets locals - caseNum <- nextCase - let - genCall :: Int -> (Ident, [Either SSMExp Reference]) -> C.Stm - genCall i (r, as) = - [cstm|$id:fork($id:(enter_ (identName r))($args:enterArgs));|] - where - enterArgs = - [ [cexp|actg|] - , [cexp|actg->priority + $int:i * (1 << $exp:newDepth)|] - , newDepth - ] - ++ map genArg as - genArg :: Either SSMExp Reference -> C.Exp - genArg (Left e) = genExp locs e - genArg (Right r) = refPtr r locs - - newDepth :: C.Exp - newDepth = [cexp|actg->depth - $int:depthSub|] - - depthSub :: Int - depthSub = - (ceiling $ logBase (2 :: Double) $ fromIntegral $ length cs) :: Int - - checkNewDepth :: C.Stm - checkNewDepth = [cstm| - if ($id:actg->depth < $int:depthSub) - $id:throw($exp:exhausted_priority); |] - - genTrace :: (Ident, [Either SSMExp Reference]) -> C.Stm - genTrace (r, _) = [cstm|$id:debug_trace($string:event);|] - where event = show $ T.ActActivate $ identName r - - return - $ checkNewDepth - : map genTrace cs - ++ zipWith genCall [0 :: Int ..] cs - ++ [ [cstm| $id:actg->pc = $int:caseNum; |] - , [cstm| return; |] - , [cstm| case $int:caseNum: ; |] - ] -genCase Skip = return [] diff --git a/ssm/SSM/Backend/C/Types.hs b/ssm/SSM/Backend/C/Types.hs index 65ccf501..d50dcd65 100644 --- a/ssm/SSM/Backend/C/Types.hs +++ b/ssm/SSM/Backend/C/Types.hs @@ -6,6 +6,8 @@ import Language.C.Quote.GCC ( cexp ) import qualified Language.C.Syntax as C import qualified SSM.Interpret.Trace as T +import Control.Monad.State + -- | Obtain base type for a type, i.e., unwrapping all references. baseType :: Type -> Type baseType (Ref t) = baseType t @@ -33,5 +35,44 @@ intFmt = fmt . baseType fmt TUInt8 = "%u" varFmt :: (Ident, Type) -> T.VarVal -varFmt (n, t) | baseType t == TEvent = T.VarVal (identName n) (baseType t) T.UnitType - | otherwise = T.VarVal (identName n) (baseType t) $ T.IntegralFmt $ intFmt t +varFmt (n, t) + | baseType t == TEvent = T.VarVal (identName n) (baseType t) T.UnitType + | otherwise = T.VarVal (identName n) (baseType t) $ T.IntegralFmt $ intFmt t + +{- | Data type that annotates a procedures body with unique line-numbers. Used to be able +to refer to individual statements in auxiliary data objects. -} +data CStm = Numbered Int Stm -- ^ Annotate a statement with a number + | CWhile Int SSMExp [CStm] -- ^ While with recursive @CStm@ instead of @Stm@ + | CIf Int SSMExp [CStm] [CStm] -- ^ If, by the same principle as @CWhile@ + deriving Show + +-- | Take a procedure body and number all the statements +toCStm :: [Stm] -> [CStm] +toCStm stmts = evalState (toCStm' stmts) 0 + where + -- | Actually number the statements and turn them into `CStm` + toCStm' :: [Stm] -> State Int [CStm] + toCStm' [] = return [] + toCStm' (x : xs) = case x of + If c thn els -> do + thn' <- toCStm' thn + els' <- toCStm' els + n <- number + xs' <- toCStm' xs + return $ CIf n c thn' els' : xs' + While c bdy -> do + bdy' <- toCStm' bdy + n <- number + xs' <- toCStm' xs + return $ CWhile n c bdy' : xs' + _ -> do + n <- number + xs' <- toCStm' xs + return $ Numbered n x : xs' + + -- | Generate the next unique statement number + number :: State Int Int + number = do + i <- get + put $ i + 1 + return i diff --git a/ssm/SSM/Core/Syntax.hs b/ssm/SSM/Core/Syntax.hs index a6f32a23..b6cd28bb 100644 --- a/ssm/SSM/Core/Syntax.hs +++ b/ssm/SSM/Core/Syntax.hs @@ -4,14 +4,14 @@ a parser or something else (in our case the embedded language, however). The rest of the compiler will work with this representation (compiler, interpreter, pretty printer etc). -} module SSM.Core.Syntax - ( -- * SSM Core Syntax + ( -- * SSM Core Syntax -- ** Identifiers {- | Some elements in the core syntax are named, and those names are represented by these identifiers. In some places information is grabbed from the Haskell source file and added to the identifier. -} - Ident(..) - , SrcInformation(..) + Ident(..) + , SrcInformation(..) -- ** Types {- | These are the types that are valid in the SSM language, and some simple @@ -21,37 +21,37 @@ module SSM.Core.Syntax The type class `SSMType` is there so that we can marshal some Haskell types into their corresponding `Type` representation. -} - , Type(..) - , dereference - , mkReference - , isReference - , SSMType(..) + , Type(..) + , dereference + , mkReference + , isReference + , SSMType(..) -- ** References {- | References in the SSM language is simply something with a name and a type. If the reference references something of type @a@, the type will be @Ref a@. When we add IO support some references might need to be allocated globally, in which case we need to add a new variant. -} - , Reference(..) - , refType - , refName - , refIdent - , renameRef - , makeDynamicRef - , makeStaticRef - , isDynamic - , isStatic + , Reference(..) + , refType + , refName + , refIdent + , renameRef + , makeDynamicRef + , makeStaticRef + , isDynamic + , isStatic -- ** Expressions {- | Expressions in the language are quite few at the moment. Adding support for new expressions here (especially more numerical operators) should be very simple. -} - , SSMExp(..) - , SSMLit(..) - , UnaryOpE(..) - , UnaryOpR(..) - , BinOp(..) - , expType + , SSMExp(..) + , SSMLit(..) + , UnaryOpE(..) + , UnaryOpR(..) + , BinOp(..) + , expType -- ** Time {- Exposes units of time to wrap Word64 expressions. -} @@ -61,32 +61,39 @@ module SSM.Core.Syntax -- ** Statements {- | Statements that make up an SSM program take any of these forms. A program is made up of a list of these statements.-} - , Stm(..) + , Stm(..) -- ** Procedures {- | A procedure is a piece of code that is named and possibly parameterised over some parameters. When the code is later turned into C code, every procedure is compiled into three components -- an activation record, an initialization function and a step function. -} - , Procedure(..) + , Procedure(..) -- ** Programs {- | A program consists of a map of names & procedures, the name of an entry point of a program and any arguments the entry point should be applied to. -} - , Program(..) - , SSMProgram(..) - ) where - -import Data.Int -import Data.Word -import qualified Data.Map as Map -import Control.Monad.State.Lazy - ( forM, modify, runState, MonadState(put, get), State ) + , Program(..) + , SSMProgram(..) + ) where + +import Control.Monad.State.Lazy ( MonadState(get, put) + , State + , forM + , modify + , runState + ) +import Data.Int +import qualified Data.Map as Map +import Data.Word -- Identifiers -- | Data type of Identifiers -data Ident = Ident { identName :: String, identSrcInfo :: Maybe SrcInformation} +data Ident = Ident + { identName :: String + , identSrcInfo :: Maybe SrcInformation + } deriving (Show, Read) instance Eq Ident where @@ -109,12 +116,12 @@ data Type | TBool -- ^ Boolean type | TEvent -- ^ Event type | Ref Type -- ^ A reference to another type - deriving (Eq, Show, Read) + deriving (Eq, Ord, Show, Read) -- | Dereference a type. Throws an error if the type is not a reference. dereference :: Type -> Type dereference (Ref t) = t -dereference t = error $ "not a reference type: can not dereference " ++ show t +dereference t = error $ "not a reference type: can not dereference " ++ show t -- | Turn a type into a reference to that type. mkReference :: Type -> Type @@ -143,19 +150,19 @@ instance SSMType Word8 where typeOf _ = TUInt8 instance SSMType Word64 where - typeOf _ = TUInt64 + typeOf _ = TUInt64 instance SSMType Int32 where - typeOf _ = TInt32 + typeOf _ = TInt32 instance SSMType Int64 where - typeOf _ = TInt64 + typeOf _ = TInt64 instance SSMType Bool where - typeOf _ = TBool + typeOf _ = TBool instance SSMType () where - typeOf _ = TEvent + typeOf _ = TEvent -- References @@ -164,7 +171,7 @@ instance SSMType () where type Ref = (Ident, Type) -- | References in our language. They are either dynamic or static. -data Reference +data Reference {- | A Dynamic reference will be dynamically allocated and deallocated as a program is running. It will reside in an activation record in the generated C-code. -} = Dynamic Ref @@ -172,12 +179,12 @@ data Reference reside in an activation record in the generated C-code. It can be referenced from any context. -} | Static Ref - deriving (Eq, Show, Read) + deriving (Eq, Ord, Show, Read) -- | Type of a reference refType :: Reference -> Type -refType (Dynamic (_,t)) = t -refType (Static (_,t)) = t +refType (Dynamic (_, t)) = t +refType (Static (_, t)) = t -- | Name of a reference refName :: Reference -> String @@ -185,13 +192,13 @@ refName = identName . refIdent -- | Return the `Ident` of a `Reference` refIdent :: Reference -> Ident -refIdent (Dynamic (n,_)) = n -refIdent (Static (n,_)) = n +refIdent (Dynamic (n, _)) = n +refIdent (Static (n, _)) = n -- | Rename a reference renameRef :: Reference -> Ident -> Reference -renameRef (Dynamic (_,t)) n = Dynamic (n, t) -renameRef (Static (_,t)) n = Static (n, t) +renameRef (Dynamic (_, t)) n = Dynamic (n, t) +renameRef (Static (_, t)) n = Static (n, t) -- | Returns @True@ if a reference is a dynamic reference isDynamic :: Reference -> Bool @@ -224,9 +231,8 @@ data SSMLit deriving (Eq, Show, Read) -- | Expressions of unary operators on expressions -data UnaryOpE - = Neg -- ^ negation - deriving (Show, Eq, Read) +data UnaryOpE = Neg -- ^ negation + deriving (Show, Eq, Read) -- | Expressions of unary operators on references data UnaryOpR @@ -245,10 +251,10 @@ data BinOp -- | Return the type of an expression expType :: SSMExp -> Type -expType (Var t _) = t -expType (Lit t _) = t -expType (UOpE t _ _) = t -expType (UOpR t _ _) = t +expType (Var t _ ) = t +expType (Lit t _ ) = t +expType (UOpE t _ _ ) = t +expType (UOpR t _ _ ) = t expType (BOp t _ _ _) = t -- Time @@ -274,11 +280,12 @@ data SSMTime = SSMTime SSMExp SSMTimeUnit {- | A lower level representation of the statements that make up the body of an SSM program. -} data Stm - {-| Create a new reference with the given name, which references a value of the - given type, with the initial value specified by the expression. -} - = NewRef Ident Type SSMExp + {- | Create a new `SSM.Core.Syntax.Reference` with a given type. References that are + created by executing this statement reside in the context of a process, so it will + reside in the activation record of that process. -} + = CreateRef Ident Type | SetRef Reference SSMExp -- ^ Set the value of a reference - {-| Set the value of a local expression specified by the name, with the given type, + {- | Set the value of a local expression specified by the name, with the given type, with the new value specified by the expression. -} | SetLocal Ident Type SSMExp @@ -289,7 +296,9 @@ data Stm {- | @After d r v@ - After @d@ units of time the reference @r@ should get the new value @v@. -} | After SSMTime Reference SSMExp - | Wait [Reference] -- ^ Wait for any of the references to be written to + | Sensitize Reference -- ^ Sensitize the current process on this reference + | Desensitize Reference -- ^ Desensitize the current process on this reference + | Yield -- ^ Yield control {-| Fork procedures. The procedures are now identified by their name, and the fork site contains only that name and the arguments to apply the function to. -} | Fork [(Ident, [Either SSMExp Reference])] @@ -297,24 +306,25 @@ data Stm -- | A procedure has a name, parameter names & types and a body. data Procedure = Procedure - { -- | Name of the procedure. - name :: Ident + { -- | Name of the procedure. + name :: Ident -- | Parameter names and types of the procedure. - , arguments :: [(Ident, Type)] + , arguments :: [(Ident, Type)] -- | Statements that make up this procedure. - , body :: [Stm] - } deriving (Eq, Show, Read) + , body :: [Stm] + } + deriving (Eq, Show, Read) -- | Program definition data Program = Program - { -- | Name of the procedure that is the program entrypoint. - entry :: Ident + { -- | Name of the procedure that is the program entrypoint. + entry :: Ident -- | Map that associates procedure names with their definitions. - , funs :: Map.Map Ident Procedure + , funs :: Map.Map Ident Procedure -- | Name and type of references that exist in the global scope. - , globalReferences :: [(Ident, Type)] - } - deriving (Show, Read, Eq) + , globalReferences :: [(Ident, Type)] + } + deriving (Show, Read, Eq) -- | Class of types that can be converted to a `Program`. class SSMProgram a where diff --git a/ssm/SSM/Frontend/Syntax.hs b/ssm/SSM/Frontend/Syntax.hs index 5cf04b6f..00132297 100644 --- a/ssm/SSM/Frontend/Syntax.hs +++ b/ssm/SSM/Frontend/Syntax.hs @@ -247,7 +247,12 @@ transpile program = transpileProcedure :: [SSMStm] -> Transpile [S.Stm] transpileProcedure xs = fmap concat $ forM xs $ \x -> case x of - NewRef n e -> return $ [S.NewRef n (S.expType e) e] + NewRef n e -> let rt = S.mkReference $ S.expType e + ref = S.makeDynamicRef n rt + in return $ [ S.CreateRef n rt + , S.SetRef ref e + + ] SetRef r e -> return $ [S.SetRef r e] SetLocal (S.Var t n) e2 -> return $ [S.SetLocal n t e2] SetLocal _ _ -> error "Trying to set a local variable that is not a variable" @@ -263,10 +268,10 @@ transpileProcedure xs = fmap concat $ forM xs $ \x -> case x of return $ [S.While c bdy'] After d r v -> return $ [S.After d r v] - Wait refs -> return $ [S.Wait refs] + Wait refs -> return $ map S.Sensitize refs ++ [S.Yield] ++ map S.Desensitize refs Fork procs -> do procs' <- mapM getCall procs - return $ [S.Fork procs'] + return $ [S.Fork procs', S.Yield] Procedure n -> return [] Argument n x a -> return [] diff --git a/ssm/SSM/Interpret/Internal.hs b/ssm/SSM/Interpret/Internal.hs index 78d841cb..d124a93f 100644 --- a/ssm/SSM/Interpret/Internal.hs +++ b/ssm/SSM/Interpret/Internal.hs @@ -39,14 +39,15 @@ module SSM.Interpret.Internal , pushInstructions -- * Reference helpers - , newRef + , createRef , writeRef , writeLocal , readRef -- * Wait, fork, and leave + helpers - , wait , fork + , sensitize + , desensitize , setRunningChildren , addressToSelf , pds @@ -108,7 +109,7 @@ globals :: Program -> ST s (Map.Map Ident (Var s)) globals p = do vars <- forM (globalReferences p) $ \(id,t) -> do let initval = defaultValue (dereference t) - v <- newVar' initval maxBound + v <- newVar' initval 0 return (id, v) return $ Map.fromList vars @@ -125,13 +126,24 @@ defaultValue (Ref _) = error "default value of reference not allowed" -- | Log the state of all variables in the current process to the event trace. traceVars :: Interp s () traceVars = do - mapM_ varEvent . sortOn fst . Map.toList . variables =<< currentProcess - mapM_ varEvent . sortOn fst . Map.toList . localrefs =<< currentProcess + mapM_ traceNonLocal . sortOn fst . Map.toList . variables =<< currentProcess + mapM_ traceLocal . sortOn fst . Map.toList . localrefs =<< currentProcess where - varEvent (n, v) = do + -- | For non-local variables, we always wish to announce their value on entry + traceNonLocal :: (Ident, Var s) -> Interp s () + traceNonLocal (n, v) = do (e, _, _, _, _) <- lift' $ readSTRef v (t, v) <- getTypeConcreteVal <$> lift' (readSTRef e) tellEvent $ T.ActVar $ T.VarVal (identName n) t v + {- | For local variables we only wish to know of their value if they have ever been + given any. -} + traceLocal :: (Ident, Var s) -> Interp s () + traceLocal (n, v) = do + (e, _, lastwrite, _, _) <- lift' $ readSTRef v + (t, v) <- getTypeConcreteVal <$> lift' (readSTRef e) + if lastwrite /= maxBound + then tellEvent $ T.ActVar $ T.VarVal (identName n) t v + else return () {-********** Time management **********-} @@ -253,10 +265,17 @@ enqueue p = do mcqs <- gets maxActQueueSize if nc >= mcqs then terminate T.ExhaustedActQueue - else modify $ \st -> st - { readyQueue = IntMap.insert (priority p) p (readyQueue st) - , numacts = numacts st + 1 - } + else do + actQueue <- gets readyQueue + {- log (n,W) complexity, where n is the number of elements in the map, + and W is the number of bits (32 or 64) of an Int -} + if IntMap.member (priority p) actQueue + then return () + else modify $ \st -> st + { readyQueue = IntMap.insert (priority p) p (readyQueue st) + , numacts = numacts st + 1 + } + -- | Fetch the process with the lowest priority from the ready queue. dequeue :: Interp s (Proc s) @@ -266,6 +285,7 @@ dequeue = do when (IntMap.null acts) $ crash "Interpreter error: dequeue called on empty readyqueue" put $ st { readyQueue = IntMap.deleteMin acts, numacts = numacts st - 1 } + --traceM $ show $ continuation $ snd $ (IntMap.findMin acts) return $ snd $ IntMap.findMin acts -- | Size of the ready queue. @@ -289,10 +309,11 @@ Nothing will be returned if the process has no more work to do. nextInstruction :: Interp s (Maybe Stm) nextInstruction = do p <- gets process - case continuation p of + cont <- lift' $ readSTRef (continuation p) + case cont of [] -> return Nothing (x : xs) -> do - modify $ \st -> st { process = p { continuation = xs } } + lift' $ writeSTRef (continuation p) xs return $ Just x -- | Push additional instructions onto a process. Used e.g when evaluating @@ -300,7 +321,8 @@ nextInstruction = do pushInstructions :: [Stm] -> Interp s () pushInstructions stmts = do p <- gets process - modify $ \st -> st { process = p { continuation = stmts ++ continuation p } } + cont <- lift' $ readSTRef (continuation p) + lift' $ writeSTRef (continuation p) $ stmts ++ cont {-********** Variable management **********-} @@ -308,28 +330,23 @@ pushInstructions stmts = do createVar :: SSMExp -> Interp s (Var s) createVar e = do v <- eval e - n <- getNow - lift' $ newVar' v n - -{- | Create a new reference with an initial value. + lift' $ newVar' v maxBound -Note: it is added to the map containing the local variables. -} -newRef :: Ident -> SSMExp -> Interp s () -newRef n e = do - ref <- createVar e - p <- gets process - modify $ \st -> st { process = p { localrefs = Map.insert n ref (localrefs p) } } +{- | Create a new reference. The initial value of this reference tries to mirror a +zero-initialized value as much as possible, but don't try on this. -{- | Create a new variable with an initial value, and adds it to the current process's -variable storage. When a variable is created it is considered written to. +Note: it is added to the map containing local variables. -} +createRef :: Ident -> Type -> Interp s () +createRef n t = newRef n $ defaultValue (dereference t) + where + {- | Create a new reference with an initial value. -Note: This does the same thing as `NewRef`, but it adds the reference to the map -containing expression variables & references supplied by a caller. -} -newVar :: Ident -> SSMExp -> Interp s () -newVar n e = do - ref <- createVar e - p <- gets process - modify $ \st -> st { process = p { variables = Map.insert n ref (variables p) } } + Note: it is added to the map containing the local variables. -} + newRef :: Ident -> SSMExp -> Interp s () + newRef n e = do + ref <- createVar e + p <- gets process + modify $ \st -> st { process = p { localrefs = Map.insert n ref (localrefs p) } } -- | Write a value to a variable. writeRef :: Reference -> SSMExp -> Interp s () @@ -435,24 +452,16 @@ writeVar_ ref e prio = do (variable, waits, _, me, mv) <- lift' $ readSTRef ref lift' $ writeSTRef variable e -- actually update the variable value + -- keep = processes to not wake up, towake = processes that should be woken up let (keep, towake) = Map.split prio waits -- wake up and desensitize the processes - mapM_ desensitize towake + mapM_ enqueue towake -- update the variable to be written to in this instant and give it knowledge -- of which processes are still waiting on it n <- getNow lift' $ writeSTRef ref (variable, keep, n, me, mv) - where - -- | Wake up a process, remove it from all trigger lists, and enqueueing it. - desensitize :: Proc s -> Interp s () - desensitize p = do - let variables = fromJust $ waitingOn p - forM_ variables $ \r -> do - (ref, procs, b, me, mv) <- lift' $ readSTRef r - lift' $ writeSTRef r (ref, Map.delete (priority p) procs, b, me, mv) - enqueue $ p { waitingOn = Nothing } -- | Look up a variable associated with a reference lookupRef :: Reference -> Interp s (Var s) @@ -475,7 +484,6 @@ lookupRef ref = Nothing -> error $ "interpreter error - can not find global variable " ++ refName ref --- | Make a procedure wait for writes to the variable identified by the name @v@. sensitize :: Reference -> Interp s () sensitize ref = do p <- gets process @@ -486,6 +494,13 @@ sensitize ref = do then return () else lift' $ writeSTRef r (ref, Map.insert (priority p) p procs,b,me,mv) +desensitize :: Reference -> Interp s () +desensitize ref = do + p <- gets process + r <- lookupRef ref + (ref,procs,b,me,mv) <- lift' $ readSTRef r + lift' $ writeSTRef r (ref, Map.delete (priority p) procs, b, me, mv) + -- | This function will, if told how many new processes are being forked, compute -- new priorities and depths for them. pds :: Int -> Interp s [(Int, Int)] @@ -498,25 +513,6 @@ pds k = do let prios = [ prio + i * (2 ^ d') | i <- [0 .. k - 1] ] -- new prios return $ zip prios (repeat d') -{-********** Sensitizing a process **********-} - -{- | This function will make sure that the current process will block until any -of the references in the list @refs@ have been written to. --} -wait :: [Reference] -> Interp s () -wait refs = do - refs' <- mapM lookupRef refs - modify $ \st -> st { process = (process st) { waitingOn = Just refs' } } - mapM_ sensitize refs - - - - - - - - - {-********** Forking processes **********-} -- | Set the number of running children of the current process to @n@. @@ -539,7 +535,8 @@ fork :: (Ident, [Either SSMExp Reference]) -- ^ Procedure to fork (name and ar fork (n,args) prio dep par = do p <- lookupProcedure n variables <- params $ (map fst . arguments) p - enqueue $ Proc (identName n) prio dep 0 (Just par) variables Map.empty Nothing (body p) + bdy <- lift' $ newSTRef (body p) + enqueue $ Proc (identName n) prio dep 0 (Just par) variables Map.empty bdy where -- | Return an initial variable storage for the new process. Expression arguments are turned into -- new STRefs while reference arguments are passed from the calling processes variable storage. diff --git a/ssm/SSM/Interpret/Interpreter.hs b/ssm/SSM/Interpret/Interpreter.hs index 5abe95a8..2ede113d 100644 --- a/ssm/SSM/Interpret/Interpreter.hs +++ b/ssm/SSM/Interpret/Interpreter.hs @@ -7,6 +7,7 @@ module SSM.Interpret.Interpreter import SSM.Core.Syntax import SSM.Interpret.Internal +import SSM.Interpret.Types import qualified SSM.Interpret.Trace as T import SSM.Util.Default ( Default(def) ) import SSM.Util.HughesList hiding ( (++) ) @@ -43,11 +44,9 @@ interpret config program = runST $ do Nothing -> error $ "Interpreter error: cannot find entry point: " ++ identName (entry p) globs <- globals p + initprocess <- mkProc config p fun -- Run the interpret action and produce it's output - (_, events) <- runWriterT $ runStateT run $ initState config p 0 globs $ mkProc - config - p - fun + (_, events) <- runWriterT $ runStateT run $ initState config p 0 globs initprocess return $ fromHughes events -- | Run the interpreter, serving the role of the @main@ function. @@ -95,13 +94,12 @@ Yields control when the process terminates (no more instructions) or suspends step :: Interp s () step = do i <- nextInstruction - p <- currentProcess case i of Nothing -> leave Just stm -> case stm of - NewRef n _ e -> do - newRef n e + CreateRef n t -> do + createRef n t continue SetRef r e -> do @@ -132,10 +130,15 @@ step = do scheduleEvent r (n' + d') v' continue - Wait refs -> do - forM_ refs $ \r -> tellEvent $ T.ActSensitize $ refName r - wait refs - yield + Yield -> yield + + Sensitize ref -> do + tellEvent $ T.ActSensitize $ refName ref + sensitize ref + continue + Desensitize ref -> do + desensitize ref + continue Fork procs -> do setRunningChildren (length procs) @@ -143,10 +146,12 @@ step = do pdeps <- pds (length procs) forM_ procs $ \(f, _) -> tellEvent $ T.ActActivate $ identName f forM_ (zip procs pdeps) $ \(f, (prio, dep)) -> fork f prio dep parent - yield + continue where -- | Convenience names for local control flow. - continue, yield :: Interp s () + continue :: Interp s () continue = step - yield = return () + + yield :: Interp s () + yield = return () diff --git a/ssm/SSM/Interpret/Types.hs b/ssm/SSM/Interpret/Types.hs index a16288df..7dda7142 100644 --- a/ssm/SSM/Interpret/Types.hs +++ b/ssm/SSM/Interpret/Types.hs @@ -93,14 +93,12 @@ data Proc s = Proc a parent. -} , variables :: Map.Map Ident (Var s) {- | Variables found in this map are those that are local to this process, aka - those that are created by the `SSM.Core.Syntax.NewRef` constructor. We need to + those that are created by the `SSM.Core.Syntax.CreateRef` constructor. We need to put them in a separate map so that we can quickly deschedule any outstanding events on them when a process is terminating. -} , localrefs :: Map.Map Ident (Var s) - -- | Variables this process is waiting for, if any - , waitingOn :: Maybe [Var s] -- | The work left to do for this process - , continuation :: [Stm] + , continuation :: STRef s [Stm] } deriving Eq @@ -109,17 +107,18 @@ mkProc :: InterpretConfig -- ^ Configuration -> Program -- ^ Program -> Procedure -- ^ Entry point - -> Proc s -mkProc conf p fun = Proc { procName = identName $ entry p - , priority = rootPriority conf - , depth = rootDepth conf - , runningChildren = 0 - , parent = Nothing - , variables = Map.empty - , localrefs = Map.empty - , waitingOn = Nothing - , continuation = body fun - } + -> ST s (Proc s) +mkProc conf p fun = do + bdy <- newSTRef (body fun) + return $ Proc { procName = identName $ entry p + , priority = rootPriority conf + , depth = rootDepth conf + , runningChildren = 0 + , parent = Nothing + , variables = Map.empty + , localrefs = Map.empty + , continuation = bdy + } {- | The show instance will only render the priority (this was initially diff --git a/ssm/SSM/Pretty/Syntax.hs b/ssm/SSM/Pretty/Syntax.hs index 2aa965b9..370cdba3 100644 --- a/ssm/SSM/Pretty/Syntax.hs +++ b/ssm/SSM/Pretty/Syntax.hs @@ -81,13 +81,11 @@ prettyProcedure p = do prettyStm :: Stm -> PP () prettyStm stm = case stm of - NewRef n t e -> emit $ concat [ prettyType t - , " *" - , identName n - , " = var " - , prettySSMExp e - ] - SetRef r e -> emit $ concat [ refName r + CreateRef n t -> emit $ concat [ prettyType t + , " " + , identName n] + SetRef r e -> emit $ concat [ "*" + , refName r , " = " , prettySSMExp e ] @@ -114,16 +112,18 @@ prettyStm stm = case stm of , " = " , prettySSMExp v ] - - Wait refs -> emit $ concat [ "wait [" - , intercalate ", " (map refName refs) - , "]" + Sensitize r -> emit $ concat [ "sensitize " + , refName r + ] + Desensitize r -> emit $ concat [ "desensitize " + , refName r ] Fork procs -> do let procs' = map prettyApp procs sep <- separator ind <- ask emit $ concat ["fork [ ", intercalate sep procs', "\n", replicate (ind + 5) ' ', "]"] + Yield -> emit "yield" where separator :: PP String separator = do diff --git a/test/lib/Test/SSM/QuickCheck/Generator.hs b/test/lib/Test/SSM/QuickCheck/Generator.hs index ccb6f075..e6121b94 100644 --- a/test/lib/Test/SSM/QuickCheck/Generator.hs +++ b/test/lib/Test/SSM/QuickCheck/Generator.hs @@ -101,14 +101,15 @@ arbProc :: Procedures -- ^ All procedures in the program -> Gen ([Stm], Int) arbProc _ _ _ c 0 = return ([], c) arbProc funs vars refs c n = frequency $ - [ (1, do t <- elements basetypes - e <- choose (0,3) >>= arbExp t vars refs - (name,c1) <- fresh c - let rt = mkReference t - let stm = NewRef name t e - let ref = makeDynamicRef name rt + [ (1, do t <- elements basetypes + (name,c1) <- fresh c + e <- choose (0,3) >>= arbExp t vars refs + let rt = mkReference t + stm1 = CreateRef name rt + ref = makeDynamicRef name rt + stm2 = SetRef ref e (rest, c2) <- arbProc funs vars (ref:refs) c1 (n-1) - return (stm:rest, c2) + return (stm1:stm2:rest, c2) ) , (1, do cond <- choose (0,3) >>= arbExp TBool vars refs @@ -127,7 +128,7 @@ arbProc funs vars refs c n = frequency $ forks <- mapM (applyFork vars refs) tofork let stm = Fork forks (rest,c') <- arbProc funs vars refs c (n-1) - return (stm:rest, c') + return (stm:Yield:rest, c') ) ] ++ @@ -141,14 +142,20 @@ arbProc funs vars refs c n = frequency $ (if null refs then [] else [ (1, do r <- elements refs - e <- choose (0,3) >>= arbExp (dereference $ refType r) vars refs + esize <- choose (0,3) + e <- if esize == 0 + then arbExp (dereference $ refType r) vars (delete r refs) esize + else arbExp (dereference $ refType r) vars refs esize (rest,c') <- arbProc funs vars refs c (n-1) let stm = SetRef r e return (stm:rest, c') ) - , (1, do r <- elements refs - v <- choose (0,3) >>= arbExp (dereference $ refType r) vars refs + , (1, do r <- elements refs + vsize <- choose (0,3) + v <- if vsize == 0 + then arbExp (dereference $ refType r) vars (delete r refs) vsize + else arbExp (dereference $ refType r) vars refs vsize (rest,c') <- arbProc funs vars refs c (n-1) delay <- choose (0, 3) >>= genDelay let stm = After delay r v @@ -156,8 +163,8 @@ arbProc funs vars refs c n = frequency $ ) , (1, do refs' <- sublistOf refs `suchThat` (not . null) (rest,c') <- arbProc funs vars refs c (n-1) - let stm = Wait refs' - return (stm:rest, c') + let stms = map Sensitize refs' ++ [Yield] ++ map Desensitize refs' + return (stms ++ rest, c') ) ]) where @@ -229,6 +236,10 @@ arbExp t vars refs 0 = oneof $ concat [ [litGen] TUInt64 -> return . Lit TUInt64 . LUInt64 =<< choose (0, 65500) TBool -> return . Lit TBool . LBool =<< arbitrary TEvent -> return $ Lit TEvent LEvent + _ -> error $ concat [ "generator error - tried to generate " + , "expression literal of type ", show t + , ", while expressions can only be generated" + , " of one of the base types"] -- | Generator that returns a randomly selected variable from the set of variables. varGen :: [Gen SSMExp] diff --git a/test/lib/Test/SSM/QuickCheck/Shrink/Expressions.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Expressions.hs index eb367777..789d28f3 100644 --- a/test/lib/Test/SSM/QuickCheck/Shrink/Expressions.hs +++ b/test/lib/Test/SSM/QuickCheck/Shrink/Expressions.hs @@ -29,7 +29,6 @@ shrinkExpInProcedure p = distributeMutate along with the body of a procedure. -} shrinkExpInStatement :: (SSMExp -> [SSMExp]) -> Stm -> [Stm] shrinkExpInStatement shrinkexp stm = case stm of - NewRef n t e -> [ NewRef n t e' | e' <- shrinkexp e ] SetRef r e -> [ SetRef r e' | e' <- shrinkexp e ] SetLocal n t e -> [ SetLocal n t e' | e' <- shrinkexp e ] -- don't shrink the delay for fear of producing an illegal delay (< now) diff --git a/test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs index 1e67b254..7009f25c 100644 --- a/test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs +++ b/test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs @@ -1,12 +1,13 @@ module Test.SSM.QuickCheck.Shrink.Fork - ( forks ) where + ( forks + ) where -import SSM.Core.Syntax -import SSM.Util.HughesList hiding ( (++) ) +import SSM.Core.Syntax +import SSM.Util.HughesList hiding ( (++) ) -import Test.SSM.QuickCheck.Util +import Test.SSM.QuickCheck.Util -import Data.List +import Data.List {- | Shrink fork statements in a program. Each resulting program contains only one mutation. -} @@ -23,7 +24,8 @@ shrinkForksProcedure p = sublists of length @length procs - 1@. -} shrinkForkStm :: Stm -> [Stm] shrinkForkStm stm = case stm of - Fork procs -> let sublists = map (\f -> delete f procs) procs - nonemptysublists = filter (not . null) sublists - in map Fork nonemptysublists + Fork procs -> + let sublists = map (\f -> delete f procs) procs + nonemptysublists = filter (not . null) sublists + in map Fork nonemptysublists _ -> [] diff --git a/test/lib/Test/SSM/QuickCheck/Shrink/References.hs b/test/lib/Test/SSM/QuickCheck/Shrink/References.hs index 95190874..6f70666d 100644 --- a/test/lib/Test/SSM/QuickCheck/Shrink/References.hs +++ b/test/lib/Test/SSM/QuickCheck/Shrink/References.hs @@ -35,7 +35,7 @@ allRefs p = refs $ body p where refs :: [Stm] -> [Reference] refs xs = concat $ for xs $ \x -> case x of - NewRef n t e -> [makeDynamicRef n t] + CreateRef n t -> [makeDynamicRef n t] If _ thn els -> refs thn ++ refs els While _ bdy -> refs bdy _ -> [] diff --git a/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs index a167107b..4e696dcc 100644 --- a/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs +++ b/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs @@ -1,10 +1,11 @@ module Test.SSM.QuickCheck.Shrink.Statements - ( statements ) where + ( statements + ) where -import SSM.Core.Syntax -import SSM.Util.HughesList hiding ( (++) ) +import SSM.Core.Syntax +import SSM.Util.HughesList hiding ( (++) ) -import Test.SSM.QuickCheck.Util +import Test.SSM.QuickCheck.Util statements :: Program -> [Program] statements = transformProcedures shrinkAllStmtsProcedure @@ -13,14 +14,33 @@ statements = transformProcedures shrinkAllStmtsProcedure -- statements. shrinkAllStmtsProcedure :: Procedure -> [Procedure] shrinkAllStmtsProcedure p = - [ p { body = body' } | body' <- distributeMutate (body p) shrinkStmts ] + [ p { body = (removeLonelyYield body') } + | body' <- shrinkStmts (emptyHughes, (body p)) + ] --- | Replace any of the below statements with a skip instruction -shrinkStmts :: Stm -> [Stm] -shrinkStmts stm = case stm of - SetRef _ _ -> [Skip] - SetLocal _ _ _ -> [Skip] - After _ _ _ -> [Skip] - Wait _ -> [Skip] - Fork _ -> [Skip] - _ -> [] +{- | This function will take a procedure body and shrink it by removing those statements +whose type is something like `SSM ()` -- those statement you can delete without making +the remainder of the program fail typechecking. + +We do need to pay some consideration when deleting `SSM.Core.Syntax.Stm.SetRef`. If we +blindly try to delete all of these, we will run into some errors. The +`SSM.Frontend.Language.var` function will boil down to a `SSM.Core.Syntax.Stm.CreateRef` +followed by a `SSM.Core.Syntax.Stm.SetRef`. If we remove that `SetRef`, we will have +an uninitialized value, which can lead to undefined behaviour. + +What this function does is that it returns mutations where all `SetRef`s are subject +to removal, except if that `SetRef` is preceeded by a corresponding `CreateRef`. In that +case we just leave it untouched. +-} +shrinkStmts :: (Hughes Stm, [Stm]) -> [[Stm]] +shrinkStmts (_, []) = [] +shrinkStmts (front, (stm1@(CreateRef r1 t) : stm2@(SetRef r2 e) : xs)) = + if r1 == refIdent r2 + then shrinkStmts (snoc (snoc front stm1) stm2, xs) + else shrinkStmts (snoc front stm1, stm2 : xs) +shrinkStmts (front, (x : xs)) = case x of + SetLocal _ _ _ -> (fromHughes front ++ xs) : shrinkStmts (snoc front x, xs) + SetRef _ _ -> (fromHughes front ++ xs) : shrinkStmts (snoc front x, xs) + After _ _ _ -> (fromHughes front ++ xs) : shrinkStmts (snoc front x, xs) + Fork _ -> (fromHughes front ++ xs) : shrinkStmts (snoc front x, xs) + _ -> shrinkStmts (snoc front x, xs) diff --git a/test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs index fa250693..68805aab 100644 --- a/test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs +++ b/test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs @@ -1,14 +1,13 @@ module Test.SSM.QuickCheck.Shrink.Wait - ( waits ) where + ( waits + ) where -import SSM.Core.Syntax -import SSM.Util.HughesList hiding ( (++) ) +import SSM.Core.Syntax +import SSM.Util.HughesList hiding ( (++) ) -import Test.SSM.QuickCheck.Util +import Test.SSM.QuickCheck.Util -import Data.List - -import Debug.Trace +import Data.List {- | Shrinks a program into several sub programs by making every wait statement one reference smaller, if the wait statement has more than 1 reference. -} @@ -17,11 +16,153 @@ waits = transformProcedures shrinkWaitProcedure shrinkWaitProcedure :: Procedure -> [Procedure] shrinkWaitProcedure p = - [ p { body = body' } | body' <- distributeMutate (body p) shrinkWaits ] - -shrinkWaits :: Stm -> [Stm] -shrinkWaits stm = case stm of - Wait refs -> let sublists = map (\r -> delete r refs) refs - nonemptysublists = filter (not . null) sublists - in map Wait nonemptysublists - _ -> [] + [ p { body = body' } | body' <- shrinkWaits (emptyHughes, (body p)) ] + +{- | Takes the body of a procedure and returns all variants of that body where each +variant contains a shrunken wait statement. -} +shrinkWaits :: (Hughes Stm, [Stm]) -> [[Stm]] +shrinkWaits (_, []) = [] +shrinkWaits (front, If c thn els : xs) = + let + front' = fromHughes front + thns = + [ front' ++ (If c thn' els : xs) + | thn' <- shrinkWaits (emptyHughes, thn) + ] + elss = + [ front' ++ (If c thn els' : xs) + | els' <- shrinkWaits (emptyHughes, els) + ] + in + thns ++ elss ++ shrinkWaits (snoc front (If c thn els), xs) +shrinkWaits (front, While c bdy : xs) = + let front' = fromHughes front + curr = + [ front' ++ (While c bdy' : xs) + | bdy' <- shrinkWaits (emptyHughes, bdy) + ] + in curr ++ shrinkWaits (snoc front (While c bdy), xs) +shrinkWaits (front, x : xs) = case isWait (x : xs) of + Just (waitstm, rest) -> + let front' = fromHughes front + curr = + (front' ++ rest) + : [ front' ++ waitstm' ++ rest + | waitstm' <- removeOneSensitizepair waitstm + ] + in curr ++ shrinkWaits (front <> toHughes waitstm, rest) + Nothing -> shrinkWaits (snoc front x, xs) + +{- | The input is a wait statement, in the form of a sequence of constituent statements. +Wait statement = [... sensitize statements ... yield ... desensitize statements ...]. +Returns all variants of this wait statement where one reference has been removed in each +variant. + +@ +> removeOneSensitizePair [ Sensitize r1 + , Sensitize r2 + , Sensitize r3 + , Yield + , Desensitize r1 + , Desensitize r2 + , Desensitize r3 + ] +[ Sensitize r2 +, Sensitize r3 +, Yield +, Desensitize r2 +, Desensitize r3 +] +: +[ Sensitize r1 +, Sensitize r3 +, Yield +, Desensitize r1 +, Desensitize r3 +] +: +[ Sensitize r1 +, Sensitize r2 +, Yield +, Desensitize r1 +, Desensitize r2 +] +: +[] +@ +-} +removeOneSensitizepair :: [Stm] -> [[Stm]] +removeOneSensitizepair [] = [] +removeOneSensitizepair (x : xs) = case x of + Sensitize _ -> + let (sensitizes, (yield : desensitizes)) = + takeWhileAndRest isSensitize (x : xs) + in if length sensitizes == 1 + then [] + else if isYield yield + then + [ sensitizes' ++ [yield] ++ desensitizes' + | (sensitizes', desensitizes') <- removeAllIths + sensitizes + desensitizes + ] + else [] + If c thn els -> undefined + While c bdy -> undefined + _ -> undefined + where + -- | Get the @Reference@ out of a @Sensitize@ or @Desensitize@-statement. + stmRef :: Stm -> Reference + stmRef (Sensitize r) = r + stmRef (Desensitize r) = r + stmRef _ = error "shrinking error - wait" + + {- | Returns all sublists acquired by removing all pairwise elements. + + @ + > removeAllIths [1,2,3] [4,5,6] + ([2,3],[5,6]) : ([1,3],[4,6]) : ([2,3],[5,6]) : [] + @ + -} + removeAllIths :: [a] -> [b] -> [([a], [b])] + removeAllIths xs ys = go [] [] xs ys + where + go _ _ [] _ = [] + go _ _ _ [] = [] + go hx hy (x : xs) (y : ys) = + (hx ++ xs, hy ++ ys) : go (hx ++ [x]) (hy ++ [y]) xs ys + +{- | If the sequence of statements begin with a wait statement (which is made up of some +sensitize statements, a yield statement and a corresponding number of desensitize +statements), return @Just (the wait statement, the rest of the statements)@, and +otherwise returns @Nothing@. + +@ +> isWait [Sensitize r, Yield, Desensitize r, stm1, stm2, ...] +Just ([Sensitize r, Yield, Desensitize], [stm1, stm2, ...]) +@ +-} +isWait :: [Stm] -> Maybe ([Stm], [Stm]) +isWait stmts = if isSensitize $ head stmts + then + let (sensitizes , (x : xs)) = takeWhileAndRest isSensitize stmts + (desensitizes, rest ) = takeWhileAndRest isDesensitize xs + in if isYield x && length sensitizes == length desensitizes + then Just (sensitizes ++ [x] ++ desensitizes, rest) + else Nothing + else Nothing + +-- | Is the statement a @Sensitize@ statement? +isSensitize :: Stm -> Bool +isSensitize (Sensitize _) = True +isSensitize _ = False + +-- | Is the statement a @Desensitize@ statement? +isDesensitize :: Stm -> Bool +isDesensitize (Desensitize _) = True +isDesensitize _ = False + +-- | Is the statement a @Yield@ statement? +isYield :: Stm -> Bool +isYield Yield = True +isYield _ = False diff --git a/test/lib/Test/SSM/QuickCheck/Util.hs b/test/lib/Test/SSM/QuickCheck/Util.hs index 1638f652..7f761a1b 100644 --- a/test/lib/Test/SSM/QuickCheck/Util.hs +++ b/test/lib/Test/SSM/QuickCheck/Util.hs @@ -6,14 +6,16 @@ module Test.SSM.QuickCheck.Util , distributeMutate , for , removeNth + , takeWhileAndRest , filterWith , removeVars + , removeLonelyYield ) where -import SSM.Core.Syntax -import SSM.Util.HughesList hiding ( (++) ) +import SSM.Core.Syntax +import SSM.Util.HughesList hiding ( (++) ) -import qualified Data.Map as Map +import qualified Data.Map as Map {- | This function takes a function that returns a list of shrunk `Procedure`s, and applies it to all procedures in the `Program`. For each new mutated procedure, a @@ -22,10 +24,11 @@ new program is produced. In each new `Program`, only one procedure has been muta Example: You have a program with 5 procedures and they can all be shrunk twice each. The result of calling @transformProcedures@ will be a list of 10 new programs. -} transformProcedures :: (Procedure -> [Procedure]) -> Program -> [Program] -transformProcedures tr prg = [ prg { funs = Map.insert n fun' (funs prg) } - | (n,fun) <- Map.toList (funs prg) - , fun' <- tr fun - ] +transformProcedures tr prg = + [ prg { funs = Map.insert n fun' (funs prg) } + | (n, fun) <- Map.toList (funs prg) + , fun' <- tr fun + ] {- | Distribute a mutation function over a list of elements. @@ -36,10 +39,10 @@ Example: distributeMutate :: forall a . [a] -> (a -> [a]) -> [[a]] distributeMutate xs f = map fromHughes $ go (emptyHughes, xs) where - go :: (Hughes a, [a]) -> [Hughes a] - go (_, []) = [] - go (current, (y:ys)) = [ current <> (cons_ y' ys) | y' <- f y ] ++ - go (snoc current y, ys) + go :: (Hughes a, [a]) -> [Hughes a] + go (_, []) = [] + go (current, (y : ys)) = + [ current <> (cons_ y' ys) | y' <- f y ] ++ go (snoc current y, ys) {- | Flip the arguments to map - in some cases it's a bit nicer on the eyes. Especially in the function is more than a few characters big. -} @@ -48,19 +51,18 @@ for = flip map -- | Remove the n:th element from a list, with the first element being indexed as 0. removeNth :: Show a => Int -> [a] -> [a] -removeNth 0 (_:xs) = xs -removeNth n (x:xs) = x : removeNth (n-1) xs -removeNth _ [] = error "can not remove from empty list" +removeNth 0 (_ : xs) = xs +removeNth n (x : xs) = x : removeNth (n - 1) xs +removeNth _ [] = error "can not remove from empty list" -- | Like normal filter, but applies a function to the filtered elements filterWith :: (a -> Bool) -> (a -> b) -> [a] -> [b] -filterWith _ _ [] = [] -filterWith pred f (x:xs) = - if pred x - then f x : filterWith pred f xs - else filterWith pred f xs - +filterWith _ _ [] = [] +filterWith pred f (x : xs) = + if pred x then f x : filterWith pred f xs else filterWith pred f xs +takeWhileAndRest :: (a -> Bool) -> [a] -> ([a], [a]) +takeWhileAndRest pred xs = (takeWhile pred xs, dropWhile pred xs) {- | Shrinks a sequence of statements by removing declarations. The first argument list contains variable names that should be removed. If a `NewRef` or `GetRef` constructor @@ -70,135 +72,178 @@ possible to use. -} removeVars :: [Ident] -> [Reference] -> [Stm] -> [Stm] -removeVars = go +removeVars invalid validrefs stmts = removeLonelyYield + $ go invalid validrefs stmts where - -- | Transforms a procedure body to contain no reference of the invalid identifiers - go :: [Ident] -- ^ Names of invalid identifiers - -> [Reference] -- ^ Names & Types of valid references - -> [Stm] -- ^ Statements to transform - -> [Stm] - go _ _ [] = [] - go invalid validrefs (x:xs) = case x of - - NewRef n t e -> - if n `elem` invalid - then Skip : go invalid validrefs xs - else NewRef n t (rewriteExp e invalid validrefs) : - go invalid (makeDynamicRef n t:validrefs) xs - - SetRef r e -> - if not $ r `elem` validrefs - then Skip : go invalid validrefs xs - else SetRef r (rewriteExp e invalid validrefs) : - go invalid validrefs xs - - SetLocal n t e -> - if n `elem` invalid - then Skip : go invalid validrefs xs - else SetLocal n t (rewriteExp e invalid validrefs) : - go invalid validrefs xs - - If c thn els -> + -- | Transforms a procedure body to contain no reference of the invalid identifiers + go + :: [Ident] -- ^ Names of invalid identifiers + -> [Reference] -- ^ Names & Types of valid references + -> [Stm] -- ^ Statements to transform + -> [Stm] + go _ _ [] = [] + go invalid validrefs (x : xs) = case x of + CreateRef n t -> if n `elem` invalid + then Skip : go invalid validrefs xs + else x : go invalid (makeDynamicRef n t : validrefs) xs + + SetRef r e -> if not $ r `elem` validrefs + then Skip : go invalid validrefs xs + else + SetRef r (rewriteExp e invalid validrefs) + : go invalid validrefs xs + + SetLocal n t e -> if n `elem` invalid + then Skip : go invalid validrefs xs + else + SetLocal n t (rewriteExp e invalid validrefs) + : go invalid validrefs xs + + If c thn els -> let thn' = go invalid validrefs thn els' = go invalid validrefs els - in If (rewriteExp c invalid validrefs) thn' els' : - go invalid validrefs xs + in If (rewriteExp c invalid validrefs) thn' els' + : go invalid validrefs xs - While c bdy -> + While c bdy -> let bdy' = go invalid validrefs bdy - in While (rewriteExp c invalid validrefs) bdy' : - go invalid validrefs xs - - Skip -> Skip : go invalid validrefs xs - - After d r v -> - if not $ r `elem` validrefs - then Skip : go invalid validrefs xs - else After (rewriteDelay d invalid validrefs) - r - (rewriteExp v invalid validrefs) : - go invalid validrefs xs - - Wait refs -> - let refs' = filter (`elem` validrefs) refs - in if null refs' - then Skip : go invalid validrefs xs - else Wait refs' : go invalid validrefs xs - - Fork procs -> - let procs' = concat $ for procs $ \(n,args) -> - case rewriteCall args invalid validrefs of - Just args' -> [(n, args')] - Nothing -> [] - in if null procs' - then Skip : go invalid validrefs xs - else Fork procs' : go invalid validrefs xs - - {- | Rewrite an expression by replacing invalid expressions with fresh literals - and my replacing invalid references with a `True` literal. -} - rewriteExp :: SSMExp -> [Ident] -> [Reference] -> SSMExp - rewriteExp e invalid validrefs = case e of - Var t n -> if n `elem` invalid - then defaultExp t - else Var t n - Lit t l -> Lit t l - UOpE t e op -> case op of - Neg -> UOpE t (rewriteExp e invalid validrefs) Neg - UOpR t r op -> case op of - Changed -> if r `elem` validrefs - then UOpR t r Changed - else Lit TBool (LBool True) - Deref -> if r `elem` validrefs - then UOpR t r Deref - else defaultExp t - BOp t e1 e2 op -> - BOp t - (rewriteExp e1 invalid validrefs) - (rewriteExp e2 invalid validrefs) - op - - -- | Rewrite an SSMTime expression - rewriteDelay :: SSMTime -> [Ident] -> [Reference] -> SSMTime - rewriteDelay d invalid validrefs = case d of - SSMTime del units -> SSMTime (rewriteExp del invalid validrefs) units - SSMTimeAdd t1 t2 -> SSMTimeAdd (rewriteDelay t1 invalid validrefs) - (rewriteDelay t2 invalid validrefs) - SSMTimeSub t1 t2 -> SSMTimeSub (rewriteDelay t1 invalid validrefs) - (rewriteDelay t2 invalid validrefs) - - -- | Default literal of expressions - defaultExp :: Type -> SSMExp - defaultExp TInt32 = Lit TInt32 (LInt32 1) - defaultExp TInt64 = Lit TInt64 (LInt64 1) - defaultExp TUInt8 = Lit TUInt8 (LUInt8 1) - defaultExp TUInt64 = Lit TUInt64 (LUInt64 1) - defaultExp TBool = Lit TBool (LBool True) - defaultExp TEvent = Lit TEvent LEvent - defaultExp (Ref _) = error "can not work on reference types" - - {- | Try to rewrite the arguments to a procedure call. If there's a reference - that's no longer valid that can't be replaced with a reference of the same type, - that specific procedure call can't be left in the program. -} - rewriteCall :: [Either SSMExp Reference] - -> [Ident] - -> [Reference] - -> Maybe [Either SSMExp Reference] - rewriteCall [] _ _ = Just [] - - rewriteCall (Left e:xs) invalid validrefs = do - xs' <- rewriteCall xs invalid validrefs - return $ Left (rewriteExp e invalid validrefs) : xs' - - rewriteCall (Right r:xs) invalid validrefs = do - xs' <- rewriteCall xs invalid validrefs - if r `elem` validrefs - then return $ Right r : xs' - else do r' <- replacementRef r validrefs - return $ Right r' : xs' - - {- | If there's a ref of the same type in scope, return one of them. Otherwise, + in While (rewriteExp c invalid validrefs) bdy' + : go invalid validrefs xs + + Skip -> Skip : go invalid validrefs xs + + After d r v -> if not $ r `elem` validrefs + then Skip : go invalid validrefs xs + else + After (rewriteDelay d invalid validrefs) + r + (rewriteExp v invalid validrefs) + : go invalid validrefs xs + + Sensitize ref -> if refIdent ref `elem` invalid + then Skip : go invalid validrefs xs + else Sensitize ref : go invalid validrefs xs + + Desensitize ref -> if refIdent ref `elem` invalid + then Skip : go invalid validrefs xs + else Desensitize ref : go invalid validrefs xs + + Yield -> Yield : go invalid validrefs xs + + Fork procs -> + let procs' = concat $ for procs $ \(n, args) -> + case rewriteCall args invalid validrefs of + Just args' -> [(n, args')] + Nothing -> [] + in if null procs' + then Skip : go invalid validrefs xs + else Fork procs' : go invalid validrefs xs + + {- | Rewrite an expression by replacing invalid expressions with fresh literals + and my replacing invalid references with a `True` literal. -} + rewriteExp :: SSMExp -> [Ident] -> [Reference] -> SSMExp + rewriteExp e invalid validrefs = case e of + Var t n -> if n `elem` invalid + then defaultExp t + else Var t n + Lit t l -> Lit t l + UOpE t e op -> case op of + Neg -> UOpE t (rewriteExp e invalid validrefs) Neg + UOpR t r op -> case op of + Changed -> if r `elem` validrefs + then UOpR t r Changed + else Lit TBool (LBool True) + Deref -> if r `elem` validrefs + then UOpR t r Deref + else defaultExp t + BOp t e1 e2 op -> + BOp t + (rewriteExp e1 invalid validrefs) + (rewriteExp e2 invalid validrefs) + op + + -- | Rewrite an SSMTime expression + rewriteDelay :: SSMTime -> [Ident] -> [Reference] -> SSMTime + rewriteDelay d invalid validrefs = case d of + SSMTime del units -> SSMTime (rewriteExp del invalid validrefs) units + SSMTimeAdd t1 t2 -> SSMTimeAdd (rewriteDelay t1 invalid validrefs) + (rewriteDelay t2 invalid validrefs) + SSMTimeSub t1 t2 -> SSMTimeSub (rewriteDelay t1 invalid validrefs) + (rewriteDelay t2 invalid validrefs) + + -- | Default literal of expressions + defaultExp :: Type -> SSMExp + defaultExp TInt32 = Lit TInt32 (LInt32 1) + defaultExp TInt64 = Lit TInt64 (LInt64 1) + defaultExp TUInt8 = Lit TUInt8 (LUInt8 1) + defaultExp TUInt64 = Lit TUInt64 (LUInt64 1) + defaultExp TBool = Lit TBool (LBool True) + defaultExp TEvent = Lit TEvent LEvent + defaultExp (Ref _) = error "can not work on reference types" + + {- | Try to rewrite the arguments to a procedure call. If there's a reference + that's no longer valid that can't be replaced with a reference of the same type, + that specific procedure call can't be left in the program. -} + rewriteCall + :: [Either SSMExp Reference] + -> [Ident] + -> [Reference] + -> Maybe [Either SSMExp Reference] + rewriteCall [] _ _ = Just [] + + rewriteCall (Left e : xs) invalid validrefs = do + xs' <- rewriteCall xs invalid validrefs + return $ Left (rewriteExp e invalid validrefs) : xs' + + rewriteCall (Right r : xs) invalid validrefs = do + xs' <- rewriteCall xs invalid validrefs + if r `elem` validrefs + then return $ Right r : xs' + else do + r' <- replacementRef r validrefs + return $ Right r' : xs' + + {- | If there's a ref of the same type in scope, return one of them. Otherwise, return Nothing. -} - replacementRef :: Reference -> [Reference] -> Maybe Reference - replacementRef r refs = - let refs' = filter (\r' -> refType r == refType r') refs - in if null refs' then Nothing else Just (head refs') + replacementRef :: Reference -> [Reference] -> Maybe Reference + replacementRef r refs = + let refs' = filter (\r' -> refType r == refType r') refs + in if null refs' then Nothing else Just (head refs') + +{- | While `removeVars` is a very helpful utility function, it does have to property of +leaving unsound programs. If we consider the folowing application: + +@ +> removeVars [r1] [] [ CreateRef r2 Bool + , SetRef r2 False + , Sensitize r1 + , Yield + , Desensitize r1 + , SetRef r2 True + ] +[ CreateRef r2 Bool +, SetRef r2 False +, Yield +, SetRef r2 True +] +@ + +When we are traversing the statements and removing @Sensitize@ and @Desensitize@, we +don't know at that point that there's a wild @Yield@ remaining, that actually belonged +to these statements. This function is intended to traverse the statements and remove any +solo @Yield@ statements. A @Yield@ statement is retained if it follows after a @Fork@ +statement or a @Sensitize@ statement. Otherwise, it is assumed to be a leftover from +deleting other related stuff. +-} +removeLonelyYield :: [Stm] -> [Stm] +removeLonelyYield [] = [] +removeLonelyYield (Fork procs : Yield : xs) = + Fork procs : Yield : removeLonelyYield xs +removeLonelyYield (Sensitize r : Yield : xs) = + Sensitize r : Yield : removeLonelyYield xs +removeLonelyYield (If x thn els : xs) = + If x (removeLonelyYield thn) (removeLonelyYield els) : removeLonelyYield xs +removeLonelyYield (While c bdy : xs) = + While c (removeLonelyYield bdy) : removeLonelyYield xs +removeLonelyYield (Yield : xs) = removeLonelyYield xs +removeLonelyYield (x : xs) = x : removeLonelyYield xs diff --git a/test/regression-low/Regression/CancelBothSpec.hs b/test/regression-low/Regression/CancelBothSpec.hs index 05b0f138..ba2ef4ab 100644 --- a/test/regression-low/Regression/CancelBothSpec.hs +++ b/test/regression-low/Regression/CancelBothSpec.hs @@ -20,13 +20,13 @@ p = Program { name = Ident "fun0" Nothing , arguments = [] , body = - [ NewRef (Ident "v0" Nothing) TBool (Lit TBool (LBool False)) + [ CreateRef (Ident "v0" Nothing) (Ref TBool) + , SetRef (Dynamic (Ident "v0" Nothing, Ref TBool)) (Lit TBool (LBool False)) , After (SSMTime (Lit TUInt64 (LUInt64 1)) SSMNanosecond) (Dynamic (Ident "v0" Nothing, Ref TBool)) (Lit TBool (LBool True)) - , NewRef (Ident "v1" Nothing) - TBool - (UOpR TBool (Dynamic (Ident "v0" Nothing, Ref TBool)) Changed) + , CreateRef (Ident "v1" Nothing) (Ref TBool) + , SetRef (Dynamic (Ident "v1" Nothing, Ref TBool)) (UOpR TBool (Dynamic (Ident "v0" Nothing, Ref TBool)) Changed) , After (SSMTime (Lit TUInt64 (LUInt64 3872)) SSMNanosecond) (Dynamic (Ident "v1" Nothing, Ref TBool)) (Lit TBool (LBool False)) diff --git a/test/regression-low/Regression/CancelLaterSpec.hs b/test/regression-low/Regression/CancelLaterSpec.hs index edb3b74b..8964fb08 100644 --- a/test/regression-low/Regression/CancelLaterSpec.hs +++ b/test/regression-low/Regression/CancelLaterSpec.hs @@ -15,9 +15,8 @@ p = Program , Procedure { name = Ident "fun0" Nothing , arguments = [] - , body = [ NewRef (Ident "v0" Nothing) - TInt32 - (Lit TInt32 (LInt32 0)) + , body = [ CreateRef (Ident "v0" Nothing) (Ref TInt32) + , SetRef (Dynamic (Ident "v0" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 0)) , After (SSMTime (Lit TUInt64 (LUInt64 2)) SSMNanosecond) (Dynamic (Ident "v0" Nothing, Ref TInt32)) diff --git a/test/regression-low/Regression/FiveForkerSpec.hs b/test/regression-low/Regression/FiveForkerSpec.hs index 11f14f72..ab24b6f2 100644 --- a/test/regression-low/Regression/FiveForkerSpec.hs +++ b/test/regression-low/Regression/FiveForkerSpec.hs @@ -19,9 +19,12 @@ p = Program { name = Ident "fun0" Nothing , arguments = [] , body = - [ NewRef (Ident "ref1" Nothing) TInt32 (Lit TInt32 (LInt32 0)) - , NewRef (Ident "ref2" Nothing) TUInt64 (Lit TUInt64 (LUInt64 0)) - , NewRef (Ident "ref4" Nothing) TUInt64 (Lit TUInt64 (LUInt64 0)) + [ CreateRef (Ident "ref1" Nothing) (Ref TInt32) + , SetRef (Dynamic (Ident "ref1" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 0)) + , CreateRef (Ident "ref2" Nothing) (Ref TUInt64) + , SetRef (Dynamic (Ident "ref2" Nothing, Ref TUInt64)) (Lit TUInt64 (LUInt64 0)) + , CreateRef (Ident "ref4" Nothing) (Ref TUInt64) + , SetRef (Dynamic (Ident "ref4" Nothing, Ref TUInt64)) (Lit TUInt64 (LUInt64 0)) , Fork [ ( Ident "fun5" Nothing , [ Right (Dynamic (Ident "ref1" Nothing, Ref TInt32)) @@ -48,6 +51,7 @@ p = Program ] ) ] + , Yield ] } ) @@ -145,6 +149,7 @@ p = Program ) , (Ident "fun2" Nothing, []) ] + , Yield , Fork [ (Ident "fun2" Nothing, []) , ( Ident "fun5" Nothing @@ -231,6 +236,7 @@ p = Program ) , (Ident "fun2" Nothing, []) ] + , Yield , If (BOp TBool (Var TInt32 (Ident "var7" Nothing)) (Var TInt32 (Ident "var7" Nothing)) OLT) [ After @@ -311,6 +317,7 @@ p = Program , (Ident "fun2" Nothing, []) , (Ident "fun2" Nothing, []) ] + , Yield ] [ Fork [ (Ident "fun2" Nothing, []) @@ -374,8 +381,11 @@ p = Program , (Ident "fun2" Nothing, []) , (Ident "fun2" Nothing, []) ] + , Yield ] - , Wait [Dynamic (Ident "ref1" Nothing, Ref TInt32), Dynamic (Ident "ref2" Nothing, Ref TUInt64)] + , Sensitize (Dynamic (Ident "ref1" Nothing, Ref TInt32)) + , Yield + , Desensitize (Dynamic (Ident "ref1" Nothing, Ref TInt32)) ] [ Fork [ ( Ident "fun5" Nothing @@ -454,6 +464,7 @@ p = Program ] ) ] + , Yield , Fork [ ( Ident "fun5" Nothing , [ Right (Dynamic (Ident "ref1" Nothing, Ref TInt32)) @@ -571,14 +582,23 @@ p = Program , (Ident "fun2" Nothing, []) , (Ident "fun2" Nothing, []) ] + , Yield ] - , Wait [Dynamic (Ident "ref2" Nothing, Ref TUInt64)] - , Wait [Dynamic (Ident "ref1" Nothing, Ref TInt32)] + , Sensitize (Dynamic (Ident "ref2" Nothing, Ref TUInt64)) + , Yield + , Desensitize (Dynamic (Ident "ref2" Nothing, Ref TUInt64)) + , Sensitize (Dynamic (Ident "ref1" Nothing, Ref TInt32)) + , Yield + , Desensitize (Dynamic (Ident "ref1" Nothing, Ref TInt32)) , After (SSMTime (Lit TUInt64 (LUInt64 3525)) SSMNanosecond) (Dynamic (Ident "ref2" Nothing, Ref TUInt64)) (Lit TUInt64 (LUInt64 167)) - , Wait [(Dynamic (Ident "ref1" Nothing, Ref TInt32))] - , Wait [(Dynamic (Ident "ref4" Nothing, Ref TUInt64))] + , Sensitize (Dynamic (Ident "ref1" Nothing, Ref TInt32)) + , Yield + , Desensitize (Dynamic (Ident "ref1" Nothing, Ref TInt32)) + , Sensitize (Dynamic (Ident "ref4" Nothing, Ref TUInt64)) + , Yield + , Desensitize (Dynamic (Ident "ref4" Nothing, Ref TUInt64)) , After (SSMTime (Lit TUInt64 (LUInt64 4696)) SSMNanosecond) (Dynamic (Ident "ref2" Nothing, Ref TUInt64)) @@ -597,7 +617,9 @@ p = Program OMinus ) , Fork [(Ident "fun2" Nothing, [])] + , Yield , Fork [(Ident "fun2" Nothing, [])] + , Yield ] } ) diff --git a/test/regression-low/Regression/FlipFlopLoopSpec.hs b/test/regression-low/Regression/FlipFlopLoopSpec.hs index 7f08d359..70f13f4e 100644 --- a/test/regression-low/Regression/FlipFlopLoopSpec.hs +++ b/test/regression-low/Regression/FlipFlopLoopSpec.hs @@ -10,6 +10,8 @@ import qualified Test.Hspec.QuickCheck as H import qualified Test.SSM.Prop as T import SSM.Compile +import SSM.Interpret +import SSM.Util.Default p :: Program p = Program @@ -19,8 +21,10 @@ p = Program , Procedure { name = Ident "fun0" Nothing , arguments = [] - , body = [ NewRef (Ident "ref2" Nothing) TBool (Lit TBool (LBool True)) + , body = [ CreateRef (Ident "ref2" Nothing) (Ref TBool) + , SetRef (Dynamic (Ident "ref2" Nothing, Ref TBool)) (Lit TBool (LBool True)) , Fork [(Ident "fun1" Nothing, [Right (Dynamic (Ident "ref2" Nothing, Ref TBool))])] + , Yield ] } ) @@ -34,12 +38,16 @@ p = Program SSMNanosecond) (Dynamic (Ident "ref2" Nothing, Ref TBool)) (Lit TBool (LBool False)) - , Wait [Dynamic (Ident "ref2" Nothing, Ref TBool)] + , Sensitize (Dynamic (Ident "ref2" Nothing, Ref TBool)) + , Yield + , Desensitize (Dynamic (Ident "ref2" Nothing, Ref TBool)) , After (SSMTime (Lit TUInt64 (LUInt64 2)) SSMNanosecond) (Dynamic (Ident "ref2" Nothing, Ref TBool)) (Lit TBool (LBool True)) - , Wait [Dynamic (Ident "ref2" Nothing, Ref TBool)] + , Sensitize (Dynamic (Ident "ref2" Nothing, Ref TBool)) + , Yield + , Desensitize (Dynamic (Ident "ref2" Nothing, Ref TBool)) ] ] } diff --git a/test/regression-low/Regression/LaterAssignOverwriteSpec.hs b/test/regression-low/Regression/LaterAssignOverwriteSpec.hs index 60a2d6cc..fd22469e 100644 --- a/test/regression-low/Regression/LaterAssignOverwriteSpec.hs +++ b/test/regression-low/Regression/LaterAssignOverwriteSpec.hs @@ -24,10 +24,13 @@ p = Program { name = Ident "fun0" Nothing , arguments = [] , body = - [ NewRef (Ident "ref1" Nothing) TBool (Lit TBool (LBool True)) - , NewRef (Ident "ref3" Nothing) TInt32 (Lit TInt32 (LInt32 0)) + [ CreateRef (Ident "ref1" Nothing) (Ref TBool) + , SetRef (Dynamic (Ident "ref1" Nothing, Ref TBool)) (Lit TBool (LBool True)) + , CreateRef (Ident "ref3" Nothing) (Ref TInt32) + , SetRef (Dynamic (Ident "ref3" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 0)) , Fork [(Ident "fun1" Nothing, [Right (Dynamic (Ident "ref1" Nothing, Ref TBool)), Right (Dynamic (Ident "ref3" Nothing, Ref TInt32))])] + , Yield ] } ) @@ -44,8 +47,12 @@ p = Program (Dynamic (Ident "ref3" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 3)) , SetRef (Dynamic (Ident "ref3" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 4)) - , Wait [Dynamic (Ident "ref1" Nothing, Ref TBool)] - , Wait [Dynamic (Ident "ref3" Nothing, Ref TInt32)] + , Sensitize (Dynamic (Ident "ref1" Nothing, Ref TBool)) + , Yield + , Desensitize (Dynamic (Ident "ref1" Nothing, Ref TBool)) + , Sensitize (Dynamic (Ident "ref3" Nothing, Ref TInt32)) + , Yield + , Desensitize (Dynamic (Ident "ref3" Nothing, Ref TInt32)) ] } ) diff --git a/test/regression-low/Regression/LaterWaitSpec.hs b/test/regression-low/Regression/LaterWaitSpec.hs index 9bfdd9fa..2276a04e 100644 --- a/test/regression-low/Regression/LaterWaitSpec.hs +++ b/test/regression-low/Regression/LaterWaitSpec.hs @@ -28,11 +28,14 @@ p = Program , Procedure { name = Ident "fun0" Nothing , arguments = [] - , body = [ NewRef (Ident "v0" Nothing) TInt32 (Lit TInt32 (LInt32 0)) + , body = [ CreateRef (Ident "v0" Nothing) (Ref TInt32) + , SetRef (Dynamic (Ident "v0" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 0)) , After (SSMTime (Lit TUInt64 (LUInt64 2)) SSMNanosecond) (Dynamic (Ident "v0" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 1)) - , Wait [Dynamic (Ident "v0" Nothing, Ref TInt32)] + , Sensitize (Dynamic (Ident "v0" Nothing, Ref TInt32)) + , Yield + , Desensitize (Dynamic (Ident "v0" Nothing, Ref TInt32)) ] } ) diff --git a/test/regression-low/Regression/ManyContsSpec.hs b/test/regression-low/Regression/ManyContsSpec.hs index a1477ef5..06d8ce1b 100644 --- a/test/regression-low/Regression/ManyContsSpec.hs +++ b/test/regression-low/Regression/ManyContsSpec.hs @@ -16,10 +16,10 @@ p = Program , Procedure { name = Ident "fun0" Nothing , arguments = [] - , body = [ NewRef (Ident "ref2" Nothing) - TUInt64 - (Lit TUInt64 (LUInt64 0)) + , body = [ CreateRef (Ident "ref2" Nothing) (Ref TUInt64) + , SetRef (Dynamic (Ident "ref2" Nothing, Ref TUInt64)) (Lit TUInt64 (LUInt64 0)) , Fork [(Ident "fun1" Nothing, [Right $ Dynamic (Ident "ref2" Nothing, Ref TUInt64)])] + , Yield ] } ) @@ -33,7 +33,9 @@ p = Program (SSMTime (Lit TUInt64 (LUInt64 2)) SSMNanosecond) (Dynamic (Ident "Ref2" Nothing, Ref TUInt64)) (Lit TUInt64 (LUInt64 2)) - , Wait [Dynamic (Ident "Ref2" Nothing, Ref TUInt64)] + , Sensitize (Dynamic (Ident "Ref2" Nothing, Ref TUInt64)) + , Yield + , Desensitize (Dynamic (Ident "Ref2" Nothing, Ref TUInt64)) , Fork [ ( Ident "fun1" Nothing , [ Right $ Dynamic (Ident "Ref2" Nothing, Ref TUInt64) @@ -48,6 +50,7 @@ p = Program ] ) ] + , Yield ] } ) diff --git a/test/regression-low/Regression/MultOverflowIndirectSpec.hs b/test/regression-low/Regression/MultOverflowIndirectSpec.hs index 1bbd9cf8..b7acacf3 100644 --- a/test/regression-low/Regression/MultOverflowIndirectSpec.hs +++ b/test/regression-low/Regression/MultOverflowIndirectSpec.hs @@ -19,9 +19,8 @@ p = Program { name = Ident "fun1" Nothing , arguments = [] , body = - [ NewRef ((Ident "v0" Nothing)) - TInt32 - (Lit TInt32 (LInt32 999999)) + [ CreateRef (Ident "v0" Nothing) (Ref TInt32) + , SetRef (Dynamic (Ident "v0" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 999999)) , If (BOp TBool @@ -34,8 +33,11 @@ p = Program (Lit TInt32 (LInt32 0)) ] [] - , NewRef (Ident "v3" Nothing) TInt32 (Lit TInt32 (LInt32 0)) - , Wait [Dynamic (Ident "v3" Nothing, Ref TInt32)] + , CreateRef (Ident "v3" Nothing) (Ref TInt32) + , SetRef (Dynamic (Ident "v3" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 0)) + , Sensitize (Dynamic (Ident "v3" Nothing, Ref TInt32)) + , Yield + , Desensitize (Dynamic (Ident "v3" Nothing, Ref TInt32)) ] } ) diff --git a/test/regression-low/Regression/MultOverflowSpec.hs b/test/regression-low/Regression/MultOverflowSpec.hs index 06a01330..c13351a5 100644 --- a/test/regression-low/Regression/MultOverflowSpec.hs +++ b/test/regression-low/Regression/MultOverflowSpec.hs @@ -19,7 +19,8 @@ p = Program { name = Ident "fun1" Nothing , arguments = [] , body = - [ NewRef ((Ident "v0" Nothing)) TInt32 (Lit TInt32 (LInt32 999999)) + [ CreateRef (Ident "v0" Nothing) (Ref TInt32) + , SetRef (Dynamic (Ident "v0" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 999999)) , If (BOp TBool (Lit TInt32 (LInt32 0)) @@ -34,7 +35,9 @@ p = Program (Dynamic ((Ident "v0" Nothing), Ref TInt32)) (Lit TInt32 (LInt32 1)) ] - , Wait [Dynamic ((Ident "v0" Nothing), Ref TInt32)] + , Sensitize (Dynamic (Ident "v0" Nothing, Ref TInt32)) + , Yield + , Desensitize (Dynamic (Ident "v0" Nothing, Ref TInt32)) ] } ) diff --git a/test/regression-low/Regression/RecurseExhaustDepthSpec.hs b/test/regression-low/Regression/RecurseExhaustDepthSpec.hs index 97f2cd66..15ea4c63 100644 --- a/test/regression-low/Regression/RecurseExhaustDepthSpec.hs +++ b/test/regression-low/Regression/RecurseExhaustDepthSpec.hs @@ -14,7 +14,7 @@ p = Program [ ( Ident "fun0" Nothing , Procedure { name = Ident "fun0" Nothing , arguments = [] - , body = [Fork [(Ident "fun0" Nothing, []), (Ident "fun1" Nothing, [])]] + , body = [Fork [(Ident "fun0" Nothing, []), (Ident "fun1" Nothing, [])], Yield] } ) , (Ident "fun1" Nothing, Procedure { name = Ident "fun1" Nothing, arguments = [], body = [] }) diff --git a/test/regression-low/Regression/RecurseForeverSpec.hs b/test/regression-low/Regression/RecurseForeverSpec.hs index 83a3d8fb..1e581b4c 100644 --- a/test/regression-low/Regression/RecurseForeverSpec.hs +++ b/test/regression-low/Regression/RecurseForeverSpec.hs @@ -18,7 +18,7 @@ p = Program , Procedure { name = Ident "fun0" Nothing , arguments = [] - , body = [ Fork [(Ident "fun0" Nothing, [])] ] + , body = [ Fork [(Ident "fun0" Nothing, [])], Yield ] } ) ]