Changeset 2759


Ignore:
Timestamp:
Mar 1, 2013, 7:56:34 PM (7 years ago)
Author:
campbell
Message:

Print out costs, with choice of style.
Note small anti-assertion patch to extracted ASMCosts.
No stack space yet.

Files:
4 edited

Legend:

Unmodified
Added
Removed
  • driver/clightPrinter.ml

    r2758 r2759  
    4646| Fnil -> []
    4747| Fcons (id, ty, tl) -> (nameof id,ty)::(flist tl)
     48
     49type cost_style =
     50| Cost_plain
     51| Cost_numbered of Extracted.Label.clight_cost_map
     52| Cost_instrumented of Extracted.Label.clight_cost_map
     53
     54(* Not ideal, but convenient for now *)
     55let style = ref Cost_plain
    4856
    4957let namecost l =
     
    229237      fprintf p "%a.%s" print_expr_prec (level, e1) (nameof id)
    230238  | Ecost (lbl,e1) ->
    231       fprintf p "(/* %s */ %a)" (namecost lbl) print_expr e1
     239      match !style with
     240      | Cost_plain ->
     241        fprintf p "(/* %s */ %a)" (namecost lbl) print_expr e1
     242      | Cost_numbered cm ->
     243        fprintf p "(/* %s = %d */ %a)" (namecost lbl) (int_of_matitanat (cm lbl)) print_expr e1
     244      | Cost_instrumented cm ->
     245        fprintf p "(__cost_incr(%d), %a)" (int_of_matitanat (cm lbl)) print_expr e1
    232246  (*| Ecall (f, arg, e) ->
    233247      fprintf p "(%s(%a), %a)" f print_expr arg print_expr e*)
     
    304318      fprintf p "goto %s;" (nameof lbl)
    305319 | Scost (lbl,s1) ->
    306      fprintf p "%s:@ %a" (namecost lbl) print_stmt s1
     320      match !style with
     321      | Cost_plain ->
     322        fprintf p "%s:@ %a" (namecost lbl) print_stmt s1
     323      | Cost_numbered cm ->
     324        fprintf p "/* %s = %d */@ %a" (namecost lbl) (int_of_matitanat (cm lbl)) print_stmt s1
     325      | Cost_instrumented cm ->
     326        fprintf p "__cost_incr(%d);@ %a" (int_of_matitanat (cm lbl)) print_stmt s1
    307327
    308328and print_cases p cases =
     
    597617  fprintf p "@]@."
    598618
    599 let print_program prog =
     619let print_program cs prog =
     620  style := cs;
     621  (match cs with
     622  | Cost_instrumented _ ->
     623      fprintf str_formatter "int __cost = 0;@\n@\n";
     624      fprintf str_formatter "void __cost_incr(int incr) {@\n";
     625      fprintf str_formatter "  __cost = __cost + incr;@\n}@\n@\n"
     626  | _ -> ());
    600627  print_program_2 str_formatter prog;
    601628  flush_str_formatter ()
     
    603630let string_of_ctype = name_type
    604631
    605 let print_expression e =
     632let print_expression cs e =
     633  style := cs;
    606634  print_expr str_formatter e;
    607635  flush_str_formatter ()
    608636
    609 let print_statement s =
     637let print_statement cs s =
     638  style := cs;
    610639  print_stmt str_formatter s;
    611640  flush_str_formatter ()
  • driver/clightPrinter.mli

    r2758 r2759  
    22    programs. *)
    33
    4 val print_program: Extracted.Csyntax.clight_program -> string
     4type cost_style =
     5| Cost_plain
     6| Cost_numbered of Extracted.Label.clight_cost_map
     7| Cost_instrumented of Extracted.Label.clight_cost_map
    58
    6 val print_expression: Extracted.Csyntax.expr -> string
     9val print_program: cost_style -> Extracted.Csyntax.clight_program -> string
     10
     11val print_expression: cost_style -> Extracted.Csyntax.expr -> string
    712
    813val string_of_ctype: Extracted.Csyntax.type0 -> string
    914
    10 val print_statement: Extracted.Csyntax.statement -> string
     15val print_statement: cost_style -> Extracted.Csyntax.statement -> string
    1116
    1217val print_ctype_prot: Extracted.Csyntax.type0 -> string
  • driver/compiler.ml

    r2758 r2759  
    11open Extracted.Errors
     2open ClightPrinter
    23
    34let rec run g s =
     
    2526let OK {Extracted.Types.fst = oc; snd = acl} = Extracted.Compiler.compile cl in
    2627let {Extracted.Types.dpi1 = labelled; Extracted.Types.dpi2 = l_costmap} = acl in
    27 print_endline (ClightPrinter.print_program labelled)
     28let style =
     29  match try Sys.argv.(2) with _ -> "instrumented" with
     30  | "plain" -> Cost_plain
     31  | "numbered" -> Cost_numbered l_costmap
     32  | "instrumented" -> Cost_instrumented l_costmap
     33  | x -> failwith ("I have no idea what " ^ x ^ " means")
     34in
     35print_endline (ClightPrinter.print_program style labelled)
    2836(*
    2937let OK mid = Extracted.Compiler.front_end cl in
  • extracted/aSMCosts.ml

    r2743 r2759  
    108108      (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    109109      Nat.O)))))))))))))))) (Obj.magic pc) cost_labels);
    110     StructuredTraces.as_call_ident = (assert false (* absurd case *));
    111     StructuredTraces.as_tailcall_ident = (assert false (* absurd case *)) }
     110    StructuredTraces.as_call_ident = (fun _ -> assert false (* absurd case *));
     111    StructuredTraces.as_tailcall_ident = (fun _ -> assert false (* absurd case *)) }
    112112
    113113(** val trace_any_label_length :
Note: See TracChangeset for help on using the changeset viewer.