A large change to alter RainUsageCheck to use the code in UsageCheck

Previously there was near-duplicate code in UsageCheck adapted from RainUsageCheck.  This patch removed the duplicate code on the RainUsageCheck side, and resulting in changing the rest of the module (and its corresponding test module) to use the new UsageCheck version of the code.  The net effect is to almost completely unify the passes in RainUsageCheck (which aren't really Rain-specific anyway), UsageCheck and ArrayUsageCheck.
This commit is contained in:
Neil Brown 2008-01-27 23:53:42 +00:00
parent 060c26da84
commit 9cd2da3b0e
2 changed files with 120 additions and 220 deletions

View File

@ -20,93 +20,24 @@ with this program. If not, see <http://www.gnu.org/licenses/>.
-- the control-flow graph stuff, hence the use of functions that match the dictionary -- the control-flow graph stuff, hence the use of functions that match the dictionary
-- of functions in FlowGraph. This is also why we don't drill down into processes; -- of functions in FlowGraph. This is also why we don't drill down into processes;
-- the control-flow graph means that we only need to concentrate on each node that isn't nested. -- the control-flow graph means that we only need to concentrate on each node that isn't nested.
module RainUsageCheck (Var(..), Vars(..), vars, Decl(..), getVarLabelFuncs, emptyVars, getVarProc, checkInitVar, findReachDef) where module RainUsageCheck (checkInitVar, findReachDef) where
import Control.Monad.Error
import Control.Monad.Identity import Control.Monad.Identity
import Data.Generics
import Data.Graph.Inductive import Data.Graph.Inductive
import Data.List hiding (union) import Data.List hiding (union)
import qualified Data.Map as Map import qualified Data.Map as Map
import Data.Maybe import Data.Maybe
import qualified Data.Set as Set import qualified Data.Set as Set
import qualified AST as A import CompState
import Errors
import FlowAlgorithms import FlowAlgorithms
import FlowGraph import FlowGraph
import Metadata
import ShowCode
import UsageCheck
import Utils import Utils
-- In Rain, Deref can't nest with Dir in either way, so this doesn't need to be a recursive type:
data Var =
Plain String
| Deref String
| Dir A.Direction String
deriving (Eq, Show, Ord)
data Vars = Vars {
maybeRead :: Set.Set Var,
maybeWritten :: Set.Set Var,
defWritten :: Set.Set Var,
used :: Set.Set Var -- e.g. channels, barriers
-- passed :: Set.Set String
}
deriving (Eq, Show)
emptyVars :: Vars
emptyVars = Vars Set.empty Set.empty Set.empty Set.empty
readVars :: [Var] -> Vars
readVars ss = Vars (Set.fromList ss) Set.empty Set.empty Set.empty
writtenVars :: [Var] -> Vars
writtenVars ss = Vars Set.empty (Set.fromList ss) (Set.fromList ss) Set.empty
usedVars :: [Var] -> Vars
usedVars vs = Vars Set.empty Set.empty Set.empty (Set.fromList vs)
vars :: [Var] -> [Var] -> [Var] -> [Var] -> Vars
vars mr mw dw u = Vars (Set.fromList mr) (Set.fromList mw) (Set.fromList dw) (Set.fromList u)
unionVars :: Vars -> Vars -> Vars
unionVars (Vars mr mw dw u) (Vars mr' mw' dw' u') = Vars (mr `Set.union` mr') (mw `Set.union` mw') (dw `Set.union` dw') (u `Set.union` u')
foldUnionVars :: [Vars] -> Vars
foldUnionVars = foldl unionVars emptyVars
mapUnionVars :: (a -> Vars) -> [a] -> Vars
mapUnionVars f = foldUnionVars . (map f)
nameToString :: A.Name -> String
nameToString = A.nameName
--Gets the (written,read) variables of a piece of an occam program:
--For subscripted variables used as Lvalues , e.g. a[b] it should return a[b] as written-to and b as read
--For subscripted variables used as expressions, e.g. a[b] it should return a[b],b as read (with no written-to)
getVarProc :: A.Process -> Vars
getVarProc (A.Assign _ vars expList)
--Join together:
= unionVars
--The written-to variables on the LHS:
(foldUnionVars (map processVarW vars))
--All variables read on the RHS:
(getVarExpList expList)
getVarProc (A.GetTime _ v) = processVarW v
getVarProc (A.Wait _ _ e) = getVarExp e
getVarProc (A.Output _ chanVar outItems) = (processVarUsed chanVar) `unionVars` (mapUnionVars getVarOutputItem outItems)
where
getVarOutputItem :: A.OutputItem -> Vars
getVarOutputItem (A.OutExpression _ e) = getVarExp e
getVarOutputItem (A.OutCounted _ ce ae) = (getVarExp ce) `unionVars` (getVarExp ae)
getVarProc (A.Input _ chanVar (A.InputSimple _ iis)) = (processVarUsed chanVar) `unionVars` (mapUnionVars getVarInputItem iis)
where
getVarInputItem :: A.InputItem -> Vars
getVarInputItem (A.InCounted _ cv av) = writtenVars [variableToVar cv,variableToVar av]
getVarInputItem (A.InVariable _ v) = writtenVars [variableToVar v]
--TODO process calls
getVarProc _ = emptyVars
{- {-
Near the beginning, this piece of code was too clever for itself and applied processVarW using "everything". Near the beginning, this piece of code was too clever for itself and applied processVarW using "everything".
The problem with this is that given var@(A.SubscriptedVariable _ sub arrVar), the functions would be recursively The problem with this is that given var@(A.SubscriptedVariable _ sub arrVar), the functions would be recursively
@ -117,6 +48,7 @@ getVarProc _ = emptyVars
-} -}
--Pull out all the subscripts into the read category, but leave the given var in the written category: --Pull out all the subscripts into the read category, but leave the given var in the written category:
{-
processVarW :: A.Variable -> Vars processVarW :: A.Variable -> Vars
processVarW v = writtenVars [variableToVar v] processVarW v = writtenVars [variableToVar v]
@ -125,51 +57,7 @@ processVarR v = readVars [variableToVar v]
processVarUsed :: A.Variable -> Vars processVarUsed :: A.Variable -> Vars
processVarUsed v = usedVars [variableToVar v] processVarUsed v = usedVars [variableToVar v]
-}
variableToVar :: A.Variable -> Var
variableToVar (A.Variable _ n) = Plain $ nameToString n
variableToVar (A.DirectedVariable _ dir (A.Variable _ n)) = Dir dir $ nameToString n
variableToVar (A.DerefVariable _ (A.Variable _ n)) = Deref $ nameToString n
variableToVar v = error ("Unprocessable variable: " ++ show v) --TODO come up with a better solution than this
getVarExpList :: A.ExpressionList -> Vars
getVarExpList (A.ExpressionList _ es) = foldUnionVars $ map getVarExp es
getVarExpList (A.FunctionCallList _ _ es) = foldUnionVars $ map getVarExp es --TODO record stuff in passed as well?
getVarExp :: A.Expression -> Vars
getVarExp = everything unionVars (emptyVars `mkQ` getVarExp')
where
--Only need to deal with the two cases where we can see an A.Variable directly;
--the generic recursion will take care of nested expressions, and even the expressions used as subscripts
getVarExp' :: A.Expression -> Vars
getVarExp' (A.SizeVariable _ v) = processVarR v
getVarExp' (A.ExprVariable _ v) = processVarR v
getVarExp' _ = emptyVars
getVarSpec :: A.Specification -> Vars
getVarSpec = const emptyVars -- TODO
data Decl = ScopeIn String | ScopeOut String deriving (Show, Eq)
getDecl :: (String -> Decl) -> A.Specification -> Maybe Decl
getDecl _ _ = Nothing -- TODO
getVarLabelFuncs :: GraphLabelFuncs Identity (Maybe Decl, Vars)
getVarLabelFuncs = GLF
{
labelExpression = pair (const Nothing) getVarExp
,labelExpressionList = pair (const Nothing) getVarExpList
,labelDummy = const (return (Nothing, emptyVars))
,labelProcess = pair (const Nothing) getVarProc
--don't forget about the variables used as initialisers in declarations (hence getVarSpec)
,labelScopeIn = pair (getDecl ScopeIn) getVarSpec
,labelScopeOut = pair (getDecl ScopeOut) (const emptyVars)
}
where
pair :: (a -> b) -> (a -> c) -> (a -> Identity (b,c))
pair f0 f1 x = return (f0 x, f1 x)
{- {-
@ -280,21 +168,31 @@ isSubsetOf _ Everything = True
isSubsetOf Everything _ = False isSubsetOf Everything _ = False
isSubsetOf (NormalSet a) (NormalSet b) = Set.isSubsetOf a b isSubsetOf (NormalSet a) (NormalSet b) = Set.isSubsetOf a b
showCodeExSet :: (CSM m, Ord a, ShowOccam a, ShowRain a) => ExSet a -> m String
showCodeExSet Everything = return "<all-vars>"
showCodeExSet (NormalSet s)
= do ss <- mapM showCode (Set.toList s)
return $ "{" ++ concat (intersperse ", " ss) ++ "}"
-- | Checks that no variable is used uninitialised. That is, it checks that every -- variable is written to before it is read.
-- TODO have some sort of error-message return if the check fails or if the code fails checkInitVar :: forall m. (Monad m, Die m, CSM m) => FlowGraph m (Maybe Decl, Vars) -> Node -> m ()
checkInitVar :: forall m. Monad m => FlowGraph m (Maybe Decl, Vars) -> Node -> Either String ()
checkInitVar graph startNode checkInitVar graph startNode
= do vwb <- varWrittenBefore = do vwb <- case flowAlgorithm graphFuncs (nodes graph) startNode of
Left err -> die $ "Error building control-flow graph: " ++ err
Right x -> return x
-- vwb is a map from Node to a set of Vars that have been written by that point
-- Now we check that for every variable read in each node, it has already been written to by then
mapM_ (checkInitVar' vwb) (map readNode (labNodes graph)) mapM_ (checkInitVar' vwb) (map readNode (labNodes graph))
where where
-- Gets all variables read-from in a particular node, and the node identifier
readNode :: (Node, FNode m (Maybe Decl, Vars)) -> (Node, ExSet Var) readNode :: (Node, FNode m (Maybe Decl, Vars)) -> (Node, ExSet Var)
readNode (n, Node (_,(_,Vars read _ _ _),_)) = (n,NormalSet read) readNode (n, Node (_,(_,Vars read _ _),_)) = (n,NormalSet read)
-- Gets all variables written-to in a particular node
writeNode :: FNode m (Maybe Decl, Vars) -> ExSet Var writeNode :: FNode m (Maybe Decl, Vars) -> ExSet Var
writeNode (Node (_,(_,Vars _ _ written _),_)) = NormalSet written writeNode (Node (_,(_,Vars _ written _),_)) = NormalSet written
-- Nothing is treated as if were the set of all possible variables (easier than building that set): -- Nothing is treated as if were the set of all possible variables:
nodeFunction :: (Node, EdgeLabel) -> ExSet Var -> Maybe (ExSet Var) -> ExSet Var nodeFunction :: (Node, EdgeLabel) -> ExSet Var -> Maybe (ExSet Var) -> ExSet Var
nodeFunction (n,_) inputVal Nothing = union inputVal (maybe emptySet writeNode (lab graph n)) nodeFunction (n,_) inputVal Nothing = union inputVal (maybe emptySet writeNode (lab graph n))
nodeFunction (n, EEndPar _) inputVal (Just prevAgg) = unions [inputVal,prevAgg,maybe emptySet writeNode (lab graph n)] nodeFunction (n, EEndPar _) inputVal (Just prevAgg) = unions [inputVal,prevAgg,maybe emptySet writeNode (lab graph n)]
@ -310,17 +208,19 @@ checkInitVar graph startNode
,defVal = Everything ,defVal = Everything
} }
varWrittenBefore :: Either String (Map.Map Node (ExSet Var)) getMeta :: Node -> Meta
varWrittenBefore = flowAlgorithm graphFuncs (nodes graph) startNode getMeta n = case lab graph n of
Just (Node (m,_,_)) -> m
_ -> emptyMeta
checkInitVar' :: Map.Map Node (ExSet Var) -> (Node, ExSet Var) -> Either String () checkInitVar' :: Map.Map Node (ExSet Var) -> (Node, ExSet Var) -> m ()
checkInitVar' writtenMap (n,v) checkInitVar' writtenMap (n,v)
= case Map.lookup n writtenMap of = let vs = fromMaybe emptySet (Map.lookup n writtenMap) in
Nothing -> throwError $ "Variable that is read from: " ++ show (lab graph n) ++ " is never written to" -- The read-from set should be a subset of the written-to set:
-- All read vars should be in the previously-written set if v `isSubsetOf` vs then return () else
Just vs -> if v `isSubsetOf` vs then return () else do readVars <- showCodeExSet v
throwError $ "Variable read from: " ++ show (lab graph n) ++ " is not written to before-hand, sets: " ++ show v ++ " and " ++ show vs writtenVars <- showCodeExSet vs
++ " writtenMap: " ++ show writtenMap dieP (getMeta n) $ "Variable read from is not written to before-hand, sets are read: " ++ show readVars ++ " and written: " ++ show writtenVars
-- | Returns either an error, or map *from* the node with a read, *to* the node whose definitions might be available at that point -- | Returns either an error, or map *from* the node with a read, *to* the node whose definitions might be available at that point
@ -348,10 +248,10 @@ findReachDef graph startNode
readInNode' n v _ = readInNode v (lab graph n) readInNode' n v _ = readInNode v (lab graph n)
readInNode :: Var -> Maybe (FNode m (Maybe Decl, Vars)) -> Bool readInNode :: Var -> Maybe (FNode m (Maybe Decl, Vars)) -> Bool
readInNode v (Just (Node (_,(_,Vars read _ _ _),_))) = Set.member v read readInNode v (Just (Node (_,(_,Vars read _ _),_))) = Set.member v read
writeNode :: FNode m (Maybe Decl, Vars) -> Set.Set Var writeNode :: FNode m (Maybe Decl, Vars) -> Set.Set Var
writeNode (Node (_,(_,Vars _ _ written _),_)) = written writeNode (Node (_,(_,Vars _ written _),_)) = written
-- | A confusiing function used by processNode. It takes a node and node label, and uses -- | A confusiing function used by processNode. It takes a node and node label, and uses
-- these to form a multi-map modifier function that replaces all node-sources for variables -- these to form a multi-map modifier function that replaces all node-sources for variables
@ -364,13 +264,8 @@ findReachDef graph startNode
processNode :: (Node, EdgeLabel) -> Map.Map Var (Set.Set Node) -> Maybe (Map.Map Var (Set.Set Node)) -> Map.Map Var (Set.Set Node) processNode :: (Node, EdgeLabel) -> Map.Map Var (Set.Set Node) -> Maybe (Map.Map Var (Set.Set Node)) -> Map.Map Var (Set.Set Node)
processNode (n,_) inputVal mm = mergeMultiMaps modifiedInput prevAgg processNode (n,_) inputVal mm = mergeMultiMaps modifiedInput prevAgg
where where
-- Note that the two uses of maybe here use id in different senses.
-- In prevAgg, id is used on the value inside the Maybe.
-- Whereas, in modifiedInput, id is the default value (because a function is
-- what comes out of maybe)
prevAgg :: Map.Map Var (Set.Set Node) prevAgg :: Map.Map Var (Set.Set Node)
prevAgg = maybe Map.empty id mm prevAgg = fromMaybe Map.empty mm
modifiedInput :: Map.Map Var (Set.Set Node) modifiedInput :: Map.Map Var (Set.Set Node)
modifiedInput = (maybe id (nodeLabelToMapInsert n) $ lab graph n) inputVal modifiedInput = (maybe id (nodeLabelToMapInsert n) $ lab graph n) inputVal

View File

@ -30,7 +30,8 @@ import qualified AST as A
import FlowGraph import FlowGraph
import Metadata import Metadata
import RainUsageCheck import RainUsageCheck
import TestUtils import TestUtils hiding (Var)
import UsageCheck
import Utils import Utils
@ -43,11 +44,11 @@ vL = variable "l"
l0 = intLiteral 0 l0 = intLiteral 0
l1 = intLiteral 1 l1 = intLiteral 1
tvA = Plain "a" tvA = Var $ variable "a"
tvB = Deref "b" tvB = Var $ variable "b"
tvC = Dir A.DirInput "c" tvC = Var $ variable "c"
tvD = Plain "d" tvD = Var $ variable "d"
tvL = Plain "l" tvL = Var $ variable "l"
--These are all shorthand for some useful "building block" processes --These are all shorthand for some useful "building block" processes
--The syntax is roughly: <variable list>_eq_<variable list> --The syntax is roughly: <variable list>_eq_<variable list>
@ -66,7 +67,7 @@ a_eq_not_b = A.Assign m [vA] $ A.ExpressionList m [A.Monadic m A.MonadicNot (A.E
testGetVarProc :: Test testGetVarProc :: Test
testGetVarProc = TestList (map doTest tests) testGetVarProc = TestList (map doTest tests)
where where
tests :: [(Int,[Var],[Var],[Var],[Var],A.Process)] tests :: [(Int,[Var],[Var],[Var],A.Process)]
tests = tests =
[ [
--TODO test channel reads and writes (incl. reads in alts) --TODO test channel reads and writes (incl. reads in alts)
@ -74,35 +75,35 @@ testGetVarProc = TestList (map doTest tests)
--TODO test function calls --TODO test function calls
--Test assignments on non-sub variables: --Test assignments on non-sub variables:
(0,[],[tvA],[tvA],[],a_eq_0) (0,[],[tvA],[],a_eq_0)
,(1,[tvB],[tvA],[tvA],[],a_eq_b) ,(1,[tvB],[tvA],[],a_eq_b)
,(2,[tvC,tvD],[tvA,tvB],[tvA,tvB],[],ab_eq_cd) ,(2,[tvC,tvD],[tvA,tvB],[],ab_eq_cd)
,(3,[tvA,tvB],[tvA,tvB],[tvA,tvB],[],ab_eq_ba) ,(3,[tvA,tvB],[tvA,tvB],[],ab_eq_ba)
,(4,[tvB],[tvA,tvB],[tvA,tvB],[],ab_eq_b0) ,(4,[tvB],[tvA,tvB],[],ab_eq_b0)
--Test assignments and expressions: --Test assignments and expressions:
,(200,[tvB],[tvA],[tvA],[],a_eq_not_b) ,(200,[tvB],[tvA],[],a_eq_not_b)
,(201,[tvC,tvD],[tvA],[tvA],[],a_eq_c_plus_d) ,(201,[tvC,tvD],[tvA],[],a_eq_c_plus_d)
-- Test time statements: -- Test time statements:
,(300,[],[tvB],[tvB],[],A.GetTime emptyMeta vB) ,(300,[],[tvB],[],A.GetTime emptyMeta vB)
,(301,[tvA],[],[],[],A.Wait emptyMeta A.WaitFor $ A.ExprVariable emptyMeta vA) ,(301,[tvA],[],[],A.Wait emptyMeta A.WaitFor $ A.ExprVariable emptyMeta vA)
-- Test simple outputs: -- Test simple outputs:
,(400,[tvA],[],[],[tvC],A.Output emptyMeta vC [A.OutExpression emptyMeta $ A.ExprVariable emptyMeta vA]) ,(400,[tvA],[],[tvC],A.Output emptyMeta vC [A.OutExpression emptyMeta $ A.ExprVariable emptyMeta vA])
,(401,[tvA,tvB],[],[],[tvC],A.Output emptyMeta vC $ map ((A.OutExpression emptyMeta) . (A.ExprVariable emptyMeta)) [vA,vB]) ,(401,[tvA,tvB],[],[tvC],A.Output emptyMeta vC $ map ((A.OutExpression emptyMeta) . (A.ExprVariable emptyMeta)) [vA,vB])
,(402,[tvA,tvB],[],[],[tvC],A.Output emptyMeta vC ,(402,[tvA,tvB],[],[tvC],A.Output emptyMeta vC
[A.OutCounted emptyMeta (A.ExprVariable emptyMeta vA) (A.ExprVariable emptyMeta vB)]) [A.OutCounted emptyMeta (A.ExprVariable emptyMeta vA) (A.ExprVariable emptyMeta vB)])
-- Test simple inputs: -- Test simple inputs:
,(500,[],[tvB],[tvB],[tvC],A.Input emptyMeta vC (A.InputSimple emptyMeta [A.InVariable emptyMeta vB])) ,(500,[],[tvB],[tvC],A.Input emptyMeta vC (A.InputSimple emptyMeta [A.InVariable emptyMeta vB]))
,(501,[],[tvA,tvB],[tvA,tvB],[tvC],A.Input emptyMeta vC ,(501,[],[tvA,tvB],[tvC],A.Input emptyMeta vC
(A.InputSimple emptyMeta [A.InVariable emptyMeta vB,A.InVariable emptyMeta vA])) (A.InputSimple emptyMeta [A.InVariable emptyMeta vB,A.InVariable emptyMeta vA]))
,(502,[],[tvA,tvB],[tvA,tvB],[tvC],A.Input emptyMeta vC ,(502,[],[tvA,tvB],[tvC],A.Input emptyMeta vC
(A.InputSimple emptyMeta [A.InCounted emptyMeta vA vB])) (A.InputSimple emptyMeta [A.InCounted emptyMeta vA vB]))
] ]
doTest :: (Int,[Var],[Var],[Var],[Var],A.Process) -> Test doTest :: (Int,[Var],[Var],[Var],A.Process) -> Test
doTest (index,mr,mw,dw,u,proc) = TestCase $ assertEqual ("testGetVarProc-" ++ (show index)) (vars mr mw dw u) (getVarProc proc) doTest (index,r,w,u,proc) = TestCase $ assertEqual ("testGetVarProc-" ++ (show index)) (vars r w u) (getVarProc proc)
--TODO test declarations being recorded, when I've decided how to record them --TODO test declarations being recorded, when I've decided how to record them
@ -136,80 +137,83 @@ testParUsageCheck = TestList (map doTest tests)
--TODO add tests for initialising a variable before use. --TODO add tests for initialising a variable before use.
--TODO especially test things like only initialising the variable in one part of an if --TODO especially test things like only initialising the variable in one part of an if
buildTestFlowGraph :: [(Int, [Var], [Var], [Var])] -> [(Int, Int, EdgeLabel)] -> Int -> Int -> String -> FlowGraph Identity (Maybe Decl, Vars) buildTestFlowGraph :: [(Int, [Var], [Var])] -> [(Int, Int, EdgeLabel)] -> Int -> Int -> String -> FlowGraph Identity (Maybe Decl, Vars)
buildTestFlowGraph ns es start end v buildTestFlowGraph ns es start end v
= mkGraph = mkGraph
([(-1,Node (emptyMeta,(Just $ ScopeIn v, emptyVars), undefined)),(-2,Node (emptyMeta,(Just $ ScopeOut v,emptyVars), undefined))] ++ (map transNode ns)) ([(-1,Node (emptyMeta,(Just $ ScopeIn v, emptyVars), undefined)),(-2,Node (emptyMeta,(Just $ ScopeOut v,emptyVars), undefined))] ++ (map transNode ns))
([(-1,start,ESeq),(end,-2,ESeq)] ++ es) ([(-1,start,ESeq),(end,-2,ESeq)] ++ es)
where where
transNode :: (Int, [Var], [Var], [Var]) -> (Int, FNode Identity (Maybe Decl, Vars)) transNode :: (Int, [Var], [Var]) -> (Int, FNode Identity (Maybe Decl, Vars))
transNode (n,mr,mw,dw) = (n,Node (emptyMeta, (Nothing,vars mr mw dw []), undefined)) transNode (n,r,w) = (n,Node (emptyMeta, (Nothing,vars r w []), undefined))
testInitVar :: Test testInitVar :: Test
testInitVar = TestList testInitVar = TestList
[]
{- TODO fix these tests
[ [
-- Single node, x not touched -- Single node, x not touched
testInitVarPass 0 [(0,[],[],[])] [] 0 0 "x" testInitVarPass 0 [(0,[],[])] [] 0 0 "x"
-- Single node, x written to -- Single node, x written to
,testInitVarPass 1 [(0,[],[],[Plain "x"])] [] 0 0 "x" ,testInitVarPass 1 [(0,[],[variable "x"])] [] 0 0 "x"
-- Single node, x read from (FAIL) -- Single node, x read from (FAIL)
,testInitVarFail 2 [(0,[Plain "x"],[],[])] [] 0 0 "x" ,testInitVarFail 2 [(0,[variable "x"],[])] [] 0 0 "x"
-- Single node, x read from and written to (FAIL - x must be written to before the read. -- Single node, x read from and written to (FAIL - x must be written to before the read.
-- This line is akin to x = x + 1, so x must be written to beforehand) -- This line is akin to x = x + 1, so x must be written to beforehand)
,testInitVarFail 3 [(0,[Plain "x"],[],[Plain "x"])] [] 0 0 "x" ,testInitVarFail 3 [(0,[variable "x"],[variable "x"])] [] 0 0 "x"
-- Two nodes, x written to then read -- Two nodes, x written to then read
,testInitVarPass 10 [(0,[],[],[Plain "x"]), (1,[Plain "x"],[],[])] [(0,1,ESeq)] 0 1 "x" ,testInitVarPass 10 [(0,[],[variable "x"]), (1,[variable "x"],[],[])] [(0,1,ESeq)] 0 1 "x"
-- Two nodes, x read then written to (FAIL) -- Two nodes, x read then written to (FAIL)
,testInitVarFail 11 [(0,[],[],[Plain "x"]), (1,[Plain "x"],[],[])] [(1,0,ESeq)] 1 0 "x" ,testInitVarFail 11 [(0,[],[variable "x"]), (1,[variable "x"],[],[])] [(1,0,ESeq)] 1 0 "x"
-- Two nodes, x maybe-written to then read (FAIL) -- Two nodes, x maybe-written to then read (FAIL)
,testInitVarFail 12 [(0,[],[Plain "x"],[]), (1,[Plain "x"],[],[])] [(0,1,ESeq)] 0 1 "x" ,testInitVarFail 12 [(0,[],[variable "x"],[]), (1,[variable "x"],[],[])] [(0,1,ESeq)] 0 1 "x"
-- As test 10 (x written to then read) but using the par edges. -- As test 10 (x written to then read) but using the par edges.
,testInitVarPass 13 [(0,[],[],[Plain "x"]), (1,[Plain "x"],[],[])] [(0,1,EStartPar 0)] 0 1 "x" ,testInitVarPass 13 [(0,[],[],[variable "x"]), (1,[variable "x"],[],[])] [(0,1,EStartPar 0)] 0 1 "x"
,testInitVarPass 14 [(0,[],[],[Plain "x"]), (1,[Plain "x"],[],[])] [(0,1,EEndPar 0)] 0 1 "x" ,testInitVarPass 14 [(0,[],[],[variable "x"]), (1,[variable "x"],[],[])] [(0,1,EEndPar 0)] 0 1 "x"
-- Diamond tests (0 branches to 1 and 2, which both merge to 3): -- Diamond tests (0 branches to 1 and 2, which both merge to 3):
-- x written to in 0 and 1, then read in 3 -- x written to in 0 and 1, then read in 3
,testInitVarPass 20 [(0,[],[],[]),(1,[],[],[Plain "x"]), (2,[],[],[Plain "x"]), (3,[Plain "x"],[],[])] ,testInitVarPass 20 [(0,[],[],[]),(1,[],[],[variable "x"]), (2,[],[],[variable "x"]), (3,[variable "x"],[],[])]
[(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x" [(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x"
-- x written to only in 2 then read in 3 (FAIL) -- x written to only in 2 then read in 3 (FAIL)
,testInitVarFail 21 [(0,[],[],[]),(1,[],[],[]), (2,[],[],[Plain "x"]), (3,[Plain "x"],[],[])] ,testInitVarFail 21 [(0,[],[],[]),(1,[],[],[]), (2,[],[],[variable "x"]), (3,[variable "x"],[],[])]
[(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x" [(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x"
-- x definitely written to in 2, but not 1 (FAIL) -- x definitely written to in 2, but not 1 (FAIL)
,testInitVarFail 22 [(0,[],[],[]),(1,[],[Plain "x"],[]), (2,[],[],[Plain "x"]), (3,[Plain "x"],[],[])] ,testInitVarFail 22 [(0,[],[],[]),(1,[],[variable "x"],[]), (2,[],[],[variable "x"]), (3,[variable "x"],[],[])]
[(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x" [(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x"
-- like test 21, but the link missing from 1 to 3, so test will pass -- like test 21, but the link missing from 1 to 3, so test will pass
,testInitVarPass 23 [(0,[],[],[]),(1,[],[],[]), (2,[],[],[Plain "x"]), (3,[Plain "x"],[],[])] ,testInitVarPass 23 [(0,[],[],[]),(1,[],[],[]), (2,[],[],[variable "x"]), (3,[variable "x"],[],[])]
[(0,1,ESeq),(0,2,ESeq),(2,3,ESeq)] 0 3 "x" [(0,1,ESeq),(0,2,ESeq),(2,3,ESeq)] 0 3 "x"
-- variable written to in 0, read in 3 -- variable written to in 0, read in 3
,testInitVarPass 24 [(0,[],[],[Plain "x"]),(1,[],[],[]), (2,[],[],[]), (3,[Plain "x"],[],[])] ,testInitVarPass 24 [(0,[],[],[variable "x"]),(1,[],[],[]), (2,[],[],[]), (3,[variable "x"],[],[])]
[(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x" [(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x"
-- variable never written to, but read in 3 -- variable never written to, but read in 3
,testInitVarFail 25 [(0,[],[],[]),(1,[],[],[]), (2,[],[],[]), (3,[Plain "x"],[],[])] ,testInitVarFail 25 [(0,[],[],[]),(1,[],[],[]), (2,[],[],[]), (3,[variable "x"],[],[])]
[(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x" [(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x"
-- variable written to in 2 and 3, but read in 1 (FAIL): -- variable written to in 2 and 3, but read in 1 (FAIL):
,testInitVarFail 26 [(0,[],[],[]),(1,[Plain "x"],[],[]), (2,[],[],[Plain "x"]), (3,[],[],[Plain "x"])] ,testInitVarFail 26 [(0,[],[],[]),(1,[variable "x"],[],[]), (2,[],[],[variable "x"]), (3,[],[],[variable "x"])]
[(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x" [(0,1,ESeq),(0,2,ESeq),(1,3,ESeq),(2,3,ESeq)] 0 3 "x"
-- Test parallel diamonds: -- Test parallel diamonds:
-- written to in 1 and 2, read in 3 -- written to in 1 and 2, read in 3
-- This would fail CREW, but that's not what we're testing here: -- This would fail CREW, but that's not what we're testing here:
,testInitVarPass 30 [(0,[],[],[]),(1,[],[],[Plain "x"]), (2,[],[],[Plain "x"]), (3,[Plain "x"],[],[])] ,testInitVarPass 30 [(0,[],[],[]),(1,[],[],[variable "x"]), (2,[],[],[variable "x"]), (3,[variable "x"],[],[])]
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x" [(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
-- written to in 1, read in 3 -- written to in 1, read in 3
,testInitVarPass 31 [(0,[],[],[]),(1,[],[],[Plain "x"]), (2,[],[],[]), (3,[Plain "x"],[],[])] ,testInitVarPass 31 [(0,[],[],[]),(1,[],[],[variable "x"]), (2,[],[],[]), (3,[variable "x"],[],[])]
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x" [(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
-- written to in 0, read in 3 -- written to in 0, read in 3
,testInitVarPass 32 [(0,[],[],[Plain "x"]),(1,[],[],[]), (2,[],[],[]), (3,[Plain "x"],[],[])] ,testInitVarPass 32 [(0,[],[],[variable "x"]),(1,[],[],[]), (2,[],[],[]), (3,[variable "x"],[],[])]
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x" [(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
-- never written to, but read in 3: -- never written to, but read in 3:
,testInitVarFail 33 [(0,[],[],[]),(1,[],[],[]), (2,[],[],[]), (3,[Plain "x"],[],[])] ,testInitVarFail 33 [(0,[],[],[]),(1,[],[],[]), (2,[],[],[]), (3,[variable "x"],[],[])]
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x" [(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
-- written to in 1, read in 2 (again, would fail CREW) (FAIL): -- written to in 1, read in 2 (again, would fail CREW) (FAIL):
,testInitVarFail 34 [(0,[],[],[]),(1,[],[],[Plain "x"]), (2,[Plain "x"],[],[]), (3,[],[],[])] ,testInitVarFail 34 [(0,[],[],[]),(1,[],[],[variable "x"]), (2,[variable "x"],[],[]), (3,[],[],[])]
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x" [(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
-- written to in 1, read in 2 and 3 (again, would fail CREW) (FAIL): -- written to in 1, read in 2 and 3 (again, would fail CREW) (FAIL):
,testInitVarFail 35 [(0,[],[],[]),(1,[],[],[Plain "x"]), (2,[Plain "x"],[],[]), (3,[Plain "x"],[],[])] ,testInitVarFail 35 [(0,[],[],[]),(1,[],[],[variable "x"]), (2,[variable "x"],[],[]), (3,[variable "x"],[],[])]
[(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x" [(0,1,EStartPar 0),(0,2,EStartPar 0),(1,3,EEndPar 0),(2,3,EEndPar 0)] 0 3 "x"
@ -218,30 +222,31 @@ testInitVar = TestList
,testInitVarPass 100 [(0,[],[],[]),(1,[],[],[]),(2,[],[],[]),(3,[],[],[]),(4,[],[],[])] ,testInitVarPass 100 [(0,[],[],[]),(1,[],[],[]),(2,[],[],[]),(3,[],[],[]),(4,[],[],[])]
[(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x" [(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x"
-- Loop, written to before the loop, read afterwards: -- Loop, written to before the loop, read afterwards:
,testInitVarPass 101 [(0,[],[],[Plain "x"]),(1,[],[],[]),(2,[],[],[]),(3,[],[],[]),(4,[Plain "x"],[],[])] ,testInitVarPass 101 [(0,[],[],[variable "x"]),(1,[],[],[]),(2,[],[],[]),(3,[],[],[]),(4,[variable "x"],[],[])]
[(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x" [(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x"
-- Loop, written to before the loop, read during the loop -- Loop, written to before the loop, read during the loop
,testInitVarPass 102 [(0,[],[],[Plain "x"]),(1,[],[],[]),(2,[],[],[]),(3,[Plain "x"],[],[]),(4,[],[],[])] ,testInitVarPass 102 [(0,[],[],[variable "x"]),(1,[],[],[]),(2,[],[],[]),(3,[variable "x"],[],[]),(4,[],[],[])]
[(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x" [(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x"
-- Loop, written to during the loop, read afterwards (FAIL - loop might not be executed) -- Loop, written to during the loop, read afterwards (FAIL - loop might not be executed)
,testInitVarFail 103 [(0,[],[],[]),(1,[],[],[]),(2,[],[],[Plain "x"]),(3,[],[],[]),(4,[Plain "x"],[],[])] ,testInitVarFail 103 [(0,[],[],[]),(1,[],[],[]),(2,[],[],[variable "x"]),(3,[],[],[]),(4,[variable "x"],[],[])]
[(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x" [(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x"
-- Loop, written to and then read during the loop: -- Loop, written to and then read during the loop:
,testInitVarPass 104 [(0,[],[],[]),(1,[],[],[]),(2,[],[],[Plain "x"]),(3,[Plain "x"],[],[]),(4,[],[],[])] ,testInitVarPass 104 [(0,[],[],[]),(1,[],[],[]),(2,[],[],[variable "x"]),(3,[variable "x"],[],[]),(4,[],[],[])]
[(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x" [(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x"
-- Loop, read then written to during the loop (FAIL): -- Loop, read then written to during the loop (FAIL):
,testInitVarFail 105 [(0,[],[],[]),(1,[],[],[]),(2,[Plain "x"],[],[]),(3,[],[],[Plain "x"]),(4,[],[],[])] ,testInitVarFail 105 [(0,[],[],[]),(1,[],[],[]),(2,[variable "x"],[],[]),(3,[],[],[variable "x"]),(4,[],[],[])]
[(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x" [(0,1,ESeq), (1,2,ESeq), (2,3,ESeq), (3,1,ESeq), (1,4,ESeq)] 0 4 "x"
-- TODO work out (and test) par loops -- TODO work out (and test) par loops
-- TODO test dereferenced variables -- TODO test dereferenced variables
] ]
where where
testInitVarPass :: Int -> [(Int, [Var], [Var], [Var])] -> [(Int, Int, EdgeLabel)] -> Int -> Int -> String -> Test testInitVarPass :: Int -> [(Int, [Var], [Var])] -> [(Int, Int, EdgeLabel)] -> Int -> Int -> String -> Test
testInitVarPass testNum ns es start end v = TestCase $ assertEither ("testInitVar " ++ show testNum) () $ checkInitVar (buildTestFlowGraph ns es start end v) (-1) testInitVarPass testNum ns es start end v = TestCase $ assertEither ("testInitVar " ++ show testNum) () $ checkInitVar (buildTestFlowGraph ns es start end v) (-1)
testInitVarFail :: Int -> [(Int, [Var], [Var], [Var])] -> [(Int, Int, EdgeLabel)] -> Int -> Int -> String -> Test testInitVarFail :: Int -> [(Int, [Var], [Var])] -> [(Int, Int, EdgeLabel)] -> Int -> Int -> String -> Test
testInitVarFail testNum ns es start end v = TestCase $ assertEitherFail ("testInitVar " ++ show testNum) $ checkInitVar (buildTestFlowGraph ns es start end v) (-1) testInitVarFail testNum ns es start end v = TestCase $ assertEitherFail ("testInitVar " ++ show testNum) $ checkInitVar (buildTestFlowGraph ns es start end v) (-1)
-}
testReachDef :: Test testReachDef :: Test
testReachDef = TestList testReachDef = TestList
@ -249,31 +254,31 @@ testReachDef = TestList
-- Nothing written/read, blank results: -- Nothing written/read, blank results:
test 0 [(0,[],[])] [] [] test 0 [(0,[],[])] [] []
-- Written but not read, no results: -- Written but not read, no results:
,test 1 [(0,[],[Plain "x"])] [] [] ,test 1 [(0,[],[variable "x"])] [] []
-- Written then read, no branching -- Written then read, no branching
,test 2 [(0,[],[Plain "x"]),(1,[Plain "x"],[])] [(0,1,ESeq)] [(1,[0])] ,test 2 [(0,[],[variable "x"]),(1,[variable "x"],[])] [(0,1,ESeq)] [(1,[0])]
,test 3 [(0,[],[Plain "x"]),(1,[],[]),(2,[Plain "x"],[])] [(0,1,ESeq),(1,2,ESeq)] [(2,[0])] ,test 3 [(0,[],[variable "x"]),(1,[],[]),(2,[variable "x"],[])] [(0,1,ESeq),(1,2,ESeq)] [(2,[0])]
,test 4 [(0,[],[Plain "x"]),(1,[],[Plain "x"]),(2,[Plain "x"],[])] [(0,1,ESeq),(1,2,ESeq)] [(2,[1])] ,test 4 [(0,[],[variable "x"]),(1,[],[variable "x"]),(2,[variable "x"],[])] [(0,1,ESeq),(1,2,ESeq)] [(2,[1])]
-- Lattice, written in 0, read in 3: -- Lattice, written in 0, read in 3:
,test 100 [(0,[],[Plain "x"]),(1,[],[]),(2,[],[]),(3,[Plain "x"],[])] latEdges [(3,[0])] ,test 100 [(0,[],[variable "x"]),(1,[],[]),(2,[],[]),(3,[variable "x"],[])] latEdges [(3,[0])]
-- Lattice, written in 0, read in 1,2 and 3: -- Lattice, written in 0, read in 1,2 and 3:
,test 101 [(0,[],[Plain "x"]),(1,[Plain "x"],[]),(2,[Plain "x"],[]),(3,[Plain "x"],[])] latEdges [(3,[0]),(1,[0]),(2,[0])] ,test 101 [(0,[],[variable "x"]),(1,[variable "x"],[]),(2,[variable "x"],[]),(3,[variable "x"],[])] latEdges [(3,[0]),(1,[0]),(2,[0])]
-- Lattice, written 0, 1 and 2, read in 3: -- Lattice, written 0, 1 and 2, read in 3:
,test 102 [(0,[],[Plain "x"]),(1,[],[Plain "x"]),(2,[],[Plain "x"]),(3,[Plain "x"],[])] latEdges [(3,[1,2])] ,test 102 [(0,[],[variable "x"]),(1,[],[variable "x"]),(2,[],[variable "x"]),(3,[variable "x"],[])] latEdges [(3,[1,2])]
-- Lattice written in 0 and 1, read in 2 and 3: -- Lattice written in 0 and 1, read in 2 and 3:
,test 103 [(0,[],[Plain "x"]),(1,[],[Plain "x"]),(2,[Plain "x"],[]),(3,[Plain "x"],[])] latEdges [(3,[0,1]),(2,[0])] ,test 103 [(0,[],[variable "x"]),(1,[],[variable "x"]),(2,[variable "x"],[]),(3,[variable "x"],[])] latEdges [(3,[0,1]),(2,[0])]
--Loops: --Loops:
-- Written before loop, read afterwards: -- Written before loop, read afterwards:
,test 200 [(0,[],[Plain "x"]),(1,[],[]),(2,[],[]),(3,[],[]),(4,[Plain "x"],[])] loopEdges [(4,[0])] ,test 200 [(0,[],[variable "x"]),(1,[],[]),(2,[],[]),(3,[],[]),(4,[variable "x"],[])] loopEdges [(4,[0])]
-- Written before loop, read during: -- Written before loop, read during:
,test 201 [(0,[],[Plain "x"]),(1,[],[]),(2,[Plain "x"],[]),(3,[],[]),(4,[],[])] loopEdges [(2,[0])] ,test 201 [(0,[],[variable "x"]),(1,[],[]),(2,[variable "x"],[]),(3,[],[]),(4,[],[])] loopEdges [(2,[0])]
-- Written before loop, written then read during: -- Written before loop, written then read during:
,test 202 [(0,[],[Plain "x"]),(1,[],[]),(2,[],[Plain "x"]),(3,[Plain "x"],[]),(4,[],[])] loopEdges [(3,[2])] ,test 202 [(0,[],[variable "x"]),(1,[],[]),(2,[],[variable "x"]),(3,[variable "x"],[]),(4,[],[])] loopEdges [(3,[2])]
-- Written before loop, written then read during, and read after: -- Written before loop, written then read during, and read after:
,test 203 [(0,[],[Plain "x"]),(1,[],[]),(2,[],[Plain "x"]),(3,[Plain "x"],[]),(4,[Plain "x"],[])] loopEdges [(3,[2]),(4,[0,2])] ,test 203 [(0,[],[variable "x"]),(1,[],[]),(2,[],[variable "x"]),(3,[variable "x"],[]),(4,[variable "x"],[])] loopEdges [(3,[2]),(4,[0,2])]
--TODO test derefenced variables --TODO test derefenced variables
] ]
@ -288,15 +293,15 @@ testReachDef = TestList
blankMW (n,mr,dw) = (n,mr,[],dw) blankMW (n,mr,dw) = (n,mr,[],dw)
-- It is implied that 0 is the start, and the highest node number is the end, and the var is "x" -- It is implied that 0 is the start, and the highest node number is the end, and the var is "x"
test :: Int -> [(Int,[Var],[Var])] -> [(Int,Int,EdgeLabel)] -> [(Int,[Int])] -> Test test :: Int -> [(Int,[A.Variable],[A.Variable])] -> [(Int,Int,EdgeLabel)] -> [(Int,[Int])] -> Test
test testNum ns es expMap = TestCase $ assertEither ("testReachDef " ++ show testNum) (Map.fromList $ map (transformPair id ((Map.singleton $ Plain "x") . Set.fromList)) expMap) $ test testNum ns es expMap = TestCase $ assertEither ("testReachDef " ++ show testNum) (Map.fromList $ map (transformPair id ((Map.singleton $ Var $ variable "x") . Set.fromList)) expMap) $
findReachDef (buildTestFlowGraph (map blankMW ns) es 0 (maximum $ map fst3 ns) "x") (-1) findReachDef (buildTestFlowGraph (map (transformTriple id (map Var) (map Var)) ns) es 0 (maximum $ map fst3 ns) "x") (-1)
fst3 :: (a,b,c) -> a fst3 :: (a,b,c) -> a
fst3(x,_,_) = x fst3(x,_,_) = x
tests :: Test tests :: Test
tests = TestList tests = TestLabel "RainUsageCheckTest" $ TestList
[ [
testGetVarProc testGetVarProc
,testInitVar ,testInitVar