Changeset 1382 for src/joint


Ignore:
Timestamp:
Oct 14, 2011, 10:50:56 PM (9 years ago)
Author:
sacerdot
Message:
  • succ_pc generalized to return a res (necessary for LIN semantics)
  • succ_pc implemented for LIN
Location:
src/joint
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/joint/SemanticUtils.ma

    r1359 r1382  
    4040(*CSC: XXX This code is cut&paste from joint/semantics.ma, address_of_label.
    4141  Maybe there is a better way to organize the code!!! *)
    42 definition graph_succ_p: label → address → address.
     42definition graph_succ_p: label → address → res address.
    4343 #l #_ generalize in match (refl … (address_of_pointer (pointer_of_label l)))
    4444 cases (address_of_pointer (pointer_of_label l)) in ⊢ (???% → ?)
    45   [ #res #_ @res
    46   | #msg cases (pointer_of_label l) * * #q #com #off #E1 #E2 destruct normalize in E2; destruct ]
     45  [ #res #_ @(OK … res)
     46  | #msg cases (pointer_of_label l) * * #q #com #off #E1 destruct #E2 normalize in E2; destruct ]
    4747qed.
    4848
  • src/joint/semantics.ma

    r1377 r1382  
    1515 ; regsT: Type[0]
    1616
    17  ; succ_pc: succ p → address → address
     17 ; succ_pc: succ p → address → res address
    1818 ; greg_store_: generic_reg p → beval → regsT → res regsT
    1919 ; greg_retrieve_: regsT → generic_reg p → res beval
     
    128128 λp,l,st. set_pc … (address_of_label p l) st.
    129129
    130 definition next: ∀p:sem_params. succ … p → state p → state p ≝
    131  λp,l,st. set_pc … (succ_pc … (more_sem_pars p) l (pc … st)) st.
     130definition 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) ;
     133  OK … (set_pc … l' st).
    132134
    133135definition greg_store: ∀p:sem_params. generic_reg p → beval → state p → res (state p) ≝
     
    217219      match seq with
    218220      [ extension c ⇒ exec_extended … p ge c l st
    219       | COST_LABEL cl ⇒ ret ? 〈Echarge cl, next … l st〉
    220       | COMMENT c ⇒ ret ? 〈E0, next … l st〉
     221      | COST_LABEL cl ⇒
     222         ! st ← next … l st ;
     223         ret ? 〈Echarge cl, st〉
     224      | COMMENT c ⇒
     225         ! st ← next … l st ;
     226         ret ? 〈E0, st〉
    221227      | INT dest v ⇒
    222         ! st ← greg_store p dest (BVByte v) st;
    223           ret ? 〈E0, next … l st〉
     228         ! st ← greg_store p dest (BVByte v) st;
     229         ! st ← next … l st ;
     230          ret ? 〈E0, st〉
    224231      | LOAD dst addrl addrh ⇒
    225232        ! vaddrh ← dph_retrieve … st addrh;
     
    228235        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
    229236        ! st ← acca_store p … dst v st;
    230           ret ? 〈E0, next … l st〉
     237        ! st ← next … l st ;
     238          ret ? 〈E0, st〉
    231239      | STORE addrl addrh src ⇒
    232240        ! vaddrh ← dph_retrieve … st addrh;
     
    235243        ! v ← acca_retrieve … st src;
    236244        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
    237           ret ? 〈E0, next … l (set_m … m' st)〉
     245        let st ≝ set_m … m' st in
     246        ! st ← next … l st ;
     247          ret ? 〈E0, st〉
    238248      | COND src ltrue ⇒
    239249        ! v ← acca_retrieve … st src;
    240250        ! b ← bool_of_beval v;
    241           ret ? 〈E0, (if b then goto … ltrue else next … l) st〉
     251        if b then
     252         ret ? 〈E0, goto … ltrue st〉
     253        else
     254         ! st ← next … l st ;
     255         ret ? 〈E0, st〉
    242256      | ADDRESS ident prf ldest hdest ⇒
    243257        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
     
    245259        ! st ← dpl_store p ldest laddr st;
    246260        ! st ← dph_store p hdest haddr st;
    247           ret ? 〈E0, next … l st〉
     261        ! st ← next … l st ;
     262          ret ? 〈E0, st〉
    248263      | OP1 op dacc_a sacc_a ⇒
    249264        ! v ← acca_retrieve … st sacc_a;
     
    251266          let v' ≝ BVByte (op1 eval op v) in
    252267        ! st ← acca_store p dacc_a v' st;
    253           ret ? 〈E0, next … l st〉
     268        ! st ← next … l st ;
     269          ret ? 〈E0, st〉
    254270      | OP2 op dacc_a sacc_a src ⇒
    255271        ! v1 ← acca_retrieve … st sacc_a;
     
    262278          let carry ≝ beval_of_bool carry in
    263279        ! st ← acca_store p dacc_a v' st;
    264           ret ? 〈E0, next … l (set_carry … carry st)〉
    265       | CLEAR_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVfalse st)〉
    266       | SET_CARRY ⇒ ret ? 〈E0, next … l (set_carry … BVtrue st)〉
     280          let st ≝ set_carry … carry st in
     281        ! st ← next … l st ;
     282          ret ? 〈E0, st〉
     283      | CLEAR_CARRY ⇒
     284        ! st ← next … l (set_carry … BVfalse st) ;
     285         ret ? 〈E0, st〉
     286      | SET_CARRY ⇒
     287        ! st ← next … l (set_carry … BVtrue st) ;
     288         ret ? 〈E0, st〉
    267289      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    268290        ! v1 ← acca_retrieve … st sacc_a_reg;
     
    275297        ! st ← acca_store p dacc_a_reg v1' st;
    276298        ! st ← accb_store p dacc_b_reg v2' st;
    277           ret ? 〈E0, next … l st〉
     299        ! st ← next … l st ;
     300          ret ? 〈E0, st〉
    278301      | POP dst ⇒
    279302        ! 〈st,v〉 ← pop … st;
    280303        ! st ← acca_store p dst v st;
    281           ret ? 〈E0, next … l st〉
     304        ! st ← next … l st ;
     305          ret ? 〈E0, st〉
    282306      | PUSH src ⇒
    283307        ! v ← acca_retrieve … st src;
    284308        ! st ← push … st v;
    285           ret ? 〈E0, next … l st〉
     309        ! st ← next … l st ;
     310          ret ? 〈E0, st〉
    286311      | MOVE dst_src ⇒
    287312        ! st ← pair_reg_move … st dst_src ;
    288           ret ? 〈E0, next … l st〉
     313        ! st ← next … l st ;
     314          ret ? 〈E0, st〉
    289315      | CALL_ID id args dest ⇒
    290316        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     
    292318          match fd with
    293319          [ Internal fn ⇒
    294             let l ≝ succ_pc … (more_sem_pars p) l (pc … st) in
     320            ! l ← succ_pc … (more_sem_pars p) l (pc … st) ;
    295321            ! st ← save_frame … l (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
    296322            let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
     
    304330               components; instead I am making a singleton out of it *)
    305331              let vs ≝ [mk_val ? evres] in
    306             ! st ← set_result … vs st;
    307               ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), next … l st〉
     332            ! st ← set_result … vs st;
     333            ! st ← next … l st ;
     334              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    308335          ]]
    309336    | RETURN ⇒
Note: See TracChangeset for help on using the changeset viewer.