Changeset 1163 for src/ERTL/semantics.ma


Ignore:
Timestamp:
Sep 1, 2011, 4:23:42 PM (9 years ago)
Author:
mulligan
Message:

even more streamlining and fixes to get things type checking

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1162 r1163  
    214214  OK ? (set_regs regs st))).
    215215
     216definition retrieve: state → move_registers → res val ≝
     217  λst.
     218  λr.
     219  match r with
     220  [ pseudo   src ⇒ reg_retrieve (locals st) src
     221  | hardware src ⇒ hwreg_retrieve (regs st) src
     222  ].
     223
     224definition store ≝
     225  λst.
     226  λv.
     227  λr.
     228  match r with
     229  [ pseudo   dst ⇒
     230    ! locals ← reg_store dst v (locals st);
     231      ret ? (set_locals locals st)
     232  | hardware dst ⇒
     233    ! regs ← hwreg_store dst v (regs st);
     234      ret ? (set_regs regs st)
     235  ].
     236
    216237definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
    217238  λglobals. λge,st.
     
    271292      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
    272293      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
    273       | joint_instr_hdw_to_hdw dst_src ⇒
    274           let 〈dst, src〉 ≝ dst_src in
    275         ! v ← hwreg_retrieve (regs st) src;
    276         ! regs ← hwreg_store dst v (regs st);
    277           ret ? 〈E0, goto l (set_regs regs st)〉
    278294      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    279295        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     
    295311        ! v ← Byte_of_val v;
    296312        ! st ← push st v;
     313          ret ? 〈E0, goto l st〉
     314      | joint_instr_move dst_src ⇒
     315        let 〈dst, src〉 ≝ dst_src in
     316        ! v ← retrieve st src;
     317        ! st ← store st v dst;
    297318          ret ? 〈E0, goto l st〉
    298319      (* CSC: changed, where the meat is *)
     
    316337            ! st ← set_result vs st;
    317338              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     339          ]
    318340      ]
    319       | _ ⇒ ?
    320       ]
     341    (* CSC: changed, where the meat is *)
    321342    | joint_st_return ⇒
    322343      ! st ← pop_frame st;
     
    327348    | _ ⇒ ?
    328349    ]
    329   | ertl_st_get_hdw dst src l ⇒
    330      ! v ← hwreg_retrieve (regs st) src;
    331      ! locals ← reg_store dst v (locals st);
    332      ret ? 〈E0, goto l (set_locals locals st)〉
    333   | ertl_st_set_hdw dst src l ⇒
    334      ! v ← reg_retrieve (locals st) src;
    335      ! regs ← hwreg_store dst v (regs st);
    336      ret ? 〈E0, goto l (set_regs regs st)〉
    337   | ertl_st_new_frame _ ⇒ ?
    338   | ertl_st_del_frame _ ⇒ ?
    339   | ertl_st_frame_size _ _ ⇒ ?
    340   (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
    341          ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
    342          be more than enough... *)
    343   | ertl_st_move dst src l ⇒
    344      ! v ← reg_retrieve (locals st) src;
    345      ! locals ← reg_store dst v (locals st);
    346      ret ? 〈E0, goto l (set_locals locals st)〉
    347   ].
    348 
     350  | ertl_st_new_frame l ⇒
     351    ! v ← framesize globals st;
     352    ! sp ← get_hwsp st;
     353      let newsp ≝ addr_sub sp v in
     354    ! st ← set_hwsp newsp st;
     355      ret ? 〈E0,goto l st〉
     356  | ertl_st_del_frame l ⇒
     357    ! v ← framesize globals st;
     358    ! sp ← get_hwsp st;
     359      let newsp ≝ addr_add sp v in
     360    ! st ← set_hwsp newsp st;
     361      ret ? 〈E0,goto l st〉
     362  | ertl_st_frame_size dst l ⇒
     363    ! v ← framesize globals st;
     364    ! locals ← reg_store dst (val_of_nat v) (locals st);
     365      ret ? 〈E0, goto l (set_locals locals st)〉
    349366  (* CSC: Dropped:
    350367      - rtl_st_stackaddr (becomes two get_hdw)
    351368      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
    352369      - rtl_st_call_ptr (unimplemented ATM) *)
    353   cases daemon
    354 qed.
     370  ].
    355371     
    356372axiom WrongReturnValueType: String.
Note: See TracChangeset for help on using the changeset viewer.