Changeset 693 for Deliverables/D3.1


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.

Location:
Deliverables/D3.1/C-semantics
Files:
4 edited

Legend:

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

    r487 r693  
    1313].
    1414
    15 let rec up_to_nth_step (n:nat) (input:list eventval) (e:execution) (t:trace) : res (trace × state) ≝
     15let rec up_to_nth_step (n:nat) (input:list eventval) (e:execution state io_out io_in) (t:trace) : res (trace × state) ≝
    1616match n with
    1717[ O ⇒ match e with [ e_step tr s _ ⇒ OK ? 〈t⧺tr, s〉
  • Deliverables/D3.1/C-semantics/Cexec.ma

    r638 r693  
    11
    2 include "Csem.ma".
    32
    43include "extralib.ma".
    54include "IOMonad.ma".
     5include "SmallstepExec.ma".
     6include "Csem.ma".
    67
    78(*
     
    709710].
    710711
    711 (* A (possibly non-terminating) execution.   *)
    712 coinductive execution : Type[0] ≝
    713 | e_stop : trace → int → mem → execution
    714 | e_step : trace → state → execution → execution
    715 | e_wrong : execution
    716 | e_interact : ∀o:io_out. (io_in o → execution) → execution.
    717 
    718712definition mem_of_state : state → mem ≝
    719713λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
    720714
    721 (* This definition is slightly awkward because of the need to provide resumptions.
    722    It records the last trace/state passed in, then recursively processes the next
    723    state. *)
    724 
    725 let corec exec_inf_aux (ge:genv) (s:IO io_out io_in (trace×state)) : execution ≝
    726 match s with
    727 [ Wrong ⇒ e_wrong
    728 | Value v ⇒ match v with [ pair t s' ⇒
    729     match is_final_state s' with
    730     [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s')
    731     | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
    732 | Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
    733 ].
    734 
    735 
    736 definition exec_inf : clight_program → execution ≝
     715definition is_final : state → option int ≝
     716λs.match is_final_state s with
     717[ inl r ⇒ Some ? (sig_eject … r)
     718| inr _ ⇒ None ?
     719].
     720
     721definition clight_exec : clight_program → execstep ≝
     722λp. mk_execstep … (initial_state p) is_final mem_of_state exec_step.
     723
     724definition exec_inf : ∀p:clight_program. execution (state (clight_exec p)) io_out io_in ≝
    737725λp.
    738726  match make_initial_state p with
    739   [ OK gs ⇒ exec_inf_aux (\fst gs) (ret ? 〈E0,\snd gs〉)
    740   | _ ⇒ e_wrong
     727  [ OK gs ⇒ exec_inf_aux (clight_exec p) (\fst gs) (ret ? 〈E0,\snd gs〉)
     728  | _ ⇒ e_wrong ???
    741729  ].
    742 
    743 lemma execution_cases: ∀e.
    744  e = match e with [ e_stop tr r m ⇒ e_stop tr r m | e_step tr s e ⇒ e_step tr s e
    745  | e_wrong ⇒ e_wrong | e_interact o k ⇒ e_interact o k ].
    746 #e cases e; //; qed.
    747 
    748 lemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s =
    749 match s with
    750 [ Wrong ⇒ e_wrong
    751 | Value v ⇒ match v with [ pair t s' ⇒
    752     match is_final_state s' with
    753     [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s')
    754     | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
    755 | Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
    756 ].
    757 #ge #s >(execution_cases (exec_inf_aux …)) cases s;
    758 [ #o #k
    759 | #x cases x; #tr #s' cases s';
    760   [ #fn #st #k #env #m
    761   | #fd #args #k #mem
    762   | #v #k #mem (* for final state check *) cases k;
    763     [ cases v; [ 2,3: #v' | 4: #r | 5: #r #loc #pc #off ]
    764     | #s' #k' | 3,4: #e #s' #k' | 5,6: #e #s' #s'' #k' | #k' | #a #b #c #d ]
    765   ]
    766 | ]
    767 whd in ⊢ (??%%); //;
    768 qed.
    769 
  • 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.
  • Deliverables/D3.1/C-semantics/SmallstepExec.ma

    r469 r693  
    44include "Integers.ma".
    55include "Events.ma".
     6include "Mem.ma".
    67
    7 nrecord execstep : Type[1] ≝
    8 { genv  : Type
    9 ; state : Type
    10 ; input : Type
    11 ; output : (input → Type)
     8record execstep : Type[1] ≝
     9{ genv  : Type[0]
     10; state : Type[0]
     11; output : Type[0]
     12; input : output → Type[0]
    1213; initial : state → Prop
    13 ; final : state → int → Prop
    14 ; step : genv → state → IO input output (trace×state)
     14; is_final : state → option int
     15; mem_of_state : state → mem
     16; step : genv → state → IO output input (trace×state)
    1517}.
    1618
    17 nlet rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
    18  : IO (input exec) (output exec) (trace × (state exec)) ≝
     19let rec repeat (n:nat) (exec:execstep) (g:genv exec) (s:state exec)
     20 : IO (output exec) (input exec) (trace × (state exec)) ≝
    1921match n with
    2022[ O ⇒ Value ??? 〈E0, s〉
     
    2325].
    2426
     27(* A (possibly non-terminating) execution.   *)
     28coinductive execution (state:Type[0]) (output:Type[0]) (input:output → Type[0]) : Type[0] ≝
     29| e_stop : trace → int → mem → execution state output input
     30| e_step : trace → state → execution state output input → execution state output input
     31| e_wrong : execution state output input
     32| e_interact : ∀o:output. (input o → execution state output input) → execution state output input.
     33
     34(* This definition is slightly awkward because of the need to provide resumptions.
     35   It records the last trace/state passed in, then recursively processes the next
     36   state. *)
     37
     38let corec exec_inf_aux (exec:execstep) (ge:genv exec)
     39                       (s:IO (output exec) (input exec) (trace×(state exec)))
     40                       : execution ??? ≝
     41match s with
     42[ Wrong ⇒ e_wrong ???
     43| Value v ⇒ match v with [ pair t s' ⇒
     44    match is_final exec s' with
     45    [ Some r ⇒ e_stop ??? t r (mem_of_state exec s')
     46    | None ⇒ e_step ??? t s' (exec_inf_aux ? ge (step exec ge s')) ] ]
     47| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ? ge (k' v))
     48].
     49
     50lemma execution_cases: ∀ex.∀e:execution (state ex) (output ex) (input ex).
     51 e = match e with [ e_stop tr r m ⇒ e_stop ??? tr r m
     52 | e_step tr s e ⇒ e_step ??? tr s e
     53 | e_wrong ⇒ e_wrong ??? | e_interact o k ⇒ e_interact ??? o k ].
     54#ex #e cases e; //; qed.
     55
     56axiom exec_inf_aux_unfold: ∀exec,ge,s. exec_inf_aux exec ge s =
     57match s with
     58[ Wrong ⇒ e_wrong ???
     59| Value v ⇒ match v with [ pair t s' ⇒
     60    match is_final exec s' with
     61    [ Some r ⇒ e_stop ??? t r (mem_of_state exec s')
     62    | None ⇒ e_step ??? t s' (exec_inf_aux ? ge (step exec ge s')) ] ]
     63| Interact out k' ⇒ e_interact ??? out (λv. exec_inf_aux ? ge (k' v))
     64].
     65(*
     66#exec #ge #s >(execution_cases ? (exec_inf_aux …)) cases s
     67[ #o #k
     68| #x cases x #tr #s' (* XXX Can't unfold exec_inf_aux here *)
     69| ]
     70whd in ⊢ (??%%); //;
     71qed.
     72*)
     73
     74
     75
    2576alias symbol "and" (instance 2) = "logical and".
    26 nrecord related_semantics : Type[1] ≝
     77record related_semantics : Type[1] ≝
    2778{ sem1 : execstep
    2879; sem2 : execstep
     
    3182; match_states : state sem1 → state sem2 → Prop
    3283; match_initial_states : ∀st1. (initial sem1) st1 → ∃st2. (initial sem2) st2 ∧ match_states st1 st2
    33 ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (final sem1) st1 r → (final sem2) st2 r
     84; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final sem1) st1 = Some ? r → (is_final sem2) st2 = Some ? r
    3485}.
    3586
    3687
    3788
    38 nrecord simulation : Type[1] ≝
     89record simulation : Type[1] ≝
    3990{ sems :> related_semantics
    4091; sim : ∀st1,st2,t,st1'.
Note: See TracChangeset for help on using the changeset viewer.