Changeset 1140


Ignore:
Timestamp:
Aug 30, 2011, 2:23:37 PM (8 years ago)
Author:
sacerdot
Message:

More instructions implemented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1137 r1140  
    2929axiom val_of_Byte: Byte → val.
    3030axiom Byte_of_val: val → res Byte.
    31 (*
    3231(* Map from the front-end memory model to the back-end memory model *)
    3332axiom represent_block: block → val × val.
    34 *)
    3533(* CSC: fixed size chunk *)
    3634axiom chunk: memory_chunk.
     35axiom val_of_memory_chunk: memory_chunk → val. (* CSC: only to shift the sp *)
    3736
    3837axiom address: Type[0].
     38axiom val_of_address: address → val. (* CSC: only to shift the sp *)
     39axiom address_of_val: val → address. (* CSC: only to shift the sp *)
    3940(* CSC: ??? *)
    4041axiom address_of_label: mem → label → address.
     42axiom address_chunks_of_label: mem → label → Byte × Byte.
     43axiom label_of_address_chunks: Byte → Byte → label.
    4144axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    4245axiom hwreg_retrieve : mRegisterMap → Register → res val.
     
    6871 λregs,st. mk_state (st_frms st) (pc st) (sp st) (locals st) (carry st) regs (m st).
    6972
     73definition set_sp: address → state → state ≝
     74 λsp,st. mk_state (st_frms st) (pc st) sp (locals st) (carry st) (regs st) (m st).
     75
    7076definition set_carry: val → state → state ≝
    7177 λcarry,st. mk_state (st_frms st) (pc st) (sp st) (locals st) carry (regs st) (m st).
     
    8288 λst. mk_state (locals st::st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) (m st).
    8389
    84 definition push: state → Byte → state ≝
     90axiom FailedStore: String.
     91
     92definition push: state → Byte → res state ≝
    8593 λst,v.
    86 
    87 definition pop: state → state × Byte ≝
     94  let sp ≝ val_of_address (sp st) in
     95  (*CSC: no monadic notation here *)
     96  bind ?? (opt_to_res ? (msg FailedStore) (storev chunk (m st) sp (val_of_Byte v)))
     97   (λm.
     98    let sp ≝ address_of_val (add sp (val_of_memory_chunk chunk)) in
     99    OK ? (set_m m (set_sp sp st))).
     100
     101
     102definition pop: state → res (state × Byte) ≝
     103 λst:state.
     104  let sp ≝ val_of_address (sp st) in
     105  let sp ≝ sub sp (val_of_memory_chunk chunk) in
     106  let st ≝ set_sp (address_of_val sp) st in
     107  (*CSC: no monadic notation here *)
     108  bind ?? (opt_to_res ? (msg FailedStore) (loadv chunk (m st) sp))
     109   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
     110
     111definition save_ra : state → label → res state ≝
     112 λst,l.
     113  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m st) l in
     114  (* No monadic notation here *)
     115  bind ?? (push st addrl) (λst.push st addrh).
     116
     117definition fetch_ra : state → res (state × label) ≝
    88118 λst.
    89 
    90 definition save_ra : state → ? → state ≝
    91  λst,l.
    92   let 〈addrl,addrh〉 ≝ ? l in
    93   let st ≝ push st addrl in
    94   let st ≝ push st addrh in
    95    st.
    96 
    97 definition fetch_ra : state → state × ? ≝
    98  λst.
    99   let 〈st,addrh〉 ≝ pop st in
    100   let 〈st,addrl〉 ≝ pop st in
    101    〈st, ? addrl addrh〉.
     119  (* No monadic notation here *)
     120  bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
     121  bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
     122   OK ? 〈st, label_of_address_chunks addrl addrh〉)).
    102123
    103124(*CSC: To be implemented *)
     
    136157axiom FailedConstant : String. *)
    137158axiom FailedLoad : String.
    138 axiom FailedStore : String.
    139159axiom BadFunction : String.
    140160(*axiom BadJumpTable : String.
     
    171191      ! b ← eval_bool_of_val v;
    172192      ret ? 〈E0, goto (if b then ltrue else lfalse) st〉
    173 (*  | ertl_st_addr ldest hdest id l ⇒
     193  | ertl_st_addr ldest hdest id l ⇒
    174194     ! addr ← opt_to_res … [MSG MissingSymbol; CTX … id] (find_symbol ?? ge id);
    175195     let 〈laddr,haddr〉 ≝ represent_block addr in
     
    177197     ! locals ← reg_store hdest haddr locals;
    178198     ret ? 〈E0, goto l (set_locals locals st)〉
    179 *)  | ertl_st_op1 op dst src l ⇒
     199  | ertl_st_op1 op dst src l ⇒
    180200     ! v ← reg_retrieve (locals st) src;
    181201     ! v ← Byte_of_val v;
     
    194214     ! locals ← reg_store dst v' (locals st);
    195215     ret ? 〈E0, goto l (set_locals locals (set_carry carry st))〉
    196 (*  | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
     216  | ertl_st_opaccs op dacc dbacc sacc sbacc l ⇒
    197217     ! v1 ← reg_retrieve (locals st) sacc;
    198218     ! v1 ← Byte_of_val v1;
     
    204224     ! locals ← reg_store dacc v1' (locals st);
    205225     ! locals ← reg_store dbacc v2' locals;
    206      ret ? 〈E0, goto l (set_locals locals st)〉 *)
     226     ret ? 〈E0, goto l (set_locals locals st)〉
    207227  | ertl_st_clear_carry l ⇒
    208228    ret ? 〈E0, goto l (set_carry Vfalse st)〉
     
    241261      match fd with
    242262      [ Internal fn ⇒
    243         let st ≝ save_ra st l in
     263        ! st ← save_ra st l;
    244264        let st ≝ save_frame st in
    245265        let locals ≝ init_locals (ertl_if_locals fn) in
    246266        let pc ≝ ertl_if_entry fn in
    247          goto pc (set_locals locals st)
     267         ret ? 〈 E0, goto pc (set_locals locals st)〉
    248268      | External fn ⇒ ? (*
    249269        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
Note: See TracChangeset for help on using the changeset viewer.