blob: 255e7ecf63f1047c26676a9817d0ba5b039f3f73 (
plain)
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
|
// ####################################################################
/// This module is intended to store and handle configuration options
///
/// author: Aleksandar Milicevic (t-alekm@microsoft.com)
// ####################################################################
module Options
open Utils
type Config = {
help : bool;
inputFilename : string;
methodToSynth : string;
constructorsOnly : bool;
inferConditionals : bool;
verifyPartialSolutions : bool;
verifySolutions : bool;
checkUnifications : bool;
genRepr : bool;
genMod : bool;
timeout : int;
numLoopUnrolls : int;
recursiveValid : bool;
breakIntoDebugger : bool;
}
type CfgOption<'a> = {
optionName: string;
optionType: string;
optionSetter: 'a -> Config -> Config;
descr: string;
}
exception InvalidCmdLineArg of string
exception InvalidCmdLineOption of string
let CheckNonEmpty value optName =
if value = "" then raise (InvalidCmdLineArg("A value for option " + optName + " must not be empty")) else value
let CheckInt value optName =
try
System.Int32.Parse value
with
| ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be a boolean"))
let CheckBool value optName =
if value = "" then
true
else
try
System.Boolean.Parse value
with
| ex -> raise (InvalidCmdLineArg("A value for option " + optName + " must be an integer"))
let cfgOptions = [
{ optionName = "help"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with help = CheckBool v "help"}); descr = "description not available"; }
{ optionName = "method"; optionType = "string"; optionSetter = (fun v (cfg: Config) -> {cfg with methodToSynth = CheckNonEmpty v "method"}); descr = "description not available"; }
{ optionName = "constrOnly"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with constructorsOnly = CheckBool v "constrOnly"}); descr = "description not available"; }
{ optionName = "inferConds"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals = CheckBool v "inferConds"}); descr = "description not available"; }
{ optionName = "noInferConds"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with inferConditionals = not (CheckBool v "inferConds")}); descr = "description not available"; }
{ optionName = "verifyParSol"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions = CheckBool v "verifyParSol"}); descr = "description not available"; }
{ optionName = "noVerifyParSol"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with verifyPartialSolutions = not (CheckBool v "verifyParSol")}); descr = "description not available"; }
{ optionName = "verifySol"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with verifySolutions = CheckBool v "verifySol"}); descr = "description not available"; }
{ optionName = "noVerifySol"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with verifySolutions = not (CheckBool v "verifySol")}); descr = "description not available"; }
{ optionName = "checkUnifs"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with checkUnifications = CheckBool v "checkUnifs"}); descr = "description not available"; }
{ optionName = "noCheckUnifs"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with checkUnifications = not (CheckBool v "noCheckUnifs")}); descr = "description not available"; }
{ optionName = "genRepr"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with genRepr = CheckBool v "genRepr"}); descr = "description not available"; }
{ optionName = "noGenRepr"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with genRepr = not (CheckBool v "noGenRepr")}); descr = "description not available"; }
{ optionName = "genMod"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with genMod = CheckBool v "genMod"}); descr = "description not available"; }
{ optionName = "noGenMod"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with genMod = not (CheckBool v "noGenMod")}); descr = "description not available"; }
{ optionName = "timeout"; optionType = "int"; optionSetter = (fun v (cfg: Config) -> {cfg with timeout = CheckInt v "timeout"}); descr = "description not available"; }
{ optionName = "unrolls"; optionType = "int"; optionSetter = (fun v (cfg: Config) -> {cfg with numLoopUnrolls = CheckInt v "unrolls"}); descr = "description not available"; }
{ optionName = "recValid"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with recursiveValid = CheckBool v "recValid"}); descr = "description not available"; }
{ optionName = "noRecValid"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with recursiveValid = not (CheckBool v "noRecValid")}); descr = "description not available"; }
{ optionName = "break"; optionType = "bool"; optionSetter = (fun v (cfg: Config) -> {cfg with breakIntoDebugger = CheckBool v "break"}); descr = "launches debugger upon start-up"; }
]
let cfgOptMap = cfgOptions |> List.fold (fun acc o -> acc |> Map.add o.optionName o) Map.empty
let newline = System.Environment.NewLine
let PrintHelpMsg =
let maxw = cfgOptions |> List.fold (fun acc o -> if String.length o.optionName > acc then String.length o.optionName else acc) 0
let maxwStr = sprintf "%d" (maxw + 2)
let strf = new Printf.StringFormat<_>(" %-" + maxwStr + "s: %-6s | %s")
let rec __PrintHelp optLst =
match optLst with
| fs :: [] -> (sprintf strf fs.optionName fs.optionType fs.descr)
| fs :: rest -> (sprintf strf fs.optionName fs.optionType fs.descr) + newline + (__PrintHelp rest)
| [] -> ""
(* --- function body starts here --- *)
newline +
"Jennisys usage: Jennisys [ option ... ] filename" + newline +
" where <option> is one of " + newline + newline +
" ----- General options -----------------------------------------------------" + newline +
" (available switches are: /, -, --)" + newline + newline +
(__PrintHelp cfgOptions)
let defaultConfig: Config = {
help = false;
inputFilename = "";
inferConditionals = true;
methodToSynth = "*";
constructorsOnly = false;
verifyPartialSolutions = true;
verifySolutions = true;
checkUnifications = false;
genRepr = true;
genMod = false;
timeout = 0;
numLoopUnrolls = 2;
recursiveValid = true;
breakIntoDebugger = false;
}
/// Should not be mutated outside the ParseCmdLineArgs method, which is
/// typically called only once at the beginning of the program execution
let mutable CONFIG = defaultConfig
let ParseCmdLineArgs args =
let __StripSwitches str =
match str with
| Prefix "--" x
| Prefix "-" x
| Prefix "/" x -> x
| _ -> str
let __Split (str: string) =
let stripped = __StripSwitches str
if stripped = str then
("",str)
else
let splits = stripped.Split([| ':' |])
if splits.Length > 2 then raise (InvalidCmdLineOption("more than 2 colons in " + str))
if splits.Length = 2 then
let opt = splits.[0]
let value = splits.[1]
(opt,value)
else
let x = __StripSwitches splits.[0]
(x, "")
let rec __Parse args cfg =
match args with
| fs :: rest ->
let opt,value = __Split fs
if opt = "" then
__Parse rest { cfg with inputFilename = CheckNonEmpty value opt }
else
match Map.tryFind opt cfgOptMap with
| Some(opt) -> __Parse rest (opt.optionSetter value cfg)
| None -> raise (InvalidCmdLineOption("Unknown option: " + opt))
| [] -> cfg
(* --- function body starts here --- *)
CONFIG <- __Parse args defaultConfig
|
