|
definition:
|
tryVerifyProg :: TermDomain a => Options -> Int -> VerifyState a -> String
-> Map.Map QName [FuncDecl] -> [FuncDecl]
-> IO (Int,VerifyState a)
tryVerifyProg opts numits vstate mname funusage fdecls = do
st <- execStateT (mapM_ verifyFunc fdecls) vstate
-- remove NewFailed information about unchanged operations
-- (usually, these are failed operations with changed conditions)
let newfailures = filter (\(qf,ct) -> maybe True (\fct -> ct /= fct)
(Map.lookup qf (vstCallTypes st)))
(vstNewFailed st)
unless (null newfailures || optVerb opts < 2) $ printFailures st
unless (null newfailures) $ printWhenStatus opts $ unlines $
"Operations with refined call types (used in future analyses):" :
showFunResults prettyFunCallAType (reverse newfailures)
let newcts = Map.union (Map.fromList newfailures) (vstCallTypes st)
enforceNormalForm opts "NEWCALLTYPES" newcts
let (failconds,refineconds) =
partition (\(qf,_) -> qf `elem` (map fst (vstFunConds st)))
(vstNewFunConds st)
newfailconds = filter (\(qf,_) -> (qf,nfcFalse) `notElem` vstFunConds st)
failconds
-- Condition for next iteration: set already existing conditions to
-- `False` to avoid infinite refinements
nextfunconds = (unionBy (\x y -> fst x == fst y)
(map (\(qf,_) -> (qf, nfcFalse)) newfailconds)
(vstFunConds st)) ++ refineconds
newrefineconds = newfailconds ++ refineconds
--fdecls <- currentFuncDecls st
unless (null newrefineconds) $ printWhenStatus opts $
"Operations with refined call conditions (used in future analyses):\n" ++
showConditions fdecls newrefineconds
let st' = st { vstCallTypes = newcts, vstNewFailed = []
, vstFunConds = nextfunconds, vstNewFunConds = [] }
if null newfailures && null newrefineconds
then do printFailures st'
-- remove always failing conditions (since the call types are
-- always failing for such functions):
let st'' = st' { vstFunConds =
filter ((/= nfcFalse) . snd) nextfunconds }
return (numits + 1, st'')
else do
let -- functions with refined call types:
rfuns = map fst (filter (not . isFailACallType . snd) newfailures)
newfdecls =
foldr unionFDecls
(filter (\fd -> funcName fd `elem` rfuns) fdecls)
(map (\qf -> maybe [] id (Map.lookup qf funusage))
(union (map fst newfailures) (map fst newrefineconds)))
printWhenStatus opts $ "Repeat verification with new call types..." ++
"(" ++ show (length newfdecls) ++ " functions)"
--printInfoLine $ unlines $
-- showFunResults prettyFunCallAType (sortFunResults $ vstCallTypes st')
tryVerifyProg opts (numits + 1) st' mname funusage newfdecls
where
failLine = take 78 (repeat '!')
failComment = failLine ++ "\nPROGRAM CONTAINS POSSIBLY FAILING "
printFailures st = whenStatus opts $ do
unless (null (vstFailedFuncs st)) $
printInfoLine $ failComment ++ "FUNCTION CALLS:\n" ++
unlines (map (\ (qf,_,e) -> "Function '" ++ snd qf ++
"': call '" ++ showExp e ++ "'")
(reverse (vstFailedFuncs st)) ++ [failLine])
unless (null (vstPartialBranches st)) $
printInfoLine $ failComment ++ "FUNCTIONS:\n" ++
unlines
(map (\ (qf,_,e,cs) -> showIncompleteBranch qf e cs)
(reverse (vstPartialBranches st)) ++ [failLine])
|