diff --git a/checks/UsageCheckTest.hs b/checks/UsageCheckTest.hs index a10e543..e5aa478 100644 --- a/checks/UsageCheckTest.hs +++ b/checks/UsageCheckTest.hs @@ -184,69 +184,37 @@ testInitVar = TestList ,oX *:= oZ ] ]]] - - -- Single node, x not touched - ,testInitVarPass 0 [(0,[],[])] [] 0 0 "x" - -- Single node, x written to - ,testInitVarPass 1 [(0,[],[variable "x"])] [] 0 0 "x" - -- Single node, x read from (FAIL) - ,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. - -- This line is akin to x = x + 1, so x must be written to beforehand) - ,testInitVarFail 3 [(0,[variable "x"],[variable "x"])] [] 0 0 "x" - - -- Two nodes, x written to then read - ,testInitVarPass 10 [(0,[],[variable "x"]), (1,[variable "x"],[])] [(0,1,ESeq Nothing)] 0 1 "x" - -- Two nodes, x read then written to (FAIL) - ,testInitVarFail 11 [(0,[],[variable "x"]), (1,[variable "x"],[])] [(1,0,ESeq Nothing)] 1 0 "x" - -- As test 10 (x written to then read) but using the par edges. - ,testInitVarPass 13 [(0,[],[variable "x"]), (1,[variable "x"],[])] [(0,1,EStartPar 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): - -- x written to in 0 and 1, then read in 3 - ,testInitVarPass 20 [(0,[],[]),(1,[],[variable "x"]), (2,[],[variable "x"]), (3,[variable "x"],[])] - [(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x" - -- x written to only in 2 then read in 3 (FAIL) - ,testInitVarFail 21 [(0,[],[]),(1,[],[]), (2,[],[variable "x"]), (3,[variable "x"],[])] - [(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x" - -- x definitely written to in 2, but not 1 (FAIL) - ,testInitVarFail 22 [(0,[],[]),(1,[],[]), (2,[],[variable "x"]), (3,[variable "x"],[])] - [(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x" - -- like test 21, but the link missing from 1 to 3, so test will pass - ,testInitVarPass 23 [(0,[],[]),(1,[],[]), (2,[],[variable "x"]), (3,[variable "x"],[])] - [(0,1,ESeq Nothing),(0,2,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x" - -- variable written to in 0, read in 3 - ,testInitVarPass 24 [(0,[],[variable "x"]),(1,[],[]), (2,[],[]), (3,[variable "x"],[])] - [(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x" - -- variable never written to, but read in 3 - ,testInitVarFail 25 [(0,[],[]),(1,[],[]), (2,[],[]), (3,[variable "x"],[])] - [(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x" - -- variable written to in 2 and 3, but read in 1 (FAIL): - ,testInitVarFail 26 [(0,[],[]),(1,[variable "x"],[]), (2,[],[variable "x"]), (3,[],[variable "x"])] - [(0,1,ESeq Nothing),(0,2,ESeq Nothing),(1,3,ESeq Nothing),(2,3,ESeq Nothing)] 0 3 "x" - - -- Test parallel diamonds: - -- written to in 1 and 2, read in 3 - -- This would fail CREW, but that's not what we're testing here: - ,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" - -- written to in 1, read in 3 - ,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" - -- written to in 0, read in 3 - ,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" - -- never written to, but read in 3: - ,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" - -- written to in 1, read in 2 (again, would fail CREW) (FAIL): - ,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" - -- written to in 1, read in 2 and 3 (again, would fail CREW) (FAIL): - ,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" + ,test "Written to in all (two) IF guards, then self-assign" $ wrap $ + oSEQ [ + decl (return A.Int) oX [ + oIF [ + ifChoice (False, oX *:= return (3::Int)) + ,ifChoice (False, oX *:= return (4::Int)) + ] + ] + ,oX *:= oX + ] + ,testWarn "Written to in only one IF guards, then self-assign" $ wrap $ + oSEQ [ + decl (return A.Int) oX [ + oIF [ + ifChoice (False, oX *:= return (3::Int)) + ,ifChoice (False, oSKIP) + ] + ] + ,oX *:= oX + ] + ,testWarn "Read from in last IF guards, then self-assign" $ wrap $ + oSEQ [ + decl (return A.Int) oX [ + oIF [ + ifChoice (False, oX *:= return (3::Int)) + ,ifChoice (oX, oX *:= return (4::Int)) + ] + ] + ,oX *:= oX + ] -- Test loops (0 -> 1, 1 -> 2 -> 3 -> 1, 1 -> 4) -- Loop, nothing happens: diff --git a/common/OccamEDSL.hs b/common/OccamEDSL.hs index 5f716c2..dab7842 100644 --- a/common/OccamEDSL.hs +++ b/common/OccamEDSL.hs @@ -17,13 +17,15 @@ with this program. If not, see . -} -- | The necessary components for using an occam EDSL (for building test-cases). -module OccamEDSL (ExpInp, ExpInpT, oSEQ, oPAR, oPROC, oSKIP, oINT, - oCASE, oCASEinput, oALT, guard, +module OccamEDSL (ExpInp, ExpInpT, + oSEQ, oPAR, oPROC, oSKIP, oINT, + oCASE, oCASEinput, caseOption, inputCaseOption, + oALT, guard, + oIF, ifChoice, Occ, oA, oB, oC, oX, oY, oZ, p0, p1, p2, (*?), (*!), (*:=), (*+), decl, decl', decl'', oempty, testOccamPass, oprocess, testOccamPassWarn, testOccamPassTransform, ExpInpC(shouldComeFrom), - caseOption, inputCaseOption, becomes) where import Control.Monad.State hiding (guard) @@ -168,6 +170,15 @@ instance Castable (A.Structured A.Variant) A.Variant where makeStruct = id makePlain = A.Only emptyMeta +instance Castable A.Choice A.Choice where + makeStruct = A.Only emptyMeta + makePlain = id + +instance Castable (A.Structured A.Choice) A.Choice where + makeStruct = id + makePlain = A.Only emptyMeta + + p0, p1, p2 :: Castable c A.Process => O c p0 = return $ makePlain $ A.Skip emptyMeta p1 = return $ makePlain $ A.Seq emptyMeta (A.Several emptyMeta []) @@ -209,6 +220,15 @@ guard (inp, body) body' <- body return $ A.Only emptyMeta $ A.Alternative m (A.True emptyMeta) v im body' +oIF :: Castable c A.Process => [O (A.Structured A.Choice)] -> O c +oIF = liftM (makePlain . A.If emptyMeta . singlify . A.Several emptyMeta) . sequence + +ifChoice :: (CanBeExpression e, Castable c A.Choice) => (e, O A.Process) -> O c +ifChoice (e, body) + = do e' <- liftExpInp $ expr e + body' <- body + return $ makePlain $ A.Choice emptyMeta e' body' + singlify :: Data a => A.Structured a -> A.Structured a singlify (A.Several _ [s]) = s singlify ss = ss @@ -246,17 +266,15 @@ oZ = return $ variable "Z" dest <- liftExpInp bdest >>* inputItem return $ makePlain $ A.Input emptyMeta ch dest -(*!), (*:=) :: CanBeExpression e => ExpInp A.Variable -> ExpInp e -> O (A.Structured A.Process) +(*!), (*:=) :: (Castable r A.Process, CanBeExpression e) => ExpInp A.Variable -> ExpInp e -> O r (*!) bch bsrc = do ch <- liftExpInp bch src <- liftExpInp bsrc >>= (liftExpInp . expr) - return $ A.Only emptyMeta $ A.Output emptyMeta ch [A.OutExpression emptyMeta - src] + return $ makePlain $ A.Output emptyMeta ch [A.OutExpression emptyMeta src] (*:=) bdest bsrc = do dest <- liftExpInp bdest src <- liftExpInp bsrc >>= (liftExpInp . expr) - return $ A.Only emptyMeta $ A.Assign emptyMeta [dest] (A.ExpressionList emptyMeta - [src]) + return $ makePlain $ A.Assign emptyMeta [dest] (A.ExpressionList emptyMeta [src]) infix 8 *:= @@ -307,6 +325,10 @@ instance CanBeExpression A.Expression where instance CanBeExpression Int where expr = return . A.Literal emptyMeta A.Int . A.IntLiteral emptyMeta . show +instance CanBeExpression Bool where + expr True = return $ A.True emptyMeta + expr False = return $ A.False emptyMeta + instance CanBeExpression e => CanBeExpression (ExpInp e) where expr = join . liftM expr