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