Changeset 124 for Csemantics/CexecIO.ma
 Timestamp:
 Sep 24, 2010, 10:31:32 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/CexecIO.ma
r25 r124 5 5 include "IOMonad.ma". 6 6 7 (* Some experimental definitions for an executable semantics. *)8 9 ndefinition bool_of_val_1 : val → type → res val ≝10 λv,ty. match v with11 [ Vint i ⇒ match ty with12 [ Tint _ _ ⇒ OK ? (of_bool (¬eq i zero))13  Tpointer _ ⇒ OK ? (of_bool (¬eq i zero))14  _ ⇒ Error ?15 ]16  Vfloat f ⇒ match ty with17 [ Tfloat _ ⇒ OK ? (of_bool (¬Fcmp Ceq f Fzero))18  _ ⇒ Error ?19 ]20  Vptr _ _ ⇒ match ty with21 [ Tint _ _ ⇒ OK ? Vtrue22  Tpointer _ ⇒ OK ? Vtrue23  _ ⇒ Error ?24 ]25  _ ⇒ Error ?26 ].27 28 (* There's a lot more repetition than I'd like here, in large part because29 there's no way to introduce different numbers of hypotheses when doing the30 case distinctions. *)31 32 nlemma bool_of_val_1_ok : ∀v,ty,r. bool_of_val_1 v ty = OK ? r ↔ bool_of_val v ty r.33 #v ty r; @;34 ##[35 nelim v; ##[ #H; nnormalize in H; ndestruct; ## ##2,3: #x; ## ##4: #x y; ##]36 ncases ty;37 ##[ ##1,10,19: #H; nnormalize in H; ndestruct;38 ## #i s; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H;39 ##[ nrewrite > H; nrewrite > (eq_true …); #H';40 ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]41 #H''; nrewrite > H''; /2/;42 ## nrewrite > (eq_false …); //; #H';43 ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]44 #H''; nrewrite > H''; /3/;45 ##]46 ####3,9,13,18,21,27: #x H; nnormalize in H; ndestruct;47 ## #t; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H;48 ##[ nrewrite > H; nrewrite > (eq_true …); #H';49 ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]50 #H''; nrewrite > H''; /2/;51 ## nrewrite > (eq_false …); //; #H';52 ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]53 #H''; nrewrite > H''; /3/;54 ##]55 ## ##5,6,7,8,11,14,15,16,17,23,24,25,26: #a b H; nnormalize in H; ndestruct;56 ## #f; nwhd in ⊢ (??%? → ?); nelim (eq_dec x Fzero); #H;57 ##[ nrewrite > H; nrewrite > (Feq_zero_true …); #H';58 ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]59 #H''; nrewrite > H''; /2/;60 ## nrewrite > (Feq_zero_false …); //; #H';61 ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##]62 #H''; nrewrite > H''; /3/;63 ##]64 ## #i s H; nwhd in H:(??%?);65 ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##]66 #H'; nrewrite > H'; /2/;67 ## #t H; nwhd in H:(??%?);68 ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##]69 #H'; nrewrite > H'; /2/;70 ##]71 ## #H; nelim H; #v t H'; nelim H';72 ##[ #i is s ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;73 ## ##2,4: //74 ## #i t ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;75 ## #f s ne; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;76 ## #i s; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;77 ## #t; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;78 ## #s; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;79 ##]80 ##] nqed.81 82 7 include "Plogic/russell_support.ma". 83 84 (* Nicer  we still have to deal with all of the cases, but only need to85 introduce the result value, so there's a single case for getting rid of86 all the Error goals. *)87 88 ndefinition bool_of_val_2 : ∀v:val. ∀ty:type. { r : res bool  ∀r'. r = OK ? r' → bool_of_val v ty (of_bool r') } ≝89 λv,ty. match v in val with90 [ Vint i ⇒ match ty with91 [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))92  Tpointer _ ⇒ Some ? (OK ? (¬eq i zero))93  _ ⇒ Some ? (Error ?)94 ]95  Vfloat f ⇒ match ty with96 [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero))97  _ ⇒ Some ? (Error ?)98 ]99  Vptr _ _ ⇒ match ty with100 [ Tint _ _ ⇒ Some ? (OK ? true)101  Tpointer _ ⇒ Some ? (OK ? true)102  _ ⇒ Some ? (Error ?)103 ]104  _ ⇒ Some ? (Error ?)105 ]. nwhd;106 ##[ ##3,5: #r; nlapply (eq_spec c0 zero); nelim (eq c0 zero);107 ##[ ##1,3: #e H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2,4: ndestruct; // ##] nrewrite > e; /3/;108 ## ##2,4: #ne H; nrewrite > (?:of_bool r=Vtrue); ##[ ##2,4: ndestruct; // ##] /3/;109 ##]110 ## ##13: #r; nelim (eq_dec c0 Fzero);111 ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); #H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2: ndestruct; // ##] /2/;112 ## #ne; nrewrite > (Feq_zero_false …); //; #H;113 nrewrite > (?:of_bool r=Vtrue); ##[ ##2: ndestruct; // ##] /3/;114 ##]115 ## ##21,23: #r H; nrewrite > (?:of_bool r = Vtrue); ##[ ##2,4: ndestruct; // ##] /2/116 ## ##*: #a b; ndestruct;117 ##] nqed.118 119 (* Same as before, except we have to write eject in because the type for the120 equality is left implied, so the coercion isn't used. *)121 122 nlemma bool_of_val_2_complete : ∀v,ty,r.123 bool_of_val v ty r →124 ∃b. r = of_bool b ∧ eject ?? (bool_of_val_2 v ty) = OK ? b.125 #v ty r H; nelim H; #v t H'; nelim H';126 ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;127 ## #b i i0 s; @ true; @; //128 ## #i t ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //;129 ## #b i t0; @ true; @; //130 ## #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //;131 ## #i s; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)132 ## #t; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*)133 ## #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //;134 ##]135 nqed.136 137 138 (* Nicer again (after the extra definitions). Just use sigma type rather than139 the subset, but take into account the error monad. The error cases all140 become trivial and we don't have to muck around to get the result. *)141 8 142 9 ndefinition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝ … … 175 42 [ Vint i ⇒ match ty with 176 43 [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero)) 177  Tpointer _ ⇒ Some ? (OK ? (¬eq i zero))44  Tpointer _ _ ⇒ Some ? (OK ? (¬eq i zero)) 178 45  _ ⇒ Some ? (Error ?) 179 46 ] … … 182 49  _ ⇒ Some ? (Error ?) 183 50 ] 184  Vptr _ _ ⇒ match ty with51  Vptr _ _ _ ⇒ match ty with 185 52 [ Tint _ _ ⇒ Some ? (OK ? true) 186  Tpointer _ ⇒ Some ? (OK ? true)53  Tpointer _ _ ⇒ Some ? (OK ? true) 187 54  _ ⇒ Some ? (Error ?) 188 55 ] … … 210 77 #v ty r H; nelim H; #v t H'; nelim H'; 211 78 ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; 212 ## # b i i0 s; @ true; @; //213 ## #i t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;214 ## # b it0; @ true; @; //79 ## #p b i i0 s; @ true; @; // 80 ## #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; 81 ## #p b i p0 t0; @ true; @; // 215 82 ## #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //; 216 83 ## #i s; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*) 217 ## # t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*)84 ## #p t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*) 218 85 ## #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //; 219 86 ##] … … 232 99 233 100 nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B. 234 (∀v:A. err_eq A P e v →∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True  OK v' ⇒ P' v'] ) →101 (∀v:A. ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True  OK v' ⇒ P' v'] ) → 235 102 match bind (sigma A P) B e f with [ Error ⇒ True  OK v' ⇒ P' v' ]. 236 #A B P P' e f; nelim e; //; 237 #v0; nelim v0; #v Hv IH; napply IH; //; nqed. 103 #A B P P' e f; nelim e; 104 ##[ #v0; nelim v0; #v Hv IH; napply IH; 105 ## #_; napply I; 106 ##] nqed. 238 107 239 108 nlemma bind2_OK: ∀A,B,C,P,e,f. … … 286 155 ##] nqed. 287 156 288 nlet rec is_neutral_cast (ty:type) : res (Σu:unit.neutral_for_cast ty) ≝289 match ty with290 [ Tint sz _ ⇒ match sz with [ I32 ⇒ Some ? (OK ? something)  _ ⇒ Some ? (Error ?) ]291  Tpointer _ ⇒ Some ? (OK ? something)292  Tarray _ _ ⇒ Some ? (OK ? something)293  Tfunction _ _ ⇒ Some ? (OK ? something)294  _ ⇒ Some ? (Error ?)295 ]. nwhd; //; nqed.296 157 (* 297 158 nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B  OK v ⇒ Error B ] = Error B. … … 299 160 *) 300 161 301 nlet rec exec_cast (v:val) (ty:type) (ty':type) : res (Σv':val. cast v ty ty' v') ≝ 162 nlet rec try_cast_null (m:mem) (i:int) (ty:type) (ty':type) : res (Σv':val. cast m (Vint i) ty ty' v') ≝ 163 match eq i zero with 164 [ true ⇒ 165 match ty with 166 [ Tpointer _ _ ⇒ 167 match ty' with 168 [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i)) 169  Tarray _ _ _ ⇒ Some ? (OK ? (Vint i)) 170  Tfunction _ _ ⇒ Some ? (OK ? (Vint i)) 171  _ ⇒ Some ? (Error ?) 172 ] 173  Tarray _ _ _ ⇒ 174 match ty' with 175 [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i)) 176  Tarray _ _ _ ⇒ Some ? (OK ? (Vint i)) 177  Tfunction _ _ ⇒ Some ? (OK ? (Vint i)) 178  _ ⇒ Some ? (Error ?) 179 ] 180  Tfunction _ _ ⇒ 181 match ty' with 182 [ Tpointer _ _ ⇒ Some ? (OK ? (Vint i)) 183  Tarray _ _ _ ⇒ Some ? (OK ? (Vint i)) 184  Tfunction _ _ ⇒ Some ? (OK ? (Vint i)) 185  _ ⇒ Some ? (Error ?) 186 ] 187  _ ⇒ Some ? (Error ?) 188 ] 189  false ⇒ Some ? (Error ?) 190 ]. nwhd; //; nlapply (eq_spec i zero); nrewrite > c0; #e; nrewrite > e; 191 napply cast_pp_z; //; nqed. 192 193 nlet rec exec_cast (m:mem) (v:val) (ty:type) (ty':type) : res (Σv':val. cast m v ty ty' v') ≝ 302 194 match v with 303 195 [ Vint i ⇒ … … 307 199 [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i))) 308 200  Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i)))) 309 (* no change in data repr *) 310  _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i)) 311 ] 312  _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i)) 201  Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for nonnull values? *) 202  Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for nonnull values? *) 203  Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for nonnull values? *) 204  _ ⇒ Some ? (Error ?) 205 ] 206  Tpointer _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for nonnull values? *) 207  Tarray _ _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for nonnull values? *) 208  Tfunction _ _ ⇒ Some (res val) (r ← try_cast_null m i ty ty';: OK val r) (* XXX: is this ok for nonnull values? *) 209  _ ⇒ Some ? (Error ?) 313 210 ] 314 211  Vfloat f ⇒ … … 322 219  _ ⇒ Some ? (Error ?) 323 220 ] 324  Vptr b ofs ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vptr b ofs)) 221  Vptr p b ofs ⇒ 222 Some ? ( 223 p ← match ty with [ Tpointer _ _ ⇒ OK ? something  Tarray _ _ _ ⇒ OK ? something  Tfunction _ _ ⇒ OK ? something  _ ⇒ Error ? ];: 224 s' ← match ty' with [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code  _ ⇒ Error ? ];: 225 if is_class_compat (blockclass m b) (ptr_spc_cls s') 226 then OK ? (Vptr (ptr_spc_cls s') b ofs) 227 else Error ?) 228 (* XXX: maybe should allow some Tint? *) 325 229  _ ⇒ Some ? (Error ?) 326 ]. ndestruct; /2/; 327 ##[ ##1,2,3: ncases c2; //; napply cast_nn_i; // 328 ## ##4,5,6: napply sig_bind_OK; #u;#_;#H; napply cast_nn_i; //; 329 ## napply sig_bind_OK; #u;#_;#H; napply sig_bind_OK; #u';#_;#H'; 330 napply cast_nn_p; // 230 ]. nwhd; //; 231 ##[ ##1,2,3,4,5,6: napply sig_bind_OK; #v'; #H; ndestruct; napply H; 232 ## napply bind_OK; #u1 tyok; 233 napply bind_OK; #s' es'; 234 ncut (type_pointable ty); 235 ##[ ncases ty in tyok ⊢ %; //; 236 ##[ #e; ## ##3,6: #a e; ## ##2,4,5: #a b e; ##] nwhd in e:(??%?); ndestruct; 237 ## ncut (type_space ty' s'); 238 ##[ ncases ty' in es' ⊢ %; ##[ #e; ## ##3,9: #a e; ## ##2,4,6,7,8: #a b e; ## #a b c e; ##] 239 nwhd in e:(??%?); ndestruct; //; 240 ## #Hty' Hty; 241 nwhd in match (is_class_compat ??) in ⊢ %; 242 ncases (class_compat_dec (blockclass m c1) (ptr_spc_cls s')); #Hcompat; 243 nwhd; /2/; 244 ##] 245 ##] 331 246 ##] nqed. 247 248 ndefinition load_value_of_type' ≝ 249 λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ 250 load_value_of_type ty m pcl loc ofs ] ]. 332 251 333 252 (* To make the evaluation of bare lvalue expressions invoke exec_lvalue with … … 342 261  Econst_float f ⇒ Some ? (OK ? (Vfloat f)) 343 262  Evar _ ⇒ Some ? ( 344 〈loc, ofs〉← exec_lvalue' ge en m e' ty;:345 opt_to_res ? (load_value_of_type ty m loc ofs))263 l ← exec_lvalue' ge en m e' ty;: 264 opt_to_res ? (load_value_of_type' ty m l)) 346 265  Ederef _ ⇒ Some ? ( 347 〈loc, ofs〉← exec_lvalue' ge en m e' ty;:348 opt_to_res ? (load_value_of_type ty m loc ofs))266 l ← exec_lvalue' ge en m e' ty;: 267 opt_to_res ? (load_value_of_type' ty m l)) 349 268  Efield _ _ ⇒ Some ? ( 350 〈loc, ofs〉← exec_lvalue' ge en m e' ty;:351 opt_to_res ? (load_value_of_type ty m loc ofs))269 l ← exec_lvalue' ge en m e' ty;: 270 opt_to_res ? (load_value_of_type' ty m l)) 352 271  Eaddrof a ⇒ Some ? ( 353 〈 loc, ofs〉 ← exec_lvalue ge en m a;:354 OK ? ( Vptr loc ofs))272 〈pl, ofs〉 ← exec_lvalue ge en m a;: 273 OK ? (match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ])) 355 274  Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty')))) 356 275  Eunop op a ⇒ Some ? ( … … 383 302  Ecast ty' a ⇒ Some ? ( 384 303 v ← exec_expr ge en m a;: 385 exec_cast v (typeof a) ty')304 exec_cast m v (typeof a) ty') 386 305 ] 387 306 ] 388 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr: block × int. eval_lvalue ge en m (Expr e' ty) (\fst r) (\snd r)) ≝307 and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:ptr_class × block × int. eval_lvalue ge en m (Expr e' ty) (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝ 389 308 match e' with 390 309 [ Evar id ⇒ 391 310 match (get … id en) with 392 [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈 l,zero〉) (* global *)393  Some l ⇒ Some ? (OK ? 〈l,zero〉)(* local *)311 [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈〈Universal (* XXX *),l〉,zero〉) (* global *) 312  Some bl ⇒ match bl with [ mk_pair bcl loc ⇒ Some ? (OK ? 〈〈blk_ptr_cls bcl,loc〉,zero〉) ] (* local *) 394 313 ] 395 314  Ederef a ⇒ Some ? ( 396 315 v ← exec_expr ge en m a;: 397 316 match v with 398 [ Vptr l ofs ⇒ OK ? 〈l,ofs〉317 [ Vptr pcl l ofs ⇒ OK ? 〈〈pcl,l〉,ofs〉 399 318  _ ⇒ Error ? 400 319 ]) … … 402 321 match (typeof a) with 403 322 [ Tstruct id fList ⇒ Some ? ( 404 〈 l,ofs〉 ← exec_lvalue ge en m a;:323 〈pl,ofs〉 ← exec_lvalue ge en m a;: 405 324 delta ← field_offset i fList;: 406 OK ? 〈 l,add ofs (repr delta)〉)325 OK ? 〈pl,add ofs (repr delta)〉) 407 326  Tunion id fList ⇒ Some ? ( 408 〈 l,ofs〉 ← exec_lvalue ge en m a;:409 OK ? 〈 l,ofs〉)327 〈pl,ofs〉 ← exec_lvalue ge en m a;: 328 OK ? 〈pl,ofs〉) 410 329  _ ⇒ Some ? (Error ?) 411 330 ] 412 331  _ ⇒ Some ? (Error ?) 413 332 ] 414 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr: block × int. eval_lvalue ge en m e (\fst r) (\snd r)) ≝333 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:ptr_class × block × int. eval_lvalue ge en m e (\fst (\fst r)) (\snd (\fst r)) (\snd r)) ≝ 415 334 match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ]. 416 nwhd; //; 417 ##[ napply sig_bind2_OK; nrewrite > c4; #loc ofs H; 418 napply opt_OK; #v ev; /2/; 419 ## napply sig_bind2_OK; nrewrite > c4; #loc ofs H; 420 napply opt_OK; #v ev; /2/; 421 ## napply sig_bind2_OK; #loc ofs H; 335 nwhd; 336 ##[ // 337 ## // 338 ## ##3,4: 339 napply sig_bind_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #pcl loc ofs H; 340 napply opt_OK; #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev); 341 ## napply sig_bind2_OK; #x; ncases x; #pcl loc ofs H; 422 342 nwhd; napply eval_Eaddrof; //; 423 ## napply sig_bind_OK; #v1 ev1Hv1;343 ## napply sig_bind_OK; #v1 Hv1; 424 344 napply opt_OK; #v ev; 425 345 napply (eval_Eunop … Hv1 ev); 426 ## napply sig_bind_OK; #v1 ev1Hv1;427 napply sig_bind_OK; #v2 ev2Hv2;346 ## napply sig_bind_OK; #v1 Hv1; 347 napply sig_bind_OK; #v2 Hv2; 428 348 napply opt_OK; #v ev; 429 349 napply (eval_Ebinop … Hv1 Hv2 ev); 430 ## napply sig_bind_OK; #v evHv;431 napply sig_bind_OK; #v' ev'Hv';350 ## napply sig_bind_OK; #v Hv; 351 napply sig_bind_OK; #v' Hv'; 432 352 napply (eval_Ecast … Hv Hv'); 433 ## napply sig_bind_OK; #vb evbHvb;353 ## napply sig_bind_OK; #vb Hvb; 434 354 napply sig_bind_OK; #b; 435 ncases b; # ebHb; napply reinject; #v ev Hv;355 ncases b; #Hb; napply reinject; #v ev Hv; 436 356 ##[ napply (eval_Econdition_true … Hvb ? Hv); napply (bool_of ??? Hb); 437 357 ## napply (eval_Econdition_false … Hvb ? Hv); napply (bool_of ??? Hb); 438 358 ##] 439 ## napply sig_bind_OK; #v1 ev1Hv1;440 napply sig_bind_OK; #b1; ncases b1; # eb1Hb1;441 ##[ napply sig_bind_OK; #v2 ev2Hv2;442 napply sig_bind_OK; #b2 eb2Hb2;359 ## napply sig_bind_OK; #v1 Hv1; 360 napply sig_bind_OK; #b1; ncases b1; #Hb1; 361 ##[ napply sig_bind_OK; #v2 Hv2; 362 napply sig_bind_OK; #b2 Hb2; 443 363 napply (eval_Eandbool_2 … Hv1 … Hv2); 444 364 ##[ napply (bool_of … Hb1); ## napply Hb2; ##] 445 365 ## napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1); 446 366 ##] 447 ## napply sig_bind_OK; #v1 ev1Hv1;448 napply sig_bind_OK; #b1; ncases b1; # eb1Hb1;367 ## napply sig_bind_OK; #v1 Hv1; 368 napply sig_bind_OK; #b1; ncases b1; #Hb1; 449 369 ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1); 450 ## napply sig_bind_OK; #v2 ev2Hv2;451 napply sig_bind_OK; #b2 eb2Hb2;370 ## napply sig_bind_OK; #v2 Hv2; 371 napply sig_bind_OK; #b2 Hb2; 452 372 napply (eval_Eorbool_2 … Hv1 … Hv2); 453 373 ##[ napply (bool_of … Hb1); ## napply Hb2; ##] 454 374 ##] 455 ## napply sig_bind2_OK; nrewrite > c5; #l ofs H; 456 napply opt_OK; #v ev; /2/; 375 ## // 376 ## napply sig_bind_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #pcl l ofs H; 377 napply opt_OK; #v ev; napply (eval_Elvalue … H ev); 378 ## // 379 ## // 457 380 ## napply opt_bind_OK; #l el; napply eval_Evar_global; /2/; 458 ## napply eval_Evar_local; /2/459 ## napply sig_bind_OK; #v; ncases v; //; # l ofs evHv; nwhd;381 ## napply eval_Evar_local; nrewrite < c6; /2/ 382 ## napply sig_bind_OK; #v; ncases v; //; #pcl l ofs Hv; nwhd; 460 383 napply eval_Ederef; // 461 ## napply sig_bind2_OK; #l ofs H; 384 ## ##19,20,21,22,23,24,25,26,27,28,29,30,31,32: // 385 ## napply sig_bind2_OK; #x; ncases x; #pcl l ofs H; 462 386 napply bind_OK; #delta Hdelta; 463 387 napply (eval_Efield_struct … H c5 Hdelta); 464 ## napply sig_bind2_OK; # l ofs H;388 ## napply sig_bind2_OK; #x; ncases x; #pcl l ofs H; 465 389 napply (eval_Efield_union … H c5); 390 ## // 466 391 ##] nqed. 467 392 … … 475 400 OK ? (cons val v vs)) 476 401 ]. nwhd; //; 477 napply sig_bind_OK; #v evHv;478 napply sig_bind_OK; #vs evsHvs;402 napply sig_bind_OK; #v Hv; 403 napply sig_bind_OK; #vs Hvs; 479 404 nnormalize; /2/; 480 405 nqed. … … 489 414  cons h vars ⇒ 490 415 match h with [ mk_pair id ty ⇒ 491 match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒492 match exec_alloc_variables (set … id b1en) m1 vars with416 match alloc m 0 (sizeof ty) UnspecifiedB with [ mk_pair m1 b1 ⇒ 417 match exec_alloc_variables (set … id 〈UnspecifiedB,b1〉 en) m1 vars with 493 418 [ sig_intro r p ⇒ r ] 494 419 ]]]. nwhd; //; 495 nelim (exec_alloc_variables (set ident ? block c3 c7en) c6 c1);420 nelim (exec_alloc_variables (set ident ? ? c3 〈UnspecifiedB,c7〉 en) c6 c1); 496 421 #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH; 497 422 napply (alloc_variables_cons … IH); /2/; … … 506 431 [ nil ⇒ Some ? (Error ?) 507 432  cons v1 vl ⇒ Some ? ( 508 b← opt_to_res ? (get … id e);:509 m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:433 〈bcl,b〉 ← opt_to_res ? (get … id e);: 434 m1 ← opt_to_res ? (store_value_of_type ty m (blk_ptr_cls bcl) b zero v1);: 510 435 err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *) 511 436 ] 512 437 ] ]. 513 438 nwhd; //; 514 napply opt_bind_OK; # b eb;439 napply opt_bind_OK; #x; ncases x; #bcl b eb; 515 440 napply opt_bind_OK; #m1 em1; 516 441 napply reinject; #m2 em2 Hm2; … … 549 474 ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2). 550 475 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. 476 ndefinition ms_eq_dec : ∀s1,s2:mem_space. (s1 = s2) + (s1 ≠ s2). 477 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. 551 478 552 479 nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝ … … 555 482  Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy  _ ⇒ dn ]  _ ⇒ dn ]  _ ⇒ dn ] 556 483  Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy  _ ⇒ dn ]  _ ⇒ dn ] 557  Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match assert_type_eq t t' with [ OK _ ⇒ dy  _ ⇒ dn ]  _ ⇒ dn ] 558  Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒ 559 match assert_type_eq t t' with [ OK _ ⇒ 560 match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy  inr _ ⇒ dn ]  _ ⇒ dn ]  _ ⇒ dn ] 484  Tpointer s t ⇒ match t2 with [ Tpointer s' t' ⇒ 485 match ms_eq_dec s s' with [ inl _ ⇒ 486 match assert_type_eq t t' with [ OK _ ⇒ dy  _ ⇒ dn ]  _ ⇒ dn ]  _ ⇒ dn ] 487  Tarray s t n ⇒ match t2 with [ Tarray s' t' n' ⇒ 488 match ms_eq_dec s s' with [ inl _ ⇒ 489 match assert_type_eq t t' with [ OK _ ⇒ 490 match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy  inr _ ⇒ dn ]  _ ⇒ dn ]  _ ⇒ dn ]  _ ⇒ dn ] 561 491  Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒ 562 492 match assert_type_eq t t' with [ OK _ ⇒ dy  _ ⇒ dn ]  _ ⇒ dn ]  _ ⇒ dn ] … … 652 582 ] 653 583 ]. nwhd; //; 654 napply sig_bind_OK; #ev eevHev;655 napply sig_bind_OK; #evt eevtHevt;584 napply sig_bind_OK; #ev Hev; 585 napply sig_bind_OK; #evt Hevt; 656 586 nnormalize; /2/; 657 587 nqed. 658 588 659 589 (* execution *) 590 591 ndefinition store_value_of_type' ≝ 592 λty,m,l,v. 593 match l with [ mk_pair pl ofs ⇒ 594 match pl with [ mk_pair pcl loc ⇒ 595 store_value_of_type ty m pcl loc ofs v ] ]. 660 596 661 597 nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝ … … 664 600 match s with 665 601 [ Sassign a1 a2 ⇒ Some ? ( 666 ! 〈loc, ofs〉← exec_lvalue ge e m a1;:602 ! l ← exec_lvalue ge e m a1;: 667 603 ! v2 ← exec_expr ge e m a2;: 668 ! m' ← store_value_of_type (typeof a1) m loc ofsv2;:604 ! m' ← store_value_of_type' (typeof a1) m l v2;: 669 605 ret ? 〈E0, State f Sskip k e m'〉) 670 606  Scall lhs a al ⇒ Some ? ( … … 802 738 ] 803 739  Some r' ⇒ 804 match r' with [ mk_pair l ocofsty ⇒805 match locofs with [ mk_pair loc ofs ⇒Some ? (806 ! m' ← store_value_of_type ty m loc ofsres;:740 match r' with [ mk_pair l ty ⇒ 741 Some ? ( 742 ! m' ← store_value_of_type' ty m l res;: 807 743 ret ? 〈E0, (State f Sskip k' e m')〉) 808 ]809 744 ] 810 745 ] … … 824 759 ## napply step_skip_break_switch; @; //; 825 760 ## nrewrite > c11; napply step_skip_call; //; napply c12; 826 ## napply sig_bindIO 2_OK; #loc ofs Hlval;761 ## napply sig_bindIO_OK; #x; ncases x; #y; ncases y; #pcl loc ofs Hlval; 827 762 napply sig_bindIO_OK; #v2 Hv2; 828 763 napply opt_bindIO_OK; #m' em'; … … 835 770 ##[ napply (step_call_none … Hvf Hvargs efd ety); 836 771 ## #lhs'; 837 napply sig_bindIO_OK; # locofs; ncases locofs; #loc ofs Hlocofs;772 napply sig_bindIO_OK; #x; ncases x; #y; ncases y; #pcl loc ofs Hlocofs; 838 773 nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety); 839 774 ##] … … 879 814 napply sig_bindIO_OK; #res Hres; 880 815 nwhd; napply step_external_function; @; ##[ napply Hevs; ## napply Hres; ##] 881 ## napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; //; 816 ## ncases c11; #x; ncases x; #pcl b ofs; 817 napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //; 882 818 ##] 883 819 nqed. … … 905 841 ## ##1: @2; @; *; #r H; ninversion H; #i m e; ndestruct; 906 842 ## #f; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 907 ## # b of; @2; @; *; #r H; ninversion H; #i m e; ndestruct;843 ## #pcl b of; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 908 844 ##] 909 845 ## #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
Note: See TracChangeset
for help on using the changeset viewer.