source: src/Clight/Cexec.ma @ 694

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

Separate out whole program executions from the clight semantics and start
setting it up for RTLabs too.

File size: 29.5 KB
Line 
1
2
3include "extralib.ma".
4include "IOMonad.ma".
5include "SmallstepExec.ma".
6include "Csem.ma".
7
8(*
9include "Plogic/russell_support.ma".
10*)
11definition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝
12  λA,P,a.match a with [ None ⇒ False | Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True | OK z ⇒ P z ]].
13
14definition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (Sig A P) ≝
15  λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a.
16  (match a return λa'.a=a' → res (Sig A P) with
17   [ None ⇒ λe1.?
18   | Some b ⇒ λe1.(match b return λb'.b=b' → ? with
19     [ Error ⇒ λ_. Error ?
20     | OK c ⇒ λe2. OK ? (dp A P c ?)
21     ]) (refl ? b)
22   ]) (refl ? a).
23[ >e1 in p; normalize; *;
24| >e1 in p >e2 normalize; //
25] qed.
26
27definition err_eject : ∀A.∀P: A → Prop. res (Sig A P) → res A ≝
28  λA,P,a.match a with [ Error ⇒ Error ? | OK b ⇒
29    match b with [ dp w p ⇒ OK ? w] ].
30
31definition sig_eject : ∀A.∀P: A → Prop. Sig A P → A ≝
32  λA,P,a.match a with [ dp w p ⇒ w].
33
34coercion err_inject :
35  ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (Sig A P) ≝ err_inject
36  on a:option (res ?) to res (Sig ? ?).
37coercion err_eject : ∀A.∀P:A → Prop.∀c:res (Sig A P).res A ≝ err_eject
38  on _c:res (Sig ? ?) to res ?.
39coercion sig_eject : ∀A.∀P:A → Prop.∀c:Sig A P.A ≝ sig_eject
40  on _c:Sig ? ? to ?.
41
42definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
43  λA,P,a. match a with [ Error ⇒ True | OK v ⇒ P v ].
44
45definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
46  λv,ty. match v in val with
47  [ Vint i ⇒ match ty with
48    [ Tint _ _ ⇒ OK ? (¬eq i zero)
49    | _ ⇒ Error ?
50    ]
51  | Vfloat f ⇒ match ty with
52    [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero)
53    | _ ⇒ Error ?
54    ]
55  | Vptr _ _ _ _ ⇒ match ty with
56    [ Tpointer _ _ ⇒ OK ? true
57    | _ ⇒ Error ?
58    ]
59  | Vnull _ ⇒ match ty with
60    [ Tpointer _ _ ⇒ OK ? false
61    | _ ⇒ Error ?
62    ]
63  | _ ⇒ Error ?
64  ].
65
66lemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b.
67#v #ty #r #H elim H; #v #t #H' elim H';
68  [ #i #is #s #ne %{ true} % //; whd in ⊢ (??%?); >(eq_false … ne) //;
69  | #r #b #pc #i #i0 #s %{ true} % //
70  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
71  | #i #s %{ false} % //;
72  | #r #r' #t %{ false} % //;
73  | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;
74  ]
75qed.
76
77(* Prove a few minor results to make proof obligations easy. *)
78
79lemma bind_OK: ∀A,B,P,e,f.
80  (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
81  match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ].
82#A #B #P #e #f elim e; /2/; qed.
83
84lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
85  (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
86  match bind (Sig A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
87#A #B #P #P' #e #f elim e;
88[ #v0 elim v0; #v #Hv #IH @IH
89| #_ @I
90] qed.
91
92lemma bind2_OK: ∀A,B,C,P,e,f.
93  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) →
94  match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ].
95#A #B #C #P #e #f elim e; //; #v cases v; /2/; qed.
96
97lemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (Sig (A×B) P). ∀f:A → B → res C.
98  (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
99  match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
100#A #B #C #P #P' #e #f elim e; //;
101#v0 elim v0; #v elim v; #v1 #v2 #Hv #IH @IH //; qed.
102
103lemma opt_bind_OK: ∀A,B,P,e,f.
104  (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
105  match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ].
106#A #B #P #e #f elim e; normalize; /2/; qed.
107(*
108lemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop.
109  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) →
110  match match eject ?? e with [ pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ].
111#A #B #C #P #e #Q #R cases e; #e' cases e'; normalize;
112[ #H @(False_ind … H)
113| #e'' cases e''; #a #b #Pab #H normalize; /2/;
114] qed.
115*)
116(*
117nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B.
118#A #B #e cases e; //; qed.
119*)
120
121definition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val  ≝
122λm:mem. λi:int. λty:type. λty':type.
123match eq i zero with
124[ true ⇒
125  match ty with
126  [ Tint _ _ ⇒
127    match ty' with
128    [ Tpointer r _ ⇒ OK ? (Vnull r)
129    | Tarray r _ _ ⇒ OK ? (Vnull r)
130    | Tfunction _ _ ⇒ OK ? (Vnull Code)
131    | _ ⇒ Error ?
132    ]
133  | _ ⇒ Error ?
134  ]
135| false ⇒ Error ?
136].
137
138definition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
139λm:mem. λv:val. λty:type. λty':type.
140match v with
141[ Vint i ⇒
142  match ty with
143  [ Tint sz1 si1 ⇒
144    match ty' with
145    [ Tint sz2 si2 ⇒ OK ? (Vint (cast_int_int sz2 si2 i))
146    | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
147    | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
148    | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
149    | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
150    | _ ⇒ Error ?
151    ]
152  | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
153  | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
154  | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
155  | _ ⇒ Error ?
156  ]
157| Vfloat f ⇒
158  match ty with
159  [ Tfloat sz ⇒
160    match ty' with
161    [ Tint sz' si' ⇒ OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f)))
162    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
163    | _ ⇒ Error ?
164    ]
165  | _ ⇒ Error ?
166  ]
167| Vptr r b _ ofs ⇒
168    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
169    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? ];
170    do s' ← match ty' with
171         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
172         | _ ⇒ Error ? ];
173    match pointer_compat_dec b s' with
174    [ inl p' ⇒ OK ? (Vptr s' b p' ofs)
175    | inr _ ⇒ Error ?
176    ]
177| Vnull r ⇒
178    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ];
179    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? ];
180    do s' ← match ty' with
181         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
182         | _ ⇒ Error ? ];
183    OK ? (Vnull s')
184| _ ⇒ Error ?
185].
186
187definition load_value_of_type' ≝
188λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
189
190(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
191   a structurally smaller value, we break out the surrounding Expr constructor
192   and use exec_lvalue'. *)
193
194let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
195match e with
196[ Expr e' ty ⇒
197  match e' with
198  [ Econst_int i ⇒ OK ? 〈Vint i, E0〉
199  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉
200  | Evar _ ⇒
201      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
202      do v ← opt_to_res ? (load_value_of_type' ty m l);
203      OK ? 〈v,tr〉
204  | Ederef _ ⇒
205      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
206      do v ← opt_to_res ? (load_value_of_type' ty m l);
207      OK ? 〈v,tr〉
208  | Efield _ _ ⇒
209      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
210      do v ← opt_to_res ? (load_value_of_type' ty m l);
211      OK ? 〈v,tr〉
212  | Eaddrof a ⇒
213      do 〈lo,tr〉 ← exec_lvalue ge en m a;
214      match ty with
215      [ Tpointer r _ ⇒
216        match lo with [ pair loc ofs ⇒
217          match pointer_compat_dec loc r with
218          [ inl pc ⇒ OK ? 〈Vptr r loc pc ofs, tr〉
219          | inr _ ⇒ Error ?
220          ]
221        ]
222      | _ ⇒ Error ?
223      ]
224  | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉
225  | Eunop op a ⇒
226      do 〈v1,tr〉 ← exec_expr ge en m a;
227      do v ← opt_to_res ? (sem_unary_operation op v1 (typeof a));
228      OK ? 〈v,tr〉
229  | Ebinop op a1 a2 ⇒
230      do 〈v1,tr1〉 ← exec_expr ge en m a1;
231      do 〈v2,tr2〉 ← exec_expr ge en m a2;
232      do v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
233      OK ? 〈v,tr1⧺tr2〉
234  | Econdition a1 a2 a3 ⇒
235      do 〈v,tr1〉 ← exec_expr ge en m a1;
236      do b ← exec_bool_of_val v (typeof a1);
237      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
238                 [ true ⇒ (exec_expr ge en m a2)
239                 | false ⇒ (exec_expr ge en m a3) ];
240      OK ? 〈v',tr1⧺tr2〉
241(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
242  | Eorbool a1 a2 ⇒
243      do 〈v1,tr1〉 ← exec_expr ge en m a1;
244      do b1 ← exec_bool_of_val v1 (typeof a1);
245      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
246        do 〈v2,tr2〉 ← exec_expr ge en m a2;
247        do b2 ← exec_bool_of_val v2 (typeof a2);
248        OK ? 〈of_bool b2, tr1⧺tr2〉 ]
249  | Eandbool a1 a2 ⇒
250      do 〈v1,tr1〉 ← exec_expr ge en m a1;
251      do b1 ← exec_bool_of_val v1 (typeof a1);
252      match b1 return λ_.res (val×trace) with [ true ⇒
253        do 〈v2,tr2〉 ← exec_expr ge en m a2;
254        do b2 ← exec_bool_of_val v2 (typeof a2);
255        OK ? 〈of_bool b2, tr1⧺tr2〉
256      | false ⇒ OK ? 〈Vfalse,tr1〉 ]
257  | Ecast ty' a ⇒
258      do 〈v,tr〉 ← exec_expr ge en m a;
259      do v' ← exec_cast m v (typeof a) ty';
260      OK ? 〈v',tr〉
261  | Ecost l a ⇒
262      do 〈v,tr〉 ← exec_expr ge en m a;
263      OK ? 〈v,tr⧺(Echarge l)〉
264  ]
265]
266and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
267  match e' with
268  [ Evar id ⇒
269      match (get … id en) with
270      [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
271      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
272      ]
273  | Ederef a ⇒
274      do 〈v,tr〉 ← exec_expr ge en m a;
275      match v with
276      [ Vptr _ l _ ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
277      | _ ⇒ Error ?
278      ]
279  | Efield a i ⇒
280      match (typeof a) with
281      [ Tstruct id fList ⇒
282          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
283          do delta ← field_offset i fList;
284          OK ? 〈〈\fst lofs,shift_offset (\snd lofs) (repr delta)〉,tr〉
285      | Tunion id fList ⇒
286          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
287          OK ? 〈lofs,tr〉
288      | _ ⇒ Error ?
289      ]
290  | _ ⇒ Error ?
291  ]
292and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
293match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
294
295lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
296#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
297
298(* We define a special induction principle tailored to the recursive definition
299   above. *)
300
301definition is_not_lvalue: expr_descr → Prop ≝
302λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
303
304definition Plvalue ≝ λP:(expr → Prop).λe,ty.
305match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
306
307(* TODO: Can we do this sensibly with a map combinator? *)
308let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
309match l with
310[ nil ⇒ OK ? 〈nil val, E0〉
311| cons e1 es ⇒
312  do 〈v,tr1〉 ← exec_expr ge e m e1;
313  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
314  OK ? 〈cons val v vs, tr1⧺tr2〉
315].
316
317let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝
318match l with
319[ nil ⇒ 〈en, m〉
320| cons h vars ⇒
321  match h with [ pair id ty ⇒
322    match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒
323      exec_alloc_variables (set … id b1 en) m1 vars
324]]].
325
326(* TODO: can we establish that length params = length vs in advance? *)
327let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
328  match params with
329  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? ]
330  | cons idty params' ⇒ match idty with [ pair id ty ⇒
331      match vs with
332      [ nil ⇒ Error ?
333      | cons v1 vl ⇒
334          do b ← opt_to_res ? (get … id e);
335          do m1 ← opt_to_res ? (store_value_of_type ty m b zero_offset v1);
336          exec_bind_parameters e m1 params' vl
337      ]
338  ] ].
339
340definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
341#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
342definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
343#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
344definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
345#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
346
347let rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝
348match t1 return λt'. (t' = t2) + (t' ≠ t2) with
349[ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
350| Tint sz sg ⇒ match t2 return λt'. (Tint ?? = t') + (Tint ?? ≠ t')  with [ Tint sz' sg' ⇒
351    match sz_eq_dec sz sz' with [ inl e1 ⇒
352    match sg_eq_dec sg sg' with [ inl e2 ⇒ inl ???
353    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
354    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
355    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
356| Tfloat f ⇒ match t2 return λt'. (Tfloat ? = t') + (Tfloat ? ≠ t')  with [ Tfloat f' ⇒
357    match fs_eq_dec f f' with [ inl e1 ⇒ inl ???
358    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
359    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
360| Tpointer s t ⇒ match t2 return λt'. (Tpointer ?? = t') + (Tpointer ?? ≠ t')  with [ Tpointer s' t' ⇒
361    match eq_region_dec s s' with [ inl e1 ⇒
362      match type_eq_dec t t' with [ inl e2 ⇒ inl ???
363      | inr e2 ⇒ inr ?? (nmk ? (λH.match e2 with [ nmk e' ⇒ e' ? ])) ]
364    | inr e1 ⇒ inr ?? (nmk ? (λH.match e1 with [ nmk e' ⇒ e' ? ])) ] | _ ⇒ inr ?? (nmk ? (λH.?)) ]
365| Tarray s t n ⇒ match t2 return λt'. (Tarray ??? = t') + (Tarray ??? ≠ t')  with [ Tarray s' t' n' ⇒
366    match eq_region_dec s s' with [ inl e1 ⇒
367      match type_eq_dec t t' with [ inl e2 ⇒
368        match decidable_eq_Z_Type n n' with [ inl e3 ⇒ inl ???
369        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
370        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
371        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
372        | _ ⇒ inr ?? (nmk ? (λH.?)) ]
373| Tfunction tl t ⇒ match t2 return λt'. (Tfunction ?? = t') + (Tfunction ?? ≠ t')  with [ Tfunction tl' t' ⇒
374    match typelist_eq_dec tl tl' with [ inl e1 ⇒
375    match type_eq_dec t t' with [ inl e2 ⇒ inl ???
376    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
377    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
378  | _ ⇒ inr ?? (nmk ? (λH.?)) ]
379| Tstruct i fl ⇒
380    match t2 return λt'. (Tstruct ?? = t') + (Tstruct ?? ≠ t')  with [ Tstruct i' fl' ⇒
381    match ident_eq i i' with [ inl e1 ⇒
382    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
383    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
384    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
385    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
386| Tunion i fl ⇒
387    match t2 return λt'. (Tunion ?? = t') + (Tunion ?? ≠ t')  with [ Tunion i' fl' ⇒
388    match ident_eq i i' with [ inl e1 ⇒
389    match fieldlist_eq_dec fl fl' with [ inl e2 ⇒ inl ???
390    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
391    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
392    |  _ ⇒ inr ?? (nmk ? (λH.?)) ]
393| Tcomp_ptr r i ⇒ match t2 return λt'. (Tcomp_ptr ? ? = t') + (Tcomp_ptr ? ? ≠ t')  with [ Tcomp_ptr r' i' ⇒
394    match eq_region_dec r r' with [ inl e1 ⇒
395      match ident_eq i i' with [ inl e2 ⇒ inl ???
396      | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
397    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
398    | _ ⇒ inr ?? (nmk ? (λH.?)) ]
399]
400and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝
401match tl1 return λtl'. (tl' = tl2) + (tl' ≠ tl2) with
402[ Tnil ⇒ match tl2 return λtl'. (Tnil = tl') + (Tnil ≠ tl') with [ Tnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
403| Tcons t1 ts1 ⇒ match tl2 return λtl'. (Tcons ?? = tl') + (Tcons ?? ≠ tl') with [ Tnil ⇒ inr ?? (nmk ? (λH.?)) | Tcons t2 ts2 ⇒
404    match type_eq_dec t1 t2 with [ inl e1 ⇒
405    match typelist_eq_dec ts1 ts2 with [ inl e2 ⇒ inl ???
406    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
407    | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
408]
409and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝
410match fl1 return λfl'. (fl' = fl2) + (fl' ≠ fl2) with
411[ Fnil ⇒ match fl2 return λfl'. (Fnil = fl') + (Fnil ≠ fl') with [ Fnil ⇒ inl ?? (refl ??) | _ ⇒ inr ?? (nmk ? (λH.?)) ]
412| Fcons i1 t1 fs1 ⇒ match fl2 return λfl'. (Fcons ??? = fl') + (Fcons ??? ≠ fl') with [ Fnil ⇒ inr ?? (nmk ? (λH.?)) | Fcons i2 t2 fs2 ⇒
413    match ident_eq i1 i2 with [ inl e1 ⇒
414      match type_eq_dec t1 t2 with [ inl e2 ⇒
415        match fieldlist_eq_dec fs1 fs2 with [ inl e3 ⇒ inl ???
416        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
417        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ]
418        | inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ]
419]. destruct; //; qed.
420
421definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝
422λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p | inr _ ⇒ Error ? ].
423
424let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
425match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
426[ Kstop ⇒ ?
427| Kcall _ _ _ _ ⇒ ?
428| _ ⇒ ?
429].
430[ 1,8: %1 ; //
431| *: %2 ; /2/
432] qed.
433
434definition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝
435λs.match s return λs'.(s' = Sskip) + (s' ≠ Sskip) with
436[ Sskip ⇒ inl ?? (refl ??)
437| _ ⇒ inr ?? (nmk ? (λH.?))
438]. destruct
439qed.
440
441(* Checking types of values given to / received from an external function call. *)
442
443definition eventval_type : ∀ty:typ. Type[0] ≝
444λty. match ty with [ ASTint ⇒ int | ASTfloat ⇒ float ].
445
446definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝
447λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v | ASTfloat ⇒ λv.EVfloat v ].
448
449definition mk_val: ∀ty:typ. eventval_type ty → val ≝
450λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v | ASTfloat ⇒ λv.Vfloat v ].
451
452lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.
453  eventval_match (mk_eventval ty v) ty (mk_val ty v).
454#ty cases ty; normalize; //; qed.
455
456definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝
457λev,ty.
458match ty with
459[ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i) | _ ⇒ Error ? ]
460| ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f) | _ ⇒ Error ? ]
461| _ ⇒ Error ?
462].
463
464definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝
465λv,ty.
466match ty with
467[ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i) | _ ⇒ Error ? ]
468| ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f) | _ ⇒ Error ? ]
469| _ ⇒ Some ? (Error ?)
470].
471
472let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝
473match vs with
474[ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?) | _ ⇒ Error ? ]
475| cons v vt ⇒
476  match tys with
477  [ nil ⇒ Error ?
478  | cons ty tyt ⇒
479    do ev ← check_eventval' v ty;
480    do evt ← check_eventval_list vt tyt;
481    OK ? (ev::evt)
482  ]
483].
484
485(* IO monad *)
486
487(* Interactions are function calls that return a value and do not change
488   the rest of the Clight program's state. *)
489record io_out : Type[0] ≝
490{ io_function: ident
491; io_args: list eventval
492; io_in_typ: typ
493}.
494
495definition io_in ≝ λo. eventval_type (io_in_typ o).
496
497definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝
498λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res).
499
500definition ret: ∀T. T → (IO io_out io_in T) ≝
501λT,x.(Value ?? T x).
502
503(* execution *)
504
505definition store_value_of_type' ≝
506λty,m,l,v.
507match l with [ pair loc ofs ⇒
508  store_value_of_type ty m loc ofs v ].
509
510let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
511match st with
512[ State f s k e m ⇒
513  match s with
514  [ Sassign a1 a2 ⇒
515    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
516    ! 〈v2,tr2〉 ← exec_expr ge e m a2;
517    ! m' ← store_value_of_type' (typeof a1) m l v2;
518    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
519  | Scall lhs a al ⇒
520    ! 〈vf,tr2〉 ← exec_expr ge e m a;
521    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
522    ! fd ← find_funct ? ? ge vf;
523    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
524(* requires associativity of IOMonad, so rearrange it below
525    ! k' ← match lhs with
526         [ None ⇒ ret ? (Kcall (None ?) f e k)
527         | Some lhs' ⇒
528           ! locofs ← exec_lvalue ge e m lhs';
529           ret ? (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k)
530         ];
531    ret ? 〈E0, Callstate fd vargs k' m〉)
532*)
533    match lhs with
534         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
535         | Some lhs' ⇒
536           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
537           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
538         ]
539  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
540  | Sskip ⇒
541      match k with
542      [ Kseq s k' ⇒ ret ? 〈E0, State  f s k' e m〉
543      | Kstop ⇒
544          match fn_return f with
545          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
546          | _ ⇒ Wrong ???
547          ]
548      | Kcall _ _ _ _ ⇒
549          match fn_return f with
550          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
551          | _ ⇒ Wrong ???
552          ]
553      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
554      | Kdowhile a s' k' ⇒
555          ! 〈v,tr〉 ← exec_expr ge e m a;
556          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
557          match b with
558          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
559          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
560          ]
561      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
562      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
563      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
564      | _ ⇒ Wrong ???
565      ]
566  | Scontinue ⇒
567      match k with
568      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
569      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
570      | Kdowhile a s' k' ⇒
571          ! 〈v,tr〉 ← exec_expr ge e m a;
572          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
573          match b with
574          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
575          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
576          ]
577      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
578      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
579      | _ ⇒ Wrong ???
580      ]
581  | Sbreak ⇒
582      match k with
583      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
584      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
585      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
586      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
587      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
588      | _ ⇒ Wrong ???
589      ]
590  | Sifthenelse a s1 s2 ⇒
591      ! 〈v,tr〉 ← exec_expr ge e m a;
592      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
593      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
594  | Swhile a s' ⇒
595      ! 〈v,tr〉 ← exec_expr ge e m a;
596      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
597      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
598                      else State f Sskip k e m〉
599  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
600  | Sfor a1 a2 a3 s' ⇒
601      match is_Sskip a1 with
602      [ inl _ ⇒
603          ! 〈v,tr〉 ← exec_expr ge e m a2;
604          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
605          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
606      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
607      ]
608  | Sreturn a_opt ⇒
609    match a_opt with
610    [ None ⇒ match fn_return f with
611      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
612      | _ ⇒ Wrong ???
613      ]
614    | Some a ⇒
615        match type_eq_dec (fn_return f) Tvoid with
616        [ inl _ ⇒ Wrong ???
617        | inr _ ⇒
618          ! 〈v,tr〉 ← exec_expr ge e m a;
619          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
620        ]
621    ]
622  | Sswitch a sl ⇒
623      ! 〈v,tr〉 ← exec_expr ge e m a;
624      match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
625                   | _ ⇒ Wrong ??? ]
626  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
627  | Sgoto lbl ⇒
628      match find_label lbl (fn_body f) (call_cont k) with
629      [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
630      | None ⇒ Wrong ???
631      ]
632  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
633  ]
634| Callstate f0 vargs k m ⇒
635  match f0 with
636  [ Internal f ⇒
637    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒
638      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
639      ret ? 〈E0, State f (fn_body f) k e m2〉
640    ]
641  | External f argtys retty ⇒
642      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
643      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
644      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
645  ]
646| Returnstate res k m ⇒
647  match k with
648  [ Kcall r f e k' ⇒
649    match r with
650    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
651    | Some r' ⇒
652      match r' with [ pair l ty ⇒
653       
654          ! m' ← store_value_of_type' ty m l res;
655          ret ? 〈E0, (State f Sskip k' e m')〉
656      ]
657    ]
658  | _ ⇒ Wrong ???
659  ]
660].
661
662let rec make_initial_state (p:clight_program) : res (genv × state) ≝
663  do ge ← globalenv Genv ?? p;
664  do m0 ← init_mem Genv ?? p;
665  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
666  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
667  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
668
669definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
670#st elim st;
671[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
672| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
673| #v #k #m cases k;
674  [ cases v;
675    [ 2: #i %1 ; %{ i} //;
676    | 1: %2 ; % *;   #r #H inversion H; #i #m #e destruct;
677    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
678    | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
679    | #r #b #pc #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
680    ]
681  | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
682  | 3,4: #a #b #c %2 ; % *; #r #H inversion H; #i #m #e destruct;
683  | 5,6,8: #a #b #c #d %2 ; % *; #r #H inversion H; #i #m #e destruct;
684  | #a %2 ; % *; #r #H inversion H; #i #m #e destruct;
685  ]
686] qed.
687
688let rec exec_steps (n:nat) (ge:genv) (s:state) :
689 IO io_out io_in (trace×state) ≝
690match is_final_state s with
691[ inl _ ⇒ ret ? 〈E0, s〉
692| inr _ ⇒
693  match n with
694  [ O ⇒ ret ? 〈E0, s〉
695  | S n' ⇒
696      ! 〈t,s'〉 ← exec_step ge s;
697(*      ! 〈t,s'〉 ← match s with
698                 [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (State f s k e (mk_mem c n p)) ]
699                 | Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Callstate fd args k (mk_mem c n p)) ]
700                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ]
701                 ] ;*)
702      ! 〈t',s''〉 ← match s' with
703                 [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (State f s k e (mk_mem c n p)) ]
704                 | Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Callstate fd args k (mk_mem c n p)) ]
705                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ]
706                 ] ;
707(*      ! 〈t',s''〉 ← exec_steps n' ge s';*)
708      ret ? 〈t ⧺ t',s''〉
709  ]
710].
711
712definition mem_of_state : state → mem ≝
713λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
714
715definition is_final : state → option int ≝
716λs.match is_final_state s with
717[ inl r ⇒ Some ? (sig_eject … r)
718| inr _ ⇒ None ?
719].
720
721definition clight_exec : clight_program → execstep ≝
722λp. mk_execstep … (initial_state p) is_final mem_of_state exec_step.
723
724definition exec_inf : ∀p:clight_program. execution (state (clight_exec p)) io_out io_in ≝
725λp.
726  match make_initial_state p with
727  [ OK gs ⇒ exec_inf_aux (clight_exec p) (\fst gs) (ret ? 〈E0,\snd gs〉)
728  | _ ⇒ e_wrong ???
729  ].
Note: See TracBrowser for help on using the repository browser.