Commit 83e9f4ab authored by Michael Hanus 's avatar Michael Hanus
Browse files

Determinism analysis fixed, demanded analysis added

parent 8a872fea
......@@ -37,6 +37,7 @@ import RightLinearity
import SolutionCompleteness
import TotallyDefined
import Indeterministic
import Demandedness
--- Each analysis name should be added here together with a short explanation.
--- The first component is the registered analysis name.
......@@ -47,24 +48,26 @@ import Indeterministic
analysisInfos = functionAnalysisInfos ++ typeAnalysisInfos
functionAnalysisInfos =
[("Overlapping", "Overlapping rules", "Overlapping function analysis"),
("Deterministic","Deterministic operations",
"(Non-)determinism function analysis"),
("SetValued", "Set-valued operations", "Set-valued function analysis"),
("PatComplete", "Pattern completeness", "Pattern completeness analysis"),
("Total", "Totally defined operations",
"Totally definedness analysis"),
("SolComplete", "Solution completeness","Solution completeness analysis"),
("Indeterministic","Indeterministic operations",
"Indeterminism function analysis"),
("RightLinear", "Right-linear operations","Right-linear function analysis"),
("HiOrderFunc", "Higher-order functions","Higher-order function analysis")]
[("Overlapping", "Overlapping rules", "Overlapping function analysis")
,("Deterministic","Deterministic operations",
"(Non-)determinism function analysis")
,("PatComplete", "Pattern completeness", "Pattern completeness analysis")
,("Total", "Totally defined operations",
"Totally definedness analysis")
,("SolComplete", "Solution completeness","Solution completeness analysis")
,("Indeterministic","Indeterministic operations",
"Indeterminism function analysis")
,("RightLinear", "Right-linear operations","Right-linear function analysis")
,("HiOrderFunc", "Higher-order functions","Higher-order function analysis")
,("Demand", "Demanded arguments","Demanded arguments analysis")
]
typeAnalysisInfos =
[("HiOrderType", "Higher-order datatypes", "Higher-order datatype analysis"),
("HiOrderConstr","Higher-order constructors",
"Higher-order constructor analysis"),
("SiblingCons", "Sibling constructors","Sibling constructor analysis")]
[("HiOrderType", "Higher-order datatypes", "Higher-order datatype analysis")
,("HiOrderConstr","Higher-order constructors",
"Higher-order constructor analysis")
,("SiblingCons", "Sibling constructors","Sibling constructor analysis")
]
--------------------------------------------------------------------
--- Each analysis used in our tool must be registered in this list
......@@ -72,13 +75,13 @@ typeAnalysisInfos =
registeredAnalysis :: [RegisteredAnalysis]
registeredAnalysis =
[scAnalysis overlapAnalysis showOverlap
,scAnalysis ndAnalysis showDet
,scAnalysis setValAnalysis showSetValued
,scAnalysis nondetAnalysis showDet
,scAnalysis rlinAnalysis showRightLinear
,scAnalysis solcompAnalysis showSolComplete
,scAnalysis patCompAnalysis showComplete
,scAnalysis totalAnalysis showTotally
,scAnalysis indetAnalysis showIndet
,scAnalysis demandAnalysis showDemand
,scAnalysis hiOrdType showOrder
,scAnalysis hiOrdCons showOrder
,scAnalysis hiOrdFunc show
......
......@@ -8,7 +8,7 @@
--- @version April 2013
--------------------------------------------------------------------------
module AnalysisServer(main,analyzeModuleForBrowser,analyzeGeneric,
module AnalysisServer(main, analyzeModuleForBrowser, analyzeGeneric,
analyzeInterface) where
import ReadNumeric(readNat)
......@@ -263,8 +263,9 @@ sendServerError handle errstring = do
hPutStrLn handle ("error "++errstring)
hFlush handle
-- worker threads are given changed library-search-path
changeWorkerPath _ [] = return()
-- Inform the worker threads about a given changed library search path
changeWorkerPath :: String -> [Handle] -> IO ()
changeWorkerPath _ [] = done
changeWorkerPath path (handle:whandles) = do
hPutStrLn handle (showQTerm (ChangePath path))
changeWorkerPath path whandles
......
......@@ -23,7 +23,8 @@ DEPS = Analysis.curry AnalysisCollection.curry AnalysisDependencies.curry \
$(METADIR)/FlatCurry.curry \
$(ANADIR)/Deterministic.curry $(ANADIR)/HigherOrder.curry \
$(ANADIR)/Indeterministic.curry $(ANADIR)/RightLinearity.curry \
$(ANADIR)/SolutionCompleteness.curry $(ANADIR)/TotallyDefined.curry
$(ANADIR)/SolutionCompleteness.curry $(ANADIR)/TotallyDefined.curry \
$(ANADIR)/Demandedness.curry
.PHONY: install
install: cass_worker cass
......
------------------------------------------------------------------------------
--- Demandedness analysis:
--- checks whether functions demands a particular argument, i.e.,
--- delivers only bottom if some argument is bottom.
---
--- @author Michael Hanus
--- @version April 2013
------------------------------------------------------------------------------
module Demandedness
where
import Analysis
import FlatCurry
import FlatCurryGoodies
import List((\\))
------------------------------------------------------------------------------
--- Data type to represent determinism information.
type DemandedArgs = [Int]
-- Show determinism information as a string.
showDemand :: DemandedArgs -> String
showDemand = show
-- Abstract demand domain.
data DemandDomain = Bot | Top
-- Least upper bound on abstract demand domain.
lub :: DemandDomain -> DemandDomain -> DemandDomain
lub Bot x = x
lub Top _ = Top
--- Demandedness analysis.
demandAnalysis :: Analysis DemandedArgs
demandAnalysis = dependencyFuncAnalysis "Demand" [1..] daFunc
-- An operation is non-deterministic if it has an overlapping definition.
-- or if it calls a non-deterministic operation.
daFunc :: FuncDecl -> [(QName,DemandedArgs)] -> DemandedArgs
daFunc (Func (m,f) _ _ _ rule) calledFuncs
| f `elem` ["$#","$##","$!","$!!"] && m==prelude = [1,2]
| f `elem` ["seq","ensureNotFree","apply","cond","=:<="] && m==prelude = [1]
| f `elem` ["==","=:=","compare"] && m==prelude = [1,2]
| otherwise = daFuncRule calledFuncs rule
-- TODO: >>= catch catchFail
daFuncRule :: [(QName,DemandedArgs)] -> Rule -> DemandedArgs
daFuncRule _ (External _) = [] -- nothing known about other externals
daFuncRule calledFuncs (Rule args rhs) =
map fst
(filter ((==Bot) . snd)
(map (\botarg -> (botarg,absEvalExpr rhs [botarg])) args))
where
-- abstract evaluation of an expression w.r.t. variables assumed to be Bot
absEvalExpr (Var i) bvs = if i `elem` bvs then Bot else Top
absEvalExpr (Lit _) _ = Top
absEvalExpr (Comb ct g es) bvs =
if ct == FuncCall
then maybe (error $ "Abstract value of " ++ show g ++ " not found!")
(\gdas -> let curargs = map (\ (i,e) -> (i,absEvalExpr e bvs))
(zip [1..] es)
cdas = gdas \\
(map fst (filter ((/=Bot) . snd) curargs))
in if null cdas then Top else Bot)
(lookup g calledFuncs)
else Top
absEvalExpr (Free _ e) bvs = absEvalExpr e bvs
absEvalExpr (Let bs e) bvs = absEvalExpr e (absEvalBindings bs bvs)
absEvalExpr (Or e1 e2) bvs = lub (absEvalExpr e1 bvs) (absEvalExpr e2 bvs)
absEvalExpr (Case _ e bs) bvs =
if absEvalExpr e bvs == Bot
then Bot
else foldr lub Bot (map absEvalBranch bs)
where absEvalBranch (Branch _ be) = absEvalExpr be bvs
absEvalExpr (Typed e _) bvs = absEvalExpr e bvs
-- could be improved with local fixpoint computation
absEvalBindings [] bvs = bvs
absEvalBindings ((i,exp) : bs) bvs =
let ival = absEvalExpr exp bvs
in if ival==Bot
then absEvalBindings bs (i:bvs)
else absEvalBindings bs bvs
prelude = "Prelude"
------------------------------------------------------------------------------
......@@ -8,8 +8,8 @@
--- @version March 2013
------------------------------------------------------------------------------
module Deterministic(overlapAnalysis,showOverlap,showDet,showSetValued,
Deterministic(..),ndAnalysis,setValAnalysis) where
module Deterministic(overlapAnalysis,showOverlap,showDet,
Deterministic(..),nondetAnalysis) where
import Analysis
import FlatCurry
......@@ -37,6 +37,7 @@ orInExpr (Let bs e) = any orInExpr (map snd bs) || orInExpr e
orInExpr (Or _ _) = True
orInExpr (Case _ e bs) = orInExpr e || any orInBranch bs
where orInBranch (Branch _ be) = orInExpr be
orInExpr (Typed e _) = orInExpr e
-- Show overlapping information as a string.
showOverlap :: Bool -> String
......@@ -44,52 +45,40 @@ showOverlap True = "overlapping"
showOverlap False = "non-overlapping"
------------------------------------------------------------------------------
-- 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.
--- Data type to represent determinism information.
data Deterministic = NDet | Det
--- Determinism analysis.
ndAnalysis :: Analysis Deterministic
ndAnalysis = dependencyFuncAnalysis "Deterministic" Det ndFunc
-- An operation is non-deterministic if it has an overlapping definition.
-- or if it calls a non-deterministic operation.
ndFunc :: FuncDecl -> [(QName,Deterministic)] -> Deterministic
ndFunc fdecl calledFuncs =
--trace (snd(funcName fdecl)++"...") $
if isOverlappingFunction fdecl || any (==NDet) (map snd calledFuncs)
then NDet
else Det
-- Show determinism information as a string.
showDet :: Deterministic -> String
showDet NDet = "nondeterministic"
showDet Det = "deterministic"
------------------------------------------------------------------------------
-- The set-valued analysis is a global function dependency analysis.
-- It assigns to a function a flag which is True if this function
-- might be set-valued, i.e., might reduce to different values
-- for given ground arguments.
setValAnalysis :: Analysis Bool
setValAnalysis = dependencyFuncAnalysis "SetValued" False setValFunc
nondetAnalysis :: Analysis Deterministic
nondetAnalysis = dependencyFuncAnalysis "Deterministic" Det nondetFunc
-- An operation is set-valued if its definition is potentially set-valued
-- or it depends on a set-valued function.
setValFunc :: FuncDecl -> [(QName,Bool)] -> Bool
setValFunc func calledFuncs =
isSetValuedDefined func || any snd calledFuncs
-- An operation is non-deterministic if its definition is potentially
-- non-deterministic or it depends on a non-deterministic function.
nondetFunc :: FuncDecl -> [(QName,Deterministic)] -> Deterministic
nondetFunc func calledFuncs =
if isNondetDefined func || any (==NDet) (map snd calledFuncs)
then NDet
else Det
-- Is a function f defined to be potentially set-valued, i.e., is the rule
-- nondeterministic or does it contain extra variables?
isSetValuedDefined :: FuncDecl -> Bool
isSetValuedDefined (Func f _ _ _ rule) =
-- Is a function f defined to be potentially non-deterministic, i.e.,
-- is the rule non-deterministic or does it contain extra variables?
isNondetDefined :: FuncDecl -> Bool
isNondetDefined (Func f _ _ _ rule) =
f `notElem` (map pre ["failed","$!!","$##","normalForm","groundNormalForm"])
-- these operations are internally defined in PAKCS with extra variables
&& isSetValuedRule rule
&& isNondetRule rule
isSetValuedRule (Rule _ e) = orInExpr e || extraVarInExpr e
isSetValuedRule (External _) = False
isNondetRule (Rule _ e) = orInExpr e || extraVarInExpr e
isNondetRule (External _) = False
-- check an expression for occurrences of extra variables:
......@@ -102,12 +91,7 @@ extraVarInExpr (Let bs e) = any extraVarInExpr (map snd bs) || extraVarInExpr e
extraVarInExpr (Or e1 e2) = extraVarInExpr e1 || extraVarInExpr e2
extraVarInExpr (Case _ e bs) = extraVarInExpr e || any extraVarInBranch bs
where extraVarInBranch (Branch _ be) = extraVarInExpr be
-- Show set-valued information as a string.
showSetValued :: Bool -> String
showSetValued True = "set-valued"
showSetValued False = "single-valued"
extraVarInExpr (Typed e _) = extraVarInExpr e
pre n = ("Prelude",n)
......
......@@ -6,7 +6,7 @@
--- to `SetFunctions.select` or to a committed choice.
---
--- @author Michael Hanus
--- @version March 2013
--- @version April 2013
------------------------------------------------------------------------------
module Indeterministic(indetAnalysis,showIndet) where
......@@ -52,6 +52,7 @@ choiceInExpr (Let bs e) = any choiceInExpr (map snd bs) || choiceInExpr e
choiceInExpr (Or e1 e2) = choiceInExpr e1 || choiceInExpr e2
choiceInExpr (Case _ e bs) = choiceInExpr e || any choiceInBranch bs
where choiceInBranch (Branch _ be) = choiceInExpr be
choiceInExpr (Typed e _) = choiceInExpr e
indetFuns = [("Prelude","commit"),
("Ports","send"),("Ports","doSend"),
......
......@@ -3,7 +3,7 @@
--- check whether functions are defined by right-linear rules.
---
--- @author Michael Hanus
--- @version March 2013
--- @version April 2013
------------------------------------------------------------------------------
module RightLinearity(rlinAnalysis,hasRightLinearRules,linearExpr,
......@@ -87,3 +87,4 @@ linearVariables (Case _ e bs) =
where
patternVars (Branch (Pattern _ vs) _) = vs
patternVars (Branch (LPattern _) _) = []
linearVariables (Typed e _) = linearVariables e
......@@ -4,7 +4,7 @@
--- non-rigid functions
---
--- @author Michael Hanus
--- @version March 2013
--- @version April 2013
------------------------------------------------------------------------------
module SolutionCompleteness(solcompAnalysis,showSolComplete) where
......@@ -50,6 +50,7 @@ isFlexExpr (Let bs e) = all isFlexExpr (map snd bs) && isFlexExpr e
isFlexExpr (Or e1 e2) = isFlexExpr e1 && isFlexExpr e2
isFlexExpr (Case ctype e bs) = ctype==Flex &&
all isFlexExpr (e : map (\(Branch _ be)->be) bs)
isFlexExpr (Typed e _) = isFlexExpr e
-- Show solution completeness information as a string.
showSolComplete :: Bool -> String
......
......@@ -6,7 +6,7 @@
--- constructor terms
---
--- @author Johannes Koj, Michael Hanus
--- @version March 2013
--- @version April 2013
-----------------------------------------------------------------------------
module TotallyDefined(siblingCons,
......@@ -109,6 +109,7 @@ isComplete consinfo (Case _ _ (Branch (Pattern cons _) bexp : ces)) =
checkAllCons (c:cs) (Branch (Pattern i _) e : ps) =
combineAndResults (checkAllCons (delete i (c:cs)) ps)
(isComplete consinfo e)
isComplete consinfo (Typed e _) = isComplete consinfo e
-- Combines the completeness results in different Or branches.
combineOrResults Complete _ = Complete
......
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