------------------------------------------------------------------------------ --- Termination analysis: --- checks whether an operation is terminating, i.e., --- whether all evaluations on ground argument terms are finite. --- The method used here checks whether the arguments in all recursive --- calls of an operation are smaller than the arguments passed to --- the operation. --- --- @author Michael Hanus --- @version February 2017 ------------------------------------------------------------------------------ module Analysis.Termination ( terminationAnalysis, showTermination , productivityAnalysis, showProductivity, Productivity(..) ) where import Analysis.Types import Analysis.ProgInfo import Analysis.RootReplaced (rootCyclicAnalysis) import Data.Char (isDigit) import Data.List import FlatCurry.Types import FlatCurry.Goodies import Data.SCC (scc) ------------------------------------------------------------------------------ -- The termination analysis is a global function dependency analysis. -- It assigns to a FlatCurry function definition a flag which is True -- if this operation is terminating, i.e., whether all evaluations terminationAnalysis :: Analysis Bool terminationAnalysis = dependencyFuncAnalysis "Terminating" False isTerminating -- Show termination information as a string. showTermination :: AOutFormat -> Bool -> String showTermination AText True = "terminating" showTermination ANote True = "" showTermination AText False = "possibly non-terminating" showTermination ANote False = "maybe not term." -- An operation is functionally defined if its definition is not -- non-deterministic (no overlapping rules, no extra variables) and -- it depends only on functionally defined operations. isTerminating :: FuncDecl -> [(QName,Bool)] -> Bool isTerminating (Func qfunc _ _ _ rule) calledFuncs = hasTermRule rule where hasTermRule (Rule args e) = hasTermExp (map (\a -> (a,[])) args) e -- we assume that all externally defined operations are terminating: hasTermRule (External _) = True hasTermExp _ (Var _) = True hasTermExp _ (Lit _) = True hasTermExp _ (Free _ _) = False -- could be improved if the domain is finite hasTermExp args (Let bs e) = -- compute strongly connected components of local let declarationss -- in order to check for recursive lets let sccs = scc ((:[]) . fst) (allVars . snd) bs in if any (\scc -> any (`elem` concatMap allVars (map snd scc)) (map fst scc)) sccs then False -- non-terminating due to recursive let else all (hasTermExp args) (e : map snd bs) hasTermExp args (Or e1 e2) = hasTermExp args e1 && hasTermExp args e2 hasTermExp args (Case _ e bs) = hasTermExp args e && all (\ (Branch pt be) -> hasTermExp (addSmallerArgs args e pt) be) bs hasTermExp args (Typed e _) = hasTermExp args e hasTermExp args (Comb ct qf es) = case ct of ConsCall -> all (hasTermExp args) es ConsPartCall _ -> all (hasTermExp args) es _ -> (if qf == qfunc -- is this a recursive call? then any isSmallerArg (zip args es) else maybe False id (lookup qf calledFuncs)) && all (hasTermExp args) es isSmallerArg ((_,sargs),exp) = case exp of Var v -> v `elem` sargs _ -> False -- compute smaller args w.r.t. a given discriminating expression and -- branch pattern addSmallerArgs :: [(Int, [Int])] -> Expr -> Pattern -> [(Int, [Int])] addSmallerArgs args de pat = case de of Var v -> maybe args (\argpos -> let (av,vs) = args!!argpos in replace (av, varsOf pat ++ vs) argpos args) (findIndex (isInArg v) args) _ -> args -- other expression, no definite smaller expressions where varsOf (LPattern _) = [] varsOf (Pattern _ pargs) = pargs isInArg v (argv,svs) = v==argv || v `elem` svs ------------------------------------------------------------------------------ -- The productivity analysis is a global function dependency analysis -- which depends on the termination analysis. -- An operation is considered as being productive if it cannot -- perform an infinite number of steps without producing -- outermost constructors. -- It assigns to a FlatCurry function definition an abstract value -- indicating whether the function is looping or productive. --- Data type to represent productivity status of an operation. data Productivity = NoInfo | Terminating -- definitely terminating operation | DCalls [QName] -- possible direct (top-level) calls to operations that may -- not terminate, which corresponds to being productive | Looping -- possibly looping deriving (Eq, Ord, Show, Read) productivityAnalysis :: Analysis Productivity productivityAnalysis = combinedDependencyFuncAnalysis "Productive" terminationAnalysis NoInfo isProductive -- Show productivity information as a string. showProductivity :: AOutFormat -> Productivity -> String showProductivity _ NoInfo = "no info" showProductivity _ Terminating = "terminating" showProductivity _ (DCalls qfs) = "productive / calls: " ++ "[" ++ intercalate ", " (map snd qfs) ++ "]" showProductivity _ Looping = "possibly looping" lubProd :: Productivity -> Productivity -> Productivity lubProd Looping _ = Looping lubProd (DCalls _ ) Looping = Looping lubProd (DCalls xs) (DCalls ys) = DCalls (sort (union xs ys)) lubProd (DCalls xs) Terminating = DCalls xs lubProd (DCalls xs) NoInfo = DCalls xs lubProd Terminating p = if p==NoInfo then Terminating else p lubProd NoInfo p = p -- An operation is productive if its recursive calls are below -- a constructor (except for calls to terminating operations so that -- this property is also checked). isProductive :: ProgInfo Bool -> FuncDecl -> [(QName,Productivity)] -> Productivity isProductive terminfo (Func qf _ _ _ rule) calledFuncs = hasProdRule rule where -- we assume that all externally defined operations are terminating: hasProdRule (External _) = Terminating hasProdRule (Rule _ e) = case hasProdExp False e of DCalls fs -> if qf `elem` fs then Looping else DCalls fs prodinfo -> prodinfo -- first argument: True if we are below a constructor hasProdExp _ (Var _) = Terminating hasProdExp _ (Lit _) = Terminating hasProdExp bc (Free _ e) = -- could be improved for finite domains: lubProd (DCalls []) (hasProdExp bc e) hasProdExp bc (Let bs e) = -- compute strongly connected components of local let declarationss -- in order to check for recursive lets let sccs = scc ((:[]) . fst) (allVars . snd) bs in if any (\scc -> any (`elem` concatMap allVars (map snd scc)) (map fst scc)) sccs then Looping -- improve: check for variable occs under constructors else foldr lubProd (hasProdExp bc e) (map (\ (_,be) -> hasProdExp bc be) bs) hasProdExp bc (Or e1 e2) = lubProd (hasProdExp bc e1) (hasProdExp bc e2) hasProdExp bc (Case _ e bs) = foldr lubProd (hasProdExp bc e) (map (\ (Branch _ be) -> hasProdExp bc be) bs) hasProdExp bc (Typed e _) = hasProdExp bc e hasProdExp bc (Comb ct qg es) = case ct of ConsCall -> cprodargs ConsPartCall _ -> cprodargs FuncCall -> if qg == ("Prelude","?") then fprodargs -- equivalent to Or else funCallInfo FuncPartCall _ -> funCallInfo where cprodargs = foldr lubProd NoInfo (map (hasProdExp True) es) fprodargs = foldr lubProd NoInfo (map (hasProdExp bc ) es) funCallInfo = let prodinfo = if fprodargs <= Terminating then if maybe False id (lookupProgInfo qg terminfo) then Terminating else lubProd (DCalls [qg]) (maybe Looping id (lookup qg calledFuncs)) else Looping -- worst case assumption, could be improved... in if not bc then prodinfo else case prodinfo of DCalls _ -> DCalls [] _ -> prodinfo ------------------------------------------------------------------------------