{-|

Module : $Header$

Copyright : (c) Till Mossakowski, Uni Bremen 2002-2004

Licence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer : hets@tzi.de

Stability : provisional

Portability : non-portable(Logic)

Analysis of libraries

Follows the verification semantics sketched in Chap. IV:6

of the CASL Reference Manual.

-}

{-

Todo:

Generalization to heterogeneous views

check that libname coincides with filename (otherwise internal error occurs)

-}

module Static.AnalysisLibrary (anaFile, ana_LIB_DEFN, anaString) where

import Logic.Logic

import Logic.Grothendieck

import Comorphisms.LogicGraph

import Common.Lib.Graph

import Static.DevGraph

import qualified Syntax.AS_Structured

import Syntax.Parse_AS_Structured (lookupLogicName)

import Syntax.AS_Library

import Static.AnalysisStructured

import Static.AnalysisArchitecture

import Common.AS_Annotation

import Common.GlobalAnnotations

import Common.ConvertGlobalAnnos

import Common.AnalyseAnnos

import Common.Result

import Common.Id

import qualified Common.Lib.Map as Map

import Common.PrettyPrint

import Options

import System

import List

import ReadFn

import WriteFn (writeFileInfo)

import System.Posix.Files

-- | parsing and static analysis for files

-- Parameters: logic graph, default logic, file name

anaFile :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> String

-> IO (Maybe (LIB_NAME,LIB_DEFN,DGraph,LibEnv))

anaFile logicGraph defaultLogic opts libenv fname = do

putIfVerbose opts 1 ("Reading " ++ fname)

fname' <- existsAnSource fname

case fname' of

Nothing -> do

if outputToStdout opts then

putStrLn (fname++" not found.")

else return ()

return Nothing

Just fname'' -> do

input <- readFile fname''

anaString logicGraph defaultLogic opts libenv input (Just fname'')

-- | parsing and static analysis for string (=contents of file)

-- Parameters: logic graph, default logic, contents of file, filename (if any)

anaString :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> String

-> Maybe String -> IO (Maybe (LIB_NAME,LIB_DEFN,DGraph,LibEnv))

anaString logicGraph defaultLogic opts libenv input fname = do

let fname' = case fname of

Nothing -> "<stdin>"

Just n -> n

ast <- read_LIB_DEFN_M defaultLogic fname' input

Result diags res <-

ioresToIO (ana_LIB_DEFN logicGraph defaultLogic opts

libenv ast)

-- no diags expected here, since these are handled in ana_LIB_DEFN

-- sequence (map (putStrLn . show) diags)

case (res,fname) of

(Just (ln,_,_,lenv), Just n) ->

writeFileInfo opts diags n ln lenv

_ -> return ()

return res

-- lookup/read a library

anaLibFile :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> LIB_NAME

-> IO ([Diagnosis], LibEnv)

anaLibFile logicGraph defaultLogic opts libenv libname = do

-- is the library already in memory?

case Map.lookup libname libenv of

Just _ -> return ([],libenv)

Nothing -> do

-- if not compute the filename,

fname <- case getLIB_ID libname of

Indirect_link file _ -> do

path <- case libdir opts of

"" -> catch (getEnv "HETS_LIB")

(\ _ -> return "")

p -> return p

-- add trailing "/" if necessary

let path1 = case path of

"" -> ""

p -> case last p of

'/' -> p

_ -> p++"/"

return (path1++file)

Direct_link _ _ ->

if outputToStdout opts then

error "No direct links implemented yet"

else return (error "No direct links implemented yet")

-- check if and env file is there and read it if it is recent

let env_fname = fname++".env"

-- fname is sufficient here, because anaFile

-- trys all possible suffices with this basename

recent_env_file <- checkRecentEnv env_fname fname

if recent_env_file

then do

putIfVerbose opts 1 ("Reading "++env_fname)

(Result dias mgc) <- globalContextfromShATerm env_fname

-- the conversion/reading might yield an error that

-- should be caught here

(dias2, mLibEnv) <-

maybe (do ioresToIO $ showDiags1 opts (resToIORes (Result dias mgc))

anaLibFile' fname dias)

(\ gc@(_,_,dgraph) -> do

if outputToStdout opts then

putStrLn ""

else return()

-- get all DGRefs from DGraph

let libEnv' = (Map.insert libname gc libenv)

nodesDGRef =

filter (\ labDG -> case labDG of

DGRef _ _ _ -> True

_ -> False)

(map snd (labNodes dgraph))

-- and call anaLibFile with each of the dgn_libname

-- of the DGRefs

refLibs = nub $ map dgn_libname nodesDGRef

newRefLibs =

filter (\ ln ->

not (ln `elem` Map.keys libEnv'))

refLibs

foldl (\ioLibEnv tlibname ->

do (dias3 ,p_libEnv) <- ioLibEnv

putIfVerbose opts 1

("Analyzing from " ++

showPretty tlibname "\n")

(dias4, libEnvF) <- anaLibFile logicGraph defaultLogic opts p_libEnv tlibname

return ((dias3 ++ dias4),libEnvF)

) (return ([], libEnv')) newRefLibs

)

mgc

if outputToStdout opts then

return ([], mLibEnv)

else return( dias ++ dias2 , mLibEnv)

else anaLibFile' fname []

where anaLibFile' :: FilePath -> [Diagnosis] -> IO ([Diagnosis], LibEnv)

anaLibFile' fname diags'=

do

-- read and analyze the library,

if outputToStdout opts then

do

res <- anaFile logicGraph defaultLogic opts libenv fname

putStrLn ""

-- and just return the libenv

return (case res of

Just (_,_,_,libenv') -> (diags', libenv')

Nothing -> (diags', libenv)

)

else do

(dias, res) <- anaFileW logicGraph defaultLogic opts libenv fname

return (case res of

Just (_,_,_,libenv') -> (diags'++dias, libenv')

Nothing -> ((diags $ message () (fname ++" not found.")) ++ diags',libenv))

anaFileW :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> String

-> IO ([Diagnosis], Maybe (LIB_NAME,LIB_DEFN,DGraph,LibEnv))

anaFileW logicGraph defaultLogic opts libenv fname = do

fname' <- existsAnSource fname

case fname' of

Nothing -> return ([], Nothing)

Just fname'' -> do

input <- readFile fname''

anaStringW logicGraph defaultLogic opts libenv input (Just fname'')

anaStringW :: LogicGraph -> AnyLogic -> HetcatsOpts -> LibEnv -> String

-> Maybe String

-> IO ([Diagnosis], Maybe (LIB_NAME,LIB_DEFN,DGraph,LibEnv))

anaStringW logicGraph defaultLogic opts libenv input fname = do

let fname' = case fname of

Nothing -> "<stdin>"

Just n -> n

(_, ast) <- read_LIB_DEFN_M_WI defaultLogic fname' input

Result diags res <-

ioresToIO (ana_LIB_DEFN logicGraph defaultLogic opts

libenv ast)

case (res,fname) of

(Just (ln,_,_,lenv), Just n) ->

writeFileInfo opts diags n ln lenv

_ -> return ()

return (diags, res)

-- | analyze a LIB_DEFN

-- Parameters: logic graph, default logic, opts, library env, LIB_DEFN

-- call this function as follows:

-- do Result diags res <- ioresToIO (ana_LIB_DEFN ...)

-- sequence (map (putStrLn . show) diags)

ana_LIB_DEFN :: LogicGraph -> AnyLogic -> HetcatsOpts

-> LibEnv -> LIB_DEFN

-> IOResult (LIB_NAME,LIB_DEFN,DGraph,LibEnv)

ana_LIB_DEFN lgraph defl opts libenv (Lib_defn ln alibItems pos ans) = do

gannos <- resToIORes $ addGlobalAnnos emptyGlobalAnnos ans

(libItems',gctx@(_,_,dg),_,libenv') <-

foldl ana (return ([],(gannos,Map.empty,empty),defl,libenv))

(map item alibItems)

return (ln,

Lib_defn ln

(map (uncurry replaceAnnoted)

(zip (reverse libItems') alibItems))

pos

ans,

dg,

Map.insert ln gctx libenv')

where

ana res1 libItem = do

(libItems',gctx1,l1,libenv1) <- res1

IOResult (do

Result diags2 res <-

ioresToIO $ ana_LIB_ITEM lgraph defl opts libenv1 gctx1 l1 libItem

ioresToIO $ showDiags1 opts (resToIORes (Result diags2 res))

if outputToStdout opts then

if hasErrors diags2 then

fail "Stopped due to errors"

else case res of

Just (libItem',gctx1',l1',libenv1') ->

return (return (libItem':libItems',gctx1',l1',libenv1'))

Nothing -> fail "Stopped. No result available"

else do

--result1 <- ioresToIO res1

--let diags1 = diags result1

if hasErrors diags2 then

ioresToIO $ resToIORes (Result (diags2) Nothing)

else case res of

Just (libItem',gctx1',l1',libenv1') ->

return ((return (libItem':libItems',gctx1',l1',libenv1')){diags = diags2})

Nothing -> return $ fail "Stopped. No result available"

)

-- analyse a LIB_ITEM

-- Parameters: logic graph, default logic, opts, library env

-- global context, current logic, LIB_ITEM

ana_LIB_ITEM :: LogicGraph -> AnyLogic -> HetcatsOpts

-> LibEnv -> GlobalContext -> AnyLogic

-> LIB_ITEM

-> IOResult (LIB_ITEM,GlobalContext,AnyLogic,LibEnv)

ana_LIB_ITEM lgraph defl opts libenv gctx@(gannos,genv,dg) l

(Spec_defn spn gen asp pos) = do

let analyseMessage = "Analyzing spec " ++ showPretty spn ""

ioToIORes (putIfVerbose opts 1 analyseMessage)

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

(gen',(imp,params,parsig,allparams),dg') <-

resToIORes (ana_GENERICITY lgraph gctx l opts gen)

(sp',body,dg'') <-

resToIORes (ana_SPEC lgraph (gannos,genv,dg')

allparams (Just spn) opts (item asp))

let libItem' = Spec_defn spn gen' (replaceAnnoted sp' asp) pos

if Map.member spn genv

then resToIORes (plain_error (libItem',gctx,l,libenv)

("Name "++ showPretty spn " already defined")

(headPos pos))

else return (libItem',

(gannos,

Map.insert spn (SpecEntry (imp,params,parsig,body)) genv,

dg''),

l,

libenv)

ana_LIB_ITEM lgraph defl opts libenv gctx l

(View_defn vn gen vt gsis pos) = do

let analyseMessage = "Analyzing view " ++ showPretty vn ""

ioToIORes (putIfVerbose opts 1 analyseMessage)

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

resToIORes (ana_VIEW_DEFN lgraph defl libenv gctx l opts

vn gen vt gsis pos)

-- architectural specification

ana_LIB_ITEM lgraph defl opts libenv gctx@(gannos, genv, dg) l

asd@(Arch_spec_defn asn asp pos) = do

let analyseMessage = "Analyzing arch spec " ++ showPretty asn ""

ioToIORes (putIfVerbose opts 1 analyseMessage )

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

(archSig, dg', asp') <- resToIORes (ana_ARCH_SPEC lgraph defl gctx l opts (item asp))

let asd' = Arch_spec_defn asn (replaceAnnoted asp' asp) pos

gctx' = (gannos, genv, dg')

if Map.member asn genv

then

resToIORes (plain_error (asd', gctx', l, libenv)

("Name " ++ showPretty asn " already defined")

(headPos pos))

else

return (asd',

(gannos,

Map.insert asn (ArchEntry archSig) genv,

dg'),

l,

libenv)

-- unit specification

ana_LIB_ITEM lgraph defl opts libenv gctx@(gannos, genv, _) l

usd@(Unit_spec_defn usn usp pos) = do

let analyseMessage = "Analyzing unit spec " ++ showPretty usn ""

ioToIORes (putIfVerbose opts 1 analyseMessage)

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

(unitSig, dg', usp') <- resToIORes (ana_UNIT_SPEC lgraph defl gctx l opts (EmptyNode defl) usp)

let usd' = Unit_spec_defn usn usp' pos

if Map.member usn genv

then

resToIORes (plain_error (usd, (gannos, genv, dg'), l, libenv)

("Name " ++ showPretty usn " already defined")

(headPos pos))

else

return (usd',

(gannos,

Map.insert usn (UnitEntry unitSig) genv,

dg'),

l,

libenv)

ana_LIB_ITEM lgraph defl opts libenv gctx l

(Logic_decl ln pos) = do

log <- lookupLogicName ln lgraph

let analyseMessage = "logic "++show log

ioToIORes (putIfVerbose opts 1 analyseMessage)

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

return (Logic_decl ln pos,gctx,log,libenv)

ana_LIB_ITEM lgraph defl opts libenv gctx@(gannos,genv,dg) l

libItem@(Download_items ln items pos) = do

-- we take as the default logic for imported libs

-- the global default logic

let items' = zip items (drop 2 (pos ++ repeat nullPos))

analyseMessage = "Analyzing from " ++ showPretty ln "\n"

ioToIORes (putIfVerbose opts 1 analyseMessage)

if outputToStdout opts then

return()

else

resToIORes $ message () analyseMessage

(diags', libenv') <- ioToIORes (anaLibFile lgraph defl opts libenv ln)

resToIORes $ Result diags' $ Just ()

-- let libMsg = unlines $ map show diags'

-- resToIORes $ message () libMsg

case Map.lookup ln libenv' of

Nothing -> do

if outputToStdout opts then

do

ioToIORes (putStrLn ("Internal error: did not find library "++show ln++" available: "++show (Map.keys libenv')))

return (libItem,gctx,l,libenv')

else

resToIORes $ (fatal_error ("Internal error: did not find library "++show ln++" available: "++show (Map.keys libenv')) nullPos)

Just (gannos',genv',dg') -> do

(genv1,dg1) <- resToIORes (foldl (ana_ITEM_NAME_OR_MAP ln genv')

(return (genv,dg)) items'

)

gannos'' <- resToIORes $ gannos `mergeGlobalAnnos` gannos'

return (libItem,(gannos'',genv1,dg1),l,libenv')

-- ??? Needs to be generalized to views between different logics

ana_VIEW_DEFN lgraph defl libenv gctx@(gannos,genv,dg) l opts

vn gen vt gsis pos = do

let adj = adjustPos (headPos pos)

(gen',(imp,params,parsig,allparams),dg') <-

ana_GENERICITY lgraph gctx l opts gen

(vt',(src,tar),dg'') <-

ana_VIEW_TYPE lgraph (gannos,genv,dg') l allparams opts vt

let gsigmaS = getSig src

gsigmaT = getSig tar

G_sign lidS sigmaS <- return gsigmaS

G_sign lidT sigmaT <- return gsigmaT

gsis1 <- adj $ Syntax.AS_Structured.homogenizeGM (Logic lidS) gsis

G_symb_map_items_list lid sis <- return gsis1

sigmaS' <- rcoerce lid lidS (headPos pos) sigmaS

sigmaT' <- rcoerce lid lidT (headPos pos) sigmaT

mor <- if analysis opts == Structured then return (ide lid sigmaS')

else do

rmap <- adj $ stat_symb_map_items lid sis

adj $ induced_from_to_morphism lid rmap sigmaS' sigmaT'

nodeS <- maybeToResult (headPos pos)

"Internal error: empty source spec of view" (getNode src)

nodeT <- maybeToResult (headPos pos)

"Internal error: empty source spec of view" (getNode tar)

let gmor = gEmbed (G_morphism lid mor)

link = (nodeS,nodeT,DGLink {

dgl_morphism = gmor,

dgl_type = GlobalThm Open None Open,

-- 'Open' for conserv correct?

dgl_origin = DGView vn})

vsig = (src,gmor,(imp,params,parsig,tar))

if Map.member vn genv

then plain_error (View_defn vn gen' vt' gsis pos,gctx,l,libenv)

("Name "++showPretty vn " already defined")

(headPos pos)

else return (View_defn vn gen' vt' gsis pos,

(gannos,

Map.insert vn (ViewEntry vsig) genv,

insEdge link dg''),

l,

libenv)

ana_ITEM_NAME_OR_MAP ln genv' res (Item_name name,pos) =

ana_ITEM_NAME_OR_MAP1 ln genv' res name name pos

ana_ITEM_NAME_OR_MAP ln genv' res (Item_name_map old new _, pos) =

ana_ITEM_NAME_OR_MAP1 ln genv' res old new pos

ana_ITEM_NAME_OR_MAP1 ln genv' res old new pos = do

(genv,dg) <- res

entry <- maybeToResult pos

(showPretty old " not found") (Map.lookup old genv')

case Map.lookup new genv of

Nothing -> return ()

Just _ -> fatal_error (showPretty new " already used") pos

case entry of

SpecEntry extsig ->

let (dg1,extsig1) = refExtsig ln dg (Just new) extsig

genv1 = Map.insert new (SpecEntry extsig1) genv

in return (genv1,dg1)

ViewEntry vsig ->

let (dg1,vsig1) = refViewsig ln dg vsig

genv1 = Map.insert new (ViewEntry vsig1) genv

in return (genv1,dg1)

ArchEntry asig -> ana_err "arch spec download"

UnitEntry usig -> ana_err "unit spec download"

refNodesig ln (dg,refdNodes) (name,NodeSig(n,sigma)) =

let node_contents = DGRef {

dgn_renamed = name,

dgn_libname = ln,

dgn_node = n }

[node] = newNodes 0 dg

in (insNode (node,node_contents) dg, NodeSig(node,sigma) : refdNodes)

refNodesig ln (dg,refdNodes) (_,EmptyNode l) =

(dg,EmptyNode l : refdNodes)

refNodesigs ln dg nodes =

(dg',reverse nodes')

where (dg', nodes') = foldl (refNodesig ln) (dg,[]) nodes

refExtsig ln dg name (imps,params,gsigmaP,body) =

(dg1,(imps1,params1,gsigmaP,body1))

where

params' = map (\x -> (Nothing,x)) params

(dg1,imps1:body1:params1) =

refNodesigs ln dg

((Nothing,imps):(name,body):params')

refViewsig ln dg (src,mor,extsig) =

(dg2,(src1,mor,extsig1))

where

(_,[src1]) = refNodesigs ln dg [(Nothing,src)]

(dg2,extsig1) = refExtsig ln dg Nothing extsig