source: src/Clight/Cexec.ma @ 2588

Last change on this file since 2588 was 2588, checked in by garnier, 7 years ago

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File size: 22.3 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  | Vptr _ ⇒ match ty with
22    [ Tpointer _ ⇒ OK ? true
23    | _ ⇒ Error ? (msg TypeMismatch)
24    ]
25  | Vnull ⇒ match ty with
26    [ Tpointer _ ⇒ OK ? false
27    | _ ⇒ Error ? (msg TypeMismatch)
28    ]
29  | _ ⇒ Error ? (msg ValueIsNotABoolean)
30  ].
31
32lemma 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.
33#v #ty #r #H elim H; #v #t #H' elim H';
34  [ * #sg #i #ne %{ true} % // whd in ⊢ (??%?); >(eq_bv_false … ne) //
35  | #ptr #ty %{ true} % //
36  | * #sg %{ false} % //
37  | #t %{ false} % //;
38  ]
39qed.
40
41(* Prove a few minor results to make proof obligations easy. *)
42
43lemma bind_OK: ∀A,B,P,e,f.
44  (∀v. e = OK A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
45  match bind A B e f with [ Error _ ⇒ True | OK v ⇒ P v ].
46#A #B #P #e #f elim e; /2/; qed.
47
48lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
49  (∀v:A. ∀p:P v. match f (mk_Sig A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
50  match bind (Sig A P) B e f with [ Error _ ⇒ True | OK v' ⇒ P' v' ].
51#A #B #P #P' #e #f elim e;
52[ #v0 elim v0; #v #Hv #IH @IH
53| #m #_ @I
54] qed.
55
56lemma bind2_OK: ∀A,B,C,P,e,f.
57  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
58  match bind2 A B C e f with [ Error _ ⇒ True | OK v ⇒ P v ].
59#A #B #C #P #e #f elim e; //; #v cases v; /2/; qed.
60
61lemma opt_bind_OK: ∀A,B,P,m,e,f.
62  (∀v. e = Some A v → match f v with [ Error _ ⇒ True | OK v' ⇒ P v' ]) →
63  match bind A B (opt_to_res A m e) f with [ Error _ ⇒ True | OK v ⇒ P v ].
64#A #B #P #m #e #f elim e; normalize; /2/; qed.
65
66
67axiom BadCast : String. (* TODO: refine into more precise errors? *)
68
69definition try_cast_null : ∀m:mem. ∀sz. ∀i:BitVector (bitsize_of_intsize sz). ∀ty:type. ∀ty':type. res val  ≝
70λm:mem. λsz. λi. λty:type. λty':type.
71match eq_bv ? i (zero ?) with
72[ true ⇒
73  match ty with
74  [ Tint sz' _ ⇒
75    if eq_intsize sz sz' then
76      match ty' with
77      [ Tpointer _ ⇒ OK ? Vnull
78      | Tarray _ _ ⇒ OK ? Vnull
79      | Tfunction _ _ ⇒ OK ? Vnull
80      | _ ⇒ Error ? (msg BadCast)
81      ]
82    else Error ? (msg TypeMismatch)
83  | _ ⇒ Error ? (msg BadCast)
84  ]
85| false ⇒ Error ? (msg BadCast)
86].
87
88definition ptr_like_type : type → bool ≝
89λt. match t with
90[ Tpointer _ ⇒ true
91| Tarray _ _ ⇒ true
92| Tfunction _ _ ⇒ true
93| _ ⇒ false
94].
95
96definition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝
97λm:mem. λv:val. λty:type. λty':type.
98match v with
99[ Vint sz i ⇒
100  match ty with
101  [ Tint sz1 si1 ⇒
102    intsize_eq_elim ? sz sz1 ? i
103    (λi.
104      match ty' with
105      [ Tint sz2 si2 ⇒ OK ? (Vint ? (cast_int_int sz1 si1 sz2 i))
106(*      | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))*)
107      | Tpointer _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
108      | Tarray _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
109      | Tfunction _ _ ⇒ do r ← try_cast_null m ? i ty ty'; OK val r
110      | _ ⇒ Error ? (msg BadCast)
111      ])
112    (Error ? (msg BadCast))
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 TypeMismatch)
117  ]
118(*| Vfloat f ⇒
119  match ty with
120  [ Tfloat sz ⇒
121    match ty' with
122    [ Tint sz' si' ⇒ OK ? (Vint sz' (cast_float_int sz' si' f))
123    | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f))
124    | _ ⇒ Error ? (msg BadCast)
125    ]
126  | _ ⇒ Error ? (msg TypeMismatch)
127  ]*)
128| Vptr ptr ⇒
129(*    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
130    do u ← match eq_region_dec (ptype ptr) s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
131    do s' ← match ty' with
132         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
133         | _ ⇒ Error ? (msg BadCast)];
134    match pointer_compat_dec (pblock ptr) s' with
135    [ inl p' ⇒ OK ? (Vptr (mk_pointer s' (pblock ptr) p' (poff ptr)))
136    | inr _ ⇒ Error ? (msg BadCast)
137    ]*)
138    if ptr_like_type ty ∧ ptr_like_type ty' then OK ? (Vptr ptr) else Error ? (msg BadCast)
139| Vnull ⇒
140(*
141    do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? (msg TypeMismatch) ];
142    do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it | inr _ ⇒ Error ? (msg BadCast) ];
143    do s' ← match ty' with
144         [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code
145         | _ ⇒ Error ? (msg BadCast) ];
146    OK ? (Vnull s')*)
147    if ptr_like_type ty ∧ ptr_like_type ty' then OK ? Vnull else Error ? (msg BadCast)
148| _ ⇒ Error ? (msg BadCast)
149].
150
151definition load_value_of_type' ≝
152λty,m,l. let 〈loc,ofs〉 ≝ l in load_value_of_type ty m loc ofs.
153
154axiom BadlyTypedTerm : String.
155axiom UnknownIdentifier : String.
156axiom BadLvalueTerm : String.
157axiom FailedLoad : String.
158axiom FailedOp : String.
159
160(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
161   a structurally smaller value, we break out the surrounding Expr constructor
162   and use exec_lvalue'. *)
163
164let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝
165match e with
166[ Expr e' ty ⇒
167  match e' with
168  [ Econst_int sz i ⇒
169      match ty with
170      [ Tint sz' _ ⇒
171          if eq_intsize sz sz' then OK ? 〈Vint sz i, E0〉
172          else Error ? (msg BadlyTypedTerm)
173      | _ ⇒ Error ? (msg BadlyTypedTerm)
174      ]
175(*  | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉 *)
176  | Evar _ ⇒
177      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
178      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
179      OK ? 〈v,tr〉
180  | Ederef _ ⇒
181      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
182      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
183      OK ? 〈v,tr〉
184  | Efield _ _ ⇒
185      do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
186      do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l);
187      OK ? 〈v,tr〉
188  | Eaddrof a ⇒
189      do 〈lo,tr〉 ← exec_lvalue ge en m a;
190      match ty with
191      [ Tpointer  _ ⇒
192        let 〈loc,ofs〉 ≝ lo in
193(*          match pointer_compat_dec loc r with
194          [ inl pc ⇒ OK ? 〈Vptr (mk_pointer r loc pc ofs), tr〉
195          | inr _ ⇒ Error ? (msg TypeMismatch)
196          ]*)  OK ? 〈Vptr (mk_pointer loc ofs), tr〉
197      | _ ⇒ Error ? (msg BadlyTypedTerm)
198      ]
199  | Esizeof ty' ⇒
200      match ty with
201      [ Tint sz _ ⇒ OK ? 〈Vint sz (repr ? (sizeof ty')), E0〉
202      | _ ⇒ Error ? (msg BadlyTypedTerm)
203      ]
204  | Eunop op a ⇒
205      do 〈v1,tr〉 ← exec_expr ge en m a;
206      do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a));
207      OK ? 〈v,tr〉
208  | Ebinop op a1 a2 ⇒
209      do 〈v1,tr1〉 ← exec_expr ge en m a1;
210      do 〈v2,tr2〉 ← exec_expr ge en m a2;
211      do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m ty);
212      OK ? 〈v,tr1⧺tr2〉
213  | Econdition a1 a2 a3 ⇒
214      do 〈v,tr1〉 ← exec_expr ge en m a1;
215      do b ← exec_bool_of_val v (typeof a1);
216      do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
217                 [ true ⇒ (exec_expr ge en m a2)
218                 | false ⇒ (exec_expr ge en m a3) ];
219      OK ? 〈v',tr1⧺tr2〉
220(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
221  | Eorbool a1 a2 ⇒
222      do 〈v1,tr1〉 ← exec_expr ge en m a1;
223      do b1 ← exec_bool_of_val v1 (typeof a1);
224      match b1 return λ_.res (val×trace) with
225      [ true ⇒
226        match cast_bool_to_target ty (Some ? Vtrue) with
227        [ None ⇒
228          Error ? (msg BadlyTypedTerm)
229        | Some vtr ⇒
230          OK ? 〈vtr,tr1〉 ]
231      | false ⇒
232        do 〈v2,tr2〉 ← exec_expr ge en m a2;
233        do b2 ← exec_bool_of_val v2 (typeof a2);
234        match cast_bool_to_target ty (Some ? (of_bool b2)) with
235        [ None ⇒
236          Error ? (msg BadlyTypedTerm)
237        | Some v2 ⇒
238          OK ? 〈v2,tr1⧺tr2〉 ] ]
239  | Eandbool a1 a2 ⇒
240      do 〈v1,tr1〉 ← exec_expr ge en m a1;
241      do b1 ← exec_bool_of_val v1 (typeof a1);
242      match b1 return λ_.res (val×trace) with
243      [ true ⇒
244        do 〈v2,tr2〉 ← exec_expr ge en m a2;
245        do b2 ← exec_bool_of_val v2 (typeof a2);
246        match cast_bool_to_target ty (Some ? (of_bool b2)) with
247        [ None ⇒
248          Error ? (msg BadlyTypedTerm)
249        | Some v2 ⇒
250          OK ? 〈v2, tr1⧺tr2〉
251        ]
252      | false ⇒
253        match cast_bool_to_target ty (Some ? Vfalse) with
254        [ None ⇒
255          Error ? (msg BadlyTypedTerm)
256        | Some vfls ⇒
257          OK ? 〈vfls,tr1〉 ]
258      ]
259  | Ecast ty' a ⇒
260      do 〈v,tr〉 ← exec_expr ge en m a;
261      do v' ← exec_cast m v (typeof a) ty';
262      OK ? 〈v',tr〉
263  | Ecost l a ⇒
264      do 〈v,tr〉 ← exec_expr ge en m a;
265      OK ? 〈v,(Echarge l)⧺tr〉
266  ]
267]
268and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (block × offset × trace) ≝
269  match e' with
270  [ Evar id ⇒
271      match (lookup ?? en id) with
272      [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol … ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)
273      | Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *)
274      ]
275  | Ederef a ⇒
276      do 〈v,tr〉 ← exec_expr ge en m a;
277      match v with
278      [ Vptr ptr ⇒ OK ? 〈〈pblock ptr, poff ptr〉,tr〉
279      | _ ⇒ Error ? (msg TypeMismatch)
280      ]
281  | Efield a i ⇒
282      match (typeof a) with
283      [ Tstruct id fList ⇒
284          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
285          do delta ← field_offset i fList;
286          OK ? 〈〈\fst lofs,shift_offset ? (\snd lofs) (repr I16 delta)〉,tr〉
287      | Tunion id fList ⇒
288          do 〈lofs,tr〉 ← exec_lvalue ge en m a;
289          OK ? 〈lofs,tr〉
290      | _ ⇒ Error ? (msg BadlyTypedTerm)
291      ]
292  | _ ⇒ Error ? (msg BadLvalueTerm)
293  ]
294and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝
295match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
296
297lemma P_res_to_P: ∀A,P,e,v.  P_res A P e → e = OK A v → P v.
298#A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed.
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  let 〈id,ty〉 ≝ h in
315  let 〈m1,b1〉 ≝ alloc m 0 (sizeof ty) XData in
316      exec_alloc_variables (add ?? en id b1) 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' ⇒ let 〈id,ty〉 ≝ idty in
327      match vs with
328      [ nil ⇒ Error ? (msg WrongNumberOfParameters)
329      | cons v1 vl ⇒
330          do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (lookup ?? e id);
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.
358let 〈loc,ofs〉 ≝ l in
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 : IO ???;
372    ! 〈v2,tr2〉 ← exec_expr ge e m a2 : IO ???;
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 : IO ???;
377    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al : IO ???;
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' : IO ???;
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 : IO ???;
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 : IO ???;
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 : IO ???;
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 : IO ???;
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 : IO ???;
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 : IO ???;
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 : IO ???;
480      match v with
481      [ Vint sz n ⇒
482        match typeof a with
483        [ Tint sz' _ ⇒
484          match sz_eq_dec sz sz' with
485          [ inl _ ⇒
486            ! sl' ← opt_to_io … (msg TypeMismatch) (select_switch sz n sl);
487            ret ? 〈tr, State f (seq_of_labeled_statement sl') (Kswitch k) e m〉
488          | _ ⇒ Wrong ??? (msg TypeMismatch)
489          ]
490        | _ ⇒ Wrong ??? (msg TypeMismatch)
491        ]
492      | _ ⇒ Wrong ??? (msg TypeMismatch)]
493  | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉
494  | Sgoto lbl ⇒
495      match find_label lbl (fn_body f) (call_cont k) with
496      [ Some sk' ⇒ let 〈s',k'〉 ≝ sk' in ret ? 〈E0, State f s' k' e m〉
497      | None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl]
498      ]
499  | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉
500  ]
501| Callstate f0 vargs k m ⇒
502  match f0 with
503  [ CL_Internal f ⇒
504    let 〈e,m1〉 ≝ exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) in
505      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs : IO ???;
506      ret ? 〈E0, State f (fn_body f) k e m2〉
507  | CL_External f argtys retty ⇒
508      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys) : IO ???;
509      ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty));
510      ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉
511  ]
512| Returnstate res k m ⇒
513  match k with
514  [ Kcall r f e k' ⇒
515    match r with
516    [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉
517    | Some r' ⇒
518      let 〈l,ty〉 ≝ r' in
519          ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res);
520          ret ? 〈E0, (State f Sskip k' e m')〉
521    ]
522  | Kstop ⇒
523    match res with
524    [ Vint sz r ⇒ match sz return λsz.bvint sz → ? with [ I32 ⇒ λr. ret ? 〈E0, Finalstate r〉 | _ ⇒ λ_. Wrong ??? (msg ReturnMismatch) ] r
525    | _ ⇒ Wrong ??? (msg ReturnMismatch)
526    ]
527  | _ ⇒ Wrong ??? (msg NonsenseState)
528  ]
529| Finalstate r ⇒
530    Wrong ??? (msg NonsenseState)
531].
532
533axiom MainMissing : String.
534
535definition make_global : clight_program → genv ≝
536λp. globalenv … (fst ??) p.
537
538let rec make_initial_state (p:clight_program) : res state ≝
539  let ge ≝ make_global p in
540  do m0 ← init_mem … (fst ??) p;
541  do b ← opt_to_res ? (msg MainMissing) (find_symbol … ge (prog_main ?? p));
542  do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr … ge b);
543  OK ? (Callstate f (nil ?) Kstop m0).
544
545let rec is_final (s:state) : option int ≝
546match s with
547[ Finalstate r ⇒ Some ? r
548| _ ⇒ None ?
549].
550
551definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r).
552#st elim st;
553[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
554| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
555| #v #k #m %2 % * #r #H inversion H #H1 #H2 #H3 #H4 destruct
556| #r %1 %{r} %
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''〉 ← exec_steps n' ge s';
569      ret ? 〈t ⧺ t',s''〉
570  ]
571].
572(*
573definition mem_of_state : state → mem ≝
574λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
575*)
576definition clight_exec : trans_system io_out io_in ≝
577  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
578
579definition clight_fullexec : fullexec io_out io_in ≝
580  mk_fullexec ??? clight_exec make_global make_initial_state.
581
582
583(* A few lemmas about the semantics. *)
584
585lemma cl_step_not_final : ∀ge,s1,tr,s2.
586  exec_step ge s1 = OK … 〈tr,s2〉 →
587  is_final s1 = None ?.
588#ge * //
589#r #tr #s2 #E
590whd in E:(??%%);
591destruct
592qed.
593
594(* If you can step in Clight, then you aren't in a final state.  Hence we can
595   give nicer constructors for plus. *)
596lemma cl_plus_one : ∀ge,s1,tr,s2.
597  exec_step ge s1 = OK … 〈tr,s2〉 →
598  plus … clight_exec ge s1 tr s2.
599#ge #s1 #tr #s2 #EX @(plus_one … EX) /2/
600qed.
601
602lemma cl_plus_succ : ∀ge,s1,tr,s2,tr',s3.
603    exec_step ge s1 = OK … 〈tr,s2〉 →
604    plus … clight_exec ge s2 tr' s3 →
605    plus … clight_exec ge s1 (tr⧺tr') s3.
606#ge #s1 #tr #s2 #tr' #s3 #EX @plus_succ /2/ @EX
607qed.
608
Note: See TracBrowser for help on using the repository browser.