Changeset 1320


Ignore:
Timestamp:
Oct 7, 2011, 2:17:25 PM (8 years ago)
Author:
sacerdot
Message:

Frame operations implemented.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1313 r1320  
    99include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
    1010
     11(* CSC: a streamlined version of the ERTL state *)
     12record frame: Type[0] ≝
     13 { fr_pc: address
     14 ; fr_sp: pointer
     15 ; fr_carry: beval
     16 ; fr_regs: register_env beval
     17 }.
     18
    1119definition rtl_more_sem_params: more_sem_params rtl_params_ :=
    1220 mk_more_sem_params rtl_params_
    13   unit(*framesT*) (register_env beval) graph_succ_p
     21  (list frame) (register_env beval) graph_succ_p
    1422   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
    1523    reg_store reg_retrieve reg_store reg_retrieve
     
    2028definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
    2129
    22 (*CSC: XXXXX *)
    23 axiom rtl_init_locals : list register → register_env beval → register_env beval.
    24 axiom rtl_pop_frame: state … rtl_sem_params → res (state … rtl_sem_params).
    25 axiom rtl_save_frame: state … rtl_sem_params → state … rtl_sem_params.
     30definition rtl_init_locals :
     31 list register → register_env beval → register_env beval ≝
     32 λlocals.λ_.
     33  foldl ?? (λlenv,reg. add … lenv reg BVundef) (empty_map …) locals.
     34
     35(*CSC: could we use here a dependent type to avoid the Error case? *)
     36axiom EmptyStack: String.
     37definition rtl_pop_frame: state … rtl_sem_params → res (state … rtl_sem_params) ≝
     38 λst.
     39  let frms ≝ st_frms ? st in
     40  match frms with
     41  [ nil ⇒ Error ? [MSG EmptyStack]
     42  | cons hd tl ⇒
     43     OK …
     44      (set_frms rtl_sem_params tl
     45       (set_regs rtl_sem_params (fr_regs hd)
     46        (set_sp … (fr_sp hd)
     47         (set_pc … (fr_pc hd)
     48          (set_carry … (fr_carry hd) st))))) ].
     49
     50definition rtl_save_frame: state … rtl_sem_params → state … rtl_sem_params ≝
     51 λst.
     52  set_frms rtl_sem_params
     53   (mk_frame (pc … st) (sp … st) (carry … st) (regs ? st) :: (st_frms … st)) st.
    2654
    2755definition rtl_more_sem_params1 : more_sem_params1 … rtl_params1 ≝
Note: See TracChangeset for help on using the changeset viewer.