source: driver/cerco.ml @ 2998

Last change on this file since 2998 was 2993, checked in by sacerdot, 8 years ago
  1. performance improved: the type inference was inferring load_code_memory ... in computational positions, duplicating the work at every step of execution of the assembly code. We now force the use of the let-in-ed variable
  2. new extraction after 1)
  3. driver/printer.ml repaired
  4. the output of the intermediate passes is now printed on file
File size: 3.4 KB
Line 
1open Extracted.Errors
2open ClightPrinter
3
4let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
5
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;;
16
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                  "
31 | Extracted.Compiler.Assembly_pass              -> "Assembly_pass             "
32 | Extracted.Compiler.Object_code_pass           -> "Object_code_pass          "
33;;
34
35let argv1 = Sys.argv.(1) in
36let do_exec,filename,style =
37 if argv1 = "-exec" then
38  true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented")
39 else
40  false,argv1,(try Sys.argv.(2) with _ -> "instrumented") in
41let cl = ClightParser.process filename in
42let observe =
43 let rec infinity = Extracted.Nat.S infinity in
44 (fun pass prog ->
45   if do_exec || pass = Extracted.Compiler.Clight_label_pass ||
46      pass = Extracted.Compiler.Object_code_pass then
47    Printer.print_program filename pass prog;
48   if do_exec then
49    Extracted.Semantics.run_and_print pass prog infinity
50     (fun p -> print_string ("\n" ^ string_of_pass p ^ ": "); flush stdout;
51       Extracted.Types.It)
52     (fun evn -> print_string (string_of_intensional_event evn); flush stdout;
53       Extracted.Types.It)
54     (fun msg -> print_endline (Error.errormsg msg); flush stdout;
55       Extracted.Types.It)
56     (fun n-> print_endline (string_of_int(Extracted.Glue.int_of_bitvector n));
57       flush stdout; Extracted.Types.It)
58   else
59    Extracted.Types.It)
60in
61let output = 
62  match Extracted.Compiler.compile observe cl with
63  | OK o -> o
64  | Error m -> failwith (Error.errormsg m)
65in
66let labelled = output.Extracted.Compiler.c_labelled_clight in
67let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
68let s_costmap = output.Extracted.Compiler.c_stack_cost in
69let style =
70  match style with
71  | "plain" -> Cost_plain
72  | "numbered" -> Cost_numbered (l_costmap,s_costmap)
73  | "instrumented" -> Cost_instrumented (l_costmap,s_costmap)
74  | x -> failwith ("I have no idea what " ^ x ^ " means")
75in
76print_endline (ClightPrinter.print_program style labelled);
77print_newline (); flush stdout;
78print_endline (ASMPrinter.print_program (Extracted.ASM.oc (Extracted.Compiler.c_labelled_object_code output)));
Note: See TracBrowser for help on using the repository browser.