|
definition:
|
proveNonFailingRule :: Options -> ProgInfo [(QName,Int)] -> IORef VState
-> QName -> TypeExpr -> TARule -> IO ()
proveNonFailingRule _ _ vstref qn ftype (AExternal _ _) = do
ti <- readVerifyInfoRef vstref
let atypes = argTypes ftype
args = zip [1 .. length atypes] atypes
nfcond <- evalStateT (nonfailPreCondExpOf ti qn ftype args) emptyTransState
unless (nfcond == tTrue) $ modifyIORef vstref incNumNFCInStats
proveNonFailingRule opts siblingconsinfo vstref qn@(_,fn) ftype
(ARule _ rargs rhs) = do
ti <- readVerifyInfoRef vstref
let st = makeTransState (maximum (0 : map fst rargs ++ allVars rhs) + 1) rargs
(flip evalStateT) st $ do
-- compute non-fail precondition of operation:
precondformula <- nonfailPreCondExpOf ti qn ftype rargs
setAssertion precondformula
unless (precondformula == tTrue) $ lift $
modifyIORef vstref incNumNFCInStats
-- verify only if the precondition is different from always failing:
unless (precondformula == tFalse) $ proveNonFailExp ti rhs
where
proveNonFailExp ti exp = case simpExpr exp of
AComb _ ct (qf,qfty) args -> do
mapM_ (proveNonFailExp ti) args
when (isCombTypeFuncPartCall ct) $
let qnnonfail = toNonFailQName qf
in maybe
(return ()) -- h.o. call nonfailing if op. has no non-fail cond.
(\_ -> lift $ do
let reason = "due to call '" ++ ppTAExpr exp ++ "'"
modifyIORef vstref (addFailedFuncToStats fn reason)
printWhenIntermediate opts $
fn ++ ": POSSIBLY FAILING CALL OF '" ++ snd qf ++ "'")
(find (\fd -> funcName fd == qnnonfail) (nfConds ti))
when (ct==FuncCall) $ do
lift $ printWhenIntermediate opts $ "Analyzing call to " ++ snd qf
precond <- getAssertion
(bs,_) <- normalizeArgs args
bindexps <- mapM (binding2SMT True ti) bs
let callargs = zip (map fst bs) (map annExpr args)
nfcondcall <- nonfailPreCondExpOf ti qf qfty callargs
-- TODO: select from 'bindexps' only demanded argument positions
vartypes <- getVarTypes
valid <- if nfcondcall == tTrue
then return (Just True) -- true non-fail cond. is valid
else lift $ do
modifyIORef vstref incFailTestInStats
let title = "SMT script to verify non-failing call of '" ++
snd qf ++ "' in function '" ++ fn ++ "'"
checkImplicationWithSMT opts vstref title vartypes
precond (tConj bindexps) nfcondcall
if valid == Just True
then lift $ printWhenIntermediate opts $
fn ++ ": NON-FAILING CALL OF '" ++ snd qf ++ "'"
else lift $ do
let reason = if valid == Nothing
then "due to SMT error"
else "due to call '" ++ ppTAExpr exp ++ "'"
modifyIORef vstref (addFailedFuncToStats fn reason)
printWhenIntermediate opts $
fn ++ ": POSSIBLY FAILING CALL OF '" ++ snd qf ++ "'"
ACase _ _ e brs -> do
proveNonFailExp ti e
maybe
(do -- check a case expression for missing constructors:
freshvar <- getFreshVar
let freshtypedvar = (freshvar, annExpr e)
be <- binding2SMT True ti (freshvar,e)
addToAssertion be
addVarTypes [freshtypedvar]
let misscons = missingConsInBranch siblingconsinfo brs
st <- get -- use same state to prove missing and non-fail branches
mapM_ (verifyMissingCons freshtypedvar exp) misscons
put st
mapM_ (proveNonFailBranch ti freshtypedvar) brs
)
(\ (fe,te) -> do
-- check a Boolean case with True/False branch:
be <- pred2SMT e
st <- get
addToAssertion (tNot be)
proveNonFailExp ti fe
put st
addToAssertion be
proveNonFailExp ti te
)
(testBoolCase brs)
AOr _ e1 e2 -> do st <- get -- use same state for both branches
proveNonFailExp ti e1
put st
proveNonFailExp ti e2
ALet _ bs e -> do (rbs,re) <- renameLetVars bs e
mapM_ (proveNonFailExp ti) (map snd rbs)
proveNonFailExp ti re
AFree _ fvs e -> do (_,re) <- renameFreeVars fvs e
proveNonFailExp ti re
ATyped _ e _ -> proveNonFailExp ti e
AVar _ _ -> return ()
ALit _ _ -> return ()
-- verify whether a variable (2. argument) can have the constructor (3. arg.)
-- as a value w.r.t. the collected assertions
verifyMissingCons (var,vartype) exp (cons,_) = do
let title = "check missing constructor case '" ++ snd cons ++
"' in function '" ++ fn ++ "'"
lift $ printWhenIntermediate opts $
title ++ "\nVAR: " ++ show (var,vartype) ++ "\nCASE:: " ++
show (unAnnExpr (simpExpr exp))
lift $ modifyIORef vstref incPatTestInStats
vartypes <- getVarTypes
precond <- getAssertion
valid <- lift $ checkImplicationWithSMT opts vstref
("SMT script to " ++ title) vartypes precond tTrue
(tNot (constructorTest False cons (TSVar var) vartype))
unless (valid == Just True) $ lift $ do
let reason = if valid == Nothing
then "due to SMT error"
else "maybe not defined on constructor '" ++
showQName cons ++ "'"
modifyIORef vstref (addFailedFuncToStats fn reason)
printWhenIntermediate opts $
"POSSIBLY FAILING BRANCH in function '" ++ fn ++
"' with constructor " ++ snd cons
proveNonFailBranch ti (var,vartype) branch = do
ABranch p e <- renamePatternVars branch
-- set pattern type correctly (important for [] pattern)
let bpat = pat2SMT (setAnnPattern vartype p)
addToAssertion (tEquVar var bpat)
proveNonFailExp ti e
|
|
signature:
|
ToolOptions.Options
-> Analysis.ProgInfo.ProgInfo [((String, String), Prelude.Int)]
-> Data.IORef.IORef VerifierState.VState -> (String, String)
-> FlatCurry.Types.TypeExpr
-> FlatCurry.Annotated.Types.ARule FlatCurry.Types.TypeExpr -> Prelude.IO ()
|