Ignore:
Timestamp:
Oct 22, 2011, 4:18:11 AM (9 years ago)
Author:
sacerdot
Message:
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1430 r1451  
    1919 ; call_dest_for_main: call_dest p
    2020
    21  (*CSC: XXXX succ_pc and pointer_of_label deal with fetching; same for
    22    fetch_statement below.
    23    should we take 'em out in a different record to simplify the code? *)
    24  ; succ_pc: succ p → address → res address
    2521 ; greg_store_: generic_reg p → beval → regsT → res regsT
    2622 ; greg_retrieve_: regsT → generic_reg p → res beval
     
    3430 ; dph_retrieve_: regsT → dph_reg p → res beval
    3531 ; pair_reg_move_: regsT → pair_reg p → res regsT
    36  
    37  ; pointer_of_label: label → Σp:pointer. ptype p = Code
    3832 }.
    3933
     
    6357 { more_sparams :> more_sem_params p
    6458
     59 (*CSC: XXXX succ_pc, pointer_of_label and fetch_statement all deal with fetching
     60   should we take 'em out in a different record to simplify the code? *)
     61 ; succ_pc: succ p → address → res address
     62 ; pointer_of_label: genv … p → pointer → label → res (Σp:pointer. ptype p = Code)
    6563 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
    6664
     
    10199 ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1 ?.
    102100
    103 definition address_of_label: sem_params → label → address ≝
    104  λp,l.address_of_code_pointer (pointer_of_label … p l).
    105 
    106101definition set_m: ∀p. bemem → state p → state p ≝
    107102 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
     
    125120 λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
    126121
    127 definition goto: ∀p:sem_params. label → state p → state p ≝
    128  λp,l,st. set_pc … (address_of_label p l) st.
    129 
    130 definition next: ∀p:sem_params. succ … p → state p → res (state p) ≝
    131  λp,l,st.
    132   do l' ← succ_pc … (more_sem_pars p) l (pc … st) ;
     122
     123definition address_of_label: ∀globals. ∀p:sem_params1 globals. genv globals p → pointer → label → res address ≝
     124 λglobals,p,ge,ptr,l.
     125  do newptr ← pointer_of_label … p ge … ptr l ;
     126  OK … (address_of_code_pointer newptr).
     127
     128definition goto: ∀globals. ∀p:sem_params1 globals. genv globals p → label → state p → res (state p) ≝
     129 λglobals,p,ge,l,st.
     130  do oldpc ← pointer_of_address (pc … st) ;
     131  do newpc ← address_of_label … ge oldpc l ;
     132  OK … (set_pc … newpc st).
     133
     134definition next: ∀globals. ∀p:sem_params1 globals. succ … p → state p → res (state p) ≝
     135 λglobals,p,l,st.
     136  do l' ← succ_pc … p l (pc … st) ;
    133137  OK … (set_pc … l' st).
    134138
     
    222226      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
    223227      let l' ≝ joint_if_entry … fn in
    224        ret ? 〈 E0, goto … l' (set_regs p regs st)〉
     228      ! st ← goto … ge l' (set_regs p regs st) ;
     229       ret ? 〈 E0, st〉
    225230    | External fn ⇒
    226231      ! params ← fetch_external_args … fn st;
     
    247252  ! s ← fetch_statement … ge st;
    248253  match s with
    249     [ GOTO l ⇒ ret ? 〈E0, goto … l st〉
     254    [ GOTO l ⇒
     255       ! st ← goto … p ge l st ;
     256       ret ? 〈E0, st〉
    250257    | sequential seq l ⇒
    251258      match seq with
    252259      [ extension c ⇒ exec_extended … p ge c l st
    253260      | COST_LABEL cl ⇒
    254          ! st ← next … l st ;
     261         ! st ← next … p l st ;
    255262         ret ? 〈Echarge cl, st〉
    256263      | COMMENT c ⇒
    257          ! st ← next … l st ;
     264         ! st ← next … p l st ;
    258265         ret ? 〈E0, st〉
    259266      | INT dest v ⇒
    260267         ! st ← greg_store p dest (BVByte v) st;
    261          ! st ← next … l st ;
     268         ! st ← next … p l st ;
    262269          ret ? 〈E0, st〉
    263270      | LOAD dst addrl addrh ⇒
     
    267274        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    268275        ! st ← acca_store p … dst v st;
    269         ! st ← next … l st ;
     276        ! st ← next … p l st ;
    270277          ret ? 〈E0, st〉
    271278      | STORE addrl addrh src ⇒
     
    276283        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    277284        let st ≝ set_m … m' st in
    278         ! st ← next … l st ;
     285        ! st ← next … p l st ;
    279286          ret ? 〈E0, st〉
    280287      | COND src ltrue ⇒
     
    282289        ! b ← bool_of_beval v;
    283290        if b then
    284          ret ? 〈E0, goto … ltrue st〉
     291         ! st ← goto … p ge ltrue st ;
     292         ret ? 〈E0, st〉
    285293        else
    286          ! st ← next … l st ;
     294         ! st ← next … p l st ;
    287295         ret ? 〈E0, st〉
    288296      | ADDRESS ident prf ldest hdest ⇒
     
    291299        ! st ← dpl_store p ldest laddr st;
    292300        ! st ← dph_store p hdest haddr st;
    293         ! st ← next … l st ;
     301        ! st ← next … p l st ;
    294302          ret ? 〈E0, st〉
    295303      | OP1 op dacc_a sacc_a ⇒
     
    298306          let v' ≝ BVByte (op1 eval op v) in
    299307        ! st ← acca_store p dacc_a v' st;
    300         ! st ← next … l st ;
     308        ! st ← next … p l st ;
    301309          ret ? 〈E0, st〉
    302310      | OP2 op dacc_a sacc_a src ⇒
     
    311319        ! st ← acca_store p dacc_a v' st;
    312320          let st ≝ set_carry … carry st in
    313         ! st ← next … l st ;
     321        ! st ← next … p l st ;
    314322          ret ? 〈E0, st〉
    315323      | CLEAR_CARRY ⇒
    316         ! st ← next … l (set_carry … BVfalse st) ;
     324        ! st ← next … p l (set_carry … BVfalse st) ;
    317325         ret ? 〈E0, st〉
    318326      | SET_CARRY ⇒
    319         ! st ← next … l (set_carry … BVtrue st) ;
     327        ! st ← next … p l (set_carry … BVtrue st) ;
    320328         ret ? 〈E0, st〉
    321329      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
     
    329337        ! st ← acca_store p dacc_a_reg v1' st;
    330338        ! st ← accb_store p dacc_b_reg v2' st;
    331         ! st ← next … l st ;
     339        ! st ← next … p l st ;
    332340          ret ? 〈E0, st〉
    333341      | POP dst ⇒
    334342        ! 〈st,v〉 ← pop … st;
    335343        ! st ← acca_store p dst v st;
    336         ! st ← next … l st ;
     344        ! st ← next … p l st ;
    337345          ret ? 〈E0, st〉
    338346      | PUSH src ⇒
    339347        ! v ← acca_retrieve … st src;
    340348        ! st ← push … st v;
    341         ! st ← next … l st ;
     349        ! st ← next … p l st ;
    342350          ret ? 〈E0, st〉
    343351      | MOVE dst_src ⇒
    344352        ! st ← pair_reg_move … st dst_src ;
    345         ! st ← next … l st ;
     353        ! st ← next … p l st ;
    346354          ret ? 〈E0, st〉
    347355      | CALL_ID id args dest ⇒
    348         ! ra ← succ_pc … (more_sem_pars p) l (pc … st) ;         
     356        ! ra ← succ_pc … p l (pc … st) ;         
    349357          eval_call_id … p ge st id args dest ra ]
    350358    | RETURN ⇒
     
    419427[3: % | cases ispb | cases spb] *; #r #off #E >E %
    420428qed.
    421 (*
    422 RTL:
    423  init_prog == init_mem
    424  init_sp: inizializzare lo stack pointer
    425  init_isp: inizializzare l'altro stack pointer
    426  init_renv: inizializzare i registri fisici
    427  init_main_call: chiamata di funzione
    428    --- init_fun_call: cambia fra ERTL e LTL
    429  change_carry: a 0
    430 *)
    431429
    432430definition joint_fullexec :
Note: See TracChangeset for help on using the changeset viewer.