Changeset 3263 for src/joint/Joint.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/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)
Note: See TracChangeset for help on using the changeset viewer.