source: src/Clight/Cexec.ma @ 880

Last change on this file since 880 was 880, checked in by campbell, 8 years ago

Add type information into Cminor.
As a result, the Clight to Cminor stage now does extra type checking.

File size: 22.8 KB
Line 
1
2
3include "utilities/extralib.ma".
4include "common/IO.ma".
5include "common/SmallstepExec.ma".
6include "Clight/Csem.ma".
7include "Clight/TypeComparison.ma".
8
9(*
10include "Plogic/russell_support.ma".
11
12definition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝
13  λA,P,a.match a with [ None ⇒ False | Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True | OK z ⇒ P z ]].
14
15definition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (Sig A P) ≝
16  λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a.
17  (match a return λa'.a=a' → res (Sig A P) with
18   [ None ⇒ λe1.?
19   | Some b ⇒ λe1.(match b return λb'.b=b' → ? with
20     [ Error ⇒ λ_. Error ?
21     | OK c ⇒ λe2. OK ? (dp A P c ?)
22     ]) (refl ? b)
23   ]) (refl ? a).
24[ >e1 in p; normalize; *;
25| >e1 in p >e2 normalize; //
26] qed.
27
28definition err_eject : ∀A.∀P: A → Prop. res (Sig A P) → res A ≝
29  λA,P,a.match a with [ Error m ⇒ Error ? m | OK b ⇒
30    match b with [ dp w p ⇒ OK ? w] ].
31
32definition sig_eject : ∀A.∀P: A → Prop. Sig A P → A ≝
33  λA,P,a.match a with [ dp w p ⇒ w].
34
35coercion err_inject :
36  ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (Sig A P) ≝ err_inject
37  on a:option (res ?) to res (Sig ? ?).
38coercion err_eject : ∀A.∀P:A → Prop.∀c:res (Sig A P).res A ≝ err_eject
39  on _c:res (Sig ? ?) to res ?.
40coercion sig_eject : ∀A.∀P:A → Prop.∀c:Sig A P.A ≝ sig_eject
41  on _c:Sig ? ? to ?.
42*)
43definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
44  λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ].
45
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
336let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
337match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
338[ Kstop ⇒ ?
339| Kcall _ _ _ _ ⇒ ?
340| _ ⇒ ?
341].
342[ 1,8: %1 ; //
343| *: %2 ; /2/
344] qed.
345
346definition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝
347λs.match s return λs'.(s' = Sskip) + (s' ≠ Sskip) with
348[ Sskip ⇒ inl ?? (refl ??)
349| _ ⇒ inr ?? (nmk ? (λH.?))
350]. destruct
351qed.
352
353
354(* execution *)
355
356definition store_value_of_type' ≝
357λty,m,l,v.
358match l with [ pair loc ofs ⇒
359  store_value_of_type ty m loc ofs v ].
360
361axiom NonsenseState : String.
362axiom ReturnMismatch : String.
363axiom UnknownLabel : String.
364axiom BadFunctionValue : String.
365
366let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
367match st with
368[ State f s k e m ⇒
369  match s with
370  [ Sassign a1 a2 ⇒
371    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
372    ! 〈v2,tr2〉 ← exec_expr ge e m a2;
373    ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2);
374    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
375  | Scall lhs a al ⇒
376    ! 〈vf,tr2〉 ← exec_expr ge e m a;
377    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
378    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf);
379    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
380(* requires associativity of IOMonad, so rearrange it below
381    ! k' ← match lhs with
382         [ None ⇒ ret ? (Kcall (None ?) f e k)
383         | Some lhs' ⇒
384           ! locofs ← exec_lvalue ge e m lhs';
385           ret ? (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k)
386         ];
387    ret ? 〈E0, Callstate fd vargs k' m〉)
388*)
389    match lhs with
390         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
391         | Some lhs' ⇒
392           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
393           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
394         ]
395  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
396  | Sskip ⇒
397      match k with
398      [ Kseq s k' ⇒ ret ? 〈E0, State  f s k' e m〉
399      | Kstop ⇒
400          match fn_return f with
401          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
402          | _ ⇒ Wrong ??? (msg NonsenseState)
403          ]
404      | Kcall _ _ _ _ ⇒
405          match fn_return f with
406          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
407          | _ ⇒ Wrong ??? (msg NonsenseState)
408          ]
409      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
410      | Kdowhile a s' k' ⇒
411          ! 〈v,tr〉 ← exec_expr ge e m a;
412          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
413          match b with
414          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
415          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
416          ]
417      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
418      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
419      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
420      | _ ⇒ Wrong ??? (msg NonsenseState)
421      ]
422  | Scontinue ⇒
423      match k with
424      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
425      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
426      | Kdowhile a s' k' ⇒
427          ! 〈v,tr〉 ← exec_expr ge e m a;
428          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
429          match b with
430          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
431          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
432          ]
433      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
434      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
435      | _ ⇒ Wrong ??? (msg NonsenseState)
436      ]
437  | Sbreak ⇒
438      match k with
439      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
440      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
441      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
442      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
443      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
444      | _ ⇒ Wrong ??? (msg NonsenseState)
445      ]
446  | Sifthenelse a s1 s2 ⇒
447      ! 〈v,tr〉 ← exec_expr ge e m a;
448      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
449      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
450  | Swhile a s' ⇒
451      ! 〈v,tr〉 ← exec_expr ge e m a;
452      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
453      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
454                      else State f Sskip k e m〉
455  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
456  | Sfor a1 a2 a3 s' ⇒
457      match is_Sskip a1 with
458      [ inl _ ⇒
459          ! 〈v,tr〉 ← exec_expr ge e m a2;
460          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
461          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
462      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
463      ]
464  | Sreturn a_opt ⇒
465    match a_opt with
466    [ None ⇒ match fn_return f with
467      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
468      | _ ⇒ Wrong ??? (msg ReturnMismatch)
469      ]
470    | Some a ⇒
471        match type_eq_dec (fn_return f) Tvoid with
472        [ inl _ ⇒ Wrong ??? (msg ReturnMismatch)
473        | inr _ ⇒
474          ! 〈v,tr〉 ← exec_expr ge e m a;
475          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
476        ]
477    ]
478  | Sswitch a sl ⇒
479      ! 〈v,tr〉 ← exec_expr ge e m a;
480      match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
481                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
482  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
483  | Sgoto lbl ⇒
484      match find_label lbl (fn_body f) (call_cont k) with
485      [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
486      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
487      ]
488  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
489  ]
490| Callstate f0 vargs k m ⇒
491  match f0 with
492  [ CL_Internal f ⇒
493    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒
494      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
495      ret ? 〈E0, State f (fn_body f) k e m2〉
496    ]
497  | CL_External f argtys retty ⇒
498      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
499      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
500      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
501  ]
502| Returnstate res k m ⇒
503  match k with
504  [ Kcall r f e k' ⇒
505    match r with
506    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
507    | Some r' ⇒
508      match r' with [ pair l ty ⇒
509          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
510          ret ? 〈E0, (State f Sskip k' e m')〉
511      ]
512    ]
513  | _ ⇒ Wrong ??? (msg NonsenseState)
514  ]
515].
516
517axiom MainMissing : String.
518
519let rec make_initial_state (p:clight_program) : res (genv × state) ≝
520  do ge ← globalenv Genv ?? p;
521  do m0 ← init_mem Genv ?? p;
522  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
523  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
524  OK ? 〈ge,Callstate f (nil ?) Kstop m0〉.
525
526let rec is_final (s:state) : option int ≝
527match s with
528[ Returnstate res k m ⇒
529  match k with
530  [ Kstop ⇒
531    match res with
532    [ Vint r ⇒ Some ? r
533    | _ ⇒ None ?
534    ]
535  | _ ⇒ None ?
536  ]
537| _ ⇒ None ?
538].
539
540definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
541#st elim st;
542[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
543| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
544| #v #k #m cases k;
545  [ cases v;
546    [ 2: #i %1 ; %{ i} //;
547    | 1: %2 ; % *;   #r #H inversion H; #i #m #e destruct;
548    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
549    | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
550    | #r #b #pc #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
551    ]
552  | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
553  | 3,4: #a #b #c %2 ; % *; #r #H inversion H; #i #m #e destruct;
554  | 5,6,8: #a #b #c #d %2 ; % *; #r #H inversion H; #i #m #e destruct;
555  | #a %2 ; % *; #r #H inversion H; #i #m #e destruct;
556  ]
557] qed.
558
559let rec exec_steps (n:nat) (ge:genv) (s:state) :
560 IO io_out io_in (trace×state) ≝
561match is_final_state s with
562[ inl _ ⇒ ret ? 〈E0, s〉
563| inr _ ⇒
564  match n with
565  [ O ⇒ ret ? 〈E0, s〉
566  | S n' ⇒
567      ! 〈t,s'〉 ← exec_step ge s;
568(*      ! 〈t,s'〉 ← match s with
569                 [ 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)) ]
570                 | 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)) ]
571                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ]
572                 ] ;*)
573      ! 〈t',s''〉 ← match s' with
574                 [ 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)) ]
575                 | 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)) ]
576                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ]
577                 ] ;
578(*      ! 〈t',s''〉 ← exec_steps n' ge s';*)
579      ret ? 〈t ⧺ t',s''〉
580  ]
581].
582
583definition mem_of_state : state → mem ≝
584λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
585
586definition clight_exec : execstep io_out io_in ≝
587  mk_execstep … is_final mem_of_state exec_step.
588
589definition clight_fullexec : fullexec io_out io_in ≝
590  mk_fullexec ?? clight_exec ? make_initial_state.
Note: See TracBrowser for help on using the repository browser.