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

CASS: analysis Functional added, Deterministic modified; currypp improved for...

CASS: analysis Functional added, Deterministic modified; currypp improved for reading non-local modules
parent f18d26b0
...@@ -13,15 +13,15 @@ module AnalysisServer(mainServer, initializeAnalysisSystem, analyzeModuleAsText, ...@@ -13,15 +13,15 @@ module AnalysisServer(mainServer, initializeAnalysisSystem, analyzeModuleAsText,
analyzeGeneric, analyzePublic, analyzeInterface) analyzeGeneric, analyzePublic, analyzeInterface)
where where
import ReadNumeric(readNat) import ReadNumeric (readNat)
import Char(isSpace) import Char (isSpace)
import Directory import Directory
import FileGoodies (splitDirectoryBaseName)
import FlatCurry.Types(QName) import FlatCurry.Types(QName)
import Socket(Socket(..),listenOn,listenOnFresh,sClose,waitForSocketAccept)
import IO import IO
import ReadShowTerm(readQTerm,showQTerm) import ReadShowTerm (readQTerm, showQTerm)
import System(system,sleep,setEnviron,getArgs) import Socket (Socket(..),listenOn,listenOnFresh,sClose,waitForSocketAccept)
import FileGoodies(stripSuffix,splitDirectoryBaseName) import System (system, sleep, setEnviron, getArgs)
import Analysis(Analysis,AOutFormat(..)) import Analysis(Analysis,AOutFormat(..))
import Configuration import Configuration
...@@ -76,7 +76,7 @@ mainServer mbport = do ...@@ -76,7 +76,7 @@ mainServer mbport = do
--- by 'initializeAnalysisSystem'. --- by 'initializeAnalysisSystem'.
analyzeModuleAsText :: String -> String -> Bool -> Bool -> IO String analyzeModuleAsText :: String -> String -> Bool -> Bool -> IO String
analyzeModuleAsText ananame mname optall enforce = analyzeModuleAsText ananame mname optall enforce =
analyzeModule ananame (stripSuffix mname) enforce AText >>= analyzeModule ananame mname enforce AText >>=
return . formatResult mname "Text" Nothing (not optall) return . formatResult mname "Text" Nothing (not optall)
--- Run the analysis system to show the analysis results in the BrowserGUI. --- Run the analysis system to show the analysis results in the BrowserGUI.
......
...@@ -7,3 +7,8 @@ this operation applied to ground terms does not cause any non-determinism. ...@@ -7,3 +7,8 @@ this operation applied to ground terms does not cause any non-determinism.
The determinism analysis returns `nondeterministic` for a given operation The determinism analysis returns `nondeterministic` for a given operation
if its definition contains overlapping left-hand sides or free variables, if its definition contains overlapping left-hand sides or free variables,
or if it depends on some non-deterministic operation. 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.
...@@ -49,7 +49,8 @@ import RootReplaced ...@@ -49,7 +49,8 @@ import RootReplaced
--- together with an operation to show the analysis result as a string. --- together with an operation to show the analysis result as a string.
registeredAnalysis :: [RegisteredAnalysis] registeredAnalysis :: [RegisteredAnalysis]
registeredAnalysis = registeredAnalysis =
[cassAnalysis "Overlapping rules" overlapAnalysis showOverlap [cassAnalysis "Functionally defined" functionalAnalysis showFunctional
,cassAnalysis "Overlapping rules" overlapAnalysis showOverlap
,cassAnalysis "Deterministic operations" nondetAnalysis showDet ,cassAnalysis "Deterministic operations" nondetAnalysis showDet
,cassAnalysis "Depends on non-deterministic operations" ,cassAnalysis "Depends on non-deterministic operations"
nondetDepAnalysis showNonDetDeps nondetDepAnalysis showNonDetDeps
......
...@@ -10,6 +10,7 @@ ...@@ -10,6 +10,7 @@
module Deterministic module Deterministic
( overlapAnalysis, showOverlap, showDet ( overlapAnalysis, showOverlap, showDet
, functionalAnalysis, showFunctional
, Deterministic(..),nondetAnalysis , Deterministic(..),nondetAnalysis
, showNonDetDeps, nondetDepAnalysis, nondetDepAllAnalysis , showNonDetDeps, nondetDepAnalysis, nondetDepAllAnalysis
) where ) where
...@@ -52,30 +53,26 @@ showOverlap AText False = "non-overlapping" ...@@ -52,30 +53,26 @@ showOverlap AText False = "non-overlapping"
showOverlap ANote False = "" showOverlap ANote False = ""
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
-- The determinism analysis is a global function dependency analysis. -- The functional analysis is a global function dependency analysis.
-- It assigns to a function a flag which indicates whether is function -- It assigns to a FlatCurry function definition a flag which is True
-- might be non-deterministic, i.e., might reduce in different ways -- if this function is purely functional defined, i.e., its definition
-- for given ground arguments. -- does not depend on operation containing overlapping rules or free variables.
--- Data type to represent determinism information. functionalAnalysis :: Analysis Bool
data Deterministic = NDet | Det functionalAnalysis = dependencyFuncAnalysis "Functional" True isFuncDefined
-- Show determinism information as a string. -- Show functionally defined information as a string.
showDet :: AOutFormat -> Deterministic -> String showFunctional :: AOutFormat -> Bool -> String
showDet _ NDet = "nondeterministic" showFunctional _ True = "functional"
showDet AText Det = "deterministic" showFunctional AText False = "defined with logic features"
showDet ANote Det = "" showFunctional ANote False = ""
nondetAnalysis :: Analysis Deterministic -- An operation is functionally defined if its definition is not
nondetAnalysis = dependencyFuncAnalysis "Deterministic" Det nondetFunc -- non-deterministic (no overlapping rules, no extra variables) and
-- it depends only on functionally defined operations.
-- An operation is non-deterministic if its definition is potentially isFuncDefined :: FuncDecl -> [(QName,Bool)] -> Bool
-- non-deterministic or it depends on a non-deterministic function. isFuncDefined func calledFuncs =
nondetFunc :: FuncDecl -> [(QName,Deterministic)] -> Deterministic not (isNondetDefined func) && and (map snd calledFuncs)
nondetFunc func calledFuncs =
if isNondetDefined func || any (==NDet) (map snd calledFuncs)
then NDet
else Det
-- Is a function f defined to be potentially non-deterministic, i.e., -- Is a function f defined to be potentially non-deterministic, i.e.,
-- is the rule non-deterministic or does it contain extra variables? -- is the rule non-deterministic or does it contain extra variables?
...@@ -101,8 +98,58 @@ extraVarInExpr (Case _ e bs) = extraVarInExpr e || any extraVarInBranch bs ...@@ -101,8 +98,58 @@ extraVarInExpr (Case _ e bs) = extraVarInExpr e || any extraVarInBranch bs
where extraVarInBranch (Branch _ be) = extraVarInExpr be where extraVarInBranch (Branch _ be) = extraVarInExpr be
extraVarInExpr (Typed e _) = extraVarInExpr e extraVarInExpr (Typed e _) = extraVarInExpr e
pre :: String -> QName ------------------------------------------------------------------------------
pre n = ("Prelude",n) -- The determinism analysis is a global function dependency analysis.
-- It assigns to a function a flag which indicates whether is function
-- might be non-deterministic, i.e., might reduce in different ways
-- for given ground arguments.
-- If the non-determinism is encapsulated (set functions, AllSolutions),
-- it is classified as deterministic.
--- Data type to represent determinism information.
data Deterministic = NDet | Det
-- Show determinism information as a string.
showDet :: AOutFormat -> Deterministic -> String
showDet _ NDet = "non-deterministic"
showDet AText Det = "deterministic"
showDet ANote Det = ""
nondetAnalysis :: Analysis Deterministic
nondetAnalysis = dependencyFuncAnalysis "Deterministic" Det nondetFunc
-- An operation is non-deterministic if its definition is potentially
-- non-deterministic or it calls a non-deterministic operation
-- where the non-deterministic call is not encapsulated.
nondetFunc :: FuncDecl -> [(QName,Deterministic)] -> Deterministic
nondetFunc func@(Func _ _ _ _ rule) calledFuncs =
if isNondetDefined func || callsNDOpInRule rule
then NDet
else Det
where
callsNDOpInRule (Rule _ e) = callsNDOp e
callsNDOpInRule (External _) = False
callsNDOp (Var _) = False
callsNDOp (Lit _) = False
callsNDOp (Free _ e) = callsNDOp e
callsNDOp (Let bs e) = any callsNDOp (map snd bs) || callsNDOp e
callsNDOp (Or _ _) = True
callsNDOp (Case _ e bs) =
callsNDOp e || any (\ (Branch _ be) -> callsNDOp be) bs
callsNDOp (Typed e _) = callsNDOp e
callsNDOp (Comb _ qf@(mn,fn) es)
| mn == "SetFunctions" && take 3 fn == "set" && all isDigit (drop 3 fn)
= -- non-determinism of function (first argument) is encapsulated so that
-- its called ND functions are not relevant:
if null es then False -- this case should not occur
else any callsNDOp (tail es)
| mn == "AllSolutions" -- && fn `elem`== "getAllValues"
= -- non-determinism of argument is encapsulated so that
-- its called ND functions are not relevant:
False
| otherwise
= maybe False (==NDet) (lookup qf calledFuncs) || any callsNDOp es
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
--- Data type to represent information about non-deterministic dependencies. --- Data type to represent information about non-deterministic dependencies.
...@@ -194,6 +241,11 @@ nondetDeps alldeps func@(Func f _ _ _ rule) calledFuncs = ...@@ -194,6 +241,11 @@ nondetDeps alldeps func@(Func f _ _ _ rule) calledFuncs =
-- its called ND functions are not relevant: -- its called ND functions are not relevant:
[] []
| otherwise | otherwise
= maybe [] id (lookup qf calledFuncs) ++ (concatMap calledNDFuncs es) = maybe [] id (lookup qf calledFuncs) ++ concatMap calledNDFuncs es
------------------------------------------------------------------------------ ------------------------------------------------------------------------------
pre :: String -> QName
pre n = ("Prelude",n)
------------------------------------------------------------------------------
\ No newline at end of file
...@@ -29,7 +29,7 @@ import TransContracts(transContracts) ...@@ -29,7 +29,7 @@ import TransContracts(transContracts)
cppBanner :: String cppBanner :: String
cppBanner = unlines [bannerLine,bannerText,bannerLine] cppBanner = unlines [bannerLine,bannerText,bannerLine]
where where
bannerText = "Curry Preprocessor (version of 07/06/2016)" bannerText = "Curry Preprocessor (version of 12/01/2017)"
bannerLine = take (length bannerText) (repeat '=') bannerLine = take (length bannerText) (repeat '=')
--- Preprocessor targets, i.e., kind of entities to be preprocessed: --- Preprocessor targets, i.e., kind of entities to be preprocessed:
...@@ -74,10 +74,12 @@ main = do ...@@ -74,10 +74,12 @@ main = do
if optHelp opts if optHelp opts
then putStrLn (cppBanner ++ usageText) >> exitWith 1 then putStrLn (cppBanner ++ usageText) >> exitWith 1
else do else do
let modname = pathToModName orgSourceFile cpath <- getEnviron "CURRYPATH"
let modname = pathToModName cpath orgSourceFile
when (optVerb opts > 1) $ putStr cppBanner when (optVerb opts > 1) $ putStr cppBanner
when (optVerb opts > 2) $ putStr $ unlines when (optVerb opts > 2) $ putStr $ unlines
["Module name : " ++ modname ["CURRYPATH : " ++ cpath
,"Module name : " ++ modname
,"Original file name : " ++ orgSourceFile ,"Original file name : " ++ orgSourceFile
,"Input file name : " ++ inFile ,"Input file name : " ++ inFile
,"Output file name : " ++ outFile ] ,"Output file name : " ++ outFile ]
...@@ -251,16 +253,21 @@ callPreprocessors opts optlines modname srcprog orgfile ...@@ -251,16 +253,21 @@ callPreprocessors opts optlines modname srcprog orgfile
--- Transforms a file path name for a module back into a hierarchical module --- Transforms a file path name for a module back into a hierarchical module
--- since only the file path of a module is passed to the preprocessor. --- since only the file path of a module is passed to the preprocessor.
--- This is done if if it is a local file path name, --- This is done only if it is a local file path name,
--- otherwise only theit is difficult to reconstruct the original module name --- otherwise it is difficult to reconstruct the original module name
--- from the file path. --- from the file path.
pathToModName :: String -> String pathToModName :: String -> String -> String
pathToModName psf = pathToModName currypath psf =
if isRelative p if isRelative p
then intercalate "." (splitDirectories p) then intercalate "." (splitDirectories p)
else takeBaseName p else takeBaseName p
where where
p = stripCurrySuffix psf p = tryRemovePathPrefix (splitSearchPath currypath) (stripCurrySuffix psf)
tryRemovePathPrefix [] pp = pp
tryRemovePathPrefix (dir:dirs) pp
| dir `isPrefixOf` pp = drop (length dir + 1) pp
| otherwise = tryRemovePathPrefix dirs pp
-- Replace OPTIONS_CYMAKE line containing currypp call -- Replace OPTIONS_CYMAKE line containing currypp call
-- in a source text by blank line (to avoid recursive calls): -- in a source text by blank line (to avoid recursive calls):
......
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