source: src/Clight/Cexec.ma @ 1231

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

Change SmallstepExec? so that states can depend on global information.
Use less suggestive names for the transition system so that it's obvious
the global information isn't restricted to Genv.
Separate set up of global environment from initialisation so that it never
fails.
Some minimal changes to get Clight execution working; rest to follow.

File size: 21.4 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
9definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
10  λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ].
11
12axiom ValueIsNotABoolean : String.
13
14definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
15  λv,ty. match v in val with
16  [ Vint sz i ⇒ match ty with
17    [ Tint sz' _ ⇒ intsize_eq_elim ? sz sz' ? i
18                   (λi. OK ? (¬eq_bv ? i (zero ?))) (Error ? (msg TypeMismatch))
19    | _ ⇒ Error ? (msg TypeMismatch)
20    ]
21  | Vfloat f ⇒ match ty with
22    [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero)
23    | _ ⇒ Error ? (msg TypeMismatch)
24    ]
25  | Vptr _ _ _ _ ⇒ match ty with
26    [ Tpointer _ _ ⇒ OK ? true
27    | _ ⇒ Error ? (msg TypeMismatch)
28    ]
29  | Vnull _ ⇒ match ty with
30    [ Tpointer _ _ ⇒ OK ? false
31    | _ ⇒ Error ? (msg TypeMismatch)
32    ]
33  | _ ⇒ Error ? (msg ValueIsNotABoolean)
34  ].
35
36lemma 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.
37#v #ty #r #H elim H; #v #t #H' elim H';
38  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?) >(eq_bv_false … ne) //
39  | #r #b #pc #i #i0 #s %{ true} % //
40  | #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //;
41  | * #sg %{ false} % //
42  | #r #r' #t %{ false} % //;
43  | #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //;
44  ]
45qed.
46
47(* Prove a few minor results to make proof obligations easy. *)
48
49lemma bind_OK: ∀A,B,P,e,f.
50  (∀v. e = OK A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
51  match bind A B e f with [ Error _ ⇒ True | OK v ⇒ P v ].
52#A #B #P #e #f elim e; /2/; qed.
53
54lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
55  (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
56  match bind (Sig A P) B e f with [ Error _ ⇒ True | OK v' ⇒ P' v' ].
57#A #B #P #P' #e #f elim e;
58[ #v0 elim v0; #v #Hv #IH @IH
59| #m #_ @I
60] qed.
61
62lemma bind2_OK: ∀A,B,C,P,e,f.
63  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
64  match bind2 A B C e f with [ Error _ ⇒ True | OK v ⇒ P v ].
65#A #B #C #P #e #f elim e; //; #v cases v; /2/; qed.
66
67lemma opt_bind_OK: ∀A,B,P,m,e,f.
68  (∀v. e = Some A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
69  match bind A B (opt_to_res A m e) f with [ Error _ ⇒ True | OK v ⇒ P v ].
70#A #B #P #m #e #f elim e; normalize; /2/; qed.
71
72
73axiom BadCast : String. (* TODO: refine into more precise errors? *)
74
75definition try_cast_null : ∀m:mem. ∀sz. ∀i:BitVector (bitsize_of_intsize sz). ∀ty:type. ∀ty':type. res val  ≝
76λm:mem. λsz. λi. λty:type. λty':type.
77match eq_bv ? i (zero ?) with
78[ true ⇒
79  match ty with
80  [ Tint sz' _ ⇒
81    if eq_intsize sz sz' then
82      match ty' with
83      [ Tpointer r _ ⇒ OK ? (Vnull r)
84      | Tarray r _ _ ⇒ OK ? (Vnull r)
85      | Tfunction _ _ ⇒ OK ? (Vnull Code)
86      | _ ⇒ Error ? (msg BadCast)
87      ]
88    else Error ? (msg TypeMismatch)
89  | _ ⇒ Error ? (msg BadCast)
90  ]
91| false ⇒ Error ? (msg BadCast)
92].
93
94definition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
95λm:mem. λv:val. λty:type. λty':type.
96match v with
97[ Vint sz i ⇒
98  match ty with
99  [ Tint sz1 si1 ⇒
100    intsize_eq_elim ? sz sz1 ? i
101    (λi.
102      match ty' with
103      [ Tint sz2 si2 ⇒ OK ? (Vint ? (cast_int_int sz1 si1 sz2 i))
104      | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
105      | Tpointer _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
106      | Tarray _ _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
107      | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
108      | _ ⇒ Error ? (msg BadCast)
109      ])
110    (Error ? (msg BadCast))
111  | Tpointer _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
112  | Tarray _ _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
113  | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
114  | _ ⇒ Error ? (msg TypeMismatch)
115  ]
116| Vfloat f ⇒
117  match ty with
118  [ Tfloat sz ⇒
119    match ty' with
120    [ Tint sz' si' ⇒ OK ? (Vint sz' (cast_float_int sz' si' f))
121    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
122    | _ ⇒ Error ? (msg BadCast)
123    ]
124  | _ ⇒ Error ? (msg TypeMismatch)
125  ]
126| Vptr r b _ ofs ⇒
127    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
128    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
129    do s' ← match ty' with
130         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
131         | _ ⇒ Error ? (msg BadCast)];
132    match pointer_compat_dec b s' with
133    [ inl p' ⇒ OK ? (Vptr s' b p' ofs)
134    | inr _ ⇒ Error ? (msg BadCast)
135    ]
136| Vnull r ⇒
137    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
138    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
139    do s' ← match ty' with
140         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
141         | _ ⇒ Error ? (msg BadCast) ];
142    OK ? (Vnull s')
143| _ ⇒ Error ? (msg BadCast)
144].
145
146definition load_value_of_type' ≝
147λty,m,l. match l with [ pair loc ofs ⇒ load_value_of_type ty m loc ofs ].
148
149axiom BadlyTypedTerm : String.
150axiom UnknownIdentifier : String.
151axiom BadLvalueTerm : String.
152axiom FailedLoad : String.
153axiom FailedOp : String.
154
155(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
156   a structurally smaller value, we break out the surrounding Expr constructor
157   and use exec_lvalue'. *)
158
159let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
160match e with
161[ Expr e' ty ⇒
162  match e' with
163  [ Econst_int sz i ⇒
164      match ty with
165      [ Tint sz' _ ⇒
166          if eq_intsize sz sz' then OK ? 〈Vint sz i, E0〉
167          else Error ? (msg BadlyTypedTerm)
168      | _ ⇒ Error ? (msg BadlyTypedTerm)
169      ]
170  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉
171  | Evar _ ⇒
172      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
173      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
174      OK ? 〈v,tr〉
175  | Ederef _ ⇒
176      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
177      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
178      OK ? 〈v,tr〉
179  | Efield _ _ ⇒
180      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
181      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
182      OK ? 〈v,tr〉
183  | Eaddrof a ⇒
184      do 〈lo,tr〉 ← exec_lvalue ge en m a;
185      match ty with
186      [ Tpointer r _ ⇒
187        match lo with [ pair loc ofs ⇒
188          match pointer_compat_dec loc r with
189          [ inl pc ⇒ OK ? 〈Vptr r loc pc ofs, tr〉
190          | inr _ ⇒ Error ? (msg TypeMismatch)
191          ]
192        ]
193      | _ ⇒ Error ? (msg BadlyTypedTerm)
194      ]
195  | Esizeof ty' ⇒
196      match ty with
197      [ Tint sz _ ⇒ OK ? 〈Vint sz (repr ? (sizeof ty')), E0〉
198      | _ ⇒ Error ? (msg BadlyTypedTerm)
199      ]
200  | Eunop op a ⇒
201      do 〈v1,tr〉 ← exec_expr ge en m a;
202      do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a));
203      OK ? 〈v,tr〉
204  | Ebinop op a1 a2 ⇒
205      do 〈v1,tr1〉 ← exec_expr ge en m a1;
206      do 〈v2,tr2〉 ← exec_expr ge en m a2;
207      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
208      OK ? 〈v,tr1⧺tr2〉
209  | Econdition a1 a2 a3 ⇒
210      do 〈v,tr1〉 ← exec_expr ge en m a1;
211      do b ← exec_bool_of_val v (typeof a1);
212      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
213                 [ true ⇒ (exec_expr ge en m a2)
214                 | false ⇒ (exec_expr ge en m a3) ];
215      OK ? 〈v',tr1⧺tr2〉
216(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
217  | Eorbool a1 a2 ⇒
218      do 〈v1,tr1〉 ← exec_expr ge en m a1;
219      do b1 ← exec_bool_of_val v1 (typeof a1);
220      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
221        do 〈v2,tr2〉 ← exec_expr ge en m a2;
222        do b2 ← exec_bool_of_val v2 (typeof a2);
223        OK ? 〈of_bool b2, tr1⧺tr2〉 ]
224  | Eandbool a1 a2 ⇒
225      do 〈v1,tr1〉 ← exec_expr ge en m a1;
226      do b1 ← exec_bool_of_val v1 (typeof a1);
227      match b1 return λ_.res (val×trace) with [ true ⇒
228        do 〈v2,tr2〉 ← exec_expr ge en m a2;
229        do b2 ← exec_bool_of_val v2 (typeof a2);
230        OK ? 〈of_bool b2, tr1⧺tr2〉
231      | false ⇒ OK ? 〈Vfalse,tr1〉 ]
232  | Ecast ty' a ⇒
233      do 〈v,tr〉 ← exec_expr ge en m a;
234      do v' ← exec_cast m v (typeof a) ty';
235      OK ? 〈v',tr〉
236  | Ecost l a ⇒
237      do 〈v,tr〉 ← exec_expr ge en m a;
238      OK ? 〈v,tr⧺(Echarge l)〉
239  ]
240]
241and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
242  match e' with
243  [ Evar id ⇒
244      match (lookup ?? en id) with
245      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
246      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
247      ]
248  | Ederef a ⇒
249      do 〈v,tr〉 ← exec_expr ge en m a;
250      match v with
251      [ Vptr _ l _ ofs ⇒ OK ? 〈〈l,ofs〉,tr〉
252      | _ ⇒ Error ? (msg TypeMismatch)
253      ]
254  | Efield a i ⇒
255      match (typeof a) with
256      [ Tstruct id fList ⇒
257          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
258          do delta ← field_offset i fList;
259          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I32 delta)〉,tr〉
260      | Tunion id fList ⇒
261          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
262          OK ? 〈lofs,tr〉
263      | _ ⇒ Error ? (msg BadlyTypedTerm)
264      ]
265  | _ ⇒ Error ? (msg BadLvalueTerm)
266  ]
267and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
268match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
269
270lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
271#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
272
273(* We define a special induction principle tailored to the recursive definition
274   above. *)
275
276definition is_not_lvalue: expr_descr → Prop ≝
277λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
278
279definition Plvalue ≝ λP:(expr → Prop).λe,ty.
280match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
281
282(* TODO: Can we do this sensibly with a map combinator? *)
283let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
284match l with
285[ nil ⇒ OK ? 〈nil val, E0〉
286| cons e1 es ⇒
287  do 〈v,tr1〉 ← exec_expr ge e m e1;
288  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
289  OK ? 〈cons val v vs, tr1⧺tr2〉
290].
291
292let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝
293match l with
294[ nil ⇒ 〈en, m〉
295| cons h vars ⇒
296  match h with [ pair id ty ⇒
297    match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒
298      exec_alloc_variables (add ?? en id b1) m1 vars
299]]].
300
301axiom WrongNumberOfParameters : String.
302axiom FailedStore : String.
303
304(* TODO: can we establish that length params = length vs in advance? *)
305let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
306  match params with
307  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
308  | cons idty params' ⇒ match idty with [ pair id ty ⇒
309      match vs with
310      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
311      | cons v1 vl ⇒
312          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (lookup ?? e id);
313          do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1);
314          exec_bind_parameters e m1 params' vl
315      ]
316  ] ].
317
318let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
319match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
320[ Kstop ⇒ ?
321| Kcall _ _ _ _ ⇒ ?
322| _ ⇒ ?
323].
324[ 1,8: %1 ; //
325| *: %2 ; /2/
326] qed.
327
328definition is_Sskip : ∀s:statement. (s = Sskip) ⊎ (s ≠ Sskip) ≝
329λs.match s return λs'.(s' = Sskip) ⊎ (s' ≠ Sskip) with
330[ Sskip ⇒ inl ?? (refl ??)
331| _ ⇒ inr ?? (nmk ? (λH.?))
332]. destruct
333qed.
334
335
336(* execution *)
337
338definition store_value_of_type' ≝
339λty,m,l,v.
340match l with [ pair loc ofs ⇒
341  store_value_of_type ty m loc ofs v ].
342
343axiom NonsenseState : String.
344axiom ReturnMismatch : String.
345axiom UnknownLabel : String.
346axiom BadFunctionValue : String.
347
348let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
349match st with
350[ State f s k e m ⇒
351  match s with
352  [ Sassign a1 a2 ⇒
353    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
354    ! 〈v2,tr2〉 ← exec_expr ge e m a2;
355    ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2);
356    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
357  | Scall lhs a al ⇒
358    ! 〈vf,tr2〉 ← exec_expr ge e m a;
359    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
360    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf);
361    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
362(* requires associativity of IOMonad, so rearrange it below
363    ! k' ← match lhs with
364         [ None ⇒ ret ? (Kcall (None ?) f e k)
365         | Some lhs' ⇒
366           ! locofs ← exec_lvalue ge e m lhs';
367           ret ? (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k)
368         ];
369    ret ? 〈E0, Callstate fd vargs k' m〉)
370*)
371    match lhs with
372         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
373         | Some lhs' ⇒
374           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
375           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
376         ]
377  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
378  | Sskip ⇒
379      match k with
380      [ Kseq s k' ⇒ ret ? 〈E0, State  f s k' e m〉
381      | Kstop ⇒
382          match fn_return f with
383          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
384          | _ ⇒ Wrong ??? (msg NonsenseState)
385          ]
386      | Kcall _ _ _ _ ⇒
387          match fn_return f with
388          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
389          | _ ⇒ Wrong ??? (msg NonsenseState)
390          ]
391      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
392      | Kdowhile a s' k' ⇒
393          ! 〈v,tr〉 ← exec_expr ge e m a;
394          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
395          match b with
396          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
397          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
398          ]
399      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
400      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
401      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
402      | _ ⇒ Wrong ??? (msg NonsenseState)
403      ]
404  | Scontinue ⇒
405      match k with
406      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
407      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
408      | Kdowhile a s' k' ⇒
409          ! 〈v,tr〉 ← exec_expr ge e m a;
410          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
411          match b with
412          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
413          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
414          ]
415      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
416      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
417      | _ ⇒ Wrong ??? (msg NonsenseState)
418      ]
419  | Sbreak ⇒
420      match k with
421      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
422      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
423      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
424      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
425      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
426      | _ ⇒ Wrong ??? (msg NonsenseState)
427      ]
428  | Sifthenelse a s1 s2 ⇒
429      ! 〈v,tr〉 ← exec_expr ge e m a;
430      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
431      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
432  | Swhile a s' ⇒
433      ! 〈v,tr〉 ← exec_expr ge e m a;
434      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
435      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
436                      else State f Sskip k e m〉
437  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
438  | Sfor a1 a2 a3 s' ⇒
439      match is_Sskip a1 with
440      [ inl _ ⇒
441          ! 〈v,tr〉 ← exec_expr ge e m a2;
442          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
443          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
444      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
445      ]
446  | Sreturn a_opt ⇒
447    match a_opt with
448    [ None ⇒ match fn_return f with
449      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
450      | _ ⇒ Wrong ??? (msg ReturnMismatch)
451      ]
452    | Some a ⇒
453        match type_eq_dec (fn_return f) Tvoid with
454        [ inl _ ⇒ Wrong ??? (msg ReturnMismatch)
455        | inr _ ⇒
456          ! 〈v,tr〉 ← exec_expr ge e m a;
457          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
458        ]
459    ]
460  | Sswitch a sl ⇒
461      ! 〈v,tr〉 ← exec_expr ge e m a;
462      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
463                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
464  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
465  | Sgoto lbl ⇒
466      match find_label lbl (fn_body f) (call_cont k) with
467      [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]
468      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
469      ]
470  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
471  ]
472| Callstate f0 vargs k m ⇒
473  match f0 with
474  [ CL_Internal f ⇒
475    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒
476      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
477      ret ? 〈E0, State f (fn_body f) k e m2〉
478    ]
479  | CL_External f argtys retty ⇒
480      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
481      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
482      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
483  ]
484| Returnstate res k m ⇒
485  match k with
486  [ Kcall r f e k' ⇒
487    match r with
488    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
489    | Some r' ⇒
490      match r' with [ pair l ty ⇒
491          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
492          ret ? 〈E0, (State f Sskip k' e m')〉
493      ]
494    ]
495  | _ ⇒ Wrong ??? (msg NonsenseState)
496  ]
497].
498
499axiom MainMissing : String.
500
501let rec make_global (p:clight_program) : genv ≝
502  globalenv Genv ?? (fst ??) p.
503
504let rec make_initial_state (p:clight_program) : res state ≝
505  let ge ≝ make_global p in
506  do m0 ← init_mem Genv ?? (fst ??) p;
507  do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p));
508  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b);
509  OK ? (Callstate f (nil ?) Kstop m0).
510
511let rec is_final (s:state) : option int ≝
512match s with
513[ Returnstate res k m ⇒
514  match k with
515  [ Kstop ⇒
516    match res with
517    [ Vint sz r ⇒ intsize_eq_elim ? sz I32 ? r (λr. Some ? r) (None ?)
518    | _ ⇒ None ?
519    ]
520  | _ ⇒ None ?
521  ]
522| _ ⇒ None ?
523].
524
525definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
526#st elim st;
527[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
528| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
529| #v #k #m cases k;
530  [ cases v;
531    [ 2: * #i [ 1,2: %2 % * #r #H inversion H #i' #m #e destruct
532              | %1 ; %{ i} //;
533              ]
534    | 1: %2 ; % *;   #r #H inversion H; #i #m #e destruct;
535    | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
536    | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
537    | #r #b #pc #of %2 ; % *;   #r #H inversion H; #i #m #e destruct;
538    ]
539  | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
540  | 3,4: #a #b #c %2 ; % *; #r #H inversion H; #i #m #e destruct;
541  | 5,6,8: #a #b #c #d %2 ; % *; #r #H inversion H; #i #m #e destruct;
542  | #a %2 ; % *; #r #H inversion H; #i #m #e destruct;
543  ]
544] qed.
545
546let rec exec_steps (n:nat) (ge:genv) (s:state) :
547 IO io_out io_in (trace×state) ≝
548match is_final_state s with
549[ inl _ ⇒ ret ? 〈E0, s〉
550| inr _ ⇒
551  match n with
552  [ O ⇒ ret ? 〈E0, s〉
553  | S n' ⇒
554      ! 〈t,s'〉 ← exec_step ge s;
555      ! 〈t',s''〉 ← exec_steps n' ge s';
556      ret ? 〈t ⧺ t',s''〉
557  ]
558].
559
560definition mem_of_state : state → mem ≝
561λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
562
563definition clight_exec : trans_system io_out io_in ≝
564  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
565
566definition clight_fullexec : fullexec io_out io_in ≝
567  mk_fullexec ??? clight_exec make_global make_initial_state.
Note: See TracBrowser for help on using the repository browser.