source: C-semantics/CexecIO.ma @ 127

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

Allow the storage of pointers in suitably large integers.

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