acc.ml

   1 open Extracted.Errors
   2 open ClightPrinter
   3
   4 let string_of_pos n = string_of_int (Extracted.Glue.int_of_matitapos n)
   5
   6 let 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
  17 let 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.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          "
  32 ;;
  33
  34 List.iter (fun filename ->
  35 let do_exec = Options.interpretations_requested () in
  36 let cl = ClightParser.process filename in
  37 let observe =
  38  let rec infinity = Extracted.Nat.S infinity in
  39  (fun pass prog ->
  40    if do_exec || pass = Extracted.Compiler.Object_code_pass then
  41     Printer.print_program filename pass prog;
  42    if do_exec then
  43     Extracted.Semantics.run_and_print pass prog infinity
  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)
  54 in
  55 let output =
  56   match Extracted.Compiler.compile observe cl with
  57   | OK o -> o
  58   | Error m -> failwith (Error.errormsg m) in
  59 if 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 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
  68   let basename =
  69    (match Options.get_output_files () with
  70       None -> Filename.chop_extension filename
  71     | Some s -> s) in
  72   let och = open_out (basename ^ "-instrumented.c") in
  73   output_string och instrumented;
  74   close_out och;
  75   let och = open_out (basename ^ ".cerco") in
  76   output_string och "__cost\n";
  77   output_string och "__cost_incr\n";
  78   close_out och;
  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";
  83   close_out och
  84  end
  85 ) (OptionsParsing.results ())