|
definition:
|
verifyModule :: TermDomain a => Analysis a -> IORef ProgInfo
-> IORef (AnalysisStore a) -> Options -> String -> Prog -> IO ()
verifyModule valueanalysis pistore astore opts mname flatprog = do
let orgfdecls = progFuncs flatprog
numfdecls = length orgfdecls
visfuncs = map funcName (filter ((== Public) . funcVisibility)
orgfdecls)
visfuncset = Set.fromList visfuncs
isVisible qf = Set.member qf visfuncset
showfuncset = Set.fromList
(filter (\fn -> optGenerated opts || isCurryID fn)
visfuncs)
isShowable qf = Set.member qf showfuncset
imps@(impconsinfos,impacalltypes,impnftypes,impiotypes) <-
if optImports opts
then do
let imports = progImports flatprog
whenStatus opts $ printInfoString $
"Reading abstract types of imports: " ++ unwords imports
-- if only verification results should be shown, use quiet mode and
-- do not show in/out types for imports:
let impopts = if optVerb opts <= 1
then opts { optVerb = 0, optIOTypes = False }
else opts
readTypesOfModules impopts
(verifyModuleIfNew valueanalysis pistore astore)
imports
else return ([],[],[],[])
if optTime opts then do whenStatus opts $ printInfoString "..."
(id $## imps) `seq` printWhenStatus opts "done"
else printWhenStatus opts ""
let modconsinfos = consInfoOfTypeDecls (progTypes flatprog)
consinfos = modconsinfos ++ impconsinfos
-- verify function declarations with completed branches:
fdecls = map (completeBranchesInFunc consinfos False) orgfdecls
funusage = funcDecls2Usage mname fdecls
mtime <- getModuleModTime mname
-- infer initial abstract call types:
mboldacalltypes <- readCallTypeFile opts mtime mname
(acalltypes, numntacalltypes, numpubacalltypes) <- id $!!
inferCallTypes opts consinfos isVisible mname mtime flatprog mboldacalltypes
-- infer in/out types:
iotypes <- id $!! inferIOTypes opts valueanalysis astore flatprog
printIOTypesIfDemanded opts isShowable iotypes
-- read previously inferred non-fail conditions:
mbnfconds <- readNonFailCondFile opts mtime mname
vstate <- initVerifyState pistore flatprog consinfos
(Map.fromList impacalltypes)
(Map.fromList impnftypes)
(Map.fromList acalltypes)
(Map.fromList (iotypes ++ impiotypes))
(maybe [] id mbnfconds) opts
enforceNormalForm opts "VERIFYSTATE" vstate
printWhenAll opts $ unlines $
("Function usage in module '" ++ mname ++ "':") :
map (\ (qf, qfs) -> snd qf ++ ": used in " ++
unwords (map (snd . funcName) qfs))
(Map.toList funusage)
let withverify = optVerify opts &&
(null (optFunction opts) ||
isNothing mbnfconds || isNothing mboldacalltypes)
(vnumits, vtime, vst) <-
if withverify
then do
printWhenStatus opts $ "Start verification of '" ++ mname ++ "' (" ++
show numfdecls ++ " functions):"
pi1 <- getProcessInfos
(numits,st) <- tryVerifyProg opts 0 vstate mname funusage fdecls
pi2 <- getProcessInfos
printVerifyResult opts st mname isShowable
let tdiff = maybe 0 id (lookup ElapsedTime pi2) -
maybe 0 id (lookup ElapsedTime pi1)
when (optTime opts && optVerb opts > 0) $ printInfoLine $
"TOTAL VERIFICATION TIME: " ++ show tdiff ++ " msec"
return (numits, tdiff, st)
else return (0, 0, vstate)
-- print statistics:
let finalacalltypes = Map.toList (vstCallTypes vst)
finalntacalltypes = filter (not . isTotalACallType . snd) finalacalltypes
ntiotypes = filter (not . isAnyIOType . snd) iotypes
numpubntiotypes = length (filter (isShowable . fst) ntiotypes)
numvisfuncs = length visfuncs
(stattxt,statcsv) = showStatistics opts vtime vnumits isShowable
numvisfuncs numfdecls
(numpubntiotypes, length ntiotypes)
(numpubacalltypes, numntacalltypes)
finalntacalltypes
(map fst (vstFunConds vst)) (vstStats vst)
when (optStats opts) $ printInfoString stattxt
when withverify $ do
storeTypes opts mname fdecls modconsinfos finalacalltypes
(filter (isVisible .fst) finalntacalltypes) (vstFunConds vst)
(filter (isVisible . fst) iotypes)
storeStatistics opts mname stattxt statcsv
when (optStoreFuncs opts) $ do
let nfname = mname ++ ".NONFAIL"
flname = mname ++ ".FAIL"
totalfuncs = filter (isTotalACallType . snd) finalacalltypes
writeFile nfname
(unlines (map (\((mn,fn),_) -> mn ++ " " ++ fn) totalfuncs))
printWhenStatus opts $
"Non-failing functions stored in '" ++ nfname ++ "'."
writeFile flname
(unlines (map (\((mn,fn),_) -> mn ++ " " ++ fn) finalntacalltypes))
printWhenStatus opts $
"Possibly failing functions stored in '" ++ flname ++ "'."
unless (null (optFunction opts)) $ showFunctionInfo opts mname vst
when (vstError vst) $ exitWith 1
|