Changeset 3263 for src/ERTL/ERTLToLTL.ma


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)

File:
1 edited

Legend:

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