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 :: (IORef ProgInfo) -> String -> (QName,Int,[Int]) -> [(QName,ConsInfo)] -> Int -> [(Int,TypeExpr,Expr)] -> (VarTypesMap a) -> (Expr -> Expr) -> (Map QName (ACallType a)) -> (Map QName (ACallType a)) -> (Map QName (InOutType a)) -> [(QName,Int,Expr)] -> [(QName,Int,Expr,[QName])] -> [(QName,ACallType a)] -> (Map QName NonFailCond) -> [(QName,NonFailCond)] -> [(QName,NonFailCond)] -> (Int,Int,Int) -> Options -> VerifyState a
Fields:
- vstModules :: (IORef ProgInfo)
- vstCurrModule :: String
- vstCurrFunc :: (QName,Int,[Int])
- vstConsInfos :: [(QName,ConsInfo)]
- vstFreshVar :: Int
- vstVarExp :: [(Int,TypeExpr,Expr)]
- vstVarTypes :: (VarTypesMap a)
- vstCondition :: (Expr -> Expr)
- 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)]
- vstImpFunConds :: (Map QName NonFailCond)
- vstFunConds :: [(QName,NonFailCond)]
- vstNewFunConds :: [(QName,NonFailCond)]
- vstStats :: (Int,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 ProgInfo -> IORef (AnalysisStore a) -> Options -> String -> IO ()

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)

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)

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)

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

Prints a message about the result of the module verification.

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

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)

Initializes the verification state.

currentFuncDecls :: TermDomain a => VerifyState a -> IO [FuncDecl]

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

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

getConsInfos :: TermDomain a => StateT (VerifyState a) IO [((String,String),(Int,ConsType,[((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 ()

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

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

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

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

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

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

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

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

addVarExps :: TermDomain a => [(Int,TypeExpr,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 ()

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

getExpandedCondition :: TermDomain a => StateT (VerifyState a) IO Expr

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

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

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

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

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

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

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

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

incrUnsatSMT :: 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] -> TypeExpr -> Expr -> StateT (VerifyState a) IO ()

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

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 => Expr -> (String,String) -> [Int] -> StateT (VerifyState a) IO ()

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

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

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

restoreBranchState :: TermDomain a => ([(Int,TypeExpr,Expr)],[(Int,[(InOutType a,[Int])])],Expr -> Expr) -> 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 :: Options -> String -> a -> IO ()

showSimpExp :: Expr -> String

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

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

Exported names:

Imported modules:

Module Main

Summary of exported operations:

Exported datatypes:

Exported operations: