source: C-semantics/Cexec.ma @ 17

Last change on this file since 17 was 17, checked in by campbell, 10 years ago

Remainder of the statements for the executable semantics (except for
"external" function calls, which can do I/O).

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