Ignore:
Timestamp:
Oct 6, 2011, 10:35:29 PM (8 years ago)
Author:
sacerdot
Message:

Type of frame operations (pop_frame/save_frame) generalized to take in account
the RTL semantics. LTL and LIN semantics fixed. Fixing of ERTL/RTL still to
be done.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1303 r1312  
    2222
    2323 ; succ_pc: succ p → address → address
    24  ; pop_frame_: framesT → res framesT
    25  ; save_frame_: framesT → regsT → framesT
    2624 ; greg_store_: generic_reg p → beval → regsT → res regsT
    2725 ; greg_retrieve_: regsT → generic_reg p → res beval
     
    5351 }.
    5452
     53record more_sem_params1 (succT: Type[0]) (p:params1): Type[1] ≝
     54 { more_sparams :> more_sem_params (mk_params_ p succT)
     55
     56   (* Functions that manipulate the st_frms component of the state *)
     57 ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
     58 ; pop_frame: state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
     59 ; save_frame: state (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams)
     60 }.
     61
     62record sem_params1: Type[1] ≝
     63 { spp1 :> params1
     64 ; ssucc_ : Type[0]
     65 ; more_sem_params1 :> more_sem_params1 ssucc_ spp1
     66 }.
     67
     68definition sem_params_of_sem_params1 ≝ λsp1: sem_params1. mk_sem_params … sp1.
     69coercion sem_params_of_sem_params1 : ∀_x:sem_params1. sem_params
     70 ≝ sem_params_of_sem_params1 on _x: sem_params1 to sem_params.
     71
    5572definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
    5673
    5774record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
    58  { more_sparams:> more_sem_params p
    59 
    60  ; init_locals : localsT p → regsT … more_sparams → regsT … more_sparams
    61  
    62  ; fetch_statement: genv … p → state (mk_sem_params … more_sparams) → res (joint_statement (mk_sem_params … more_sparams) globals)
    63  ; fetch_result: state (mk_sem_params … more_sparams) → nat → res val
    64 
    65  ; fetch_external_args: external_function → state (mk_sem_params … more_sparams) → res (list val)
    66  ; set_result: list val → state (mk_sem_params … more_sparams) → res (state (mk_sem_params … more_sparams))
    67 
    68  ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams) → state (mk_sem_params … more_sparams) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams)))
     75 { more_sparams1 :> more_sem_params1 (succ p) p
     76
     77 ; fetch_statement: genv … p → state (mk_sem_params … more_sparams1) → res (joint_statement (mk_sem_params … more_sparams1) globals)
     78 ; fetch_result: state (mk_sem_params … more_sparams1) → nat → res val
     79
     80 ; fetch_external_args: external_function → state (mk_sem_params … more_sparams1) → res (list val)
     81 ; set_result: list val → state (mk_sem_params … more_sparams1) → res (state (mk_sem_params … more_sparams1))
     82
     83 ; exec_extended: genv globals p → extend_statements (mk_sem_params … more_sparams1) → state (mk_sem_params … more_sparams1) → IO io_out io_in (trace × (state (mk_sem_params … more_sparams1)))
    6984 }.
    7085
     
    85100    (more_sparams2 globals p)))) ≡ spp__o__pars_ S.
    86101*)
     102definition sem_params1_of_sem_params2 ≝ λglobals. λsp2: sem_params2 globals. mk_sem_params1 sp2 (succ sp2) sp2.
     103coercion sem_params1_of_sem_params2 : ∀globals. ∀_x:sem_params2 globals. sem_params1
     104 ≝ sem_params1_of_sem_params2 on _x: sem_params2 ? to sem_params1.
     105
    87106definition address_of_label: sem_params → label → address.
    88107 #p #l generalize in match (refl … (beval_pair_of_pointer (pointer_of_label … p l)))
     
    160179  do regs ← pair_reg_move_ … (regs … st) rs;
    161180  OK … (set_regs … regs st).
    162 
    163 definition save_frame: ∀p:sem_params. state p → state p ≝
    164  λp,st. set_frms … (save_frame_ … (st_frms … st) (regs … st)) st.
    165 
    166 (* removes the top frame from the frames list *)
    167 definition pop_frame: ∀p. state p → res (state p) ≝
    168  λp,st.
    169   do frames ← pop_frame_ … p (st_frms … st);
    170   OK ? (mk_state ? frames (pc … st) (sp … st) (carry … st) (regs … st) (m … st)).
    171181
    172182axiom FailedStore: String.
Note: See TracChangeset for help on using the changeset viewer.