Module Main

A tool to verify Curry programs w.r.t. failing computations. Thus, a program successfully verified by this tool should never fail at run-time (apart from explicit error) provided that the call types are satisfied when invoking a function.

Author: Michael Hanus

Version: October 2024

Summary of exported operations:

:: String  Deterministic 
main :: IO ()  Non-deterministic 
verifyModuleIfNew :: TermDomain a => Analysis a -> IORef ProgInfo -> IORef (AnalysisStore a) -> Options -> String -> IO ()  Non-deterministic 
Verify a single module if necessary, i.e., not previously verified.
verifyModule :: TermDomain a => Analysis a -> IORef ProgInfo -> IORef (AnalysisStore a) -> Options -> String -> Prog -> IO ()  Non-deterministic 
Verify a single module.
inferCallTypes :: TermDomain a => Options -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> ((String,String) -> Bool) -> String -> ClockTime -> Prog -> Maybe [((String,String),Maybe [a])] -> IO ([((String,String),Maybe [a])],Int,Int)  Non-deterministic 
Infer the initial (abstract) call types of all functions in a program and return them together with the number of all/public non-trivial call types.
inferIOTypes :: TermDomain a => Options -> Analysis a -> IORef (AnalysisStore a) -> ((String,String) -> Bool) -> Prog -> IO ([((String,String),InOutType a)],Int,Int)  Non-deterministic 
Infer the in/out types of all functions in a program and return them together with the number of all and public non-trivial in/out types.
showFunctionInfo :: TermDomain a => Options -> String -> VerifyState a -> IO ()  Non-deterministic 
tryVerifyProg :: TermDomain a => Options -> Int -> VerifyState a -> String -> Map (String,String) [FuncDecl] -> [FuncDecl] -> IO (Int,VerifyState a)  Non-deterministic 
printVerifyResult :: TermDomain a => Options -> VerifyState a -> String -> ((String,String) -> Bool) -> IO ()  Non-deterministic 
Prints a message about the result of the module verification.
printVerifyResults :: TermDomain a => Options -> String -> ((String,String) -> Bool) -> [FuncDecl] -> [((String,String),Maybe [a])] -> [((String,String),([(Int,TypeExpr)],Expr))] -> IO ()  Deterministic 
showIncompleteBranch :: (String,String) -> Expr -> [(String,String)] -> String  Deterministic 
initVerifyState :: TermDomain a => IORef ProgInfo -> Prog -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> Map (String,String) (Maybe [a]) -> Map (String,String) ([(Int,TypeExpr)],Expr) -> Map (String,String) (Maybe [a]) -> Map (String,String) (InOutType a) -> [((String,String),([(Int,TypeExpr)],Expr))] -> Options -> IO (VerifyState a)  Deterministic 
Initializes the verification state.
setToolError :: TermDomain a => StateT (VerifyState a) IO ()  Deterministic 
currentFuncDecls :: TermDomain a => VerifyState a -> IO [FuncDecl]  Non-deterministic 
setCurrentFunc :: TermDomain a => (String,String) -> Int -> [Int] -> StateT (VerifyState a) IO ()  Deterministic 
getCurrentFuncName :: TermDomain a => StateT (VerifyState a) IO (String,String)  Deterministic 
getConsInfos :: TermDomain a => StateT (VerifyState a) IO [((String,String),(Int,ConsType,[((String,String),Int)]))]  Deterministic 
setFreshVarIndex :: TermDomain a => Int -> StateT (VerifyState a) IO ()  Deterministic 
newFreshVarIndex :: TermDomain a => StateT (VerifyState a) IO Int  Deterministic 
addCallTypeRestriction :: TermDomain a => (String,String) -> Maybe [a] -> StateT (VerifyState a) IO ()  Deterministic 
addConditionRestriction :: TermDomain a => (String,String) -> Expr -> StateT (VerifyState a) IO ()  Non-deterministic 
setNewFunCondition :: TermDomain a => (String,String) -> ([(Int,TypeExpr)],Expr) -> StateT (VerifyState a) IO ()  Deterministic 
Sets a new non-fail condition for a function.
aCallType2Bool :: TermDomain a => [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [Int] -> Maybe [a] -> Expr  Deterministic 
Tries to generate a Boolean condition from an abstract call type, if possible.
addFailedFunc :: TermDomain a => Expr -> Maybe [(Int,a)] -> Expr -> StateT (VerifyState a) IO ()  Non-deterministic 
addMissingCase :: TermDomain a => Expr -> [(String,String)] -> StateT (VerifyState a) IO ()  Deterministic 
getVarExps :: TermDomain a => StateT (VerifyState a) IO [(Int,TypeExpr,Expr)]  Deterministic 
setVarExps :: TermDomain a => [(Int,TypeExpr,Expr)] -> StateT (VerifyState a) IO ()  Deterministic 
setVarExpTypeOf :: TermDomain a => Int -> TypeExpr -> StateT (VerifyState a) IO ()  Deterministic 
addVarExps :: TermDomain a => [(Int,TypeExpr,Expr)] -> StateT (VerifyState a) IO ()  Deterministic 
getVarTypes :: TermDomain a => StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]  Deterministic 
getVarTypeOf :: TermDomain a => Int -> StateT (VerifyState a) IO [(InOutType a,[Int])]  Deterministic 
setVarTypes :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> StateT (VerifyState a) IO ()  Deterministic 
addVarType :: TermDomain a => Int -> [(InOutType a,[Int])] -> StateT (VerifyState a) IO ()  Deterministic 
addVarTypes :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> StateT (VerifyState a) IO ()  Deterministic 
addVarAnyType :: TermDomain a => Int -> StateT (VerifyState a) IO ()  Deterministic 
removeVarAnyType :: TermDomain a => Int -> StateT (VerifyState a) IO ()  Deterministic 
getCondition :: TermDomain a => StateT (VerifyState a) IO (Expr -> Expr)  Deterministic 
getExpandedCondition :: TermDomain a => StateT (VerifyState a) IO Expr  Deterministic 
getExpandedConditionWithConj :: TermDomain a => Expr -> StateT (VerifyState a) IO Expr  Deterministic 
setCondition :: TermDomain a => (Expr -> Expr) -> StateT (VerifyState a) IO ()  Deterministic 
setCallCondition :: TermDomain a => Expr -> StateT (VerifyState a) IO ()  Deterministic 
addConjunct :: TermDomain a => Expr -> StateT (VerifyState a) IO ()  Deterministic 
addSingleCase :: TermDomain a => Int -> (String,String) -> [Int] -> StateT (VerifyState a) IO ()  Deterministic 
addEquVarCondition :: TermDomain a => Int -> Expr -> StateT (VerifyState a) IO ()  Deterministic 
getNonFailConditionOf :: TermDomain a => (String,String) -> StateT (VerifyState a) IO (Maybe ([(Int,TypeExpr)],Expr))  Deterministic 
getCallType :: TermDomain a => (String,String) -> Int -> StateT (VerifyState a) IO (Maybe [a])  Deterministic 
getFuncType :: TermDomain a => (String,String) -> Int -> StateT (VerifyState a) IO (InOutType a)  Deterministic 
incrNonTrivialCall :: TermDomain a => StateT (VerifyState a) IO ()  Deterministic 
incrIncompleteCases :: TermDomain a => StateT (VerifyState a) IO ()  Deterministic 
incrUnsatSMT :: TermDomain a => StateT (VerifyState a) IO ()  Deterministic 
getToolOptions :: TermDomain a => StateT (VerifyState a) IO Options  Deterministic 
printIfVerb :: TermDomain a => Int -> String -> StateT (VerifyState a) IO ()  Deterministic 
Prints a string with putStrLn if the verbosity is at least as the given one.
verifyFunc :: TermDomain a => FuncDecl -> StateT (VerifyState a) IO ()  Non-deterministic 
noVerifyFunctions :: [(String,String)]  Deterministic 
verifyFuncRule :: TermDomain a => [Int] -> TypeExpr -> Expr -> StateT (VerifyState a) IO ()  Non-deterministic 
showVarExpTypes :: TermDomain a => StateT (VerifyState a) IO ()  Deterministic 
verifyExpr :: TermDomain a => Bool -> Expr -> StateT (VerifyState a) IO Int  Non-deterministic 
verifyVarExpr :: TermDomain a => Int -> Expr -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]  Non-deterministic 
verifyFuncCall :: TermDomain a => Expr -> (String,String) -> [Int] -> StateT (VerifyState a) IO ()  Non-deterministic 
verifyNonTrivFuncCall :: TermDomain a => Expr -> (String,String) -> [Int] -> Maybe [a] -> Maybe ([(Int,TypeExpr)],Expr) -> StateT (VerifyState a) IO ()  Non-deterministic 
checkPredefinedOp :: TermDomain a => Expr -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])] -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]  Non-deterministic 
verifyMissingBranches :: TermDomain a => Expr -> Int -> [BranchExpr] -> StateT (VerifyState a) IO ()  Non-deterministic 
getBranchState :: TermDomain a => StateT (VerifyState a) IO ([(Int,TypeExpr,Expr)],[(Int,[(InOutType a,[Int])])],Expr -> Expr)  Deterministic 
restoreBranchState :: TermDomain a => ([(Int,TypeExpr,Expr)],[(Int,[(InOutType a,[Int])])],Expr -> Expr) -> StateT (VerifyState a) IO ()  Deterministic 
verifyBranch :: TermDomain a => Int -> Int -> BranchExpr -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]  Non-deterministic 
getVarType :: TermDomain a => Int -> [(Int,[(InOutType a,[Int])])] -> a  Deterministic 
funcDecls2Usage :: String -> [FuncDecl] -> Map (String,String) [FuncDecl]  Deterministic 
Computes for a given set of function declarations in a module a mapping from module function names to the list of function declarations where these names are used in the right-hand side.
unionFDecls :: [FuncDecl] -> [FuncDecl] -> [FuncDecl]  Deterministic 
usedFuncsInFunc :: FuncDecl -> [(String,String)]  Deterministic 
Get function names used in the right-hand side of a function declaration.
usedFuncsInRule :: Rule -> [(String,String)]  Deterministic 
Get function names used in the right-hand side of a rule.
anyTypes :: TermDomain a => Int -> [a]  Deterministic 
A list of any types of a given length.
enforceNormalForm :: Options -> String -> a -> IO ()  Deterministic 
showSimpExp :: Expr -> String  Deterministic 
isUnsatisfiable :: TermDomain a => Expr -> StateT (VerifyState a) IO Bool  Non-deterministic 
Checks the unsatisfiability of a Boolean expression w.r.t.

Exported datatypes:


VerifyState

Constructors:


VerifyStateM

Type synonym: VerifyStateM a b = StateT (VerifyState a) IO b


Exported operations:

main :: IO ()  Non-deterministic 

verifyModuleIfNew :: TermDomain a => Analysis a -> IORef ProgInfo -> IORef (AnalysisStore a) -> Options -> String -> IO ()  Non-deterministic 

Verify a single module if necessary, i.e., not previously verified.

verifyModule :: TermDomain a => Analysis a -> IORef ProgInfo -> IORef (AnalysisStore a) -> Options -> String -> Prog -> IO ()  Non-deterministic 

Verify a single module.

inferCallTypes :: TermDomain a => Options -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> ((String,String) -> Bool) -> String -> ClockTime -> Prog -> Maybe [((String,String),Maybe [a])] -> IO ([((String,String),Maybe [a])],Int,Int)  Non-deterministic 

Infer the initial (abstract) call types of all functions in a program and return them together with the number of all/public non-trivial call types. The last argument are the already stored old call types, if they are up to date.

inferIOTypes :: TermDomain a => Options -> Analysis a -> IORef (AnalysisStore a) -> ((String,String) -> Bool) -> Prog -> IO ([((String,String),InOutType a)],Int,Int)  Non-deterministic 

Infer the in/out types of all functions in a program and return them together with the number of all and public non-trivial in/out types.

showFunctionInfo :: TermDomain a => Options -> String -> VerifyState a -> IO ()  Non-deterministic 

tryVerifyProg :: TermDomain a => Options -> Int -> VerifyState a -> String -> Map (String,String) [FuncDecl] -> [FuncDecl] -> IO (Int,VerifyState a)  Non-deterministic 

printVerifyResult :: TermDomain a => Options -> VerifyState a -> String -> ((String,String) -> Bool) -> IO ()  Non-deterministic 

Prints a message about the result of the module verification.

printVerifyResults :: TermDomain a => Options -> String -> ((String,String) -> Bool) -> [FuncDecl] -> [((String,String),Maybe [a])] -> [((String,String),([(Int,TypeExpr)],Expr))] -> IO ()  Deterministic 

Further infos:
  • partially defined

showIncompleteBranch :: (String,String) -> Expr -> [(String,String)] -> String  Deterministic 

initVerifyState :: TermDomain a => IORef ProgInfo -> Prog -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> Map (String,String) (Maybe [a]) -> Map (String,String) ([(Int,TypeExpr)],Expr) -> Map (String,String) (Maybe [a]) -> Map (String,String) (InOutType a) -> [((String,String),([(Int,TypeExpr)],Expr))] -> Options -> IO (VerifyState a)  Deterministic 

Initializes the verification state.

setToolError :: TermDomain a => StateT (VerifyState a) IO ()  Deterministic 

setCurrentFunc :: TermDomain a => (String,String) -> Int -> [Int] -> StateT (VerifyState a) IO ()  Deterministic 

getCurrentFuncName :: TermDomain a => StateT (VerifyState a) IO (String,String)  Deterministic 

getConsInfos :: TermDomain a => StateT (VerifyState a) IO [((String,String),(Int,ConsType,[((String,String),Int)]))]  Deterministic 

setFreshVarIndex :: TermDomain a => Int -> StateT (VerifyState a) IO ()  Deterministic 

newFreshVarIndex :: TermDomain a => StateT (VerifyState a) IO Int  Deterministic 

addCallTypeRestriction :: TermDomain a => (String,String) -> Maybe [a] -> StateT (VerifyState a) IO ()  Deterministic 

addConditionRestriction :: TermDomain a => (String,String) -> Expr -> StateT (VerifyState a) IO ()  Non-deterministic 

setNewFunCondition :: TermDomain a => (String,String) -> ([(Int,TypeExpr)],Expr) -> StateT (VerifyState a) IO ()  Deterministic 

Sets a new non-fail condition for a function. If the function has already a new non-fail condition, they will be combined.

aCallType2Bool :: TermDomain a => [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [Int] -> Maybe [a] -> Expr  Deterministic 

Tries to generate a Boolean condition from an abstract call type, if possible.

addFailedFunc :: TermDomain a => Expr -> Maybe [(Int,a)] -> Expr -> StateT (VerifyState a) IO ()  Non-deterministic 

addMissingCase :: TermDomain a => Expr -> [(String,String)] -> StateT (VerifyState a) IO ()  Deterministic 

getVarExps :: TermDomain a => StateT (VerifyState a) IO [(Int,TypeExpr,Expr)]  Deterministic 

setVarExps :: TermDomain a => [(Int,TypeExpr,Expr)] -> StateT (VerifyState a) IO ()  Deterministic 

setVarExpTypeOf :: TermDomain a => Int -> TypeExpr -> StateT (VerifyState a) IO ()  Deterministic 

addVarExps :: TermDomain a => [(Int,TypeExpr,Expr)] -> StateT (VerifyState a) IO ()  Deterministic 

getVarTypes :: TermDomain a => StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]  Deterministic 

getVarTypeOf :: TermDomain a => Int -> StateT (VerifyState a) IO [(InOutType a,[Int])]  Deterministic 

setVarTypes :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> StateT (VerifyState a) IO ()  Deterministic 

addVarType :: TermDomain a => Int -> [(InOutType a,[Int])] -> StateT (VerifyState a) IO ()  Deterministic 

addVarTypes :: TermDomain a => [(Int,[(InOutType a,[Int])])] -> StateT (VerifyState a) IO ()  Deterministic 

addVarAnyType :: TermDomain a => Int -> StateT (VerifyState a) IO ()  Deterministic 

removeVarAnyType :: TermDomain a => Int -> StateT (VerifyState a) IO ()  Deterministic 

getCondition :: TermDomain a => StateT (VerifyState a) IO (Expr -> Expr)  Deterministic 

setCondition :: TermDomain a => (Expr -> Expr) -> StateT (VerifyState a) IO ()  Deterministic 

setCallCondition :: TermDomain a => Expr -> StateT (VerifyState a) IO ()  Deterministic 

addConjunct :: TermDomain a => Expr -> StateT (VerifyState a) IO ()  Deterministic 

addSingleCase :: TermDomain a => Int -> (String,String) -> [Int] -> StateT (VerifyState a) IO ()  Deterministic 

addEquVarCondition :: TermDomain a => Int -> Expr -> StateT (VerifyState a) IO ()  Deterministic 

getNonFailConditionOf :: TermDomain a => (String,String) -> StateT (VerifyState a) IO (Maybe ([(Int,TypeExpr)],Expr))  Deterministic 

getCallType :: TermDomain a => (String,String) -> Int -> StateT (VerifyState a) IO (Maybe [a])  Deterministic 

getFuncType :: TermDomain a => (String,String) -> Int -> StateT (VerifyState a) IO (InOutType a)  Deterministic 

Further infos:
  • partially defined

incrUnsatSMT :: TermDomain a => StateT (VerifyState a) IO ()  Deterministic 

printIfVerb :: TermDomain a => Int -> String -> StateT (VerifyState a) IO ()  Deterministic 

Prints a string with putStrLn if the verbosity is at least as the given one.

verifyFunc :: TermDomain a => FuncDecl -> StateT (VerifyState a) IO ()  Non-deterministic 

noVerifyFunctions :: [(String,String)]  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

verifyFuncRule :: TermDomain a => [Int] -> TypeExpr -> Expr -> StateT (VerifyState a) IO ()  Non-deterministic 

showVarExpTypes :: TermDomain a => StateT (VerifyState a) IO ()  Deterministic 

verifyExpr :: TermDomain a => Bool -> Expr -> StateT (VerifyState a) IO Int  Non-deterministic 

verifyVarExpr :: TermDomain a => Int -> Expr -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]  Non-deterministic 

verifyFuncCall :: TermDomain a => Expr -> (String,String) -> [Int] -> StateT (VerifyState a) IO ()  Non-deterministic 

verifyNonTrivFuncCall :: TermDomain a => Expr -> (String,String) -> [Int] -> Maybe [a] -> Maybe ([(Int,TypeExpr)],Expr) -> StateT (VerifyState a) IO ()  Non-deterministic 

checkPredefinedOp :: TermDomain a => Expr -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])] -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]  Non-deterministic 

verifyMissingBranches :: TermDomain a => Expr -> Int -> [BranchExpr] -> StateT (VerifyState a) IO ()  Non-deterministic 

getBranchState :: TermDomain a => StateT (VerifyState a) IO ([(Int,TypeExpr,Expr)],[(Int,[(InOutType a,[Int])])],Expr -> Expr)  Deterministic 

restoreBranchState :: TermDomain a => ([(Int,TypeExpr,Expr)],[(Int,[(InOutType a,[Int])])],Expr -> Expr) -> StateT (VerifyState a) IO ()  Deterministic 

verifyBranch :: TermDomain a => Int -> Int -> BranchExpr -> StateT (VerifyState a) IO [(Int,[(InOutType a,[Int])])]  Non-deterministic 

getVarType :: TermDomain a => Int -> [(Int,[(InOutType a,[Int])])] -> a  Deterministic 

funcDecls2Usage :: String -> [FuncDecl] -> Map (String,String) [FuncDecl]  Deterministic 

Computes for a given set of function declarations in a module a mapping from module function names to the list of function declarations where these names are used in the right-hand side.

unionFDecls :: [FuncDecl] -> [FuncDecl] -> [FuncDecl]  Deterministic 

usedFuncsInFunc :: FuncDecl -> [(String,String)]  Deterministic 

Get function names used in the right-hand side of a function declaration.

usedFuncsInRule :: Rule -> [(String,String)]  Deterministic 

Get function names used in the right-hand side of a rule.

anyTypes :: TermDomain a => Int -> [a]  Deterministic 

A list of any types of a given length.

enforceNormalForm :: Options -> String -> a -> IO ()  Deterministic 

Further infos:
  • partially defined

showSimpExp :: Expr -> String  Deterministic 

isUnsatisfiable :: TermDomain a => Expr -> StateT (VerifyState a) IO Bool  Non-deterministic 

Checks the unsatisfiability of a Boolean expression w.r.t. a set of variables (second argument) with an SMT solver.