Changeset 2993 for driver


Ignore:
Timestamp:
Mar 28, 2013, 9:56:26 AM (8 years ago)
Author:
sacerdot
Message:
  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
Location:
driver
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • driver/cerco.ml

    r2964 r2993  
    3434
    3535let argv1 = Sys.argv.(1) in
    36 let do_print,filename,style =
     36let do_exec,filename,style =
    3737 if argv1 = "-exec" then
    3838  true,Sys.argv.(2),(try Sys.argv.(3) with _ -> "instrumented")
     
    4141let cl = ClightParser.process filename in
    4242let observe =
    43  if do_print then
    44   let rec infinity = Extracted.Nat.S infinity in
    45   (fun pass prog ->
    46     print_string (Printer.print_program pass prog);
     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
    4749    Extracted.Semantics.run_and_print pass prog infinity
    48      (fun p -> print_string ("\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)
     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)
    5360in
    5461let output =
  • driver/printer.ml

    r2982 r2993  
    221221    l)
    222222
    223 let print_program pass (program : Extracted.Preamble.__) =
     223let extension_of_pass =
     224 function
     225 | Extracted.Compiler.Clight_pass                -> "clight"
     226 | Extracted.Compiler.Clight_switch_removed_pass -> "clight_sr"
     227 | Extracted.Compiler.Clight_label_pass          -> "clight_l"
     228 | Extracted.Compiler.Clight_simplified_pass     -> "clight_s"
     229 | Extracted.Compiler.Cminor_pass                -> "cminor"
     230 | Extracted.Compiler.Rtlabs_pass                -> "rtlabs"
     231 | Extracted.Compiler.Rtl_separate_pass          -> "rtl"
     232 | Extracted.Compiler.Rtl_uniq_pass              -> "rtl_u"
     233 | Extracted.Compiler.Ertl_pass                  -> "ertl"
     234 | Extracted.Compiler.Ertlptr_pass               -> "ertlptr"
     235 | Extracted.Compiler.Ltl_pass                   -> "ltl"
     236 | Extracted.Compiler.Lin_pass                   -> "lin"
     237 | Extracted.Compiler.Assembly_pass              -> "assembly"
     238 | Extracted.Compiler.Object_code_pass           -> "hex"
     239;;
     240
     241
     242let print_program sourcename pass (program : Extracted.Preamble.__) =
    224243 let beprint pcs =
    225244  print_graph (pcs (Extracted.Types.fst (Obj.magic program))) in
     
    250269   | _ -> ""
    251270 in
    252   "\n" ^ lines ^ "\n"
     271  let filename =
     272   Filename.chop_extension sourcename ^ "." ^ extension_of_pass pass in
     273  let och = open_out filename in
     274  output_string och lines;
     275  close_out och
  • driver/printer.mli

    r2901 r2993  
    1 val print_program: Extracted.Compiler.pass -> Extracted.Preamble.__ -> string
     1val print_program:
     2 string -> Extracted.Compiler.pass -> Extracted.Preamble.__ -> unit
Note: See TracChangeset for help on using the changeset viewer.