Commit 1a4af256 authored by Michael Hanus's avatar Michael Hanus
Browse files

New analyses for termination and productivity of operations added

parent ceee9142
......@@ -10,17 +10,18 @@
--- (instead of the data constructors).
---
--- @author Heiko Hoffmann, Michael Hanus
--- @version May 2013
--- @version January 2017
-------------------------------------------------------------------------
module Analysis(Analysis(..),
simpleFuncAnalysis,simpleTypeAnalysis,
simpleFuncAnalysis, simpleTypeAnalysis,
simpleConstructorAnalysis,
dependencyFuncAnalysis,dependencyTypeAnalysis,
combinedSimpleFuncAnalysis,combinedSimpleTypeAnalysis,
combinedDependencyFuncAnalysis,combinedDependencyTypeAnalysis,
isSimpleAnalysis,isCombinedAnalysis,isFunctionAnalysis,
analysisName,baseAnalysisName,startValue,
dependencyFuncAnalysis, dependencyTypeAnalysis,
combinedSimpleFuncAnalysis, combined2SimpleFuncAnalysis,
combinedSimpleTypeAnalysis,
combinedDependencyFuncAnalysis, combinedDependencyTypeAnalysis,
isSimpleAnalysis, isCombinedAnalysis, isFunctionAnalysis,
analysisName, baseAnalysisNames, startValue,
AOutFormat(..))
where
......@@ -40,7 +41,7 @@ data Analysis a =
| SimpleConstructorAnalysis String (ConsDecl -> TypeDecl -> a)
| DependencyFuncAnalysis String a (FuncDecl -> [(QName,a)] -> a)
| DependencyTypeAnalysis String a (TypeDecl -> [(QName,a)] -> a)
| CombinedSimpleFuncAnalysis String String Bool
| CombinedSimpleFuncAnalysis [String] String Bool
(String -> IO (FuncDecl -> a))
| CombinedSimpleTypeAnalysis String String Bool
(String -> IO (TypeDecl -> a))
......@@ -101,9 +102,22 @@ dependencyTypeAnalysis anaName startval anaType =
combinedSimpleFuncAnalysis :: String -> Analysis b
-> (ProgInfo b -> FuncDecl -> a) -> Analysis a
combinedSimpleFuncAnalysis ananame baseAnalysis anaFunc =
CombinedSimpleFuncAnalysis analysisAName ananame True
CombinedSimpleFuncAnalysis [analysisName baseAnalysis] ananame True
(runWithBaseAnalysis baseAnalysis anaFunc)
where analysisAName = analysisName baseAnalysis
--- A simple combined analysis for functions.
--- The analysis is based on an operation that computes
--- some information from a given function declaration
--- and information provided by two base analyses.
--- The base analyses are provided as the second and third argument.
combined2SimpleFuncAnalysis :: String -> Analysis b -> Analysis c
-> (ProgInfo b -> ProgInfo c -> FuncDecl -> a) -> Analysis a
combined2SimpleFuncAnalysis ananame baseAnalysisA baseAnalysisB anaFunc =
CombinedSimpleFuncAnalysis
[analysisName baseAnalysisA, analysisName baseAnalysisB]
ananame
True
(runWith2BaseAnalyses baseAnalysisA baseAnalysisB anaFunc)
--- A simple combined analysis for types.
--- The analysis is based on an operation that computes
......@@ -162,6 +176,23 @@ runWithBaseAnalysis baseAnalysis analysisFunction moduleName = do
let baseinfos = combineProgInfo impbaseinfos mainbaseinfos
return (analysisFunction baseinfos)
--- Loads the results of the base analysis and put it as the first
--- argument of the main analysis operation which is returned.
runWith2BaseAnalyses :: Analysis a -> Analysis b
-> (ProgInfo a -> ProgInfo b -> (input -> c)) -> String
-> IO (input -> c)
runWith2BaseAnalyses baseanaA baseanaB analysisFunction moduleName = do
importedModules <- getImports moduleName
let baseananameA = analysisName baseanaA
baseananameB = analysisName baseanaB
impbaseinfosA <- getInterfaceInfos baseananameA importedModules
mainbaseinfosA <- loadCompleteAnalysis baseananameA moduleName
impbaseinfosB <- getInterfaceInfos baseananameB importedModules
mainbaseinfosB <- loadCompleteAnalysis baseananameB moduleName
let baseinfosA = combineProgInfo impbaseinfosA mainbaseinfosA
baseinfosB = combineProgInfo impbaseinfosB mainbaseinfosB
return (analysisFunction baseinfosA baseinfosB)
--- Is the analysis a simple analysis?
--- Otherwise, it is a dependency analysis which requires a fixpoint
--- computation to compute the results.
......@@ -206,19 +237,23 @@ analysisName (CombinedSimpleTypeAnalysis _ nameB _ _) = nameB
analysisName (CombinedDependencyFuncAnalysis _ nameB _ _ _) = nameB
analysisName (CombinedDependencyTypeAnalysis _ nameB _ _ _) = nameB
--- Name of the base analysis of a combined analysis.
baseAnalysisName :: Analysis a -> String
baseAnalysisName (CombinedSimpleFuncAnalysis bName _ _ _) = bName
baseAnalysisName (CombinedSimpleTypeAnalysis bName _ _ _) = bName
baseAnalysisName (CombinedDependencyFuncAnalysis bName _ _ _ _) = bName
baseAnalysisName (CombinedDependencyTypeAnalysis bName _ _ _ _) = bName
--- Names of the base analyses of a combined analysis.
baseAnalysisNames :: Analysis a -> [String]
baseAnalysisNames ana = case ana of
CombinedSimpleFuncAnalysis bnames _ _ _ -> bnames
CombinedSimpleTypeAnalysis bname _ _ _ -> [bname]
CombinedDependencyFuncAnalysis bname _ _ _ _ -> [bname]
CombinedDependencyTypeAnalysis bname _ _ _ _ -> [bname]
_ -> []
--- Start value of a dependency analysis.
startValue :: Analysis a -> a
startValue (DependencyFuncAnalysis _ startval _) = startval
startValue (DependencyTypeAnalysis _ startval _) = startval
startValue (CombinedDependencyFuncAnalysis _ _ _ startval _) = startval
startValue (CombinedDependencyTypeAnalysis _ _ _ startval _) = startval
startValue ana = case ana of
DependencyFuncAnalysis _ startval _ -> startval
DependencyTypeAnalysis _ startval _ -> startval
CombinedDependencyFuncAnalysis _ _ _ startval _ -> startval
CombinedDependencyTypeAnalysis _ _ _ startval _ -> startval
_ -> error "Internal error in Analysis.startValue"
-------------------------------------------------------------------------
--- The desired kind of output of an analysis result.
......@@ -229,4 +264,4 @@ startValue (CombinedDependencyTypeAnalysis _ _ _ startval _) = startval
--- in a module.
data AOutFormat = AText | ANote
-------------------------------------------------------------------------
\ No newline at end of file
-------------------------------------------------------------------------
......@@ -2,7 +2,7 @@
--- Operations to handle dependencies of analysis files.
---
--- @author Heiko Hoffmann, Michael Hanus
--- @version January 2015
--- @version January 2017
-----------------------------------------------------------------------
module AnalysisDependencies(getModulesToAnalyze,reduceDependencies) where
......@@ -167,7 +167,8 @@ findModulesToAnalyze (m@(mod,imports):ms)
(modulesToDo,(mod:modulesUpToDate))
else findModulesToAnalyze ms anaTimeList sourceTimeList fcyTimeList
((m:modulesToDo),modulesUpToDate)
where
Nothing -> error
"Internal error in AnalysisDependencies.findModulesToAnalyz"
-- function to check if result file is up-to-date
......
......@@ -309,6 +309,7 @@ parseServerMessage message = case words message of
"GetAnalysis" -> GetAnalysis
"AnalyzeModule" -> case ws of
s1:s2:s3:[] -> checkFormat s2 $ AnalyzeModule s1 s2 s3 False
_ -> ParseError
"AnalyzeInterface" -> case ws of
s1:s2:s3:[] -> checkFormat s2 $ AnalyzeModule s1 s2 s3 True
_ -> ParseError
......
......@@ -31,7 +31,7 @@ import Char(isSpace)
systemBanner :: String
systemBanner =
let bannerText = "CASS: Curry Analysis Server System ("++
"version of 12/01/2017 for "++curryCompiler++")"
"version of 23/01/2017 for "++curryCompiler++")"
bannerLine = take (length bannerText) (repeat '=')
in bannerLine ++ "\n" ++ bannerText ++ "\n" ++ bannerLine
......
......@@ -5,7 +5,7 @@
--- registered in the top part of this module.
---
--- @author Heiko Hoffmann, Michael Hanus
--- @version July 2016
--- @version January 2017
--------------------------------------------------------------------
module Registry
......@@ -32,17 +32,18 @@ import LoadAnalysis(loadCompleteAnalysis)
-- Configurable part of this module.
--------------------------------------------------------------------
import Demandedness
import Deterministic
import Groundness
import HigherOrder
import RightLinearity
import SolutionCompleteness
import TotallyDefined
import Indeterministic
import Demandedness
import Groundness
import RequiredValue
import qualified RequiredValues as RVS
import RightLinearity
import RootReplaced
import SolutionCompleteness
import Termination
import TotallyDefined
--------------------------------------------------------------------
--- Each analysis used in our tool must be registered in this list
......@@ -67,10 +68,13 @@ registeredAnalysis =
,cassAnalysis "Higher-order datatypes" hiOrdType showOrder
,cassAnalysis "Higher-order constructors" hiOrdCons showOrder
,cassAnalysis "Higher-order functions" hiOrdFunc showOrder
,cassAnalysis "Productive operations" productivityAnalysis showProductivity
,cassAnalysis "Sibling constructors" siblingCons showSibling
,cassAnalysis "Required value" reqValueAnalysis showAFType
,cassAnalysis "Required value sets" RVS.reqValueAnalysis RVS.showAFType
,cassAnalysis "Root cyclic replacements" rootCyclicAnalysis showRootCyclic
,cassAnalysis "Root replacements" rootReplAnalysis showRootRepl
,cassAnalysis "Terminating operations" terminationAnalysis showTermination
]
......@@ -243,14 +247,18 @@ prepareCombinedAnalysis analysis moduleName depmods handles =
then do
-- the directly imported interface information might be required...
importedModules <- getImports moduleName
mapIO_ (runAnalysisWithWorkersNoLoad baseAnaName handles)
(importedModules++[moduleName])
else do
mapIO_ (\basename ->
mapIO_ (runAnalysisWithWorkersNoLoad basename handles)
(importedModules++[moduleName]))
baseAnaNames
else
-- for a dependency analysis, the information of all implicitly
-- imported modules might be required:
mapIO_ (runAnalysisWithWorkersNoLoad baseAnaName handles) depmods
mapIO_ (\baseaname ->
mapIO_ (runAnalysisWithWorkersNoLoad baseaname handles) depmods)
baseAnaNames
else done
where
baseAnaName = baseAnalysisName analysis
baseAnaNames = baseAnalysisNames analysis
--------------------------------------------------------------------
......@@ -3,13 +3,14 @@
--- anlysis server.
---
--- @author Heiko Hoffmann, Michael Hanus
--- @version May 2015
--- @version January 2017
--------------------------------------------------------------------
module ServerFormats(serverFormats,formatResult) where
import GenericProgInfo
import FlatCurry.Types(QName,showQNameInModule)
import Sort(sortBy)
import XML
--------------------------------------------------------------------
......@@ -39,6 +40,7 @@ formatResult moduleName outForm (Just name) _ (Left pinfo) =
"CurryTerm" -> value
"Text" -> value
"XML" -> showXmlDoc (xml "result" [xtxt value])
_ -> error "Internal error ServerFormats.formatResult"
-- Format a complete module:
formatResult moduleName outForm Nothing public (Left pinfo) =
case outForm of
......@@ -48,9 +50,12 @@ formatResult moduleName outForm Nothing public (Left pinfo) =
in showXmlDoc
(xml "results"
(pubxml ++ if public then [] else privxml))
_ -> error "Internal error ServerFormats.formatResult"
where
entities = let (pubents,privents) = progInfo2Lists pinfo
in if public then pubents else pubents++privents
in if public then pubents
else sortBy (\ (qf1,_) (qf2,_) -> qf1<=qf2)
(pubents++privents)
-- Format a list of analysis results as a string (lines of analysis results).
formatAsText :: String -> [(QName,String)] -> String
......
......@@ -3,7 +3,7 @@
--- In particular, it contains some simple fixpoint computations.
---
--- @author Heiko Hoffmann, Michael Hanus
--- @version August 2016
--- @version January 2017
--------------------------------------------------------------------------
module WorkerFunctions where
......@@ -109,6 +109,7 @@ getStartValues analysis prog =
CombinedDependencyTypeAnalysis _ _ _ _ _ ->
map (\typeDecl->(typeName typeDecl,startValue analysis))
(progTypes prog)
_ -> error "Internal error in WorkerFunctions.getStartValues"
return startvals
--- Compute a ProgInfo from a given list of infos for each function name w.r.t.
......@@ -164,6 +165,7 @@ execCombinedAnalysis analysis prog importInfos startvals moduleName fpmethod =
anaFunc <- runWithBaseAna moduleName
runAnalysis (DependencyTypeAnalysis ananame startval anaFunc)
prog importInfos startvals fpmethod
_ -> error "Internal error in WorkerFunctions.execCombinedAnalysis"
-----------------------------------------------------------------------
--- Run an analysis but load default values (e.g., for external operations)
......@@ -192,6 +194,7 @@ runAnalysis analysis prog importInfos startvals fpmethod = do
(definedFuncs, funcInfos2ProgInfo defaultFuncs deflts)
DependencyTypeAnalysis _ _ _ ->
(definedTypes, typeInfos2ProgInfo defaultTypes deflts)
_ -> error "Internal error in WorkerFunctions.runAnalysis"
let result = executeAnalysis analysis progWithoutDefaults
(combineProgInfo importInfos defaultproginfo)
startvals fpmethod
......@@ -266,6 +269,15 @@ executeAnalysis (DependencyTypeAnalysis _ _ anaType) prog
(listToFM (<) startvals)
(reverse sccDecls)
_ -> error unknownFixpointMessage
-- These cases are handled elsewhere:
executeAnalysis (CombinedSimpleFuncAnalysis _ _ _ _) _ _ _ _ =
error "Internal error in WorkerFunctions.executeAnalysis"
executeAnalysis (CombinedSimpleTypeAnalysis _ _ _ _) _ _ _ _ =
error "Internal error in WorkerFunctions.executeAnalysis"
executeAnalysis (CombinedDependencyFuncAnalysis _ _ _ _ _) _ _ _ _ =
error "Internal error in WorkerFunctions.executeAnalysis"
executeAnalysis (CombinedDependencyTypeAnalysis _ _ _ _ _) _ _ _ _ =
error "Internal error in WorkerFunctions.executeAnalysis"
unknownFixpointMessage :: String
unknownFixpointMessage = "Unknown value for 'fixpoint' in configuration file!"
......
This directory contains the implementation of various
program analyses which can be used with CASS
(the Curry Analysis Server System), available by the command
> curry analyze <options>
A description how to implement and integrate a new analysis is described
in the user manual (section CASS: Implementing Program Analyses).
......@@ -8,11 +8,14 @@
--- h x = k x : []
---
--- then the root replacements of f are [g,h].
---
--- This analysis could be useful to detect simple loops, e.g., if
--- a function is in its root replacement.
--- a function is in its root replacement. This is the purpose
--- of the analysis `RootCyclic` which assigns `True` to some
--- operation if this operation might cause a cyclic root replacement.
---
--- @author Michael Hanus
--- @version June 2016
--- @version January 2017
------------------------------------------------------------------------------
module RootReplaced
......@@ -20,6 +23,7 @@ module RootReplaced
import Analysis
import FlatCurry.Types
import GenericProgInfo
import List
import Sort(sort)
......@@ -29,7 +33,7 @@ import Sort(sort)
--- all function names to which a function can be root replaced.
type RootReplaced = [QName]
-- Show determinism information as a string.
-- Show root-replacement information as a string.
showRootRepl :: AOutFormat -> RootReplaced -> String
showRootRepl AText [] = "no root replacements"
showRootRepl ANote [] = ""
......@@ -66,3 +70,30 @@ rrFuncRule calledFuncs (Rule _ rhs) = rrOfExp rhs
(map (\ (Branch _ be) -> rrOfExp be) bs))
------------------------------------------------------------------------------
-- Show root-cyclic information as a string.
showRootCyclic :: AOutFormat -> Bool -> String
showRootCyclic AText False = "no cycles at the root"
showRootCyclic ANote False = ""
showRootCyclic AText True = "possible cyclic root replacement"
showRootCyclic ANote True = "root-cyclic"
--- Root cyclic analysis.
rootCyclicAnalysis :: Analysis Bool
rootCyclicAnalysis =
combinedSimpleFuncAnalysis "RootCyclic" rootReplAnalysis rcFunc
rcFunc :: ProgInfo RootReplaced -> FuncDecl -> Bool
-- we assume that external functions are not root cyclic:
rcFunc _ (Func _ _ _ _ (External _)) = False
-- otherwise we check whether the operation is in its set of root replacements:
rcFunc rrinfo (Func qf _ _ _ (Rule _ _)) =
maybe True -- no information, but this case should not occur
(\rrfuncs -> qf `elem` rrfuncs -- direct cycle
-- or cycle in some root-replacement:
|| any (\rrf -> maybe True
(rrf `elem`)
(lookupProgInfo rrf rrinfo))
rrfuncs)
(lookupProgInfo qf rrinfo)
------------------------------------------------------------------------------
------------------------------------------------------------------------------
--- 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 Januar 2017
------------------------------------------------------------------------------
module Termination
( terminationAnalysis, showTermination
, productivityAnalysis, showProductivity, Productivity(..)
) where
import Analysis
import Char(isDigit)
import FlatCurry.Types
import FlatCurry.Goodies
import GenericProgInfo
import List
import RootReplaced (rootCyclicAnalysis)
import Sort(sort)
import Unsafe
------------------------------------------------------------------------------
-- 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 -- to be improved!!!
hasTermExp args (Let bs e) =
all (hasTermExp args) (map snd bs) && hasTermExp args e -- ???
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 and root-cyclic analysis.
-- It assigns to a FlatCurry function definition a flag which is True
-- if this operation is terminating, i.e., whether all evaluations
--- Data type to represent productivity status of an operation.
data Productivity = Terminating | Productive | Looping
productivityAnalysis :: Analysis Productivity
productivityAnalysis =
combined2SimpleFuncAnalysis "Productive"
terminationAnalysis
rootCyclicAnalysis
isProductive
-- Show productivity information as a string.
showProductivity :: AOutFormat -> Productivity -> String
showProductivity _ Looping = "possibly looping"
showProductivity _ Productive = "productive"
showProductivity _ Terminating = "terminating"
lubProd :: Productivity -> Productivity -> Productivity
lubProd Looping _ = Looping
lubProd Productive Terminating = Productive
lubProd Productive Productive = Productive
lubProd Productive Looping = Looping
lubProd Terminating p = p
-- 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.
isProductive :: ProgInfo Bool -> ProgInfo Bool
-> FuncDecl -> Productivity --[(QName,Bool)] -> Bool
isProductive terminfo rcyclicinfo (Func _ _ _ _ rule) = hasProdRule rule
where
hasProdRule (Rule _ e) = hasProdExp e
-- we assume that all externally defined operations are terminating:
hasProdRule (External _) = Terminating
hasProdExp (Var _) = Terminating
hasProdExp (Lit _) = Terminating
hasProdExp (Free _ e) = lubProd Productive (hasProdExp e) -- to be improved!!!
hasProdExp (Let bs e) =
lubProd (hasProdExp e)
(foldr lubProd Terminating (map (\ (_,be) -> hasProdExp be) bs))
hasProdExp (Or e1 e2) = lubProd (hasProdExp e1) (hasProdExp e2)
hasProdExp (Case _ e bs) =
foldr lubProd (hasProdExp e) (map (\ (Branch _ be) -> hasProdExp be) bs)
hasProdExp (Typed e _) = hasProdExp e
hasProdExp (Comb ct qf es) =
case ct of
ConsCall -> foldr lubProd Terminating (map hasProdExp es)
ConsPartCall _ -> foldr lubProd Terminating (map hasProdExp es)
_ -> foldr lubProd
(if maybe False id (lookupProgInfo qf terminfo)
then Terminating
else if maybe True id (lookupProgInfo qf rcyclicinfo)
then Looping
else Productive)
(map hasProdExp es)
------------------------------------------------------------------------------
......@@ -3,7 +3,7 @@
--- programs.
---
--- @author Michael Hanus
--- @version September 2016
--- @version January 2017
---------------------------------------------------------------------
module BrowserGUI where
......@@ -49,7 +49,7 @@ title :: String
title = "CurryBrowser"
version :: String
version = "Version of 07/09/2016"
version = "Version of 22/01/2017"
patchReadmeVersion :: IO ()
patchReadmeVersion = do
......
......@@ -12,7 +12,7 @@ they have no effect.
Developed by
Michael Hanus (CAU Kiel, Germany, mh@informatik.uni-kiel.de)
Version of 07/09/2016
Version of 22/01/2017
Software requirements:
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment