source: C-semantics/Cexec.ma @ 13

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

Minor syntactic changes.

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