Changeset 366 for C-semantics/CexecIO.ma


Ignore:
Timestamp:
Dec 2, 2010, 4:41:43 PM (9 years ago)
Author:
campbell
Message:

Make I/O type safe, removing a discrepancy between the executable and
inductive semantics.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/CexecIO.ma

    r321 r366  
    781781##] nqed.
    782782
    783 (* IO monad *)
    784 
    785 (* Interactions are function calls that return a value and do not change
    786    the rest of the Clight program's state. *)
    787 ndefinition io_out ≝ (ident × (list eventval)).
    788 
    789 ndefinition do_io : ident → list eventval → IO eventval io_out eventval ≝
    790 λfn,args. Interact ?? eventval 〈fn,args〉 (λres. Value ?? eventval res).
    791 
    792 ndefinition ret: ∀T. T → (IO eventval io_out T) ≝
    793 λT,x.(Value ?? T x).
    794 
    795783(* Checking types of values given to / received from an external function call. *)
    796784
    797 ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
     785ndefinition eventval_type : ∀ty:typ. Type ≝
     786λty. match ty with [ Tint ⇒ int | Tfloat ⇒ float ].
     787
     788ndefinition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
     789λty:typ. match ty return λty'.eventval_type ty' → eventval with [ Tint ⇒ λv.EVint v | Tfloat ⇒ λv.EVfloat v ].
     790
     791ndefinition mk_val: ∀ty:typ. eventval_type ty → val ≝
     792λty:typ. match ty return λty'.eventval_type ty' → val with [ Tint ⇒ λv.Vint v | Tfloat ⇒ λv.Vfloat v ].
     793
     794nlemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
     795  eventval_match (mk_eventval ty v) ty (mk_val ty v).
     796#ty; ncases ty; nnormalize; //; nqed.
     797
     798ndefinition convert_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
    798799λev,ty.
    799800match ty with
     
    828829nqed.
    829830
     831(* IO monad *)
     832
     833(* Interactions are function calls that return a value and do not change
     834   the rest of the Clight program's state. *)
     835nrecord io_out : Type ≝
     836{ io_function: ident
     837; io_args: list eventval
     838; io_in_typ: typ
     839}.
     840
     841ndefinition io_in ≝ λo. eventval_type (io_in_typ o).
     842
     843ndefinition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
     844λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
     845
     846ndefinition ret: ∀T. T → (IO io_out io_in T) ≝
     847λT,x.(Value ?? T x).
     848
    830849(* execution *)
    831850
     
    836855    store_value_of_type ty m pcl loc ofs v ] ].
    837856
    838 nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (trace × state)) ≝
     857nlet rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
    839858match st with
    840859[ State f s k e m ⇒
     
    966985  | External f argtys retty ⇒
    967986      ! evargs ← err_to_io_sig … (check_eventval_list vargs (typlist_of_typelist argtys));
    968       ! evres ← do_io f evargs;
    969       ! vres ← err_to_io_sig … (check_eventval evres (proj_sig_res (signature_of_type argtys retty)));
    970       ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉
     987      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
     988      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
    971989  ]
    972990| Returnstate res k m ⇒
     
    11131131    nwhd; napply (step_internal_function … Halloc Hbind);
    11141132  ##| #id argtys rty; napply sig_bindIO_OK; #evs Hevs;
    1115     napply bindIO_OK; #eres;
    1116     napply sig_bindIO_OK; #res Hres;
    1117     nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##]
     1133    napply bindIO_OK; #eres; nwhd;
     1134    napply step_external_function; @; ##[ napply Hevs; ##| napply mk_val_correct; ##]
    11181135  ##] 
    11191136##| #v k' m'; nwhd in ⊢ (?????%); ncases k'; //;
     
    11261143nqed.
    11271144
    1128 nlet rec make_initial_state (p:program) : IO eventval io_out state ≝
     1145nlet rec make_initial_state (p:program) : IO io_out io_in state ≝
    11291146  let ge ≝ globalenv Genv ?? p in
    11301147  let m0 ≝ init_mem Genv ?? p in
     
    11631180
    11641181nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
    1165  IO eventval io_out (trace×state) ≝
     1182 IO io_out io_in (trace×state) ≝
    11661183match is_final_state s with
    11671184[ inl _ ⇒ ret ? 〈E0, s〉
     
    12251242| e_step : trace → state → execution → execution
    12261243| e_wrong : execution
    1227 | e_interact : io_out → (eventval → execution) → execution.
     1244| e_interact : ∀o:io_out. (io_in o → execution) → execution.
    12281245
    12291246ndefinition mem_of_state : state → mem ≝
     
    12341251   state. *)
    12351252
    1236 nlet corec exec_inf_aux (ge:genv) (s:IO eventval io_out (trace×state)) : execution ≝
     1253nlet corec exec_inf_aux (ge:genv) (s:IO io_out io_in (trace×state)) : execution ≝
    12371254match s with
    12381255[ Wrong ⇒ e_wrong
     
    13091326    execution_isteps tr' s e s' e' →
    13101327    execution_isteps (tr⧺tr') s0 (e_step tr s e) s' e'
    1311 | isteps_interact : ∀e,e',k,o,i,s,s',s0,tr,tr'.
     1328| isteps_interact : ∀e,e',o,k,i,s,s',s0,tr,tr'.
    13121329    execution_isteps tr' s e s' e' →
    13131330    k i = e_step tr s e →
     
    13781395    ##| #E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC');
    13791396    ##]
    1380 ##| #e e' k o i s s' s0 tr tr' H1 H2 H3 IH;
     1397##| #e e' o k i s s' s0 tr tr' H1 H2 H3 IH;
    13811398    nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%? → ?);
    13821399    ncases (is_final_state s0); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct;
Note: See TracChangeset for help on using the changeset viewer.