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

Last change on this file since 1507 was 1507, checked in by tranquil, 8 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: 2.8 KB
Line 
1open Options
2
3(** Parse the command line. *)
4let input_files = OptionsParsing.results ()
5
6(** For each input file of the source language:
7
8    1. Parse.
9
10    2. Add runtime functions.
11
12    3. Labelize.
13
14    4. Compile to the target language.
15       (And keep track of annotations if required).
16 
17    5. Annotate the input program with collected costs.
18
19    6. Save the annotated input program.
20
21    Optionnally, we can interpret the intermediate programs
22    if {!Options.interpretation_requested}.
23*)
24let process filename = 
25  let _ = Printf.eprintf "Processing %s.\n%!" filename in
26  let src_language    = Options.get_source_language () in
27  let tgt_language    = Options.get_target_language () in
28  let input_ast       = Languages.parse src_language filename in 
29  let input_ast       = Languages.add_runtime input_ast in 
30  let input_ast       = Languages.labelize input_ast in
31  let (exact_output, output_filename) = match Options.get_output_files () with
32    | None -> (false, filename)
33    | Some filename' -> (true, filename') in
34  let save ?(suffix="") ast = 
35    Languages.save exact_output output_filename suffix ast
36  in
37  let target_asts =
38    (** If debugging is enabled, the compilation function returns all
39        the intermediate programs. *)
40    Languages.compile (Options.is_debug_enabled ()) 
41      (Options.get_transformations ()) src_language tgt_language input_ast
42  in
43  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
44  save final_ast;
45  if Options.annotation_requested () then
46    begin
47      let (annotated_input_ast, cost_id, cost_incr) =
48        let cost_tern = Options.is_cost_ternary_enabled () in
49        Languages.annotate cost_tern input_ast final_ast in (
50          save ~suffix:"-annotated" annotated_input_ast;
51          Languages.save_cost output_filename cost_id cost_incr);
52    end;
53                                             
54  if Options.is_debug_enabled () then 
55    List.iter save intermediate_asts;
56
57  if Options.interpretation_requested () || Options.is_debug_enabled () ||
58               Options.trace_requested () then
59    begin
60      let asts = target_asts in
61      let debug = Options.is_debug_enabled () in
62      let label_traces = List.map (Languages.interpret debug) asts in
63      Printf.eprintf "Checking execution traces...%!";
64      if Options.trace_requested () then
65        let print_l l =
66          Printf.printf "%s, " (CostLabel.string_of_cost_label
67                                  ~pretty:true l) in
68        let print_ls ls = List.iter print_l ls in
69        let print_trace (v, ls) =
70          Printf.printf "%s | " (Big_int.string_of_big_int v);
71          print_ls ls;
72          Printf.printf "\n" in
73        List.iter print_trace label_traces
74      else ();
75      Checker.same_traces (List.combine asts label_traces);
76      Printf.eprintf "OK.\n%!";
77    end
78
79let _ =
80  if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files
81  else List.iter process input_files
Note: See TracBrowser for help on using the repository browser.