source: Deliverables/D2.2/8051/src/acc.ml @ 1462

Last change on this file since 1462 was 1462, checked in by ayache, 8 years ago

Added D5.1: Frama-C plug-in and Lustre wrapper. D2.2 (8051) has been updated accordingly.

File size: 3.9 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.printf "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 is_lustre_file = Options.is_lustre_file () in
29  let remove_lustre_externals = Options.is_remove_lustre_externals () in
30  let input_ast =
31    Languages.parse ~is_lustre_file ~remove_lustre_externals
32      src_language filename in
33  let input_ast = Languages.add_runtime input_ast in 
34  let input_ast = Languages.labelize input_ast in
35  let (exact_output, output_filename) = match Options.get_output_files () with
36    | None -> (false, filename)
37    | Some filename' -> (true, filename') in
38  let save ?(suffix="") ast = 
39    Languages.save
40      (Options.is_asm_pretty ()) exact_output output_filename suffix ast
41  in
42  let target_asts =
43    (** If debugging is enabled, the compilation function returns all
44        the intermediate programs. *)
45    Languages.compile (Options.is_debug_enabled ()) 
46      src_language tgt_language input_ast
47  in
48  let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in
49  save final_ast;
50  if Options.annotation_requested () then
51    begin
52      let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) =
53        Languages.annotate input_ast final_ast in (
54          save ~suffix:"-annotated" annotated_input_ast;
55          Languages.save_cost exact_output output_filename cost_id cost_incr
56            extern_cost_variables);
57    end;
58                                             
59  if Options.is_debug_enabled () then 
60    List.iter save intermediate_asts;
61
62  if Options.interpretations_requested () then
63    begin
64      let asts = target_asts in
65      let debug = Options.is_debug_enabled () in
66      let label_traces = List.map (Languages.interpret debug) asts in
67      Printf.eprintf "Checking execution traces...%!";
68      Checker.same_traces (List.combine asts label_traces);
69      Printf.eprintf "OK.\n%!";
70    end;
71
72  if Options.interpretation_requested () then
73    ignore (Languages.interpret (Options.is_debug_enabled ()) final_ast)
74
75let lustre_test filename =
76  let lustre_test       = match Options.get_lustre_test () with
77    | None -> assert false (* do not use on this argument *)
78    | Some lustre_test -> lustre_test in
79  let lustre_test_cases = Options.get_lustre_test_cases () in
80  let lustre_test_cycles = Options.get_lustre_test_cycles () in
81  let lustre_test_min_int = Options.get_lustre_test_min_int () in
82  let lustre_test_max_int = Options.get_lustre_test_max_int () in
83  let src_language      = Languages.Clight in
84  let tgt_language      = Languages.Clight in
85  let input_ast         = Languages.parse src_language filename in
86  let input_ast         =
87    Languages.add_lustre_main lustre_test lustre_test_cases lustre_test_cycles
88      lustre_test_min_int lustre_test_max_int input_ast in 
89  let (exact_output, output_filename) = match Options.get_output_files () with
90    | None -> (false, filename)
91    | Some filename' -> (true, filename') in
92  let save ast =
93    Languages.save
94      (Options.is_asm_pretty ()) exact_output output_filename "" ast in
95  let target_asts = Languages.compile false src_language tgt_language input_ast
96  in
97  let final_ast, _ = Misc.ListExt.cut_last target_asts in
98  save input_ast ;
99  save final_ast
100
101let _ =
102  if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files
103  else
104    if Options.get_lustre_test () <> None then List.iter lustre_test input_files
105    else List.iter process input_files
Note: See TracBrowser for help on using the repository browser.