Changeset 3261 for src/ERTL


Ignore:
Timestamp:
May 9, 2013, 11:12:07 AM (7 years ago)
Author:
piccolo
Message:

reverted joint_semantics rtl_semantics and ltl_semantics

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTLProof.ma

    r3259 r3261  
    110110 ∀fn : joint_closed_internal_function ERTL (prog_names … prog). ∀l.
    111111 let after ≝ analyse_liveness fix_comp (prog_names … prog) fn in
    112   ¬ lives (inr ? ? RegisterA) (livebefore  … fn after l).
     112  ¬ in_lattice (inr ? ? RegisterA) (livebefore  … fn after l).
    113113(*
    114114axiom dead_registers_in_dead :
     
    164164let before ≝ livebefore … fn after in
    165165let coloured_graph ≝ build … fn after in
    166 let R ≝ λbv1,bv2.bv2 = sigma_beval fix_comp build prog init_regs f_lbls f_regs bv1 in
    167 let live_fun ≝ λv.lives v (before (point_of_pc ERTL_semantics pc)) in
     166let R ≝ λbv1,bv2.bv1 = sigma_beval fix_comp build prog init_regs f_lbls f_regs bv2 in
     167let live_fun ≝ λv.in_lattice v (before (point_of_pc ERTL_semantics pc)) in
    168168match st_frms … st1 with
    169169[ None ⇒ False
     
    205205qed.
    206206
     207
    207208lemma ps_reg_retrieve_hw_reg_retrieve_commute :
    208 ∀fix_comp,colour,prog,init_regs,f_lbls,f_regs,fn,pc.
    209 let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
     209∀fix_comp,colour,prog,init_regs,f_lbls,f_regs.∀f : ident.
     210∀fn : joint_closed_internal_function ERTL (prog_names … prog).
     211∀pc.
     212let m1 ≝ (\snd (\fst (ertl_to_ltl fix_comp colour prog))) in
     213let stacksizes ≝ lookup_stack_cost … m1 in 
     214let after ≝ (analyse_liveness fix_comp (prog_names … prog) fn) in
     215fetch_internal_function … (joint_globalenv ERTL_semantics prog stacksizes)
     216(pc_block pc) = return 〈f,fn〉 → 
    210217gen_preserving2 ?? gen_res_preserve ??????
    211218     (state_rel fix_comp colour prog init_regs f_lbls f_regs pc)
    212      (λr : register.λd : arg_decision.d =
     219     (λr :Σr : register.bool_to_Prop(in_lattice (inl ?? r)
     220       (livebefore … fn after (point_of_pc ERTL_semantics pc))).λd : decision.d =
    213221      (colouring … (colour (prog_names … prog) fn after)
    214222       (inl register Register r)))
     
    217225     (λst,d.m_map Res ?? (\fst …)
    218226      (read_arg_decision (joint_if_local_stacksize ?? fn) st d)).
    219 xxxxxxxxxxxxxx
     227#fix_comp #colour #prog #init_regs #f_lbls #f_regs #f #fn #pc #EQfn #st1 #st2
     228* #r #Hr #d whd in match state_rel; normalize nodelta * #f1 * #fn1
     229>EQfn * whd in ⊢ (??%% → ?); #EQ destruct(EQ) inversion(st_frms … st1)
     230[#_ *] #frames #EQframes normalize nodelta ***** #Hmem #Hrames #Hw_relation
     231#His #Hcarry * #ptr * #EQptr whd in match ps_relation; whd in match gen_preserving;
     232normalize nodelta #H #EQd #bv #EQbv cases(H «r,Hr» d ? bv EQbv)
     233[2: <EQd in ⊢ (??%?); %] #bv' cases d
     234[2: #R normalize nodelta * whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     235    change with (hwreg_retrieve ??) in match (lookup ?????);
     236    #Hrel %{(hwreg_retrieve (regs … st2) R)} %
     237    [ whd in match m_map; whd in match read_arg_decision; normalize nodelta %]
     238    assumption ]
     239xxxxxxxxxxxx
     240
     241[ #R whd in match ps_relation; normalize nodelta whd in match gen_preserving;
     242normalize nodelta #H #EQR #bv #EQbv cases(H «r,Hr» R
    220243     
    221244(*set_theoretical axioms *)
  • src/ERTL/ERTL_semantics.ma

    r3259 r3261  
    3838{ psd_reg_env : register_env beval
    3939; funct_block : Σb:block.block_region b=Code
    40 ; callee_values : Σl : list beval. |l| = |RegisterCalleeSaved|
     40; callee_values : list beval
    4141}.
    4242
     
    8080  (set_frms ERTL_state
    8181  ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc_block (pc ? st))
    82       «callee_val,length_map … ») :: frms)
     82     callee_val) :: frms)
    8383    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
    8484
     
    137137
    138138
    139 definition ertl_setup_call : ∀F. ∀globals. genv_gen F globals →
    140 ident → state ERTL_state → res (state ERTL_state) ≝
    141 λF,globals,ge,id,st.
     139definition ertl_setup_call : ℕ → state ERTL_state → res (state ERTL_state) ≝
     140λframesize,st.
    142141  ! sp ← sp … st ;
    143   ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
    144142  let framesize : Byte ≝ bitvector_of_nat 8 framesize in
    145143  let newsp ≝ neg_shift_pointer … sp framesize in
Note: See TracChangeset for help on using the changeset viewer.