1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168

-------------------------------------------------------------------------
--- The options of the contract verification tool together with some
--- related operations.
---
--- @author Michael Hanus
--- @version February 2022
-------------------------------------------------------------------------

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
  }

--- 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
  }

--- 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"
  ]
 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)"

-------------------------------------------------------------------------