StatAnaCSP.hs revision 7ed9dd4cb1efebf38025cff55e9a28d0c274ef69
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Id$
5ba323da9f037264b4a356085e844889aedeac23Christian MaederDescription : static analysis for CspCASL
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian MaederCopyright : (c) Markus Roggenbach, Till Mossakowski, Uni Bremen 2004-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : M.Roggenbach@swansea.ac.uk
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : provisional
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederPortability : portable
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederStatic analysis for CSP-CASL
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maeder-}
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
23f2c59644866aa82e90de353e77f9f1d1b51b9aChristian Maedermodule CspCASL.StatAnaCSP where
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maederimport qualified Control.Monad as Monad
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport qualified Data.Map as Map
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport qualified Data.Maybe as Maybe
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maederimport qualified Data.Set as S
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederimport CASL.AS_Basic_CASL (FunKind(..), SORT, TERM(..), VAR)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport CASL.MixfixParser (emptyMix, Mix(..), makeRules, mkIdSets,
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder resolveMixfix, unite)
fc8c6570c7b4ee13f375eb607bed2290438573bfChristian Maederimport CASL.Overload (oneExpTerm)
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport CASL.Sign
950e053ba55ac9c7d9c26a1ab48bd00202b29511Christian Maederimport CASL.StaticAna (allOpIds, allPredIds)
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport Common.AS_Annotation
10397bcc134edbcfbe3ae2c7ea4c6080036aae22Christian Maederimport Common.Result
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport Common.GlobalAnnotations
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport qualified Common.Lib.Rel as Rel
af621d0066770895fd79562728e93099c8c52060Christian Maederimport Common.Id (Id, simpleIdToId)
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maederimport Common.Lib.State
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport Common.ExtSign
79d11c2e3ad242ebb241f5d4a5e98a674c0b986fChristian Maeder
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport CspCASL.AS_CspCASL
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport CspCASL.AS_CspCASL_Process
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport CspCASL.LocalTop (Obligation(..), unmetObs)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maederimport CspCASL.Print_CspCASL ()
f8f78a2c8796a387a4348cc672ae08e8d9f69315Christian Maederimport CspCASL.SignCSP
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederbasicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder -> Result (CspBasicSpec, ExtSign CspCASLSign (), [Named ()])
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederbasicAnalysisCspCASL (cc, sigma, _ga) = do
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder let (_, accSig) = runState (ana_BASIC_CSP cc) sigma
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder let ds = reverse $ envDiags accSig
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Result ds (Just ()) -- insert diagnostics
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder return (cc, mkExtSign accSig, [])
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederana_BASIC_CSP :: CspBasicSpec -> State CspCASLSign ()
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederana_BASIC_CSP cc = do checkLocalTops
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder mapM anaChanDecl (channels cc)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder mapM anaProcItem (proc_items cc)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder return ()
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- Analysis of local top elements
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | Check CspCASL signature for local top elements in subsorts.
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedercheckLocalTops :: State CspCASLSign ()
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedercheckLocalTops = do
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder sig <- get
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder let obs = unmetObs $ Rel.toList $ Rel.transClosure $ sortRel sig
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder addDiags (map lteError obs)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder return ()
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- | Add diagnostic error for every unmet local top element obligation.
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederlteError :: Obligation SORT -> Diagnosis
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaederlteError (Obligation x y z) = mkDiag Error msg ()
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder where msg = ("local top element obligation ("
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ++ (show x) ++ "<" ++ (show y) ++ "," ++ (show z)
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder ++ ") unfulfilled")
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder-- Analysis of channel declarations
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederanaChanDecl :: CHANNEL_DECL -> State CspCASLSign CHANNEL_DECL
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederanaChanDecl (ChannelDecl chanNames chanSort) = do
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder checkSorts [chanSort] -- check channel sort is known
9e0472be46104307b974fe5079bf5cc9e94a1a96Christian Maeder sig <- get
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder let ext = extendedInfo sig
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder oldChanMap = chans ext
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder newChanMap <- Monad.foldM (anaChannelName chanSort) oldChanMap chanNames
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder vds <- gets envDiags
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder put sig { extendedInfo = ext { chans = newChanMap }
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , envDiags = vds
792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder }
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder return (ChannelDecl chanNames chanSort)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederanaChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME ->
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian Maeder State CspCASLSign ChanNameMap
d976ba42e9d48c289f9c73147669c7e57b7aa98eChristian MaederanaChannelName s m chanName = do
986e0e9cf8c2358f455460b3fc75ce7c5dcf0973Christian Maeder sig <- get
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder if (show chanName) `S.member` (S.map show (sortSet sig))
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder then do let err = "channel name already in use as a sort name"
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder addDiags [mkDiag Error err chanName]
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder return m
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder else case Map.lookup chanName m of
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder Nothing -> return (Map.insert chanName s m) -- insert new.
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder Just e ->
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder if e == s
5ba323da9f037264b4a356085e844889aedeac23Christian Maeder then do let warn = "channel redeclared with same sort"
6a7e00a968cb0f3f9ccae19ab47ef3636c7e79bfChristian Maeder addDiags [mkDiag Warning warn chanName]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder return m -- already declared with this sort.
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder else do let err = "channel declared with multiple sorts"
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder addDiags [mkDiag Error err chanName]
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder return m
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder-- Analysis of process items
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
59c301c268f79cfde0a4c30a2c572a368db98da5Christian MaederanaProcItem :: PROC_ITEM -> State CspCASLSign ()
0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian MaederanaProcItem procItem =
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder case procItem of
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder (Proc_Decl name argSorts alpha) -> anaProcDecl name argSorts alpha
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder (Proc_Eq parmProcName procTerm) -> anaProcEq parmProcName procTerm
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder-- Analysis of process declarations
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederanaProcDecl :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder -> State CspCASLSign ()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederanaProcDecl name argSorts (ProcAlphabet commTypes _) = do
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder sig <- get
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder let ext = extendedInfo sig
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder oldProcDecls = procSet ext
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder newProcDecls <-
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder if name `Map.member` oldProcDecls
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder then do -- duplicate process declaration
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder let err = "process name declared more than once"
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder addDiags [mkDiag Error err name]
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder return oldProcDecls
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder else do -- new process declation
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder checkSorts argSorts -- check argument sorts are known
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder -- build alphabet: set of CommType values
5334aa8fe0b0d1eb8a1cad40b741aa07172773c9Christian Maeder alpha <- Monad.foldM (anaCommType sig) S.empty commTypes
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder let profile = (ProcProfile argSorts alpha)
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder return (Map.insert name profile oldProcDecls)
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder vds <- gets envDiags
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder put sig { extendedInfo = ext {procSet = newProcDecls }
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder , envDiags = vds
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder }
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder return ()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder-- Analysis of process equations
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederanaProcEq :: PARM_PROCNAME -> PROCESS -> State CspCASLSign ()
31a189d4cff554f78407cdc422480e84e99a6ec6Christian MaederanaProcEq (ParmProcname pn vs) proc = do
997c56f3bc74a703043010978e5013fdb074d659Christian Maeder sig <- get
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder let ext = extendedInfo sig
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder procDecls = procSet ext
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder prof = pn `Map.lookup` procDecls
8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder case prof of
8485da94b57d8b5135ee685b55c982b037ed4140Christian Maeder -- Only analyse a process if its name (and thus profile) is known
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder Just (ProcProfile procArgs procAlpha) ->
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder do gVars <- anaProcVars pn procArgs vs -- compute global vars
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder termAlpha <- anaProcTerm proc gVars Map.empty
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder checkCommAlphaSub termAlpha procAlpha proc "process equation"
ad187062b0009820118c1b773a232e29b879a2faChristian Maeder return ()
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Nothing ->
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder do addDiags [mkDiag Error "process equation for unknown process" pn]
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder return ()
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder vds <- gets envDiags
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder put sig { envDiags = vds }
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder return ()
dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maeder
53301de22afd7190981b363b57c48df86fcb50f7Christian Maeder-- Analysis of process variable names.
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian MaederanaProcVars :: PROCESS_NAME -> [SORT] -> [VAR] -> State CspCASLSign ProcVarMap
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederanaProcVars pn ss vs = do
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder case (compare (length ss) (length vs)) of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder LT -> do addDiags [mkDiag Error "too many process arguments" pn]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder return Map.empty
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder GT -> do addDiags [mkDiag Error "not enough process arguments" pn]
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder return Map.empty
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder EQ -> Monad.foldM anaProcVar Map.empty (zip vs ss)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian MaederanaProcVar :: ProcVarMap -> (VAR, SORT) -> State CspCASLSign ProcVarMap
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederanaProcVar old (v, s) = do
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder if v `Map.member` old
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder then do addDiags [mkDiag Error "process arg declared more than once" v]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder return old
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder else return (Map.insert v s old)
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder
f6f2955769bfe80dbb4cca3b3ee33c5a8a0f5355Christian Maeder-- Analysis of process terms
c1031ac42b3f3d7d0fe7d9d6b54423a092d473a0Christian Maeder
fce77b2785912d1abbcc3680088b235f534bdeffChristian MaederanaProcTerm :: PROCESS -> ProcVarMap -> ProcVarMap -> State CspCASLSign CommAlpha
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian MaederanaProcTerm proc gVars lVars = case proc of
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder NamedProcess name args _ ->
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder do addDiags [mkDiag Debug "Named process" proc]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder al <- anaNamedProc proc name args (lVars `Map.union` gVars)
ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder return al
039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder Skip _ ->
fe5dbb45b6a8abf34375b4bc5f2a81cda664c0e4Christian Maeder do addDiags [mkDiag Debug "Skip" proc]
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder return S.empty
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Stop _ ->
039b7a8265baaeab2ded2a3e3826c04f13364d87Christian Maeder do addDiags [mkDiag Debug "Stop" proc]
ac19566dc64536c38b5d1d3ae510fb8a07784c2fChristian Maeder return S.empty
3cafc73a998493f9ed3d5e934c0ab80bcfb465c2Christian Maeder Div _ ->
7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder do addDiags [mkDiag Debug "Div" proc]
021d7137df04ec1834911d99d90243a092841cedChristian Maeder return S.empty
021d7137df04ec1834911d99d90243a092841cedChristian Maeder Run es _ ->
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder do addDiags [mkDiag Debug "Run" proc]
5581c4644d91dcb9b7e2e7f6052f7cbf5f97b6deChristian Maeder comms <- anaEventSet es
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder return comms
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder Chaos es _ ->
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder do addDiags [mkDiag Debug "Chaos" proc]
7c554e9d4a39b8eb3b0881f20807c95dd8e793aeChristian Maeder comms <- anaEventSet es
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return comms
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder PrefixProcess e p _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "Prefix" proc]
adfdcfa67b7f12df6df7292e238c3f9a4b637980Christian Maeder (evComms, rcvMap) <- anaEvent e (lVars `Map.union` gVars)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder comms <- anaProcTerm p gVars (rcvMap `Map.union` lVars)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (comms `S.union` evComms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder InternalPrefixProcess v s p _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "Internal prefix" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder checkSorts [s] -- check sort is known
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder comms <- anaProcTerm p gVars (Map.insert v s lVars)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (S.insert (CommTypeSort s) comms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder ExternalPrefixProcess v s p _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "External prefix" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder checkSorts [s] -- check sort is known
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder comms <- anaProcTerm p gVars (Map.insert v s lVars)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (S.insert (CommTypeSort s) comms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Sequential p q _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "Sequential" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder pComms <- anaProcTerm p gVars lVars
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder qComms <- anaProcTerm q gVars Map.empty
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (pComms `S.union` qComms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder InternalChoice p q _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "InternalChoice" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder pComms <- anaProcTerm p gVars lVars
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder qComms <- anaProcTerm q gVars lVars
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (pComms `S.union` qComms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder ExternalChoice p q _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "ExternalChoice" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder pComms <- anaProcTerm p gVars lVars
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder qComms <- anaProcTerm q gVars lVars
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder return (pComms `S.union` qComms)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder Interleaving p q _ ->
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder do addDiags [mkDiag Debug "Interleaving" proc]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder pComms <- anaProcTerm p gVars lVars
7bf6d421b0ea31ae63f1fe04919942b931abda47Christian Maeder qComms <- anaProcTerm q gVars lVars
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder return (pComms `S.union` qComms)
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder SynchronousParallel p q _ ->
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder do addDiags [mkDiag Debug "Synchronous" proc]
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder pComms <- anaProcTerm p gVars lVars
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder qComms <- anaProcTerm q gVars lVars
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder return (pComms `S.union` qComms)
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder GeneralisedParallel p es q _ ->
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder do addDiags [mkDiag Debug "Generalised parallel" proc]
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder pComms <- anaProcTerm p gVars lVars
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder synComms <- anaEventSet es
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder qComms <- anaProcTerm q gVars lVars
908a6351595b57641353608c4449d5faa0d1adf8Christian Maeder return (S.unions [pComms, qComms, synComms])
bb3bdd4a260606a6184b5f5a5774ca6632ca597aChristian Maeder AlphabetisedParallel p esp esq q _ ->
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder do addDiags [mkDiag Debug "Alphabetised parallel" proc]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder pComms <- anaProcTerm p gVars lVars
e76e6a43f51438215737d6fc176c89da05bb86daChristian Maeder pSynComms <- anaEventSet esp
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder checkCommAlphaSub pSynComms pComms proc "alphabetised parallel, left"
7de39d39bc1700cc8a9bb9df90b920aad9e18d4aChristian Maeder qSynComms <- anaEventSet esq
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder qComms <- anaProcTerm q gVars lVars
ff9a53595208f532c25ac5168f772f48fd80fdb5Christian Maeder checkCommAlphaSub qSynComms qComms proc "alphabetised parallel, right"
return (pComms `S.union` qComms)
Hiding p es _ ->
do addDiags [mkDiag Debug "Hiding" proc]
pComms <- anaProcTerm p gVars lVars
hidComms <- anaEventSet es
return (pComms `S.union` hidComms)
RenamingProcess p r _ ->
do addDiags [mkDiag Debug "Renaming" proc]
pComms <- anaProcTerm p gVars lVars
renAlpha <- anaRenaming r
return (pComms `S.union` renAlpha)
ConditionalProcess _ p q _ ->
do addDiags [mkDiag Debug "Conditional" proc]
pComms <- anaProcTerm p gVars lVars
qComms <- anaProcTerm q gVars lVars
let fComms = S.empty -- XXX get formula sorts here
return (S.unions [pComms, qComms, fComms])
anaNamedProc :: PROCESS -> PROCESS_NAME -> [TERM ()] -> ProcVarMap ->
State CspCASLSign CommAlpha
anaNamedProc proc pn terms procVars = do
sig <- get
let ext = extendedInfo sig
procDecls = procSet ext
prof = pn `Map.lookup` procDecls
case prof of
Just (ProcProfile _ permAlpha) ->
do mapM (anaTermCspCASL procVars) terms
-- XXX Check casting of terms
return permAlpha
Nothing ->
do addDiags [mkDiag Error "unknown process name" proc]
return S.empty
-- Analysis of event sets and communication types
anaEventSet :: EVENT_SET -> State CspCASLSign CommAlpha
anaEventSet (EventSet es _) = do
sig <- get
comms <- Monad.foldM (anaCommType sig) S.empty es
vds <- gets envDiags
put sig { envDiags = vds }
return comms
anaCommType :: CspCASLSign -> CommAlpha -> COMM_TYPE -> State CspCASLSign CommAlpha
anaCommType sig alpha ct =
if ctSort `S.member` (sortSet sig)
then -- ct is a sort name; insert sort into alpha
do return (S.insert (CommTypeSort ctSort) alpha)
else -- ct not a sort name, so should be a channel name
case Map.lookup ct (chans $ extendedInfo sig) of
Just s -> -- ct is a channel name; insert typed chan name into alpha
return (S.insert (mkTypedChan ct s) alpha)
Nothing -> do let err = "not a sort or channel name"
addDiags [mkDiag Error err ct]
return alpha
where ctSort = simpleIdToId ct
mkTypedChan c s = CommTypeChan $ TypedChanName c s
-- Analysis of events
anaEvent :: EVENT -> ProcVarMap -> State CspCASLSign (CommAlpha, ProcVarMap)
anaEvent e vars = case e of
TermEvent t _ -> anaTermEvent t vars
ChanSend c t _ -> anaChanSend c t vars
ChanNonDetSend c v s _ -> anaChanBinding c v s
ChanRecv c v s _ -> anaChanBinding c v s
anaTermEvent :: (TERM ()) -> ProcVarMap ->
State CspCASLSign (CommAlpha, ProcVarMap)
anaTermEvent t vars = do
anaTermCspCASL vars t
let alpha = [] -- XXX Need to implement term sort computation
return (S.fromList alpha, Map.empty)
anaChanSend :: CHANNEL_NAME -> (TERM ()) -> ProcVarMap ->
State CspCASLSign (CommAlpha, ProcVarMap)
anaChanSend c t vars = do
sig <- get
let ext = extendedInfo sig
case c `Map.lookup` (chans ext) of
Nothing -> do
addDiags [mkDiag Error "unknown channel" c]
return (S.empty, Map.empty)
Just _ -> do -- XXX _ is to be chanSort
anaTermCspCASL vars t
-- XXX Need to implement term casting
let alpha = []
return (S.fromList alpha, Map.empty)
anaChanBinding :: CHANNEL_NAME -> VAR -> SORT ->
State CspCASLSign (CommAlpha, ProcVarMap)
anaChanBinding c v s = do
checkSorts [s] -- check sort is known
sig <- get
let ext = extendedInfo sig
case c `Map.lookup` (chans ext) of
Nothing -> do
addDiags [mkDiag Error "unknown channel" c]
return (S.empty, Map.empty)
Just chanSort -> do
if s `S.member` (subsorts chanSort)
then do let alpha = [CommTypeSort s
,CommTypeChan (TypedChanName c s)]
let binding = [(v, s)]
return (S.fromList alpha, Map.fromList binding)
else do let err = "sort not a subsort of channel's sort"
addDiags [mkDiag Error err s]
return (S.empty, Map.empty)
where subsorts = Rel.predecessors (sortRel sig)
-- Analysis of renaming and renaming items
anaRenaming :: RENAMING -> State CspCASLSign CommAlpha
anaRenaming r = do al <- Monad.foldM anaRenamingItem S.empty r
return al
anaRenamingItem :: CommAlpha -> Id -> State CspCASLSign CommAlpha
anaRenamingItem inAl ri = do
totOps <- getBinOpsById ri Total
if (not $ S.null totOps)
then return (inAl `S.union` totOps)
else do parOps <- getBinOpsById ri Partial
if (not $ S.null parOps)
then return (inAl `S.union` parOps)
else do preds <- getBinPredsById ri
if (not $ S.null preds)
then return (inAl `S.union` preds)
else do let err = ("renaming item not a binary " ++
"operation or predicate name")
addDiags [mkDiag Error err ri]
return inAl
-- |Get sorts of binary operations of the specified id and kind
getBinOpsById :: Id -> FunKind -> State CspCASLSign (S.Set CommType)
getBinOpsById ri kind = do
sig <- get
let opsWithId = Map.findWithDefault S.empty ri (opMap sig)
binOpsKind = S.filter (isBin kind) opsWithId
cts = S.map CommTypeSort $ S.fold opSorts S.empty binOpsKind
return cts
where isBin k ot = (k == opKind ot) && (1 == (length (opArgs ot)))
opSorts o inS = inS `S.union` (S.fromList ((opArgs o) ++ [opRes o]))
-- |Get sorts of binary predicates of the specified id and kind
getBinPredsById :: Id -> State CspCASLSign (S.Set CommType)
getBinPredsById ri = do
sig <- get
let predsWithId = Map.findWithDefault S.empty ri (predMap sig)
binPreds = S.filter isBin predsWithId
cts = S.map CommTypeSort $ S.fold predSorts S.empty binPreds
return cts
where isBin ot = (2 == (length (predArgs ot)))
predSorts p inS = inS `S.union` (S.fromList (predArgs p))
-- Analysis of communication alphabet subsort-closed subset relationships.
checkCommAlphaSub :: CommAlpha -> CommAlpha -> PROCESS -> String ->
State CspCASLSign ()
checkCommAlphaSub sub super proc context = do
sig <- get
let extras = ((closeCspCommAlpha sig sub) `S.difference`
(closeCspCommAlpha sig super))
if S.null extras
then do return ()
else do let err = ("Communication alphabet subset violations (" ++
context ++ "): " ++ (show $ S.toList extras))
addDiags [mkDiag Error err proc]
return ()
-- Analysis of term appearing in CspCASL context
anaTermCspCASL :: ProcVarMap -> (TERM ()) -> State CspCASLSign (Maybe (TERM ()))
anaTermCspCASL pm t = do
sig <- get
let newVars = Map.union pm (varMap sig)
sigext = sig { varMap = newVars }
Result ds mt = anaTermCspCASL' sigext t
addDiags ds
return mt
anaTermCspCASL' :: CspCASLSign -> (TERM ()) -> Result (TERM ())
anaTermCspCASL' sig t = do
let allIds = unite [mkIdSets (allOpIds sig) $ allPredIds sig]
ga = globAnnos sig
mix = emptyMix { mixRules = makeRules ga allIds }
resT <- resolveMixfix (putParen mix) (mixResolve mix)
ga (mixRules mix) t
oneExpTerm (const return) sig resT
ccTermCast :: (TERM f) -> SORT -> State CspCASLSign ()
ccTermCast _ _ = do return ()
-- this is easy when you have the term's sort.
-- nocast is t
-- upcast is (Sorted_term t s)
-- downcast is (Cast t s)
-- error is, well, error :-)