Changeset 3261


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

reverted joint_semantics rtl_semantics and ltl_semantics

Location:
src
Files:
5 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
  • src/LIN/joint_LTL_LIN_semantics.ma

    r3259 r3261  
    11include "LIN/joint_LTL_LIN.ma".
    22include "joint/semanticsUtils.ma".
    3 
     3 
    44definition hw_reg_store ≝ λr,v,e. OK … (hwreg_store r v e).
    55definition hw_reg_retrieve ≝ λl,r. OK … (hwreg_retrieve l r).
     
    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

    r3259 r3261  
    2222
    2323*)
    24 
     24 
    2525record reg_sp : Type[0] ≝
    2626{ reg_sp_env :> identifier_map RegisterTag beval
     
    241241        return reg_sp_store dest v env)
    242242      (λ_.rtl_save_frame)
    243       (λ_.λ_.λn,p,a.λ_.λst.rtl_setup_call_separate n p a st)
     243      rtl_setup_call_separate
    244244      rtl_fetch_external_args
    245245      rtl_set_result
     
    265265        return reg_sp_store dest v env)
    266266      (λ_.rtl_save_frame)
    267       (λ_.λ_.λn,p,a.λ_.λst.rtl_setup_call_separate_overflow n p a st)
     267      rtl_setup_call_separate_overflow
    268268      rtl_fetch_external_args
    269269      rtl_set_result
     
    289289        return reg_sp_store dest v env)
    290290      (λ_.rtl_save_frame)
    291       (λ_.λ_.λn,p,a.λ_.λst.rtl_setup_call_unique n p a st)
     291      rtl_setup_call_unique
    292292      rtl_fetch_external_args
    293293      rtl_set_result
  • src/joint/joint_semantics.ma

    r3259 r3261  
    66include "ASM/I8051bis.ma".
    77include "common/extraGlobalenvs.ma".
    8 
     8 
    99(* CSC: external functions never fail (??) and always return something of the
    1010   size of one register, both in the frontend and in the backend.
     
    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 : ∀globals.∀ge : genv_gen F globals.nat → paramsT … uns_pars → call_args uns_pars → ident →
     223  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
    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 … ge … stack_size (joint_if_params … globals fn) args i st ;
     587! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ;
    588588return increment_stack_usage … stack_size st'.
    589589
Note: See TracChangeset for help on using the changeset viewer.