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.

Summary of exported operations:

Exported datatypes:

VerifyState

Constructors:

VerifyState :: [FuncDecl] -> (QName,Int,[Int]) -> [[(QName,Int)]] -> Int -> [(Int,Expr)] -> (VarTypesMap a) -> (Map QName (ACallType a)) -> (Map QName (ACallType a)) -> (Map QName (InOutType a)) -> [(QName,Int,Expr)] -> [(QName,Int,Expr,[QName])] -> [(QName,ACallType a)] -> (Int,Int) -> Options -> VerifyState a
Fields:
- vstFuncDecls :: [FuncDecl]
- vstCurrFunc :: (QName,Int,[Int])
- vstAllCons :: [[(QName,Int)]]
- vstFreshVar :: Int
- vstVarExp :: [(Int,Expr)]
- vstVarTypes :: (VarTypesMap a)
- vstImpCallTypes :: (Map QName (ACallType a))
- vstCallTypes :: (Map QName (ACallType a))
- vstIOTypes :: (Map QName (InOutType a))
- vstFailedFuncs :: [(QName,Int,Expr)]
- vstPartialBranches :: [(QName,Int,Expr,[QName])]
- vstNewFailed :: [(QName,ACallType a)]
- vstStats :: (Int,Int)
- vstToolOpts :: Options

VerifyStateM

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

Exported operations:

main :: IO ()

verifyModule :: TermDomain a => Analysis a -> IORef (AnalysisStore a) -> Options -> String -> IO ()

Verify a single module.

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

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)

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 ()

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

showVerifyResult :: TermDomain a => Options -> VerifyState a -> String -> ((String,String) -> Bool) -> IO ()

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

initVerifyState :: TermDomain a => [FuncDecl] -> [[((String,String),Int)]] -> Map (String,String) (Maybe [a]) -> Map (String,String) (Maybe [a]) -> Map (String,String) (InOutType a) -> Options -> VerifyState a

Initializes the verification state.

Further infos:

solution complete, i.e., able to compute all solutions

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

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

getAllCons :: TermDomain a => StateT (VerifyState a) IO [[((String,String),Int)]]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

incrNonTrivialCall :: TermDomain a => StateT (VerifyState a) IO ()

incrIncompleteCases :: TermDomain a => StateT (VerifyState a) IO ()

getToolOptions :: TermDomain a => StateT (VerifyState a) IO Options

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

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

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

noVerifyFunctions :: [(String,String)]

Further infos:

solution complete, i.e., able to compute all solutions

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

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

showBindExp :: Int -> Expr -> String

showExp :: Expr -> String

ppExp :: Expr -> Doc

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

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

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

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

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

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

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

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

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]

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

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

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

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

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

A list of any types of a given length.

enforceNormalForm :: a -> IO ()

Exported names:

Imported modules:

Module Main

Summary of exported operations:

Exported datatypes:

Exported operations: