From 704cf8dcb01f9c804feb74edea79c0c11ffb12e7 Mon Sep 17 00:00:00 2001 From: Robert Krook Date: Wed, 11 Aug 2021 12:06:31 +0200 Subject: [PATCH 01/10] remove NewRef in favor of CreateRef --- ssm.cabal | 3 +- ssm/SSM/Backend/C/CodeGen.hs | 23 +-- ssm/SSM/Core/Syntax.hs | 148 +++++++++--------- ssm/SSM/Frontend/Syntax.hs | 7 +- ssm/SSM/Interpret/Internal.hs | 23 ++- ssm/SSM/Interpret/Interpreter.hs | 7 +- ssm/SSM/Pretty/Syntax.hs | 12 +- test/lib/Test/SSM/QuickCheck/Generator.hs | 15 +- .../Test/SSM/QuickCheck/Shrink/Expressions.hs | 1 - .../Test/SSM/QuickCheck/Shrink/References.hs | 2 +- test/lib/Test/SSM/QuickCheck/Util.hs | 10 +- .../Regression/CancelBothSpec.hs | 10 +- .../Regression/CancelLaterSpec.hs | 5 +- .../Regression/FiveForkerSpec.hs | 9 +- .../Regression/FlipFlopLoopSpec.hs | 3 +- .../Regression/LaterAssignOverwriteSpec.hs | 6 +- .../Regression/LaterWaitSpec.hs | 6 + .../Regression/ManyContsSpec.hs | 5 +- .../Regression/MultOverflowIndirectSpec.hs | 8 +- .../Regression/MultOverflowSpec.hs | 3 +- 20 files changed, 169 insertions(+), 137 deletions(-) diff --git a/ssm.cabal b/ssm.cabal index 025e7c0b..ab1b2e18 100644 --- a/ssm.cabal +++ b/ssm.cabal @@ -4,7 +4,7 @@ cabal-version: 1.12 -- -- see: https://github.com/sol/hpack -- --- hash: a0f8bd48de2115636fda8c0f782dfcf3b71c53ec06ad80fd9bbef24a1a513322 +-- hash: 6573f29e908523f235835605a7bebd57b40eb94a62d4814901bb19aff3972368 name: ssm version: 0.1.0.0 @@ -47,7 +47,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/CodeGen.hs b/ssm/SSM/Backend/C/CodeGen.hs index 11ae8a29..41d74ae1 100644 --- a/ssm/SSM/Backend/C/CodeGen.hs +++ b/ssm/SSM/Backend/C/CodeGen.hs @@ -362,16 +362,19 @@ 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 (CreateRef n t) = do + addLocal $ makeDynamicRef n t + return [] +--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 diff --git a/ssm/SSM/Core/Syntax.hs b/ssm/SSM/Core/Syntax.hs index a6f32a23..30c4526e 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 @@ -114,7 +121,7 @@ data Type -- | 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 @@ -176,8 +183,8 @@ data Reference -- | 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 @@ -297,24 +304,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..8c5e9235 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" diff --git a/ssm/SSM/Interpret/Internal.hs b/ssm/SSM/Interpret/Internal.hs index 78d841cb..f6a26e3d 100644 --- a/ssm/SSM/Interpret/Internal.hs +++ b/ssm/SSM/Interpret/Internal.hs @@ -39,7 +39,7 @@ module SSM.Interpret.Internal , pushInstructions -- * Reference helpers - , newRef + , createRef , writeRef , writeLocal , readRef @@ -311,14 +311,21 @@ createVar e = do n <- getNow lift' $ newVar' v n -{- | Create a new reference with an initial value. +{- | 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. -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) } } +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: 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 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. diff --git a/ssm/SSM/Interpret/Interpreter.hs b/ssm/SSM/Interpret/Interpreter.hs index 5abe95a8..a950976b 100644 --- a/ssm/SSM/Interpret/Interpreter.hs +++ b/ssm/SSM/Interpret/Interpreter.hs @@ -100,9 +100,12 @@ step = do Nothing -> leave Just stm -> case stm of - NewRef n _ e -> do - newRef n e + CreateRef n t -> do + createRef n t continue +-- NewRef n _ e -> do +-- newRef n e +-- continue SetRef r e -> do writeRef r e diff --git a/ssm/SSM/Pretty/Syntax.hs b/ssm/SSM/Pretty/Syntax.hs index 2aa965b9..441a3084 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 ] diff --git a/test/lib/Test/SSM/QuickCheck/Generator.hs b/test/lib/Test/SSM/QuickCheck/Generator.hs index ccb6f075..e661b72b 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 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/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/Util.hs b/test/lib/Test/SSM/QuickCheck/Util.hs index 1638f652..b24987ef 100644 --- a/test/lib/Test/SSM/QuickCheck/Util.hs +++ b/test/lib/Test/SSM/QuickCheck/Util.hs @@ -73,18 +73,16 @@ removeVars :: [Ident] -> [Reference] -> [Stm] -> [Stm] removeVars = go where -- | Transforms a procedure body to contain no reference of the invalid identifiers - go :: [Ident] -- ^ Names of invalid identifiers + go :: [Ident] -- ^ Names of invalid identifiers -> [Reference] -- ^ Names & Types of valid references - -> [Stm] -- ^ Statements to transform + -> [Stm] -- ^ Statements to transform -> [Stm] go _ _ [] = [] go invalid validrefs (x:xs) = case x of - - NewRef n t e -> + CreateRef n t -> 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 + else x : go invalid (makeDynamicRef n t:validrefs) xs SetRef r e -> if not $ r `elem` validrefs diff --git a/test/regression-low/Regression/CancelBothSpec.hs b/test/regression-low/Regression/CancelBothSpec.hs index 05b0f138..91331afe 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)) - , After (SSMTime (Lit TUInt64 (LUInt64 1)) SSMNanosecond) + [ 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..21136d1d 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)) diff --git a/test/regression-low/Regression/FlipFlopLoopSpec.hs b/test/regression-low/Regression/FlipFlopLoopSpec.hs index 7f08d359..870e688b 100644 --- a/test/regression-low/Regression/FlipFlopLoopSpec.hs +++ b/test/regression-low/Regression/FlipFlopLoopSpec.hs @@ -19,7 +19,8 @@ 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))])] ] } diff --git a/test/regression-low/Regression/LaterAssignOverwriteSpec.hs b/test/regression-low/Regression/LaterAssignOverwriteSpec.hs index 60a2d6cc..9a0a70a5 100644 --- a/test/regression-low/Regression/LaterAssignOverwriteSpec.hs +++ b/test/regression-low/Regression/LaterAssignOverwriteSpec.hs @@ -24,8 +24,10 @@ 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))])] ] diff --git a/test/regression-low/Regression/LaterWaitSpec.hs b/test/regression-low/Regression/LaterWaitSpec.hs index 9bfdd9fa..2d173518 100644 --- a/test/regression-low/Regression/LaterWaitSpec.hs +++ b/test/regression-low/Regression/LaterWaitSpec.hs @@ -28,8 +28,14 @@ p = Program , Procedure { name = Ident "fun0" Nothing , arguments = [] +<<<<<<< HEAD , body = [ NewRef (Ident "v0" Nothing) TInt32 (Lit TInt32 (LInt32 0)) , After (SSMTime (Lit TUInt64 (LUInt64 2)) SSMNanosecond) +======= + , 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) +>>>>>>> remove NewRef in favor of CreateRef (Dynamic (Ident "v0" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 1)) , Wait [Dynamic (Ident "v0" Nothing, Ref TInt32)] diff --git a/test/regression-low/Regression/ManyContsSpec.hs b/test/regression-low/Regression/ManyContsSpec.hs index a1477ef5..de4dad6d 100644 --- a/test/regression-low/Regression/ManyContsSpec.hs +++ b/test/regression-low/Regression/ManyContsSpec.hs @@ -16,9 +16,8 @@ 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)])] ] } diff --git a/test/regression-low/Regression/MultOverflowIndirectSpec.hs b/test/regression-low/Regression/MultOverflowIndirectSpec.hs index 1bbd9cf8..b665e730 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,7 +33,8 @@ p = Program (Lit TInt32 (LInt32 0)) ] [] - , NewRef (Ident "v3" Nothing) TInt32 (Lit TInt32 (LInt32 0)) + , CreateRef (Ident "v3" Nothing) (Ref TInt32) + , SetRef (Dynamic (Ident "v3" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 0)) , Wait [Dynamic (Ident "v3" Nothing, Ref TInt32)] ] } diff --git a/test/regression-low/Regression/MultOverflowSpec.hs b/test/regression-low/Regression/MultOverflowSpec.hs index 06a01330..2101fc2d 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)) From fa1187a41778c2a87b79e6674bbe8ae764708a5f Mon Sep 17 00:00:00 2001 From: Robert Krook Date: Wed, 11 Aug 2021 14:01:11 +0200 Subject: [PATCH 02/10] Remove unused code --- ssm/SSM/Interpret/Interpreter.hs | 3 --- 1 file changed, 3 deletions(-) diff --git a/ssm/SSM/Interpret/Interpreter.hs b/ssm/SSM/Interpret/Interpreter.hs index a950976b..8c3f0872 100644 --- a/ssm/SSM/Interpret/Interpreter.hs +++ b/ssm/SSM/Interpret/Interpreter.hs @@ -103,9 +103,6 @@ step = do CreateRef n t -> do createRef n t continue --- NewRef n _ e -> do --- newRef n e --- continue SetRef r e -> do writeRef r e From ff3964e5b8d94f605243b0508c61ede3e0dc0650 Mon Sep 17 00:00:00 2001 From: Robert Krook Date: Thu, 12 Aug 2021 11:18:45 +0200 Subject: [PATCH 03/10] initial division of wait into sensitize & desensitize --- ssm.cabal | 3 +- ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs | 124 ++++++++++ ssm/SSM/Backend/C/CodeGen.hs | 218 +++++++++++++++--- ssm/SSM/Backend/C/Types.hs | 7 + ssm/SSM/Core/Syntax.hs | 9 +- ssm/SSM/Frontend/Syntax.hs | 4 +- ssm/SSM/Interpret/Internal.hs | 41 ++-- ssm/SSM/Interpret/Interpreter.hs | 20 +- ssm/SSM/Interpret/Types.hs | 4 +- ssm/SSM/Pretty/Syntax.hs | 10 +- test/lib/Test/SSM/QuickCheck/Generator.hs | 4 +- .../Test/SSM/QuickCheck/Shrink/Statements.hs | 1 - test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs | 10 +- test/lib/Test/SSM/QuickCheck/Util.hs | 14 +- .../Regression/FiveForkerSpec.hs | 29 ++- .../Regression/FlipFlopLoopSpec.hs | 11 +- .../Regression/LaterAssignOverwriteSpec.hs | 9 +- .../Regression/LaterWaitSpec.hs | 4 +- .../Regression/ManyContsSpec.hs | 6 +- .../Regression/MultOverflowIndirectSpec.hs | 4 +- .../Regression/MultOverflowSpec.hs | 4 +- .../Regression/RecurseExhaustDepthSpec.hs | 2 +- .../Regression/RecurseForeverSpec.hs | 2 +- 23 files changed, 451 insertions(+), 89 deletions(-) create mode 100644 ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs diff --git a/ssm.cabal b/ssm.cabal index ab1b2e18..65e8bdc2 100644 --- a/ssm.cabal +++ b/ssm.cabal @@ -4,7 +4,7 @@ cabal-version: 1.12 -- -- see: https://github.com/sol/hpack -- --- hash: 6573f29e908523f235835605a7bebd57b40eb94a62d4814901bb19aff3972368 +-- 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 diff --git a/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs b/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs new file mode 100644 index 00000000..972d9a15 --- /dev/null +++ b/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs @@ -0,0 +1,124 @@ +module SSM.Backend.C.Analysis.WaitAnalysis where + +import SSM.Backend.C.Types +import SSM.Core.Syntax + +import Control.Monad.State + +import qualified Data.Map as Map + +data St = St + { nextLineNumber :: Int + , widestwait :: Int + , sensitizemap :: Map.Map Int Int + , desensitizemap :: Map.Map Int Int + , currentSensitize :: Map.Map Reference Int + } + +analyseWait :: Procedure -> ([CStm], Map.Map Int Int, Map.Map Int Int, Int) +analyseWait p = + let (body', st) = runState (numberStmts (body p)) + $ St 1 0 Map.empty Map.empty Map.empty + in (body', sensitizemap st, desensitizemap st, widestwait st) + where + numberStmts :: [Stm] -> State St [CStm] + numberStmts [] = return [] + numberStmts stmts@(x : xs) = case x of + Sensitize _ -> do + -- fetch all @Sensitize@ and number them + let (sensitizes, rest) = getSensitizes stmts + csensitizes <- mapM (\stm -> flip Numbered stm <$> nextNumber) + sensitizes + + -- record information about triggers and size of the wait block + tagSensitizeWithTriggerId csensitizes + widestWait $ length csensitizes + + -- number the rest of the statements and return them + rest' <- numberStmts rest + return $ csensitizes ++ rest' + + Desensitize r -> do + n <- nextNumber + tagDesensitizeWithTriggerId r n + xs' <- numberStmts xs + return $ Numbered n (Desensitize r) : xs' + + If c thn els -> do + n <- nextNumber + thn' <- numberStmts thn + els' <- numberStmts els + xs' <- numberStmts xs + return $ CIf n c thn' els' : xs' + + While c bdy -> do + n <- nextNumber + bdy' <- numberStmts bdy + xs' <- numberStmts xs + return $ CWhile n c bdy' : xs' + + otherwise -> do + n <- nextNumber + xs' <- numberStmts xs + return $ Numbered n x : xs' + + where + -- | Return the number of the next st + nextNumber :: State St Int + nextNumber = do + n <- gets nextLineNumber + modify $ \st -> st { nextLineNumber = n + 1 } + return n + + {- | If @i@ in @widestWait i@ is larger than the previously largest widest wait, + update the known widest wait to be @i@ instead. -} + widestWait :: Int -> State St () + widestWait i = + modify $ \st -> st { widestwait = max (widestwait st) i } + + {- | Input to this function is a list of sensitize statements. All the sensitize + statements should make up the entire sequence of sensitize statements. This + function will assign a trigger ID to each sensitize statement and record this + information in the state. -} + tagSensitizeWithTriggerId :: [CStm] -> State St () + tagSensitizeWithTriggerId stmts = mapM_ (uncurry uploadID) + $ zip stmts [1 ..] + where + {- | @uploadID statementNumber triggerID@ registers that the statement + numbered with @number@ should be sensitized with trigger id @triggerID@. -} + uploadID :: CStm -> Int -> State St () + uploadID (Numbered l (Sensitize r)) tid = modify $ \st -> st + { sensitizemap = Map.insert l tid (sensitizemap st) + , currentSensitize = Map.insert r tid (currentSensitize st) + } + uploadID _ _ = + error "Robert made a mistake - should only be Numbered values" + + {- | Given a reference and the line number at which we wish to desensitize it, + look up which trigger ID this reference was last sensitized on and register that + this trigger ID should be desensitized, while also removing the state that says + that the reference is currently sensitized on that trigger. -} + tagDesensitizeWithTriggerId :: Reference -> Int -> State St () + tagDesensitizeWithTriggerId r l = do + sensinfo <- gets currentSensitize + let tid = case Map.lookup r sensinfo of + Just tid -> tid + Nothing -> error $ concat + [ "error in wait analysis - trying to " + , "desensitize reference that was " + , "never sensitized" + ] + modify $ \st -> st + { desensitizemap = Map.insert l tid (desensitizemap st) + , currentSensitize = Map.delete r (currentSensitize st) + } + + {- | Return a pair where the first element is all the `SSM.Core.Syntax.Sensitize` + values and the second component is the rest of the statements. -} + getSensitizes :: [Stm] -> ([Stm], [Stm]) + getSensitizes xs = (takeWhile isSensitize xs, dropWhile isSensitize xs) + + -- | Returns @True@ if a statement is a `SSM.Core.Syntax.Stm.Sensitize` value + isSensitize :: Stm -> Bool + isSensitize (Sensitize _) = True + isSensitize _ = False diff --git a/ssm/SSM/Backend/C/CodeGen.hs b/ssm/SSM/Backend/C/CodeGen.hs index 41d74ae1..69418258 100644 --- a/ssm/SSM/Backend/C/CodeGen.hs +++ b/ssm/SSM/Backend/C/CodeGen.hs @@ -11,11 +11,16 @@ module SSM.Backend.C.CodeGen ( compile_ + , exampleProcedure + , analyseWait ) where import Control.Monad.State.Lazy ( State , evalState + , runState , gets + , get + , put , modify ) @@ -30,6 +35,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 +77,8 @@ 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? + { --procedure :: Procedure -- ^ Procedure we are compiling + {-,-} 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 +87,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 @@ -172,6 +178,40 @@ includes = [cunit| $esc:("#include \"ssm-platform.h\"") |] +exampleProcedure :: Procedure +exampleProcedure = Procedure + (Ident "example" Nothing) + [ (Ident "r1" Nothing, Ref TInt32) + , (Ident "r2" Nothing, Ref TInt32) + , (Ident "r3" Nothing, Ref TInt32) + , (Ident "r4" Nothing, Ref TInt32) + , (Ident "r5" Nothing, Ref TInt32) + ] + [ CreateRef (Ident "l1" Nothing) (Ref TUInt64) + , SetRef (Dynamic (Ident "l1" Nothing, Ref TUInt64)) (Lit TUInt64 (LUInt64 0)) + , Sensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) + , Sensitize (Dynamic (Ident "r2" Nothing, Ref TInt32)) + , Sensitize (Dynamic (Ident "r3" Nothing, Ref TInt32)) + , Sensitize (Dynamic (Ident "r4" Nothing, Ref TInt32)) + , Yield + , Desensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) + , Desensitize (Dynamic (Ident "r2" Nothing, Ref TInt32)) + , Desensitize (Dynamic (Ident "r3" Nothing, Ref TInt32)) + , Desensitize (Dynamic (Ident "r4" Nothing, Ref TInt32)) + , SetRef (Dynamic (Ident "r1" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 5)) + , If (Lit TBool (LBool True)) + [ Sensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) + , Yield + , Desensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) + ] + [ Sensitize (Dynamic (Ident "r2" Nothing, Ref TInt32)) + , Sensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) + , Yield + , Desensitize (Dynamic (Ident "r2" Nothing, Ref TInt32)) + , Desensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) + ] + ] + {- | Generate definitions for an SSM 'Procedure'. The fst element of the returned tuple contains the struct definition and @@ -179,19 +219,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 +263,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 +321,12 @@ 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 + let (cstmts, sensitizemap, desensitizemap, widestwait) = analyseWait p + modify $ \st -> st { numwaits = widestwait } _ <- nextCase -- Toss away 0th case - cases <- concat <$> mapM genCase (body p) + cases <- concat <$> mapM (genCase' sensitizemap desensitizemap) cstmts -- (body p) locs <- gets locals final <- nextCase let @@ -355,6 +394,128 @@ genStep = do |] ) +genCase' :: Map.Map Int Int -> Map.Map 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 = genExp 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 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 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' 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' sensitizemap desensitizemap) bdy + return [[cstm| while ($exp:cnd) { $id:debug_microtick(); $stms:bod } |]] + {- | Generate the list of statements from each 'Stm' in an SSM 'Procedure'. Note that this compilation scheme might not work if the language were to @@ -365,16 +526,6 @@ genCase :: Stm -> TR [C.Stm] genCase (CreateRef n t) = do addLocal $ makeDynamicRef n t return [] ---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 @@ -416,7 +567,7 @@ genCase (After d r v) = do 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 +{-genCase (Wait ts) = do caseNum <- nextCase maxWaits $ length ts locs <- gets locals @@ -439,7 +590,14 @@ genCase (Wait ts) = do getTrace :: Reference -> C.Stm getTrace r = [cstm|$id:debug_trace($string:event);|] - where event = show $ T.ActSensitize $ refName r + where event = show $ T.ActSensitize $ refName r-} +genCase (Sensitize ref) = do + return [ [cstm| $id:debug_trace($string:(show $ T.ActSensitize $ refName ref));|] + , undefined] + where + trace = [cstm| $id:debug_trace($string:(show $ T.ActSensitize $ refName ref));|] +genCase (Desensitize ref) = undefined +genCase Yield = undefined genCase (Fork cs) = do locs <- gets locals caseNum <- nextCase diff --git a/ssm/SSM/Backend/C/Types.hs b/ssm/SSM/Backend/C/Types.hs index 65ccf501..ba8f4499 100644 --- a/ssm/SSM/Backend/C/Types.hs +++ b/ssm/SSM/Backend/C/Types.hs @@ -35,3 +35,10 @@ intFmt = fmt . baseType 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 + +{- | 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 diff --git a/ssm/SSM/Core/Syntax.hs b/ssm/SSM/Core/Syntax.hs index 30c4526e..79fa16cc 100644 --- a/ssm/SSM/Core/Syntax.hs +++ b/ssm/SSM/Core/Syntax.hs @@ -116,7 +116,7 @@ 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 @@ -179,7 +179,7 @@ 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 @@ -296,7 +296,10 @@ 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 +-- | Wait [Reference] -- ^ Wait for any of the references to be written to + | Sensitize Reference + | Desensitize Reference + | Yield {-| 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])] diff --git a/ssm/SSM/Frontend/Syntax.hs b/ssm/SSM/Frontend/Syntax.hs index 8c5e9235..00132297 100644 --- a/ssm/SSM/Frontend/Syntax.hs +++ b/ssm/SSM/Frontend/Syntax.hs @@ -268,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 f6a26e3d..33e6c7f1 100644 --- a/ssm/SSM/Interpret/Internal.hs +++ b/ssm/SSM/Interpret/Internal.hs @@ -45,8 +45,10 @@ module SSM.Interpret.Internal , readRef -- * Wait, fork, and leave + helpers - , wait +-- , wait , fork + , sensitize + , desensitize , setRunningChildren , addressToSelf , pds @@ -442,10 +444,12 @@ 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_ 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 @@ -453,13 +457,13 @@ writeVar_ ref e prio = do 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 } +-- 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) @@ -493,6 +497,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)] @@ -510,11 +521,11 @@ pds k = do {- | 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 +--wait :: [Reference] -> Interp s () +--wait refs = do +-- refs' <- mapM lookupRef refs +-- modify $ \st -> st { process = (process st) { waitingOn = Just refs' } } +-- mapM_ sensitize refs @@ -546,7 +557,7 @@ 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) + enqueue $ Proc (identName n) prio dep 0 (Just par) variables Map.empty (body p) 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 8c3f0872..da2a3d99 100644 --- a/ssm/SSM/Interpret/Interpreter.hs +++ b/ssm/SSM/Interpret/Interpreter.hs @@ -132,10 +132,20 @@ 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 + +-- Wait refs -> do +-- forM_ refs $ \r -> tellEvent $ T.ActSensitize $ refName r +-- wait refs +-- yield Fork procs -> do setRunningChildren (length procs) @@ -143,7 +153,7 @@ 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. diff --git a/ssm/SSM/Interpret/Types.hs b/ssm/SSM/Interpret/Types.hs index a16288df..b59514fc 100644 --- a/ssm/SSM/Interpret/Types.hs +++ b/ssm/SSM/Interpret/Types.hs @@ -98,7 +98,7 @@ data Proc s = Proc 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] +-- , waitingOn :: Maybe [Var s] -- | The work left to do for this process , continuation :: [Stm] } @@ -117,7 +117,7 @@ mkProc conf p fun = Proc { procName = identName $ entry p , parent = Nothing , variables = Map.empty , localrefs = Map.empty - , waitingOn = Nothing +-- , waitingOn = Nothing , continuation = body fun } diff --git a/ssm/SSM/Pretty/Syntax.hs b/ssm/SSM/Pretty/Syntax.hs index 441a3084..370cdba3 100644 --- a/ssm/SSM/Pretty/Syntax.hs +++ b/ssm/SSM/Pretty/Syntax.hs @@ -112,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 e661b72b..0ebe2e3d 100644 --- a/test/lib/Test/SSM/QuickCheck/Generator.hs +++ b/test/lib/Test/SSM/QuickCheck/Generator.hs @@ -157,8 +157,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 diff --git a/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs index a167107b..dd327e59 100644 --- a/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs +++ b/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs @@ -21,6 +21,5 @@ shrinkStmts stm = case stm of SetRef _ _ -> [Skip] SetLocal _ _ _ -> [Skip] After _ _ _ -> [Skip] - Wait _ -> [Skip] Fork _ -> [Skip] _ -> [] diff --git a/test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs index fa250693..175bfb5a 100644 --- a/test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs +++ b/test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs @@ -20,8 +20,8 @@ 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 - _ -> [] +shrinkWaits stm = [] --case stm of +-- Wait refs -> let sublists = map (\r -> delete r refs) refs +-- nonemptysublists = filter (not . null) sublists +-- in map Wait nonemptysublists +-- _ -> [] diff --git a/test/lib/Test/SSM/QuickCheck/Util.hs b/test/lib/Test/SSM/QuickCheck/Util.hs index b24987ef..d0e84daa 100644 --- a/test/lib/Test/SSM/QuickCheck/Util.hs +++ b/test/lib/Test/SSM/QuickCheck/Util.hs @@ -117,11 +117,17 @@ removeVars = go (rewriteExp v invalid validrefs) : go invalid validrefs xs - Wait refs -> - let refs' = filter (`elem` validrefs) refs - in if null refs' + Sensitize ref -> + if refIdent ref `elem` invalid then Skip : go invalid validrefs xs - else Wait refs' : 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) -> diff --git a/test/regression-low/Regression/FiveForkerSpec.hs b/test/regression-low/Regression/FiveForkerSpec.hs index 21136d1d..ab24b6f2 100644 --- a/test/regression-low/Regression/FiveForkerSpec.hs +++ b/test/regression-low/Regression/FiveForkerSpec.hs @@ -51,6 +51,7 @@ p = Program ] ) ] + , Yield ] } ) @@ -148,6 +149,7 @@ p = Program ) , (Ident "fun2" Nothing, []) ] + , Yield , Fork [ (Ident "fun2" Nothing, []) , ( Ident "fun5" Nothing @@ -234,6 +236,7 @@ p = Program ) , (Ident "fun2" Nothing, []) ] + , Yield , If (BOp TBool (Var TInt32 (Ident "var7" Nothing)) (Var TInt32 (Ident "var7" Nothing)) OLT) [ After @@ -314,6 +317,7 @@ p = Program , (Ident "fun2" Nothing, []) , (Ident "fun2" Nothing, []) ] + , Yield ] [ Fork [ (Ident "fun2" Nothing, []) @@ -377,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 @@ -457,6 +464,7 @@ p = Program ] ) ] + , Yield , Fork [ ( Ident "fun5" Nothing , [ Right (Dynamic (Ident "ref1" Nothing, Ref TInt32)) @@ -574,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)) @@ -600,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 870e688b..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 @@ -22,6 +24,7 @@ p = Program , 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 ] } ) @@ -35,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 9a0a70a5..fd22469e 100644 --- a/test/regression-low/Regression/LaterAssignOverwriteSpec.hs +++ b/test/regression-low/Regression/LaterAssignOverwriteSpec.hs @@ -30,6 +30,7 @@ p = Program , 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 ] } ) @@ -46,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 2d173518..c1bbb0eb 100644 --- a/test/regression-low/Regression/LaterWaitSpec.hs +++ b/test/regression-low/Regression/LaterWaitSpec.hs @@ -38,7 +38,9 @@ p = Program >>>>>>> remove NewRef in favor of CreateRef (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 de4dad6d..6c17658c 100644 --- a/test/regression-low/Regression/ManyContsSpec.hs +++ b/test/regression-low/Regression/ManyContsSpec.hs @@ -19,6 +19,7 @@ p = Program , 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 ] } ) @@ -32,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) @@ -47,6 +50,7 @@ p = Program ] ) ] + , Yield ] } ) diff --git a/test/regression-low/Regression/MultOverflowIndirectSpec.hs b/test/regression-low/Regression/MultOverflowIndirectSpec.hs index b665e730..b7acacf3 100644 --- a/test/regression-low/Regression/MultOverflowIndirectSpec.hs +++ b/test/regression-low/Regression/MultOverflowIndirectSpec.hs @@ -35,7 +35,9 @@ p = Program [] , CreateRef (Ident "v3" Nothing) (Ref TInt32) , SetRef (Dynamic (Ident "v3" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 0)) - , Wait [Dynamic (Ident "v3" Nothing, Ref TInt32)] + , 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 2101fc2d..c13351a5 100644 --- a/test/regression-low/Regression/MultOverflowSpec.hs +++ b/test/regression-low/Regression/MultOverflowSpec.hs @@ -35,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 ] } ) ] From e6afd483f54a131d06e1883aabac9c2c5d353f55 Mon Sep 17 00:00:00 2001 From: Robert Krook Date: Mon, 16 Aug 2021 19:59:55 +0200 Subject: [PATCH 04/10] fixed some bugs and rewrote some of the shrinking strategies --- ssm/SSM/Backend/C/CodeGen.hs | 14 +- ssm/SSM/Core/Syntax.hs | 9 +- ssm/SSM/Interpret/Internal.hs | 92 ++--- ssm/SSM/Interpret/Interpreter.hs | 21 +- ssm/SSM/Interpret/Types.hs | 29 +- test/lib/Test/SSM/Prop.hs | 3 +- test/lib/Test/SSM/QuickCheck/Generator.hs | 18 +- test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs | 10 +- .../Test/SSM/QuickCheck/Shrink/Statements.hs | 17 +- test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs | 171 ++++++++- test/lib/Test/SSM/QuickCheck/Util.hs | 327 ++++++++++-------- .../Regression/ManyContsSpec.hs | 4 +- 12 files changed, 448 insertions(+), 267 deletions(-) diff --git a/ssm/SSM/Backend/C/CodeGen.hs b/ssm/SSM/Backend/C/CodeGen.hs index 69418258..2a147944 100644 --- a/ssm/SSM/Backend/C/CodeGen.hs +++ b/ssm/SSM/Backend/C/CodeGen.hs @@ -133,15 +133,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] diff --git a/ssm/SSM/Core/Syntax.hs b/ssm/SSM/Core/Syntax.hs index 79fa16cc..b2555f58 100644 --- a/ssm/SSM/Core/Syntax.hs +++ b/ssm/SSM/Core/Syntax.hs @@ -295,11 +295,10 @@ 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 - | Desensitize Reference - | Yield + | After SSMExp Reference SSMExp + | 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])] diff --git a/ssm/SSM/Interpret/Internal.hs b/ssm/SSM/Interpret/Internal.hs index 33e6c7f1..423a4d33 100644 --- a/ssm/SSM/Interpret/Internal.hs +++ b/ssm/SSM/Interpret/Internal.hs @@ -102,7 +102,7 @@ import SSM.Util.Operators ( (<#>) ) import SSM.Core.Syntax import qualified SSM.Interpret.Trace as T import SSM.Interpret.Types - +import Debug.Trace {-********** Main interpret function helpers **********-} -- | Create initial global variable storage @@ -110,7 +110,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 @@ -127,13 +127,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 **********-} @@ -255,10 +266,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) @@ -268,6 +286,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. @@ -291,10 +310,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 @@ -302,7 +322,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 **********-} @@ -310,8 +331,8 @@ pushInstructions stmts = do createVar :: SSMExp -> Interp s (Var s) createVar e = do v <- eval e - n <- getNow - lift' $ newVar' v n + --n <- getNow + lift' $ newVar' v maxBound--n {- | 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. @@ -329,17 +350,6 @@ createRef n t = newRef n $ defaultValue (dereference t) p <- gets process modify $ \st -> st { process = p { localrefs = Map.insert n ref (localrefs p) } } -{- | 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: 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) } } - -- | Write a value to a variable. writeRef :: Reference -> SSMExp -> Interp s () writeRef r e = do @@ -455,15 +465,6 @@ writeVar_ ref e prio = do -- 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) @@ -486,7 +487,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 @@ -516,25 +516,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@. @@ -557,7 +538,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 (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 da2a3d99..59429416 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 ( (++) ) @@ -19,7 +20,7 @@ import Control.Monad import Control.Monad.ST.Lazy import Control.Monad.State.Lazy import Control.Monad.Writer.Lazy - +import Debug.Trace -- | Interpret an SSM program with the default configuration. interpret_ :: SSMProgram p => p -> T.Trace interpret_ = interpret def @@ -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,7 +94,6 @@ 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 @@ -142,11 +140,6 @@ step = do desensitize ref continue --- Wait refs -> do --- forM_ refs $ \r -> tellEvent $ T.ActSensitize $ refName r --- wait refs --- yield - Fork procs -> do setRunningChildren (length procs) parent <- addressToSelf @@ -157,6 +150,8 @@ step = do 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 b59514fc..6ab062cb 100644 --- a/ssm/SSM/Interpret/Types.hs +++ b/ssm/SSM/Interpret/Types.hs @@ -93,14 +93,14 @@ 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] +-- , toSensitizeOn :: [Reference] -- | The work left to do for this process - , continuation :: [Stm] + , continuation :: STRef s [Stm] } deriving Eq @@ -109,17 +109,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/test/lib/Test/SSM/Prop.hs b/test/lib/Test/SSM/Prop.hs index 22e4b34e..f233ee97 100644 --- a/test/lib/Test/SSM/Prop.hs +++ b/test/lib/Test/SSM/Prop.hs @@ -33,7 +33,8 @@ import Test.SSM.Trace ( doCompareTraces -- | List of act and event queue sizes to test. queueSizes :: [(Int, Int)] -queueSizes = [(32, 32), (256, 256), (2048, 2048)] +--queueSizes = [(32, 32), (256, 256), (2048, 2048)] +queueSizes = [(2048, 2048)] -- | Tests that generated SSM programs compile successfully. propCompiles :: SSMProgram p => TestName -> p -> QC.Property diff --git a/test/lib/Test/SSM/QuickCheck/Generator.hs b/test/lib/Test/SSM/QuickCheck/Generator.hs index 0ebe2e3d..e6121b94 100644 --- a/test/lib/Test/SSM/QuickCheck/Generator.hs +++ b/test/lib/Test/SSM/QuickCheck/Generator.hs @@ -128,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') ) ] ++ @@ -142,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 @@ -230,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/Fork.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs index 1e67b254..d558302d 100644 --- a/test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs +++ b/test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs @@ -22,8 +22,8 @@ shrinkForksProcedure p = {- | Shrink fork statements by replacing the list of forked processes with all 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 - _ -> [] +shrinkForkStm stm = [] --case stm of +-- 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/Statements.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs index dd327e59..ab19a6a4 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,13 +14,15 @@ statements = transformProcedures shrinkAllStmtsProcedure -- statements. shrinkAllStmtsProcedure :: Procedure -> [Procedure] shrinkAllStmtsProcedure p = - [ p { body = body' } | body' <- distributeMutate (body p) shrinkStmts ] + [ p { body = (removeLonelyYield body') } + | body' <- distributeMutate (body p) shrinkStmts + ] -- | Replace any of the below statements with a skip instruction shrinkStmts :: Stm -> [Stm] shrinkStmts stm = case stm of - SetRef _ _ -> [Skip] +-- SetRef _ _ -> [Skip] SetLocal _ _ _ -> [Skip] - After _ _ _ -> [Skip] + After _ _ _ -> [Skip] Fork _ -> [Skip] _ -> [] diff --git a/test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Wait.hs index 175bfb5a..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 d0e84daa..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,139 +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 - 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 -> + -- | 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 + in While (rewriteExp c invalid validrefs) bdy' + : go invalid validrefs xs - Skip -> Skip : 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 + 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 + 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 + 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, + 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/ManyContsSpec.hs b/test/regression-low/Regression/ManyContsSpec.hs index 6c17658c..06d8ce1b 100644 --- a/test/regression-low/Regression/ManyContsSpec.hs +++ b/test/regression-low/Regression/ManyContsSpec.hs @@ -33,9 +33,9 @@ p = Program (SSMTime (Lit TUInt64 (LUInt64 2)) SSMNanosecond) (Dynamic (Ident "Ref2" Nothing, Ref TUInt64)) (Lit TUInt64 (LUInt64 2)) - , Sensitize (Dynamic (Ident "ref2" Nothing, Ref TUInt64)) + , Sensitize (Dynamic (Ident "Ref2" Nothing, Ref TUInt64)) , Yield - , Desensitize (Dynamic (Ident "ref2" Nothing, Ref TUInt64)) + , Desensitize (Dynamic (Ident "Ref2" Nothing, Ref TUInt64)) , Fork [ ( Ident "fun1" Nothing , [ Right $ Dynamic (Ident "Ref2" Nothing, Ref TUInt64) From be9fd2dc1e26d523306c0e791c8ef014fdadabb3 Mon Sep 17 00:00:00 2001 From: Robert Krook Date: Mon, 16 Aug 2021 22:53:29 +0200 Subject: [PATCH 05/10] doc work --- .../Test/SSM/QuickCheck/Shrink/Statements.hs | 36 ++++++++++++++----- 1 file changed, 27 insertions(+), 9 deletions(-) diff --git a/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs index ab19a6a4..4e696dcc 100644 --- a/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs +++ b/test/lib/Test/SSM/QuickCheck/Shrink/Statements.hs @@ -15,14 +15,32 @@ statements = transformProcedures shrinkAllStmtsProcedure shrinkAllStmtsProcedure :: Procedure -> [Procedure] shrinkAllStmtsProcedure p = [ p { body = (removeLonelyYield body') } - | body' <- distributeMutate (body p) shrinkStmts + | 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] - 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) From 7ae9a7e68bb78d7549e54df583877ad407a60642 Mon Sep 17 00:00:00 2001 From: Robert Krook Date: Tue, 17 Aug 2021 11:40:23 +0200 Subject: [PATCH 06/10] Document the new wait analysis module, to make it easier to review --- ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs | 101 +++++++++++++++++++-- 1 file changed, 94 insertions(+), 7 deletions(-) diff --git a/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs b/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs index 972d9a15..64df0717 100644 --- a/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs +++ b/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs @@ -1,26 +1,113 @@ -module SSM.Backend.C.Analysis.WaitAnalysis where - -import SSM.Backend.C.Types -import SSM.Core.Syntax - -import Control.Monad.State +{- | This module implements an analysis pass that annotates the body of a procedure with +information about which triggers to sensitize on. + +Earlier in the project, there was a single statement @Wait :: [Reference] -> Stm@ and +no @Yield :: Stm@ statement. When generating code for @Wait@ you immediately knew how +many references you needed to sensitize (since you had them all in that list) and you +could record that you are now sensitizing @n@ references, to know how many unique +triggers you're going to need. + +When the syntax was split up into the more fine-grained statements +`Sensitize`, `Desensitize` and +`Yield` in favour of @Wait@, this information become lost. When +generating code for a single `Sensitize` statement, it is not clear +how many references you are waiting on in total, or which of them in the sequence this +is. This makes it hard to know which trigger ID to sensitize on. + +What this module does is that it implement an analysis pass that infers the now lost +information from the sequence of statements that make up a procedure body. It will +return the same procedure body as before, but where each statement has been given a +unique @Int@ ID. Alongside these new statements two maps are produced. They associate +a statement ID with a trigger ID. So if you generate code for @Numbered n (Sensitize r)@, +you will look up which ID @r@ should be @Sensitized@ on by checking which trigger ID @n@ +is associated with in the sensitize map. Lastly, the size of the widest wait is inferred +from the procedure body and returned. + +@ +> analyseWait [ CreateRef r1 (Ref TInt) + , SetRef r1 5 + , CreateRef r2 (Ref TBool) + , SetRef r2 False + , Sensitize r1 + , Sensitize r2 + , Yield + , Desensitize r1 + , Desensitize r2 + , SetRef r2 True] +( [ Numbered 1 $ CreateRef r1 $ Ref TInt + , Numbered 2 $ SetRef r2 5) + , Numbered 3 $ CreateRef r2 $ Ref TBool + , Numbered 4 $ SetRef r2 False + , Numbered 5 $ Sensitize r1 + , Numbered 6 $ Sensitize r2 + , Numbered 7 $ Yield + , Numbered 8 4 Desensitize r1 + , Numbered 9 $ Desensitize r2 + , Numbered 10 $ SetRef r2 True] +, [ (5, 1), (6, 2)] +, [ (8, 1), (9, 2)] +, 2 +) +@ + +It's a bit crude, and should probably be made better later on when we wish to perform +different analysis passes. In particular, I am not too fond of the makeshift datatype +I implemented to number the statements. +-} +module SSM.Backend.C.Analysis.WaitAnalysis + ( analyseWait + ) where + +import SSM.Backend.C.Types ( CStm(..) ) +import SSM.Core.Syntax ( Procedure(body) + , Reference + , Stm + ( Desensitize + , If + , Sensitize + , While + ) + ) + +import Control.Monad.State ( State + , gets + , modify + , runState + ) import qualified Data.Map as Map +-- | Analysis state data St = St - { nextLineNumber :: Int + { -- | ID of next statement + nextLineNumber :: Int + -- | Size of the widest wait statement , widestwait :: Int + -- | Map associating sensitize statement IDs with trigger IDs , sensitizemap :: Map.Map Int Int + -- | Map associating desensitize statement IDs with trigger IDs , desensitizemap :: Map.Map Int Int + {- | Since references need to desensitize on the same reference they sensitized on, + we must remember which triggers references were sensitized on. -} , currentSensitize :: Map.Map Reference Int } +{- | Analyse the body of a procedure and return a tuple with + +1. The same procedure body, but with the statements given unique IDs +2. Map associating sensitize statement IDs with trigger IDs to sensitize on +3. Map associating desensitize statement IDs with trigger IDs to sensitize on +4. The size of the widest wait statement, which is used to determine how many unique + triggers needs to be generated. +-} analyseWait :: Procedure -> ([CStm], Map.Map Int Int, Map.Map Int Int, Int) analyseWait p = let (body', st) = runState (numberStmts (body p)) $ St 1 0 Map.empty Map.empty Map.empty in (body', sensitizemap st, desensitizemap st, widestwait st) where + {- | Assign unique numbers to statements and possible record trigger usage + information. -} numberStmts :: [Stm] -> State St [CStm] numberStmts [] = return [] numberStmts stmts@(x : xs) = case x of From f87b53a19805c4de2c2dbb022f2aa1de4c5b67eb Mon Sep 17 00:00:00 2001 From: Robert Krook Date: Tue, 17 Aug 2021 14:10:55 +0200 Subject: [PATCH 07/10] removed unused code and cleaned up. Added back fork shrinking strategies --- ssm/SSM/Backend/C/CodeGen.hs | 189 ++------------------ ssm/SSM/Backend/C/Types.hs | 5 +- ssm/SSM/Interpret/Internal.hs | 7 +- ssm/SSM/Interpret/Interpreter.hs | 2 +- ssm/SSM/Interpret/Types.hs | 2 - test/lib/Test/SSM/Prop.hs | 3 +- test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs | 22 +-- 7 files changed, 35 insertions(+), 195 deletions(-) diff --git a/ssm/SSM/Backend/C/CodeGen.hs b/ssm/SSM/Backend/C/CodeGen.hs index 2a147944..32973d82 100644 --- a/ssm/SSM/Backend/C/CodeGen.hs +++ b/ssm/SSM/Backend/C/CodeGen.hs @@ -11,8 +11,6 @@ module SSM.Backend.C.CodeGen ( compile_ - , exampleProcedure - , analyseWait ) where import Control.Monad.State.Lazy ( State @@ -77,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 } @@ -186,40 +183,6 @@ includes = [cunit| $esc:("#include \"ssm-platform.h\"") |] -exampleProcedure :: Procedure -exampleProcedure = Procedure - (Ident "example" Nothing) - [ (Ident "r1" Nothing, Ref TInt32) - , (Ident "r2" Nothing, Ref TInt32) - , (Ident "r3" Nothing, Ref TInt32) - , (Ident "r4" Nothing, Ref TInt32) - , (Ident "r5" Nothing, Ref TInt32) - ] - [ CreateRef (Ident "l1" Nothing) (Ref TUInt64) - , SetRef (Dynamic (Ident "l1" Nothing, Ref TUInt64)) (Lit TUInt64 (LUInt64 0)) - , Sensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) - , Sensitize (Dynamic (Ident "r2" Nothing, Ref TInt32)) - , Sensitize (Dynamic (Ident "r3" Nothing, Ref TInt32)) - , Sensitize (Dynamic (Ident "r4" Nothing, Ref TInt32)) - , Yield - , Desensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) - , Desensitize (Dynamic (Ident "r2" Nothing, Ref TInt32)) - , Desensitize (Dynamic (Ident "r3" Nothing, Ref TInt32)) - , Desensitize (Dynamic (Ident "r4" Nothing, Ref TInt32)) - , SetRef (Dynamic (Ident "r1" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 5)) - , If (Lit TBool (LBool True)) - [ Sensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) - , Yield - , Desensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) - ] - [ Sensitize (Dynamic (Ident "r2" Nothing, Ref TInt32)) - , Sensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) - , Yield - , Desensitize (Dynamic (Ident "r2" Nothing, Ref TInt32)) - , Desensitize (Dynamic (Ident "r1" Nothing, Ref TInt32)) - ] - ] - {- | Generate definitions for an SSM 'Procedure'. The fst element of the returned tuple contains the struct definition and @@ -334,7 +297,7 @@ genStep p = do let (cstmts, sensitizemap, desensitizemap, widestwait) = analyseWait p modify $ \st -> st { numwaits = widestwait } _ <- nextCase -- Toss away 0th case - cases <- concat <$> mapM (genCase' sensitizemap desensitizemap) cstmts -- (body p) + cases <- concat <$> mapM (genCase sensitizemap desensitizemap) cstmts locs <- gets locals final <- nextCase let @@ -402,8 +365,14 @@ genStep p = do |] ) -genCase' :: Map.Map Int Int -> Map.Map Int Int -> CStm -> TR [C.Stm] -genCase' sensitizemap desensitizemap (Numbered n stm) = case stm of +{- | Generate the list of statements from each 'Stm' in an SSM 'Procedure'. + +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 :: Map.Map Int Int -> Map.Map Int Int -> CStm -> TR [C.Stm] +genCase sensitizemap desensitizemap (Numbered n stm) = case stm of CreateRef n t -> do addLocal $ makeDynamicRef n t @@ -436,7 +405,7 @@ genCase' sensitizemap desensitizemap (Numbered n stm) = case stm of locs <- gets locals let lvar = refIdent r t = refType r - del = genExp locs d + del = genTimeDelay locs d lhs = refPtr r locs rhs = genExp locs v -- Note that the semantics of 'After' and 'later_' differ---the former @@ -512,140 +481,14 @@ genCase' sensitizemap desensitizemap (Numbered n stm) = case stm of : map genTrace cs ++ zipWith genCall [0 :: Int ..] cs -genCase' sensitizemap desensitizemap (CIf n c thn els) = do +genCase sensitizemap desensitizemap (CIf n c thn els) = do locs <- gets locals let cnd = genExp locs c - thn' <- concat <$> mapM (genCase' sensitizemap desensitizemap) thn - els' <- concat <$> mapM (genCase' sensitizemap desensitizemap) els + 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 +genCase sensitizemap desensitizemap (CWhile n c bdy) = do locs <- gets locals let cnd = genExp locs c - bod <- concat <$> mapM (genCase' sensitizemap desensitizemap) bdy + bod <- concat <$> mapM (genCase sensitizemap desensitizemap) bdy return [[cstm| while ($exp:cnd) { $id:debug_microtick(); $stms:bod } |]] - -{- | Generate the list of statements from each 'Stm' in an SSM 'Procedure'. - -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 (CreateRef n t) = do - addLocal $ makeDynamicRef n t - return [] -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 - 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 - let cnd = genExp locs c - bod <- concat <$> mapM genCase b - 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 (Sensitize ref) = do - return [ [cstm| $id:debug_trace($string:(show $ T.ActSensitize $ refName ref));|] - , undefined] - where - trace = [cstm| $id:debug_trace($string:(show $ T.ActSensitize $ refName ref));|] -genCase (Desensitize ref) = undefined -genCase Yield = undefined -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 ba8f4499..1fbe344f 100644 --- a/ssm/SSM/Backend/C/Types.hs +++ b/ssm/SSM/Backend/C/Types.hs @@ -33,8 +33,9 @@ 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. -} diff --git a/ssm/SSM/Interpret/Internal.hs b/ssm/SSM/Interpret/Internal.hs index 423a4d33..d124a93f 100644 --- a/ssm/SSM/Interpret/Internal.hs +++ b/ssm/SSM/Interpret/Internal.hs @@ -45,7 +45,6 @@ module SSM.Interpret.Internal , readRef -- * Wait, fork, and leave + helpers --- , wait , fork , sensitize , desensitize @@ -102,7 +101,7 @@ import SSM.Util.Operators ( (<#>) ) import SSM.Core.Syntax import qualified SSM.Interpret.Trace as T import SSM.Interpret.Types -import Debug.Trace + {-********** Main interpret function helpers **********-} -- | Create initial global variable storage @@ -331,8 +330,7 @@ pushInstructions stmts = do createVar :: SSMExp -> Interp s (Var s) createVar e = do v <- eval e - --n <- getNow - lift' $ newVar' v maxBound--n + lift' $ newVar' v maxBound {- | 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. @@ -458,7 +456,6 @@ writeVar_ ref e prio = do 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 diff --git a/ssm/SSM/Interpret/Interpreter.hs b/ssm/SSM/Interpret/Interpreter.hs index 59429416..2ede113d 100644 --- a/ssm/SSM/Interpret/Interpreter.hs +++ b/ssm/SSM/Interpret/Interpreter.hs @@ -20,7 +20,7 @@ import Control.Monad import Control.Monad.ST.Lazy import Control.Monad.State.Lazy import Control.Monad.Writer.Lazy -import Debug.Trace + -- | Interpret an SSM program with the default configuration. interpret_ :: SSMProgram p => p -> T.Trace interpret_ = interpret def diff --git a/ssm/SSM/Interpret/Types.hs b/ssm/SSM/Interpret/Types.hs index 6ab062cb..7dda7142 100644 --- a/ssm/SSM/Interpret/Types.hs +++ b/ssm/SSM/Interpret/Types.hs @@ -97,8 +97,6 @@ data Proc s = Proc 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 --- , toSensitizeOn :: [Reference] -- | The work left to do for this process , continuation :: STRef s [Stm] } diff --git a/test/lib/Test/SSM/Prop.hs b/test/lib/Test/SSM/Prop.hs index f233ee97..22e4b34e 100644 --- a/test/lib/Test/SSM/Prop.hs +++ b/test/lib/Test/SSM/Prop.hs @@ -33,8 +33,7 @@ import Test.SSM.Trace ( doCompareTraces -- | List of act and event queue sizes to test. queueSizes :: [(Int, Int)] ---queueSizes = [(32, 32), (256, 256), (2048, 2048)] -queueSizes = [(2048, 2048)] +queueSizes = [(32, 32), (256, 256), (2048, 2048)] -- | Tests that generated SSM programs compile successfully. propCompiles :: SSMProgram p => TestName -> p -> QC.Property diff --git a/test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs b/test/lib/Test/SSM/QuickCheck/Shrink/Fork.hs index d558302d..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. -} @@ -22,8 +23,9 @@ shrinkForksProcedure p = {- | Shrink fork statements by replacing the list of forked processes with all 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 --- _ -> [] +shrinkForkStm stm = case stm of + Fork procs -> + let sublists = map (\f -> delete f procs) procs + nonemptysublists = filter (not . null) sublists + in map Fork nonemptysublists + _ -> [] From dd5208f7b09fb5c9f76752b5c599e3024dcb2263 Mon Sep 17 00:00:00 2001 From: Robert Krook Date: Tue, 17 Aug 2021 14:49:32 +0200 Subject: [PATCH 08/10] fixed some problems I missed, small changes only --- ssm/SSM/Core/Syntax.hs | 2 +- test/regression-low/Regression/CancelBothSpec.hs | 2 +- test/regression-low/Regression/LaterWaitSpec.hs | 5 ----- 3 files changed, 2 insertions(+), 7 deletions(-) diff --git a/ssm/SSM/Core/Syntax.hs b/ssm/SSM/Core/Syntax.hs index b2555f58..b6cd28bb 100644 --- a/ssm/SSM/Core/Syntax.hs +++ b/ssm/SSM/Core/Syntax.hs @@ -295,7 +295,7 @@ data Stm {- | @After d r v@ - After @d@ units of time the reference @r@ should get the new value @v@. -} - | After SSMExp Reference SSMExp + | After SSMTime Reference SSMExp | Sensitize Reference -- ^ Sensitize the current process on this reference | Desensitize Reference -- ^ Desensitize the current process on this reference | Yield -- ^ Yield control diff --git a/test/regression-low/Regression/CancelBothSpec.hs b/test/regression-low/Regression/CancelBothSpec.hs index 91331afe..ba2ef4ab 100644 --- a/test/regression-low/Regression/CancelBothSpec.hs +++ b/test/regression-low/Regression/CancelBothSpec.hs @@ -22,7 +22,7 @@ p = Program , body = [ CreateRef (Ident "v0" Nothing) (Ref TBool) , SetRef (Dynamic (Ident "v0" Nothing, Ref TBool)) (Lit TBool (LBool False)) - , After (SSMTime (Lit TUInt64 (LUInt64 1)) (SSMNanosecond) + , After (SSMTime (Lit TUInt64 (LUInt64 1)) SSMNanosecond) (Dynamic (Ident "v0" Nothing, Ref TBool)) (Lit TBool (LBool True)) , CreateRef (Ident "v1" Nothing) (Ref TBool) diff --git a/test/regression-low/Regression/LaterWaitSpec.hs b/test/regression-low/Regression/LaterWaitSpec.hs index c1bbb0eb..2276a04e 100644 --- a/test/regression-low/Regression/LaterWaitSpec.hs +++ b/test/regression-low/Regression/LaterWaitSpec.hs @@ -28,14 +28,9 @@ p = Program , Procedure { name = Ident "fun0" Nothing , arguments = [] -<<<<<<< HEAD - , body = [ NewRef (Ident "v0" Nothing) TInt32 (Lit TInt32 (LInt32 0)) - , After (SSMTime (Lit TUInt64 (LUInt64 2)) SSMNanosecond) -======= , 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) ->>>>>>> remove NewRef in favor of CreateRef (Dynamic (Ident "v0" Nothing, Ref TInt32)) (Lit TInt32 (LInt32 1)) , Sensitize (Dynamic (Ident "v0" Nothing, Ref TInt32)) From d2eb56074f06b85605812e627ce2b68ca912da61 Mon Sep 17 00:00:00 2001 From: Robert Krook Date: Wed, 1 Sep 2021 16:47:59 +0200 Subject: [PATCH 09/10] Separated turning [Stm] to [CStm], and the algorithm that assigns trigger IDs --- ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs | 180 ++++++--------------- ssm/SSM/Backend/C/CodeGen.hs | 11 +- ssm/SSM/Backend/C/Types.hs | 33 ++++ 3 files changed, 87 insertions(+), 137 deletions(-) diff --git a/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs b/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs index 64df0717..f12ebe8a 100644 --- a/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs +++ b/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs @@ -54,9 +54,7 @@ It's a bit crude, and should probably be made better later on when we wish to pe different analysis passes. In particular, I am not too fond of the makeshift datatype I implemented to number the statements. -} -module SSM.Backend.C.Analysis.WaitAnalysis - ( analyseWait - ) where +module SSM.Backend.C.Analysis.WaitAnalysis where import SSM.Backend.C.Types ( CStm(..) ) import SSM.Core.Syntax ( Procedure(body) @@ -71,141 +69,59 @@ import SSM.Core.Syntax ( Procedure(body) import Control.Monad.State ( State , gets + , get + , put , modify , runState + , execState ) import qualified Data.Map as Map --- | Analysis state -data St = St - { -- | ID of next statement - nextLineNumber :: Int - -- | Size of the widest wait statement - , widestwait :: Int - -- | Map associating sensitize statement IDs with trigger IDs - , sensitizemap :: Map.Map Int Int - -- | Map associating desensitize statement IDs with trigger IDs - , desensitizemap :: Map.Map Int Int - {- | Since references need to desensitize on the same reference they sensitized on, - we must remember which triggers references were sensitized on. -} - , currentSensitize :: Map.Map Reference Int - } +-- | Keys of the sensitize/desensitize map are pairs of references and statement numbers +type TriggerKey = (Reference, Int) +-- | A map associating `TriggerKey` with a trigger ID +type TriggerMap = Map.Map TriggerKey Int -{- | Analyse the body of a procedure and return a tuple with +-- | State for the primitive trigger scheme +type PrimSt = (Int, Map.Map Reference Int, TriggerMap, TriggerMap) -1. The same procedure body, but with the statements given unique IDs -2. Map associating sensitize statement IDs with trigger IDs to sensitize on -3. Map associating desensitize statement IDs with trigger IDs to sensitize on -4. The size of the widest wait statement, which is used to determine how many unique - triggers needs to be generated. --} -analyseWait :: Procedure -> ([CStm], Map.Map Int Int, Map.Map Int Int, Int) -analyseWait p = - let (body', st) = runState (numberStmts (body p)) - $ St 1 0 Map.empty Map.empty Map.empty - in (body', sensitizemap st, desensitizemap st, widestwait st) +-- | Return (how many unique triggers are needed, sensitize map, desensitize map) +primitiveTriggerIDs :: [CStm] -> (Int, TriggerMap, TriggerMap) +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 - {- | Assign unique numbers to statements and possible record trigger usage - information. -} - numberStmts :: [Stm] -> State St [CStm] - numberStmts [] = return [] - numberStmts stmts@(x : xs) = case x of - Sensitize _ -> do - -- fetch all @Sensitize@ and number them - let (sensitizes, rest) = getSensitizes stmts - csensitizes <- mapM (\stm -> flip Numbered stm <$> nextNumber) - sensitizes - - -- record information about triggers and size of the wait block - tagSensitizeWithTriggerId csensitizes - widestWait $ length csensitizes - - -- number the rest of the statements and return them - rest' <- numberStmts rest - return $ csensitizes ++ rest' - - Desensitize r -> do - n <- nextNumber - tagDesensitizeWithTriggerId r n - xs' <- numberStmts xs - return $ Numbered n (Desensitize r) : xs' - - If c thn els -> do - n <- nextNumber - thn' <- numberStmts thn - els' <- numberStmts els - xs' <- numberStmts xs - return $ CIf n c thn' els' : xs' - - While c bdy -> do - n <- nextNumber - bdy' <- numberStmts bdy - xs' <- numberStmts xs - return $ CWhile n c bdy' : xs' - - otherwise -> do - n <- nextNumber - xs' <- numberStmts xs - return $ Numbered n x : xs' - - where - -- | Return the number of the next st - nextNumber :: State St Int - nextNumber = do - n <- gets nextLineNumber - modify $ \st -> st { nextLineNumber = n + 1 } - return n - - {- | If @i@ in @widestWait i@ is larger than the previously largest widest wait, - update the known widest wait to be @i@ instead. -} - widestWait :: Int -> State St () - widestWait i = - modify $ \st -> st { widestwait = max (widestwait st) i } - - {- | Input to this function is a list of sensitize statements. All the sensitize - statements should make up the entire sequence of sensitize statements. This - function will assign a trigger ID to each sensitize statement and record this - information in the state. -} - tagSensitizeWithTriggerId :: [CStm] -> State St () - tagSensitizeWithTriggerId stmts = mapM_ (uncurry uploadID) - $ zip stmts [1 ..] - where - {- | @uploadID statementNumber triggerID@ registers that the statement - numbered with @number@ should be sensitized with trigger id @triggerID@. -} - uploadID :: CStm -> Int -> State St () - uploadID (Numbered l (Sensitize r)) tid = modify $ \st -> st - { sensitizemap = Map.insert l tid (sensitizemap st) - , currentSensitize = Map.insert r tid (currentSensitize st) - } - uploadID _ _ = - error "Robert made a mistake - should only be Numbered values" - - {- | Given a reference and the line number at which we wish to desensitize it, - look up which trigger ID this reference was last sensitized on and register that - this trigger ID should be desensitized, while also removing the state that says - that the reference is currently sensitized on that trigger. -} - tagDesensitizeWithTriggerId :: Reference -> Int -> State St () - tagDesensitizeWithTriggerId r l = do - sensinfo <- gets currentSensitize - let tid = case Map.lookup r sensinfo of - Just tid -> tid - Nothing -> error $ concat - [ "error in wait analysis - trying to " - , "desensitize reference that was " - , "never sensitized" - ] - modify $ \st -> st - { desensitizemap = Map.insert l tid (desensitizemap st) - , currentSensitize = Map.delete r (currentSensitize st) - } - - {- | Return a pair where the first element is all the `SSM.Core.Syntax.Sensitize` - values and the second component is the rest of the statements. -} - getSensitizes :: [Stm] -> ([Stm], [Stm]) - getSensitizes xs = (takeWhile isSensitize xs, dropWhile isSensitize xs) - - -- | Returns @True@ if a statement is a `SSM.Core.Syntax.Stm.Sensitize` value - isSensitize :: Stm -> Bool - isSensitize (Sensitize _) = True - isSensitize _ = False + 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 32973d82..3d6f5fbf 100644 --- a/ssm/SSM/Backend/C/CodeGen.hs +++ b/ssm/SSM/Backend/C/CodeGen.hs @@ -294,10 +294,11 @@ wraps the statements of the procedure. The heavy lifting is performed by -} genStep :: Procedure -> TR (C.Definition, C.Definition) genStep p = do - let (cstmts, sensitizemap, desensitizemap, widestwait) = analyseWait p + let cstmts = toCStm $ body p + (widestwait, semap, demap) = primitiveTriggerIDs cstmts modify $ \st -> st { numwaits = widestwait } _ <- nextCase -- Toss away 0th case - cases <- concat <$> mapM (genCase sensitizemap desensitizemap) cstmts + cases <- concat <$> mapM (genCase semap demap) cstmts locs <- gets locals final <- nextCase let @@ -371,7 +372,7 @@ 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 :: Map.Map Int Int -> Map.Map Int Int -> CStm -> TR [C.Stm] +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 @@ -418,7 +419,7 @@ genCase sensitizemap desensitizemap (Numbered n stm) = case stm of Sensitize r -> do -- fetch the id of the trigger to sensitize on - let trigid = case Map.lookup n sensitizemap of + 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 ++ @@ -429,7 +430,7 @@ genCase sensitizemap desensitizemap (Numbered n stm) = case stm of ] Desensitize r -> do - let trigid = case Map.lookup n desensitizemap of + 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 ++ diff --git a/ssm/SSM/Backend/C/Types.hs b/ssm/SSM/Backend/C/Types.hs index 1fbe344f..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 @@ -43,3 +45,34 @@ data CStm = Numbered Int Stm -- ^ Annotate a statement with a numbe | 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 From b59d7e8a24e48f85afe40844cc4bbeb70ea917b6 Mon Sep 17 00:00:00 2001 From: Robert Krook Date: Thu, 2 Sep 2021 14:35:24 +0200 Subject: [PATCH 10/10] document --- ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs | 168 ++++++++------------- ssm/SSM/Backend/C/CodeGen.hs | 10 +- 2 files changed, 71 insertions(+), 107 deletions(-) diff --git a/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs b/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs index f12ebe8a..c72e95a8 100644 --- a/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs +++ b/ssm/SSM/Backend/C/Analysis/WaitAnalysis.hs @@ -1,127 +1,87 @@ -{- | This module implements an analysis pass that annotates the body of a procedure with -information about which triggers to sensitize on. - -Earlier in the project, there was a single statement @Wait :: [Reference] -> Stm@ and -no @Yield :: Stm@ statement. When generating code for @Wait@ you immediately knew how -many references you needed to sensitize (since you had them all in that list) and you -could record that you are now sensitizing @n@ references, to know how many unique -triggers you're going to need. - -When the syntax was split up into the more fine-grained statements -`Sensitize`, `Desensitize` and -`Yield` in favour of @Wait@, this information become lost. When -generating code for a single `Sensitize` statement, it is not clear -how many references you are waiting on in total, or which of them in the sequence this -is. This makes it hard to know which trigger ID to sensitize on. - -What this module does is that it implement an analysis pass that infers the now lost -information from the sequence of statements that make up a procedure body. It will -return the same procedure body as before, but where each statement has been given a -unique @Int@ ID. Alongside these new statements two maps are produced. They associate -a statement ID with a trigger ID. So if you generate code for @Numbered n (Sensitize r)@, -you will look up which ID @r@ should be @Sensitized@ on by checking which trigger ID @n@ -is associated with in the sensitize map. Lastly, the size of the widest wait is inferred -from the procedure body and returned. - -@ -> analyseWait [ CreateRef r1 (Ref TInt) - , SetRef r1 5 - , CreateRef r2 (Ref TBool) - , SetRef r2 False - , Sensitize r1 - , Sensitize r2 - , Yield - , Desensitize r1 - , Desensitize r2 - , SetRef r2 True] -( [ Numbered 1 $ CreateRef r1 $ Ref TInt - , Numbered 2 $ SetRef r2 5) - , Numbered 3 $ CreateRef r2 $ Ref TBool - , Numbered 4 $ SetRef r2 False - , Numbered 5 $ Sensitize r1 - , Numbered 6 $ Sensitize r2 - , Numbered 7 $ Yield - , Numbered 8 4 Desensitize r1 - , Numbered 9 $ Desensitize r2 - , Numbered 10 $ SetRef r2 True] -, [ (5, 1), (6, 2)] -, [ (8, 1), (9, 2)] -, 2 -) -@ - -It's a bit crude, and should probably be made better later on when we wish to perform -different analysis passes. In particular, I am not too fond of the makeshift datatype -I implemented to number the statements. +{- | 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 where +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 - ) + ( Desensitize + , If + , Sensitize + , While + ) ) import Control.Monad.State ( State - , gets + , execState , get - , put + , gets , modify + , put , runState - , execState ) import qualified Data.Map as Map --- | Keys of the sensitize/desensitize map are pairs of references and statement numbers -type TriggerKey = (Reference, Int) --- | A map associating `TriggerKey` with a trigger ID -type TriggerMap = Map.Map TriggerKey Int - -- | State for the primitive trigger scheme -type PrimSt = (Int, Map.Map Reference Int, TriggerMap, TriggerMap) +type PrimSt + = ( Int + , Map.Map Reference Int + , Map.Map (Reference, Int) Int + , Map.Map (Reference, Int) Int + ) + +{- | Return a triple containing --- | Return (how many unique triggers are needed, sensitize map, desensitize map) -primitiveTriggerIDs :: [CStm] -> (Int, TriggerMap, TriggerMap) + 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 + 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, + {- | 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 + 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 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) + -- | 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 3d6f5fbf..5475a80d 100644 --- a/ssm/SSM/Backend/C/CodeGen.hs +++ b/ssm/SSM/Backend/C/CodeGen.hs @@ -294,9 +294,13 @@ wraps the statements of the procedure. The heavy lifting is performed by -} genStep :: Procedure -> TR (C.Definition, C.Definition) genStep p = do - let cstmts = toCStm $ body p - (widestwait, semap, demap) = primitiveTriggerIDs cstmts + -- 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 semap demap) cstmts locs <- gets locals @@ -366,7 +370,7 @@ genStep p = 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