source: driver/cerco.ml @ 2900

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

Flushing to understand where it is slow.

File size: 3.0 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
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.Ertlptr_pass               -> "Ertlptr_pass"
29 | Extracted.Compiler.Ltl_pass                   -> "Ltl_pass"
30 | Extracted.Compiler.Lin_pass                   -> "Lin_pass"
[2875]31 | Extracted.Compiler.Assembly_pass              -> "Assembly_pass"
32 | Extracted.Compiler.Object_code_pass           -> "Object_code_pass"
[2747]33;;
34
[2834]35let argv1 = Sys.argv.(1) in
[2874]36let do_print,filename,style =
[2834]37 if argv1 = "-exec" then
[2874]38  true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented")
[2834]39 else
[2874]40  false,argv1,(try Sys.argv.(2) with _ -> "instrumented") in
[2834]41let cl = ClightParser.process filename in
42let observe =
43 if do_print then
44  let rec infinity = Extracted.Nat.S infinity in
45  (fun pass prog ->
[2864]46    print_string (BackendPrinter.print_program pass prog);
[2834]47    Extracted.Semantics.run_and_print pass prog infinity
48     (fun p -> print_endline ("\n" ^ string_of_pass p ^ ":"); Extracted.Types.It)
49     (fun evn -> print_string (string_of_intensional_event evn); Extracted.Types.It)
50     (fun msg -> print_endline (Error.errormsg msg); Extracted.Types.It)
51     (fun n-> print_endline (string_of_int (Extracted.Glue.int_of_bitvector n)); Extracted.Types.It))
52 else (fun _ _ -> Extracted.Types.It) 
53in
[2788]54let output = 
[2834]55  match Extracted.Compiler.compile observe cl with
[2788]56  | OK o -> o
57  | Error m -> failwith (Error.errormsg m)
58in
[2776]59let labelled = output.Extracted.Compiler.c_labelled_clight in
60let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
[2787]61let s_costmap = output.Extracted.Compiler.c_stack_cost in
[2759]62let style =
[2874]63  match style with
[2759]64  | "plain" -> Cost_plain
[2787]65  | "numbered" -> Cost_numbered (l_costmap,s_costmap)
66  | "instrumented" -> Cost_instrumented (l_costmap,s_costmap)
[2759]67  | x -> failwith ("I have no idea what " ^ x ^ " means")
68in
[2778]69print_endline (ClightPrinter.print_program style labelled);
[2900]70print_newline (); flush stdout;
[2778]71print_endline (ASMPrinter.print_program (Extracted.ASM.oc (Extracted.Compiler.c_labelled_object_code output)));
Note: See TracBrowser for help on using the repository browser.