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/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 
Note: See TracChangeset for help on using the changeset viewer.