source: C-semantics/CexecIO.ma @ 25

Last change on this file since 25 was 25, checked in by campbell, 9 years ago

Simplify the IO monad a little.

File size: 38.0 KB
Line 
1
2include "Csem.ma".
3
4include "extralib.ma".
5include "IOMonad.ma".
6
7(* Some experimental definitions for an executable semantics. *)
8
9ndefinition bool_of_val_1 : val → type → res val ≝
10  λv,ty. match v with
11  [ Vint i ⇒ match ty with
12    [ Tint _ _ ⇒ OK ? (of_bool (¬eq i zero))
13    | Tpointer _ ⇒ OK ? (of_bool (¬eq i zero))
14    | _ ⇒ Error ?
15    ]
16  | Vfloat f ⇒ match ty with
17    [ Tfloat _ ⇒ OK ? (of_bool (¬Fcmp Ceq f Fzero))
18    | _ ⇒ Error ?
19    ]
20  | Vptr _ _ ⇒ match ty with
21    [ Tint _ _ ⇒ OK ? Vtrue
22    | Tpointer _ ⇒ OK ? Vtrue
23    | _ ⇒ Error ?
24    ]
25  | _ ⇒ Error ?
26  ].
27
28(* There's a lot more repetition than I'd like here, in large part because
29   there's no way to introduce different numbers of hypotheses when doing the
30   case distinctions. *)
31
32nlemma bool_of_val_1_ok : ∀v,ty,r. bool_of_val_1 v ty = OK ? r ↔ bool_of_val v ty r.
33#v ty r; @;
34##[
35  nelim v; ##[ #H; nnormalize in H; ndestruct; ##| ##2,3: #x; ##| ##4: #x y; ##]
36  ncases ty;
37  ##[ ##1,10,19: #H; nnormalize in H; ndestruct;
38  ##| #i s; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H;
39    ##[ nrewrite > H; nrewrite > (eq_true …); #H';
40        ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
41        #H''; nrewrite > H''; /2/;
42    ##| nrewrite > (eq_false …); //; #H';
43        ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
44        #H''; nrewrite > H''; /3/;
45    ##]
46  ##|##3,9,13,18,21,27: #x H; nnormalize in H; ndestruct;
47  ##| #t; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H;
48    ##[ nrewrite > H; nrewrite > (eq_true …); #H';
49        ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
50        #H''; nrewrite > H''; /2/;
51    ##| nrewrite > (eq_false …); //; #H';
52        ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
53        #H''; nrewrite > H''; /3/;
54    ##]
55  ##| ##5,6,7,8,11,14,15,16,17,23,24,25,26: #a b H; nnormalize in H; ndestruct;
56  ##| #f; nwhd in ⊢ (??%? → ?); nelim (eq_dec x Fzero); #H;
57    ##[ nrewrite > H; nrewrite > (Feq_zero_true …); #H';
58        ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
59        #H''; nrewrite > H''; /2/;
60    ##| nrewrite > (Feq_zero_false …); //; #H';
61        ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]
62        #H''; nrewrite > H''; /3/;
63    ##]
64  ##| #i s H; nwhd in H:(??%?);
65      ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##]
66      #H'; nrewrite > H'; /2/;
67  ##| #t H; nwhd in H:(??%?);
68      ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##]
69      #H'; nrewrite > H'; /2/;
70  ##]
71##| #H; nelim H; #v t H'; nelim H';
72  ##[ #i is s ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
73  ##| ##2,4: //
74  ##| #i t ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
75  ##| #f s ne; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
76  ##| #i s; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
77  ##| #t; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;
78  ##| #s; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
79  ##]
80##] nqed.
81
82include "Plogic/russell_support.ma".
83
84(* Nicer - we still have to deal with all of the cases, but only need to
85   introduce the result value, so there's a single case for getting rid of
86   all the Error goals. *)
87
88ndefinition bool_of_val_2 : ∀v:val. ∀ty:type. { r : res bool | ∀r'. r = OK ? r' → bool_of_val v ty (of_bool r') } ≝
89  λv,ty. match v in val with
90  [ Vint i ⇒ match ty with
91    [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))
92    | Tpointer _ ⇒ Some ? (OK ? (¬eq i zero))
93    | _ ⇒ Some ? (Error ?)
94    ]
95  | Vfloat f ⇒ match ty with
96    [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero))
97    | _ ⇒ Some ? (Error ?)
98    ]
99  | Vptr _ _ ⇒ match ty with
100    [ Tint _ _ ⇒ Some ? (OK ? true)
101    | Tpointer _ ⇒ Some ? (OK ? true)
102    | _ ⇒ Some ? (Error ?)
103    ]
104  | _ ⇒ Some ? (Error ?)
105  ]. nwhd;
106##[ ##3,5: #r; nlapply (eq_spec c0 zero); nelim (eq c0 zero);
107  ##[ ##1,3: #e H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2,4: ndestruct; // ##] nrewrite > e; /3/;
108  ##| ##2,4: #ne H; nrewrite > (?:of_bool r=Vtrue);  ##[ ##2,4: ndestruct; // ##] /3/;
109  ##]
110##| ##13: #r; nelim (eq_dec c0 Fzero);
111  ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); #H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2: ndestruct; // ##] /2/;
112  ##| #ne; nrewrite > (Feq_zero_false …); //; #H;
113      nrewrite > (?:of_bool r=Vtrue);  ##[ ##2: ndestruct; // ##] /3/;
114  ##]
115##| ##21,23: #r H; nrewrite > (?:of_bool r = Vtrue); ##[ ##2,4: ndestruct; // ##] /2/
116##| ##*: #a b; ndestruct;
117##] nqed.
118
119(* Same as before, except we have to write eject in because the type for the
120   equality is left implied, so the coercion isn't used. *)
121
122nlemma bool_of_val_2_complete : ∀v,ty,r.
123  bool_of_val v ty r →
124  ∃b. r = of_bool b ∧ eject ?? (bool_of_val_2 v ty) = OK ? b.
125#v ty r H; nelim H; #v t H'; nelim H';
126  ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
127  ##| #b i i0 s; @ true; @; //
128  ##| #i t ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;
129  ##| #b i t0; @ true; @; //
130  ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;
131  ##| #i s; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)
132  ##| #t; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)
133  ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;
134  ##]
135nqed.
136
137
138(* Nicer again (after the extra definitions).  Just use sigma type rather than
139   the subset, but take into account the error monad.  The error cases all
140   become trivial and we don't have to muck around to get the result. *)
141
142ndefinition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝
143  λA,P,a.match a with [ None ⇒ False | Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True | OK z ⇒ P z ]].
144
145ndefinition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (sigma A P) ≝
146  λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a.
147  (match a return λa'.a=a' → res (sigma A P) with
148   [ None ⇒ λe1.?
149   | Some b ⇒ λe1.(match b return λb'.b=b' → ? with
150     [ Error ⇒ λ_. Error ?
151     | OK c ⇒ λe2. OK ? (sig_intro A P c ?)
152     ]) (refl ? b)
153   ]) (refl ? a).
154##[ nrewrite > e1 in p; nnormalize; *;
155##| nrewrite > e1 in p; nrewrite > e2; nnormalize; //
156##] nqed.
157
158ndefinition err_eject : ∀A.∀P: A → Prop. res (sigma A P) → res A ≝
159  λA,P,a.match a with [ Error ⇒ Error ? | OK b ⇒
160    match b with [ sig_intro w p ⇒ OK ? w] ].
161
162ndefinition sig_eject : ∀A.∀P: A → Prop. sigma A P → A ≝
163  λA,P,a.match a with [ sig_intro w p ⇒ w].
164
165ncoercion err_inject :
166  ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (sigma A P) ≝ err_inject
167  on a:option (res ?) to res (sigma ? ?).
168ncoercion err_eject : ∀A.∀P:A → Prop.∀c:res (sigma A P).res A ≝ err_eject
169  on _c:res (sigma ? ?) to res ?.
170ncoercion sig_eject : ∀A.∀P:A → Prop.∀c:sigma A P.A ≝ sig_eject
171  on _c:sigma ? ? to ?.
172
173ndefinition bool_of_val_3 : ∀v:val. ∀ty:type. res (Σr:bool. bool_of_val v ty (of_bool r)) ≝
174  λv,ty. match v in val with
175  [ Vint i ⇒ match ty with
176    [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))
177    | Tpointer _ ⇒ Some ? (OK ? (¬eq i zero))
178    | _ ⇒ Some ? (Error ?)
179    ]
180  | Vfloat f ⇒ match ty with
181    [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero))
182    | _ ⇒ Some ? (Error ?)
183    ]
184  | Vptr _ _ ⇒ match ty with
185    [ Tint _ _ ⇒ Some ? (OK ? true)
186    | Tpointer _ ⇒ Some ? (OK ? true)
187    | _ ⇒ Some ? (Error ?)
188    ]
189  | _ ⇒ Some ? (Error ?)
190  ]. nwhd; //;
191##[ ##1,2: nlapply (eq_spec c0 zero); nelim (eq c0 zero);
192  ##[ ##1,3: #e; nrewrite > e; napply bool_of_val_false; //;
193  ##| ##2,4: #ne; napply bool_of_val_true; /2/;
194  ##]
195##| nelim (eq_dec c0 Fzero);
196  ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //;
197  ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/;
198  ##]
199##| ##4,5: napply bool_of_val_true; //
200##] nqed.
201
202ndefinition err_eq ≝ λA,P. λx:res (sigma A P). λy:A.
203  match x with [ Error ⇒ False | OK x' ⇒
204    match x' with [ sig_intro x'' _ ⇒ x'' = y ]].
205(* TODO: can I write a coercion for the above? *)
206
207(* Same as before, except we have to use a slightly different "equality". *)
208
209nlemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ err_eq ?? (bool_of_val_3 v ty) b.
210#v ty r H; nelim H; #v t H'; nelim H';
211  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
212  ##| #b i i0 s; @ true; @; //
213  ##| #i t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
214  ##| #b i t0; @ true; @; //
215  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
216  ##| #i s; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
217  ##| #t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)
218  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
219  ##]
220nqed.
221
222(* Prove a few minor results to make proof obligations easy. *)
223
224nlemma bind_assoc_r: ∀A,B,C,e,f,g.
225  bind B C (bind A B e f) g = bind A C e (λx.bind B C (f x) g).
226#A B C e f g; ncases e; nnormalize; //; nqed.
227
228nlemma bind_OK: ∀A,B,P,e,f.
229  (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
230  match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ].
231#A B P e f; nelim e; /2/; nqed.
232
233nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B.
234  (∀v:A. err_eq A P e v → ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
235  match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
236#A B P P' e f; nelim e; //;
237#v0; nelim v0; #v Hv IH; napply IH; //; nqed.
238
239nlemma bind2_OK: ∀A,B,C,P,e,f.
240  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) →
241  match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ].
242#A B C P e f; nelim e; //; #v; ncases v; /2/; nqed.
243
244nlemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (sigma (A×B) P). ∀f:A → B → res C.
245  (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
246  match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
247#A B C P P' e f; nelim e; //;
248#v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.
249
250nlemma reinject: ∀A. ∀P,P':A → Prop. ∀e:res (sigma A P').
251  (∀v:A. err_eq A P' e v → P' v → P v) →
252  match err_eject A P' e with [ Error ⇒ True | OK v' ⇒ P v' ].
253#A P P' e; ncases e; //;
254#v0; nelim v0; #v Pv' IH; /2/;
255nqed.
256
257nlemma bool_val_distinct: Vtrue ≠ Vfalse.
258@; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero);
259nqed.
260
261nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
262  if b then is_true v ty else is_false v ty.
263#v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //;
264napply False_ind; napply (absurd ? ev ?);
265##[ ##2: napply sym_neq ##] napply bool_val_distinct;
266nqed.
267
268ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
269nlemma opt_OK: ∀A,P,e.
270  (∀v. e = Some ? v → P v) →
271  match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
272#A P e; nelim e; /2/;
273nqed.
274
275nlemma opt_bind_OK: ∀A,B,P,e,f.
276  (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
277  match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ].
278#A B P e f; nelim e; nnormalize; /2/; nqed.
279
280nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop.
281  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) →
282  match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ].
283#A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
284##[ #H; napply (False_ind … H);
285##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
286##] nqed.
287
288nlet rec is_neutral_cast (ty:type) : res (Σu:unit.neutral_for_cast ty) ≝
289match ty with
290[ Tint sz _ ⇒ match sz with [ I32 ⇒ Some ? (OK ? something) | _ ⇒ Some ? (Error ?) ]
291| Tpointer _ ⇒ Some ? (OK ? something)
292| Tarray _ _ ⇒ Some ? (OK ? something)
293| Tfunction _ _ ⇒ Some ? (OK ? something)
294| _ ⇒ Some ? (Error ?)
295]. nwhd; //; nqed.
296(*
297nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B.
298#A B e; ncases e; //; nqed.
299*)
300
301nlet rec exec_cast (v:val) (ty:type) (ty':type) : res (Σv':val. cast v ty ty' v') ≝
302match v with
303[ Vint i ⇒
304  match ty with
305  [ Tint sz1 si1 ⇒
306    match ty' with
307    [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i)))
308    | Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))))
309    (* no change in data repr *)
310    | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
311    ]
312  | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
313  ]
314| Vfloat f ⇒
315  match ty with
316  [ Tfloat sz ⇒
317    match ty' with
318    [ Tint sz' si' ⇒ Some ? (OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f))))
319    | Tfloat sz' ⇒ Some ? (OK ? (Vfloat (cast_float_float sz' f)))
320    | _ ⇒ Some ? (Error ?)
321    ]
322  | _ ⇒ Some ? (Error ?)
323  ]
324| Vptr b ofs ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vptr b ofs))
325| _ ⇒ Some ? (Error ?)
326]. ndestruct; /2/;
327##[ ##1,2,3: ncases c2; //; napply cast_nn_i; //
328##| ##4,5,6: napply sig_bind_OK; #u;#_;#H; napply cast_nn_i; //;
329##| napply sig_bind_OK; #u;#_;#H; napply sig_bind_OK; #u';#_;#H';
330    napply cast_nn_p; //
331##] nqed.
332
333(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
334   a structurally smaller value, we break out the surrounding Expr constructor
335   and use exec_lvalue'. *)
336
337nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val. eval_expr ge en m e r) ≝
338match e with
339[ Expr e' ty ⇒
340  match e' with
341  [ Econst_int i ⇒ Some ? (OK ? (Vint i))
342  | Econst_float f ⇒ Some ? (OK ? (Vfloat f))
343  | Evar _ ⇒ Some ? (
344      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
345      opt_to_res ? (load_value_of_type ty m loc ofs))
346  | Ederef _ ⇒ Some ? (
347      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
348      opt_to_res ? (load_value_of_type ty m loc ofs))
349  | Efield _ _ ⇒ Some ? (
350      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
351      opt_to_res ? (load_value_of_type ty m loc ofs))
352  | Eaddrof a ⇒ Some ? (
353      〈loc, ofs〉 ← exec_lvalue ge en m a;:
354      OK ? (Vptr loc ofs))
355  | Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty'))))
356  | Eunop op a ⇒ Some ? (
357      v1 ← exec_expr ge en m a;:
358      opt_to_res ? (sem_unary_operation op v1 (typeof a)))
359  | Ebinop op a1 a2 ⇒ Some ? (
360      v1 ← exec_expr ge en m a1;:
361      v2 ← exec_expr ge en m a2;:
362      opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m))
363  | Econdition a1 a2 a3 ⇒ Some ? (
364      v ← exec_expr ge en m a1;:
365      b ← bool_of_val_3 v (typeof a1);:
366      match b return λ_.res val with [ true ⇒ (exec_expr ge en m a2) | false ⇒ (exec_expr ge en m a3) ])
367(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
368  | Eorbool a1 a2 ⇒ Some ? (
369      v1 ← exec_expr ge en m a1;:
370      b1 ← bool_of_val_3 v1 (typeof a1);:
371      match b1 return λ_.res val with [ true ⇒ OK ? Vtrue | false ⇒
372        v2 ← exec_expr ge en m a2;:
373        b2 ← bool_of_val_3 v2 (typeof a2);:
374        OK ? (of_bool b2) ])
375  | Eandbool a1 a2 ⇒ Some ? (
376      v1 ← exec_expr ge en m a1;:
377      b1 ← bool_of_val_3 v1 (typeof a1);:
378      match b1 return λ_.res val with [ true ⇒
379        v2 ← exec_expr ge en m a2;:
380        b2 ← bool_of_val_3 v2 (typeof a2);:
381        OK ? (of_bool b2)
382      | false ⇒ OK ? Vfalse ])
383  | Ecast ty' a ⇒ Some ? (
384      v ← exec_expr ge en m a;:
385      exec_cast v (typeof a) ty')
386  ]
387]
388and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:block × int. eval_lvalue ge en m (Expr e' ty) (\fst r) (\snd r)) ≝
389  match e' with
390  [ Evar id ⇒
391      match (get … id en) with
392      [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈l,zero〉) (* global *)
393      | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *)
394      ]
395  | Ederef a ⇒ Some ? (
396      v ← exec_expr ge en m a;:
397      match v with
398      [ Vptr l ofs ⇒ OK ? 〈l,ofs〉
399      | _ ⇒ Error ?
400      ])
401  | Efield a i ⇒
402      match (typeof a) with
403      [ Tstruct id fList ⇒ Some ? (
404          〈l,ofs〉 ← exec_lvalue ge en m a;:
405          delta ← field_offset i fList;:
406          OK ? 〈l,add ofs (repr delta)〉)
407      | Tunion id fList ⇒ Some ? (
408          〈l,ofs〉 ← exec_lvalue ge en m a;:
409          OK ? 〈l,ofs〉)
410      | _ ⇒ Some ? (Error ?)
411      ]
412  | _ ⇒ Some ? (Error ?)
413  ]
414and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:block × int. eval_lvalue ge en m e (\fst r) (\snd r)) ≝
415match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
416nwhd; //;
417##[ napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
418    napply opt_OK;  #v ev; /2/;
419##| napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
420    napply opt_OK;  #v ev; /2/;
421##| napply sig_bind2_OK; #loc ofs H;
422    nwhd; napply eval_Eaddrof; //;
423##| napply sig_bind_OK; #v1 ev1 Hv1;
424    napply opt_OK; #v ev;
425    napply (eval_Eunop … Hv1 ev);
426##| napply sig_bind_OK; #v1 ev1 Hv1;
427    napply sig_bind_OK; #v2 ev2 Hv2;
428    napply opt_OK; #v ev;
429    napply (eval_Ebinop … Hv1 Hv2 ev);
430##| napply sig_bind_OK; #v ev Hv;
431    napply sig_bind_OK; #v' ev' Hv';
432    napply (eval_Ecast … Hv Hv');
433##| napply sig_bind_OK; #vb evb Hvb;
434    napply sig_bind_OK; #b;
435    ncases b; #eb Hb; napply reinject; #v ev Hv;
436    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
437    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
438    ##]
439##| napply sig_bind_OK; #v1 ev1 Hv1;
440    napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
441    ##[ napply sig_bind_OK; #v2 ev2 Hv2;
442        napply sig_bind_OK; #b2 eb2 Hb2;
443        napply (eval_Eandbool_2 … Hv1 … Hv2);
444        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
445    ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
446    ##]
447##| napply sig_bind_OK; #v1 ev1 Hv1;
448    napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
449    ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
450    ##| napply sig_bind_OK; #v2 ev2 Hv2;
451        napply sig_bind_OK; #b2 eb2 Hb2;
452        napply (eval_Eorbool_2 … Hv1 … Hv2);
453        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
454    ##]
455##| napply sig_bind2_OK; nrewrite > c5; #l ofs H;
456    napply opt_OK; #v ev; /2/;
457##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/;
458##| napply eval_Evar_local; /2/
459##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
460    napply eval_Ederef; //
461##| napply sig_bind2_OK; #l ofs H;
462    napply bind_OK; #delta Hdelta;
463    napply (eval_Efield_struct … H c5 Hdelta);
464##| napply sig_bind2_OK; #l ofs H;
465    napply (eval_Efield_union … H c5);
466##] nqed.
467
468(* TODO: Can we do this sensibly with a map combinator? *)
469nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (Σvl:list val. eval_exprlist ge e m l vl) ≝
470match l with
471[ nil ⇒ Some ? (OK ? (nil val))
472| cons e1 es ⇒ Some ? (
473  v ← exec_expr ge e m e1;:
474  vs ← exec_exprlist ge e m es;:
475  OK ? (cons val v vs))
476]. nwhd; //;
477napply sig_bind_OK; #v ev Hv;
478napply sig_bind_OK; #vs evs Hvs;
479nnormalize; /2/;
480nqed.
481
482(* Don't really want to use subset rather than sigma here, but can't be bothered
483   with *another* set of coercions. XXX: why do I have to get the recursive
484   call's property manually? *)
485
486nlet rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : { r:env × mem | alloc_variables en m l (\fst r) (\snd r) } ≝
487match l with
488[ nil ⇒ Some ? 〈en, m〉
489| cons h vars ⇒
490  match h with [ mk_pair id ty ⇒
491    match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒
492      match exec_alloc_variables (set … id b1 en) m1 vars with
493      [ sig_intro r p ⇒ r ]
494]]]. nwhd; //;
495nelim (exec_alloc_variables (set ident ? block c3 c7 en) c6 c1);
496#H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
497napply (alloc_variables_cons … IH); /2/;
498nqed.
499
500(* TODO: can we establish that length params = length vs in advance? *)
501nlet rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res (Σm2:mem. bind_parameters e m params vs m2) ≝
502  match params with
503  [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ]
504  | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒
505      match vs with
506      [ nil ⇒ Some ? (Error ?)
507      | cons v1 vl ⇒ Some ? (
508          b ← opt_to_res ? (get … id e);:
509          m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:
510          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
511      ]
512  ] ].
513nwhd; //;
514napply opt_bind_OK; #b eb;
515napply opt_bind_OK; #m1 em1;
516napply reinject; #m2 em2 Hm2;
517napply (bind_parameters_cons … eb em1 Hm2);
518nqed.
519
520ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝
521λt. match t with
522[ Tvoid ⇒ Some ? (Error ?)
523| _ ⇒ Some ? (OK ??)
524]. nwhd; //; @; #H; ndestruct; nqed.
525
526ninductive decide : Type ≝
527| dy : decide | dn : decide.
528
529ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P.
530#P d;ncases d;/2/; nqed.
531
532ncoercion decide_inject :
533  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P ≝ dodecide
534  on d:decide to ? + (¬?).
535
536ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P.
537#P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##| napply Error ##] nqed.
538
539ncoercion decide_inject2 :
540  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P ≝ dodecide2
541  on d:decide to res ?.
542
543alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
544alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
545ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
546#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
547ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
548#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
549ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
550#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
551
552nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
553match t1 with
554[ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ]
555| Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
556| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
557| Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
558| Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒
559    match assert_type_eq t t' with [ OK _ ⇒
560      match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
561| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒
562    match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
563| Tstruct i fl ⇒
564    match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
565      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
566| Tunion i fl ⇒
567    match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
568      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] |  _ ⇒ dn ]
569| Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
570]
571and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝
572match tl1 with
573[ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ]
574| Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒
575    match assert_type_eq t1 t2 with [ OK _ ⇒
576      match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
577]
578and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝
579match fl1 with
580[ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ]
581| Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒
582    match ident_eq i1 i2 with [ inl _ ⇒
583      match assert_type_eq t1 t2 with [ OK _ ⇒
584        match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy | _ ⇒ dn ]
585        | _ ⇒ dn ] | _ ⇒ dn ] ]
586].
587(* A poor man's clear, otherwise automation picks up recursive calls without
588   checking that the argument is smaller. *)
589ngeneralize in assert_type_eq;
590ngeneralize in assert_typelist_eq;
591ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //;
592(* XXX: I have no idea why the first // didn't catch these. *)
593//; //; //; //; //; //; //; //; //;
594nqed.
595
596nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
597match k with
598[ Kstop ⇒ dy
599| Kcall _ _ _ _ ⇒ dy
600| _ ⇒ dn
601]. nwhd; //; @; #H; nelim H; nqed.
602
603nlet rec is_Sskip (s:statement) : (s = Sskip) + (s ≠ Sskip) ≝
604match s with
605[ Sskip ⇒ dy
606| _ ⇒ dn
607].
608##[ //;
609##| ##*: @; #H; ndestruct;
610##] nqed.
611
612(* IO monad *)
613
614(* Interactions are function calls that return a value and do not change
615   the rest of the Clight program's state. *)
616ndefinition io_out ≝ (ident × (list eventval)).
617
618ndefinition do_io : ident → list eventval → IO eventval io_out eventval ≝
619λfn,args. Interact ?? eventval 〈fn,args〉 (λres. Value ?? eventval res).
620
621ndefinition ret: ∀T. T → (IO eventval io_out T) ≝
622λT,x.(Value ?? T x).
623
624(* Checking types of values given to / received from an external function call. *)
625
626ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
627λev,ty.
628match ty with
629[ Tint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ]
630| Tfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ]
631| _ ⇒ Some ? (Error ?)
632]. nwhd; //; nqed.
633
634ndefinition check_eventval' : ∀v:val. ∀ty:typ. res (Σev:eventval. eventval_match ev ty v) ≝
635λv,ty.
636match ty with
637[ Tint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ]
638| Tfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ]
639| _ ⇒ Some ? (Error ?)
640]. nwhd; //; nqed.
641
642nlet rec check_eventval_list (vs: list val) (tys: list typ) : res (Σevs:list eventval. eventval_list_match evs tys vs) ≝
643match vs with
644[ nil ⇒ match tys with [ nil ⇒ Some ? (OK ? (nil ?)) | _ ⇒ Some ? (Error ?) ]
645| cons v vt ⇒
646  match tys with
647  [ nil ⇒ Some ? (Error ?)
648  | cons ty tyt ⇒ Some ? (
649    ev ← check_eventval' v ty;:
650    evt ← check_eventval_list vt tyt;:
651    OK ? ((sig_eject ?? ev)::evt))
652  ]
653]. nwhd; //;
654napply sig_bind_OK; #ev eev Hev;
655napply sig_bind_OK; #evt eevt Hevt;
656nnormalize; /2/;
657nqed.
658
659(* execution *)
660
661nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
662match st with
663[ State f s k e m ⇒
664  match s with
665  [ Sassign a1 a2 ⇒ Some ? (
666    ! 〈loc, ofs〉 ← exec_lvalue ge e m a1;:
667    ! v2 ← exec_expr ge e m a2;:
668    ! m' ← store_value_of_type (typeof a1) m loc ofs v2;:
669    ret ? 〈E0, State f Sskip k e m'〉)
670  | Scall lhs a al ⇒ Some ? (
671    ! vf ← exec_expr ge e m a;:
672    ! vargs ← exec_exprlist ge e m al;:
673    ! fd ← find_funct ? ? ge vf;:
674    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a));:
675(*
676    ! k' ← match lhs with
677         [ None ⇒ ret ? (Kcall (None ?) f e k)
678         | Some lhs' ⇒
679           ! locofs ← exec_lvalue ge e m lhs';:
680           ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
681         ];:
682    ret ? 〈E0, Callstate fd vargs k' m〉)
683*)
684    match lhs with
685         [ None ⇒ ret ? 〈E0, Callstate fd vargs (Kcall (None ?) f e k) m〉
686         | Some lhs' ⇒
687           ! locofs ← exec_lvalue ge e m lhs';:
688           ret ? 〈E0, Callstate fd vargs (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k) m〉
689         ])
690  | Ssequence s1 s2 ⇒ Some ? (ret ? 〈E0, State f s1 (Kseq s2 k) e m〉)
691  | Sskip ⇒
692      match k with
693      [ Kseq s k' ⇒ Some ? (ret ? 〈E0, State  f s k' e m〉)
694      | Kstop ⇒
695          match fn_return f with
696          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
697          | _ ⇒ Some ? (Wrong ???)
698          ]
699      | Kcall _ _ _ _ ⇒
700          match fn_return f with
701          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
702          | _ ⇒ Some ? (Wrong ???)
703          ]
704      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
705      | Kdowhile a s' k' ⇒ Some ? (
706          ! v ← exec_expr ge e m a;:
707          ! b ← bool_of_val_3 v (typeof a);:
708          match b with
709          [ true ⇒ ret ? 〈E0, State f (Sdowhile a s') k' e m〉
710          | false ⇒ ret ? 〈E0, State f Sskip k' e m〉
711          ])
712      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
713      | Kfor3 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉)
714      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
715      | _ ⇒ Some ? (Wrong ???)
716      ]
717  | Scontinue ⇒
718      match k with
719      [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
720      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
721      | Kdowhile a s' k' ⇒ Some ? (
722          ! v ← exec_expr ge e m a;:
723          ! b ← bool_of_val_3 v (typeof a);:
724          match b with
725          [ true ⇒ ret ? 〈E0, State f (Sdowhile a s') k' e m〉
726          | false ⇒ ret ? 〈E0, State f Sskip k' e m〉
727          ])
728      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
729      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
730      | _ ⇒ Some ? (Wrong ???)
731      ]
732  | Sbreak ⇒
733      match k with
734      [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Sbreak k' e m〉)
735      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
736      | Kdowhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
737      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
738      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
739      | _ ⇒ Some ? (Wrong ???)
740      ]
741  | Sifthenelse a s1 s2 ⇒ Some ? (
742      ! v ← exec_expr ge e m a;:
743      ! b ← bool_of_val_3 v (typeof a);:
744      ret ? 〈E0, State f (if b then s1 else s2) k e m〉)
745  | Swhile a s' ⇒ Some ? (
746      ! v ← exec_expr ge e m a;:
747      ! b ← bool_of_val_3 v (typeof a);:
748      ret ? 〈E0, if b then State f s' (Kwhile a s' k) e m
749                     else State f Sskip k e m〉)
750  | Sdowhile a s' ⇒ Some ? (ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉)
751  | Sfor a1 a2 a3 s' ⇒
752      match is_Sskip a1 with
753      [ inl _ ⇒ Some ? (
754          ! v ← exec_expr ge e m a2;:
755          ! b ← bool_of_val_3 v (typeof a2);:
756          ret ? 〈E0, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
757      | inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉)
758      ]
759  | Sreturn a_opt ⇒
760    match a_opt with
761    [ None ⇒ match fn_return f with
762      [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
763      | _ ⇒ Some ? (Wrong ???)
764      ]
765    | Some a ⇒ Some ? (
766        ! u ← is_not_void (fn_return f);:
767        ! v ← exec_expr ge e m a;:
768        ret ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
769    ]
770  | Sswitch a sl ⇒ Some ? (
771      ! v ← exec_expr ge e m a;:
772      match v with [ Vint n ⇒ ret ? 〈E0, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
773                   | _ ⇒ Wrong ??? ])
774  | Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉)
775  | Sgoto lbl ⇒
776      match find_label lbl (fn_body f) (call_cont k) with
777      [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (ret ? 〈E0, State f s' k' e m〉) ]
778      | None ⇒ Some ? (Wrong ???)
779      ]
780  ]
781| Callstate f0 vargs k m ⇒
782  match f0 with
783  [ Internal f ⇒ Some ? (
784    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
785      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;:
786      ret ? 〈E0, State f (fn_body f) k e m2〉
787    ])
788  | External f argtys retty ⇒ Some ? (
789      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);:
790      ! evres ← do_io f evargs;:
791      ! vres ← check_eventval evres (proj_sig_res (signature_of_type argtys retty));:
792      ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉)
793  ]
794| Returnstate res k m ⇒
795  match k with
796  [ Kcall r f e k' ⇒
797    match r with
798    [ None ⇒
799      match res with
800      [ Vundef ⇒ Some ? (ret ? 〈E0, (State f Sskip k' e m)〉)
801      | _ ⇒ Some ? (Wrong ???)
802      ]
803    | Some r' ⇒
804      match r' with [ mk_pair locofs ty ⇒
805        match locofs with [ mk_pair loc ofs ⇒ Some ? (
806          ! m' ← store_value_of_type ty m loc ofs res;:
807          ret ? 〈E0, (State f Sskip k' e m')〉)
808        ]
809      ]
810    ]
811  | _ ⇒ Some ? (Wrong ???)
812  ]
813]. nwhd; //;
814##[ nrewrite > c7; napply step_skip_call; //; napply c8;
815##| napply step_skip_or_continue_while; @; //;
816##| napply sig_bindIO_OK; #v Hv;
817    napply sig_bindIO_OK; #b; ncases b; #Hb;
818    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
819      ##[ @; // ##| napply (bool_of … Hb); ##]
820    ##| napply (step_skip_or_continue_dowhile_false … Hv);
821      ##[ @; // ##| napply (bool_of … Hb); ##]
822    ##]
823##| napply step_skip_or_continue_for2; @; //;
824##| napply step_skip_break_switch; @; //;
825##| nrewrite > c11; napply step_skip_call; //; napply c12;
826##| napply sig_bindIO2_OK; #loc ofs Hlval;
827    napply sig_bindIO_OK; #v2 Hv2;
828    napply opt_bindIO_OK; #m' em';
829    nwhd; napply (step_assign … Hlval Hv2 em');
830##| napply sig_bindIO_OK; #vf Hvf;
831    napply sig_bindIO_OK; #vargs Hvargs;
832    napply opt_bindIO_OK; #fd efd;
833    napply bindIO_OK; #ety;
834    ncases c6; nwhd;
835    ##[ napply (step_call_none … Hvf Hvargs efd ety);
836    ##| #lhs';
837        napply sig_bindIO_OK; #locofs; ncases locofs; #loc ofs Hlocofs;
838        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
839    ##]
840##| napply sig_bindIO_OK; #v Hv;
841    napply sig_bindIO_OK; #b; ncases b; #Hb;
842    ##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb);
843    ##| napply (step_ifthenelse_false … Hv); napply (bool_of … Hb)
844    ##]
845##| napply sig_bindIO_OK; #v Hv;
846    napply sig_bindIO_OK; #b; ncases b; #Hb;
847    ##[ napply (step_while_true … Hv); napply (bool_of … Hb);
848    ##| napply (step_while_false … Hv); napply (bool_of … Hb);
849    ##]
850##| nrewrite > c11;
851    napply sig_bindIO_OK; #v Hv;
852    napply sig_bindIO_OK; #b; ncases b; #Hb;
853    ##[ napply (step_for_true … Hv); napply (bool_of … Hb);
854    ##| napply (step_for_false … Hv); napply (bool_of … Hb);
855    ##]
856##| napply step_for_start; //;
857##| napply step_skip_break_switch; @2; //;
858##| napply step_skip_or_continue_while; @2; //;
859##| napply sig_bindIO_OK; #v Hv;
860    napply sig_bindIO_OK; #b; ncases b; #Hb;
861    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
862      ##[ @2; // ##| napply (bool_of … Hb); ##]
863    ##| napply (step_skip_or_continue_dowhile_false … Hv);
864      ##[ @2; // ##| napply (bool_of … Hb); ##]
865    ##]
866##| napply step_skip_or_continue_for2; @2; //
867##| napply step_return_0; napply c9;
868##| napply sig_bindIO_OK; #u Hnotvoid;
869    napply sig_bindIO_OK; #v Hv;
870    nwhd; napply (step_return_1 … Hnotvoid Hv);
871##| napply sig_bindIO_OK; #v; ncases v; //; #n Hv;
872    napply step_switch; //;
873##| napply step_goto; nrewrite < c12; napply c9;
874##| napply extract_subset_pair_io; #e m1 ealloc Halloc;
875    napply sig_bindIO_OK; #m2 Hbind;
876    nwhd; napply (step_internal_function … Halloc Hbind);
877##| napply sig_bindIO_OK; #evs Hevs;
878    napply bindIO_OK; #eres;
879    napply sig_bindIO_OK; #res Hres;
880    nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##] 
881##| napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; //;
882##]
883nqed.
884
885nlet rec make_initial_state (p:program) : IO eventval io_out (Σs:state. initial_state p s) ≝
886  let ge ≝ globalenv Genv ?? p in
887  let m0 ≝ init_mem Genv ?? p in
888  Some ? (
889    ! b ← find_symbol ? ? ge (prog_main ?? p);:
890    ! f ← find_funct_ptr ? ? ge b;:
891    ret ? (Callstate f (nil ?) Kstop m0)).
892nwhd;
893napply opt_bindIO_OK; #b eb;
894napply opt_bindIO_OK; #f ef;
895nwhd; napply (initial_state_intro … eb ef);
896nqed.
897
898ndefinition is_final_state : ∀st:state. (∃r. final_state st r) + (¬∃r. final_state st r).
899#st; nelim st;
900##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
901##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
902##| #v k m; ncases k;
903  ##[ ncases v;
904    ##[ ##2: #i; @1; @ i; //;
905    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
906    ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
907    ##| #b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
908    ##]
909  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
910  ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
911  ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
912  ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
913  ##]
914##] nqed.
915
916nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
917 IO eventval io_out (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
918match is_final_state s with
919[ inl _ ⇒ Some ? (ret ? 〈E0, s〉)
920| inr _ ⇒
921  match n with
922  [ O ⇒ Some ? (ret ? 〈E0, s〉)
923  | S n' ⇒ Some ? (
924      ! 〈t,s'〉 ← exec_step ge s;:
925      ! 〈t',s''〉 ← exec_steps n' ge s';:
926      ret ? 〈t ⧺ t',s''〉)
927  ]
928]. nwhd; /2/;
929napply sig_bindIO2_OK; #t s' H1;
930napply sig_bindIO2_OK; #t' s'' IH;
931nwhd; napply (star_step … IH); //;
932nqed.
933(*
934nlet rec exec_steps_without_proof (n:nat) (ge:genv) (s:state) :
935 res (trace×state) ≝
936match is_final_state s with
937[ inl _ ⇒ OK ? 〈E0, s〉
938| inr _ ⇒
939  match n with
940  [ O ⇒ OK ? 〈E0, s〉
941  | S n' ⇒
942      〈t,s'〉 ← exec_step ge s;:
943      〈t',s''〉 ← exec_steps_without_proof n' ge s';:
944      OK ? 〈t ⧺ t',s''〉
945  ]
946].
947*)
Note: See TracBrowser for help on using the repository browser.