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.

File:
1 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 ()
Note: See TracChangeset for help on using the changeset viewer.