Changeset 1142


Ignore:
Timestamp:
Aug 30, 2011, 3:33:36 PM (8 years ago)
Author:
sacerdot
Message:

More progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1140 r1142  
    4242axiom address_chunks_of_label: mem → label → Byte × Byte.
    4343axiom label_of_address_chunks: Byte → Byte → label.
     44axiom address_of_address_chunks: Byte → Byte → address.
    4445axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    4546axiom hwreg_retrieve : mRegisterMap → Register → res val.
     
    8889 λst. mk_state (locals st::st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) (m st).
    8990
     91axiom FailedPopFrame: String.
     92
     93(* removes the top frame from the frames list *)
     94definition pop_frame: state → res state ≝
     95 λst.
     96  match st_frms st with
     97   [ nil ⇒ Error ? (msg FailedPopFrame)
     98   | cons _ frms ⇒
     99      OK ? (mk_state frms (pc st) (sp st) (locals st) (carry st) (regs st) (m st)) ].
     100
    90101axiom FailedStore: String.
    91102
     
    163174axiom ReturnMismatch : String.
    164175*)
     176
     177(*CSC: to be implemented *)
     178axiom fetch_external_args: external_function → state → list val.
     179axiom set_result: list val → state → state.
    165180
    166181definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
     
    264279        let st ≝ save_frame st in
    265280        let locals ≝ init_locals (ertl_if_locals fn) in
    266         let pc ≝ ertl_if_entry fn in
    267          ret ? 〈 E0, goto pc (set_locals locals st)〉
    268       | External fn ⇒ ? (*
     281        let l' ≝ ertl_if_entry fn in
     282         ret ? 〈 E0, goto l' (set_locals locals st)〉
     283      | External fn ⇒
     284        let params ≝ fetch_external_args fn st in
    269285        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    270286        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    271         (* CSC: return type changed from option to list *)
    272         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉 *)
     287        (* CSC: XXX bug here; I think I should split it into Byte-long
     288           components; instead I am making a singleton out of it *)
     289        let vs ≝ [mk_val ? evres] in
     290        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres),
     291         goto l (set_result vs st)〉
    273292      ]
    274 (*     
    275      
    276       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    277       ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    278 *)   
    279 
     293  | ertl_st_return ⇒
     294      ! st ← pop_frame st;
     295      ! 〈st,pch〉 ← pop st;
     296      ! 〈st,pcl〉 ← pop st;
     297      let pc ≝ address_of_address_chunks pcl pch in
     298      ret ? 〈E0,set_pc pc st〉
    280299  | _ ⇒ ? ]
    281300(*
    282   | rtl_st_return ⇒
    283       let dest ≝ rtl_if_result (func f) in
    284       ! v ←  mmap … (reg_retrieve (locals f)) dest;
    285       ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    286301  ]
    287302| Returnstate v dst fs m ⇒
Note: See TracChangeset for help on using the changeset viewer.