From c3153526475444ff24221e77174d116cf35c30df Mon Sep 17 00:00:00 2001 From: Neil Brown Date: Mon, 9 Feb 2009 16:57:13 +0000 Subject: [PATCH] Added information in the flow graph edges as to when a condition becomes non-usable (e.g. when the branches of an IF merge again) --- checks/UsageCheckAlgorithms.hs | 5 ++- flow/FlowGraph.hs | 74 +++++++++++++++++++++------------- flow/FlowGraphTest.hs | 65 ++++++++++++++++------------- flow/FlowUtils.hs | 11 ++++- 4 files changed, 95 insertions(+), 60 deletions(-) diff --git a/checks/UsageCheckAlgorithms.hs b/checks/UsageCheckAlgorithms.hs index 666c980..3f52a2c 100644 --- a/checks/UsageCheckAlgorithms.hs +++ b/checks/UsageCheckAlgorithms.hs @@ -203,8 +203,9 @@ findConstraints graph startNode Just u -> let valFilt = filter (\e -> null $ intersect (listify (const True) e) [v | Var v <- Map.keys $ writtenVars $ nodeVars u]) $ - nub $ nodeVal ++ if e == ESeq (Just True) then maybeToList (nodeCond u) - else [] in + nub $ nodeVal ++ (case e of + ESeq (Just (_, Just True)) -> maybeToList (nodeCond u) + _ -> []) in nub $ valFilt ++ fromMaybe [] curAgg Nothing -> [] diff --git a/flow/FlowGraph.hs b/flow/FlowGraph.hs index 3e561a0..c8b78ee 100644 --- a/flow/FlowGraph.hs +++ b/flow/FlowGraph.hs @@ -253,52 +253,59 @@ buildStructuredCase (nStart, nEnd) (A.Spec _ spec str) route n' --> nEnd withDeclSpec spec $ buildStructuredCase (n, n') str (route33 route A.Spec) +-- While building an IF, we keep a stack of identifiers used for the various conditionals. +-- At the end of the block you must make sure there are edges that terminate all +-- these identifiers, after the joining together of all the branches buildStructuredIf :: forall mLabel mAlter label structType. (Monad mLabel, Monad mAlter) => (Node, Node) -> A.Structured A.Choice -> ASTModifier mAlter (A.Structured A.Choice) structType -> - GraphMaker mLabel mAlter label structType Node + StateT [Integer] (GraphMaker mLabel mAlter label structType) Node buildStructuredIf (prev, end) (A.Several _ ss) route = foldM foldIf prev (zip [0..] ss) where - foldIf :: Node -> (Int,A.Structured A.Choice) -> GraphMaker mLabel mAlter label structType Node + foldIf :: Node -> (Int,A.Structured A.Choice) -> + StateT [Integer] (GraphMaker mLabel mAlter label structType) Node foldIf prev (ind, s) = buildStructuredIf (prev, end) s $ route22 route A.Several @-> (routeList ind) buildStructuredIf (prev, end) (A.ProcThen _ p str) route - = do (ps, pe) <- buildProcess p (route23 route A.ProcThen) - prev --> ps + = do (ps, pe) <- lift $ buildProcess p (route23 route A.ProcThen) + lift $ prev --> ps buildStructuredIf (pe, end) str (route33 route A.ProcThen) buildStructuredIf (prev, end) (A.Only _ c) route - = buildOnlyChoice (prev, end) (route22 route A.Only) c + = do id <- lift getNextParEdgeId + modify (id:) + lift $ buildOnlyChoice (prev, end) (route22 route A.Only) c id buildStructuredIf (prev, end) (A.Spec _ spec@(A.Specification _ nm (A.Rep _ rep)) str) route = let alter = AlterReplicator $ route22 (route33 (route23 route A.Spec) A.Specification) A.Rep in - do repNode <- addNode' (findMeta rep) labelReplicator (nm, rep) alter - lastNode <- withDeclSpec spec $ buildStructuredIf (repNode, end) str (route33 route A.Spec) - prev --> repNode - lastNode --> repNode + do repNode <- lift $ addNode' (findMeta rep) labelReplicator (nm, rep) alter + lastNode <- liftWrapStateT (withDeclSpec spec) $ buildStructuredIf (repNode, end) str (route33 route A.Spec) + lift $ prev --> repNode + lift $ lastNode --> repNode return repNode buildStructuredIf (prev, end) (A.Spec _ spec str) route -- Specs are tricky in IFs, because they can scope out either -- at the end of a choice-block, or when moving on to the next -- choice. But these nodes are not the same because they have -- different connections leading out of them - = do nIn <- addNode' (findMeta spec) labelScopeIn spec (AlterSpec $ route23 route A.Spec) - nOutBlock <- addNode' (findMeta spec) labelScopeOut spec (AlterSpec $ route23 route A.Spec) - nOutNext <- addNode' (findMeta spec) labelScopeOut spec (AlterSpec $ route23 route A.Spec) + = do nIn <- lift $ addNode' (findMeta spec) labelScopeIn spec (AlterSpec $ route23 route A.Spec) + nOutBlock <- lift $ addNode' (findMeta spec) labelScopeOut spec (AlterSpec $ route23 route A.Spec) + nOutNext <- lift $ addNode' (findMeta spec) labelScopeOut spec (AlterSpec $ route23 route A.Spec) - last <- withDeclSpec spec $ buildStructuredIf (nIn, nOutBlock) str (route33 route A.Spec) - - prev --> nIn - when (last /= prev) $ -- Only add the edge if there was a block it's connected to! - nOutBlock --> end - last --> nOutNext - return nOutNext + last <- liftWrapStateT (withDeclSpec spec) $ buildStructuredIf (nIn, nOutBlock) str (route33 route A.Spec) + lift $ do + prev --> nIn + when (last /= prev) $ -- Only add the edge if there was a block it's connected to! + nOutBlock --> end + last --> nOutNext + return nOutNext -buildOnlyChoice :: (Monad mLabel, Monad mAlter) => (Node, Node) -> ASTModifier mAlter A.Choice structType -> A.Choice -> GraphMaker mLabel mAlter label structType Node -buildOnlyChoice (cPrev, cEnd) route (A.Choice m exp p) +buildOnlyChoice :: (Monad mLabel, Monad mAlter) => (Node, Node) -> ASTModifier mAlter A.Choice structType -> A.Choice -> + Integer -> GraphMaker mLabel mAlter label structType Node +buildOnlyChoice (cPrev, cEnd) route (A.Choice m exp p) edgeId = do nexp <- addNode' (findMeta exp) labelConditionalExpression exp $ AlterExpression $ route23 route A.Choice nexpf <- addDummyNode m route (nbodys, nbodye) <- buildProcess p $ route33 route A.Choice cPrev --> nexp - addEdge (ESeq $ Just True) nexp nbodys - addEdge (ESeq $ Just False) nexp nexpf + addEdge (ESeq $ Just (edgeId, Just True)) nexp nbodys + addEdge (ESeq $ Just (edgeId, Just False)) nexp nexpf nbodye --> cEnd return nexpf @@ -362,9 +369,12 @@ buildProcess (A.While m e p) route $ route23 route A.While) nAfter <- addDummyNode m route (start, end) <- buildProcess p (route33 route A.While) - addEdge (ESeq $ Just True) n start - addEdge (ESeq $ Just False) n nAfter - end --> n + edgeId <- getNextParEdgeId + addEdge (ESeq $ Just (edgeId, Just True)) n start + addEdge (ESeq $ Just (edgeId, Just False)) n nAfter + addEdge (ESeq $ Just (edgeId, Nothing)) end n + -- We are still taking the condition to be true after the while loop -- + -- and it will remain so until the variables are later modified return (n, nAfter) buildProcess (A.Case m e s) route = do nStart <- addNodeExpression (findMeta e) e (route23 route A.Case) @@ -373,9 +383,15 @@ buildProcess (A.Case m e s) route return (nStart, nEnd) buildProcess (A.If m s) route = do nStart <- addDummyNode m route - nEnd <- addDummyNode m route - buildStructuredIf (nStart, nEnd) s (route22 route A.If) - return (nStart, nEnd) + nFirstEnd <- addDummyNode m route + allEdgeIds <- flip execStateT [] $ buildStructuredIf (nStart, nFirstEnd) s (route22 route A.If) + nLastEnd <- foldM addEndEdge nFirstEnd allEdgeIds + return (nStart, nLastEnd) + where + --addEndEdge :: Node -> Integer -> GraphMaker mLabel mAlter label structType Node + addEndEdge n id = do n' <- addDummyNode m route + addEdge (ESeq (Just (id, Nothing))) n n' + return n' buildProcess (A.Alt m _ s) route = do nStart <- addDummyNode m route nEnd <- addDummyNode m route diff --git a/flow/FlowGraphTest.hs b/flow/FlowGraphTest.hs index ff5f717..7c9fd8a 100644 --- a/flow/FlowGraphTest.hs +++ b/flow/FlowGraphTest.hs @@ -277,22 +277,23 @@ testPar = TestLabel "testPar" $ TestList testWhile :: Test testWhile = TestLabel "testWhile" $ TestList [ - testGraph "testWhile 0" [(0,m0), (1,m1), (2, m2)] [0] [(0,1,ESeq $ Just True), (1,0,ESeq Nothing), - (0,2, ESeq $ Just False)] (A.While m2 (A.True m0) sm1) + testGraph "testWhile 0" [(0,m0), (1,m1), (2, m2)] [0] [(0,1,ESeq $ Just (0, + Just True)), (1,0,ESeq $ Just (0, Nothing)), (0,2, ESeq $ Just (0, Just False))] + (A.While m2 (A.True m0) sm1) ,testGraph "testWhile 1" [(2,m2), (3, m3), (5, m5), (8, m8)] [2] - [(2,3,ESeq $ Just True), (3,2,ESeq Nothing), (8,5,ESeq Nothing), (2,8, ESeq - $ Just False)] + [(2,3,ESeq $ Just (0, Just True)), (3,2,ESeq $ Just (0, Nothing)), (8,5,ESeq Nothing), (2,8, ESeq + $ Just (0, Just False))] (A.Seq m0 $ A.Several m1 [A.Only m9 $ A.While m8 (A.True m2) sm3,A.Only m4 sm5]) ,testGraph "testWhile 2" [(2,m2), (3, m3), (5, m5), (7, m7), (8, m8)] [7] - [(7,2,ESeq Nothing), (2,3,ESeq $ Just True), (3,2,ESeq Nothing), (2, 8, ESeq - $ Just False), (8,5,ESeq Nothing)] + [(7,2,ESeq Nothing), (2,3,ESeq $ Just (0, Just True)), (3,2,ESeq $ Just (0, Nothing)), + (2, 8, ESeq $ Just (0, Just False)), (8,5,ESeq Nothing)] (A.Seq m0 $ A.Several m1 [A.Only m6 sm7,A.Only m9 $ A.While m8 (A.True m2) sm3,A.Only m4 sm5]) ,testGraph "testWhile 3" [(2,m2), (3, m3), (5, m5), (7, m7), (9, m9), (8, m8)] [7] - [(7,2,ESeq Nothing), (2,3,ESeq $ Just True), (3,9,ESeq Nothing), (9,2,ESeq Nothing), (2, - 8, ESeq $ Just False), (8,5,ESeq Nothing)] + [(7,2,ESeq Nothing), (2,3,ESeq $ Just (0, Just True)), (3,9,ESeq Nothing), (9,2,ESeq $ + Just (0, Nothing)), (2, 8, ESeq $ Just (0, Just False)), (8,5,ESeq Nothing)] (A.Seq m0 $ A.Several m1 [A.Only m6 sm7,A.Only mU $ A.While m8 (A.True m2) $ A.Seq mU $ A.Several mU [A.Only mU sm3,A.Only mU sm9],A.Only m4 sm5]) ] @@ -320,21 +321,26 @@ testIf = TestLabel "testIf" $ TestList -- Remember that the last branch of an IF doesn't link to the end of the IF, because -- occam stops if no option is found. - testGraph "testIf 0" [(0,m0), (1,sub m0 1), (2,m2), (4, sub m2 1), (3,m3)] [0] - [(0,2,nt),(2,3,tr), (2,4, fal), (3,1,nt)] + testGraph "testIf 0" [(0,m0), (1,sub m0 1), (2,m2), (4, sub m2 1), (3,m3), (5, + sub m0 2)] [0] + [(0,2,nt),(2,3,tr 0), (2,4, fal 0), (3,1,nt), (1, 5, inv 0)] (A.If m0 $ ifs mU [(A.True m2, sm3)]) ,testGraph "testIf 1" [(0,m0), (1,sub m0 1), (2,m2), (12, m2 `sub` 1), (3,m3), - (4,m4), (14, m4 `sub` 1), (5, m5)] [0] - [(0,2,nt),(2,3,tr),(3,1,nt),(2,12, fal), (12, 4, nt), - (4,5,tr),(5,1,nt),(4,14,fal)] + (4,m4), (14, m4 `sub` 1), (5, m5), (11, sub m0 2), (21, + sub m0 3)] [0] + [(0,2,nt),(2,3,tr 0),(3,1,nt),(2,12, fal 0), (12, 4, nt), + (4,5,tr 1),(5,1,nt),(4,14,fal 1), (1, 11, inv 1), (11, + 21, inv 0)] (A.If m0 $ ifs mU [(A.True m2, sm3), (A.True m4, sm5)]) ,testGraph "testIf 2" [(0,m0), (1,sub m0 1), (2,m2), (12, m2 `sub` 1), (3,m3), - (4,m4), (14, m4 `sub` 1), (5, m5), (6, m6), (16, m6 `sub` 1),(7, m7)] [0] - [(0,2,nt),(2,3,tr),(3,1,nt),(2,12,fal),(12,4,nt), - (4,5,tr),(5,1,nt),(4,14,fal), - (14,6,nt),(6,7,tr),(7,1,nt),(6,16,fal)] + (4,m4), (14, m4 `sub` 1), (5, m5), (6, m6), (16, m6 `sub` 1),(7, m7), + (11, sub m0 2), (21, sub m0 3), (31, sub m0 4)] [0] + [(0,2,nt),(2,3,tr 0),(3,1,nt),(2,12,fal 0),(12,4,nt), + (4,5,tr 1),(5,1,nt),(4,14,fal 1), + (14,6,nt),(6,7,tr 2),(7,1,nt),(6,16,fal 2), + (1,11,inv 2), (11, 21, inv 1), (21, 31, inv 0)] (A.If m0 $ ifs mU [(A.True m2, sm3), (A.True m4, sm5), (A.True m6, sm7)]) {- @@ -345,26 +351,31 @@ testIf = TestLabel "testIf" $ TestList (A.If m0 $ A.Spec mU (someSpec m4) $ ifs mU [(A.True m2, sm3)]) -} - ,testGraph "testIf 10" [(0,m0), (1,sub m0 1), (2,m2), (12, m2 `sub` 1), (3,m3), (5, m5)] [0] - [(0,5,nt), (5,2,nt), (2,3,tr), (3,1,nt), (2,12, fal), (12, 5, nt)] + ,testGraph "testIf 10" [(0,m0), (1,sub m0 1), (2,m2), (12, m2 `sub` 1), (3,m3), (5, m5), + (11, sub m0 2)] [0] + [(0,5,nt), (5,2,nt), (2,3,tr 0), (3,1,nt), (2,12, fal 0), (12, 5, nt), (1, 11, inv 0)] (A.If m0 $ rep m5 $ ifs mU [(A.True m2, sm3)]) ,testGraph "testIf 11" [(0,m0), (1,sub m0 1), (2,m2), (12, m2 `sub` 1), (3,m3), (5, m5), (6, m6), (16, - m6 `sub` 1), (7, m7)] [0] - [(0,5,nt), (5,2,nt), (2,3,tr), (3,1,nt), (2,12,fal), (12, 6, nt), (6,7,tr), (7,1,nt), (6,16,fal),(16, 5, nt)] + m6 `sub` 1), (7, m7), (11, sub m0 2), (21, sub m0 3)] [0] + [(0,5,nt), (5,2,nt), (2,3,tr 0), (3,1,nt), (2,12,fal 0), (12, 6, nt), (6,7,tr + 1), (7,1,nt), (6,16,fal 1),(16, 5, nt), (1, 11, inv 1), (11, 21, inv 0)] (A.If m0 $ rep m5 $ ifs mU [(A.True m2, sm3), (A.True m6, sm7)]) ,testGraph "testIf 12" [(0,m0), (1,sub m0 1), (2,m2), (3,m3), (5, m5), (6, m6), (7, m7), (8, m8), (9, m9), - (12, m2 `sub` 1), (16, m6 `sub` 1), (18, m8 `sub` 1)] [0] - [(0,5,nt), (5,2,nt), (2,3,tr), (3,1,nt), (2,12,fal), (12, 6, nt), - (6,7,tr), (7,1,nt), (6,16,fal), (16, 5, nt), (5,8,nt), - (8,9,tr), (9,1,nt),(8,18,fal)] + (12, m2 `sub` 1), (16, m6 `sub` 1), (18, m8 `sub` 1), (11, sub m0 2), (21, + sub m0 3), (31, sub m0 4)] [0] + [(0,5,nt), (5,2,nt), (2,3,tr 0), (3,1,nt), (2,12,fal 0), (12, 6, nt), + (6,7,tr 1), (7,1,nt), (6,16,fal 1), (16, 5, nt), (5,8,nt), + (8,9,tr 2), (9,1,nt),(8,18,fal 2), (1,11, inv 2), (11, 21, inv 1), (21, 31, + inv 0)] (A.If m0 $ A.Several mU [rep m5 $ ifs mU [(A.True m2, sm3), (A.True m6, sm7)] , ifs mU [(A.True m8, sm9)]]) ] where - fal = ESeq $ Just False - tr = ESeq $ Just True + fal n = ESeq $ Just (n, Just False) + tr n = ESeq $ Just (n, Just True) + inv n = ESeq $ Just (n, Nothing) nt = ESeq Nothing ifs :: Meta -> [(A.Expression, A.Process)] -> A.Structured A.Choice diff --git a/flow/FlowUtils.hs b/flow/FlowUtils.hs index 21f2f28..efb1c86 100644 --- a/flow/FlowUtils.hs +++ b/flow/FlowUtils.hs @@ -39,7 +39,14 @@ import Utils -- Multiple Seq links means choice. -- Multiple Par links means a parallel branch. All outgoing par links should have the same identifier, -- and this identifier is unique and matches a later endpar link -data EdgeLabel = ESeq (Maybe Bool) | EStartPar Integer | EEndPar Integer deriving (Show, Eq, Ord) +-- +-- If a Seq link has a Just label, it indicates whether the condition at the source +-- node evaluated to True or False. Each such link has an associated Integer. +-- When you see that integer again in a Seq link with a Nothing for the bool value, +-- that is the point at which you can no longer assume the condition holds. So +-- for example, going into an IF block will have an Just (N, Just True) label, +-- and the end of that block will have a Just (N, Nothing) label. +data EdgeLabel = ESeq (Maybe (Integer, Maybe Bool)) | EStartPar Integer | EEndPar Integer deriving (Show, Eq, Ord) -- | A type used to build up tree-modifying functions. When given an inner modification function, -- it returns a modification function for the whole tree. The functions are monadic, to @@ -99,7 +106,7 @@ data GraphMakerState mAlter a b = GraphMakerState , nameStack :: [String] } -type GraphMaker mLabel mAlter a b c = ErrorT String (ReaderT (GraphLabelFuncs mLabel a) (StateT (GraphMakerState mAlter a b) mLabel)) c +type GraphMaker mLabel mAlter a b = ErrorT String (ReaderT (GraphLabelFuncs mLabel a) (StateT (GraphMakerState mAlter a b) mLabel)) -- | The GraphLabelFuncs type. These are a group of functions -- used to provide labels for different elements of AST.