Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (9 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>
File:
1 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)
Note: See TracChangeset for help on using the changeset viewer.