source: src/Clight/Cexec.ma @ 1139

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

Shift init_data out of generic program record so that it only appears
in programs that contain initialisation data (Clight and Cminor). Other
stages just have the size of each variable and translate it to Init_space
when building the initial state.

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