Commit d0469315 authored by Michael Hanus 's avatar Michael Hanus
Browse files

CASS: AnalysisCollection renamed to Registry, analyses descriptions added

parent c16bbaa5
--------------------------------------------------------------------------
--- This module contains operations to deal with the documentation
--- of analyses registered in CASS.
---
--- @author Michael Hanus
--- @version July 2016
--------------------------------------------------------------------------
module AnalysisDoc(getAnalysisDoc) where
import Directory (doesFileExist)
import FilePath ((</>), (<.>))
import Configuration (docDir)
--------------------------------------------------------------------------
--- Gets the documentation of an analysis with a registered name.
--- Returns `Nothing` if no documentation exist.
getAnalysisDoc :: String -> IO (Maybe String)
getAnalysisDoc aname = do
let docfilename = docDir </> aname <.> "md"
docfileexists <- doesFileExist docfilename
if docfileexists then readFile docfilename >>= return . Just
else return Nothing
--------------------------------------------------------------------------
--------------------------------------------------------------------------
--- This is the main module of the analysis system.
--- One can either use the 'main' operation to start the system
--- in "server mode" or "batch mode" or use one of the operations below
--- to use the analysis system in another Curry program.
--- This is the main module of the analysis server.
--- It provides operations to initialize the server system,
--- start the server on a socket, or use the analysis server
--- by other Curry applications.
---
--- @author Heiko Hoffmann, Michael Hanus
--- @version June 2016
......@@ -22,12 +22,13 @@ import IO
import ReadShowTerm(readQTerm,showQTerm)
import System(system,sleep,setEnviron,getArgs)
import FileGoodies(stripSuffix,splitDirectoryBaseName)
import AnalysisCollection
import ServerFormats
import ServerFunctions(WorkerMessage(..))
import Analysis(Analysis,AOutFormat(..))
import Configuration
import GenericProgInfo
import Analysis(Analysis,AOutFormat(..))
import Registry
import ServerFormats
import ServerFunctions(WorkerMessage(..))
-- Messages to communicate with the analysis server from external programs.
data AnalysisServerMessage =
......
......@@ -12,9 +12,9 @@ import ReadShowTerm(readQTerm)
import Socket(connectToSocket)
import System(getArgs,setEnviron)
import AnalysisCollection(lookupRegAnaWorker)
import ServerFunctions(WorkerMessage(..))
import Configuration(debugMessage,waitTime,getDefaultPath)
import Registry(lookupRegAnaWorker)
import ServerFunctions(WorkerMessage(..))
main :: IO ()
main = do
......
......@@ -6,17 +6,19 @@
--- the analysis server (which is implicitly started if necessary).
---
--- @author Michael Hanus
--- @version April 2016
--- @version July 2016
--------------------------------------------------------------------------
module Configuration
(systemBanner,baseDir,getServerAddress,updateRCFile,updateCurrentProperty,
getFPMethod,getWithPrelude,
storeServerPortNumber,removeServerPortNumber,getServerPortNumber,
getDefaultPath,waitTime,numberOfWorkers,debugMessage) where
( systemBanner, baseDir, docDir
, getServerAddress, updateRCFile, updateCurrentProperty
, getFPMethod, getWithPrelude
, storeServerPortNumber, removeServerPortNumber, getServerPortNumber
, getDefaultPath, waitTime, numberOfWorkers, debugMessage
) where
import System
import Distribution(installDir,curryCompiler)
import Distribution(installDir, curryCompiler)
import PropertyFile
import ReadNumeric
import FilePath(FilePath, (</>), (<.>))
......@@ -29,16 +31,22 @@ import Char(isSpace)
systemBanner :: String
systemBanner =
let bannerText = "CASS: Curry Analysis Server System ("++
"version of 17/06/2016 for "++curryCompiler++")"
"version of 28/07/2016 for "++curryCompiler++")"
bannerLine = take (length bannerText) (repeat '=')
in bannerLine ++ "\n" ++ bannerText ++ "\n" ++ bannerLine
--- The base directory of the analysis tool containing all programs.
--- Required to copy the configuration file and to the find executables
--- of the server and the workers.
--- The base directory of the analysis tool containing all programs
--- and documentations.
--- It is used to copy the configuration file, to the find executables
--- of the server and the workers, and to find the documentation
--- of the various analyses.
baseDir :: String
baseDir = installDir ++ "/currytools/CASS"
baseDir = installDir </> "currytools" </> "CASS"
--- The directory containing the documentations of the various analyses.
docDir :: String
docDir = baseDir </> "Docs"
--- The address of the server when it is connected from the worker clients.
getServerAddress :: IO String
......
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 contain overlapping left-hand sides or free variables,
or if it depends on some non-deterministic operation.
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 property analysis
------------------------------
This analysis analyzes the higher-order status of an operation,
i.e., it shows whether an operation is first order or
it is higher-order since has functional arguments or results
or 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).
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.
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.
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.
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.
Markdown is supported
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