source: src/Clight/Cexec.ma @ 764

Last change on this file since 764 was 744, checked in by campbell, 10 years ago

Evict Coq-style integers from common/Integers.ma.

Make more bitvector operations more efficient to retain the ability to
animate semantics.

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