Ignore:
Timestamp:
Apr 4, 2013, 9:58:03 AM (7 years ago)
Author:
sacerdot
Message:

The cost and stack* variables are now initialized with the cost of
the pre-main and the size of globals.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/clightPrinter.ml

    r3038 r3083  
    6060type cost_style =
    6161| Cost_plain
    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
     62| Cost_numbered of Extracted.Label.clight_cost_map * Extracted.CostLabel.costlabel * Extracted.Joint.stack_cost_model * Extracted.Nat.nat
     63| Cost_instrumented of Extracted.Label.clight_cost_map * Extracted.CostLabel.costlabel * Extracted.Joint.stack_cost_model * Extracted.Nat.nat
    6464
    6565(* Not ideal, but convenient for now *)
     
    251251      | Cost_plain ->
    252252        fprintf p "(/* %s */ %a)" (namecost lbl) print_expr e1
    253       | Cost_numbered (cm,_) ->
     253      | Cost_numbered (cm,_,_,_) ->
    254254        fprintf p "(/* %s = %d */ %a)" (namecost lbl) (int_of_matitanat (cm lbl)) print_expr e1
    255       | Cost_instrumented (cm,_) ->
     255      | Cost_instrumented (cm,_,_,_) ->
    256256        fprintf p "(__cost_incr(%d), %a)" (int_of_matitanat (cm lbl)) print_expr e1
    257257  (*| Ecall (f, arg, e) ->
     
    341341      | Cost_plain ->
    342342        fprintf p "%s:@ %a" (namecost lbl) print_stmt s1
    343       | Cost_numbered (cm,_) ->
     343      | Cost_numbered (cm,_,_,_) ->
    344344        fprintf p "/* %s = %d */@ %a" (namecost lbl) (int_of_matitanat (cm lbl)) print_stmt s1
    345       | Cost_instrumented (cm,_) ->
     345      | Cost_instrumented (cm,_,_,_) ->
    346346        fprintf p "__cost_incr(%d);@ %a" (int_of_matitanat (cm lbl)) print_stmt s1
    347347
     
    412412  (match !style with
    413413  | Cost_plain -> return_cost := None
    414   | Cost_numbered (_,scm) ->
     414  | Cost_numbered (_,_,scm,_) ->
    415415    let cost = stack_cost_for scm id in
    416416    fprintf p "/* stack cost %d */@ " cost;
    417417    return_cost := None (* No need to tell us the stack size again *)
    418   | Cost_instrumented (_,scm) ->
     418  | Cost_instrumented (_,_,scm,_) ->
    419419    let cost = stack_cost_for scm id in
    420420    fprintf p "__stack_size_incr(%d);@ " cost;
     
    653653  style := cs;
    654654  (match cs with
    655   | Cost_instrumented _ ->
    656       fprintf str_formatter "int __cost = 0;@\n@\n";
    657       fprintf str_formatter "int __stack_size = 0, __stack_size_max = 0;@\n@\n";
     655  | Cost_instrumented (cm,initc,_,sinit) ->
     656     let cinit = int_of_matitanat (cm initc) in
     657     let sinit = int_of_float (2.0 ** 16.) - int_of_matitanat sinit in
     658      fprintf str_formatter "int __cost = %d;@\n@\n" cinit;
     659      fprintf str_formatter "int __stack_size = %d, __stack_size_max = %d;@\n@\n" sinit sinit;
    658660      fprintf str_formatter "void __cost_incr(int incr) {@\n";
    659661      fprintf str_formatter "  __cost = __cost + incr;@\n}@\n@\n";
Note: See TracChangeset for help on using the changeset viewer.