Changeset 3083 for extracted


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.

Location:
extracted
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • 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 -> __
Note: See TracChangeset for help on using the changeset viewer.