4 let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
6 let string_of_intensional_event =
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 ^ ") "
19 | Extracted.Compiler.Clight_pass -> "Clight_pass "
20 | Extracted.Compiler.Clight_switch_removed_pass -> "Clight_switch_removed_pass"
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 "
34 List.iter (fun filename ->
35 let do_exec = Options.interpretations_requested () in
36 let cl = ClightParser.process filename in
38 let rec infinity = Extracted.Nat.S infinity in
40 if do_exec || pass = Extracted.Compiler.Object_code_pass then
41 Printer.print_program filename pass prog;
43 Extracted.Semantics.run_and_print pass prog infinity
44 (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); flush stdout;
46 (fun evn -> print_string (string_of_intensional_event evn); flush stdout;
48 (fun msg -> print_endline (Error.errormsg msg); flush stdout;
50 (fun n-> print_endline (string_of_int(Extracted.Glue.int_of_bitvector n));
51 flush stdout; Extracted.Types.It)
56 match Extracted.Compiler.compile observe cl with
58 | Error m -> failwith (Error.errormsg m) in
59 if Options.annotation_requested () then
61 let labelled = output.Extracted.Compiler.c_labelled_clight in
62 let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
63 let init_costlabel = output.Extracted.Compiler.c_init_costlabel in
64 let s_costmap = output.Extracted.Compiler.c_stack_cost in
65 let maxstack = output.Extracted.Compiler.c_max_stack in
66 let style = Cost_instrumented (l_costmap,init_costlabel,s_costmap,maxstack) in
67 let instrumented = ClightPrinter.print_program style labelled in
69 (match Options.get_output_files () with
70 None -> Filename.chop_extension filename
72 let och = open_out (basename ^ "-instrumented.c") in
73 output_string och instrumented;
75 let och = open_out (basename ^ ".cerco") in
76 output_string och "__cost\n";
77 output_string och "__cost_incr\n";
79 let och = open_out (basename ^ ".stack_cerco") in
80 output_string och "__stack_size\n";
81 output_string och "__stack_size_max\n";
82 output_string och "__stack_size_incr\n";
85 ) (OptionsParsing.results ())