source: Deliverables/D2.2/8051-matita-out/src/options.ml @ 2383

Last change on this file since 2383 was 2383, checked in by campbell, 8 years ago

Branch prototype so that there's a version with the matita output patch
preinstalled.

File size: 7.9 KB
Line 
1open Misc.ArgExt
2
3let default_choice       = "default"
4let option_settings_step = "during option settings"
5
6let language_from_string kind default s =
7  try 
8    Languages.from_string s
9  with Not_found -> 
10    if s = default_choice then 
11      default
12    else 
13      Error.global_error option_settings_step
14        (Printf.sprintf "`%s' is not a valid %s language." s kind)
15 
16let source_language_of_string   = language_from_string "source" Languages.Clight
17let source_language             = ref (source_language_of_string default_choice)
18let set_source_language s       = source_language := source_language_of_string s
19let get_source_language ()      = !source_language
20
21let target_language_of_string   = language_from_string "target" Languages.ASM
22let target_language             = ref (target_language_of_string default_choice)
23let set_target_language s       = target_language := target_language_of_string s
24let get_target_language ()      = !target_language
25
26let input_files                 = ref []
27let add_input_file f            = input_files := f :: !input_files
28let input_files ()              = !input_files
29
30let output_files                = ref None
31let set_output_files s          = output_files := Some s
32let get_output_files ()         = !output_files
33
34let annotation_flag             = ref false
35let request_annotation          = (:=) annotation_flag
36let annotation_requested ()     = !annotation_flag
37
38let interpretation_flag         = ref false
39let request_interpretation      = (:=) interpretation_flag
40let interpretation_requested () = !interpretation_flag
41
42let interpretations_flag         = ref false
43let request_interpretations      = (:=) interpretations_flag
44let interpretations_requested () = !interpretations_flag
45
46let debug_flag                  = ref false
47let set_debug                   = (:=) debug_flag
48let is_debug_enabled ()         = !debug_flag
49
50let reindex_flag                = ref true
51
52let transformations = ref []
53let reindexing_transformations = ref []
54let add_transformation, add_reindexing_transformation =
55  let add_to l t () = l := !l @ [t] in
56  add_to transformations, add_to reindexing_transformations
57let add_transformations (safe, reindexing) () =
58  transformations := !transformations @ safe ;
59  reindexing_transformations := !reindexing_transformations @ reindexing
60let get_transformations () =
61  if !reindex_flag then
62    !transformations @ !reindexing_transformations
63  else !transformations
64
65let cost_ternary_flag           = ref true
66let set_cost_ternary            = (:=) cost_ternary_flag
67let is_cost_ternary_enabled ()  = !cost_ternary_flag
68
69let asm_pretty_flag             = ref false
70let set_asm_pretty              = (:=) asm_pretty_flag
71let is_asm_pretty ()            = !asm_pretty_flag
72
73let lustre_flag                 = ref false
74let set_lustre_file             = (:=) lustre_flag
75let is_lustre_file ()           = !lustre_flag
76
77let remove_lustre_externals       = ref false
78let set_remove_lustre_externals   = (:=) remove_lustre_externals
79let is_remove_lustre_externals () = !remove_lustre_externals
80
81let lustre_test                 = ref None
82let set_lustre_test s           = lustre_test := Some s
83let get_lustre_test ()          = !lustre_test
84
85let lustre_test_cases           = ref 100
86let set_lustre_test_cases       = (:=) lustre_test_cases
87let get_lustre_test_cases ()    = !lustre_test_cases
88
89let lustre_test_cycles          = ref 100
90let set_lustre_test_cycles      = (:=) lustre_test_cycles
91let get_lustre_test_cycles ()   = !lustre_test_cycles
92
93let lustre_test_min_int         = ref (-1000)
94let set_lustre_test_min_int     = (:=) lustre_test_min_int
95let get_lustre_test_min_int ()  = !lustre_test_min_int
96
97let lustre_test_max_int         = ref 1000
98let set_lustre_test_max_int     = (:=) lustre_test_max_int
99let get_lustre_test_max_int ()  = !lustre_test_max_int
100
101
102let matita_flag                 = ref false
103let is_matita_output_enabled () = !matita_flag
104
105(*
106let print_result_flag           = ref false
107let set_print_result            = (:=) print_result_flag
108let is_print_result_enabled ()  = !print_result_flag
109*)
110
111let dev_test                    = ref false
112let set_dev_test                = (:=) dev_test
113let is_dev_test_enabled ()      = !dev_test
114
115let help_specify_opt_stage ?(reind = false) (trans : Languages.transformation) =
116  extra_doc (Printf.sprintf " [%sdone in %s]"
117               (if reind then "reindexing transformation, " else "")
118               (Languages.to_string (fst trans)))
119
120let basic_optimizations =
121  ([
122    ConstPropagation.trans;
123    CopyPropagation.trans;
124    RedundancyElimination.trans;
125    CopyPropagation.trans;
126    RedundancyElimination.trans;
127    RTLConstPropagation.trans;
128    SimplePeephole.trans
129  ],[
130    LoopPeeling.trans
131  ])
132
133let options = OptionsParsing.register [
134(*
135  "-s", Arg.String set_source_language,
136  " Choose the source language between:";
137  extra_doc " Clight, Cminor";
138  extra_doc " [default is C]";
139*)
140
141  "-l", Arg.String set_target_language,
142  " Choose the target language between:";
143  extra_doc " Clight, Cminor, RTLabs, RTL, ERTL, LTL, LIN, ASM";
144  extra_doc " [default is ASM]";
145
146  "-a", Arg.Set annotation_flag,
147  " Add cost annotations on the source code.";
148
149  "-i", Arg.Set interpretation_flag,
150  " Interpret the compiled code.";
151
152  "-is", Arg.Set interpretations_flag,
153  " Interpret all the compilation passes.";
154
155  "-d", Arg.Set debug_flag,
156  " Debugging mode.";
157
158  "-o", Arg.String set_output_files,
159  " Prefix of the output files.";
160
161  "-asm-pretty", Arg.Set asm_pretty_flag,
162  " Output a pretty-printed assembly file.";
163
164  "-lustre", Arg.Set lustre_flag,
165  " Input file is a Lustre file.";
166
167  "-remove-lustre-externals", Arg.Set remove_lustre_externals,
168  " Remove Lustre externals.";
169
170  "-lustre-test", Arg.String set_lustre_test,
171  " Input file is a Lustre file, testing requested.";
172
173  "-lustre-test-cases", Arg.Int set_lustre_test_cases,
174  " Set the number of test cases when testing a Lustre";
175  extra_doc " file.";
176  extra_doc " [default is 100]";
177
178  "-lustre-test-cycles", Arg.Int set_lustre_test_cycles,
179  " Set the number of cycles for each case when testing";
180  extra_doc " a Lustre file.";
181  extra_doc " [default is 100]";
182
183  "-lustre-test-min-int", Arg.Int set_lustre_test_min_int,
184  " Random int minimum value when testing a Lustre file.";
185  extra_doc " [default is -1000]";
186
187  "-lustre-test-max-int", Arg.Int set_lustre_test_max_int,
188  " Random int maximum value when testing a Lustre file.";
189  extra_doc " [default is 1000]";
190
191  "-peel", Arg.Unit (add_reindexing_transformation LoopPeeling.trans),
192  " Apply loop peeling.";
193    help_specify_opt_stage ~reind:true LoopPeeling.trans;
194
195  "-cst-prop", Arg.Unit (add_transformations
196                           ([ConstPropagation.trans;
197                             RTLConstPropagation.trans], [])),
198  " Apply constant propagation.";
199  help_specify_opt_stage ConstPropagation.trans;
200  help_specify_opt_stage RTLConstPropagation.trans;
201
202  "-cpy-prop", Arg.Unit (add_transformation CopyPropagation.trans),
203  " Apply copy propagation.";
204    help_specify_opt_stage CopyPropagation.trans;
205
206  "-pre", Arg.Unit (add_transformation RedundancyElimination.trans),
207  " Apply partial redundancy elimination.";
208    help_specify_opt_stage RedundancyElimination.trans;
209
210  "-unroll-for",
211  Arg.Int (fun i -> add_reindexing_transformation (
212    LoopUnrolling.trans ~factor:i ()) ()),
213  " Apply loop unrolling, specifying factor.";
214  help_specify_opt_stage ~reind:true (LoopUnrolling.trans ());
215
216  "-unroll", Arg.Unit (add_reindexing_transformation (LoopUnrolling.trans ())),
217  " Apply loop unrolling.";
218  help_specify_opt_stage ~reind:true (LoopUnrolling.trans ());
219
220  "-peeph", Arg.Unit (add_transformation SimplePeephole.trans),
221  " Apply some basic peephole optimizations.";
222  help_specify_opt_stage (SimplePeephole.trans);
223
224  "-O", Arg.Unit (add_transformations basic_optimizations),
225  " Apply some optimizations.";
226
227  "-no-cost-tern",  Arg.Clear cost_ternary_flag,
228  " Replace cost ternary expressions with equivalent";
229  extra_doc " branch statements.";
230
231  "-no-reindex", Arg.Clear reindex_flag,
232  " Prevent optimizations that reindex labels.";
233(*
234  "-res", Arg.Set print_result_flag,
235  " Print the result of interpretations.";
236*)
237
238  "-dev", Arg.Set dev_test,
239  " Playground for developers.";
240
241  "-m", Arg.Set matita_flag,
242  " Output matita term (when available).";
243]
Note: See TracBrowser for help on using the repository browser.