source: Deliverables/D3.1/C-semantics/Cexec.ma @ 499

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

pointer_compat is a little more natural if it takes that block rather than
the block's region.

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