Changeset 797 for src/Clight/Cexec.ma
 Timestamp:
 May 13, 2011, 1:10:23 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Cexec.ma
r744 r797 8 8 (* 9 9 include "Plogic/russell_support.ma". 10 *) 10 11 11 definition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝ 12 12 λA,P,a.match a with [ None ⇒ False  Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True  OK z ⇒ P z ]]. … … 26 26 27 27 definition err_eject : ∀A.∀P: A → Prop. res (Sig A P) → res A ≝ 28 λA,P,a.match a with [ Error ⇒ Error ? OK b ⇒28 λA,P,a.match a with [ Error m ⇒ Error ? m  OK b ⇒ 29 29 match b with [ dp w p ⇒ OK ? w] ]. 30 30 … … 39 39 coercion sig_eject : ∀A.∀P:A → Prop.∀c:Sig A P.A ≝ sig_eject 40 40 on _c:Sig ? ? to ?. 41 41 *) 42 42 definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝ 43 λA,P,a. match a with [ Error ⇒ True  OK v ⇒ P v ]. 43 λA,P,a. match a with [ Error _ ⇒ True  OK v ⇒ P v ]. 44 45 axiom TypeMismatch : String. 46 axiom ValueIsNotABoolean : String. 44 47 45 48 definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝ … … 47 50 [ Vint i ⇒ match ty with 48 51 [ Tint _ _ ⇒ OK ? (¬eq i zero) 49  _ ⇒ Error ? 52  _ ⇒ Error ? (msg TypeMismatch) 50 53 ] 51 54  Vfloat f ⇒ match ty with 52 55 [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero) 53  _ ⇒ Error ? 56  _ ⇒ Error ? (msg TypeMismatch) 54 57 ] 55 58  Vptr _ _ _ _ ⇒ match ty with 56 59 [ Tpointer _ _ ⇒ OK ? true 57  _ ⇒ Error ? 60  _ ⇒ Error ? (msg TypeMismatch) 58 61 ] 59 62  Vnull _ ⇒ match ty with 60 63 [ Tpointer _ _ ⇒ OK ? false 61  _ ⇒ Error ? 62 ] 63  _ ⇒ Error ? 64  _ ⇒ Error ? (msg TypeMismatch) 65 ] 66  _ ⇒ Error ? (msg ValueIsNotABoolean) 64 67 ]. 65 68 … … 78 81 79 82 lemma bind_OK: ∀A,B,P,e,f. 80 (∀v. e = OK A v → match f v with [ Error ⇒ True  OK v' ⇒ P v' ]) →81 match bind A B e f with [ Error ⇒ True  OK v ⇒ P v ].83 (∀v. e = OK A v → match f v with [ Error _ ⇒ True  OK v' ⇒ P v' ]) → 84 match bind A B e f with [ Error _ ⇒ True  OK v ⇒ P v ]. 82 85 #A #B #P #e #f elim e; /2/; qed. 83 86 84 87 lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B. 85 (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error ⇒ True  OK v' ⇒ P' v'] ) →86 match bind (Sig A P) B e f with [ Error ⇒ True  OK v' ⇒ P' v' ].88 (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error _ ⇒ True  OK v' ⇒ P' v'] ) → 89 match bind (Sig A P) B e f with [ Error _ ⇒ True  OK v' ⇒ P' v' ]. 87 90 #A #B #P #P' #e #f elim e; 88 91 [ #v0 elim v0; #v #Hv #IH @IH 89  # _ @I92  #m #_ @I 90 93 ] qed. 91 94 92 95 lemma bind2_OK: ∀A,B,C,P,e,f. 93 (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True  OK v' ⇒ P v' ]) →94 match bind2 A B C e f with [ Error ⇒ True  OK v ⇒ P v ].96 (∀v1,v2. e = OK ? 〈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 ]. 95 98 #A #B #C #P #e #f elim e; //; #v cases v; /2/; qed. 96 99 97 lemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (Sig (A×B) P). ∀f:A → B → res C. 98 (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True  OK v' ⇒ P' v'] ) → 99 match bind2 A B C e f with [ Error ⇒ True  OK v' ⇒ P' v' ]. 100 #A #B #C #P #P' #e #f elim e; //; 101 #v0 elim v0; #v elim v; #v1 #v2 #Hv #IH @IH //; qed. 102 103 lemma opt_bind_OK: ∀A,B,P,e,f. 104 (∀v. e = Some A v → match f v with [ Error ⇒ True  OK v' ⇒ P v' ]) → 105 match bind A B (opt_to_res A e) f with [ Error ⇒ True  OK v ⇒ P v ]. 106 #A #B #P #e #f elim e; normalize; /2/; qed. 107 (* 108 lemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B  P e}. ∀Q:A→B→res C. ∀R:C→Prop. 109 (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v  Error ⇒ True]) → 110 match match eject ?? e with [ pair a b ⇒ Q a b ] with [ OK v ⇒ R v  Error ⇒ True ]. 111 #A #B #C #P #e #Q #R cases e; #e' cases e'; normalize; 112 [ #H @(False_ind … H) 113  #e'' cases e''; #a #b #Pab #H normalize; /2/; 114 ] qed. 115 *) 116 (* 117 nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B  OK v ⇒ Error B ] = Error B. 118 #A #B #e cases e; //; qed. 119 *) 100 lemma opt_bind_OK: ∀A,B,P,m,e,f. 101 (∀v. e = Some A v → match f v with [ Error _ ⇒ True  OK v' ⇒ P v' ]) → 102 match bind A B (opt_to_res A m e) f with [ Error _ ⇒ True  OK v ⇒ P v ]. 103 #A #B #P #m #e #f elim e; normalize; /2/; qed. 104 105 106 axiom BadCast : String. (* TODO: refine into more precise errors? *) 120 107 121 108 definition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val ≝ … … 129 116  Tarray r _ _ ⇒ OK ? (Vnull r) 130 117  Tfunction _ _ ⇒ OK ? (Vnull Code) 131  _ ⇒ Error ? 132 ] 133  _ ⇒ Error ? 134 ] 135  false ⇒ Error ? 118  _ ⇒ Error ? (msg BadCast) 119 ] 120  _ ⇒ Error ? (msg BadCast) 121 ] 122  false ⇒ Error ? (msg BadCast) 136 123 ]. 137 124 … … 148 135  Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r 149 136  Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r 150  _ ⇒ Error ? 137  _ ⇒ Error ? (msg BadCast) 151 138 ] 152 139  Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r 153 140  Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r 154 141  Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r 155  _ ⇒ Error ? 142  _ ⇒ Error ? (msg TypeMismatch) 156 143 ] 157 144  Vfloat f ⇒ … … 161 148 [ Tint sz' si' ⇒ OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f))) 162 149  Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f)) 163  _ ⇒ Error ? 164 ] 165  _ ⇒ Error ? 150  _ ⇒ Error ? (msg BadCast) 151 ] 152  _ ⇒ Error ? (msg TypeMismatch) 166 153 ] 167 154  Vptr r b _ ofs ⇒ 168 do s ← match ty with [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code  _ ⇒ Error ? ];169 do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it  inr _ ⇒ Error ? ];155 do s ← match ty with [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code  _ ⇒ Error ? (msg TypeMismatch) ]; 156 do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it  inr _ ⇒ Error ? (msg BadCast) ]; 170 157 do s' ← match ty' with 171 158 [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code 172  _ ⇒ Error ? ];159  _ ⇒ Error ? (msg BadCast)]; 173 160 match pointer_compat_dec b s' with 174 161 [ inl p' ⇒ OK ? (Vptr s' b p' ofs) 175  inr _ ⇒ Error ? 162  inr _ ⇒ Error ? (msg BadCast) 176 163 ] 177 164  Vnull r ⇒ 178 do s ← match ty with [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code  _ ⇒ Error ? ];179 do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it  inr _ ⇒ Error ? ];165 do s ← match ty with [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code  _ ⇒ Error ? (msg TypeMismatch) ]; 166 do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it  inr _ ⇒ Error ? (msg BadCast) ]; 180 167 do s' ← match ty' with 181 168 [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code 182  _ ⇒ Error ? ];169  _ ⇒ Error ? (msg BadCast) ]; 183 170 OK ? (Vnull s') 184  _ ⇒ Error ? 171  _ ⇒ Error ? (msg BadCast) 185 172 ]. 186 173 … … 191 178 a structurally smaller value, we break out the surrounding Expr constructor 192 179 and use exec_lvalue'. *) 180 181 axiom BadlyTypedTerm : String. 182 axiom UnknownIdentifier : String. 183 axiom BadLvalueTerm : String. 184 axiom FailedLoad : String. 185 axiom FailedOp : String. 193 186 194 187 let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝ … … 200 193  Evar _ ⇒ 201 194 do 〈l,tr〉 ← exec_lvalue' ge en m e' ty; 202 do v ← opt_to_res ? ( load_value_of_type' ty m l);195 do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l); 203 196 OK ? 〈v,tr〉 204 197  Ederef _ ⇒ 205 198 do 〈l,tr〉 ← exec_lvalue' ge en m e' ty; 206 do v ← opt_to_res ? ( load_value_of_type' ty m l);199 do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l); 207 200 OK ? 〈v,tr〉 208 201  Efield _ _ ⇒ 209 202 do 〈l,tr〉 ← exec_lvalue' ge en m e' ty; 210 do v ← opt_to_res ? ( load_value_of_type' ty m l);203 do v ← opt_to_res ? (msg FailedLoad) (load_value_of_type' ty m l); 211 204 OK ? 〈v,tr〉 212 205  Eaddrof a ⇒ … … 217 210 match pointer_compat_dec loc r with 218 211 [ inl pc ⇒ OK ? 〈Vptr r loc pc ofs, tr〉 219  inr _ ⇒ Error ? 212  inr _ ⇒ Error ? (msg TypeMismatch) 220 213 ] 221 214 ] 222  _ ⇒ Error ? 215  _ ⇒ Error ? (msg BadlyTypedTerm) 223 216 ] 224 217  Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉 225 218  Eunop op a ⇒ 226 219 do 〈v1,tr〉 ← exec_expr ge en m a; 227 do v ← opt_to_res ? ( sem_unary_operation op v1 (typeof a));220 do v ← opt_to_res ? (msg FailedOp) (sem_unary_operation op v1 (typeof a)); 228 221 OK ? 〈v,tr〉 229 222  Ebinop op a1 a2 ⇒ 230 223 do 〈v1,tr1〉 ← exec_expr ge en m a1; 231 224 do 〈v2,tr2〉 ← exec_expr ge en m a2; 232 do v ← opt_to_res ? ( sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);225 do v ← opt_to_res ? (msg FailedOp) (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m); 233 226 OK ? 〈v,tr1⧺tr2〉 234 227  Econdition a1 a2 a3 ⇒ … … 268 261 [ Evar id ⇒ 269 262 match (get … id en) with 270 [ None ⇒ do l ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *)263 [ None ⇒ do l ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (find_symbol ? ? ge id); OK ? 〈〈l,zero_offset〉,E0〉 (* global *) 271 264  Some loc ⇒ OK ? 〈〈loc,zero_offset〉,E0〉 (* local *) 272 265 ] … … 275 268 match v with 276 269 [ Vptr _ l _ ofs ⇒ OK ? 〈〈l,ofs〉,tr〉 277  _ ⇒ Error ? 270  _ ⇒ Error ? (msg TypeMismatch) 278 271 ] 279 272  Efield a i ⇒ … … 286 279 do 〈lofs,tr〉 ← exec_lvalue ge en m a; 287 280 OK ? 〈lofs,tr〉 288  _ ⇒ Error ? 289 ] 290  _ ⇒ Error ? 281  _ ⇒ Error ? (msg BadlyTypedTerm) 282 ] 283  _ ⇒ Error ? (msg BadLvalueTerm) 291 284 ] 292 285 and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (block × offset × trace) ≝ … … 324 317 ]]]. 325 318 319 axiom WrongNumberOfParameters : String. 320 axiom FailedStore : String. 321 326 322 (* TODO: can we establish that length params = length vs in advance? *) 327 323 let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝ 328 324 match params with 329 [ nil ⇒ match vs with [ nil ⇒ OK ? m  cons _ _ ⇒ Error ? ]325 [ nil ⇒ match vs with [ nil ⇒ OK ? m  cons _ _ ⇒ Error ? (msg WrongNumberOfParameters) ] 330 326  cons idty params' ⇒ match idty with [ pair id ty ⇒ 331 327 match vs with 332 [ nil ⇒ Error ? 328 [ nil ⇒ Error ? (msg WrongNumberOfParameters) 333 329  cons v1 vl ⇒ 334 do b ← opt_to_res ? (get … id e);335 do m1 ← opt_to_res ? (store_value_of_type ty m b zero_offset v1);330 do b ← opt_to_res ? [MSG UnknownIdentifier; CTX ? id] (get … id e); 331 do m1 ← opt_to_res ? [MSG FailedStore; CTX ? id] (store_value_of_type ty m b zero_offset v1); 336 332 exec_bind_parameters e m1 params' vl 337 333 ] … … 424 420 425 421 definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝ 426 λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p  inr _ ⇒ Error ? ].422 λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p  inr _ ⇒ Error ? (msg TypeMismatch)]. 427 423 428 424 let rec is_is_call_cont (k:cont) : Sum (is_call_cont k) (Not (is_call_cont k)) ≝ … … 451 447 store_value_of_type ty m loc ofs v ]. 452 448 449 axiom NonsenseState : String. 450 axiom ReturnMismatch : String. 451 axiom UnknownLabel : String. 452 axiom BadFunctionValue : String. 453 453 454 let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝ 454 455 match st with … … 458 459 ! 〈l,tr1〉 ← exec_lvalue ge e m a1; 459 460 ! 〈v2,tr2〉 ← exec_expr ge e m a2; 460 ! m' ← store_value_of_type' (typeof a1) m l v2;461 ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' (typeof a1) m l v2); 461 462 ret ? 〈tr1⧺tr2, State f Sskip k e m'〉 462 463  Scall lhs a al ⇒ 463 464 ! 〈vf,tr2〉 ← exec_expr ge e m a; 464 465 ! 〈vargs,tr3〉 ← exec_exprlist ge e m al; 465 ! fd ← find_funct ? ? ge vf;466 ! fd ← opt_to_io … (msg BadFunctionValue) (find_funct ? ? ge vf); 466 467 ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (fun_typeof a)); 467 468 (* requires associativity of IOMonad, so rearrange it below … … 487 488 match fn_return f with 488 489 [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉 489  _ ⇒ Wrong ??? 490  _ ⇒ Wrong ??? (msg NonsenseState) 490 491 ] 491 492  Kcall _ _ _ _ ⇒ 492 493 match fn_return f with 493 494 [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉 494  _ ⇒ Wrong ??? 495  _ ⇒ Wrong ??? (msg NonsenseState) 495 496 ] 496 497  Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉 … … 505 506  Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉 506 507  Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉 507  _ ⇒ Wrong ??? 508  _ ⇒ Wrong ??? (msg NonsenseState) 508 509 ] 509 510  Scontinue ⇒ … … 520 521  Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉 521 522  Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉 522  _ ⇒ Wrong ??? 523  _ ⇒ Wrong ??? (msg NonsenseState) 523 524 ] 524 525  Sbreak ⇒ … … 529 530  Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉 530 531  Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉 531  _ ⇒ Wrong ??? 532  _ ⇒ Wrong ??? (msg NonsenseState) 532 533 ] 533 534  Sifthenelse a s1 s2 ⇒ … … 553 554 [ None ⇒ match fn_return f with 554 555 [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉 555  _ ⇒ Wrong ??? 556  _ ⇒ Wrong ??? (msg ReturnMismatch) 556 557 ] 557 558  Some a ⇒ 558 559 match type_eq_dec (fn_return f) Tvoid with 559 [ inl _ ⇒ Wrong ??? 560 [ inl _ ⇒ Wrong ??? (msg ReturnMismatch) 560 561  inr _ ⇒ 561 562 ! 〈v,tr〉 ← exec_expr ge e m a; … … 566 567 ! 〈v,tr〉 ← exec_expr ge e m a; 567 568 match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉 568  _ ⇒ Wrong ??? ]569  _ ⇒ Wrong ??? (msg TypeMismatch)] 569 570  Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉 570 571  Sgoto lbl ⇒ 571 572 match find_label lbl (fn_body f) (call_cont k) with 572 573 [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ] 573  None ⇒ Wrong ??? 574  None ⇒ Wrong ??? [MSG UnknownLabel; CTX ? lbl] 574 575 ] 575 576  Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉 … … 594 595  Some r' ⇒ 595 596 match r' with [ pair l ty ⇒ 596 597 ! m' ← store_value_of_type' ty m l res; 597 ! m' ← opt_to_io … (msg FailedStore) (store_value_of_type' ty m l res); 598 598 ret ? 〈E0, (State f Sskip k' e m')〉 599 599 ] 600 600 ] 601  _ ⇒ Wrong ??? 601  _ ⇒ Wrong ??? (msg NonsenseState) 602 602 ] 603 603 ]. 604 605 axiom MainMissing : String. 604 606 605 607 let rec make_initial_state (p:clight_program) : res (genv × state) ≝ 606 608 do ge ← globalenv Genv ?? p; 607 609 do m0 ← init_mem Genv ?? p; 608 do b ← opt_to_res ? ( find_symbol ? ? ge (prog_main ?? p));609 do f ← opt_to_res ? ( find_funct_ptr ? ? ge b);610 do b ← opt_to_res ? (msg MainMissing) (find_symbol ? ? ge (prog_main ?? p)); 611 do f ← opt_to_res ? (msg MainMissing) (find_funct_ptr ? ? ge b); 610 612 OK ? 〈ge,Callstate f (nil ?) Kstop m0〉. 611 613
Note: See TracChangeset
for help on using the changeset viewer.