source: src/Clight/Cexec.ma @ 2672

Last change on this file since 2672 was 2645, checked in by sacerdot, 8 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 21.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
9definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝
10  λA,P,a. match a with [ Error _ ⇒ True | OK v ⇒ P v ].
11
12definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝
13  λv,ty. match v in val with
14  [ Vint sz i ⇒ match ty with
15    [ Tint sz' _ ⇒ intsize_eq_elim ? sz sz' ? i
16                   (λi. OK ? (¬eq_bv ? i (zero ?))) (Error ? (msg TypeMismatch))
17    | _ ⇒ Error ? (msg TypeMismatch)
18    ]
19  | Vptr _ ⇒ match ty with
20    [ Tpointer _ ⇒ OK ? true
21    | _ ⇒ Error ? (msg TypeMismatch)
22    ]
23  | Vnull ⇒ match ty with
24    [ Tpointer _ ⇒ OK ? false
25    | _ ⇒ Error ? (msg TypeMismatch)
26    ]
27  | _ ⇒ Error ? (msg ValueIsNotABoolean)
28  ].
29
30lemma 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.
31#v #ty #r #H elim H; #v #t #H' elim H';
32  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
33  | #ptr #ty %{ true} % //
34  | * #sg %{ false} % //
35  | #t %{ false} % //;
36  ]
37qed.
38
39(* Prove a few minor results to make proof obligations easy. *)
40
41lemma bind_OK: ∀A,B,P,e,f.
42  (∀v. e = OK A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
43  match bind A B e f with [ Error _ ⇒ True | OK v ⇒ P v ].
44#A #B #P #e #f elim e; /2/; qed.
45
46lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
47  (∀v:A. ∀p:P v. match f (mk_Sig A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
48  match bind (Sig A P) B e f with [ Error _ ⇒ True | OK v' ⇒ P' v' ].
49#A #B #P #P' #e #f elim e;
50[ #v0 elim v0; #v #Hv #IH @IH
51| #m #_ @I
52] qed.
53
54lemma bind2_OK: ∀A,B,C,P,e,f.
55  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
56  match bind2 A B C e f with [ Error _ ⇒ True | OK v ⇒ P v ].
57#A #B #C #P #e #f elim e; //; #v cases v; /2/; qed.
58
59lemma opt_bind_OK: ∀A,B,P,m,e,f.
60  (∀v. e = Some A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
61  match bind A B (opt_to_res A m e) f with [ Error _ ⇒ True | OK v ⇒ P v ].
62#A #B #P #m #e #f elim e; normalize; /2/; qed.
63
64
65definition try_cast_null : ∀m:mem. ∀sz. ∀i:BitVector (bitsize_of_intsize sz). ∀ty:type. ∀ty':type. res val  ≝
66λm:mem. λsz. λi. λty:type. λty':type.
67match eq_bv ? i (zero ?) with
68[ true ⇒
69  match ty with
70  [ Tint sz' _ ⇒
71    if eq_intsize sz sz' then
72      match ty' with
73      [ Tpointer _ ⇒ OK ? Vnull
74      | Tarray _ _ ⇒ OK ? Vnull
75      | Tfunction _ _ ⇒ OK ? Vnull
76      | _ ⇒ Error ? (msg BadCast)
77      ]
78    else Error ? (msg TypeMismatch)
79  | _ ⇒ Error ? (msg BadCast)
80  ]
81| false ⇒ Error ? (msg BadCast)
82].
83
84definition ptr_like_type : type → bool ≝
85λt. match t with
86[ Tpointer _ ⇒ true
87| Tarray _ _ ⇒ true
88| Tfunction _ _ ⇒ true
89| _ ⇒ false
90].
91
92definition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
93λm:mem. λv:val. λty:type. λty':type.
94match v with
95[ Vint sz i ⇒
96  match ty with
97  [ Tint sz1 si1 ⇒
98    intsize_eq_elim ? sz sz1 ? i
99    (λi.
100      match ty' with
101      [ Tint sz2 si2 ⇒ OK ? (Vint ? (cast_int_int sz1 si1 sz2 i))
102(*      | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))*)
103      | Tpointer _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
104      | Tarray _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
105      | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
106      | _ ⇒ Error ? (msg BadCast)
107      ])
108    (Error ? (msg BadCast))
109  | Tpointer _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
110  | Tarray _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
111  | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
112  | _ ⇒ Error ? (msg TypeMismatch)
113  ]
114(*| Vfloat f ⇒
115  match ty with
116  [ Tfloat sz ⇒
117    match ty' with
118    [ Tint sz' si' ⇒ OK ? (Vint sz' (cast_float_int sz' si' f))
119    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
120    | _ ⇒ Error ? (msg BadCast)
121    ]
122  | _ ⇒ Error ? (msg TypeMismatch)
123  ]*)
124| Vptr ptr ⇒
125(*    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
126    do u ← match eq_region_dec (ptype ptr) s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
127    do s' ← match ty' with
128         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
129         | _ ⇒ Error ? (msg BadCast)];
130    match pointer_compat_dec (pblock ptr) s' with
131    [ inl p' ⇒ OK ? (Vptr (mk_pointer s' (pblock ptr) p' (poff ptr)))
132    | inr _ ⇒ Error ? (msg BadCast)
133    ]*)
134    if ptr_like_type ty ∧ ptr_like_type ty' then OK ? (Vptr ptr) else Error ? (msg BadCast)
135| Vnull ⇒
136(*
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    if ptr_like_type ty ∧ ptr_like_type ty' then OK ? Vnull else Error ? (msg BadCast)
144| _ ⇒ Error ? (msg BadCast)
145].
146
147definition load_value_of_type' ≝
148λty,m,l. let 〈loc,ofs〉 ≝ l in load_value_of_type ty m loc ofs.
149
150(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
151   a structurally smaller value, we break out the surrounding Expr constructor
152   and use exec_lvalue'. *)
153
154let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
155match e with
156[ Expr e' ty ⇒
157  match e' with
158  [ Econst_int sz i ⇒
159      match ty with
160      [ Tint sz' _ ⇒
161          if eq_intsize sz sz' then OK ? 〈Vint sz i, E0〉
162          else Error ? (msg BadlyTypedTerm)
163      | _ ⇒ Error ? (msg BadlyTypedTerm)
164      ]
165(*  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉 *)
166  | Evar _ ⇒
167      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
168      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
169      OK ? 〈v,tr〉
170  | Ederef _ ⇒
171      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
172      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
173      OK ? 〈v,tr〉
174  | Efield _ _ ⇒
175      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
176      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
177      OK ? 〈v,tr〉
178  | Eaddrof a ⇒
179      do 〈lo,tr〉 ← exec_lvalue ge en m a;
180      match ty with
181      [ Tpointer  _ ⇒
182        let 〈loc,ofs〉 ≝ lo in
183(*          match pointer_compat_dec loc r with
184          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
185          | inr _ ⇒ Error ? (msg TypeMismatch)
186          ]*)  OK ? 〈Vptr (mk_pointer loc ofs), tr〉
187      | _ ⇒ Error ? (msg BadlyTypedTerm)
188      ]
189  | Esizeof ty' ⇒
190      match ty with
191      [ Tint sz _ ⇒ OK ? 〈Vint sz (repr ? (sizeof ty')), E0〉
192      | _ ⇒ Error ? (msg BadlyTypedTerm)
193      ]
194  | Eunop op a ⇒
195      do 〈v1,tr〉 ← exec_expr ge en m a;
196      do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a));
197      OK ? 〈v,tr〉
198  | Ebinop op a1 a2 ⇒
199      do 〈v1,tr1〉 ← exec_expr ge en m a1;
200      do 〈v2,tr2〉 ← exec_expr ge en m a2;
201      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m ty);
202      OK ? 〈v,tr1⧺tr2〉
203  | Econdition a1 a2 a3 ⇒
204      do 〈v,tr1〉 ← exec_expr ge en m a1;
205      do b ← exec_bool_of_val v (typeof a1);
206      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
207                 [ true ⇒ (exec_expr ge en m a2)
208                 | false ⇒ (exec_expr ge en m a3) ];
209      OK ? 〈v',tr1⧺tr2〉
210(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
211  | Eorbool a1 a2 ⇒
212      do 〈v1,tr1〉 ← exec_expr ge en m a1;
213      do b1 ← exec_bool_of_val v1 (typeof a1);
214      match b1 return λ_.res (val×trace) with
215      [ true ⇒
216        match cast_bool_to_target ty (Some ? Vtrue) with
217        [ None ⇒
218          Error ? (msg BadlyTypedTerm)
219        | Some vtr ⇒
220          OK ? 〈vtr,tr1〉 ]
221      | false ⇒
222        do 〈v2,tr2〉 ← exec_expr ge en m a2;
223        do b2 ← exec_bool_of_val v2 (typeof a2);
224        match cast_bool_to_target ty (Some ? (of_bool b2)) with
225        [ None ⇒
226          Error ? (msg BadlyTypedTerm)
227        | Some v2 ⇒
228          OK ? 〈v2,tr1⧺tr2〉 ] ]
229  | Eandbool a1 a2 ⇒
230      do 〈v1,tr1〉 ← exec_expr ge en m a1;
231      do b1 ← exec_bool_of_val v1 (typeof a1);
232      match b1 return λ_.res (val×trace) with
233      [ true ⇒
234        do 〈v2,tr2〉 ← exec_expr ge en m a2;
235        do b2 ← exec_bool_of_val v2 (typeof a2);
236        match cast_bool_to_target ty (Some ? (of_bool b2)) with
237        [ None ⇒
238          Error ? (msg BadlyTypedTerm)
239        | Some v2 ⇒
240          OK ? 〈v2, tr1⧺tr2〉
241        ]
242      | false ⇒
243        match cast_bool_to_target ty (Some ? Vfalse) with
244        [ None ⇒
245          Error ? (msg BadlyTypedTerm)
246        | Some vfls ⇒
247          OK ? 〈vfls,tr1〉 ]
248      ]
249  | Ecast ty' a ⇒
250      do 〈v,tr〉 ← exec_expr ge en m a;
251      do v' ← exec_cast m v (typeof a) ty';
252      OK ? 〈v',tr〉
253  | Ecost l a ⇒
254      do 〈v,tr〉 ← exec_expr ge en m a;
255      OK ? 〈v,(Echarge l)⧺tr〉
256  ]
257]
258and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
259  match e' with
260  [ Evar id ⇒
261      match (lookup ?? en id) with
262      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol … ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
263      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
264      ]
265  | Ederef a ⇒
266      do 〈v,tr〉 ← exec_expr ge en m a;
267      match v with
268      [ Vptr ptr ⇒ OK ? 〈〈pblock ptr, poff ptr〉,tr〉
269      | _ ⇒ Error ? (msg TypeMismatch)
270      ]
271  | Efield a i ⇒
272      match (typeof a) with
273      [ Tstruct id fList ⇒
274          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
275          do delta ← field_offset i fList;
276          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I16 delta)〉,tr〉
277      | Tunion id fList ⇒
278          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
279          OK ? 〈lofs,tr〉
280      | _ ⇒ Error ? (msg BadlyTypedTerm)
281      ]
282  | _ ⇒ Error ? (msg BadLvalueTerm)
283  ]
284and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
285match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
286
287lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
288#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
289
290(* TODO: Can we do this sensibly with a map combinator? *)
291let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝
292match l with
293[ nil ⇒ OK ? 〈nil val, E0〉
294| cons e1 es ⇒
295  do 〈v,tr1〉 ← exec_expr ge e m e1;
296  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
297  OK ? 〈cons val v vs, tr1⧺tr2〉
298].
299
300let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝
301match l with
302[ nil ⇒ 〈en, m〉
303| cons h vars ⇒
304  let 〈id,ty〉 ≝ h in
305  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) (* XData *) in
306      exec_alloc_variables (add ?? en id b1) m1 vars
307].
308
309(* TODO: can we establish that length params = length vs in advance? *)
310let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝
311  match params with
312  [ nil ⇒ match vs with [ nil ⇒ OK ? m | cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ]
313  | cons idty params' ⇒ let 〈id,ty〉 ≝ idty in
314      match vs with
315      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
316      | cons v1 vl ⇒
317          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (lookup ?? e id);
318          do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1);
319          exec_bind_parameters e m1 params' vl
320      ]
321  ].
322
323let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝
324match k return λk'.(is_call_cont k') + (¬is_call_cont k') with
325[ Kstop ⇒ ?
326| Kcall _ _ _ _ ⇒ ?
327| _ ⇒ ?
328].
329[ 1,8: %1 ; //
330| *: %2 ; /2/
331] qed.
332
333definition is_Sskip : ∀s:statement. (s = Sskip) ⊎ (s ≠ Sskip) ≝
334λs.match s return λs'.(s' = Sskip) ⊎ (s' ≠ Sskip) with
335[ Sskip ⇒ inl ?? (refl ??)
336| _ ⇒ inr ?? (nmk ? (λH.?))
337]. destruct
338qed.
339
340
341(* execution *)
342
343definition store_value_of_type' ≝
344λty,m,l,v.
345let 〈loc,ofs〉 ≝ l in
346  store_value_of_type ty m loc ofs v.
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 : IO ???;
354    ! 〈v2,tr2〉 ← exec_expr ge e m a2 : IO ???;
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 : IO ???;
359    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
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' : IO ???;
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 : IO ???;
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 : IO ???;
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 : IO ???;
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 : IO ???;
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 : IO ???;
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 : IO ???;
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 : IO ???;
462      match v with
463      [ Vint sz n ⇒
464        match typeof a with
465        [ Tint sz' _ ⇒
466          match sz_eq_dec sz sz' with
467          [ inl _ ⇒
468            ! sl' ← opt_to_io … (msg TypeMismatch) (select_switch sz n sl);
469            ret ? 〈tr, State f (seq_of_labeled_statement sl') (Kswitch k) e m〉
470          | _ ⇒ Wrong ??? (msg TypeMismatch)
471          ]
472        | _ ⇒ Wrong ??? (msg TypeMismatch)
473        ]
474      | _ ⇒ Wrong ??? (msg TypeMismatch)]
475  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
476  | Sgoto lbl ⇒
477      match find_label lbl (fn_body f) (call_cont k) with
478      [ Some sk' ⇒ let 〈s',k'〉 ≝ sk' in ret ? 〈E0, State f s' k' e m〉
479      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
480      ]
481  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
482  ]
483| Callstate f0 vargs k m ⇒
484  match f0 with
485  [ CL_Internal f ⇒
486    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
487      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs : IO ???;
488      ret ? 〈E0, State f (fn_body f) k e m2〉
489  | CL_External f argtys retty ⇒
490      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys) : IO ???;
491      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
492      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
493  ]
494| Returnstate res k m ⇒
495  match k with
496  [ Kcall r f e k' ⇒
497    match r with
498    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
499    | Some r' ⇒
500      let 〈l,ty〉 ≝ r' in
501          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
502          ret ? 〈E0, (State f Sskip k' e m')〉
503    ]
504  | Kstop ⇒
505    match res with
506    [ Vint sz r ⇒ match sz return λsz.bvint sz → ? with [ I32 ⇒ λr. ret ? 〈E0, Finalstate r〉 | _ ⇒ λ_. Wrong ??? (msg ReturnMismatch) ] r
507    | _ ⇒ Wrong ??? (msg ReturnMismatch)
508    ]
509  | _ ⇒ Wrong ??? (msg NonsenseState)
510  ]
511| Finalstate r ⇒
512    Wrong ??? (msg NonsenseState)
513].
514
515definition make_global : clight_program → genv ≝
516λp. globalenv … (fst ??) p.
517
518let rec make_initial_state (p:clight_program) : res state ≝
519  let ge ≝ make_global p in
520  do m0 ← init_mem … (fst ??) p;
521  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
522  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
523  OK ? (Callstate f (nil ?) Kstop m0).
524
525let rec is_final (s:state) : option int ≝
526match s with
527[ Finalstate r ⇒ Some ? r
528| _ ⇒ None ?
529].
530
531definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
532#st elim st;
533[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
534| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
535| #v #k #m %2 % * #r #H inversion H #H1 #H2 #H3 #H4 destruct
536| #r %1 %{r} %
537] qed.
538
539let rec exec_steps (n:nat) (ge:genv) (s:state) :
540 IO io_out io_in (trace×state) ≝
541match is_final_state s with
542[ inl _ ⇒ ret ? 〈E0, s〉
543| inr _ ⇒
544  match n with
545  [ O ⇒ ret ? 〈E0, s〉
546  | S n' ⇒
547      ! 〈t,s'〉 ← exec_step ge s;
548      ! 〈t',s''〉 ← exec_steps n' ge s';
549      ret ? 〈t ⧺ t',s''〉
550  ]
551].
552(*
553definition mem_of_state : state → mem ≝
554λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
555*)
556definition clight_exec : trans_system io_out io_in ≝
557  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
558
559definition clight_fullexec : fullexec io_out io_in ≝
560  mk_fullexec ??? clight_exec make_global make_initial_state.
561
562
563(* A few lemmas about the semantics. *)
564
565lemma cl_step_not_final : ∀ge,s1,tr,s2.
566  exec_step ge s1 = OK … 〈tr,s2〉 →
567  is_final s1 = None ?.
568#ge * //
569#r #tr #s2 #E
570whd in E:(??%%);
571destruct
572qed.
573
574(* If you can step in Clight, then you aren't in a final state.  Hence we can
575   give nicer constructors for plus. *)
576lemma cl_plus_one : ∀ge,s1,tr,s2.
577  exec_step ge s1 = OK … 〈tr,s2〉 →
578  plus … clight_exec ge s1 tr s2.
579#ge #s1 #tr #s2 #EX @(plus_one … EX) /2/
580qed.
581
582lemma cl_plus_succ : ∀ge,s1,tr,s2,tr',s3.
583    exec_step ge s1 = OK … 〈tr,s2〉 →
584    plus … clight_exec ge s2 tr' s3 →
585    plus … clight_exec ge s1 (tr⧺tr') s3.
586#ge #s1 #tr #s2 #tr' #s3 #EX @plus_succ /2/ @EX
587qed.
588
Note: See TracBrowser for help on using the repository browser.