source: Deliverables/D2.2/8051-indexed-labels-branch/src/options.ml @ 1507

Last change on this file since 1507 was 1507, checked in by tranquil, 9 years ago
  • added an option to not use ternary expressions in costs, to accomodate frama-c explosion of such expressions
  • corrected some typos in comments
  • added a check for well behaved for loops in loop unrolling, but intelligent unrolling is not done yet
  • TODO: peeling and unrolling can contradict preciseness (with difference between introduced branches around 2 cycles). I guess it can be corrected easily
File size: 4.6 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 trace_flag         = ref false
43let request_trace = (:=) trace_flag
44let trace_requested () = !trace_flag
45
46let debug_flag                  = ref false
47let set_debug                   = (:=) debug_flag
48let is_debug_enabled ()         = !debug_flag
49
50let transformations = ref []
51let add_transformation t () = transformations := !transformations @ [t]
52let add_transformations ts () = transformations := !transformations @ ts
53let get_transformations () = !transformations
54
55let cost_ternary_flag           = ref true
56let set_cost_ternary            = (:=) cost_ternary_flag
57let is_cost_ternary_enabled ()  = !cost_ternary_flag
58
59(*
60let print_result_flag           = ref false
61let set_print_result            = (:=) print_result_flag
62let is_print_result_enabled ()  = !print_result_flag
63*)
64
65let dev_test                    = ref false
66let set_dev_test                = (:=) dev_test
67let is_dev_test_enabled ()      = !dev_test
68
69let help_specify_opt_stage (trans : Languages.transformation) =
70        Printf.sprintf "(done at the %s stage)." (Languages.to_string (fst trans)) 
71
72let basic_optimizations =
73        [
74                LoopPeeling.trans;
75                ConstPropagation.trans;
76                CopyPropagation.trans;
77                RedundancyElimination.trans;
78    CopyPropagation.trans;
79    RedundancyElimination.trans
80        ]
81 
82
83let options = OptionsParsing.register [
84  "-s", Arg.String set_source_language,
85  " Choose the source language between:";
86  extra_doc " Clight, Cminor";
87  extra_doc " [default is C]";
88
89  "-l", Arg.String set_target_language,
90  " Choose the target language between:";
91  extra_doc " Clight, Cminor, RTLabs, RTL, ERTL, LTL, LIN, ASM";
92  extra_doc " [default is ASM]";
93
94  "-a", Arg.Set annotation_flag,
95  " Add cost annotations on the source code.";
96
97  "-i", Arg.Set interpretation_flag,
98  " Interpret the compiled code.";
99
100  "-t", Arg.Set trace_flag,
101  " Interpret the compiled code and print all label traces.";
102
103  "-d", Arg.Set debug_flag,
104  " Debugging mode.";
105
106  "-o", Arg.String set_output_files,
107  " Prefix of the output files.";
108
109  "-peel", Arg.Unit (add_transformation LoopPeeling.trans),
110  " Apply loop peeling " ^
111    help_specify_opt_stage LoopPeeling.trans;
112
113  "-cst-prop", Arg.Unit (add_transformation ConstPropagation.trans),
114  " Apply constant propagation " ^
115    help_specify_opt_stage ConstPropagation.trans;
116
117  "-cpy-prop", Arg.Unit (add_transformation CopyPropagation.trans),
118  " Apply copy propagation " ^
119    help_specify_opt_stage CopyPropagation.trans;
120
121  "-pre", Arg.Unit (add_transformation RedundancyElimination.trans),
122  " Apply partial redundancy elimination " ^
123    help_specify_opt_stage RedundancyElimination.trans;
124
125  "-unroll-for",
126  Arg.Int (fun i -> add_transformation (LoopUnrolling.trans ~factor:i ()) ()),
127  " Apply loop unrolling, specifying factor " ^
128  help_specify_opt_stage (LoopUnrolling.trans ());
129
130  "-unroll", Arg.Unit (add_transformation (LoopUnrolling.trans ())),
131  " Apply loop unrolling " ^
132  help_specify_opt_stage (LoopUnrolling.trans ());
133
134  "-O", Arg.Unit (add_transformations basic_optimizations),
135  " Apply some optimizations.";
136
137  "-no-cost-tern",  Arg.Clear cost_ternary_flag,
138  " Replace cost ternary expressions with equivalent branch statements.";
139 
140(*
141  "-res", Arg.Set print_result_flag,
142  " Print the result of interpretations.";
143*)
144
145  "-dev", Arg.Set dev_test,
146  " Playground for developers.";
147]
Note: See TracBrowser for help on using the repository browser.