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