Commit bb371ce1 by Michael Hanus

### Non-determinism dependency analysis extended

parent efa14f9c
 ... ... @@ -16,6 +16,8 @@ import Configuration (docDir) -------------------------------------------------------------------------- --- Gets the documentation of an analysis with a registered name. --- Returns `Nothing` if no documentation exist. --- The documentation of an analysis with name AN is usually stored --- in the file `/currytools/CASS/Docs/AN.md`. getAnalysisDoc :: String -> IO (Maybe String) getAnalysisDoc aname = do let docfilename = docDir aname <.> "md" ... ...
 ... ... @@ -5,5 +5,5 @@ 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, if its definition contains overlapping left-hand sides or free variables, or if it depends on some non-deterministic operation.
 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, 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`.
 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, 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.
 -- 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]
 -- 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: []
 ... ... @@ -5,7 +5,13 @@ --- @version January 2015 ----------------------------------------------------------------------- module GenericProgInfo where module GenericProgInfo ( ProgInfo, emptyProgInfo, lookupProgInfo, combineProgInfo , lists2ProgInfo, publicListFromProgInfo, progInfo2Lists, progInfo2XML , mapProgInfo, publicProgInfo , showProgInfo, equalProgInfo , readAnalysisFiles, readAnalysisPublicFile, writeAnalysisFiles ) where import Configuration(debugMessage) import Directory(removeFile) ... ... @@ -66,6 +72,16 @@ mapProgInfo func (ProgInfo map1 map2) = publicProgInfo :: ProgInfo a -> ProgInfo a publicProgInfo (ProgInfo pub _) = ProgInfo pub (emptyFM (<)) --- Show a ProgInfo as a string (used for debugging only). showProgInfo :: ProgInfo _ -> String showProgInfo (ProgInfo fm1 fm2) = "Public: "++showFM fm1++"\nPrivate: "++showFM fm2 -- Equality on ProgInfo equalProgInfo :: ProgInfo a -> ProgInfo a -> Bool equalProgInfo (ProgInfo pi1p pi1v) (ProgInfo pi2p pi2v) = eqFM pi1p pi2p && eqFM pi1v pi2v --- Writes a ProgInfo into a file. writeAnalysisFiles :: String -> ProgInfo _ -> IO () writeAnalysisFiles basefname (ProgInfo pub priv) = do ... ... @@ -103,12 +119,4 @@ readAnalysisPublicFile fname = do putStrLn "Please try to re-run the analysis!" ioError err) --- Show a ProgInfo as a string (used for debugging only). showProgInfo :: ProgInfo _ -> String showProgInfo (ProgInfo fm1 fm2) = "Public: "++showFM fm1++"\nPrivate: "++showFM fm2 -- Equality on ProgInfo equalProgInfo :: ProgInfo a -> ProgInfo a -> Bool equalProgInfo (ProgInfo pi1p pi1v) (ProgInfo pi2p pi2v) = eqFM pi1p pi2p && eqFM pi1v pi2v -----------------------------------------------------------------------
 ... ... @@ -3,22 +3,24 @@ --- persistently in files. --- --- @author Heiko Hoffmann, Michael Hanus --- @version January 2015 --- @version July 2016 -------------------------------------------------------------------------- module LoadAnalysis where import Directory import Distribution(stripCurrySuffix) import FlatCurry.Types(QName) import FilePath import System(system) import GenericProgInfo import Configuration(debugMessage,getWithPrelude) import IO import FiniteMap import ReadShowTerm(readQTerm,showQTerm) import FlatCurry.Types(QName) import IO import List(isPrefixOf, isSuffixOf) import ReadShowTerm(readQTerm, showQTerm) import System(system) import Configuration(debugMessage, getWithPrelude) import CurryFiles(findModuleSourceInLoadPath) import GenericProgInfo --- Get the file name in which analysis results are stored ... ... @@ -122,9 +124,24 @@ createDirectoryR maindir = createDirectory createdDir createDirectories createdDir dirs -- delete all savefiles of analysis deleteAnalysisFiles :: String -> IO Int deleteAnalysisFiles ananame = do --- Deletes all analysis files for a given analysis name. deleteAllAnalysisFiles :: String -> IO () deleteAllAnalysisFiles ananame = do analysisDir <- getAnalysisDirectory system ("find "++analysisDir++" -name '*."++ananame++"' -type f -delete") deleteAllInDir analysisDir where deleteAllInDir dir = do dircont <- getDirectoryContents dir mapIO_ processDirElem (filter (not . isPrefixOf ".") dircont) where processDirElem f = do let fullname = dir f when (isAnaFile f) \$ do putStrLn ("DELETE: " ++ fullname) removeFile fullname isdir <- doesDirectoryExist fullname when isdir \$ deleteAllInDir fullname isAnaFile f = (".pub" `isSuffixOf` f && ('.':ananame) `isSuffixOf` dropExtension f) || (".priv" `isSuffixOf` f && ('.':ananame) `isSuffixOf` dropExtension f)
 ... ... @@ -2,7 +2,7 @@ --- This is the main module to start the executable of the analysis system. --- --- @author Michael Hanus --- @version June 2016 --- @version July 2016 -------------------------------------------------------------------------- module Main(main) where ... ... @@ -16,6 +16,7 @@ import System (exitWith,getArgs) import AnalysisDoc (getAnalysisDoc) import AnalysisServer import Configuration import LoadAnalysis (deleteAllAnalysisFiles) import Registry --- Main function to start the analysis system. ... ... @@ -30,6 +31,7 @@ main = do (putStr (unlines opterrors) >> putStr usageText >> exitWith 1) initializeAnalysisSystem when (optHelp opts) (printHelp args >> exitWith 1) when (optDelete opts) (deleteFiles args) when ((optServer opts && not (null args)) || (not (optServer opts) && length args /= 2)) (error "Illegal arguments (try `-h' for help)" >> exitWith 1) ... ... @@ -43,8 +45,18 @@ main = do in if ananame `elem` registeredAnalysisNames then analyzeModuleAsText ananame (stripCurrySuffix mname) (optReAna opts) >>= putStrLn else error \$ "Unknown analysis name `"++ ananame ++ "' (try `-h' for help)" else anaUnknownError ananame where deleteFiles args = case args of [aname] -> if aname `elem` registeredAnalysisNames then deleteAllAnalysisFiles aname >> exitWith 0 else anaUnknownError aname [] -> error "Missing analysis name!" _ -> error "Too many arguments (only analysis name should be given)!" anaUnknownError aname = error \$ "Unknown analysis name `"++ aname ++ "' (try `-h' for help)" -------------------------------------------------------------------------- -- Representation of command line options. ... ... @@ -53,7 +65,8 @@ data Options = Options , optVerb :: Int -- verbosity level , optServer :: Bool -- start CASS in server mode? , optPort :: Int -- port number (if used in server mode) , optReAna :: Bool -- fore re-analysis? , optReAna :: Bool -- force re-analysis? , optDelete :: Bool -- delete analysis files? , optProp :: [(String,String)] -- property (of ~/.curryanalsisrc) to be set } ... ... @@ -65,6 +78,7 @@ defaultOptions = Options , optServer = False , optPort = 0 , optReAna = False , optDelete = False , optProp = [] } ... ... @@ -87,6 +101,9 @@ options = , Option "r" ["reanalyze"] (NoArg (\opts -> opts { optReAna = True })) "force re-analysis \n(i.e., ignore old analysis information)" , Option "d" ["delete"] (NoArg (\opts -> opts { optDelete = True })) "delete existing analysis results" , Option "D" [] (ReqArg checkSetProperty "name=v") "set property (of ~/.curryanalysisrc)\n`name' as `v'" ... ... @@ -131,7 +148,7 @@ usageText = "(use option `-h ' for more documentation)" : "" : map showAnaInfo registeredAnalysisInfos) where maxName = foldr1 max (map (length . fst) registeredAnalysisInfos) maxName = foldr1 max (map (length . fst) registeredAnalysisInfos) + 1 showAnaInfo (n,t) = n ++ take (maxName - length n) (repeat ' ') ++ ": " ++ t --------------------------------------------------------------------------
 ... ... @@ -5,7 +5,7 @@ --- registered in the top part of this module. --- --- @author Heiko Hoffmann, Michael Hanus --- @version June 2015 --- @version July 2016 -------------------------------------------------------------------- module Registry ... ... @@ -53,6 +53,8 @@ registeredAnalysis = ,cassAnalysis "Deterministic operations" nondetAnalysis showDet ,cassAnalysis "Depends on non-deterministic operations" nondetDepAnalysis showNonDetDeps ,cassAnalysis "Depends on all non-deterministic operations" nondetDepAllAnalysis showNonDetDeps ,cassAnalysis "Right-linear operations" rlinAnalysis showRightLinear ,cassAnalysis "Solution completeness" solcompAnalysis showSolComplete ,cassAnalysis "Pattern completeness" patCompAnalysis showComplete ... ...
 ... ... @@ -5,16 +5,17 @@ --- different computation paths. --- --- @author Michael Hanus --- @version September 2013 --- @version July 2016 ------------------------------------------------------------------------------ module Deterministic ( overlapAnalysis, showOverlap, showDet , Deterministic(..),nondetAnalysis , showNonDetDeps, nondetDepAnalysis , showNonDetDeps, nondetDepAnalysis, nondetDepAllAnalysis ) where import Analysis import Char(isDigit) import FlatCurry.Types import FlatCurry.Goodies import List ... ... @@ -114,23 +115,57 @@ type NonDetDeps = [QName] showNonDetDeps :: AOutFormat -> NonDetDeps -> String showNonDetDeps AText [] = "deterministic" showNonDetDeps ANote [] = "" showNonDetDeps fmt (x:xs) = (if fmt==AText then "depends on non-deterministic operations: " else "") ++ intercalate "," (map (\ (mn,fn) -> mn++"."++fn) (x:xs)) showNonDetDeps AText xs@(_:_) = "depends on non-deterministic operations: " ++ intercalate ", " (map (\ (mn,fn) -> mn++"."++fn) xs) showNonDetDeps ANote xs@(_:_) = intercalate " " (map snd xs) --- Non-deterministic dependency analysis. --- The analysis computes for each operation the set of operations --- with a non-deterministic definition which might be called by this --- operation. 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. nondetDepAnalysis :: Analysis NonDetDeps nondetDepAnalysis = dependencyFuncAnalysis "NonDetDependency" [] nondetDeps nondetDepAnalysis = dependencyFuncAnalysis "NonDetDeps" [] (nondetDeps False) --- Non-deterministic dependency analysis. --- The analysis computes for each operation the set of *all* operations --- with a non-deterministic definition which might be called by this --- operation. nondetDepAllAnalysis :: Analysis NonDetDeps nondetDepAllAnalysis = dependencyFuncAnalysis "NonDetAllDeps" [] (nondetDeps True) -- An operation is non-deterministic if its definition is potentially -- non-deterministic (i.e., the dependency is the operation itself) -- or it depends on some called non-deterministic function. -- TODO: check if non-determinism is encapsulated by set function -- so that it is actually a deterministic function nondetDeps :: FuncDecl -> [(QName,NonDetDeps)] -> NonDetDeps nondetDeps func calledFuncs = nondetDeps :: Bool -> FuncDecl -> [(QName,NonDetDeps)] -> NonDetDeps nondetDeps alldeps func@(Func f _ _ _ rule) calledFuncs = if isNondetDefined func then [funcName func] else sort (nub (concatMap snd calledFuncs)) then f : (if alldeps then sort (nub (calledNDFuncsInRule rule)) else []) else sort (nub (calledNDFuncsInRule rule)) where calledNDFuncsInRule (Rule _ e) = calledNDFuncs e calledNDFuncsInRule (External _) = [] calledNDFuncs (Var _) = [] calledNDFuncs (Lit _) = [] calledNDFuncs (Free vars e) = calledNDFuncs e calledNDFuncs (Let bs e) = concatMap calledNDFuncs (map snd bs) ++ calledNDFuncs e calledNDFuncs (Or e1 e2) = calledNDFuncs e1 ++ calledNDFuncs e2 calledNDFuncs (Case _ e bs) = calledNDFuncs e ++ concatMap (\ (Branch _ be) -> calledNDFuncs be) bs calledNDFuncs (Typed e _) = calledNDFuncs e calledNDFuncs (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 [] -- this case should not occur else concatMap calledNDFuncs (tail es) | otherwise = maybe [] id (lookup qf calledFuncs) ++ (concatMap calledNDFuncs es) ------------------------------------------------------------------------------
 ... ... @@ -33,9 +33,9 @@ type RootReplaced = [QName] showRootRepl :: AOutFormat -> RootReplaced -> String showRootRepl AText [] = "no root replacements" showRootRepl ANote [] = "" showRootRepl fmt (x:xs) = (if fmt==AText then "root replacements: " else "") ++ intercalate "," (map (\ (mn,fn) -> mn++"."++fn) (x:xs)) showRootRepl AText xs@(_:_) = "root replacements: " ++ intercalate "," (map (\ (mn,fn) -> mn++"."++fn) xs) showRootRepl ANote xs@(_:_) = "[" ++ intercalate "," (map snd xs) ++ "]" --- Root replacement analysis. rootReplAnalysis :: Analysis RootReplaced ... ...
 ... ... @@ -3,38 +3,39 @@ --- programs. --- --- @author Michael Hanus --- @version April 2016 --- @version July 2016 --------------------------------------------------------------------- module BrowserGUI where import GUI import Read import IOExts import Imports import Directory import Distribution import FileGoodies import FlatCurry.Types import FlatCurry.Files import FlatCurry.Goodies import FlatCurry.Show import ShowFlatCurry(leqFunc,funcModule) import System import FileGoodies import List import GUI import Imports import IOExts import List (isPrefixOf,delete,union) import Maybe import Read import Sort (sortBy) import System import Time (toCalendarTime,calendarTimeToString) import AnalysisTypes import BrowserAnalysis import Sort import Dependency(callsDirectly,indirectlyDependent) import ShowGraph import Dependency (callsDirectly,indirectlyDependent) import ImportCalls import Directory import Time(toCalendarTime,calendarTimeToString) import Distribution import ShowFlatCurry (leqFunc,funcModule) import ShowGraph import Analysis (AOutFormat(..)) import AnalysisDoc (getAnalysisDoc) import AnalysisServer (initializeAnalysisSystem,analyzeModuleForBrowser) import Registry (functionAnalysisInfos) import Analysis (AOutFormat(..)) import AnalysisDoc (getAnalysisDoc) import AnalysisServer (initializeAnalysisSystem,analyzeModuleForBrowser) import Registry (functionAnalysisInfos) --------------------------------------------------------------------- -- Set this constant to True if the execution times of the main operations ... ... @@ -48,7 +49,7 @@ title :: String title = "CurryBrowser" version :: String version = "Version of 16/01/2015" version = "Version of 29/07/2016" patchReadmeVersion :: IO () patchReadmeVersion = do ... ... @@ -204,7 +205,7 @@ getFuns gs = readIORef gs >>= \ (GS _ _ _ funs _ _ _) -> return funs storeSelectedFunctions :: IORef GuiState -> [FuncDecl] -> IO () storeSelectedFunctions gs funs = do (GS t mm ms _ ct flag fana) <- readIORef gs writeIORef gs (GS t mm ms (mergeSortBy leqFunc funs) ct flag fana) writeIORef gs (GS t mm ms (sortBy leqFunc funs) ct flag fana) setMainContentsModule :: IORef GuiState -> String -> ContentsKind -> String -> IO () ... ... @@ -341,7 +342,7 @@ browserGUI gstate rmod rtxt names = Menu (map (\ (aname,atitle) -> MButton (showMBusy (analyzeAllFunsWithCASS aname atitle)) atitle) functionAnalysisInfos)], (sortBy (\i1 i2 -> snd i1 <= snd i2) functionAnalysisInfos))], row [MenuButton [Text "Select functions...", Menu [MButton (showMBusy (executeForModule showExportedFuns)) ... ... @@ -581,7 +582,7 @@ browserGUI gstate rmod rtxt names = if mod==Nothing || null self then done else getFuns gstate >>= \funs -> let mainfun = funs!!(readNat self) qfnames = mergeSortBy leqQName qfnames = sortBy leqQName (union [funcName mainfun] (callsDirectly mainfun)) in getAllFunctions gstate (showDoing gp) (fromJust mod) >>= \allfuns -> storeSelectedFunctions gstate (map (findDecl4name allfuns) qfnames) >> ... ... @@ -596,7 +597,7 @@ browserGUI gstate rmod rtxt names = getFuns gstate >>= \funs -> let mainfun = funcName (funs!!(readNat self)) in getAllFunctions gstate (showDoing gp) (fromJust mod) >>= \allfuns -> let qfnames = mergeSortBy leqQName let qfnames = sortBy leqQName (union [mainfun] (fromJust (lookup mainfun (indirectlyDependent allfuns)))) in storeSelectedFunctions gstate (map (findDecl4name allfuns) qfnames) >> ... ... @@ -773,7 +774,7 @@ browserDir = installDir++"/currytools/browser" -- order qualified names by basename first: leqQName :: QName -> QName -> Bool leqQName (mod1,n1) (mod2,n2) = leqString n1 n2 || n1==n2 && leqString mod1 mod2 leqQName (mod1,n1) (mod2,n2) = n1 <= n2 || n1==n2 && mod1 <= mod2 -- show qualified name with module: showQNameWithMod :: QName -> String ... ...
 ... ... @@ -12,7 +12,7 @@ they have no effect. Developed by Michael Hanus (CAU Kiel, Germany, mh@informatik.uni-kiel.de) Version of 16/01/2015 Version of 29/07/2016 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