[486] | 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 | |
---|
[818] | 10 | 2. Add runtime functions. |
---|
[486] | 11 | |
---|
[818] | 12 | 3. Labelize. |
---|
| 13 | |
---|
| 14 | 4. Compile to the target language. |
---|
[486] | 15 | (And keep track of annotations if required). |
---|
| 16 | |
---|
[818] | 17 | 5. Annotate the input program with collected costs. |
---|
[486] | 18 | |
---|
[818] | 19 | 6. Save the annotated input program. |
---|
[486] | 20 | |
---|
| 21 | Optionnally, we can interpret the intermediate programs |
---|
| 22 | if {!Options.interpretation_requested}. |
---|
| 23 | *) |
---|
| 24 | let process filename = |
---|
[1462] | 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 |
---|
[619] | 35 | let (exact_output, output_filename) = match Options.get_output_files () with |
---|
| 36 | | None -> (false, filename) |
---|
| 37 | | Some filename' -> (true, filename') in |
---|
[740] | 38 | let save ?(suffix="") ast = |
---|
[1462] | 39 | Languages.save |
---|
| 40 | (Options.is_asm_pretty ()) exact_output output_filename suffix ast |
---|
[740] | 41 | in |
---|
[486] | 42 | let target_asts = |
---|
| 43 | (** If debugging is enabled, the compilation function returns all |
---|
| 44 | the intermediate programs. *) |
---|
[1546] | 45 | Languages.compile |
---|
| 46 | (Options.is_debug_enabled ()) |
---|
| 47 | (Options.get_transformations ()) |
---|
| 48 | src_language tgt_language input_ast |
---|
[486] | 49 | in |
---|
| 50 | let final_ast, intermediate_asts = Misc.ListExt.cut_last target_asts in |
---|
[740] | 51 | save final_ast; |
---|
| 52 | if Options.annotation_requested () then |
---|
| 53 | begin |
---|
[1462] | 54 | let (annotated_input_ast, cost_id, cost_incr, extern_cost_variables) = |
---|
[1542] | 55 | let cost_tern = Options.is_cost_ternary_enabled () in |
---|
| 56 | Languages.annotate cost_tern input_ast final_ast in ( |
---|
[740] | 57 | save ~suffix:"-annotated" annotated_input_ast; |
---|
[1462] | 58 | Languages.save_cost exact_output output_filename cost_id cost_incr |
---|
| 59 | extern_cost_variables); |
---|
[740] | 60 | end; |
---|
[1542] | 61 | |
---|
| 62 | if Options.is_debug_enabled () then |
---|
[740] | 63 | List.iter save intermediate_asts; |
---|
[486] | 64 | |
---|
[1462] | 65 | if Options.interpretations_requested () then |
---|
[740] | 66 | begin |
---|
[818] | 67 | let asts = target_asts in |
---|
| 68 | let debug = Options.is_debug_enabled () in |
---|
| 69 | let label_traces = List.map (Languages.interpret debug) asts in |
---|
[740] | 70 | Printf.eprintf "Checking execution traces...%!"; |
---|
| 71 | Checker.same_traces (List.combine asts label_traces); |
---|
| 72 | Printf.eprintf "OK.\n%!"; |
---|
[1462] | 73 | end; |
---|
[740] | 74 | |
---|
[1462] | 75 | if Options.interpretation_requested () then |
---|
| 76 | ignore (Languages.interpret (Options.is_debug_enabled ()) final_ast) |
---|
| 77 | |
---|
| 78 | let lustre_test filename = |
---|
| 79 | let lustre_test = match Options.get_lustre_test () with |
---|
| 80 | | None -> assert false (* do not use on this argument *) |
---|
| 81 | | Some lustre_test -> lustre_test in |
---|
| 82 | let lustre_test_cases = Options.get_lustre_test_cases () in |
---|
| 83 | let lustre_test_cycles = Options.get_lustre_test_cycles () in |
---|
| 84 | let lustre_test_min_int = Options.get_lustre_test_min_int () in |
---|
| 85 | let lustre_test_max_int = Options.get_lustre_test_max_int () in |
---|
| 86 | let src_language = Languages.Clight in |
---|
| 87 | let tgt_language = Languages.Clight in |
---|
| 88 | let input_ast = Languages.parse src_language filename in |
---|
| 89 | let input_ast = |
---|
| 90 | Languages.add_lustre_main lustre_test lustre_test_cases lustre_test_cycles |
---|
| 91 | lustre_test_min_int lustre_test_max_int input_ast in |
---|
| 92 | let (exact_output, output_filename) = match Options.get_output_files () with |
---|
| 93 | | None -> (false, filename) |
---|
| 94 | | Some filename' -> (true, filename') in |
---|
| 95 | let save ast = |
---|
| 96 | Languages.save |
---|
| 97 | (Options.is_asm_pretty ()) exact_output output_filename "" ast in |
---|
[1542] | 98 | let target_asts = |
---|
| 99 | Languages.compile false (Options.get_transformations ()) |
---|
| 100 | src_language tgt_language input_ast |
---|
[1462] | 101 | in |
---|
| 102 | let final_ast, _ = Misc.ListExt.cut_last target_asts in |
---|
| 103 | save input_ast ; |
---|
| 104 | save final_ast |
---|
| 105 | |
---|
[486] | 106 | let _ = |
---|
| 107 | if Options.is_dev_test_enabled () then Dev_test.do_dev_test input_files |
---|
[1462] | 108 | else |
---|
| 109 | if Options.get_lustre_test () <> None then List.iter lustre_test input_files |
---|
| 110 | else List.iter process input_files |
---|