Commit ef748e81 authored by Michael Hanus's avatar Michael Hanus
Browse files

Option -r added

parent 79c14fd8
......@@ -24,6 +24,7 @@ import Analysis.Types
import CASS.Server ( analyzeGeneric, analyzePublic )
import FlatCurry.Annotated.Types
import FlatCurry.Files
import FlatCurry.Types
import qualified FlatCurry.Goodies as FCG
import FlatCurry.Annotated.Goodies
import ShowFlatCurry ( showCurryModule )
......@@ -39,7 +40,7 @@ import VerifierState
test :: Int -> String -> IO ()
test v = analyzeNonFailing defaultOptions { optVerb = v }
test v = verifyNonFailingMod defaultOptions { optVerb = v }
testv :: String -> IO ()
testv = test 3
......@@ -61,16 +62,34 @@ main = do
if z3exists
then do
when (optVerb opts > 0) $ putStrLn banner
mapIO_ (analyzeNonFailing opts) progs
verifyNonFailingModules opts [] progs
else do
putStrLn "NON-FAILING ANALYSIS SKIPPED:"
putStrLn "The SMT solver Z3 is required for the analyzer to work"
putStrLn "but the program 'z3' is not found on the PATH!"
exitWith 1
analyzeNonFailing :: Options -> String -> IO ()
analyzeNonFailing opts modname = do
verifyNonFailingModules :: Options -> [String] -> [String] -> IO ()
verifyNonFailingModules _ _ [] = done
verifyNonFailingModules opts verifiedmods (mod:mods)
| mod `elem` verifiedmods
= verifyNonFailingModules opts verifiedmods mods
| optRec opts
= do (Prog _ imps _ _ _) <- readFlatCurryInt mod
let newimps = filter (`notElem` verifiedmods) imps
if null newimps
then do putStrLn ""
verifyNonFailingMod opts mod
verifyNonFailingModules opts (mod:verifiedmods) mods
else verifyNonFailingModules opts verifiedmods
(newimps ++ mod : (mods \\ newimps))
| otherwise -- non-recursive
= do verifyNonFailingMod opts mod
verifyNonFailingModules opts (mod:verifiedmods) mods
verifyNonFailingMod :: Options -> String -> IO ()
verifyNonFailingMod opts modname = do
printWhenStatus opts $ "Analyzing module '" ++ modname ++ "':"
prog <- readTypedFlatCurryWithSpec opts modname
impprogs <- mapIO (readTypedFlatCurryWithSpec opts) (progImports prog)
......@@ -80,7 +99,7 @@ analyzeNonFailing opts modname = do
siblingconsinfo <- loadAnalysisWithImports siblingCons prog
printWhenAll opts $ unlines $
["ORIGINAL PROGRAM:", line, showCurryModule (unAnnProg prog), line]
stats <- verifyNonFailing opts siblingconsinfo tinfo (progFuncs prog) vstate
stats <- proveNonFailingFuncs opts siblingconsinfo tinfo (progFuncs prog) vstate
when (optVerb opts > 0 || not (isVerified stats)) $
putStrLn (showStats stats)
where
......@@ -159,9 +178,9 @@ addVarTypes vts st = st { varTypes = vts ++ varTypes st }
-- a precondition check, a proof for the validity of the precondition
-- is extracted and, if the proof is successful, the operation without
-- the precondtion check `f'WithoutPreCondCheck` is called instead.
verifyNonFailing :: Options -> ProgInfo [(QName,Int)] -> TransInfo
-> [TAFuncDecl] -> VState -> IO VState
verifyNonFailing opts siblingconsinfo ti fdecls stats = do
proveNonFailingFuncs :: Options -> ProgInfo [(QName,Int)] -> TransInfo
-> [TAFuncDecl] -> VState -> IO VState
proveNonFailingFuncs opts siblingconsinfo ti fdecls stats = do
vstref <- newIORef stats
mapIO_ (proveNonFailingFunc opts siblingconsinfo ti vstref) fdecls
readIORef vstref
......
......@@ -20,6 +20,7 @@ data Options = Options
{ optVerb :: Int -- verbosity (0: quiet, 1: status, 2: interm, 3: all)
, optHelp :: Bool -- if help info should be printed
, optError :: Bool -- should `error` be considered as a failing function?
, optRec :: Bool -- recursive, i.e., verify imported modules first?
, optStrict :: Bool -- verify precondition w.r.t. strict evaluation?
-- in this case, we assume that all operations are
-- strictly evaluated which might give better results
......@@ -29,7 +30,7 @@ data Options = Options
}
defaultOptions :: Options
defaultOptions = Options 1 False False False
defaultOptions = Options 1 False False False False
--- Process the actual command line argument and return the options
--- and the name of the main program.
......@@ -60,6 +61,8 @@ options =
"verbosity level:\n0: quiet (same as `-q')\n1: show status messages (default)\n2: show intermediate results (same as `-v')\n3: show all intermediate results and more details"
, Option "e" ["error"] (NoArg (\opts -> opts { optError = True }))
"consider 'Prelude.error' as a failing operation"
, Option "r" ["recursive"] (NoArg (\opts -> opts { optRec = True }))
"recursive, i.e., verify imported modules first"
, Option "s" ["strict"] (NoArg (\opts -> opts { optStrict = True }))
"check contracts w.r.t. strict evaluation strategy"
]
......
Supports Markdown
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