Ignore:
Timestamp:
May 9, 2013, 12:49:38 AM (6 years ago)
Author:
piccolo
Message:

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTLProof.ma

    r3253 r3259  
    2020joint_abstract_status (mk_prog_params LTL_semantics prog stack_sizes).
    2121
    22 definition local_clear_sb_type ≝ decision → bool.
    23 definition clear_sb_type ≝ label → local_clear_sb_type.
    24 
    25 (*function that will be used in order to retrieve ERTL-states from LTL-states.
    26   Now it is an axiom. To be Implemented *)
    27 axiom to_be_cleared_sb : 
    28 ∀live_before : valuation register_lattice.
    29 coloured_graph live_before → clear_sb_type.
    30 
    31 definition local_clear_fb_type ≝ vertex → bool.
    32 definition clear_fb_type ≝ label → local_clear_fb_type.
    33 
    34 
    35 (*function that will be used in order to clear ERTL-states from dead registers.
    36   Now it is an axiom. To be implemented *)
    37 definition to_be_cleared_fb :
    38 ∀live_before : valuation register_lattice.clear_fb_type≝
    39 λlive_before,pt,v.notb (lives v (live_before pt)).
    40 
    41 include "common/ExtraIdentifiers.ma".
    42 
    43 definition sigma_fb_register_env : local_clear_fb_type → register_env beval →
    44 register_env beval ≝
    45 λclear_fun,regs.find_all … regs (λi.λ_.notb (clear_fun (inl ?? i))).
    46 
     22definition local_live_type ≝ vertex → bool.
     23definition live_type ≝ label → local_live_type.
     24
     25definition ps_relation :
     26ℕ → local_live_type → (vertex → decision) → (beval → beval → Prop) → 
     27pointer → register_env beval → hw_register_env × bemem → Prop ≝
     28λlocalss,live_fun,colour,R,sp,rgs,st.
     29gen_preserving … gen_res_preserve …
     30    (λr : (Σr.bool_to_Prop(live_fun (inl ?? r))).λd.colour(inl ?? r) = d) R
     31    (reg_retrieve rgs)
     32    (λd.match d with
     33        [decision_colour R ⇒ return hwreg_retrieve (\fst st) R
     34        |decision_spill n ⇒ opt_to_res ? [MSG FailedLoad]
     35                            (beloadv (\snd st)
     36                             (shift_pointer ? sp (bitvector_of_nat 8 (localss + n))))
     37        ]).
     38
     39definition hw_relation : local_live_type → (beval → beval → Prop) →
     40hw_register_env → hw_register_env → Prop ≝
     41λlive_fun,R,hw1,hw2.
     42∀r : Register.live_fun (inr ?? r) →
     43R (hwreg_retrieve hw1 r) (hwreg_retrieve hw2 r).
     44
     45include alias "arithmetics/nat.ma".
     46include alias "basics/logic.ma".
     47
     48(*filters now are axioms but they will be implemented *)
     49axiom ertl_sp_filter : pointer → Prop.
     50axiom ltl_sp_filter : pointer → Prop.
     51
     52definition mem_relation :
     53(beval → beval → Prop) → bemem → bemem → Prop ≝
     54λR,m1,m2.
     55gen_preserving ?? gen_opt_preserve ????
     56     (λptr1 : Σptr.ertl_sp_filter ptr.
     57     λptr2 : Σptr.ltl_sp_filter ptr.pi1 ?? ptr1 = pi1 ?? ptr2) R
     58     (beloadv m1) (beloadv m2).
     59
     60axiom frames_relation :
     61fixpoint_computer → coloured_graph_computer → 
     62ertl_program → (beval → beval → Prop) →
     63framesT ERTL_state → (hw_register_env × bemem) → Prop.
     64
     65(*
    4766definition register_of_bitvector :  BitVector 6 → option Register≝
    4867λvect.
     
    86105else if eqb n 36 then Some ? RegisterCarry (* was -1, increment as needed *)
    87106else None ?.
    88 
    89 
    90 
    91 definition sigma_fb_hw_register_env : local_clear_fb_type → hw_register_env →
    92 hw_register_env ≝
    93 λclear_fun,regs.
    94 let f ≝ λvect,val,m.
    95   match register_of_bitvector vect with
    96   [ Some r ⇒
    97      if (clear_fun (inr ?? r)) then
    98       m
    99      else
    100       insert … vect val m
    101   | None ⇒ m
    102   ] in
    103 mk_hw_register_env … (fold … f (reg_env … regs) (Stub …)) BBundef.
    104 
    105 definition sigma_fb_regs : local_clear_fb_type → ertl_reg_env → ertl_reg_env ≝
    106 λclear_fun,regs.〈sigma_fb_register_env clear_fun (\fst regs),
    107                  sigma_fb_hw_register_env clear_fun (\snd regs)〉.
    108 
    109 definition sigma_fb_frames : local_clear_fb_type →
    110 list (register_env beval × (Σb:block.block_region b=Code)) →
    111 list (register_env beval × (Σb:block.block_region b=Code)) ≝ 
    112 λclear_fun,frms.map … (λx.〈sigma_fb_register_env clear_fun (\fst x),\snd x〉) frms.
    113 
    114 definition sigma_fb_state:
    115  ertl_program → local_clear_fb_type →
    116   state ERTL_semantics → state ERTL_semantics ≝
    117 λprog,clear_fun,st.
    118 mk_state ?
    119  (option_map ?? (sigma_fb_frames clear_fun) (st_frms … st))
    120  (istack … st)
    121  (if clear_fun (inr ?? RegisterCarry) then BBundef
    122   else (carry … st))
    123  (sigma_fb_regs clear_fun (regs … st)) (m … st) (stack_usage … st).
     107*)
    124108
    125109axiom acc_is_dead : ∀fix_comp.∀prog : ertl_program.
     
    127111 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
    128112  ¬ lives (inr ? ? RegisterA) (livebefore  … fn after l).
    129 
     113(*
    130114axiom dead_registers_in_dead :
    131115 ∀fix_comp.∀build : coloured_graph_computer.
     
    138122  ¬ lives (inr ? ? R) (livebefore  … fn after l) →
    139123   to_be_cleared_sb … coloured_graph l R.
    140    
    141 axiom sigma_sb_state: list (Σb.block_region b = Code) →
    142  ertl_program → local_clear_sb_type → state LTL_semantics → state ERTL_semantics.
     124*)
    143125
    144126definition dummy_state : state ERTL_semantics ≝
     
    154136list (Σb:block.block_region b=Code) ≝ map … \snd.
    155137
    156 definition sigma_fb_state_pc :
    157  fixpoint_computer → coloured_graph_computer → ertl_program → 
    158   state_pc ERTL_semantics → state_pc ERTL_semantics ≝
    159  λfix_comp,colour,prog,st.
    160  let m ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
    161  let stacksizes ≝ lookup_stack_cost … m in 
    162  let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
    163  let globals ≝ prog_names … prog in
    164  match fetch_internal_function … ge (pc_block (pc … st)) with
    165   [ OK y ⇒
    166      let pt ≝ point_of_pc ERTL_semantics (pc ? st) in
    167      let after ≝ (analyse_liveness fix_comp (prog_names … prog) (\snd y)) in
    168      let before ≝ livebefore … (\snd y) after in
    169      mk_state_pc ? (sigma_fb_state prog (to_be_cleared_fb before pt) st) (pc … st) 
    170       (last_pop … st)
    171   | Error e ⇒ dummy_state_pc
    172   ].
    173 
    174 definition sigma_sb_state_pc:
    175  fixpoint_computer → coloured_graph_computer → 
    176   ertl_program → list (Σb:block.block_region b=Code) → 
    177   (block → list register) → lbl_funct_type →
    178   regs_funct_type →  state_pc LTL_semantics → state_pc ERTL_semantics ≝
    179  λfix_comp,build,prog,cs,init_regs,f_lbls,f_regs,st.
    180   let init ≝ (λglobals,fn.«translate_data fix_comp build globals fn,?») in
    181   let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
    182   let stacksizes ≝ lookup_stack_cost … m in 
    183   let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
    184   let globals ≝ prog_names … prog in
    185   match fetch_internal_function … ge (pc_block (pc … st)) with
    186   [ OK y ⇒ 
    187      let pt ≝ point_of_pc ERTL_semantics (pc ? st) in
    188      let after ≝ (analyse_liveness fix_comp (prog_names … prog) (\snd y)) in
    189      let coloured_graph ≝ build … (\snd y) after in
    190      mk_state_pc ? (sigma_sb_state cs prog
    191                        (to_be_cleared_sb … coloured_graph pt) st) (pc … st) 
    192                    (sigma_stored_pc ERTL_semantics LTL_semantics
    193                       prog stacksizes init init_regs f_lbls f_regs (last_pop … st))
    194   | Error e ⇒ dummy_state_pc
    195   ].
    196 @hide_prf % qed.
    197 
    198 definition state_rel : fixpoint_computer → coloured_graph_computer →
    199 ertl_program → joint_state_relation ERTL_semantics LTL_semantics ≝
    200 λfix_comp,build,prog,pc,st1,st2.
    201 let m ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
    202 let stacksizes ≝ lookup_stack_cost … m in 
    203 let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
    204 ∃f,fn.fetch_internal_function … ge (pc_block pc)
    205 = return 〈f,fn〉 ∧
    206 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
    207 let before ≝ livebefore … fn after in
    208 let coloured_graph ≝ build … fn after in
    209 match st_frms … st1 with
    210 [ None ⇒ False
    211 | Some frames ⇒
    212  (sigma_fb_state prog (to_be_cleared_fb before (point_of_pc ERTL_semantics pc)) st1) =
    213   (sigma_sb_state (get_ertl_call_stack frames) prog
    214    (to_be_cleared_sb … coloured_graph (point_of_pc ERTL_semantics pc)) st2)
    215 ].
    216 
    217 definition state_pc_rel :
    218 fixpoint_computer → coloured_graph_computer → 
    219   ertl_program → (block → list register) → lbl_funct_type →
    220   regs_funct_type →  joint_state_pc_relation ERTL_semantics LTL_semantics ≝
    221  λfix_comp,build,prog,init_regs,f_lbls,f_regs,st1,st2.
    222 match st_frms … (st_no_pc … st1) with
    223 [ None ⇒ False
    224 | Some frames ⇒
    225    sigma_fb_state_pc fix_comp build prog st1 =
    226     sigma_sb_state_pc fix_comp build prog (get_ertl_call_stack frames) init_regs
    227      f_lbls f_regs st2
    228 ].
    229 
    230 axiom insensitive_to_be_cleared_sb :
    231  ∀prog. ∀tb : local_clear_sb_type. ∀st : state LTL_LIN_state.
    232   ∀d : decision.∀bv,st',localss,cs.tb d →
    233   write_decision localss d bv st = return st' →
    234    sigma_sb_state cs prog tb st =
    235     sigma_sb_state cs prog tb st'.
    236    
    237 lemma hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.∀localss.
    238 ∀st : state LTL_LIN_state.
    239 ∀st'. (write_decision localss r bv st) = return st' →
    240 hw_reg_retrieve (regs … st') r = return bv.
    241 #r #bv #localss #st #st' whd in match write_decision; normalize nodelta
    242 whd in match hw_reg_store; normalize nodelta >m_return_bind
    243 whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    244 whd in match hw_reg_retrieve; normalize nodelta @eq_f
    245 whd in match hwreg_retrieve; whd in match hwreg_store; normalize nodelta
    246 @lookup_insert_hit
    247 qed.
    248138
    249139definition sigma_beval : fixpoint_computer → coloured_graph_computer → 
     
    262152  @hide_prf % qed.
    263153
    264 axiom ps_reg_retrieve_hw_reg_retrieve_commute :
     154definition state_rel : fixpoint_computer → coloured_graph_computer →
     155ertl_program →  (block → list register) → lbl_funct_type → regs_funct_type →
     156joint_state_relation ERTL_semantics LTL_semantics ≝
     157λfix_comp,build,prog,init_regs,f_lbls,f_regs,pc,st1,st2.
     158let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
     159let stacksizes ≝ lookup_stack_cost … m1 in 
     160let ge ≝ joint_globalenv ERTL_semantics prog stacksizes in
     161∃f,fn.fetch_internal_function … ge (pc_block pc)
     162= return 〈f,fn〉 ∧
     163let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
     164let before ≝ livebefore … fn after in
     165let coloured_graph ≝ build … fn after in
     166let R ≝ λbv1,bv2.bv2 = sigma_beval fix_comp build prog init_regs f_lbls f_regs bv1 in
     167let live_fun ≝ λv.lives v (before (point_of_pc ERTL_semantics pc)) in
     168match st_frms … st1 with
     169[ None ⇒ False
     170| Some frames ⇒
     171   mem_relation R (m … st1) (m … st2) ∧
     172   frames_relation fix_comp build prog R frames 〈regs … st2,m … st2〉 ∧
     173   hw_relation live_fun R (\snd (regs … st1)) (regs … st2) ∧
     174   make_is_relation_from_beval R (istack … st1) (istack … st2) ∧
     175   (live_fun (inr ?? RegisterCarry) → carry … st1 = carry … st2) ∧
     176   ∃ptr.sp … st2 = return ptr ∧
     177    ps_relation (joint_if_local_stacksize … fn) live_fun (colouring … coloured_graph)
     178     R ptr (\fst (regs … st1)) 〈regs … st2,m … st2〉
     179].
     180
     181definition state_pc_rel :
     182fixpoint_computer → coloured_graph_computer → 
     183  ertl_program → (block → list register) → lbl_funct_type →
     184  regs_funct_type →  joint_state_pc_relation ERTL_semantics LTL_semantics ≝
     185λfix_comp,build,prog,init_regs,f_lbls,f_regs,st1,st2.
     186let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp build prog))) in
     187let stacksizes ≝ lookup_stack_cost … m1 in 
     188let init ≝ (λglobals,fn.«translate_data fix_comp build globals fn,?») in
     189 state_rel fix_comp build prog init_regs f_lbls f_regs (pc … st1) st1 st2 ∧
     190 pc … st1 = pc … st2 ∧
     191 (last_pop … st2 = sigma_stored_pc ERTL_semantics LTL_semantics prog stacksizes
     192                    init init_regs f_lbls f_regs (last_pop … st1)).
     193@hide_prf % qed.
     194   
     195lemma hw_reg_retrieve_write_decision_hit : ∀r : Register.∀bv : beval.∀localss.
     196∀st : state LTL_LIN_state.
     197∀st'. (write_decision localss r bv st) = return st' →
     198hw_reg_retrieve (regs … st') r = return bv.
     199#r #bv #localss #st #st' whd in match write_decision; normalize nodelta
     200whd in match hw_reg_store; normalize nodelta >m_return_bind
     201whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     202whd in match hw_reg_retrieve; normalize nodelta @eq_f
     203whd in match hwreg_retrieve; whd in match hwreg_store; normalize nodelta
     204@lookup_insert_hit
     205qed.
     206
     207lemma ps_reg_retrieve_hw_reg_retrieve_commute :
    265208∀fix_comp,colour,prog,init_regs,f_lbls,f_regs,fn,pc.
    266209let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
    267210gen_preserving2 ?? gen_res_preserve ??????
    268      (state_rel fix_comp colour prog pc)
     211     (state_rel fix_comp colour prog init_regs f_lbls f_regs pc)
    269212     (λr : register.λd : arg_decision.d =
    270213      (colouring … (colour (prog_names … prog) fn after)
     
    274217     (λst,d.m_map Res ?? (\fst …)
    275218      (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
     219xxxxxxxxxxxxxx
    276220     
    277221(*set_theoretical axioms *)
Note: See TracChangeset for help on using the changeset viewer.