Changeset 1312


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.

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1303 r1312  
    44(*CSC: XXXXX *)
    55axiom ertl_init_locals : list register → (register_env beval) × hw_register_env → (register_env beval) × hw_register_env.
    6 axiom ertl_pop_frame: unit → res unit.
     6NON BASTA: DEBBO RIPRISTINARE IL LOCAL_ENV E IN RTL TANTE COSE!
     7axiom ertl_pop_frame: list (register_env beval) → res (list (register_env beval)).
    78axiom ertl_save_frame: unit → (register_env beval) × hw_register_env → unit.
    89
     
    2526definition ertl_more_sem_params: more_sem_params ertl_params_ :=
    2627 mk_more_sem_params ertl_params_
    27   unit(*framesT*) ((register_env beval) × hw_register_env) graph_succ_p ertl_pop_frame ertl_save_frame
     28  (list (register_env beval)) ((register_env beval) × hw_register_env) graph_succ_p ertl_pop_frame ertl_save_frame
    2829   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
    2930    ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
  • src/LIN/semantics.ma

    r1304 r1312  
    11include "joint/SemanticUtils.ma".
    22include "LIN/LIN.ma". (* CSC: syntax.ma in RTLabs *)
    3 
    4 definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    5 definition lin_pop_frame: unit → res unit ≝ λ_. OK … it.
    6 definition lin_save_frame: unit → hw_register_env → unit ≝ λ_.λ_. it.
    73
    84(*CSC: XXXX*)
     
    139definition lin_more_sem_params: more_sem_params lin_params_ :=
    1410 mk_more_sem_params lin_params_
    15   unit hw_register_env lin_succ_pc lin_pop_frame lin_save_frame
     11  unit hw_register_env lin_succ_pc
    1612   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    1713    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
     
    2824     pointer_of_label.
    2925definition lin_sem_params: sem_params ≝ mk_sem_params … lin_more_sem_params.
     26
     27definition lin_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
     28definition lin_pop_frame: state … lin_sem_params → res (state … lin_sem_params) ≝ λst. OK … st.
     29definition lin_save_frame: state … lin_sem_params → state … lin_sem_params ≝ λst.st.
     30
     31definition lin_more_sem_params1 : more_sem_params1 … lin_params1 ≝
     32 mk_more_sem_params1 ? lin_params1 lin_more_sem_params
     33  lin_init_locals lin_pop_frame lin_save_frame.
    3034
    3135(*CSC: XXXXXXXXXX *)
     
    4549definition lin_more_sem_params2: ∀globals. more_sem_params2 … (lin_params globals) ≝
    4650 λglobals.
    47   mk_more_sem_params2 … lin_more_sem_params lin_init_locals
     51  mk_more_sem_params2 … lin_more_sem_params1
    4852   (lin_fetch_statement …) lin_fetch_result lin_fetch_external_args lin_set_result
    4953    (lin_exec_extended …).
  • src/LTL/semantics.ma

    r1303 r1312  
    22include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
    5 definition ltl_pop_frame: unit → res unit ≝ λ_. OK … it.
    6 definition ltl_save_frame: unit → hw_register_env → unit ≝ λ_.λ_. it.
    7 
    84definition ltl_more_sem_params: more_sem_params ltl_params_ :=
    95 mk_more_sem_params ltl_params_
    10   unit hw_register_env graph_succ_p ltl_pop_frame ltl_save_frame
     6  unit hw_register_env graph_succ_p
    117   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    128    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
     
    2420definition ltl_sem_params: sem_params ≝ mk_sem_params … ltl_more_sem_params.
    2521
     22definition ltl_init_locals : unit → hw_register_env → hw_register_env ≝ λ_.λe.e.
     23definition ltl_pop_frame: state … ltl_sem_params → res (state … ltl_sem_params) ≝ λst. OK … st.
     24definition ltl_save_frame: state … ltl_sem_params → state … ltl_sem_params ≝ λst.st.
     25
     26definition ltl_more_sem_params1 : more_sem_params1 … ltl_params1 ≝
     27 mk_more_sem_params1 ? ltl_params1 ltl_more_sem_params
     28  ltl_init_locals ltl_pop_frame ltl_save_frame.
     29
    2630(*CSC: XXXXX, for is_final only *)
    2731axiom ltl_fetch_result: state ltl_sem_params → nat → res val.
     
    3741definition ltl_more_sem_params2: ∀globals. more_sem_params2 … (ltl_params globals) ≝
    3842 λglobals.
    39   mk_more_sem_params2 … ltl_more_sem_params ltl_init_locals
     43  mk_more_sem_params2 … ltl_more_sem_params1
    4044   (graph_fetch_statement …) ltl_fetch_result ltl_fetch_external_args ltl_set_result
    4145    (ltl_exec_extended …).
  • 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.