|
sourcecode:
|
module ToolOptions
( Options(..), defaultOptions, processOptions
)
where
import Control.Monad ( when, unless )
import Data.Char ( toUpper )
import System.Console.GetOpt
import Numeric ( readNat )
import System.Process ( exitWith )
import System.CurryPath ( stripCurrySuffix )
data Options = Options
{ optVerb :: Int -- verbosity (0: quiet, 1: status, 2: interm, 3: all)
, optHelp :: Bool -- if help info should be printed
, optName :: String -- show only the name of a nonfail condition
, optError :: Bool -- should `error` be considered as a failing function?
, optRec :: Bool -- recursive, i.e., verify imported modules first?
, optConFail :: Bool -- consider pre/postconditions for failfree
-- verification?
, 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
-- but not not be correct if some argument is not
-- demanded (TODO: add demand analysis to make it
-- safe and powerful)
, optFCY :: Bool -- replace FlatCurry program?
, optAFCY :: Bool -- replace type-annotated FlatCurry program?
, optFailfree :: Bool -- verify non-failing functions?
, optContract :: Int -- contract behavior (0: nothing, 1: add, 2: verify)
, optTime :: Bool -- show elapsed verification time?
, optExamples :: Int -- the maximum number of counter examples that should
-- be generated
, optTimeout :: Int -- timeout (in seconds) for SMT prover
, optStoreProof :: Bool -- store scripts of successful contract proofs
, optInferNFCs :: Bool -- infer non-failure conditions automatically
}
--- Default options.
defaultOptions :: Options
defaultOptions = Options
{ optVerb = 1
, optHelp = False
, optName = ""
, optError = False
, optRec = False
, optConFail = False
, optStrict = False
, optFCY = False
, optAFCY = False
, optFailfree = True
, optContract = 2
, optTime = False
, optExamples = 3
, optTimeout = 4
, optStoreProof = True
, optInferNFCs = False
}
--- Process the actual command line argument and return the options
--- and the name of the main program.
processOptions :: String -> [String] -> IO (Options,[String])
processOptions banner argv = do
let (funopts, args, opterrors) = getOpt Permute options argv
opts = foldl (flip id) defaultOptions funopts
unless (null opterrors)
(putStr (unlines opterrors) >> printUsage >> exitWith 1)
when (optHelp opts) (printUsage >> exitWith 0)
return (opts, map stripCurrySuffix args)
where
printUsage = putStrLn (banner ++ "\n" ++ usageText)
-- Help text
usageText :: String
usageText =
usageInfo ("Usage: curry-failfree [options] <module names>\n") options
-- Definition of actual command line options.
options :: [OptDescr (Options -> Options)]
options =
[ Option "h?" ["help"]
(NoArg (\opts -> opts { optHelp = True }))
"print help and exit"
, Option "q" ["quiet"]
(NoArg (\opts -> opts { optVerb = 0 }))
"run quietly (no output, only exit code)"
, Option "v" ["verbosity"]
(OptArg (maybe (checkVerb 2) (safeReadNat checkVerb)) "<n>")
$ unlines
[ "verbosity level:"
, "0: quiet (same as `-q')"
, "1: show status messages (default)"
, "2: show intermediate results (same as `-v')"
, "3: show all details (e.g., SMT scripts)"
]
, Option "n" ["name"]
(ReqArg (\s opts -> opts { optName = s }) "<f>") $
"show only the names of non-fail conditions\n" ++
"and pre- and postconditions of a function <f>"
, Option "m" ["checkmode"] (ReqArg readContractMode "n|a|v") $ unlines
[ "behavior of contract checking:"
, "a: only add contract checks"
, "v: verify contracts (default)"
, "n: do nothing"
]
, Option "" ["target"]
(ReqArg checkTarget "<T>")
("target of the transformed program:\n" ++
"NONE : do not store transformed program (default)\n" ++
"FCY : write FlatCurry program\n" ++
"TAFCY: write type-annotated FlatCurry program")
, Option "f" ["no-failfree"]
(NoArg (\opts -> opts { optFailfree = False }))
"don't verify non-fail conditions"
, 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 "c" ["contract"]
(NoArg (\opts -> opts { optConFail = True }))
"consider contracts (pre/postcondition)\nfor failfree verification"
, Option "s" ["strict"]
(NoArg (\opts -> opts { optStrict = True }))
"check contracts w.r.t. strict evaluation\nstrategy"
, Option "" ["timeout"]
(ReqArg (safeReadNat (\n opts -> opts { optTimeout = n })) "<n>")
("timeout for SMT prover (default: " ++
show (optTimeout defaultOptions) ++ "s)")
, Option "" ["noproof"] (NoArg (\opts -> opts { optStoreProof = False }))
"do not write scripts of successful proofs"
, Option "t" ["time"]
(NoArg (\opts -> opts { optTime = True }))
"show total verification time for each module"
, Option "x" ["examples"]
(ReqArg (safeReadNat (\n opts -> opts {optExamples = n})) "<n>")
"maximum number of counter examples to generate"
, Option "i" ["infer"]
(NoArg (\opts -> opts { optInferNFCs = True }))
"infer non-failure conditions automatically"
]
where
safeReadNat opttrans s opts = case readNat s of
[(n,"")] -> opttrans n opts
_ -> error "Illegal number argument (try `-h' for help)"
checkVerb n opts = if n>=0 && n<4
then opts { optVerb = n }
else error "Illegal verbosity level (try `-h' for help)"
checkTarget t opts = case map toUpper t of
"NONE" -> opts { optFCY = False, optAFCY = False }
"FCY" -> opts { optFCY = True, optAFCY = False }
"TAFCY" -> opts { optFCY = False, optAFCY = True }
_ -> error $ "Illegal target `" ++ t ++ "' (try `-h' for help)"
readContractMode s opts = case s of
"n" -> opts { optContract = 0 }
"a" -> opts { optContract = 1 }
"v" -> opts { optContract = 2 }
_ -> error "Illegal contract mode (try `-h' for help)"
-------------------------------------------------------------------------
|