1 | open Options |
---|
2 | |
---|
3 | (** Parse the command line. *) |
---|
4 | let 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 | *) |
---|
24 | let 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 | |
---|
75 | let 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 | |
---|
101 | let _ = |
---|
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 |
---|