Commit a04fe0e5 authored by Michael Hanus 's avatar Michael Hanus

The Curry Analysis Server System (previously distributed with PAKCS or KiCS2)

parents
*~
.curry
.cpm
Demand analysis
---------------
This analysis assigns to each operation a list of argument positions
(e.g., [1] for the first argument) which are demanded in order
to reduce this operation to some constructor-rooted value.
Analysis of deterministic operations
------------------------------------
This analysis checks whether an operation is deterministically defined.
Intuitively, an operation is deterministic if the evaluation of
this operation applied to ground terms does not cause any non-determinism.
The determinism analysis returns `nondeterministic` for a given operation
if its definition contains overlapping left-hand sides or free variables,
or if it depends on some non-deterministic operation.
If calls to non-deterministic operations are encapsulated (by the
use of set functions or operations from module `AllSolutions`),
then it is classified as deterministic since the non-determinism
does not occur at the top-level.
Analysis of functionally defined operations
-------------------------------------------
This analysis checks whether an operation is defined in a pure functional
manner.
An operation is functionally defined if its definition does not contain
overlapping left-hand sides or free variables, and it depends only
on functionally defined operations.
This analysis is stronger than the `Deterministic` analysis,
since the latter classifies an operation as deterministic
if calls to possibly non-deterministic operations are wrapped
with encapsulated search operators, whereas this analysis
does not allow the use of any logic features.
Groundness analysis
-------------------
This analysis assigns to each operation the conditions under which
a ground (non-free) result is computed. The analysis results can be
"always ground result", "possibly non-ground result",
or "ground if arguments x1,..,xn are ground".
The idea and details of this analysis can be found in the
[ICLP'05 paper](http://www.informatik.uni-kiel.de/~mh/papers/ICLP05.html).
Higher-order constructor analysis
---------------------------------
This analysis is a simple analysis for data constructors.
It associates to each data constructor a flag indicating
whether some argument contains functions.
Higher-order property analysis
------------------------------
This analysis analyzes the higher-order status of an operation.
It classifies an operations as higher-order since if it
has functional arguments or results, or or it processes
data structures with functional components.
Higher-order type analysis
--------------------------
This analysis analyzes the higher-order status of type constructors,
i.e., it shows whether some constructor of a type constructor
has functional arguments.
Indeterminism analysis
----------------------
This analysis assigns to each operation a flag which is `True`
if this operation might be indeterministic, i.e., calls directly or indirectly
a select or committed choice operation.
Thus, an indeterministic is not referentially transparent
since it might deliver different results on different program runs.
Groundness/non-determinism effect analysis
------------------------------------------
This analysis assigns to each operation the conditions under which
the evaluation of this operation might perform non-deterministic steps.
The non-deterministic steps might be due to a `choice` (overlapping rules)
or narrowing steps, where the latter might depend on the non-groundness
of particular arguments.
For instance, the operation
not True = False
not False = True
is performs non-deterministic steps if the first argument is non-ground.
The idea and details of this analysis can be found in the
[ICLP'05 paper](http://www.informatik.uni-kiel.de/~mh/papers/ICLP05.html).
Analysis of dependencies on all non-deterministic operations
------------------------------------------------------------
This analysis is useful if some operation has a non-deterministic
behavior and one wants to find the reason for this behavior.
For this purpose, the analysis computes for each operation the set of
operations with a non-deterministic definition that might be called
by this operation. An operation has a non-deterministic definition
if its definition contains overlapping left-hand sides or free variables.
If the non-determinism of an operation is encapsulated
by a set function or an encapsulated search operation of the module
`AllSolutions`, it is considered as deterministic.
For instance, consider the operations
last xs | _ ++ [x] == xs = x where x free
coin = 0 ? 1
lastCoin = id (last [coin])
Then the operation `lastCoin` depends on the non-deterministic
operations `last` and `coin`. Now consider the operations
f x = x ? lastCoin
g x = f x
Then the operation `g` depends on the non-deterministic operation `f`,
and also on the non-deterministic operations `last` and `coin`.
In the long analysis output (produced by CASS in batch mode),
the non-deterministic operations are shown together with
the sequence of operations (limited to a length of 10)
which calls the non-deterministic operation.
Analysis of dependencies on non-deterministic operations
--------------------------------------------------------
This analysis is useful if some operation has a non-deterministic
behavior and one wants to find the reason for this behavior.
For this purpose, the analysis computes for each operation the set of
operations with a non-deterministic definition that might be called
by this operation. An operation has a non-deterministic definition
if its definition contains overlapping left-hand sides or free variables.
Non-deterministic operations that are called by other
non-deterministic operations are ignored so that only the first
(w.r.t. the call sequence) non-deterministic operations are returned.
Moreover, if the non-determinism of an operation is encapsulated by a
set function or an encapsulated search operation of the module
`AllSolutions`, it is considered as deterministic.
For instance, consider the operations
last xs | _ ++ [x] == xs = x where x free
coin = 0 ? 1
lastCoin = id (last [coin])
Then the operation `lastCoin` depends on the non-deterministic
operations `last` and `coin`. Now consider the operations
f x = x ? lastCoin
g x = f x
Then the operation `g` depends on the non-deterministic operation `f`,
but the dependency on the non-deterministic
operations `last` and `coin` is not reported.
In the long analysis output (produced by CASS in batch mode),
the non-deterministic operations are shown together with
the operation which directly calls the non-deterministic operation.
Overlapping rule analysis
-------------------------
The overlapping rule analysis checks whether an individual operation
is defined by overlapping left-hand sides.
For instance, the operation
not True = False
not False = True
is not overlapping, whereas
coin = 0
coin = 1
is overlapping. Note that
f = coin
is not overlapping, although it calls an operation defined by
overlapping rules.
Pattern completeness analysis
-----------------------------
This analysis analyzes an operation for a pattern-complete definition.
An operation is pattern complete if each pattern match is
defined for all constructors.
For instance, the operation
not True = False
not False = True
is pattern complete, whereas the operation
head (x:_) = x
is incomplete. If an operation is defined by overlapping rules,
it is complete if there is one alternative with complete pattern matching.
For instance, the operation
por True x = True
por x True = True
por False False = False
is not complete, since it corresponds to the following definition:
por x y = por1 x y ? por2 x y
por1 True _ = True
por1 False False = True
por2 _ True = True
Hence, each alternative is incomplete.
Productivity analysis
---------------------
This analysis computes some information about the termination
or productivity of an operation.
An operation is considered as being productive if it cannot
perform an infinite number of steps without producing
outermost constructors.
This analysis assigns to an operation an abstract value
indicating whether the function is terminating, looping, or productive.
In the latter case, the abstract value contains the top-level calls,
i.e., operations that are called at the top-level without an outermost
constructor.
For instance, consider the operations
loop = id loop
ones = 1 : ones
`loop` is classified as looping whereas `ones` is productive.
This directory contains some documention for the Curry Analysis Server System:
manual.tex:
A short description to be included in the main manual of the Curry system.
<ana>.md:
The documentation of the analysis registered with name <ana> in
markdown syntax.
Required value analysis
-----------------------
This analysis checks for each operation in a Curry program whether
the arguments must have a particular shape in order to
compute some value.
For instance, the negation operation `not` defined by
not True = False
not False = True
requires the argument value `False` in order to compute the result
`True` and it requires the argument `True` to compute the result
`False`. This property is expressed by the following abstract type:
not : (True -> False) | (False -> True)
Hence, each abstract type is a constructor which represents
all expressions rooted by this constructor.
Moreover, the abstract type `cons` denotes any constructor-rooted
expression and the abstract type `any` denotes any expression.
The abstract type `_|_` denotes an impossible required type, i.e.,
an argument which is required but for which no applicable value exists.
For instance, the operation
f x = solve (x && not x)
has the required value typing
f: (_|_ -> {True})
A detailed description of this analysis and its application can be found in the
[LOPSTR'15 paper](http://www.informatik.uni-kiel.de/~mh/papers/LOPSTR15.html).
Required values analysis
------------------------
This analysis checks for each operation in a Curry program whether
the arguments must have a particular shape in order to
compute some value.
For instance, the negation operation `not` defined by
not True = False
not False = True
requires the argument value `False` in order to compute the result
`True` and it requires the argument `True` to compute the result
`False`. This property is expressed by the following abstract type:
not : ({True} -> {False}) | ({False} -> {True})
Hence, each abstract type is a set of constructors which represents
all expressions rooted by one of the constructors in this set.
Moreover, the abstract type `any` denotes any expression.
The empty list denotes an impossible required type, i.e.,
an argument which is required but for which no applicable value exists.
For instance, the operation
f x = solve (x && not x)
has the required value typing
f: ({} -> True)
A detailed description of this analysis and its application can be found in the
[LOPSTR'15 paper](http://www.informatik.uni-kiel.de/~mh/papers/LOPSTR15.html).
Right-linearity analysis
------------------------
This analysis checks whether an operation is right-linear, i.e.,
whether its evaluation does not duplicate any argument.
Hence, this analysis returns `right-linear` for a given operation
if it is defined by right-linear rules (i.e., rules that does not
contain multiple occurrences of argument variables in its right-hand sides)
and depends only on right-linear operations.
Root cyclic analysis
--------------------
This analysis assigns `True` to an operation `f` if its evaluation
might result in an expression rooted by `f`.
Hence, this analysis is useful to detect simple loops.
f x = g x
g x = h x
h x = id (f x)
id x = x
Then `f`, `g`, and `h` are root-cyclic whereas `id` is not root-cyclic.
Root replacement analysis
-------------------------
This analysis returns for each function `f` all functions into which `f` can
be replaced at the root. For instance, if there are the definitions:
f x = g x
g x = h x
h x = k x : []
k x = x
then the root replacements of `f` are `[g,h]` and the
root replacements of `g` are `[h]`.
This analysis could be useful to detect simple loops, e.g., if
a function is in its own root replacement.
Sibling constructor analysis
----------------------------
This analysis associates to each data constructor the list of
sibling constructors, i.e., all constructors of the same type
without this data constructor.
For instance, the sibling constructors of `Prelude.True` are
`[Prelude.False]`.
Solution completeness analysis
------------------------------
This analysis assigns to a function a flag which is `True` if this function
is operationally complete, i.e., does not call (explicitly or implicitly)
a rigid function.
For instance, the operation
not True = False
not False = True
is `solution complete`, whereas the prelude operation `putChar`
is not solution complete but may suspend if it is called with
a free variable as argument.
Termination analysis
--------------------
This analysis assigns `True` to an operation `f` if all its evaluations
on ground argument terms are finite.
The current method used in this analysis is quite simple.
It checks whether the arguments in all recursive
calls of an operation are smaller than the arguments passed to
the operation. Indirect calls are not considered.
Therefore, the operation
length [] = 0
length (x:xs) = 1 + length xs
is classified as terminating, whereas the semantically equivalent operation
length [] = 0
length (x:xs) = incLength xs
incLength xs = 1 + length xs
is classified as possibly non-terminating.
Operations containing free variables in their definitions are
also classified as possibly non-terminating since a free variable
might reduce to arbitrarily large constructor terms (in case of
recursive data types).
Totally definedness analysis
----------------------------
This analysis assigns to each operation a flag which is `True`
if this operation is completely defined on its input types,
i.e., reducible for all ground data terms.
Thus, an operation is totally defined if it is pattern complete
and depends only on totally defined functions.
Analyzing types occurring in values
-----------------------------------
The `TypesInValues` analysis is a type analysis which assigns
to each data type defined in a program the list of data types
(type constructors) which might occur in value arguments of this type.
For instance, no type constructors are associated to `Bool`
since Boolean values have no arguments.
The type constructor `[]` is associated to the `[]` since a list
occurs in the second argument of a non-empty list.
Thus, this analysis can be used to check for recursive types:
if a type constructor is associated to itself, the type is recursive,
i.e., can have values of arbitrary size.
For instance, consider the following type declarations:
data List a = Empty | Cons a (List a)
data Tree a = Leaf | Node (List (Tree a))
Then this analysis computes the following information:
List : List
Tree : List, Tree
Hence, both types are recursive.
This diff is collapsed.
-- Tests for the RootReplaced analysis
--
-- Runt test with:
-- > cass NonDetDeps NonDetTest.curry
import SetFunctions
last xs | _ ++ [x] == xs = x where x free
lastfp (_ ++ [x]) = x
printLast = do
print $ last [1..7]
print $ lastfp [1..42]
coin = 0 ? 1
lastCoin = id (last [coin])
--> last, coin
f x = x ? lastCoin
g x = f x
-- For this operation, the NonDetDeps analysis reports that the
-- non-determinism depends on `f`.
-- However, the analysis NonDetAllDeps reports also the dependency
-- on the non-deterministic operations coin, last,...
main0 = set0 lastCoin
main1 = set1 last [1,2,3]
main2 = set1 last [1,2,coin]
append :: [a] -> [a] -> [a]
append [] ys = ys
append (x:xs) ys = x : append xs ys
rev :: [a] -> [a]
rev [] = []
rev (x:xs) = append (rev xs) [x]
main :: Int -> Int -> [Int]
main x y = rev [x .. y]
-- Tests for the RootReplaced analysis
--
-- Runt test with:
-- > cass RootReplaced RootReplacedTest.curry
loop = loop
--> root replacements: [loop] --> indicates infinite loop
f x = g x
--> root replacements: [g,h]
g x = h x
--> root replacements: [h]
h x = k x : []
--> root replacements: []
k x = x
--> root replacements: []
--- A simple program to show the usage of the API mode of CASS
--- to access the demanded values of the operation Rev.main:
import AnalysisServer (analyzeGeneric)
import GenericProgInfo (lookupProgInfo)
import Demandedness (demandAnalysis)
demandedArgumentsOf :: String -> String -> IO [Int]
demandedArgumentsOf modname fname = do
deminfo <- analyzeGeneric demandAnalysis modname >>= return . either id error
return $ maybe [] id (lookupProgInfo (modname,fname) deminfo)
main = demandedArgumentsOf "Rev" "main"
Protocol to communicate with the analysis server
================================================
Server commands:
----------------
GetAnalysis
SetCurryPath <dir1>:<dir2>:...
StopServer
AnalyzeModule <kind of analysis> <output type> <module name>
AnalyzeInterface <kind of analysis> <output type> <module name>
AnalyzeFunction <kind of analysis> <output type> <module name> <function name>
AnalyzeDataConstructor <kind of analysis> <output type> <module name> <constructor name>
AnalyzeTypeConstructor <kind of analysis> <output type> <module name> <type name>
Server answers:
---------------
error ...
ok <n>\n<result text>
(here <n> denotes the number of lines in <result text>)
The answer to the command `GetAnalysis` is a list of all available
analyses. The list has the form "<kind of analysis> <output type>".
For instance, a communication could be:
> GetAnalysis
< ok 5
< Deterministic CurryTerm
< Deterministic Text
< Deterministic XML
< HigherOrder CurryTerm
< DependsOn CurryTerm
Further examples for server requests:
> AnalyzeModule Deterministic CurryTerm SolverServer
> AnalyzeModule Deterministic Text SolverServer
> AnalyzeModule Deterministic XML SolverServer
> AnalyzeFunction Deterministic XML SolverServer main
> AnalyzeDataConstructor HigherOrder CurryTerm Prelude Just
> AnalyzeFunction DependsOn CurryTerm SolverServer main
CASS: The Curry Analysis Server System
======================================
This directory contains the implementation of CASS,
a generic and distributed analysis system for Curry programs.
The analysis system is structured as a worker/server application
where the workers are triggered by the main server to analyse
individual modules.
The analysis system can also be used as a client from other
application programs by a socket interface.
The protocol of this interface is described in `Protocol.txt`.
The server is explicitly started by the program `cass`
(generated via `make`) or implicitly by application programs
that use of the operation `Configuration.getServerPortNumber`
to find out the port number to connect to the analysis server.
The port number can either be explicitly specified the starting
the main server program via
cass -p <port>
or a free port number is chosen when the analysis server is started.
The current port and process numbers of a running analysis server
are temporarily stored in the file `$HOME/.curryanalysis.port`
(in the tuple format `(port,pid)`).
The program `cass` can also be started on a console with arguments:
cass <analysis> <module>
In this case, the analysis with the specified name is applied
to the specified module without the use of the server protocol
and the output is shown on stdout. Run the command
cass --help
to get a description of the arguments and a list of registered analysis
names.
The analysis system can be configured in the file `$HOME/.curryanalysisrc`
which is installed after the first run of the system.
The implementations of the individual analysis are
usually defined in the package `cass-analysis`).
Description of some Curry modules:
----------------------------------
* `CASS.Registry`: All available analyses must be registered here.
* `CASS.Server`: The main module implementing the use of the server.