Changeset 1382


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

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1380 r1382  
    33
    44(*CSC: re-organize to take succ_pc out of lin_more_sem_params? *)
    5 definition ltl_lin_more_sem_params: ∀succT:Type[0].∀succ:succT → address → address. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
     5definition ltl_lin_more_sem_params: ∀succT:Type[0].∀succ:succT → address → res address. more_sem_params (mk_params_ ltl_lin_params__ succT) :=
    66 λsuccT,succ.
    77 mk_more_sem_params ?
     
    2222
    2323definition ltl_lin_sem_params:
    24  ∀succT:Type[0].∀succ:succT → address → address. sem_params ≝
     24 ∀succT:Type[0].∀succ:succT → address → res address. sem_params ≝
    2525 λsuccT,succ.mk_sem_params … (ltl_lin_more_sem_params … succ).
    2626
    2727definition ltl_lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    2828definition ltl_lin_pop_frame:
    29  ∀succT:Type[0].∀succ:succT → address → address. state … (ltl_lin_sem_params … succ) → res ((state … (ltl_lin_sem_params … succ)) × address) ≝
     29 ∀succT:Type[0].∀succ:succT → address → res address. state … (ltl_lin_sem_params … succ) → res ((state … (ltl_lin_sem_params … succ)) × address) ≝
    3030 λ_.λ_.fetch_ra ….
    3131definition ltl_lin_save_frame:
    32  ∀succT:Type[0].∀succ:succT → address → address. address → nat → unit → nat → unit → state … (ltl_lin_sem_params … succ) → res (state … (ltl_lin_sem_params … succ)) ≝
     32 ∀succT:Type[0].∀succ:succT → address → res address. address → nat → unit → nat → unit → state … (ltl_lin_sem_params … succ) → res (state … (ltl_lin_sem_params … succ)) ≝
    3333 λ_.λ_.λl.λ_.λ_.λ_.λ_.λst.save_ra … st l.
    3434
    35 definition ltl_lin_more_sem_params1 : ∀succT:Type[0].∀succ:succT → address → address.more_sem_params1 … ltl_lin_params1 ≝
     35definition ltl_lin_more_sem_params1 : ∀succT:Type[0].∀succ:succT → address → res address.more_sem_params1 … ltl_lin_params1 ≝
    3636 λsuccT,succ.
    3737 mk_more_sem_params1 ? ltl_lin_params1 (ltl_lin_more_sem_params ? succ)
     
    3939
    4040(*CSC: XXXXX, for is_final only *)
    41 axiom ltl_lin_fetch_result: ∀succT:Type[0].∀succ:succT → address → address.state (ltl_lin_sem_params … succ) → res (list beval).
     41axiom ltl_lin_fetch_result: ∀succT:Type[0].∀succ:succT → address → res address.state (ltl_lin_sem_params … succ) → res (list beval).
    4242
    4343(*CSC: XXXX, for external functions only*)
    44 axiom ltl_lin_fetch_external_args: ∀succT:Type[0].∀succ:succT → address → address.external_function → state (ltl_lin_sem_params … succ) → res (list val).
    45 axiom ltl_lin_set_result: ∀succT:Type[0].∀succ:succT → address → address.list val → state (ltl_lin_sem_params … succ) → res (state (ltl_lin_sem_params … succ)).
     44axiom ltl_lin_fetch_external_args: ∀succT:Type[0].∀succ:succT → address → res address.external_function → state (ltl_lin_sem_params … succ) → res (list val).
     45axiom ltl_lin_set_result: ∀succT:Type[0].∀succ:succT → address → res address.list val → state (ltl_lin_sem_params … succ) → res (state (ltl_lin_sem_params … succ)).
    4646
    47 definition ltl_lin_exec_extended: ∀succT:Type[0].∀succ:succT → address → address.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params … succ) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ)))
     47definition ltl_lin_exec_extended: ∀succT:Type[0].∀succ:succT → address → res address.∀p.∀globals. genv globals (p globals) → False → succT → state (ltl_lin_sem_params … succ) → IO io_out io_in (trace × (state (ltl_lin_sem_params … succ)))
    4848 ≝ λsuccT,succ,p,globals,ge,abs. ⊥.
    4949@abs qed.
  • src/LIN/semantics.ma

    r1380 r1382  
    22include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 (*CSC: XXXX*)
    5 axiom lin_succ_pc: unit → address → address.
     4definition lin_succ_pc: unit → address → res address :=
     5 λ_.λaddr. addr_add addr 1.
    66
    77(*CSC: XXXXXXXXXX *)
  • 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.