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