Changeset 3263 for src/ERTL


Ignore:
Timestamp:
May 10, 2013, 1:40:31 PM (7 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/ERTL
Files:
5 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).
Note: See TracChangeset for help on using the changeset viewer.