source: driver/acc.ml @ 3027

Last change on this file since 3027 was 3027, checked in by sacerdot, 8 years ago

Another output used by the plug-in.

File size: 3.4 KB
RevLine 
[2747]1open Extracted.Errors
[2759]2open ClightPrinter
[2747]3
[2834]4let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
[2747]5
[2834]6let string_of_intensional_event =
7 function
8    Extracted.StructuredTraces.IEVcost cl ->
9     "COST(k_" ^ string_of_pos cl ^") "
10  | Extracted.StructuredTraces.IEVcall id ->
11     "CALL(fun_" ^ string_of_pos id ^ ") "
12  | Extracted.StructuredTraces.IEVtailcall _ -> assert false
13  | Extracted.StructuredTraces.IEVret id ->
14     "RET(fun_" ^ string_of_pos id ^ ") "
15;;
[2747]16
[2834]17let string_of_pass =
18 function
[2934]19 | Extracted.Compiler.Clight_pass                -> "Clight_pass               "
[2834]20 | Extracted.Compiler.Clight_switch_removed_pass -> "Clight_switch_removed_pass"
[2934]21 | Extracted.Compiler.Clight_label_pass          -> "Clight_label_pass         "
22 | Extracted.Compiler.Clight_simplified_pass     -> "Clight_simplified_pass    "
23 | Extracted.Compiler.Cminor_pass                -> "Cminor_pass               "
24 | Extracted.Compiler.Rtlabs_pass                -> "Rtlabs_pass               "
25 | Extracted.Compiler.Rtl_separate_pass          -> "Rtl_separate_pass         "
26 | Extracted.Compiler.Rtl_uniq_pass              -> "Rtl_uniq_pass             "
27 | Extracted.Compiler.Ertl_pass                  -> "Ertl_pass                 "
28 | Extracted.Compiler.Ltl_pass                   -> "Ltl_pass                  "
29 | Extracted.Compiler.Lin_pass                   -> "Lin_pass                  "
30 | Extracted.Compiler.Assembly_pass              -> "Assembly_pass             "
31 | Extracted.Compiler.Object_code_pass           -> "Object_code_pass          "
[2747]32;;
33
[3005]34List.iter (fun filename ->
35let do_exec = Options.interpretations_requested () in
[2834]36let cl = ClightParser.process filename in
37let observe =
[2993]38 let rec infinity = Extracted.Nat.S infinity in
39 (fun pass prog ->
[2999]40   if do_exec || pass = Extracted.Compiler.Object_code_pass then
[2993]41    Printer.print_program filename pass prog;
42   if do_exec then
[2834]43    Extracted.Semantics.run_and_print pass prog infinity
[2993]44     (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); flush stdout;
45       Extracted.Types.It)
46     (fun evn -> print_string (string_of_intensional_event evn); flush stdout;
47       Extracted.Types.It)
48     (fun msg -> print_endline (Error.errormsg msg); flush stdout;
49       Extracted.Types.It)
50     (fun n-> print_endline (string_of_int(Extracted.Glue.int_of_bitvector n));
51       flush stdout; Extracted.Types.It)
52   else
53    Extracted.Types.It)
[2834]54in
[2788]55let output = 
[2834]56  match Extracted.Compiler.compile observe cl with
[2788]57  | OK o -> o
[3020]58  | Error m -> failwith (Error.errormsg m) in
59if Options.annotation_requested () then
60 begin
61  let labelled = output.Extracted.Compiler.c_labelled_clight in
62  let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
63  let s_costmap = output.Extracted.Compiler.c_stack_cost in
64  let style = Cost_instrumented (l_costmap,s_costmap) in
65  let instrumented = ClightPrinter.print_program style labelled in
[3026]66  let basename =
[3025]67   (match Options.get_output_files () with
68      None -> Filename.chop_extension filename
[3026]69    | Some s -> s) in
70  let och = open_out (basename ^ "-instrumented.c") in
[3020]71  output_string och instrumented;
[3026]72  close_out och;
73  let och = open_out (basename ^ ".cerco") in
74  output_string och "__cost\n";
75  output_string och "__cost_incr\n";
[3027]76  close_out och;
77  let och = open_out (basename ^ ".stack_cerco") in
78  output_string och "__stack_size\n";
79  output_string och "__stack_size_max\n";
80  output_string och "__stack_size_incr\n";
[3020]81  close_out och
82 end
[3005]83) (OptionsParsing.results ())
Note: See TracBrowser for help on using the repository browser.