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)
This commit is contained in:
parent
904b913ebd
commit
c315352647
|
@ -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 -> []
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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.
|
||||
|
|
Loading…
Reference in New Issue
Block a user