|
documentation:
|
------------------------------------------------------------------------------
--- Indeterminism analysis:
--- check whether functions are indeterministic, i.e., might deliver
--- different results for different runs of a program.
--- This could be the case if there are explicit or implicit calls
--- to indeterministic encapsulation operation
--- (e.g. `Control.Search.SetFunctions.select`) or operations from the module
--- `System.IO.Unsafe`.
---
--- @author Michael Hanus
--- @version February 2025
------------------------------------------------------------------------------
|
|
sourcecode:
|
module Analysis.Indeterministic ( indetAnalysis, showIndet ) where
import Analysis.Types
import FlatCurry.Types
------------------------------------------------------------------------------
--- The indeterminism analysis is a global function dependency analysis.
--- It assigns to a function a flag which is True if this function
--- might be indeterministic (i.e., calls directly or indirectly
--- some indeterministic operation.
indetAnalysis :: Analysis Bool
indetAnalysis = dependencyFuncAnalysis "Indeterministic" False indetFunc
--- An operation is indeterministic if it calls directly or indirectly
--- some indeterministic operation.
indetFunc :: FuncDecl -> [(QName,Bool)] -> Bool
indetFunc func calledFuncs =
hasIndetRules func || any snd calledFuncs
-- Show right-linearity information as a string.
showIndet :: AOutFormat -> Bool -> String
showIndet AText True = "impure (indeterministic) operation"
showIndet ANote True = "indeterministic"
showIndet AText False = "referentially transparent operation"
showIndet ANote False = ""
------------------------------------------------------------------------------
-- Check a function declaration for occurrences of indeterministic operations.
hasIndetRules :: FuncDecl -> Bool
hasIndetRules (Func _ _ _ _ (Rule _ e)) = indetInExpr e
hasIndetRules (Func _ _ _ _ (External _)) = False
-- Check an expression for occurrences of indeterministic operations.
indetInExpr :: Expr -> Bool
indetInExpr (Var _) = False
indetInExpr (Lit _) = False
indetInExpr (Comb _ f es) = isIndetFunction f || any indetInExpr es
indetInExpr (Free _ e) = indetInExpr e
indetInExpr (Let bs e) = any indetInExpr (map snd bs) || indetInExpr e
indetInExpr (Or e1 e2) = indetInExpr e1 || indetInExpr e2
indetInExpr (Case _ e bs) = indetInExpr e || any indetInBranch bs
where indetInBranch (Branch _ be) = indetInExpr be
indetInExpr (Typed e _) = indetInExpr e
-- Is the given operation indeterministic?
isIndetFunction :: QName -> Bool
isIndetFunction (mn,fn) =
(mn `elem` ["Control.Search.SetFunctions", "Control.SetFunctions"] &&
fn `elem` ["select", "selectValue"]) ||
mn `elem` ["System.IO.Unsafe", "Control.Search.Unsafe", "Control.AllValues",
"Control.Findall", "Control.Search.SearchTree.Unsafe"] ||
(mn == "Network.Ports" &&
fn `elem` ["send", "timeoutOnStream", "choiceSPEP"])
-------------------------------------------------------------------------------
|