Changeset 3259


Ignore:
Timestamp:
May 9, 2013, 12:49:38 AM (4 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

Location:
src
Files:
8 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 *)
  • src/ERTL/ERTL_semantics.ma

    r2946 r3259  
    3434definition set_hwsp : ertl_reg_env → xpointer → ertl_reg_env ≝
    3535 λst,sp.〈\fst st, hwreg_store_sp (\snd st) sp〉.
     36 
     37record ERTL_frame : Type[0] ≝
     38{ psd_reg_env : register_env beval
     39; funct_block : Σb:block.block_region b=Code
     40; callee_values : Σl : list beval. |l| = |RegisterCalleeSaved|
     41}.
    3642
    3743definition ERTL_state : sem_state_params ≝
    3844  mk_sem_state_params
    39  (* framesT ≝ *) (list (register_env beval × (Σb:block.block_region b=Code)))
     45 (* framesT ≝ *) (list (ERTL_frame))
    4046 (* empty_framesT ≝ *) [ ]
    4147 (* regsT ≝ *) ertl_reg_env
     
    4652(* we ignore need_spilled_no as we never move framesize based values around in the
    4753   translation *)
    48 definition ertl_eval_move ≝ λenv,pr.
     54definition ertl_eval_move ≝ λenv.λpr : move_dst × move_src.
    4955      ! v ←
    5056        match \snd pr with
     
    6975  ! st' ← push_ra … st (pc … st) ;
    7076  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
     77  let callee_val ≝ map … (λr.hwreg_retrieve (\snd (regs …  st')) r)
     78                    RegisterCalleeSaved in
    7179  return
    7280  (set_frms ERTL_state
    73   (〈\fst (regs ERTL_state st'),(pc_block (pc ? st))〉 :: frms)
     81  ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc_block (pc ? st))
     82      «callee_val,length_map … ») :: frms)
    7483    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    7584
     85definition callee_values_ok : hw_register_env →
     86   (Σl : list beval.|l| = |RegisterCalleeSaved|) → bool ≝
     87λregs,l.
     88foldl … andb true
     89 (map2 … (λr : Register.λbv :beval.eq_beval (hwreg_retrieve regs r) bv)
     90  RegisterCalleeSaved l ?).
     91@hide_prf >(pi2 … l) % qed.
     92
     93
    7694definition ertl_pop_frame:
    77  state ERTL_state →
     95 ∀F. ∀globals. genv_gen F globals → ident →  state ERTL_state →
    7896   res (state ERTL_state × program_counter) ≝
    79  λst.
     97 λF,globals,ge,id,st.
    8098 ! frms ← opt_to_res ? [MSG FrameErrorOnPop] (st_frms … st);
    8199 match frms with
    82100 [ nil ⇒ Error ? [MSG FramesEmptyOnPop]
    83101 | cons hd tl ⇒
    84    let 〈local_mem, bl〉 ≝ hd in
    85    let st' ≝ set_regs ERTL_state 〈local_mem, \snd (regs … st)〉
    86       (set_frms ERTL_state tl st) in
    87    ! 〈st'', pc〉 ← pop_ra … st' ;
    88    if eq_block bl (pc_block pc) then
    89      OK … 〈st'', pc〉
    90    else Error ? [MSG BlockInFramesCorrupted]
     102   if callee_values_ok (\snd (regs … st)) (callee_values hd) then
     103    let st' ≝ set_regs ERTL_state 〈(psd_reg_env hd), \snd (regs … st)〉
     104       (set_frms ERTL_state tl st) in
     105    ! 〈st'', pc〉 ← pop_ra … st' ;
     106    if eq_block (funct_block hd) (pc_block pc) then
     107      ! sp ← sp … st'' ;
     108      ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
     109      let framesize : Byte ≝ bitvector_of_nat 8 framesize in
     110      let newsp ≝ shift_pointer … sp framesize in
     111      OK … 〈set_sp … newsp st'', pc〉
     112    else Error ? [MSG BlockInFramesCorrupted]
     113   else Error ? [MSG BadRegister]
    91114 ].
     115@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
    92116
    93117(*CSC: XXXX, for external functions only*)
     
    112136  return set_regs ERTL_state env' st.
    113137
     138
     139definition ertl_setup_call : ∀F. ∀globals. genv_gen F globals →
     140ident → state ERTL_state → res (state ERTL_state) ≝
     141λF,globals,ge,id,st.
     142  ! sp ← sp … st ;
     143  ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
     144  let framesize : Byte ≝ bitvector_of_nat 8 framesize in
     145  let newsp ≝ neg_shift_pointer … sp framesize in
     146  return set_sp … newsp st.
     147@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
     148 
     149definition eval_ertl_seq:
     150 ∀F. ∀globals. genv_gen F globals →
     151  ertl_seq → ident → state ERTL_state →
     152   res (state ERTL_state) ≝
     153 λF,globals,ge,stm,id,st.
     154 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
     155 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
     156   match stm with
     157   [ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st].
     158   
     159(*
    114160definition eval_ertl_seq:
    115161 ∀F. ∀globals. genv_gen F globals →
     
    129175      return set_sp … newsp st
    130176   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
    131    ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
     177   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.  *)
    132178
    133179definition ERTL_sem_uns ≝ 
     
    149195  (* pair_reg_move_     ≝ *) ertl_eval_move
    150196  (* save_frame         ≝ *) ertl_save_frame
    151   (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
     197  (* setup_call         ≝ *) (λgl,ge.λ_.λ_.λ_.λid,st.ertl_setup_call F gl ge id st)
    152198  (* fetch_external_args≝ *) ertl_fetch_external_args
    153199  (* set_result         ≝ *) ertl_set_result
     
    157203     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
    158204  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
    159   (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.ertl_pop_frame).
     205  (* pop_frame          ≝ *) (λglobals,ge,id.λ_.λst.ertl_pop_frame F globals ge id st).
    160206
    161207definition ERTL_semantics ≝
  • src/LIN/joint_LTL_LIN_semantics.ma

    r3037 r3259  
    8686  (* allocate_local     ≝ *) (λabs.match abs in void with [ ])
    8787*)  (* save_frame         ≝ *) LTL_LIN_save_frame
    88   (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
     88  (* setup_call         ≝ *) (λ_.λ_.λ_.λ_.λ_.λ_.λst.return st)
    8989  (* fetch_external_args≝ *) ltl_lin_fetch_external_args
    9090  (* set_result         ≝ *) ltl_lin_set_result
  • src/RTL/RTL_semantics.ma

    r2958 r3259  
    241241        return reg_sp_store dest v env)
    242242      (λ_.rtl_save_frame)
    243       rtl_setup_call_separate
     243      (λ_.λ_.λn,p,a.λ_.λst.rtl_setup_call_separate n p a st)
    244244      rtl_fetch_external_args
    245245      rtl_set_result
     
    265265        return reg_sp_store dest v env)
    266266      (λ_.rtl_save_frame)
    267       rtl_setup_call_separate_overflow
     267      (λ_.λ_.λn,p,a.λ_.λst.rtl_setup_call_separate_overflow n p a st)
    268268      rtl_fetch_external_args
    269269      rtl_set_result
     
    289289        return reg_sp_store dest v env)
    290290      (λ_.rtl_save_frame)
    291       rtl_setup_call_unique
     291      (λ_.λ_.λn,p,a.λ_.λst.rtl_setup_call_unique n p a st)
    292292      rtl_fetch_external_args
    293293      rtl_set_result
  • src/common/ByteValues.ma

    r2927 r3259  
    277277  [ BBbit b ⇒ OK … b
    278278  | _ ⇒ Error … [MSG err]].
     279
     280definition eq_option_map : ∀A: Type[0].(A → A → bool) → option A → option A → bool ≝
     281λA,eq,a1,a2.
     282match a1 with
     283[ Some x ⇒ match a2 with [Some y ⇒ eq x y | _ ⇒ false ]
     284| None ⇒ match a2 with [None ⇒ true | _ ⇒ false]
     285].
     286
     287lemma eq_option_map_elim : ∀A : Type[0].∀P:bool → Prop.∀eq,
     288x,y. (∀P:bool → Prop.∀z,w.(z = w → P true) → (z ≠w → P false) → P (eq z w)) →
     289(x = y → P true) → (x ≠ y → P false) → P (eq_option_map A eq x y).
     290#A #P #eq * [|#x] * [1,3:|*: #y] normalize #H #H1 #H2
     291[@H1 % |2,3: @H2 % #EQ destruct(EQ)] @H
     292[ #EQ @H1 >EQ %
     293| * #H3 @H2 % #EQ destruct @H3 %
     294]
     295qed.
     296
     297
     298definition eq_beval : beval → beval → bool ≝
     299λbv1,bv2.
     300match bv1 with
     301[ BVundef ⇒ match bv2 with [ BVundef ⇒ true | _ ⇒ false ]
     302| BVnonzero ⇒ match bv2 with [ BVnonzero ⇒ true | _ ⇒ false ]
     303| BVXor pt1 pt1' p1 ⇒
     304  match bv2 with
     305  [ BVXor pt2 pt2' p2 ⇒ eq_option_map … eq_pointer pt1 pt2 ∧
     306                        eq_option_map … eq_pointer pt1' pt2' ∧
     307                        eqb (part_no … p1) (part_no … p2)
     308  | _ ⇒ false
     309  ]
     310| BVByte b1 ⇒ match bv2 with [ BVByte b2 ⇒ eq_bv … b1 b2 | _ ⇒ false]
     311| BVnull p1 ⇒ match bv2 with
     312              [ BVnull p2 ⇒ eqb (part_no … p1) (part_no … p2) | _ ⇒ false ]
     313| BVptr ptr1 p1 ⇒ match bv2 with
     314                 [ BVptr ptr2 p2 ⇒ eq_pointer ptr1 ptr2 ∧
     315                                   eqb (part_no … p1) (part_no … p2)
     316                 | _ ⇒ false
     317                 ]
     318| BVpc pc1 p1 ⇒ match bv2 with
     319                [ BVpc pc2 p2 ⇒ eq_program_counter pc1 pc2 ∧
     320                  eqb (part_no … p1) (part_no … p2)
     321                | _⇒ false
     322                ]
     323].
     324
     325lemma eq_beval_elim : ∀P:bool → Prop.∀x,y.
     326(x = y → P true) → (x ≠ y → P false) → P (eq_beval x y).
     327#P *
     328[|| #pt1 #pt1' #p1 | #b1 | #p1 | #ptr1 #p1 | #pc1 #p1 ]
     329*
     330[1,8,15,22,29,36,43:
     331|2,9,16,23,30,37,44:
     332|3,10,17,24,31,38,45: #pt2 #pt2' #p2
     333|4,11,18,25,32,39,46: #b2
     334|5,12,19,26,33,40,47: #p2
     335|6,13,20,26,34,41,48: #ptr2 #p2
     336|*: #pc2 #p2
     337]
     338normalize nodelta #H1 #H2 try(@H1 %) try(@H2 % #EQ destruct)
     339whd in match eq_beval; normalize nodelta
     340[ @eq_option_map_elim
     341 [ @eq_pointer_elim
     342 |3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H %
     343 | normalize nodelta #EQ destruct(EQ) @eq_option_map_elim
     344 [ @eq_pointer_elim
     345 |3: * #H whd in match (andb ??); @H2 % #EQ destruct(EQ) @H %
     346 | #EQ destruct(EQ) cases p1 in H1 H2; -p1 cases p2 -p2
     347   #p2 #prf #p1 #prf1 #H1 #H2 @eqb_elim
     348  [ #EQ destruct(EQ) @H1 %
     349  | * #H @H2 % #EQ destruct(EQ) @H %
     350  ]
     351 ]
     352 ]
     353| @eq_bv_elim [#EQ destruct(EQ) @H1 % | * #H @H2 % #EQ destruct(EQ) @H %]
     354| cases p1 in H1 H2; -p1 cases p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
     355 [ #EQ destruct(EQ) @H1 %
     356 | * #H @H2 % #EQ destruct @H %
     357 ]
     358| @eq_pointer_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct(EQ)
     359  cases p1 in H1 H2; -p1 cases p2 -p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
     360  [#EQ destruct @H1 %
     361  | * #H @H2 % #EQ destruct @H %
     362  ]
     363| @eq_program_counter_elim [2: * #H @H2 % #EQ destruct @H %] #EQ destruct
     364  cases p1 in H1 H2; -p1 cases p2 -p2 #p2 #prf2 #p1 #prf1 #H1 #H2 @eqb_elim
     365  [ #EQ destruct @H1 %
     366  | * #H @H2 % #EQ destruct @H %
     367  ]
     368]
     369qed.
  • src/common/ExtraIdentifiers.ma

    r3217 r3259  
    2121[//] #i #IH #f #b @IH
    2222qed.
    23    
     23
     24let rec pm_clean (A : Type[0]) (p : positive_map A) on p : positive_map A ≝
     25match p with
     26[ pm_leaf ⇒ pm_leaf A
     27| pm_node a l r ⇒ let l' ≝ pm_clean A l in
     28                  let r' ≝ pm_clean A r in
     29                  if andb (is_none ? a)
     30                      (andb (is_pm_leaf ? l') (is_pm_leaf ? r')) then
     31                     pm_leaf A
     32                  else
     33                     pm_node ? a l' r'
     34].
     35 
     36lemma lookup_pm_clean : ∀A : Type[0].∀p,p' : positive_map A.
     37(∀i.lookup_opt A i p = lookup_opt A i p') →
     38pm_clean A p = pm_clean A p'.
     39#A #p elim p
     40[ #p' elim p' [ #_ normalize %] * [2: #a] #l #r #IHl #IHr #H normalize
     41  [ lapply(H one) normalize #EQ destruct]
     42  <IHl [2,4: #i lapply(H (p0 i)) normalize //] normalize
     43  <IHr [2,4: #i lapply(H (p1 i)) normalize //] %
     44| #opt_a #l #r #IHl #IHr *
     45  [ #H normalize lapply(H one) normalize #EQ destruct(EQ) normalize
     46    >(IHl (pm_leaf ?)) [2: #i lapply(H (p0 i)) normalize //] normalize
     47    >(IHr (pm_leaf ?)) [2: #i lapply(H (p1 i)) normalize //] %
     48  | #opt_a' #l' #r' #H normalize lapply(H one) normalize #EQ destruct(EQ)
     49    >(IHl l') [2: #i lapply(H (p0 i)) normalize //]
     50    >(IHr r') [2: #i lapply(H (p1 i)) normalize //] %
     51  ]
     52]
     53qed. 
     54
     55definition pm_find_all : ∀A : Type[0].positive_map A →
     56(Pos → A → bool) → positive_map A ≝
     57λA,p,P.fold ??
     58 (λi,a,p'.if P i a then pm_set ? i (Some ? a) p' else p') p (pm_leaf A).
     59 
     60
     61lemma pm_clean_idempotent : ∀A : Type[0].∀p : positive_map A.
     62pm_clean ? p = pm_clean ? (pm_clean ? p).
     63cases daemon
     64qed.
     65
     66 
     67lemma pm_find_all_canonic : ∀A : Type[0].∀p : positive_map A.∀P.
     68pm_find_all A p P = pm_clean A (pm_find_all A p P).
     69#A #p #P whd in match pm_find_all; normalize nodelta
     70@pm_fold_ind
     71[ %] #i #ps #a #b #H #H1 #H2 cases(P i a) normalize
     72[2: assumption] lapply H2 lapply b elim i
     73[ normalize * [ #_ %] #opt_a #l #r
     74  normalize nodelta normalize cases opt_a
     75  [2: #a1 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?);
     76      >e1 in ⊢ (??%?); % ] normalize
     77  cases(pm_clean ? l) normalize [2: #opt_a1 #l1 #r1
     78  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?); %]
     79  cases(pm_clean ? r) normalize [#EQ destruct] #opt_a1 #l1 #r1
     80  #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct %
     81|*: #x #IH * normalize
     82   [1,3: #_ <IH [2,4: % ]
     83    inversion(pm_set A x ??) [2,4: #opt_a1 #l1 #r1 #_#_#_ %]
     84    #ABS @⊥ cases x in ABS; [1,4: normalize #EQ destruct] #x1 normalize
     85    #EQ destruct
     86   |*: * [2,4: #a1] #l #r normalize
     87       [1,2: #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct >e0 in ⊢ (??%?);
     88             >e1 in ⊢ (??%?); <IH
     89             [ @eq_f3 try % >e1 in ⊢ (???%); %
     90             | assumption
     91             | @eq_f3 try % @pm_clean_idempotent
     92             | @pm_clean_idempotent
     93             ]
     94       |*: inversion(pm_clean A l) normalize
     95           [ #H3 inversion(pm_clean A r) normalize [#_ #EQ destruct] #opt_a1 #l1 #r1
     96             #_ #_ #H4 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ  <(IH r)
     97             [2: cut(r = pm_node A opt_a1 l1 r1) [ destruct %] #H5
     98             >H5 in ⊢ (??%?); <H4 % ] inversion(pm_set A x ??)
     99             [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %]
     100             #ABS @⊥ cases x in ABS; normalize cases r normalize
     101             [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
     102             #EQ1 destruct
     103           | #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     104             <(IH r) [destruct %] destruct assumption
     105           | #H3 cases(pm_clean A r) normalize [#EQ destruct] #opt_a1 #l1 #r1
     106              #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ <(IH l) [2: >H3 destruct %]
     107              inversion(pm_set A x ??)
     108              [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct %]
     109              #ABS @⊥ cases x in ABS; normalize cases l normalize
     110              [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
     111              #EQ1 destruct
     112           | #opt_a1 #l1 #r1 #_ #_ #H3 #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ
     113             <(IH l) [2: >H3 destruct %] inversion(pm_set A x ??)
     114              [2: #opt_a2 #l2 #r2 #_ #_ #_ normalize destruct >e0 in ⊢ (??%?); %]
     115              #ABS @⊥ cases x in ABS; normalize cases l normalize
     116              [| #z #w1 #w2| #x1 | #z #w1 #w2 #x1 | #x1 | #z #w1 #w2 #x1 ]
     117              #EQ1 destruct
     118           ] 
     119       ]   
     120   ]
     121]
     122qed. 
     123
    24124
    25125definition find_all : ∀tag,A. identifier_map tag A →
    26126(identifier tag → A → bool) → identifier_map tag A ≝
    27 λtag,A,m,P.foldi A (identifier_map tag A) tag
    28 (λi,a,l.if (P i a) then (add tag A l i a) else l) m (empty_map tag A).
    29 
     127λtag,A,m,P.match m with
     128  [an_id_map p ⇒ an_id_map ?? (pm_find_all A p (λx,a.P (an_identifier tag x) a))].
     129(*
    30130
    31131lemma find_all_lookup_predicate : ∀tag,A.∀m : identifier_map tag A.
     
    33133lookup tag A (find_all tag A m P) i = Some ? a →
    34134lookup tag A m i = Some ? a  ∧ (bool_to_Prop (P i a)).
    35 #tag #A #m #P #i #a whd in match find_all; normalize nodelta @foldi_ind
     135#tag #A * #m #P * #i #a whd in match find_all; normalize @pm_fold_ind
    36136[ normalize #EQ destruct
    37 | #k #ks #a1 #b * #H #H1 #H2 inversion(P k a1)
    38   [ #H3 normalize nodelta >H3
    39     cut(bool_to_Prop (eq_identifier tag i k) ∨
     137| #k #ks #a1 #b * #H #H1 #H2 inversion(P (an_identifier tag i) a1)
     138  [ cases(decidable_eq_pos i k)
     139    [#EQ destruct #H3 >H3 in H2; normalize >looku
     140
     141
     142  [#EQ destruct inversion(
     143
     144  [ #H3 normalize nodelta >H3 cases(decidable_eq_pos i k)
     145    [ #EQ destruct >H3 in H2;
     146 
     147 
     148    cut(bool_to_Prop (eq_identifier tag (an_identifier tag i) (an_identifierk) ∨
    40149     (bool_to_Prop (notb (eq_identifier tag i k))))
    41150    [@eq_identifier_elim #_ [ %%|%2 %]]
     
    68177]
    69178qed.
    70 
     179*)
    71180(*
    72181 whd in match (add ?????); whd in match (add ?????); normalize nodelta
  • src/joint/StatusSimulationUtils.ma

    r3154 r3259  
    419419  ∀n.stack_sizes f1 = return n → 
    420420  ∀st1'.
    421   setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' →
     421  setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … n (joint_if_params … fn1)
     422   arg f1 st1_pre = return st1' →
    422423  st_rel st1 st2 → 
    423424  ∀t_fn1.
     
    444445         (mk_state_pc ? st2_pre_call pc' (last_pop … st2)) = return st2_pre ∧
    445446       ∃st2_after_call.
    446          setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre
     447         setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) … n
     448          (joint_if_params … t_fn1) arg' f1 st2_pre
    447449          = return st2_after_call ∧
    448450       bind_new_P' ??
     
    515517   ∀ssize_f1.stack_sizes f1 = return ssize_f1 →   
    516518   ∀st1'.
    517     setup_call ?? P_in ssize_f1 (joint_if_params … fn1) arg
     519    setup_call ?? P_in … (joint_globalenv P_in prog stack_sizes) … ssize_f1
     520     (joint_if_params … fn1) arg f1
    518521     (decrement_stack_usage P_in ssize_f (st_no_pc … st1)) = return st1' →
    519522   st_rel st1 st2 → 
     
    533536         st2_pre_call = return bl ∧
    534537       ∃st2_after.
    535         setup_call ?? P_out ssize_f1 (joint_if_params … t_fn1) arg'
     538        setup_call ?? P_out … (joint_globalenv P_out trans_prog stack_sizes) …
     539         ssize_f1 (joint_if_params … t_fn1) arg' f1
    536540         (decrement_stack_usage P_out ssize_f st2_pre_call) = return st2_after ∧
    537541       bind_new_P' ??
  • src/joint/joint_semantics.ma

    r3154 r3259  
    221221   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
    222222     type of arguments. To be fixed using a dependent type *)
    223   ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
     223  ; setup_call : ∀globals.∀ge : genv_gen F globals.nat → paramsT … uns_pars → call_args uns_pars → ident →
    224224      state st_pars → res (state st_pars)
    225225  ; fetch_external_args: external_function → state st_pars → call_args … uns_pars →
     
    585585λst : state p.
    586586! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ;
    587 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
     587! st' ← setup_call … ge … stack_size (joint_if_params … globals fn) args i st ;
    588588return increment_stack_usage … stack_size st'.
    589589
Note: See TracChangeset for help on using the changeset viewer.