Changeset 2787


Ignore:
Timestamp:
Mar 6, 2013, 3:48:14 PM (7 years ago)
Author:
campbell
Message:

Output stack costs in driver.

Location:
driver
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • driver/clightPrinter.ml

    r2773 r2787  
    4141| Extracted.List.Cons (h,t) -> h::(mlist t)
    4242
     43let stack_cost_for scm id =
     44  let check ids =
     45    let id' = Extracted.Types.fst ids in
     46    match Extracted.Identifiers.eq_identifier Extracted.PreIdentifiers.SymbolTag id id' with
     47    | Extracted.Bool.True -> Extracted.Types.Some (Extracted.Types.snd ids)
     48    | _ -> Extracted.Types.None
     49  in
     50  match Extracted.List.find check scm with
     51  | Extracted.Types.None -> 0
     52  | Extracted.Types.Some n -> int_of_matitanat n
     53
    4354
    4455let rec flist l =
     
    4960type cost_style =
    5061| Cost_plain
    51 | Cost_numbered of Extracted.Label.clight_cost_map
    52 | Cost_instrumented of Extracted.Label.clight_cost_map
     62| Cost_numbered of Extracted.Label.clight_cost_map * Extracted.Joint.stack_cost_model
     63| Cost_instrumented of Extracted.Label.clight_cost_map * Extracted.Joint.stack_cost_model
    5364
    5465(* Not ideal, but convenient for now *)
     
    240251      | Cost_plain ->
    241252        fprintf p "(/* %s */ %a)" (namecost lbl) print_expr e1
    242       | Cost_numbered cm ->
     253      | Cost_numbered (cm,_) ->
    243254        fprintf p "(/* %s = %d */ %a)" (namecost lbl) (int_of_matitanat (cm lbl)) print_expr e1
    244       | Cost_instrumented cm ->
     255      | Cost_instrumented (cm,_) ->
    245256        fprintf p "(__cost_incr(%d), %a)" (int_of_matitanat (cm lbl)) print_expr e1
    246257  (*| Ecall (f, arg, e) ->
     
    260271      print_expr p e1;
    261272      print_expr_list p (false, et)
     273
     274(* Another quick hack :( *)
     275let return_cost = ref None
     276let print_return_cost p =
     277  match !return_cost with
     278  | None -> ()
     279  | Some s -> fprintf p "__stack_size_incr(-%d);@ " s
    262280
    263281let rec print_stmt p s =
     
    310328              print_cases cases
    311329  | Sreturn Extracted.Types.None ->
     330      print_return_cost p;
    312331      fprintf p "return;"
    313332  | Sreturn (Extracted.Types.Some e) ->
     333      print_return_cost p;
    314334      fprintf p "return %a;" print_expr e
    315335  | Slabel(lbl, s1) ->
     
    321341      | Cost_plain ->
    322342        fprintf p "%s:@ %a" (namecost lbl) print_stmt s1
    323       | Cost_numbered cm ->
     343      | Cost_numbered (cm,_) ->
    324344        fprintf p "/* %s = %d */@ %a" (namecost lbl) (int_of_matitanat (cm lbl)) print_stmt s1
    325       | Cost_instrumented cm ->
     345      | Cost_instrumented (cm,_) ->
    326346        fprintf p "__cost_incr(%d);@ %a" (int_of_matitanat (cm lbl)) print_stmt s1
    327347
     
    383403let print_function p id f =
    384404  fprintf p "%s@ "
    385             (name_cdecl (name_function_parameters id f.fn_params)
     405            (name_cdecl (name_function_parameters (nameof id) f.fn_params)
    386406                        f.fn_return);
    387407  fprintf p "@[<v 2>{@ ";
     
    390410      fprintf p "%s;@ " (name_cdecl (nameof id) ty))
    391411    f.fn_vars;
     412  (match !style with
     413  | Cost_plain -> return_cost := None
     414  | Cost_numbered (_,scm) ->
     415    let cost = stack_cost_for scm id in
     416    fprintf p "/* stack cost %d */@ " cost;
     417    return_cost := None (* No need to tell us the stack size again *)
     418  | Cost_instrumented (_,scm) ->
     419    let cost = stack_cost_for scm id in
     420    fprintf p "__stack_cost_incr(%d);@ " cost;
     421    return_cost := Some cost
     422  );
    392423  print_stmt p f.fn_body;
     424  (* We don't always need this (e.g., when it ends with a return), but
     425     better safe than sorry... *)
     426  print_return_cost p;
    393427  fprintf p "@;<0 -2>}@]@ @ "
    394428
    395429let print_fundef p {Extracted.Types.fst = id; Extracted.Types.snd = fd} =
    396   let id = nameof id in
    397430  match fd with
    398431  | CL_External(_, args, res) ->
    399432      fprintf p "extern %s;@ @ "
    400                 (name_cdecl id (Tfunction(args, res)))
     433                (name_cdecl (nameof id) (Tfunction(args, res)))
    401434  | CL_Internal f ->
    402435      print_function p id f
     
    623656      fprintf str_formatter "int __cost = 0;@\n@\n";
    624657      fprintf str_formatter "void __cost_incr(int incr) {@\n";
    625       fprintf str_formatter "  __cost = __cost + incr;@\n}@\n@\n"
     658      fprintf str_formatter "  __cost = __cost + incr;@\n}@\n@\n";
     659      fprintf str_formatter "int __stack_size = 0, __stack_size_max = 0;@\n@\n";
     660      fprintf str_formatter "void __stack_size_incr(int incr) {@\n";
     661      fprintf str_formatter "  __stack_size = __stack_size + incr;@\n";
     662      fprintf str_formatter "  __stack_size_max = __stack_size_max < __stack_size ? __stack_size : __stack_size_max@\n}@\n@\n"
    626663  | _ -> ());
    627664  print_program_2 str_formatter prog;
  • driver/clightPrinter.mli

    r2759 r2787  
    44type cost_style =
    55| Cost_plain
    6 | Cost_numbered of Extracted.Label.clight_cost_map
    7 | Cost_instrumented of Extracted.Label.clight_cost_map
     6| Cost_numbered of Extracted.Label.clight_cost_map * Extracted.Joint.stack_cost_model
     7| Cost_instrumented of Extracted.Label.clight_cost_map * Extracted.Joint.stack_cost_model
    88
    99val print_program: cost_style -> Extracted.Csyntax.clight_program -> string
  • driver/compiler.ml

    r2778 r2787  
    2727let labelled = output.Extracted.Compiler.c_labelled_clight in
    2828let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
     29let s_costmap = output.Extracted.Compiler.c_stack_cost in
    2930let style =
    3031  match try Sys.argv.(2) with _ -> "instrumented" with
    3132  | "plain" -> Cost_plain
    32   | "numbered" -> Cost_numbered l_costmap
    33   | "instrumented" -> Cost_instrumented l_costmap
     33  | "numbered" -> Cost_numbered (l_costmap,s_costmap)
     34  | "instrumented" -> Cost_instrumented (l_costmap,s_costmap)
    3435  | x -> failwith ("I have no idea what " ^ x ^ " means")
    3536in
Note: See TracChangeset for help on using the changeset viewer.