Changeset 3263 for src/joint


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/joint
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • 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.