StatAnaCSP.hs revision d326dac41dadbe2b84bb7021cbfd91f4dd4a19bc
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till MossakowskiDescription : static analysis for CspCASL
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederCopyright : (c) Markus Roggenbach, Till Mossakowski, Uni Bremen 2004-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiMaintainer : M.Roggenbach@swansea.ac.uk
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettStatic analysis for CSP-CASL
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Most of the process and channel analysis missing.
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Sentences are completely missing.
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblettimport qualified Control.Monad as Monad
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport qualified Data.Map as Map
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport qualified Data.Maybe as Maybe
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport qualified Data.Set as Set
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport qualified Common.Lib.Rel as Rel
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettimport CspCASL.AS_CspCASL_Process (CHANNEL_NAME, PROCESS_NAME)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblettimport CspCASL.LocalTop (Obligation(..), unmetObs)
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettbasicAnalysisCspCASL :: (CspBasicSpec, CspSign, GlobalAnnos)
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett -> Result (CspBasicSpec, ExtSign CspSign (), [Named ()])
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettbasicAnalysisCspCASL (cc, sigma, _ga) = do
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett let (_, accSig) = runState (ana_BASIC_CSP cc) sigma
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett let ds = reverse $ envDiags accSig
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett Result ds (Just ()) -- insert diags
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett return (cc, mkExtSign accSig, [])
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettana_BASIC_CSP :: CspBasicSpec -> State CspSign CspBasicSpec
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettana_BASIC_CSP cc = do
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett checkLocalTops
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett chs <- anaChannels (channels cc)
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett peqs <- anaProcesses (proc_items cc)
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett return (CspBasicSpec chs peqs)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett-- | Check CspCASL signature for local top elements in subsorts.
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettcheckLocalTops :: State CspSign ()
e771539425f4a0abef9f94cf4b63690f3603f682Andy GimblettcheckLocalTops = do
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett let obs = unmetObs $ Rel.toList $ Rel.transClosure $ sortRel sig
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett addDiags (map lteError obs)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett-- | Add diagnostic error for every unmet local top element obligation.
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettlteError :: Obligation SORT -> Diagnosis
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy GimblettlteError (Obligation x y z) = mkDiag Error msg ()
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett where msg = ("local top element obligation ("
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett ++ (show x) ++ "<" ++ (show y) ++ "," ++ (show z)
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett ++ ") unfulfilled.")
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettanaChannels :: [CHANNEL_DECL] -> State CspSign [CHANNEL_DECL]
61051521e4d82769a47f23aecb5fb477de47d534Andy GimblettanaChannels cs = mapM (anaChannel) cs
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettanaChannel :: CHANNEL_DECL -> State CspSign CHANNEL_DECL
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaChannel cd = do
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett checkSorts [(channelSort cd)]
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett let ext = extendedInfo sig
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett oldChanMap = chans ext
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett s = channelSort cd
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett cns = channelNames cd
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett newChanMap <- Monad.foldM (checkChannelName s) oldChanMap cns
820947bd01ca952c3909eaa0366c6914c87cc1cbTill Mossakowski vds <- gets envDiags
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett put sig { extendedInfo = ext { chans = newChanMap }
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , envDiags = vds
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettcheckChannelName :: SORT -> ChanNameMap -> CHANNEL_NAME ->
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett State CspSign ChanNameMap
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimblettcheckChannelName s m c = do
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett Nothing -> return (Map.insert c s m) -- new channel name; insert.
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett Just e -> if e == s
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett then do return m -- already declared with this sort.
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett else do let err = "channel declared with multiple sorts:"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett addDiags [mkDiag Error err c]
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy GimblettanaProcesses :: [PROC_ITEM] -> State CspSign [PROC_ITEM]
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaProcesses ps = mapM (anaProcess) ps
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaProcess :: PROC_ITEM -> State CspSign PROC_ITEM
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaProcess (ProcDecl n args alpha) = do
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett let ext = extendedInfo sig
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett oldProcDecls = procs ext
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett newProcDecls <- if n `Map.member` oldProcDecls
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett then do let err = "process name declared more than once:"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett addDiags [mkDiag Error err n]
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett return oldProcDecls
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett else anaNewProc n args alpha oldProcDecls -- new declation
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett vds <- gets envDiags
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett put sig { extendedInfo = ext {procs = newProcDecls }
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , envDiags = vds
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett return (ProcDecl n args alpha)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaProcess (ProcEq ppn proc) = return (ProcEq ppn proc)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- Analyse a process declaration for a new process name.
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaNewProc :: PROCESS_NAME -> PROC_ARGS -> PROC_ALPHABET ->
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett ProcNameMap -> State CspSign ProcNameMap
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettanaNewProc n args alpha oldMap = do
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett checkSorts args
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett checkSorts (commSorts alpha)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett let ext = extendedInfo sig
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett chanMap = chans ext
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -- check channel names are known
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett addDiags $ concatMap (knownChan chanMap) (commChans alpha)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett -- Build process profile to return
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett let chan_sorts = Maybe.catMaybes (map (flip Map.lookup chanMap)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett (commChans alpha))
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett alpha_sorts = Set.fromList ((commSorts alpha) ++ chan_sorts)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett alpha_chans = Set.fromList (commChans alpha)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett prof = (ProcProfile args (ProcAlpha alpha_sorts alpha_chans))
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett return (Map.insert n prof oldMap)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettknownChan :: ChanNameMap -> CHANNEL_NAME -> [Diagnosis]
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettknownChan cm c =
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett if c `Map.member` cm then [] else [mkDiag Error "unknown channel" c]