source: src/Clight/Cexec.ma @ 855

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

Add error messages wherever the error monad is used.
Sticks to CompCert? style strings+identifiers for the moment.
Use axioms for strings as we currently have no representation or literals
for them - still *very* useful for animation in the proof assistant.

File size: 28.2 KB
Line 
1
2
3include "utilities/extralib.ma".
4include "common/IO.ma".
5include "common/SmallstepExec.ma".
6include "Clight/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 m ⇒ Error ? m | 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
45axiom TypeMismatch : String.
46axiom ValueIsNotABoolean : String.
47
48definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
49  λv,ty. match v in val with
50  [ Vint i ⇒ match ty with
51    [ Tint _ _ ⇒ OK ? (¬eq i zero)
52    | _ ⇒ Error ? (msg TypeMismatch)
53    ]
54  | Vfloat f ⇒ match ty with
55    [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero)
56    | _ ⇒ Error ? (msg TypeMismatch)
57    ]
58  | Vptr _ _ _ _ ⇒ match ty with
59    [ Tpointer _ _ ⇒ OK ? true
60    | _ ⇒ Error ? (msg TypeMismatch)
61    ]
62  | Vnull _ ⇒ match ty with
63    [ Tpointer _ _ ⇒ OK ? false
64    | _ ⇒ Error ? (msg TypeMismatch)
65    ]
66  | _ ⇒ Error ? (msg ValueIsNotABoolean)
67  ].
68
69lemma 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.
70#v #ty #r #H elim H; #v #t #H' elim H';
71  [ #i #is #s #ne %{ true} % //; whd in ⊢ (??%?); >(eq_false … ne) //;
72  | #r #b #pc #i #i0 #s %{ true} % //
73  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
74  | #i #s %{ false} % //;
75  | #r #r' #t %{ false} % //;
76  | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;
77  ]
78qed.
79
80(* Prove a few minor results to make proof obligations easy. *)
81
82lemma bind_OK: ∀A,B,P,e,f.
83  (∀v. e = OK A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
84  match bind A B e f with [ Error _ ⇒ True | OK v ⇒ P v ].
85#A #B #P #e #f elim e; /2/; qed.
86
87lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
88  (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
89  match bind (Sig A P) B e f with [ Error _ ⇒ True | OK v' ⇒ P' v' ].
90#A #B #P #P' #e #f elim e;
91[ #v0 elim v0; #v #Hv #IH @IH
92| #m #_ @I
93] qed.
94
95lemma bind2_OK: ∀A,B,C,P,e,f.
96  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
97  match bind2 A B C e f with [ Error _ ⇒ True | OK v ⇒ P v ].
98#A #B #C #P #e #f elim e; //; #v cases v; /2/; qed.
99
100lemma opt_bind_OK: ∀A,B,P,m,e,f.
101  (∀v. e = Some A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
102  match bind A B (opt_to_res A m e) f with [ Error _ ⇒ True | OK v ⇒ P v ].
103#A #B #P #m #e #f elim e; normalize; /2/; qed.
104
105
106axiom BadCast : String. (* TODO: refine into more precise errors? *)
107
108definition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val  ≝
109λm:mem. λi:int. λty:type. λty':type.
110match eq i zero with
111[ true ⇒
112  match ty with
113  [ Tint _ _ ⇒
114    match ty' with
115    [ Tpointer r _ ⇒ OK ? (Vnull r)
116    | Tarray r _ _ ⇒ OK ? (Vnull r)
117    | Tfunction _ _ ⇒ OK ? (Vnull Code)
118    | _ ⇒ Error ? (msg BadCast)
119    ]
120  | _ ⇒ Error ? (msg BadCast)
121  ]
122| false ⇒ Error ? (msg BadCast)
123].
124
125definition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
126λm:mem. λv:val. λty:type. λty':type.
127match v with
128[ Vint i ⇒
129  match ty with
130  [ Tint sz1 si1 ⇒
131    match ty' with
132    [ Tint sz2 si2 ⇒ OK ? (Vint (cast_int_int sz2 si2 i))
133    | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))
134    | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
135    | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
136    | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
137    | _ ⇒ Error ? (msg BadCast)
138    ]
139  | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
140  | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
141  | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r
142  | _ ⇒ Error ? (msg TypeMismatch)
143  ]
144| Vfloat f ⇒
145  match ty with
146  [ Tfloat sz ⇒
147    match ty' with
148    [ Tint sz' si' ⇒ OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f)))
149    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
150    | _ ⇒ Error ? (msg BadCast)
151    ]
152  | _ ⇒ Error ? (msg TypeMismatch)
153  ]
154| Vptr r b _ ofs ⇒
155    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
156    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
157    do s' ← match ty' with
158         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
159         | _ ⇒ Error ? (msg BadCast)];
160    match pointer_compat_dec b s' with
161    [ inl p' ⇒ OK ? (Vptr s' b p' ofs)
162    | inr _ ⇒ Error ? (msg BadCast)
163    ]
164| Vnull r ⇒
165    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
166    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
167    do s' ← match ty' with
168         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
169         | _ ⇒ Error ? (msg BadCast) ];
170    OK ? (Vnull s')
171| _ ⇒ Error ? (msg BadCast)
172].
173
174definition load_value_of_type' ≝
175λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
176
177(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
178   a structurally smaller value, we break out the surrounding Expr constructor
179   and use exec_lvalue'. *)
180
181axiom BadlyTypedTerm : String.
182axiom UnknownIdentifier : String.
183axiom BadLvalueTerm : String.
184axiom FailedLoad : String.
185axiom FailedOp : String.
186
187let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
188match e with
189[ Expr e' ty ⇒
190  match e' with
191  [ Econst_int i ⇒ OK ? 〈Vint i, E0〉
192  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉
193  | Evar _ ⇒
194      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
195      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
196      OK ? 〈v,tr〉
197  | Ederef _ ⇒
198      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
199      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
200      OK ? 〈v,tr〉
201  | Efield _ _ ⇒
202      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
203      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
204      OK ? 〈v,tr〉
205  | Eaddrof a ⇒
206      do 〈lo,tr〉 ← exec_lvalue ge en m a;
207      match ty with
208      [ Tpointer r _ ⇒
209        match lo with [ pair loc ofs ⇒
210          match pointer_compat_dec loc r with
211          [ inl pc ⇒ OK ? 〈Vptr r loc pc ofs, tr〉
212          | inr _ ⇒ Error ? (msg TypeMismatch)
213          ]
214        ]
215      | _ ⇒ Error ? (msg BadlyTypedTerm)
216      ]
217  | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉
218  | Eunop op a ⇒
219      do 〈v1,tr〉 ← exec_expr ge en m a;
220      do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a));
221      OK ? 〈v,tr〉
222  | Ebinop op a1 a2 ⇒
223      do 〈v1,tr1〉 ← exec_expr ge en m a1;
224      do 〈v2,tr2〉 ← exec_expr ge en m a2;
225      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
226      OK ? 〈v,tr1⧺tr2〉
227  | Econdition a1 a2 a3 ⇒
228      do 〈v,tr1〉 ← exec_expr ge en m a1;
229      do b ← exec_bool_of_val v (typeof a1);
230      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
231                 [ true ⇒ (exec_expr ge en m a2)
232                 | false ⇒ (exec_expr ge en m a3) ];
233      OK ? 〈v',tr1⧺tr2〉
234(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
235  | Eorbool a1 a2 ⇒
236      do 〈v1,tr1〉 ← exec_expr ge en m a1;
237      do b1 ← exec_bool_of_val v1 (typeof a1);
238      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
239        do 〈v2,tr2〉 ← exec_expr ge en m a2;
240        do b2 ← exec_bool_of_val v2 (typeof a2);
241        OK ? 〈of_bool b2, tr1⧺tr2〉 ]
242  | Eandbool 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 ⇒
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      | false ⇒ OK ? 〈Vfalse,tr1〉 ]
250  | Ecast ty' a ⇒
251      do 〈v,tr〉 ← exec_expr ge en m a;
252      do v' ← exec_cast m v (typeof a) ty';
253      OK ? 〈v',tr〉
254  | Ecost l a ⇒
255      do 〈v,tr〉 ← exec_expr ge en m a;
256      OK ? 〈v,tr⧺(Echarge l)〉
257  ]
258]
259and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
260  match e' with
261  [ Evar id ⇒
262      match (get … id en) with
263      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
264      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
265      ]
266  | Ederef a ⇒
267      do 〈v,tr〉 ← exec_expr ge en m a;
268      match v with
269      [ Vptr _ l _ ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
270      | _ ⇒ Error ? (msg TypeMismatch)
271      ]
272  | Efield a i ⇒
273      match (typeof a) with
274      [ Tstruct id fList ⇒
275          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
276          do delta ← field_offset i fList;
277          OK ? 〈〈\fst lofs,shift_offset (\snd lofs) (repr delta)〉,tr〉
278      | Tunion id fList ⇒
279          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
280          OK ? 〈lofs,tr〉
281      | _ ⇒ Error ? (msg BadlyTypedTerm)
282      ]
283  | _ ⇒ Error ? (msg BadLvalueTerm)
284  ]
285and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
286match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
287
288lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
289#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
290
291(* We define a special induction principle tailored to the recursive definition
292   above. *)
293
294definition is_not_lvalue: expr_descr → Prop ≝
295λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
296
297definition Plvalue ≝ λP:(expr → Prop).λe,ty.
298match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
299
300(* TODO: Can we do this sensibly with a map combinator? *)
301let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
302match l with
303[ nil ⇒ OK ? 〈nil val, E0〉
304| cons e1 es ⇒
305  do 〈v,tr1〉 ← exec_expr ge e m e1;
306  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
307  OK ? 〈cons val v vs, tr1⧺tr2〉
308].
309
310let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝
311match l with
312[ nil ⇒ 〈en, m〉
313| cons h vars ⇒
314  match h with [ pair id ty ⇒
315    match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒
316      exec_alloc_variables (set … id b1 en) m1 vars
317]]].
318
319axiom WrongNumberOfParameters : String.
320axiom FailedStore : String.
321
322(* TODO: can we establish that length params = length vs in advance? *)
323let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
324  match params with
325  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
326  | cons idty params' ⇒ match idty with [ pair id ty ⇒
327      match vs with
328      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
329      | cons v1 vl ⇒
330          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (get … id e);
331          do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1);
332          exec_bind_parameters e m1 params' vl
333      ]
334  ] ].
335
336definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
337#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
338definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
339#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
340definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
341#s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed.
342
343definition eq_nat_dec : ∀n,m:nat. Sum (n=m) (n≠m).
344#n #m lapply (refl ? (eqb n m)) cases (eqb n m) in ⊢ (???% → ?) #E
345[ %1 | %2 ] @(eqb_elim … E) // #_ #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 eq_nat_dec 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 ? (msg TypeMismatch)].
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
442(* execution *)
443
444definition store_value_of_type' ≝
445λty,m,l,v.
446match l with [ pair loc ofs ⇒
447  store_value_of_type ty m loc ofs v ].
448
449axiom NonsenseState : String.
450axiom ReturnMismatch : String.
451axiom UnknownLabel : String.
452axiom BadFunctionValue : String.
453
454let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
455match st with
456[ State f s k e m ⇒
457  match s with
458  [ Sassign a1 a2 ⇒
459    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
460    ! 〈v2,tr2〉 ← exec_expr ge e m a2;
461    ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2);
462    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
463  | Scall lhs a al ⇒
464    ! 〈vf,tr2〉 ← exec_expr ge e m a;
465    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
466    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf);
467    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
468(* requires associativity of IOMonad, so rearrange it below
469    ! k' ← match lhs with
470         [ None ⇒ ret ? (Kcall (None ?) f e k)
471         | Some lhs' ⇒
472           ! locofs ← exec_lvalue ge e m lhs';
473           ret ? (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k)
474         ];
475    ret ? 〈E0, Callstate fd vargs k' m〉)
476*)
477    match lhs with
478         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
479         | Some lhs' ⇒
480           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
481           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
482         ]
483  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
484  | Sskip ⇒
485      match k with
486      [ Kseq s k' ⇒ ret ? 〈E0, State  f s k' e m〉
487      | Kstop ⇒
488          match fn_return f with
489          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
490          | _ ⇒ Wrong ??? (msg NonsenseState)
491          ]
492      | Kcall _ _ _ _ ⇒
493          match fn_return f with
494          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
495          | _ ⇒ Wrong ??? (msg NonsenseState)
496          ]
497      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
498      | Kdowhile a s' k' ⇒
499          ! 〈v,tr〉 ← exec_expr ge e m a;
500          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
501          match b with
502          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
503          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
504          ]
505      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
506      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
507      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
508      | _ ⇒ Wrong ??? (msg NonsenseState)
509      ]
510  | Scontinue ⇒
511      match k with
512      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
513      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
514      | Kdowhile a s' k' ⇒
515          ! 〈v,tr〉 ← exec_expr ge e m a;
516          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
517          match b with
518          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
519          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
520          ]
521      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
522      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
523      | _ ⇒ Wrong ??? (msg NonsenseState)
524      ]
525  | Sbreak ⇒
526      match k with
527      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
528      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
529      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
530      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
531      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
532      | _ ⇒ Wrong ??? (msg NonsenseState)
533      ]
534  | Sifthenelse a s1 s2 ⇒
535      ! 〈v,tr〉 ← exec_expr ge e m a;
536      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
537      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
538  | Swhile a s' ⇒
539      ! 〈v,tr〉 ← exec_expr ge e m a;
540      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
541      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
542                      else State f Sskip k e m〉
543  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
544  | Sfor a1 a2 a3 s' ⇒
545      match is_Sskip a1 with
546      [ inl _ ⇒
547          ! 〈v,tr〉 ← exec_expr ge e m a2;
548          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
549          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
550      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
551      ]
552  | Sreturn a_opt ⇒
553    match a_opt with
554    [ None ⇒ match fn_return f with
555      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
556      | _ ⇒ Wrong ??? (msg ReturnMismatch)
557      ]
558    | Some a ⇒
559        match type_eq_dec (fn_return f) Tvoid with
560        [ inl _ ⇒ Wrong ??? (msg ReturnMismatch)
561        | inr _ ⇒
562          ! 〈v,tr〉 ← exec_expr ge e m a;
563          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
564        ]
565    ]
566  | Sswitch a sl ⇒
567      ! 〈v,tr〉 ← exec_expr ge e m a;
568      match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
569                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
570  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
571  | Sgoto lbl ⇒
572      match find_label lbl (fn_body f) (call_cont k) with
573      [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
574      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
575      ]
576  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
577  ]
578| Callstate f0 vargs k m ⇒
579  match f0 with
580  [ CL_Internal f ⇒
581    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒
582      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
583      ret ? 〈E0, State f (fn_body f) k e m2〉
584    ]
585  | CL_External f argtys retty ⇒
586      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
587      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
588      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
589  ]
590| Returnstate res k m ⇒
591  match k with
592  [ Kcall r f e k' ⇒
593    match r with
594    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
595    | Some r' ⇒
596      match r' with [ pair l ty ⇒
597          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
598          ret ? 〈E0, (State f Sskip k' e m')〉
599      ]
600    ]
601  | _ ⇒ Wrong ??? (msg NonsenseState)
602  ]
603].
604
605axiom MainMissing : String.
606
607let rec make_initial_state (p:clight_program) : res (genv × state) ≝
608  do ge ← globalenv Genv ?? p;
609  do m0 ← init_mem Genv ?? p;
610  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
611  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
612  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
613
614let rec is_final (s:state) : option int ≝
615match s with
616[ Returnstate res k m ⇒
617  match k with
618  [ Kstop ⇒
619    match res with
620    [ Vint r ⇒ Some ? r
621    | _ ⇒ None ?
622    ]
623  | _ ⇒ None ?
624  ]
625| _ ⇒ None ?
626].
627
628definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
629#st elim st;
630[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
631| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
632| #v #k #m cases k;
633  [ cases v;
634    [ 2: #i %1 ; %{ i} //;
635    | 1: %2 ; % *;   #r #H inversion H; #i #m #e destruct;
636    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
637    | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
638    | #r #b #pc #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
639    ]
640  | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
641  | 3,4: #a #b #c %2 ; % *; #r #H inversion H; #i #m #e destruct;
642  | 5,6,8: #a #b #c #d %2 ; % *; #r #H inversion H; #i #m #e destruct;
643  | #a %2 ; % *; #r #H inversion H; #i #m #e destruct;
644  ]
645] qed.
646
647let rec exec_steps (n:nat) (ge:genv) (s:state) :
648 IO io_out io_in (trace×state) ≝
649match is_final_state s with
650[ inl _ ⇒ ret ? 〈E0, s〉
651| inr _ ⇒
652  match n with
653  [ O ⇒ ret ? 〈E0, s〉
654  | S n' ⇒
655      ! 〈t,s'〉 ← exec_step ge s;
656(*      ! 〈t,s'〉 ← match s with
657                 [ 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)) ]
658                 | 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)) ]
659                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ]
660                 ] ;*)
661      ! 〈t',s''〉 ← match s' with
662                 [ 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)) ]
663                 | 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)) ]
664                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ]
665                 ] ;
666(*      ! 〈t',s''〉 ← exec_steps n' ge s';*)
667      ret ? 〈t ⧺ t',s''〉
668  ]
669].
670
671definition mem_of_state : state → mem ≝
672λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
673
674definition clight_exec : execstep io_out io_in ≝
675  mk_execstep … is_final mem_of_state exec_step.
676
677definition clight_fullexec : fullexec io_out io_in ≝
678  mk_fullexec ?? clight_exec ? make_initial_state.
Note: See TracBrowser for help on using the repository browser.