Ignore:
Timestamp:
Mar 18, 2011, 12:11:23 PM (9 years ago)
Author:
campbell
Message:

Separate out whole program executions from the clight semantics and start
setting it up for RTLabs too.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/RTLabs/RTLabs-sem.ma

    r639 r693  
    1010include "Globalenvs.ma".
    1111include "IOMonad.ma".
     12include "SmallstepExec.ma".
    1213
    1314definition genv ≝ (genv_t Genv) (fundef internal_function).
    1415
    1516record frame : Type[0] ≝
    16 { locals : register_env split_val
     17{ func   : internal_function
     18; locals : register_env split_val
    1719; next   : label
    1820; sp     : block
     
    2123
    2224definition adv : label → frame → frame ≝
    23 λl,f. mk_frame (locals f) l (sp f) (retdst f).
     25λl,f. mk_frame (func f) (locals f) l (sp f) (retdst f).
    2426
    2527inductive state : Type[0] ≝
    26 | State : frame → list frame → mem → state
     28| State :
     29   ∀   f : frame.
     30   ∀  fs : list frame.
     31   ∀   m : mem.
     32   state
    2733| Callstate :
    2834   ∀  fd : fundef internal_function.
     
    3844   ∀   m : mem.
    3945   state.
     46
     47definition mem_of_state : state → mem ≝
     48λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
    4049
    4150definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
     
    165174].
    166175
    167 definition eval_statement : genv → statement → state → IO io_out io_in (trace × state) ≝
    168 λge,s,st.
     176definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
     177λge,st.
    169178match st with
    170179[ State f fs m ⇒
     180  ! s ← graph_lookup ? (f_graph (func f)) (next f);
    171181  match s with
    172182  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
     
    175185      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
    176186      ! locals ← reg_store rs v (locals f);
    177       ret ? 〈E0, State (mk_frame locals l (sp f) (retdst f)) fs m〉
     187      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    178188  | St_op1 op dst src l ⇒
    179189      ! v ← reg_retrieve (locals f) src;
    180190      ! v' ← opt_to_res … (eval_unop op v);
    181191      ! locals ← reg_store dst v' (locals f);
    182       ret ? 〈E0, State (mk_frame locals l (sp f) (retdst f)) fs m〉
     192      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    183193  | St_op2 op dst src1 src2 l ⇒
    184194      ! v1 ← reg_retrieve (locals f) src1;
     
    186196      ! v' ← opt_to_res … (eval_binop op v1 v2);
    187197      ! locals ← reg_store dst v' (locals f);
    188       ret ? 〈E0, State (mk_frame locals l (sp f) (retdst f)) fs m〉
     198      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    189199  | St_load chunk mode args dst l ⇒
    190200      ! vaddr ← eval_addr ge f mode args;
    191201      ! v ← opt_to_res … (loadv chunk m vaddr);
    192202      ! locals ← reg_store dst v (locals f);
    193       ret ? 〈E0, State (mk_frame locals l (sp f) (retdst f)) fs m〉
     203      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    194204  | St_store chunk mode args src l ⇒
    195205      ! vaddr ← eval_addr ge f mode args;
     
    253263        ! locals ← params_store (f_params fn) params (register_empty ?);
    254264        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) Any in
    255         ret ? 〈E0, State (mk_frame locals (f_entry fn) sp dst) fs m'〉
     265        ret ? 〈E0, State (mk_frame fn locals (f_entry fn) sp dst) fs m'〉
    256266    | External fn ⇒
    257267        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     
    265275    | cons f fs' ⇒
    266276        ! locals ← reg_store dst v (locals f);
    267         ret ? 〈E0, State (mk_frame locals (next f) (sp f) (retdst f)) fs m〉
     277        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs m〉
    268278    ]
    269279].
     280
     281definition is_final : state → option int ≝
     282λs. match s with
     283[ State _ _ _ ⇒ None ?
     284| Callstate _ _ _ _ _ ⇒ None ?
     285| Returnstate v _ fs _ ⇒
     286    match fs with [ nil ⇒ match v with [ Vint i ⇒ Some ? i | _ ⇒ None ? ] | cons _ _ ⇒ None ? ]
     287].
     288
     289definition RTLabs_exec : RTLabs_program → execstep ≝
     290λp. mk_execstep … ? is_final mem_of_state eval_statement.
Note: See TracChangeset for help on using the changeset viewer.