Changeset 3083


Ignore:
Timestamp:
Apr 4, 2013, 9:58:03 AM (4 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.

Files:
5 edited

Legend:

Unmodified
Added
Removed
  • driver/acc.ml

    r3027 r3083  
    6161  let labelled = output.Extracted.Compiler.c_labelled_clight in
    6262  let l_costmap = output.Extracted.Compiler.c_clight_cost_map in
     63  let init_costlabel = output.Extracted.Compiler.c_init_costlabel in
    6364  let s_costmap = output.Extracted.Compiler.c_stack_cost in
    64   let style = Cost_instrumented (l_costmap,s_costmap) in
     65  let maxstack = output.Extracted.Compiler.c_max_stack in
     66  let style = Cost_instrumented (l_costmap,init_costlabel,s_costmap,maxstack) in
    6567  let instrumented = ClightPrinter.print_program style labelled in
    6668  let basename =
  • 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";
  • extracted/compiler.ml

    r3059 r3083  
    471471let colour_graph = Compute_colouring.colour_graph
    472472 
    473 
    474 
    475473open AssocList
    476474
     
    485483(** val back_end :
    486484    observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
    487     ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod,
    488     Nat.nat) Types.prod Errors.res **)
     485    (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
     486    Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res **)
    489487let back_end observe init_cost p =
    490488  let p0 = RTLabsToRTL.rtlabs_to_rtl init_cost p in
     
    498496  let st0 = lookup_stack_cost (Joint.graph_params_to_params ERTL.eRTL) p1 in
    499497  let i1 = Obj.magic observe Ertl_pass { Types.fst = p1; Types.snd = st0 } in
    500   let { Types.fst = eta28675; Types.snd = max_stack } =
     498  let { Types.fst = eta2; Types.snd = max_stack } =
    501499    ERTLToLTL.ertl_to_ltl compute_fixpoint colour_graph p1
    502500  in
    503   let { Types.fst = p2; Types.snd = stack_cost } = eta28675 in
     501  let { Types.fst = p2; Types.snd = stack_cost } = eta2 in
    504502  let st1 = lookup_stack_cost (Joint.graph_params_to_params LTL.lTL) p2 in
    505503  let i2 = Obj.magic observe Ltl_pass { Types.fst = p2; Types.snd = st1 } in
     
    514512          (LINToASM.lin_to_asm p3))) (fun p4 ->
    515513      Monad.m_return0 (Monad.max_def Errors.res0) { Types.fst = { Types.fst =
    516         p4; Types.snd = stack_cost }; Types.snd = max_stack }))
     514        { Types.fst = p4; Types.snd = init_cost }; Types.snd = stack_cost };
     515        Types.snd = max_stack }))
    517516
    518517open Assembly
     
    584583                         c_stack_cost : Joint.stack_cost_model;
    585584                         c_max_stack : Nat.nat;
     585                         c_init_costlabel : CostLabel.costlabel;
    586586                         c_labelled_clight : Csyntax.clight_program;
    587587                         c_clight_cost_map : Label.clight_cost_map }
     
    589589(** val compiler_output_rect_Type4 :
    590590    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    591     Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    592     compiler_output -> 'a1 **)
    593 let rec compiler_output_rect_Type4 h_mk_compiler_output x_23441 =
     591    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     592    'a1) -> compiler_output -> 'a1 **)
     593let rec compiler_output_rect_Type4 h_mk_compiler_output x_185 =
    594594  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    595     c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    596     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23441
     595    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
     596    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
     597    c_clight_cost_map = c_clight_cost_map0 } = x_185
    597598  in
    598599  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    599     c_labelled_clight0 c_clight_cost_map0
     600    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
    600601
    601602(** val compiler_output_rect_Type5 :
    602603    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    603     Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    604     compiler_output -> 'a1 **)
    605 let rec compiler_output_rect_Type5 h_mk_compiler_output x_23443 =
     604    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     605    'a1) -> compiler_output -> 'a1 **)
     606let rec compiler_output_rect_Type5 h_mk_compiler_output x_187 =
    606607  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    607     c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    608     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23443
     608    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
     609    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
     610    c_clight_cost_map = c_clight_cost_map0 } = x_187
    609611  in
    610612  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    611     c_labelled_clight0 c_clight_cost_map0
     613    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
    612614
    613615(** val compiler_output_rect_Type3 :
    614616    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    615     Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    616     compiler_output -> 'a1 **)
    617 let rec compiler_output_rect_Type3 h_mk_compiler_output x_23445 =
     617    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     618    'a1) -> compiler_output -> 'a1 **)
     619let rec compiler_output_rect_Type3 h_mk_compiler_output x_189 =
    618620  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    619     c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    620     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23445
     621    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
     622    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
     623    c_clight_cost_map = c_clight_cost_map0 } = x_189
    621624  in
    622625  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    623     c_labelled_clight0 c_clight_cost_map0
     626    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
    624627
    625628(** val compiler_output_rect_Type2 :
    626629    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    627     Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    628     compiler_output -> 'a1 **)
    629 let rec compiler_output_rect_Type2 h_mk_compiler_output x_23447 =
     630    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     631    'a1) -> compiler_output -> 'a1 **)
     632let rec compiler_output_rect_Type2 h_mk_compiler_output x_191 =
    630633  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    631     c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    632     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23447
     634    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
     635    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
     636    c_clight_cost_map = c_clight_cost_map0 } = x_191
    633637  in
    634638  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    635     c_labelled_clight0 c_clight_cost_map0
     639    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
    636640
    637641(** val compiler_output_rect_Type1 :
    638642    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    639     Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    640     compiler_output -> 'a1 **)
    641 let rec compiler_output_rect_Type1 h_mk_compiler_output x_23449 =
     643    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     644    'a1) -> compiler_output -> 'a1 **)
     645let rec compiler_output_rect_Type1 h_mk_compiler_output x_193 =
    642646  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    643     c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    644     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23449
     647    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
     648    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
     649    c_clight_cost_map = c_clight_cost_map0 } = x_193
    645650  in
    646651  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    647     c_labelled_clight0 c_clight_cost_map0
     652    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
    648653
    649654(** val compiler_output_rect_Type0 :
    650655    (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    651     Csyntax.clight_program -> Label.clight_cost_map -> 'a1) ->
    652     compiler_output -> 'a1 **)
    653 let rec compiler_output_rect_Type0 h_mk_compiler_output x_23451 =
     656    CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     657    'a1) -> compiler_output -> 'a1 **)
     658let rec compiler_output_rect_Type0 h_mk_compiler_output x_195 =
    654659  let { c_labelled_object_code = c_labelled_object_code0; c_stack_cost =
    655     c_stack_cost0; c_max_stack = c_max_stack0; c_labelled_clight =
    656     c_labelled_clight0; c_clight_cost_map = c_clight_cost_map0 } = x_23451
     660    c_stack_cost0; c_max_stack = c_max_stack0; c_init_costlabel =
     661    c_init_costlabel0; c_labelled_clight = c_labelled_clight0;
     662    c_clight_cost_map = c_clight_cost_map0 } = x_195
    657663  in
    658664  h_mk_compiler_output c_labelled_object_code0 c_stack_cost0 c_max_stack0
    659     c_labelled_clight0 c_clight_cost_map0
     665    c_init_costlabel0 c_labelled_clight0 c_clight_cost_map0
    660666
    661667(** val c_labelled_object_code :
     
    672678  xxx.c_max_stack
    673679
     680(** val c_init_costlabel : compiler_output -> CostLabel.costlabel **)
     681let rec c_init_costlabel xxx =
     682  xxx.c_init_costlabel
     683
    674684(** val c_labelled_clight : compiler_output -> Csyntax.clight_program **)
    675685let rec c_labelled_clight xxx =
     
    682692(** val compiler_output_inv_rect_Type4 :
    683693    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    684     Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
    685     -> 'a1 **)
     694    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     695    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
    686696let compiler_output_inv_rect_Type4 hterm h1 =
    687697  let hcut = compiler_output_rect_Type4 h1 hterm in hcut __
     
    689699(** val compiler_output_inv_rect_Type3 :
    690700    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    691     Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
    692     -> 'a1 **)
     701    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     702    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
    693703let compiler_output_inv_rect_Type3 hterm h1 =
    694704  let hcut = compiler_output_rect_Type3 h1 hterm in hcut __
     
    696706(** val compiler_output_inv_rect_Type2 :
    697707    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    698     Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
    699     -> 'a1 **)
     708    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     709    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
    700710let compiler_output_inv_rect_Type2 hterm h1 =
    701711  let hcut = compiler_output_rect_Type2 h1 hterm in hcut __
     
    703713(** val compiler_output_inv_rect_Type1 :
    704714    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    705     Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
    706     -> 'a1 **)
     715    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     716    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
    707717let compiler_output_inv_rect_Type1 hterm h1 =
    708718  let hcut = compiler_output_rect_Type1 h1 hterm in hcut __
     
    710720(** val compiler_output_inv_rect_Type0 :
    711721    compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    712     Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1)
    713     -> 'a1 **)
     722    Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     723    Label.clight_cost_map -> __ -> 'a1) -> 'a1 **)
    714724let compiler_output_inv_rect_Type0 hterm h1 =
    715725  let hcut = compiler_output_rect_Type0 h1 hterm in hcut __
    716 
    717 (** val compiler_output_discr : compiler_output -> compiler_output -> __ **)
    718 let compiler_output_discr x y =
    719   Logic.eq_rect_Type2 x
    720     (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
    721        c_labelled_clight = a3; c_clight_cost_map = a4 } = x
    722      in
    723     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
    724726
    725727(** val compiler_output_jmdiscr :
     
    728730  Logic.eq_rect_Type2 x
    729731    (let { c_labelled_object_code = a0; c_stack_cost = a1; c_max_stack = a2;
    730        c_labelled_clight = a3; c_clight_cost_map = a4 } = x
     732       c_init_costlabel = a3; c_labelled_clight = a4; c_clight_cost_map =
     733       a5 } = x
    731734     in
    732     Obj.magic (fun _ dH -> dH __ __ __ __ __)) y
     735    Obj.magic (fun _ dH -> dH __ __ __ __ __ __)) y
    733736
    734737(** val compile :
     
    740743      Monad.m_bind3 (Monad.max_def Errors.res0)
    741744        (Obj.magic (back_end observe init_cost p0))
    742         (fun p1 stack_cost max_stack ->
     745        (fun p_init_costlabel stack_cost max_stack ->
     746        let { Types.fst = p1; Types.snd = init_costlabel } = p_init_costlabel
     747        in
    743748        Monad.m_bind0 (Monad.max_def Errors.res0)
    744749          (Obj.magic (assembler observe p1)) (fun p2 ->
     
    747752          Monad.m_return0 (Monad.max_def Errors.res0)
    748753            { c_labelled_object_code = p2; c_stack_cost = stack_cost;
    749             c_max_stack = max_stack; c_labelled_clight = p';
    750             c_clight_cost_map = k' }))))
    751 
     754            c_max_stack = max_stack; c_init_costlabel = init_costlabel;
     755            c_labelled_clight = p'; c_clight_cost_map = k' }))))
     756
  • extracted/compiler.mli

    r3059 r3083  
    320320val back_end :
    321321  observe_pass -> CostLabel.costlabel -> RTLabs_syntax.rTLabs_program ->
    322   ((ASM.pseudo_assembly_program, Joint.stack_cost_model) Types.prod, Nat.nat)
    323   Types.prod Errors.res
     322  (((ASM.pseudo_assembly_program, CostLabel.costlabel) Types.prod,
     323  Joint.stack_cost_model) Types.prod, Nat.nat) Types.prod Errors.res
    324324
    325325open Assembly
     
    363363                         c_stack_cost : Joint.stack_cost_model;
    364364                         c_max_stack : Nat.nat;
     365                         c_init_costlabel : CostLabel.costlabel;
    365366                         c_labelled_clight : Csyntax.clight_program;
    366367                         c_clight_cost_map : Label.clight_cost_map }
     
    368369val compiler_output_rect_Type4 :
    369370  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    370   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    371   -> 'a1
     371  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     372  'a1) -> compiler_output -> 'a1
    372373
    373374val compiler_output_rect_Type5 :
    374375  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    375   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    376   -> 'a1
     376  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     377  'a1) -> compiler_output -> 'a1
    377378
    378379val compiler_output_rect_Type3 :
    379380  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    380   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    381   -> 'a1
     381  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     382  'a1) -> compiler_output -> 'a1
    382383
    383384val compiler_output_rect_Type2 :
    384385  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    385   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    386   -> 'a1
     386  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     387  'a1) -> compiler_output -> 'a1
    387388
    388389val compiler_output_rect_Type1 :
    389390  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    390   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    391   -> 'a1
     391  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     392  'a1) -> compiler_output -> 'a1
    392393
    393394val compiler_output_rect_Type0 :
    394395  (ASM.labelled_object_code -> Joint.stack_cost_model -> Nat.nat ->
    395   Csyntax.clight_program -> Label.clight_cost_map -> 'a1) -> compiler_output
    396   -> 'a1
     396  CostLabel.costlabel -> Csyntax.clight_program -> Label.clight_cost_map ->
     397  'a1) -> compiler_output -> 'a1
    397398
    398399val c_labelled_object_code : compiler_output -> ASM.labelled_object_code
     
    401402
    402403val c_max_stack : compiler_output -> Nat.nat
     404
     405val c_init_costlabel : compiler_output -> CostLabel.costlabel
    403406
    404407val c_labelled_clight : compiler_output -> Csyntax.clight_program
     
    408411val compiler_output_inv_rect_Type4 :
    409412  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    410   Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
    411   'a1
     413  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     414  Label.clight_cost_map -> __ -> 'a1) -> 'a1
    412415
    413416val compiler_output_inv_rect_Type3 :
    414417  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    415   Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
    416   'a1
     418  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     419  Label.clight_cost_map -> __ -> 'a1) -> 'a1
    417420
    418421val compiler_output_inv_rect_Type2 :
    419422  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    420   Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
    421   'a1
     423  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     424  Label.clight_cost_map -> __ -> 'a1) -> 'a1
    422425
    423426val compiler_output_inv_rect_Type1 :
    424427  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    425   Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
    426   'a1
     428  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     429  Label.clight_cost_map -> __ -> 'a1) -> 'a1
    427430
    428431val compiler_output_inv_rect_Type0 :
    429432  compiler_output -> (ASM.labelled_object_code -> Joint.stack_cost_model ->
    430   Nat.nat -> Csyntax.clight_program -> Label.clight_cost_map -> __ -> 'a1) ->
    431   'a1
    432 
    433 val compiler_output_discr : compiler_output -> compiler_output -> __
     433  Nat.nat -> CostLabel.costlabel -> Csyntax.clight_program ->
     434  Label.clight_cost_map -> __ -> 'a1) -> 'a1
    434435
    435436val compiler_output_jmdiscr : compiler_output -> compiler_output -> __
  • src/compiler.ma

    r3022 r3083  
    8787definition back_end :
    8888 observe_pass → costlabel → RTLabs_program →
    89   res (pseudo_assembly_program × stack_cost_model × nat) ≝
     89  res (pseudo_assembly_program × costlabel × stack_cost_model × nat) ≝
    9090λobserve,init_cost,p.
    9191  let p ≝ rtlabs_to_rtl init_cost p in
     
    105105  let i ≝ observe lin_pass 〈p,st〉 in
    106106   ! p ← opt_to_res ? (msg AssemblyTooLarge) (lin_to_asm p) ;
    107    return 〈p,stack_cost,max_stack〉.
     107   return 〈〈p,init_cost〉,stack_cost,max_stack〉.
    108108
    109109(* The assembler *)
     
    148148 ; c_stack_cost: stack_cost_model
    149149 ; c_max_stack: nat
     150 ; c_init_costlabel: costlabel
    150151 ; c_labelled_clight: clight_program
    151152 ; c_clight_cost_map: clight_cost_map
     
    155156λobserve,p.
    156157  ! 〈init_cost,p',p〉 ← front_end observe p;
    157   ! 〈p,stack_cost,max_stack〉 ← back_end observe init_cost p;
     158  ! 〈p_init_costlabel,stack_cost,max_stack〉 ← back_end observe init_cost p;
     159  let 〈p,init_costlabel〉 ≝ p_init_costlabel in
    158160  ! p ← assembler observe p;
    159161  let k ≝ ASM_cost_map p in
    160162  let k' ≝
    161163   lift_cost_map_back_to_front p k in
    162   return mk_compiler_output p stack_cost max_stack p' k'.
     164  return mk_compiler_output p stack_cost max_stack init_costlabel p' k'.
Note: See TracChangeset for help on using the changeset viewer.