source: C-semantics/Cexec.ma @ 9

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

Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.

File size: 26.0 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
287(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
288   a structurally smaller value, we break out the surrounding Expr constructor
289   and use exec_lvalue'. *)
290
291nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val. eval_expr ge en m e r) ≝
292match e with
293[ Expr e' ty ⇒
294  match e' with
295  [ Econst_int i ⇒ Some ? (OK ? (Vint i))
296  | Econst_float f ⇒ Some ? (OK ? (Vfloat f))
297  | Evar _ ⇒ Some ? (
298      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
299      opt_to_res ? (load_value_of_type ty m loc ofs))
300  | Ederef _ ⇒ Some ? (
301      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
302      opt_to_res ? (load_value_of_type ty m loc ofs))
303  | Eaddrof a ⇒ Some ? (
304      〈loc, ofs〉 ← exec_lvalue ge en m a;:
305      OK ? (Vptr loc ofs))
306  | Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty'))))
307  | Eunop op a ⇒ Some ? (
308      v1 ← exec_expr ge en m a;:
309      opt_to_res ? (sem_unary_operation op v1 (typeof a)))
310  | Ebinop op a1 a2 ⇒ Some ? (
311      v1 ← exec_expr ge en m a1;:
312      v2 ← exec_expr ge en m a2;:
313      opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m))
314  | Econdition a1 a2 a3 ⇒ Some ? (
315      v ← exec_expr ge en m a1;:
316      b ← bool_of_val_3 v (typeof a1);:
317      match b return λ_.res val with [ true ⇒ (exec_expr ge en m a2) | false ⇒ (exec_expr ge en m a3) ])
318(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
319  | _ ⇒ Some ? (Error ?)
320  ]
321]
322and 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)) ≝
323  match e' with
324  [ Evar id ⇒ Some ? (
325      l ← opt_to_res ? (get ? PTree ? id en);:
326      OK ? 〈l, zero〉)
327  | Ederef a ⇒ Some ? (
328      v ← exec_expr ge en m a;:
329      match v with
330      [ Vptr l ofs ⇒ OK ? 〈l,ofs〉
331      | _ ⇒ Error ?
332      ])
333  | _ ⇒ Some ? (Error ?)
334  ]
335and 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)) ≝
336match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
337nwhd; //;
338##[ napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
339    napply opt_OK;  #v ev; /2/;
340##| napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
341    napply opt_OK;  #v ev; /2/;
342##| napply sig_bind2_OK; #loc ofs H;
343    nwhd; napply eval_Eaddrof; //;
344##| napply sig_bind_OK; #v1 ev1 Hv1;
345    napply opt_OK; #v ev;
346    napply (eval_Eunop … Hv1 ev);
347##| napply sig_bind_OK; #v1 ev1 Hv1;
348    napply sig_bind_OK; #v2 ev2 Hv2;
349    napply opt_OK; #v ev;
350    napply (eval_Ebinop … Hv1 Hv2 ev);
351##| napply sig_bind_OK; #vb evb Hvb;
352    napply sig_bind_OK; #b;
353    ncases b; #eb Hb; napply reinject; #v ev Hv;
354    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
355    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
356    ##]
357##| napply opt_bind_OK; #l el; napply eval_Evar_local; //
358##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
359    napply eval_Ederef; //
360
361##] nqed.
362
363(* TODO: Can we do this sensibly with a map combinator? *)
364nlet 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) ≝
365match l with
366[ nil ⇒ Some ? (OK ? (nil val))
367| cons e1 es ⇒ Some ? (
368  v ← exec_expr ge e m e1;:
369  vs ← exec_exprlist ge e m es;:
370  OK ? (cons val v vs))
371]. nwhd; //;
372napply sig_bind_OK; #v ev Hv;
373napply sig_bind_OK; #vs evs Hvs;
374nnormalize; /2/;
375nqed.
376
377(* Don't really want to use subset rather than sigma here, but can't be bothered
378   with *another* set of coercions. XXX: why do I have to get the recursive
379   call's property manually? *)
380
381nlet 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) } ≝
382match l with
383[ nil ⇒ Some ? 〈en, m〉
384| cons h vars ⇒
385  match h with [ mk_pair id ty ⇒
386    match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒
387      match exec_alloc_variables (set ? PTree ? id b1 en) m1 vars with
388      [ sig_intro r p ⇒ r ]
389]]]. nwhd; //;
390nelim (exec_alloc_variables (set ident PTree block c3 c7 en) c6 c1);
391#H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
392napply (alloc_variables_cons … IH); /2/;
393nqed.
394
395(* TODO: can we establish that length params = length vs in advance? *)
396nlet 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) ≝
397  match params with
398  [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ]
399  | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒
400      match vs with
401      [ nil ⇒ Some ? (Error ?)
402      | cons v1 vl ⇒ Some ? (
403          b ← opt_to_res ? (get ? PTree ? id e);:
404          m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:
405          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
406      ]
407  ] ].
408nwhd; //;
409napply opt_bind_OK; #b eb;
410napply opt_bind_OK; #m1 em1;
411napply reinject; #m2 em2 Hm2;
412napply (bind_parameters_cons … eb em1 Hm2);
413nqed.
414
415ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝
416λt. match t with
417[ Tvoid ⇒ Some ? (Error ?)
418| _ ⇒ Some ? (OK ??)
419]. nwhd; //; @; #H; ndestruct; nqed.
420
421ninductive decide : Type ≝
422| dy : decide | dn : decide.
423
424ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P.
425#P d;ncases d;/2/; nqed.
426
427ncoercion decide_inject :
428  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P ≝ dodecide
429  on d:decide to ? + (¬?).
430
431alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
432alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
433ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
434#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
435ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
436#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
437ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
438#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
439
440(* Not very happy about this. *)
441nlet rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
442match t1 with
443[ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ]
444| 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 ]
445| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
446| Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
447| Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒
448    match type_eq_dec t t' with [ inl _ ⇒
449      match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]
450| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match typelist_eq_dec tl tl' with [ inl _ ⇒
451    match type_eq_dec t t' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ]
452| Tstruct i fl ⇒
453    match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
454      match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
455| Tunion i fl ⇒
456    match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
457      match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
458| Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
459]
460and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
461match tl1 with
462[ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ]
463| Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒
464    match type_eq_dec t1 t2 with [ inl _ ⇒
465      match typelist_eq_dec ts1 ts2 with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
466]
467and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
468match fl1 with
469[ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ]
470| Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒
471    match ident_eq i1 i2 with [ inl _ ⇒
472      match type_eq_dec t1 t2 with [ inl _ ⇒
473        match fieldlist_eq_dec fs1 fs2 with [ inl _ ⇒ dy | _ ⇒ dn ]
474        | _ ⇒ dn ] | _ ⇒ dn ] ]
475].
476(* A poor man's clear, otherwise automation picks up recursive calls without
477   checking that the argument is smaller. *)
478ngeneralize in type_eq_dec;
479ngeneralize in typelist_eq_dec;
480ngeneralize in fieldlist_eq_dec; #avoid1 avoid2 avoid3 avoid4 avoid5 avoid6;
481ndestruct; //; @; #H; ndestruct;
482##[ nelim c8; /2/
483##| nelim c6; /2/
484##| nelim c4; /2/
485##| nelim c4; /2/
486##| nelim c8; /2/
487##| nelim c6; /2/
488##| nelim c8; /2/
489##| nelim c6; /2/
490##| nelim c8; /2/
491##| nelim c6; /2/
492##| nelim c8; /2/
493##| nelim c6; /2/
494##| nelim c4; /2/
495##| nelim c8; /2/
496##| nelim c6; /2/
497##| nelim c12; /2/
498##| nelim c10; /2/
499##| nelim c8; /2/
500##] nqed.
501
502ndefinition are_equal : ∀A:Type. (∀x,y:A.(x=y)+(x≠y)) → ∀x,y:A. res (x=y) ≝
503λA,dec,x,y.
504match dec … x y with
505[ inl p ⇒ OK ? p
506| inr _ ⇒ Error ?
507].
508
509nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
510match k with
511[ Kstop ⇒ dy
512| Kcall _ _ _ _ ⇒ dy
513| _ ⇒ dn
514]. nwhd; //; @; #H; nelim H; nqed.
515
516nlet rec exec_step (ge:genv) (st:state) on st : res (Σr:trace × state. step ge st (\fst r) (\snd r)) ≝
517match st with
518[ State f s k e m ⇒
519  match s with
520  [ Sassign a1 a2 ⇒ Some ? (
521    〈loc, ofs〉 ← exec_lvalue ge e m a1;:
522    v2 ← exec_expr ge e m a2;:
523    m' ← opt_to_res ? (store_value_of_type (typeof a1) m loc ofs v2);:
524    OK ? 〈E0, State f Sskip k e m'〉)
525  | Scall lhs a al ⇒ Some ? (
526    vf ← exec_expr ge e m a;:
527    vargs ← exec_exprlist ge e m al;:
528    fd ← opt_to_res ? (find_funct Genv ? ge vf);:
529    p ← are_equal ? type_eq_dec (type_of_fundef fd) (typeof a);:
530    k' ← match lhs with
531         [ None ⇒ OK ? (Kcall (None ?) f e k)
532         | Some lhs' ⇒
533           locofs ← exec_lvalue ge e m lhs';:
534           OK ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
535         ];:
536    OK ? 〈E0, Callstate fd vargs k' m〉)
537  | Ssequence s1 s2 ⇒ Some ? (OK ? 〈E0, State f s1 (Kseq s2 k) e m〉)
538  | Sskip ⇒
539      match k with
540      [ Kseq s k' ⇒ Some ? (OK ? 〈E0, State  f s k' e m〉)
541      | Kstop ⇒
542          match fn_return f with
543          [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
544          | _ ⇒ Some ? (Error ?)
545          ]
546      | Kcall _ _ _ _ ⇒
547          match fn_return f with
548          [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
549          | _ ⇒ Some ? (Error ?)
550          ]
551      | _ ⇒ Some ? (Error ?) (* TODO more *)
552      ]
553  | Sreturn a_opt ⇒
554    match a_opt with
555    [ None ⇒ match fn_return f with
556      [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
557      | _ ⇒ Some ? (Error ?)
558      ]
559    | Some a ⇒ Some ? (
560        u ← is_not_void (fn_return f);:
561        v ← exec_expr ge e m a;:
562        OK ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
563    ]
564  | _ ⇒ Some ? (Error ?)
565  ]
566| Callstate f0 vargs k m ⇒
567  match f0 with
568  [ Internal f ⇒ Some ? (
569    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
570      m2 ← exec_bind_parameters e m1 (fn_params f) vargs;:
571      OK ? 〈E0, State f (fn_body f) k e m2〉
572    ])
573  | _ ⇒ Some ? (Error ?)
574  ]
575| _ ⇒ Some ? (Error ?)
576]. nwhd; //;
577##[ nrewrite > c7; napply step_skip_call; //; napply c8;
578##| nrewrite > c11; napply step_skip_call; //; napply c12;
579##| napply sig_bind2_OK; #loc ofs Hlval;
580    napply sig_bind_OK; #v2 ev2 Hv2;
581    napply opt_bind_OK; #m' em';
582    nwhd; napply (step_assign … Hlval Hv2 em');
583##| napply sig_bind_OK; #vf evf Hvf;
584    napply sig_bind_OK; #vargs evargs Hvargs;
585    napply opt_bind_OK; #fd efd;
586    napply bind_OK; #ety ety';
587    ncases c6; nwhd;
588    ##[ napply (step_call_none … Hvf Hvargs efd ety);
589    ##| #lhs'; nrewrite > (bind_assoc_r …);
590        napply sig_bind_OK; #locofs; ncases locofs; #loc ofs elocofs Hlocofs;
591        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
592    ##]
593##| napply step_return_0; napply c9;
594##| napply sig_bind_OK; #u eu Hnotvoid;
595    napply sig_bind_OK; #v ev Hv;
596    nwhd; napply (step_return_1 … Hnotvoid Hv);
597##| napply extract_subset_pair; #e m1 ealloc Halloc;
598    napply sig_bind_OK; #m2 em1 Hbind;
599    nwhd; napply (step_internal_function … Halloc Hbind);
600##]
601nqed.
602
603nlet rec make_initial_state (p:program) : res (Σs:state. initial_state p s) ≝
604  let ge ≝ globalenv Genv ?? p in
605  let m0 ≝ init_mem Genv ?? p in
606  Some ? (
607    b ← opt_to_res ? (find_symbol Genv ? ge (prog_main ?? p));:
608    f ← opt_to_res ? (find_funct_ptr Genv ? ge b);:
609    OK ? (Callstate f (nil ?) Kstop m0)).
610nwhd;
611napply opt_bind_OK; #b eb;
612napply opt_bind_OK; #f ef;
613nwhd; napply (initial_state_intro … eb ef);
614nqed.
615
616ndefinition is_final_state : ∀st:state. (∃r. final_state st r) + (¬∃r. final_state st r).
617#st; nelim st;
618##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
619##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
620##| #v k m; ncases k;
621  ##[ ncases v;
622    ##[ ##2: #i; @1; @ i; //;
623    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
624    ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
625    ##| #b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
626    ##]
627  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
628  ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
629  ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
630  ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
631  ##]
632##] nqed.
633
634nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
635 res (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
636match is_final_state s with
637[ inl _ ⇒ Some ? (OK ? 〈E0, s〉)
638| inr _ ⇒
639  match n with
640  [ O ⇒ Some ? (OK ? 〈E0, s〉)
641  | S n' ⇒ Some ? (
642      〈t,s'〉 ← exec_step ge s;:
643      〈t',s''〉 ← exec_steps n' ge s';:
644      OK ? 〈t ⧺ t',s''〉)
645  ]
646]. nwhd; /2/;
647napply sig_bind2_OK; #t s' H1;
648napply sig_bind2_OK; #t' s'' IH;
649nwhd; napply (star_step … IH); //;
650nqed.
Note: See TracBrowser for help on using the repository browser.