source: C-semantics/Cexec.ma @ 5

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

Add a few execution steps and calculation of the initial state to the
"executable" C semantics.

File size: 17.6 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_OK: ∀A,B,P,e,f.
224  (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
225  match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ].
226#A B P e f; nelim e; /2/; nqed.
227
228nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B.
229  (∀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'] ) →
230  match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
231#A B P P' e f; nelim e; //;
232#v0; nelim v0; #v Hv IH; napply IH; //; nqed.
233
234nlemma bind2_OK: ∀A,B,C,P,e,f.
235  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) →
236  match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ].
237#A B C P e f; nelim e; //; #v; ncases v; /2/; nqed.
238
239nlemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (sigma (A×B) P). ∀f:A → B → res C.
240  (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
241  match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
242#A B C P P' e f; nelim e; //;
243#v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.
244
245nlemma reinject: ∀A. ∀P,P':A → Prop. ∀e:res (sigma A P').
246  (∀v:A. err_eq A P' e v → P' v → P v) →
247  match err_eject A P' e with [ Error ⇒ True | OK v' ⇒ P v' ].
248#A P P' e; ncases e; //;
249#v0; nelim v0; #v Pv' IH; /2/;
250nqed.
251
252nlemma bool_val_distinct: Vtrue ≠ Vfalse.
253@; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero);
254nqed.
255
256nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
257  if b then is_true v ty else is_false v ty.
258#v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //;
259napply False_ind; napply (absurd ? ev ?);
260##[ ##2: napply sym_neq ##] napply bool_val_distinct;
261nqed.
262
263ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
264nlemma opt_OK: ∀A,P,e.
265  (∀v. e = Some ? v → P v) →
266  match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
267#A P e; nelim e; /2/;
268nqed.
269
270nlemma opt_bind_OK: ∀A,B,P,e,f.
271  (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
272  match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ].
273#A B P e f; nelim e; nnormalize; /2/; nqed.
274
275nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop.
276  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) →
277  match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ].
278#A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
279##[ #H; napply (False_ind … H);
280##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
281##] nqed.
282
283(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
284   a structurally smaller value, we break out the surrounding Expr constructor
285   and use exec_lvalue'. *)
286
287nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val. eval_expr ge en m e r) ≝
288match e with
289[ Expr e' ty ⇒
290  match e' with
291  [ Econst_int i ⇒ Some ? (OK ? (Vint i))
292  | Evar _ ⇒ Some ? (
293      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
294      opt_to_res ? (load_value_of_type ty m loc ofs))
295  | Eaddrof a ⇒ Some ? (
296      〈loc, ofs〉 ← exec_lvalue ge en m a;:
297      OK ? (Vptr loc ofs))
298  | Eunop op a ⇒ Some ? (
299      v1 ← exec_expr ge en m a;:
300      opt_to_res ? (sem_unary_operation op v1 (typeof a)))
301  | Econdition a1 a2 a3 ⇒ Some ? (
302      v ← exec_expr ge en m a1;:
303      b ← bool_of_val_3 v (typeof a1);:
304      match b return λ_.res val with [ true ⇒ (exec_expr ge en m a2) | false ⇒ (exec_expr ge en m a3) ])
305(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
306  | _ ⇒ Some ? (Error ?)
307  ]
308]
309and 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)) ≝
310  match e' with
311  [ Evar id ⇒ Some ? (
312      l ← opt_to_res ? (get ? PTree ? id en);:
313      OK ? 〈l, zero〉)
314  | _ ⇒ Some ? (Error ?)
315  ]
316and 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)) ≝
317match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
318nwhd; //;
319##[ napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H;
320    napply opt_OK;  #v ev; /2/;
321##| napply sig_bind2_OK; #loc ofs H;
322    nwhd; napply eval_Eaddrof; //;
323##| napply sig_bind_OK; #v1 ev1 Hv1;
324    napply opt_OK; #v ev;
325    napply (eval_Eunop … Hv1 ev);
326##| napply sig_bind_OK; #vb evb Hvb;
327    napply sig_bind_OK; #b;
328    ncases b; #eb Hb; napply reinject; #v ev Hv;
329    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
330    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
331    ##]
332##| napply opt_bind_OK; #l el; napply eval_Evar_local; //
333##] nqed.
334
335(* Don't really want to use subset rather than sigma here, but can't be bothered
336   with *another* set of coercions. XXX: why do I have to get the recursive
337   call's property manually? *)
338
339nlet 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) } ≝
340match l with
341[ nil ⇒ Some ? 〈en, m〉
342| cons h vars ⇒
343  match h with [ mk_pair id ty ⇒
344    match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒
345      match exec_alloc_variables (set ? PTree ? id b1 en) m1 vars with
346      [ sig_intro r p ⇒ r ]
347]]]. nwhd; //;
348nelim (exec_alloc_variables (set ident PTree block c3 c7 en) c6 c1);
349#H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
350napply (alloc_variables_cons … IH); /2/;
351nqed.
352
353(* TODO: can we establish that length params = length vs in advance? *)
354nlet 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) ≝
355  match params with
356  [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ]
357  | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒
358      match vs with
359      [ nil ⇒ Some ? (Error ?)
360      | cons v1 vl ⇒ Some ? (
361          b ← opt_to_res ? (get ? PTree ? id e);:
362          m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:
363          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
364      ]
365  ] ].
366nwhd; //;
367napply opt_bind_OK; #b eb;
368napply opt_bind_OK; #m1 em1;
369napply reinject; #m2 em2 Hm2;
370napply (bind_parameters_cons … eb em1 Hm2);
371nqed.
372
373ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝
374λt. match t with
375[ Tvoid ⇒ Some ? (Error ?)
376| _ ⇒ Some ? (OK ??)
377]. nwhd; //; @; #H; ndestruct; nqed.
378
379nlet rec exec_step (ge:genv) (st:state) on st : res (Σr:trace × state. step ge st (\fst r) (\snd r)) ≝
380match st with
381[ State f s k e m ⇒
382  match s with
383  [ Sassign a1 a2 ⇒ Some ? (
384    〈loc, ofs〉 ← exec_lvalue ge e m a1;:
385    v2 ← exec_expr ge e m a2;:
386    m' ← opt_to_res ? (store_value_of_type (typeof a1) m loc ofs v2);:
387    OK ? 〈E0, State f Sskip k e m'〉)
388  | Sreturn a_opt ⇒
389    match a_opt with
390    [ None ⇒ match fn_return f with
391      [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
392      | _ ⇒ Some ? (Error ?)
393      ]
394    | Some a ⇒ Some ? (
395        u ← is_not_void (fn_return f);:
396        v ← exec_expr ge e m a;:
397        OK ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
398    ]
399  | _ ⇒ Some ? (Error ?)
400  ]
401| Callstate f0 vargs k m ⇒
402  match f0 with
403  [ Internal f ⇒ Some ? (
404    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
405      m2 ← exec_bind_parameters e m1 (fn_params f) vargs;:
406      OK ? 〈E0, State f (fn_body f) k e m2〉
407    ])
408  | _ ⇒ Some ? (Error ?)
409  ]
410| _ ⇒ Some ? (Error ?)
411]. nwhd; //;
412##[ napply sig_bind2_OK; #loc ofs Hlval;
413    napply sig_bind_OK; #v2 ev2 Hv2;
414    napply opt_bind_OK; #m' em';
415    nwhd; napply (step_assign … Hlval Hv2 em');
416##| napply step_return_0; napply c9;
417##| napply sig_bind_OK; #u eu Hnotvoid;
418    napply sig_bind_OK; #v ev Hv;
419    nwhd; napply (step_return_1 … Hnotvoid Hv);
420##| napply extract_subset_pair; #e m1 ealloc Halloc;
421    napply sig_bind_OK; #m2 em1 Hbind;
422    nwhd; napply (step_internal_function … Halloc Hbind);
423##]
424nqed.
425
426nlet rec make_initial_state (p:program) : res (Σs:state. initial_state p s) ≝
427  let ge ≝ globalenv Genv ?? p in
428  let m0 ≝ init_mem Genv ?? p in
429  Some ? (
430    b ← opt_to_res ? (find_symbol Genv ? ge (prog_main ?? p));:
431    f ← opt_to_res ? (find_funct_ptr Genv ? ge b);:
432    OK ? (Callstate f (nil ?) Kstop m0)).
433nwhd;
434napply opt_bind_OK; #b eb;
435napply opt_bind_OK; #f ef;
436nwhd; napply (initial_state_intro … eb ef);
437nqed.
Note: See TracBrowser for help on using the repository browser.