Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/options_management.ml | ||
---|---|---|
13 | 13 |
let print_version () = |
14 | 14 |
let open Utils.Format in |
15 | 15 |
printf |
16 |
"@[<v>\ |
|
17 |
Lustrec compiler, version %s (%s)@,\ |
|
16 |
"@[<v>Lustrec compiler, version %s (%s)@,\ |
|
18 | 17 |
Standard lib: %s@,\ |
19 |
User provided include directory: @[<h>%a@]\ |
|
20 |
@]@." |
|
21 |
version codename |
|
18 |
User provided include directory: @[<h>%a@]@]@." version codename |
|
22 | 19 |
Version.include_path |
23 |
(pp_print_list ~pp_sep:pp_print_space pp_print_string) !include_dirs |
|
20 |
(pp_print_list ~pp_sep:pp_print_space pp_print_string) |
|
21 |
!include_dirs |
|
24 | 22 |
|
25 | 23 |
let add_include_dir dir = |
26 | 24 |
let removed_slash_suffix = |
27 | 25 |
let len = String.length dir in |
28 |
if dir.[len-1] = '/' then |
|
29 |
String.sub dir 0 (len - 1) |
|
30 |
else |
|
31 |
dir |
|
26 |
if dir.[len - 1] = '/' then String.sub dir 0 (len - 1) else dir |
|
32 | 27 |
in |
33 | 28 |
include_dirs := removed_slash_suffix :: !include_dirs |
34 | 29 |
|
35 |
|
|
36 |
(** Solving the path of required library: |
|
37 |
If local: look in the folders described in !Options.include_dirs |
|
38 |
If non local: look first as a local, then in Version.include_path: |
|
39 |
ie. in Version.include_path::!Options.include_dirs |
|
30 |
(** Solving the path of required library: If local: look in the folders |
|
31 |
described in !Options.include_dirs If non local: look first as a local, then |
|
32 |
in Version.include_path: ie. in Version.include_path::!Options.include_dirs |
|
40 | 33 |
Note that in options.ml, include folder are added as heads. One need to |
41 |
perform a fold_right to respect the order |
|
42 |
*) |
|
34 |
perform a fold_right to respect the order *) |
|
43 | 35 |
let search_lib_path (local, full_file_name) = |
44 |
let paths = (if local then !include_dirs else Version.include_path::!include_dirs) in |
|
36 |
let paths = |
|
37 |
if local then !include_dirs else Version.include_path :: !include_dirs |
|
38 |
in |
|
45 | 39 |
let name = |
46 |
List.fold_right (fun dir res -> |
|
47 |
match res with Some _ -> res |
|
48 |
| None -> |
|
49 |
let path_to_lib = dir ^ "/" ^ full_file_name in |
|
50 |
if Sys.file_exists path_to_lib then |
|
51 |
Some dir |
|
52 |
else |
|
53 |
None |
|
54 |
) |
|
55 |
paths |
|
56 |
None |
|
40 |
List.fold_right |
|
41 |
(fun dir res -> |
|
42 |
match res with |
|
43 |
| Some _ -> |
|
44 |
res |
|
45 |
| None -> |
|
46 |
let path_to_lib = dir ^ "/" ^ full_file_name in |
|
47 |
if Sys.file_exists path_to_lib then Some dir else None) |
|
48 |
paths None |
|
57 | 49 |
in |
58 | 50 |
match name with |
59 | 51 |
| None -> |
60 | 52 |
Format.eprintf "Unable to find library %s in paths %a@.@?" full_file_name |
61 |
(Utils.fprintf_list ~sep:", " Format.pp_print_string) paths; |
|
62 |
raise Not_found |
|
63 |
| Some s -> s |
|
53 |
(Utils.fprintf_list ~sep:", " Format.pp_print_string) |
|
54 |
paths; |
|
55 |
raise Not_found |
|
56 |
| Some s -> |
|
57 |
s |
|
64 | 58 |
|
65 | 59 |
(* Search for path of core libs (without lusic: arrow and io_frontend *) |
66 |
let core_dependency lib_name = |
|
67 |
search_lib_path (false, lib_name ^ ".h") |
|
60 |
let core_dependency lib_name = search_lib_path (false, lib_name ^ ".h") |
|
68 | 61 |
|
69 | 62 |
let name_dependency (_, dep) ext = |
70 | 63 |
let dir = search_lib_path (false, dep ^ ext) in |
... | ... | |
74 | 67 |
if prec > 0 then ( |
75 | 68 |
mpfr := true; |
76 | 69 |
mpfr_prec := prec; |
77 |
real_type := "mpfr"; |
|
78 |
(* salsa_enabled := false; (* We deactivate salsa *) TODO *) |
|
79 |
) |
|
80 |
else |
|
81 |
failwith "mpfr requires a positive integer" |
|
70 |
real_type := "mpfr" |
|
71 |
(* salsa_enabled := false; (* We deactivate salsa *) TODO *)) |
|
72 |
else failwith "mpfr requires a positive integer" |
|
82 | 73 |
|
83 | 74 |
let set_real_type s = |
84 | 75 |
match s with |
85 |
"mpfr" -> (
|
|
86 |
mpfr := true;
|
|
87 |
real_type := "mpfr";
|
|
88 |
)
|
|
89 |
| _ -> real_type := s
|
|
76 |
| "mpfr" ->
|
|
77 |
mpfr := true; |
|
78 |
real_type := "mpfr"
|
|
79 |
| _ ->
|
|
80 |
real_type := s
|
|
90 | 81 |
|
91 |
let setup () = |
|
92 |
Backends.setup () |
|
82 |
let setup () = Backends.setup () |
|
93 | 83 |
|
94 |
let set_backend s = |
|
95 |
output := s |
|
84 |
let set_backend s = output := s |
|
96 | 85 |
|
97 | 86 |
let common_options = |
98 |
[ "-d", Arg.Set_string dest_dir, "uses the specified \x1b[4mdirectory\x1b[0m as root for generated/imported object and C files <default: .>"; |
|
87 |
[ |
|
88 |
( "-d", |
|
89 |
Arg.Set_string dest_dir, |
|
90 |
"uses the specified \x1b[4mdirectory\x1b[0m as root for \ |
|
91 |
generated/imported object and C files <default: .>" ); |
|
99 | 92 |
"-I", Arg.String add_include_dir, "sets include \x1b[4mdirectory\x1b[0m"; |
100 | 93 |
"-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node"; |
101 | 94 |
"-print-types", Arg.Set print_types, "prints node types"; |
102 | 95 |
"-print-clocks", Arg.Set print_clocks, "prints node clocks"; |
103 |
"-print-nodes", Arg.Set print_nodes, "prints node list";
|
|
96 |
"-print-nodes", Arg.Set print_nodes, "prints node list"; |
|
104 | 97 |
"-algebraic-loop-solve", Arg.Set solve_al, "try to solve algebraic loops"; |
105 |
"-algebraic-loop-max", Arg.Set_int al_nb_max, "try to solve \x1b[4mnb\x1b[0m number of algebraic loops <default: 15>"; |
|
98 |
( "-algebraic-loop-max", |
|
99 |
Arg.Set_int al_nb_max, |
|
100 |
"try to solve \x1b[4mnb\x1b[0m number of algebraic loops <default: 15>" ); |
|
106 | 101 |
"-kind2", Arg.Set kind2_print, "active kind2 output"; |
107 |
"-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>"; |
|
102 |
( "-verbose", |
|
103 |
Arg.Set_int verbose_level, |
|
104 |
"changes verbose \x1b[4mlevel\x1b[0m <default: 1>" ); |
|
108 | 105 |
"-version", Arg.Unit print_version, " displays the version"; |
109 | 106 |
] |
110 | 107 |
|
111 | 108 |
let lustrec_options = |
112 |
common_options @ |
|
113 |
[ |
|
114 |
"-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>"; |
|
115 |
"-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>"; |
|
116 |
"-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>"; |
|
117 |
"-mpfr", Arg.Int set_mpfr, "replaces FP numbers by the MPFR library multiple precision numbers with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP numbers>"; |
|
118 |
"-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>"; |
|
119 |
"-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification"; |
|
120 |
"-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>"; |
|
121 |
"-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend"; |
|
122 |
(* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C"; *) |
|
123 |
"-ada", Arg.Unit (fun () -> set_backend "Ada"), "generates Ada encoding output instead of C"; |
|
124 |
"-horn", Arg.Unit (fun () -> set_backend "horn"), "generates Horn clauses encoding output instead of C"; |
|
125 |
"-horn-traces", Arg.Unit (fun () -> set_backend "horn"; traces:=true), "produce traceability file for Horn backend. Enable the horn backend."; |
|
126 |
"-horn-cex", Arg.Unit (fun () -> set_backend "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)"; |
|
127 |
"-horn-query", Arg.Unit (fun () -> set_backend "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)"; |
|
128 |
"-horn-sfunction", Arg.Set_string sfunction, "Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m"; |
|
109 |
common_options |
|
110 |
@ [ |
|
111 |
( "-init", |
|
112 |
Arg.Set delay_calculus, |
|
113 |
"performs an initialisation analysis for Lustre nodes <default: no \ |
|
114 |
analysis>" ); |
|
115 |
( "-dynamic", |
|
116 |
Arg.Clear static_mem, |
|
117 |
"specifies a dynamic allocation scheme for main Lustre node <default: \ |
|
118 |
static>" ); |
|
119 |
( "-check-access", |
|
120 |
Arg.Set check, |
|
121 |
"checks at runtime that array accesses always lie within bounds \ |
|
122 |
<default: no check>" ); |
|
123 |
( "-mpfr", |
|
124 |
Arg.Int set_mpfr, |
|
125 |
"replaces FP numbers by the MPFR library multiple precision numbers \ |
|
126 |
with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP \ |
|
127 |
numbers>" ); |
|
128 |
( "-lusi", |
|
129 |
Arg.Set lusi, |
|
130 |
"only generates a .lusi interface source file from a Lustre source \ |
|
131 |
<default: no generation>" ); |
|
132 |
( "-no-spec", |
|
133 |
Arg.Unit (fun () -> spec := "no"), |
|
134 |
"do not generate any specification" ); |
|
135 |
( "-acsl-spec", |
|
136 |
Arg.Unit (fun () -> spec := "acsl"), |
|
137 |
"generates an ACSL encoding of the specification. Only meaningful for \ |
|
138 |
the C backend <default>" ); |
|
139 |
( "-c-spec", |
|
140 |
Arg.Unit (fun () -> spec := "c"), |
|
141 |
"generates a C encoding of the specification instead of ACSL contracts \ |
|
142 |
and annotations. Only meaningful for the C backend" ); |
|
143 |
(* "-java", Arg.Unit (fun () -> output := "java"), "generates Java output |
|
144 |
instead of C"; *) |
|
145 |
( "-ada", |
|
146 |
Arg.Unit (fun () -> set_backend "Ada"), |
|
147 |
"generates Ada encoding output instead of C" ); |
|
148 |
( "-horn", |
|
149 |
Arg.Unit (fun () -> set_backend "horn"), |
|
150 |
"generates Horn clauses encoding output instead of C" ); |
|
151 |
( "-horn-traces", |
|
152 |
Arg.Unit |
|
153 |
(fun () -> |
|
154 |
set_backend "horn"; |
|
155 |
traces := true), |
|
156 |
"produce traceability file for Horn backend. Enable the horn backend." ); |
|
157 |
( "-horn-cex", |
|
158 |
Arg.Unit |
|
159 |
(fun () -> |
|
160 |
set_backend "horn"; |
|
161 |
horn_cex := true), |
|
162 |
"generate cex enumeration. Enable the horn backend (work in progress)" ); |
|
163 |
( "-horn-query", |
|
164 |
Arg.Unit |
|
165 |
(fun () -> |
|
166 |
set_backend "horn"; |
|
167 |
horn_query := true), |
|
168 |
"generate queries in generated Horn file. Enable the horn backend \ |
|
169 |
(work in progress)" ); |
|
170 |
( "-horn-sfunction", |
|
171 |
Arg.Set_string sfunction, |
|
172 |
"Gets the endpoint predicate of the \x1b[4msfunction\x1b[0m" ); |
|
129 | 173 |
"-print-reuse", Arg.Set print_reuse, "prints variable reuse policy"; |
130 |
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations"; |
|
131 |
"-emf", Arg.Unit (fun () -> set_backend "emf"), "generates EMF output, to be used by CocoSim"; |
|
132 |
"-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding"; |
|
133 |
"-witnesses", Arg.Set witnesses, "enables production of witnesses during compilation"; |
|
134 |
"-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>"; |
|
135 |
|
|
136 |
"-c++" , Arg.Set cpp , "c++ backend"; |
|
137 |
"-int" , Arg.Set_string int_type , "specifies the integer type (default=\"int\")"; |
|
138 |
"-real", Arg.String set_real_type, "specifies the real type (default=\"double\" without mpfr option)"; |
|
139 |
"-real-print-prec", Arg.Set_int print_prec_double, "specifies the number of digits to be printed for real values (default=15)"; |
|
140 |
"-int_div_euclidean", Arg.Set integer_div_euclidean, "interprets integer division as Euclidean (default : C division semantics)"; |
|
141 |
"-int_div_C", Arg.Clear integer_div_euclidean, "interprets integer division as C division (default)"; |
|
142 |
|
|
143 |
"-mauve", Arg.String (fun node -> mauve := node; cpp := true; static_mem := false), "generates the mauve code"; |
|
144 |
] |
|
174 |
( "-lustre", |
|
175 |
Arg.Unit (fun () -> output := "lustre"), |
|
176 |
"generates Lustre output, performing all active optimizations" ); |
|
177 |
( "-emf", |
|
178 |
Arg.Unit (fun () -> set_backend "emf"), |
|
179 |
"generates EMF output, to be used by CocoSim" ); |
|
180 |
( "-inline", |
|
181 |
Arg.Unit |
|
182 |
(fun () -> |
|
183 |
global_inline := true; |
|
184 |
const_unfold := true), |
|
185 |
"inlines all node calls (require a main node). Implies constant \ |
|
186 |
unfolding" ); |
|
187 |
( "-witnesses", |
|
188 |
Arg.Set witnesses, |
|
189 |
"enables production of witnesses during compilation" ); |
|
190 |
( "-O", |
|
191 |
Arg.Set_int optimization, |
|
192 |
"changes optimization \x1b[4mlevel\x1b[0m <default: 2>" ); |
|
193 |
"-c++", Arg.Set cpp, "c++ backend"; |
|
194 |
( "-int", |
|
195 |
Arg.Set_string int_type, |
|
196 |
"specifies the integer type (default=\"int\")" ); |
|
197 |
( "-real", |
|
198 |
Arg.String set_real_type, |
|
199 |
"specifies the real type (default=\"double\" without mpfr option)" ); |
|
200 |
( "-real-print-prec", |
|
201 |
Arg.Set_int print_prec_double, |
|
202 |
"specifies the number of digits to be printed for real values \ |
|
203 |
(default=15)" ); |
|
204 |
( "-int_div_euclidean", |
|
205 |
Arg.Set integer_div_euclidean, |
|
206 |
"interprets integer division as Euclidean (default : C division \ |
|
207 |
semantics)" ); |
|
208 |
( "-int_div_C", |
|
209 |
Arg.Clear integer_div_euclidean, |
|
210 |
"interprets integer division as C division (default)" ); |
|
211 |
( "-mauve", |
|
212 |
Arg.String |
|
213 |
(fun node -> |
|
214 |
mauve := node; |
|
215 |
cpp := true; |
|
216 |
static_mem := false), |
|
217 |
"generates the mauve code" ); |
|
218 |
] |
|
145 | 219 |
|
146 | 220 |
let lustret_options = |
147 |
common_options @ |
|
148 |
[ "-nb-mutants", Arg.Set_int nb_mutants, "\x1b[4mnumber\x1b[0m of mutants to produce <default: 1000>"; |
|
149 |
"-mcdc-cond", Arg.Set gen_mcdc, "generates MC/DC coverage"; |
|
150 |
"-no-mutation-suffix", Arg.Set no_mutation_suffix, "does not rename node with the _mutant suffix" |
|
151 |
] |
|
221 |
common_options |
|
222 |
@ [ |
|
223 |
( "-nb-mutants", |
|
224 |
Arg.Set_int nb_mutants, |
|
225 |
"\x1b[4mnumber\x1b[0m of mutants to produce <default: 1000>" ); |
|
226 |
"-mcdc-cond", Arg.Set gen_mcdc, "generates MC/DC coverage"; |
|
227 |
( "-no-mutation-suffix", |
|
228 |
Arg.Set no_mutation_suffix, |
|
229 |
"does not rename node with the _mutant suffix" ); |
|
230 |
] |
|
152 | 231 |
|
153 | 232 |
let lustrev_options = |
154 |
common_options @ |
|
155 |
[ |
|
156 |
"-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding"; |
|
157 |
"-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>"; |
|
158 |
] |
|
233 |
common_options |
|
234 |
@ [ |
|
235 |
( "-inline", |
|
236 |
Arg.Unit |
|
237 |
(fun () -> |
|
238 |
global_inline := true; |
|
239 |
const_unfold := true), |
|
240 |
"inlines all node calls (require a main node). Implies constant \ |
|
241 |
unfolding" ); |
|
242 |
( "-O", |
|
243 |
Arg.Set_int optimization, |
|
244 |
"changes optimization \x1b[4mlevel\x1b[0m <default: 2>" ); |
|
245 |
] |
|
159 | 246 |
|
160 |
|
|
161 | 247 |
let plugin_opt (name, activate, usage, options) = |
162 | 248 |
let usage () = |
163 | 249 |
Format.printf "@[<v 2>Plugin %s:@ %t@]@." name usage; |
164 | 250 |
exit 0 |
165 | 251 |
in |
166 |
( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) :: |
|
167 |
( "-" ^ name ^ "-help" , Arg.Unit usage, "plugin " ^ name ^ " help") :: |
|
168 |
(List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options) |
|
169 |
|
|
252 |
("-" ^ name, Arg.Unit activate, "activate plugin " ^ name) |
|
253 |
:: |
|
254 |
("-" ^ name ^ "-help", Arg.Unit usage, "plugin " ^ name ^ " help") |
|
255 |
:: List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options |
|
256 |
|
|
170 | 257 |
let verifier_opt (name, activate, options) = |
171 |
( "-" ^ name , Arg.Unit activate, "run verifier " ^ name ) ::
|
|
172 |
(List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
|
|
258 |
("-" ^ name, Arg.Unit activate, "run verifier " ^ name)
|
|
259 |
:: List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options
|
|
173 | 260 |
|
174 | 261 |
let get_witness_dir filename = |
175 | 262 |
(* Make sure the directory exists *) |
176 |
let dir = !dest_dir ^ "/" ^ (Filename.basename filename) ^ "_witnesses" in
|
|
177 |
let _ = try
|
|
178 |
if not (Sys.is_directory dir) then (
|
|
179 |
Format.eprintf "File of name %s exists. It should be a directory.@." dir;
|
|
180 |
exit 1
|
|
181 |
)
|
|
263 |
let dir = !dest_dir ^ "/" ^ Filename.basename filename ^ "_witnesses" in
|
|
264 |
let _ = |
|
265 |
try
|
|
266 |
if not (Sys.is_directory dir) then (
|
|
267 |
Format.eprintf "File of name %s exists. It should be a directory.@." dir;
|
|
268 |
exit 1)
|
|
182 | 269 |
with Sys_error _ -> Unix.mkdir dir 0o750 |
183 | 270 |
in |
184 | 271 |
dir |
Also available in: Unified diff
reformatting