Changeset 2214 for src/ERTL


Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (8 years ago)
Author:
tranquil
Message:
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
Location:
src/ERTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL_paolo.ma

    r2208 r2214  
     1
    12include "LTL/LTL_paolo.ma".
    23include "ERTL/Interference_paolo.ma".
     
    1819coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.
    1920
    20 definition stacksize :
    21   ∀globals.ℕ → joint_internal_function globals ertl_params → ℕ ≝
    22   λglobals.
    23   λspilled_no.
    24   λint_fun.
    25   spilled_no + joint_if_stacksize … int_fun.
    26 
    2721(* Paolo: I'm changing the following: before, spilled registers were
    2822  assigned stack addresses going from SP + #frame_size - #stack_params
     
    3125
    3226definition preserve_carry_bit :
    33   ∀globals.bool → list (joint_seq ltl_params globals) → list (joint_seq ltl_params globals) ≝
     27  ∀globals.bool → list (joint_seq LTL globals) → list (joint_seq LTL globals) ≝
    3428  λglobals,do_it,steps.
    3529  if do_it then SAVE_CARRY :: steps @ [RESTORE_CARRY] else steps.
     
    4236(* spill should be byte-based from the start *)
    4337definition set_dp_by_offset :
    44   ∀globals.nat → list (joint_seq ltl_params globals) ≝
     38  ∀globals.nat → list (joint_seq LTL globals) ≝
    4539  λglobals,off.
    4640  [ A ← byte_of_nat off
     
    5347
    5448definition get_stack:
    55  ∀globals.Register → nat → list (joint_seq ltl_params globals) ≝
     49 ∀globals.Register → nat → list (joint_seq LTL globals) ≝
    5650 λglobals,r,off.
    5751 set_dp_by_offset ? off @
     
    6054
    6155definition set_stack_not_a :
    62  ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
     56 ∀globals.nat → Register → list (joint_seq LTL globals) ≝
    6357 λglobals,off,r.
    6458 set_dp_by_offset ? off @
     
    6761
    6862definition set_stack_a :
    69  ∀globals.nat → list (joint_seq ltl_params globals) ≝
     63 ∀globals.nat → list (joint_seq LTL globals) ≝
    7064 λglobals,off.
    7165 [ RegisterST1 ← A ] @
     
    7367
    7468definition set_stack :
    75  ∀globals.nat → Register → list (joint_seq ltl_params globals) ≝
     69 ∀globals.nat → Register → list (joint_seq LTL globals) ≝
    7670 λglobals,off,r.
    7771 if eq_Register r RegisterA then
     
    8175 
    8276definition set_stack_int :
    83   ∀globals.nat → beval →  list (joint_seq ltl_params globals) ≝
     77  ∀globals.nat → beval →  list (joint_seq LTL globals) ≝
    8478  λglobals,off,int.
    8579  set_dp_by_offset ? off @
     
    8882
    8983definition move :
    90   ∀globals.bool → decision → arg_decision → list (joint_seq ltl_params globals) ≝
     84  ∀globals.bool → decision → arg_decision → list (joint_seq LTL globals) ≝
    9185  λglobals,carry_lives_after,dst,src.
    9286  match dst with
     
    128122
    129123definition newframe :
    130   ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
     124  ∀globals.ℕ → list (joint_seq LTL globals) ≝
    131125  λglobals,stack_sz.
    132126  [ CLEAR_CARRY …
     
    140134
    141135definition delframe :
    142   ∀globals.ℕ → list (joint_seq ltl_params globals) ≝
     136  ∀globals.ℕ → list (joint_seq LTL globals) ≝
    143137  λglobals,stack_sz.
    144138  [ A ← RegisterSPL
     
    176170
    177171definition translate_op2 :
    178   ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     172  ∀globals.bool→ Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    179173  λglobals,carry_lives_after,op,dst,arg1,arg2.
    180174  (* this won't preserve the carry bit if op does not set it: left to next function *)
     
    189183
    190184definition translate_op2_smart :
    191   ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     185  ∀globals.bool → Op2 → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    192186  λglobals,carry_lives_after,op,dst,arg1,arg2.
    193187  (* if op does not set carry bit (⇒ it does not use it either) then it must be
     
    232226
    233227definition translate_op1 :
    234   ∀globals.bool → Op1 → decision → decision → list (joint_seq ltl_params globals) ≝
     228  ∀globals.bool → Op1 → decision → decision → list (joint_seq LTL globals) ≝
    235229  λglobals,carry_lives_after,op,dst,arg.
    236230  let preserve_carry ≝ carry_lives_after ∧ (is_spilled dst ∨ is_spilled arg) in
     
    241235
    242236definition translate_opaccs :
    243   ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     237  ∀globals.bool → OpAccs → decision → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    244238  λglobals,carry_lives_after,op,dst1,dst2,arg1,arg2.
    245239  (* OPACCS always has dead carry bit and sets it to zero *)
     
    255249(* does not preserve carry bit *)
    256250definition move_to_dp :
    257   ∀globals.arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     251  ∀globals.arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    258252  λglobals,arg1,arg2.
    259253  if ¬arg_is_spilled arg1 then
     
    272266
    273267definition translate_store : 
    274   ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     268  ∀globals.bool → arg_decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    275269  λglobals,carry_lives_after,addr1,addr2,src.
    276270  (* requires src != RegisterA and RegisterB *)
     
    286280
    287281definition translate_load : 
    288   ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq ltl_params globals) ≝
     282  ∀globals.bool → decision → arg_decision → arg_decision → list (joint_seq LTL globals) ≝
    289283  λglobals,carry_lives_after,dst,addr1,addr2.
    290284  preserve_carry_bit ? (carry_lives_after ∧
     
    296290definition translate_address :
    297291  ∀globals.bool → ∀i.member i (eq_identifier ?) globals → decision → decision →
    298   list (joint_seq ltl_params globals) ≝
     292  list (joint_seq LTL globals) ≝
    299293  λglobals,carry_lives_after,id,prf,addr1,addr2.
    300294  preserve_carry_bit ? (carry_lives_after ∧ (is_spilled addr1 ∨ is_spilled addr2))
    301     (ADDRESS ltl_params ? id prf it it ::
     295    (ADDRESS LTL ? id prf it it ::
    302296     move ? false addr1 RegisterDPL @
    303297     move ? false addr2 RegisterDPH).
     
    306300  ∀globals.∀after : valuation register_lattice.
    307301  coloured_graph after →
    308   ℕ → label → joint_step ertl_params globals → seq_block ltl_params globals (joint_step ltl_params globals) ≝
     302  ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals) ≝
    309303  λglobals,after,grph,stack_sz,lbl,s.
    310304  let lookup ≝ λr.colouring … grph (inl … r) in
     
    317311  match s with
    318312  [ step_seq s' ⇒
    319     match s' return λ_.seq_block ltl_params globals (joint_step ltl_params globals) with
     313    match s' return λ_.seq_block LTL globals (joint_step LTL globals) with
    320314    [ COMMENT c ⇒ COMMENT … c
    321315    | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
     
    373367        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    374368      ]
    375     | CALL_ID f n_args _ ⇒ CALL_ID ltl_params ? f n_args it
     369    | CALL_ID f n_args _ ⇒ CALL_ID LTL ? f n_args it
    376370    | extension_call abs ⇒ match abs in void with [ ]
    377371    ]
     
    381375
    382376definition translate_fin_step:
    383   ∀globals.label → joint_fin_step ertl_params → seq_block ltl_params globals (joint_fin_step ltl_params) ≝
     377  ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL) ≝
    384378  λglobals,lbl,s.
    385   match s return λ_.seq_block ltl_params globals (joint_fin_step ltl_params) with
     379  match s return λ_.seq_block LTL globals (joint_fin_step LTL) with
    386380  [ RETURN ⇒ RETURN ?
    387381  | GOTO l ⇒ GOTO ? l
     
    390384
    391385definition translate_internal: ∀globals: list ident.
    392   joint_internal_function globals ertl_params →
    393   joint_internal_function globals ltl_params ≝
     386  joint_internal_function ERTL globals →
     387  joint_internal_function LTL globals ≝
    394388  λglobals: list ident.
    395   λint_fun: joint_internal_function globals ertl_params.
     389  λint_fun: joint_internal_function ERTL globals.
    396390  (* initialize graph *)
    397391  let entry ≝ pi1 … (joint_if_entry … int_fun) in
     
    405399  let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
    406400  (* initialize internal function *)
    407   let init ≝ mk_joint_internal_function globals ltl_params
     401  let init ≝ mk_joint_internal_function LTL globals
    408402    (joint_if_luniverse … int_fun)
    409403    (joint_if_runiverse … int_fun)
  • src/ERTL/ERTL_paolo.ma

    r2208 r2214  
     1
    12include "joint/Joint_paolo.ma".
    23include "RTL/RTL_paolo.ma".
     
    4849      (* localsT ≝ *) register).
    4950
    50 definition ertl_params ≝ mk_graph_params ertl_uns_params.
    51 definition ertl_program ≝ joint_program ertl_params.
     51definition ERTL ≝ mk_graph_params ertl_uns_params.
     52definition ertl_program ≝ joint_program ERTL.
    5253
    5354interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)).
     
    5657unification hint 0 ≔
    5758(*---------------*) ⊢
    58 pair_move ertl_params ≡ move_dst × move_src.
     59pair_move ERTL ≡ move_dst × move_src.
    5960unification hint 0 ≔
    6061(*---------------*) ⊢
    61 acc_a_reg ertl_params ≡ register.
     62acc_a_reg ERTL ≡ register.
    6263unification hint 0 ≔
    6364(*---------------*) ⊢
    64 acc_b_reg ertl_params ≡ register.
     65acc_b_reg ERTL ≡ register.
    6566unification hint 0 ≔
    6667(*---------------*) ⊢
    67 acc_a_arg ertl_params ≡ psd_argument.
     68acc_a_arg ERTL ≡ psd_argument.
    6869unification hint 0 ≔
    6970(*---------------*) ⊢
    70 acc_b_arg ertl_params ≡ psd_argument.
     71acc_b_arg ERTL ≡ psd_argument.
    7172unification hint 0 ≔
    7273(*---------------*) ⊢
    73 dpl_reg ertl_params ≡ register.
     74dpl_reg ERTL ≡ register.
    7475unification hint 0 ≔
    7576(*---------------*) ⊢
    76 dph_reg ertl_params ≡ register.
     77dph_reg ERTL ≡ register.
    7778unification hint 0 ≔
    7879(*---------------*) ⊢
    79 dpl_arg ertl_params ≡ psd_argument.
     80dpl_arg ERTL ≡ psd_argument.
    8081unification hint 0 ≔
    8182(*---------------*) ⊢
    82 dph_arg ertl_params ≡ psd_argument.
     83dph_arg ERTL ≡ psd_argument.
    8384unification hint 0 ≔
    8485(*---------------*) ⊢
    85 snd_arg ertl_params ≡ psd_argument.
     86snd_arg ERTL ≡ psd_argument.
    8687unification hint 0 ≔
    8788(*---------------*) ⊢
    88 call_args ertl_params ≡ ℕ.
     89call_args ERTL ≡ ℕ.
    8990unification hint 0 ≔
    9091(*---------------*) ⊢
    91 call_dest ertl_params ≡ unit.
     92call_dest ERTL ≡ unit.
    9293
    9394unification hint 0 ≔
    9495(*---------------*) ⊢
    95 ext_seq ertl_params ≡ ertl_seq.
     96ext_seq ERTL ≡ ertl_seq.
    9697unification hint 0 ≔
    9798(*---------------*) ⊢
    98 ext_call ertl_params ≡ void.
     99ext_call ERTL ≡ void.
    99100unification hint 0 ≔
    100101(*---------------*) ⊢
    101 ext_tailcall ertl_params ≡ void.
     102ext_tailcall ERTL ≡ void.
    102103
    103 coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ertl_params
     104coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL
    104105  psd_argument_from_reg
    105   on _r : register to snd_arg ertl_params.
    106 coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ertl_params
     106  on _r : register to snd_arg ERTL.
     107coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL
    107108  psd_argument_from_byte
    108   on _b : Byte to snd_arg ertl_params.
     109  on _b : Byte to snd_arg ERTL.
    109110 
    110 definition ertl_seq_joint ≝ extension_seq ertl_params.
    111 coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ertl_params globals ≝ ertl_seq_joint
    112   on _s : ertl_seq to joint_seq ertl_params.
    113 
     111definition ertl_seq_joint ≝ extension_seq ERTL.
     112coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
     113  on _s : ertl_seq to joint_seq ERTL.
  • src/ERTL/liveness_paolo.ma

    r2208 r2214  
     1
    12include "ASM/Util.ma".
    23include "ERTL/ERTL_paolo.ma".
     
    4243definition defined ≝
    4344  λglobals: list ident.
    44   λs: joint_statement ertl_params globals.
     45  λs: joint_statement ERTL globals.
    4546  match s with
    4647  [ sequential seq l ⇒
     
    100101definition used ≝
    101102  λglobals: list ident.
    102   λs: joint_statement ertl_params globals.
     103  λs: joint_statement ERTL globals.
    103104  match s with
    104105  [ sequential seq l ⇒
     
    155156  λglobals: list ident.
    156157  λl: register_lattice.
    157   λs: joint_statement ertl_params globals.
     158  λs: joint_statement ERTL globals.
    158159  let pliveafter ≝ \fst l in
    159160  let hliveafter ≝ \snd l in
     
    225226
    226227definition statement_semantics: ∀globals: list ident.
    227   joint_statement ertl_params globals → register_lattice → register_lattice ≝
     228  joint_statement ERTL globals → register_lattice → register_lattice ≝
    228229  λglobals.
    229230  λstmt.
     
    236237definition livebefore ≝
    237238  λglobals: list ident.
    238   λint_fun: joint_internal_function globals ertl_params.
     239  λint_fun: joint_internal_function ERTL globals.
    239240  λlabel.
    240241  λliveafter: valuation register_lattice.
     
    246247definition liveafter ≝
    247248   λglobals: list ident.
    248   λint_fun: joint_internal_function globals ertl_params.
     249  λint_fun: joint_internal_function ERTL globals.
    249250  λlabel.
    250251  λliveafter: valuation register_lattice.
Note: See TracChangeset for help on using the changeset viewer.