source: src/Clight/Cexec.ma @ 1988

Last change on this file since 1988 was 1988, checked in by campbell, 6 years ago

Abstraction of the memory contents in the memory models is no longer
necessary.

File size: 21.0 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  | #ptr #r #ty %{ 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 (mk_Sig 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 ptr ⇒
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 (ptype ptr) 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 (pblock ptr) s' with
133    [ inl p' ⇒ OK ? (Vptr (mk_pointer s' (pblock ptr) p' (poff ptr)))
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. let 〈loc,ofs〉 ≝ l in 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        let 〈loc,ofs〉 ≝ lo in
188          match pointer_compat_dec loc r with
189          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
190          | inr _ ⇒ Error ? (msg TypeMismatch)
191          ]
192      | _ ⇒ Error ? (msg BadlyTypedTerm)
193      ]
194  | Esizeof ty' ⇒
195      match ty with
196      [ Tint sz _ ⇒ OK ? 〈Vint sz (repr ? (sizeof ty')), E0〉
197      | _ ⇒ Error ? (msg BadlyTypedTerm)
198      ]
199  | Eunop op a ⇒
200      do 〈v1,tr〉 ← exec_expr ge en m a;
201      do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a));
202      OK ? 〈v,tr〉
203  | Ebinop op a1 a2 ⇒
204      do 〈v1,tr1〉 ← exec_expr ge en m a1;
205      do 〈v2,tr2〉 ← exec_expr ge en m a2;
206      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
207      OK ? 〈v,tr1⧺tr2〉
208  | Econdition a1 a2 a3 ⇒
209      do 〈v,tr1〉 ← exec_expr ge en m a1;
210      do b ← exec_bool_of_val v (typeof a1);
211      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
212                 [ true ⇒ (exec_expr ge en m a2)
213                 | false ⇒ (exec_expr ge en m a3) ];
214      OK ? 〈v',tr1⧺tr2〉
215(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
216  | Eorbool a1 a2 ⇒
217      do 〈v1,tr1〉 ← exec_expr ge en m a1;
218      do b1 ← exec_bool_of_val v1 (typeof a1);
219      match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒
220        do 〈v2,tr2〉 ← exec_expr ge en m a2;
221        do b2 ← exec_bool_of_val v2 (typeof a2);
222        OK ? 〈of_bool b2, tr1⧺tr2〉 ]
223  | Eandbool a1 a2 ⇒
224      do 〈v1,tr1〉 ← exec_expr ge en m a1;
225      do b1 ← exec_bool_of_val v1 (typeof a1);
226      match b1 return λ_.res (val×trace) with [ true ⇒
227        do 〈v2,tr2〉 ← exec_expr ge en m a2;
228        do b2 ← exec_bool_of_val v2 (typeof a2);
229        OK ? 〈of_bool b2, tr1⧺tr2〉
230      | false ⇒ OK ? 〈Vfalse,tr1〉 ]
231  | Ecast ty' a ⇒
232      do 〈v,tr〉 ← exec_expr ge en m a;
233      do v' ← exec_cast m v (typeof a) ty';
234      OK ? 〈v',tr〉
235  | Ecost l a ⇒
236      do 〈v,tr〉 ← exec_expr ge en m a;
237      OK ? 〈v,tr⧺(Echarge l)〉
238  ]
239]
240and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
241  match e' with
242  [ Evar id ⇒
243      match (lookup ?? en id) with
244      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol … ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
245      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
246      ]
247  | Ederef a ⇒
248      do 〈v,tr〉 ← exec_expr ge en m a;
249      match v with
250      [ Vptr ptr ⇒ OK ? 〈〈pblock ptr, poff ptr〉,tr〉
251      | _ ⇒ Error ? (msg TypeMismatch)
252      ]
253  | Efield a i ⇒
254      match (typeof a) with
255      [ Tstruct id fList ⇒
256          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
257          do delta ← field_offset i fList;
258          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I32 delta)〉,tr〉
259      | Tunion id fList ⇒
260          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
261          OK ? 〈lofs,tr〉
262      | _ ⇒ Error ? (msg BadlyTypedTerm)
263      ]
264  | _ ⇒ Error ? (msg BadLvalueTerm)
265  ]
266and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
267match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
268
269lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
270#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
271
272(* We define a special induction principle tailored to the recursive definition
273   above. *)
274
275definition is_not_lvalue: expr_descr → Prop ≝
276λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ].
277
278definition Plvalue ≝ λP:(expr → Prop).λe,ty.
279match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ].
280
281(* TODO: Can we do this sensibly with a map combinator? *)
282let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
283match l with
284[ nil ⇒ OK ? 〈nil val, E0〉
285| cons e1 es ⇒
286  do 〈v,tr1〉 ← exec_expr ge e m e1;
287  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
288  OK ? 〈cons val v vs, tr1⧺tr2〉
289].
290
291let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝
292match l with
293[ nil ⇒ 〈en, m〉
294| cons h vars ⇒
295  let 〈id,ty〉 ≝ h in
296  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) Any in
297      exec_alloc_variables (add ?? en id b1) m1 vars
298].
299
300axiom WrongNumberOfParameters : String.
301axiom FailedStore : String.
302
303(* TODO: can we establish that length params = length vs in advance? *)
304let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
305  match params with
306  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
307  | cons idty params' ⇒ let 〈id,ty〉 ≝ idty in
308      match vs with
309      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
310      | cons v1 vl ⇒
311          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (lookup ?? e id);
312          do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1);
313          exec_bind_parameters e m1 params' vl
314      ]
315  ].
316
317let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
318match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
319[ Kstop ⇒ ?
320| Kcall _ _ _ _ ⇒ ?
321| _ ⇒ ?
322].
323[ 1,8: %1 ; //
324| *: %2 ; /2/
325] qed.
326
327definition is_Sskip : ∀s:statement. (s = Sskip) ⊎ (s ≠ Sskip) ≝
328λs.match s return λs'.(s' = Sskip) ⊎ (s' ≠ Sskip) with
329[ Sskip ⇒ inl ?? (refl ??)
330| _ ⇒ inr ?? (nmk ? (λH.?))
331]. destruct
332qed.
333
334
335(* execution *)
336
337definition store_value_of_type' ≝
338λty,m,l,v.
339let 〈loc,ofs〉 ≝ l in
340  store_value_of_type ty m loc ofs v.
341
342axiom NonsenseState : String.
343axiom ReturnMismatch : String.
344axiom UnknownLabel : String.
345axiom BadFunctionValue : String.
346
347let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝
348match st with
349[ State f s k e m ⇒
350  match s with
351  [ Sassign a1 a2 ⇒
352    ! 〈l,tr1〉 ← exec_lvalue ge e m a1 : IO ???;
353    ! 〈v2,tr2〉 ← exec_expr ge e m a2 : IO ???;
354    ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2);
355    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉
356  | Scall lhs a al ⇒
357    ! 〈vf,tr2〉 ← exec_expr ge e m a : IO ???;
358    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
359    ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct … ge vf);
360    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a));
361(* requires associativity of IOMonad, so rearrange it below
362    ! k' ← match lhs with
363         [ None ⇒ ret ? (Kcall (None ?) f e k)
364         | Some lhs' ⇒
365           ! locofs ← exec_lvalue ge e m lhs';
366           ret ? (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k)
367         ];
368    ret ? 〈E0, Callstate fd vargs k' m〉)
369*)
370    match lhs with
371         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
372         | Some lhs' ⇒
373           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs' : IO ???;
374           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
375         ]
376  | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉
377  | Sskip ⇒
378      match k with
379      [ Kseq s k' ⇒ ret ? 〈E0, State  f s k' e m〉
380      | Kstop ⇒
381          match fn_return f with
382          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
383          | _ ⇒ Wrong ??? (msg NonsenseState)
384          ]
385      | Kcall _ _ _ _ ⇒
386          match fn_return f with
387          [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉
388          | _ ⇒ Wrong ??? (msg NonsenseState)
389          ]
390      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
391      | Kdowhile a s' k' ⇒
392          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
393          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
394          match b with
395          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
396          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
397          ]
398      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
399      | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉
400      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
401      | _ ⇒ Wrong ??? (msg NonsenseState)
402      ]
403  | Scontinue ⇒
404      match k with
405      [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
406      | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉
407      | Kdowhile a s' k' ⇒
408          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
409          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
410          match b with
411          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
412          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
413          ]
414      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉
415      | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉
416      | _ ⇒ Wrong ??? (msg NonsenseState)
417      ]
418  | Sbreak ⇒
419      match k with
420      [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉
421      | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
422      | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
423      | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
424      | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉
425      | _ ⇒ Wrong ??? (msg NonsenseState)
426      ]
427  | Sifthenelse a s1 s2 ⇒
428      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
429      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
430      ret ? 〈tr, State f (if b then s1 else s2) k e m〉
431  | Swhile a s' ⇒
432      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
433      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
434      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
435                      else State f Sskip k e m〉
436  | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉
437  | Sfor a1 a2 a3 s' ⇒
438      match is_Sskip a1 with
439      [ inl _ ⇒
440          ! 〈v,tr〉 ← exec_expr ge e m a2 : IO ???;
441          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
442          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉
443      | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉
444      ]
445  | Sreturn a_opt ⇒
446    match a_opt with
447    [ None ⇒ match fn_return f with
448      [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉
449      | _ ⇒ Wrong ??? (msg ReturnMismatch)
450      ]
451    | Some a ⇒
452        match type_eq_dec (fn_return f) Tvoid with
453        [ inl _ ⇒ Wrong ??? (msg ReturnMismatch)
454        | inr _ ⇒
455          ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
456          ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉
457        ]
458    ]
459  | Sswitch a sl ⇒
460      ! 〈v,tr〉 ← exec_expr ge e m a : IO ???;
461      match v with [ Vint sz n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch sz n sl)) (Kswitch k) e m〉
462                   | _ ⇒ Wrong ??? (msg TypeMismatch)]
463  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
464  | Sgoto lbl ⇒
465      match find_label lbl (fn_body f) (call_cont k) with
466      [ Some sk' ⇒ let 〈s',k'〉 ≝ sk' in ret ? 〈E0, State f s' k' e m〉
467      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
468      ]
469  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
470  ]
471| Callstate f0 vargs k m ⇒
472  match f0 with
473  [ CL_Internal f ⇒
474    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
475      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs : IO ???;
476      ret ? 〈E0, State f (fn_body f) k e m2〉
477  | CL_External f argtys retty ⇒
478      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys) : IO ???;
479      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
480      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
481  ]
482| Returnstate res k m ⇒
483  match k with
484  [ Kcall r f e k' ⇒
485    match r with
486    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
487    | Some r' ⇒
488      let 〈l,ty〉 ≝ r' in
489          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
490          ret ? 〈E0, (State f Sskip k' e m')〉
491    ]
492  | Kstop ⇒
493    match res with
494    [ Vint sz r ⇒ match sz return λsz.bvint sz → ? with [ I32 ⇒ λr. ret ? 〈E0, Finalstate r〉 | _ ⇒ λ_. Wrong ??? (msg ReturnMismatch) ] r
495    | _ ⇒ Wrong ??? (msg ReturnMismatch)
496    ]
497  | _ ⇒ Wrong ??? (msg NonsenseState)
498  ]
499| Finalstate r ⇒
500    Wrong ??? (msg NonsenseState)
501].
502
503axiom MainMissing : String.
504
505definition make_global : clight_program → genv ≝
506λp. globalenv … (fst ??) p.
507
508let rec make_initial_state (p:clight_program) : res state ≝
509  let ge ≝ make_global p in
510  do m0 ← init_mem … (fst ??) p;
511  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
512  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
513  OK ? (Callstate f (nil ?) Kstop m0).
514
515let rec is_final (s:state) : option int ≝
516match s with
517[ Finalstate r ⇒ Some ? r
518| _ ⇒ None ?
519].
520
521definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
522#st elim st;
523[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
524| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
525| #v #k #m %2 % * #r #H inversion H #H1 #H2 #H3 #H4 destruct
526| #r %1 %{r} %
527] qed.
528
529let rec exec_steps (n:nat) (ge:genv) (s:state) :
530 IO io_out io_in (trace×state) ≝
531match is_final_state s with
532[ inl _ ⇒ ret ? 〈E0, s〉
533| inr _ ⇒
534  match n with
535  [ O ⇒ ret ? 〈E0, s〉
536  | S n' ⇒
537      ! 〈t,s'〉 ← exec_step ge s;
538      ! 〈t',s''〉 ← exec_steps n' ge s';
539      ret ? 〈t ⧺ t',s''〉
540  ]
541].
542(*
543definition mem_of_state : state → mem ≝
544λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
545*)
546definition clight_exec : trans_system io_out io_in ≝
547  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
548
549definition clight_fullexec : fullexec io_out io_in ≝
550  mk_fullexec ??? clight_exec make_global make_initial_state.
Note: See TracBrowser for help on using the repository browser.