Changeset 3263


Ignore:
Timestamp:
May 10, 2013, 1:40:31 PM (4 years ago)
Author:
tranquil
Message:

moved callee saved saving and restoring to ERTL -> LTL pass (untrusted
colourer and interference graph creator still need to be updated)
joint now has the stack size split in three (referenced locals, params
and spilled)

Location:
src
Files:
13 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r3255 r3263  
    7373    (* ext_seq_labels ≝ *) (λ_.[])
    7474    (* has_tailcall ≝ *) false
    75     (* paramsT ≝ *) .
     75    (* paramsT ≝ *) unit.
    7676
    7777definition regs_from_move_dst : move_dst → list register ≝
     
    169169  (mk_universe … (p0 (p0 one)))
    170170  (mk_universe … one)
    171   it 4 0 0 (empty_map …) l1 in
     171  it it 0 0 0 (empty_map …) l1 in
    172172(* todo: args for main? *)
    173173let res ≝ add_graph … l1
  • src/ERTL/ERTLToLTL.ma

    r3255 r3263  
    393393
    394394definition translate_fin_step:
    395   ∀globals.ℕ → label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
    396   λglobals,stack_sz,lbl,s.
     395  ∀globals.list (joint_seq LTL globals) →
     396  label → joint_fin_step ERTL → bind_fin_block LTL globals ≝
     397  λglobals,epilogue,lbl,s.
    397398  bret … (match s with
    398   [ RETURN ⇒ 〈delframe ? stack_sz, RETURN ?〉
     399  [ RETURN ⇒ 〈epilogue, RETURN ?〉
    399400  | GOTO l ⇒ 〈[ ], GOTO ? l〉
    400401  | TAILCALL abs _ _ ⇒ Ⓧabs
     
    407408  bind_new register (b_graph_translate_data ERTL LTL globals) ≝
    408409λthe_fixpoint,build,globals,int_fun.
     410νν |RegisterCalleeSaved| as callee_saved_store in
    409411(* colour registers *)
    410 let after ≝ analyse_liveness the_fixpoint globals int_fun in
    411 let coloured_graph ≝ build … int_fun after in
    412 (* compute new stack size *)
     412let after ≝ analyse_liveness the_fixpoint globals int_fun callee_saved_store in
     413let coloured_graph ≝ build … int_fun after callee_saved_store in
     414let callee_saved_pairs ≝ zip_pottier … RegisterCalleeSaved callee_saved_store in
     415let localss ≝ joint_if_local_stacksize ?? int_fun in
     416let save ≝ \fold[append ?, nil ?]_{R_r ∈ callee_saved_pairs}
     417  (move ? localss false
     418    (colouring … coloured_graph (inl … (\snd R_r)))
     419    (decision_colour (\fst R_r))) in
     420let restore ≝ \fold[append ?, nil ?]_{R_r ∈ callee_saved_pairs}
     421  (move ? localss false
     422    (decision_colour (\fst R_r))
     423    (colouring … coloured_graph (inl … (\snd R_r)))) in
    413424let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
    414425bret …
     
    416427    (* init_ret ≝ *) it
    417428    (* init_params ≝ *) it
    418     (* init_stack_size ≝ *) stack_sz
    419     (* added_prologue ≝ *) (newframe ? stack_sz)
    420     (* new_regs ≝ *) [ ]
    421     (* f_step ≝ *) (translate_step ? int_fun (joint_if_local_stacksize ?? int_fun) … coloured_graph stack_sz)
    422     (* f_fin ≝ *) (translate_fin_step globals stack_sz)
     429    (* added_local_stacksize ≝ *) 0
     430    (* added_params_stacksize ≝ *) 0
     431    (* added_spilled_stacksize ≝ *) (spilled_no … coloured_graph)
     432    (* added_prologue ≝ *) (newframe ? stack_sz @ save)
     433    (* new_regs ≝ *) callee_saved_store
     434    (* f_step ≝ *) (translate_step ? int_fun localss … coloured_graph stack_sz)
     435    (* f_fin ≝ *) (translate_fin_step globals (restore @ delframe ? stack_sz))
    423436    ????).
    424437@hide_prf
    425 [
    426 | #l #c % ]
     438[3: #l #c % ]
    427439cases daemon (* TODO *)
    428440qed.
     
    437449   let ltlprog ≝ b_graph_transform_program … (translate_data the_fixpoint build) pr in
    438450   〈ltlprog, stack_cost … ltlprog, 2^16 - globals_stacksize … ltlprog〉.
    439 %
     451#r0 #r1 #r2 #r3 #r4 #r5 #r6 #r7 %
    440452qed.
    441453
     
    444456∀p_in.
    445457let cost_m ≝ \snd (\fst (ertl_to_ltl fix col p_in)) in
    446 stack_cost_model_le (stack_cost ? p_in) cost_m.
    447 #fix #col #p_in whd
    448 @list_map_opt_All2
    449 [ @(λid_def1,id_def2.
    450    match \snd id_def1 with
    451    [ Internal f1 ⇒
    452      match \snd id_def2 with
    453      [ Internal f2 ⇒
    454        \fst id_def1 = \fst id_def2 ∧
    455        le (joint_if_stacksize … f1) (joint_if_stacksize … f2)
    456      | _ ⇒ False
    457      ]
    458    | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
    459    ])
    460 | * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
    461   ** #H %{H} % ]
    462 @All2_of_map * #id * #f normalize nodelta [2: %]
    463 % [%]
    464 cases (b_graph_translate ?????) #f_out * #data **
    465 [2: #hd #tl ] * #f_lbls * #f_regs * [*] whd in ⊢ (%→?); #EQ_data
    466 #props >(ss_def_out_eq … props) >EQ_data
    467 generalize in match (joint_if_stacksize ???); generalize in match (spilled_no ??);
    468 -p_in //
    469 qed.
    470 
     458stack_cost_model_le (stack_cost ? p_in) cost_m ≝
     459λfix,col.joint_transform_monotone_stacksizes ….
  • src/ERTL/Interference.ma

    r3255 r3263  
    7474  ∀fn:joint_internal_function ERTL globals.
    7575   ∀liveafter.
     76    list register → (* callee saved store *)
    7677    coloured_graph (interferes … fn liveafter).
  • src/ERTL/liveness.ma

    r3255 r3263  
    9696definition used ≝
    9797  λglobals: list ident.
     98  λcallee_saved_store : list register.
    9899  λs: joint_statement ERTL globals.
    99100  match s with
     
    143144  | final fin ⇒
    144145    match fin with
    145     [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
     146    [ RETURN ⇒ 〈set_from_list … callee_saved_store,
     147                set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    146148    | GOTO l ⇒ rl_bottom
    147149    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
     
    205207  ].
    206208
    207 definition statement_semantics: ∀globals: list ident.
     209definition statement_semantics: ∀globals: list ident.list register →
    208210  joint_statement ERTL globals → register_lattice → register_lattice ≝
    209   λglobals.
     211  λglobals,callee_saved_store.
    210212  λstmt.
    211213  λliveafter.
     
    213215    liveafter
    214216  else
    215     rl_join (rl_diff liveafter (defined globals stmt)) (used globals stmt).
     217    rl_join (rl_diff liveafter (defined globals stmt))
     218      (used globals callee_saved_store stmt).
    216219
    217220definition livebefore:
    218221  ∀globals: list ident.
    219222   joint_internal_function ERTL globals →
     223   list register →
    220224     valuation register_lattice → valuation register_lattice
    221225
    222226  λglobals: list ident.
    223227  λint_fun: joint_internal_function ERTL globals.
     228  λcallee_saved_store.
    224229  λliveafter: valuation register_lattice.
    225230  λlabel.
    226231  match lookup ?? (joint_if_code … int_fun) label with
    227232  [ None      ⇒ rl_bottom
    228   | Some stmt ⇒ statement_semantics globals stmt (liveafter label)
     233  | Some stmt ⇒ statement_semantics globals callee_saved_store stmt (liveafter label)
    229234  ].
    230235
     
    232237   λglobals: list ident.
    233238  λint_fun: joint_internal_function ERTL globals.
     239  λcallee_saved_store.
    234240  λlabel.
    235241  λliveafter: valuation register_lattice.
     
    238244  | Some stmt ⇒
    239245    \fold[rl_join,rl_bottom]_{successor ∈ stmt_labels … stmt}
    240       (livebefore globals int_fun liveafter successor)
     246      (livebefore globals int_fun callee_saved_store liveafter successor)
    241247  ].
    242248
    243249definition analyse_liveness ≝
    244   λthe_fixpoint: fixpoint_computer. λglobals,int_fun.
    245    the_fixpoint ? (liveafter globals int_fun).
     250  λthe_fixpoint: fixpoint_computer. λglobals,int_fun,callee_saved_store.
     251   the_fixpoint ? (liveafter globals int_fun callee_saved_store).
    246252
    247253definition vertex ≝ register + Register.
  • src/ERTL/uses.ma

    r3257 r3263  
    1919
    2020definition examine_internal:
    21  ∀globals. joint_internal_function ERTL globals →
     21 ∀globals. joint_internal_function ERTL globals → list register →
    2222  identifier_map RegisterTag Pos ≝
    23 λglobals,fun.
     23λglobals,fun,callee_saved_store.
    2424 let incr ≝
    2525  λr,map.
     
    7474   | FCOND (abs : has_fcond ERTL) _ _ _ ⇒ Ⓧabs ]
    7575 in
    76  foldi … f (joint_if_code … fun) (empty_map …).
     76 foldi … f (joint_if_code … fun)
     77  (* registers used to store callee saved are used 2 times. We can
     78     increase the likelihood of these registers being assigned the
     79     corresponding callee saved reg by artificially increasing their uses *)
     80  (foldl … (λmap,r.incr r (incr r map)) (empty_map …) callee_saved_store).
  • src/LIN/LIN.ma

    r3037 r3263  
    4040  (mk_universe … (p0 (p0 one)))
    4141  (mk_universe … one)
    42   it it 0 0 code 0.
     42  it it 0 0 0 code 0.
    4343%
    4444[ * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct
  • src/LTL/LTL.ma

    r3037 r3263  
    4444  (mk_universe … (p0 (p0 one)))
    4545  (mk_universe … one)
    46   it it 0 0 (empty_map …) l1 in
     46  it it 0 0 0 (empty_map …) l1 in
    4747(* todo: args for main? *)
    4848let res ≝ add_graph … l1
  • src/RTL/RTL.ma

    r3037 r3263  
    108108  (mk_universe … (p0 (p0 one)))
    109109  (mk_universe … (p1 (p0 one)))
    110   [ ] rs 0 0 (empty_map …) l1 in
     110  [ ] rs 0 0 0 (empty_map …) l1 in
    111111(* todo: args for main? *)
    112112let res ≝ add_graph … l1
  • src/RTL/RTLToERTL.ma

    r3256 r3263  
    2828   Register36; Register37]. %% qed.
    2929
    30 definition RegisterCalleeSavedSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
     30(*definition RegisterCalleeSavedSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
    3131[Register20; Register21; Register22; Register23; Register24; Register25;
    32    Register26; Register27]. %% qed.
     32   Register26; Register27]. %% qed.*)
    3333
    3434definition RegisterRetsSig : list (Σr.ertl_hdw_readable r∧ertl_hdw_writable r) ≝
     
    120120
    121121definition epilogue :
    122   ∀globals.list register → register → register → list (register × (Σr.?)) →
     122  ∀globals.list register → register → register →
    123123  Σl : list (joint_seq ERTL globals).
    124124  All (joint_seq ??) (λs.step_labels ?? s = [ ]) l ≝
    125   λglobals,ret_regs,sral,srah,sregs.
    126   restore_hdws … (map ?? (λx.〈Reg ? (\fst x), \snd x〉) sregs) @
     125  λglobals,ret_regs,sral,srah.
    127126  assign_result globals ret_regs @
    128127  [ PUSH ERTL ? sral ;
     
    130129@hide_prf
    131130@All_append
    132 [ @(All_map … (All_True …)) #x #_ %
    133 | @All_append
    134   [ whd in match assign_result;
    135     generalize in match reduce_strong; #f normalize nodelta
    136     cases (f ????) #l #prf normalize nodelta
    137     @All_append
    138     [ @(All_map2 … (All2_True … prf)) #x #y #_ %
    139     | @(All_map … (All_True …)) #x #_ %
    140     ]
    141   | %%%
     131[ whd in match assign_result;
     132  generalize in match reduce_strong; #f normalize nodelta
     133  cases (f ????) #l #prf normalize nodelta
     134  @All_append
     135  [ @(All_map2 … (All2_True … prf)) #x #y #_ %
     136  | @(All_map … (All_True …)) #x #_ %
    142137  ]
     138| %%%
    143139]
    144140qed.
     
    146142definition prologue :
    147143  ∀globals.list register → register → register → register → register → register →
    148   list (register×(Σr.?)) →
    149144  bind_new register (list (joint_seq ERTL globals)) ≝
    150   λglobals,params,sral,srah,tmpr,addr1,addr2,sregs.
     145  λglobals,params,sral,srah,tmpr,addr1,addr2.
    151146  [ POP ERTL … srah ;
    152147    POP … sral
    153   ] @ save_hdws … sregs @ get_params … tmpr addr1 addr2 params.
     148  ] @ get_params … tmpr addr1 addr2 params.
    154149
    155150definition set_params_hdw :
     
    264259
    265260definition translate_fin_step :
    266   ∀globals.list register → register → register → list (register × (Σr.?)) →
     261  ∀globals.list register → register → register →
    267262    label → joint_fin_step RTL →
    268263    bind_fin_block ERTL globals ≝
    269   λglobals.λret_regs,ral,rah,to_restore.λ_.λs.
     264  λglobals.λral,rah,to_restore.λ_.λs.
    270265  match s return λ_.bind_fin_block ERTL ? with
    271266  [ GOTO lbl' ⇒ bret … 〈[ ], GOTO … lbl'〉
    272   | RETURN ⇒ bret … 〈epilogue … ret_regs ral rah to_restore, RETURN ?〉
     267  | RETURN ⇒ bret … 〈epilogue … ral rah to_restore, RETURN ?〉
    273268  | TAILCALL b _ _ ⇒ match b in False with [ ]
    274269  ].
    275 
    276 definition allocate_regs :
    277   ∀X : Type[0].
    278   (list (register×(Σr.?)) → bind_new register X) →
    279   bind_new register X ≝
    280   λX,f.
    281   let allocate_regs_internal ≝
    282     λacc : bind_new register (list (register × (Σr.?))).
    283     λr: Σr.?.
    284     ! tl ← acc ;
    285     νr' in return (〈r', r〉 :: tl) in
    286   ! to_save ← foldl ?? allocate_regs_internal (return [ ]) RegisterCalleeSavedSig ;
    287   f to_save.
    288270
    289271definition translate_data :
     
    292274λglobals,def.
    293275let params ≝ joint_if_params … def in
    294 let new_stacksize ≝
    295   joint_if_stacksize … def + (|params| - |RegisterParams|) in
    296 allocate_regs ?
    297   (λto_save.
    298276    νral,rah,tmpr,addr1,addr2 in
    299     ! prologue ← prologue globals params ral rah tmpr addr1 addr2 to_save ;
     277    ! prologue ← prologue globals params ral rah tmpr addr1 addr2 ;
    300278    return mk_b_graph_translate_data RTL ERTL globals
    301279    (* init_ret ≝ *) it
    302     (* init_params ≝ *) (|params|)
    303     (* init_stack_size ≝ *) new_stacksize
     280    (* init_params ≝ *) it
     281    (* init_local_stacksize ≝ *) (joint_if_local_stacksize … def)
     282    (* init_params_stacksize ≝ *) (joint_if_params_stacksize … def + (* is 0, but needed for monotonicity *)
     283                                   (|params| - |RegisterParams|))
     284    (* init_spilled_stacksize ≝ *) (joint_if_spilled_stacksize … def(* is 0, but needed for monotonicity *))
    304285    (* added_prologue ≝ *) prologue
    305     (* new_regs ≝ *) (reverse … (addr2 :: addr1 :: tmpr :: rah :: ral :: map … (λx.\fst x) to_save))
     286    (* new_regs ≝ *) ([ral ; rah ; tmpr ; addr1 ; addr2 ])
    306287    (* f_step ≝ *) (translate_step globals)
    307     (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah to_save)
    308     ????).
     288    (* f_fin ≝ *) (translate_fin_step globals (joint_if_result … def) ral rah)
     289    ????.
    309290@hide_prf
    310 [1,2: cases daemon (* TODO *)
    311 | #l #c %
    312 | #l * [ #c' | #f #args #dest | #a #ltrue | #s ] #c whd
     291[2: #l #c %
     292|1: #l * [ #c' | #f #args #dest | #a #ltrue | #s ] #c whd
    313293  [2: #r1 #r2 ] whd #l' #EQ destruct try %
    314294  cases s in EQ; whd in match ensure_step_block; normalize nodelta
    315295  try #a try #b try #c try #d try #e try #f destruct
    316296  cases a in b; #a1 #a2 normalize nodelta #EQ destruct
    317 | #r1 #r2 #r3 #r4 #r5 #r6 #r7 #r8 #ral #rah #tmpr #addr1 #addr2 %
     297|5: #ral #rah #tmpr #addr1 #addr2 %
     298|*:  cases daemon (* TODO *)
    318299]
    319300(* #l *
     
    388369lemma RTLToERTL_monotone_stacksizes :
    389370∀p_in.let p_out ≝ rtl_to_ertl p_in in
    390 stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out).
    391 #p_in whd
    392 @list_map_opt_All2
    393 [ @(λid_def1,id_def2.
    394    match \snd id_def1 with
    395    [ Internal f1 ⇒
    396      match \snd id_def2 with
    397      [ Internal f2 ⇒
    398        \fst id_def1 = \fst id_def2 ∧
    399        le (joint_if_stacksize … f1) (joint_if_stacksize … f2)
    400      | _ ⇒ False
    401      ]
    402    | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
    403    ])
    404 | * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
    405   ** #H %{H} % ]
    406 @All2_of_map * #id * #f normalize nodelta [2: %]
    407 % [%]
    408 cases (b_graph_translate ?????) #f_out * #data
    409 * *[2:#r1*[2:#r2*[2:#r3*[2:#r4*[2:#r5*[2:#r6*[2:#r7*[2:#r8*
    410   [2:#r9*[2:#r10*[2:#r11*[2:#r12*[2:#r13*[2:#r14 #tl]]]]]]]]]]]]]]
    411 * #f_lbls * #f_regs * try ( * @False) whd in ⊢ (%→?); #EQ_data
    412 #props >(ss_def_out_eq … props) >EQ_data
    413 generalize in match (joint_if_stacksize ???); generalize in match (length ??-length ??);
    414 -p_in //
    415 qed.
     371stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out) ≝
     372joint_transform_monotone_stacksizes ….
  • src/RTLabs/RTLabsToRTL.ma

    r3145 r3263  
    132132    mk_joint_internal_function RTL globals
    133133      (joint_if_luniverse … def') (joint_if_runiverse … def') ret'
    134       params' (joint_if_stacksize … def') (joint_if_local_stacksize … def')
     134      params' (joint_if_stacksize … def') (joint_if_local_stacksize … def') 0
    135135      (joint_if_code … def') (joint_if_entry … def') in
    136136   〈def'', lenv〉. @hide_prf
     
    10851085  let entry' ≝ pi1 … (f_entry def) in
    10861086  let init ≝ mk_joint_internal_function RTL globals
    1087     luniverse' runiverse' [ ] [ ] 0 0
     1087    luniverse' runiverse' [ ] [ ] 0 0 0
    10881088    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) entry' in
    10891089  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
     
    11031103    (joint_if_result … def)
    11041104    (joint_if_params … def)
    1105     stack_size' stack_size'
     1105    stack_size' 0 0
    11061106    (joint_if_code … def)
    11071107    (joint_if_entry … def).
     
    11451145  ** #H %{H} % ]
    11461146@All2_of_map * #id * #f normalize nodelta [2: %]
    1147 % [%] whd in match translate_internal; normalize nodelta
     1147% [%] whd in match translate_internal; whd in match joint_if_stacksize;
     1148normalize nodelta
    11481149cases (initialize_locals_params_ret ?????) normalize nodelta #a #b %1
    11491150qed.
  • src/joint/Joint.ma

    r3145 r3263  
    481481  joint_if_result   : call_dest p;
    482482  joint_if_params   : paramsT p;
    483   joint_if_stacksize: nat;
    484483  joint_if_local_stacksize: nat; (* size of the stack devoted to "forced" stack positions
    485484    (that are already on stack in the front end) *)
     485  joint_if_params_stacksize: nat; (* size of the stack devoted to parameters *)
     486  joint_if_spilled_stacksize: nat; (* size of the stack devoted to spilled registers *)
    486487  joint_if_code     : codeT p globals ;
    487488  joint_if_entry : code_point p (* Paolo: condition entry ∈ code is ensured by good_if ;
    488489  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *)
    489490}.
     491
     492definition joint_if_stacksize ≝ λp,globals,fn.
     493joint_if_spilled_stacksize p globals fn + joint_if_params_stacksize … fn +
     494joint_if_local_stacksize … fn.
    490495
    491496definition regs_in_universe : ∀p,globals.
     
    560565      (joint_if_params … int_fun) (joint_if_stacksize … int_fun)
    561566       (joint_if_local_stacksize … int_fun)
     567       (joint_if_params_stacksize … int_fun)
    562568      graph entry (*exit*).
    563569
     
    569575    luniverse (joint_if_runiverse … p) (joint_if_result … p)
    570576    (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
     577     (joint_if_params_stacksize … p)
    571578    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
    572579
     
    578585    (joint_if_luniverse … p) runiverse (joint_if_result … p)
    579586    (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
     587     (joint_if_params_stacksize … p)
    580588    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
    581589   
     
    588596     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    589597     (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
     598     (joint_if_params_stacksize … p)
    590599     code
    591600     (joint_if_entry … p)
  • src/joint/TranslateUtils.ma

    r3037 r3263  
    412412{ init_ret : call_dest dst
    413413; init_params : paramsT dst
    414 ; init_stack_size : ℕ
     414; added_local_stacksize : ℕ
     415; added_params_stacksize : ℕ
     416; added_spilled_stacksize : ℕ
    415417; added_prologue : list (joint_seq dst globals)
    416418; new_regs : list register (* new registers added globally *)
     
    499501; pars_def_out_eq :
    500502           joint_if_params … def_out = init_params … data
    501 ; ss_def_out_eq :
    502            joint_if_stacksize … def_out = init_stack_size … data
     503; local_ss_def_out_eq :
     504           joint_if_local_stacksize … def_out =
     505           joint_if_local_stacksize … def_in + added_local_stacksize … data
     506; params_ss_def_out_eq :
     507           joint_if_params_stacksize … def_out =
     508           joint_if_params_stacksize … def_in + added_params_stacksize … data
     509; spilled_ss_def_out_eq :
     510           joint_if_spilled_stacksize … def_out =
     511           joint_if_spilled_stacksize … def_in + added_spilled_stacksize … data
    503512; partition_lbls : partial_partition … f_lbls
    504513; partition_regs : partial_partition … f_regs
     
    541550
    542551definition pair_swap : ∀A,B.(A × B) → B × A ≝ λA,B,pr.〈\snd pr, \fst pr〉.
     552
    543553definition set_entry ≝
    544554  λglobals: list ident.
     
    551561      (joint_if_params … int_fun) (joint_if_stacksize … int_fun)
    552562       (joint_if_local_stacksize … int_fun)
     563       (joint_if_params_stacksize … int_fun)
    553564      (joint_if_code … int_fun) entry (*exit*).
    554565
     
    576587    (joint_if_luniverse … def)
    577588    runiv
    578     (init_ret … data) (init_params … data) (init_stack_size … data)
    579     (joint_if_local_stacksize … def)
     589    (init_ret … data) (init_params … data)
     590    (joint_if_local_stacksize … def + added_local_stacksize … data)
     591    (joint_if_params_stacksize … def + added_params_stacksize … data)
     592    (joint_if_spilled_stacksize … def + added_spilled_stacksize … data)
    580593    (empty_map ? (joint_statement ??))
    581594    entry in
     
    677690  add_translates … (map ?? (λf,start_lbl,dest_lbl. add_graph pars1 ? start_lbl (f dest_lbl)) stmt_list).
    678691  *)
     692
     693include "joint/joint_stacksizes.ma".
     694
     695lemma bind_new_P_mp' : ∀R,X,P,Q,m.
     696(∀l,x.P l x → Q l x) →
     697bind_new_P' R X P m → bind_new_P' R X Q m.
     698#R #X #P #Q #m lapply Q -Q lapply P -P elim m -m
     699[ #x #P #Q #H #G @H @G
     700| #f #IH #P #Q #H #G #r
     701  @IH [3: @(G r) |*:] #l @H
     702]
     703qed.
     704
     705lemma joint_transform_monotone_stacksizes :
     706∀src_g_pars,dst_g_pars : graph_params.
     707(* initialization *)
     708∀data.
     709∀p_in.
     710let p_out ≝ b_graph_transform_program src_g_pars dst_g_pars data p_in in
     711stack_cost_model_le (stack_cost ? p_in) (stack_cost ? p_out).
     712#src #dst #data #p_in
     713whd
     714@list_map_opt_All2
     715[ @(λid_def1,id_def2.
     716   match \snd id_def1 with
     717   [ Internal f1 ⇒
     718     match \snd id_def2 with
     719     [ Internal f2 ⇒
     720       \fst id_def1 = \fst id_def2 ∧
     721       le (joint_if_stacksize … f1) (joint_if_stacksize … f2)
     722     | _ ⇒ False
     723     ]
     724   | External _ ⇒ match \snd id_def2 with [ Internal _ ⇒ False | External _ ⇒ True ]
     725   ])
     726| * #id * #f1 * #id' * #f2 normalize nodelta [|*: * %]
     727  ** #H %{H} % ]
     728@All2_of_map * #id * #f normalize nodelta [2: %]
     729% [%]
     730cases (b_graph_translate ?????)
     731whd in match (jp_functions dst ?);
     732lapply f -f
     733generalize in match (?@jp_functions ??); #globals
     734#f_in #f_out * #data' * #regs * #f_lbls * #f_regs * #inst #props
     735whd in match joint_if_stacksize; normalize nodelta
     736@le_plus [ @le_plus ]
     737[ >(spilled_ss_def_out_eq … props)
     738| >(params_ss_def_out_eq … props)
     739| >(local_ss_def_out_eq … props)
     740] //
     741qed.
  • src/joint/linearise.ma

    r3037 r3263  
    849849   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
    850850   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
    851    (joint_if_stacksize ?? f_sig) (joint_if_local_stacksize ?? f_sig)
    852    code 0 (* exit is dummy! *), hide_prf ??»,
     851   (joint_if_local_stacksize ?? f_sig)
     852   (joint_if_params_stacksize ?? f_sig)
     853   (joint_if_spilled_stacksize ?? f_sig)
     854   code 0, hide_prf ??»,
    853855   sigma〉, proj1 ?? (pi2 ?? code_sigma)».
    854856cases daemon (*)
Note: See TracChangeset for help on using the changeset viewer.