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/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.
Note: See TracChangeset for help on using the changeset viewer.