Ignore:
Timestamp:
Nov 8, 2012, 2:27:54 PM (8 years ago)
Author:
tranquil
Message:

changed joint's stack pointer and internal stack

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r2437 r2443  
    3333 ; empty_framesT: framesT
    3434 ; regsT : Type[0]
    35  ; empty_regsT: xpointer → regsT (* Stack pointer *)
     35 ; empty_regsT: xpointer → regsT (* initial stack pointer *)
     36 ; load_sp : regsT → res xpointer
     37 ; save_sp : regsT → xpointer → regsT
    3638 }.
     39
     40inductive internal_stack : Type[0] ≝
     41| empty_is : internal_stack
     42| one_is : beval → internal_stack
     43| both_is : beval → beval → internal_stack.
     44
     45axiom InternalStackFull : String.
     46axiom InternalStackEmpty : String.
     47
     48definition is_push : internal_stack → beval → res internal_stack ≝
     49λis,bv.match is with
     50[ empty_is ⇒ return one_is bv
     51| one_is bv' ⇒ return both_is bv' bv
     52| both_is _ _ ⇒ Error … [MSG … InternalStackFull]
     53].
     54
     55definition is_pop : internal_stack → res (beval × internal_stack) ≝
     56λis.match is with
     57[ empty_is ⇒ Error … [MSG … InternalStackEmpty]
     58| one_is bv' ⇒ return 〈bv', empty_is〉
     59| both_is bv bv' ⇒ return 〈bv', one_is bv〉
     60].
    3761
    3862record state (semp: sem_state_params): Type[0] ≝
    3963 { st_frms: framesT semp
    40  ; sp: xpointer
    41  ; isp: xpointer
     64 ; istack : internal_stack
    4265 ; carry: bebit
    4366 ; regs: regsT semp
     
    4568 }.
    4669
    47 coercion sem_state_params_to_state nocomposites:
    48   ∀p : sem_state_params.Type[0] ≝ state on _p : sem_state_params to Type[0].
     70definition sp ≝ λp,st.load_sp p (regs ? st).
    4971
    5072record state_pc (semp : sem_state_params) : Type[0] ≝
     
    5476
    5577definition set_m: ∀p. bemem → state p → state p ≝
    56  λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
     78 λp,m,st. mk_state p (st_frms …st) (istack … st) (carry … st) (regs … st) m.
    5779
    5880definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
    59  λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
     81 λp,regs,st.mk_state p (st_frms … st) (istack … st) (carry … st) regs (m … st).
    6082
    6183definition set_sp: ∀p. ? → state p → state p ≝
    62  λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
    63 
    64 definition set_isp: ∀p. ? → state p → state p ≝
    65  λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
     84 λp,sp,st.let regs' ≝ save_sp … (regs … st) sp in
     85 mk_state p (st_frms … st) (istack … st) (carry … st) regs' (m … st).
    6686
    6787definition set_carry: ∀p. bebit → state p → state p ≝
    68  λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
     88 λp,carry,st. mk_state … (st_frms … st) (istack … st) carry (regs … st) (m … st).
     89
     90definition set_istack: ∀p. internal_stack → state p → state p ≝
     91 λp,is,st. mk_state … (st_frms … st) is (carry … st) (regs … st) (m … st).
    6992
    7093definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
     
    7598
    7699definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
    77  λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
     100 λp,frms,st. mk_state … frms (istack … st) (carry … st) (regs … st) (m … st).
    78101
    79102axiom BadProgramCounter : String.
     
    111134  | FEnd2  : fin_step_flow p F Call. (* end flow *)
    112135
    113 record more_sem_unserialized_params
     136record sem_unserialized_params
    114137  (uns_pars : unserialized_params)
    115138  (F : list ident → Type[0]) : Type[1] ≝
    116   { st_pars :> sem_state_params (* automatic coercion has issues *)
     139  { st_pars :> sem_state_params
    117140  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
    118141  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
     
    129152  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
    130153  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
    131   ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
     154  ; fetch_ra: state st_pars → res (cpointer × (state st_pars))
    132155
    133156  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
     
    169192definition helper_def_retrieve :
    170193  ∀X : ? → ? → ? → Type[0].
    171   (∀up,F.∀p:more_sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
    172   ∀up,F.∀p : more_sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
     194  (∀up,F.∀p:sem_unserialized_params up F. regsT (st_pars up F p) → X up F p → res beval) →
     195  ∀up,F.∀p : sem_unserialized_params up F.state (st_pars up F p) → X up F p → res beval ≝
    173196    λX,f,up,F,p,st.f ?? p (regs … st).
    174197
    175198definition helper_def_store :
    176199  ∀X : ? → ? → ? → Type[0].
    177   (∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
    178   ∀up,F.∀p : more_sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
     200  (∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → regsT (st_pars … p) → res (regsT (st_pars … p))) →
     201  ∀up,F.∀p : sem_unserialized_params up F.X up F p → beval → state (st_pars … p) → res (state (st_pars … p)) ≝
    179202  λX,f,up,F,p,x,v,st.! r ← f ?? p x v (regs … st) ; return set_regs … r st.
    180203
     
    193216definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
    194217definition pair_reg_move ≝
    195   λup,F.λp : more_sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
     218  λup,F.λp : sem_unserialized_params up F.λst : state (st_pars … p).λpm : pair_move up.
    196219    ! r ← pair_reg_move_ ?? p (regs ? st) pm;
    197220    return set_regs ? r st.
    198 
    199221 
    200222axiom BadPointer : String.
     
    208230   serialization and on whether the call is a tail one. *)
    209231definition eval_call_block:
    210  ∀p,F.∀p':more_sem_unserialized_params p F.∀globals.
     232 ∀p,F.∀p':sem_unserialized_params p F.∀globals.
    211233  genv_t (fundef (F globals)) → state (st_pars ?? p') → block → call_args p → call_dest p →
    212234    IO io_out io_in ((step_flow p (F globals) Call)×(state (st_pars ?? p'))) ≝
     
    232254definition push: ∀p.state p → beval → res (state p) ≝
    233255 λp,st,v.
    234   let isp' ≝ isp ? st in
    235   do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
    236   let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
    237   return set_m … m (set_isp … isp'' st).
    238   normalize elim (isp p st) #p #H @H
    239 qed.
    240 
    241 definition pop: ∀p. state p → res ((state p ) × beval) ≝
     256 ! is ← is_push (istack … st) v ;
     257 return set_istack … is st.
     258
     259definition pop: ∀p. state p → res (beval × (state p)) ≝
    242260 λp,st.
    243   let isp' ≝ isp ? st in
    244   let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
    245   let ist ≝ set_isp … isp'' st in
    246   do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
    247   OK ? 〈ist,v〉.
    248   normalize elim (isp p st) #p #H @H
    249 qed.
     261 ! 〈bv, is〉 ← is_pop (istack … st) ;
     262 return 〈bv, set_istack … is st〉.
    250263
    251264definition save_ra : ∀p. state p → cpointer → res (state p) ≝
    252265 λp,st,l.
    253   ! 〈addrl,addrh〉 ← beval_pair_of_pointer l ; (* always succeeds *)
     266  let 〈addrl,addrh〉 ≝  beval_pair_of_pointer l in
    254267  ! st' ← push … st addrl;
    255268  push … st' addrh.
    256269
    257 definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
     270definition load_ra : ∀p.state p → res (cpointer × (state p)) ≝
    258271 λp,st.
    259   do 〈st',addrh〉 ← pop … st;
    260   do 〈st'',addrl〉 ← pop … st';
     272  do 〈addrh, st'〉 ← pop … st;
     273  do 〈addrl, st''〉 ← pop … st';
    261274  do pr ← pointer_of_address 〈addrh, addrl〉;
    262   match ptype pr return λx.ptype pr = x → res (? × cpointer) with
    263   [ Code ⇒ λprf.return 〈st'', «pr,prf»
     275  match ptype pr return λx.ptype pr = x → res (cpointer × ?) with
     276  [ Code ⇒ λprf.return 〈«pr,prf», st''
    264277  | _ ⇒ λ_.Error … [MSG BadPointer]
    265278  ] (refl …).
     
    267280(* parameters that are defined by serialization *)
    268281record more_sem_params (pp : params) : Type[1] ≝
    269   { msu_pars :> more_sem_unserialized_params pp (joint_closed_internal_function pp)
     282  { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp)
    270283  ; offset_of_point : code_point pp → option offset (* can overflow *)
    271284  ; point_of_offset : offset → code_point pp
     
    463476    return set_m … m' st
    464477  | ADDRESS id prf ldest hdest ⇒
    465     let addr ≝ opt_safe ? (find_symbol … ge id) ? in
    466     ! 〈laddr,haddr〉 ← beval_pair_of_pointer (mk_pointer addr zero_offset) ;
     478    let addr_block ≝ opt_safe ? (find_symbol … ge id) ? in
     479    let 〈laddr,haddr〉 ≝ beval_pair_of_pointer (mk_pointer addr_block zero_offset) in
    467480    ! st' ← dpl_store … ldest laddr st;
    468481    dph_store … hdest haddr st'
     
    488501    accb_store … dacc_b_reg v2' st'
    489502  | POP dst ⇒
    490     ! 〈st',v〉 ← pop p st;
     503    ! 〈v, st'〉 ← pop p st;
    491504    acca_store … p dst v st'
    492505  | PUSH src ⇒
     
    601614    do_call … ge st id fn args
    602615  | _ ⇒
    603     ! 〈st',ra〉 ← fetch_ra … st ;
     616    ! 〈ra, st'〉 ← fetch_ra … st ;
    604617    ! fn ← fetch_function … ge curr ;
    605618    ! st'' ← pop_frame … ge fn st';
     
    640653    match s' with
    641654    [ RETURN ⇒
    642       do 〈st',ra〉 ← fetch_ra … st;
     655      do 〈ra, st'〉 ← fetch_ra … st;
    643656      if eq_pointer ra exit then
    644657       do vals ← read_result … ge (joint_if_result … fn) st' ;
Note: See TracChangeset for help on using the changeset viewer.