source: src/Clight/Cexec.ma @ 2176

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

Remove memory spaces other than XData and Code; simplify pointers as a
result.

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