Changeset 2176 for src/Clight/Csem.ma
- Timestamp:
- Jul 12, 2012, 1:28:28 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/Csem.ma
r2032 r2176 39 39 | is_false_int: ∀sz,sg. 40 40 is_false (Vint sz (zero ?)) (Tint sz sg) 41 | is_false_pointer: ∀ r,r',t.42 is_false (Vnull r) (Tpointer r't)41 | is_false_pointer: ∀t. 42 is_false Vnull (Tpointer t) 43 43 | is_false_float: ∀sz. 44 44 is_false (Vfloat Fzero) (Tfloat sz). … … 48 48 n ≠ (zero ?) → 49 49 is_true (Vint sz n) (Tint sz sg) 50 | is_true_pointer_pointer: ∀ptr, s,t.51 is_true (Vptr ptr) (Tpointer st)50 | is_true_pointer_pointer: ∀ptr,t. 51 is_true (Vptr ptr) (Tpointer t) 52 52 | is_true_float: ∀f,sz. 53 53 f ≠ Fzero → … … 102 102 | _ ⇒ None ? 103 103 ] 104 | Tpointer _ _⇒104 | Tpointer _ ⇒ 105 105 match v with 106 106 [ Vptr _ ⇒ Some ? Vfalse 107 | Vnull _⇒ Some ? Vtrue107 | Vnull ⇒ Some ? Vtrue 108 108 | _ ⇒ None ? 109 109 ] … … 131 131 | _ ⇒ None ? ] 132 132 | _ ⇒ None ? ] 133 | add_case_pi _ _ty _ _ ⇒ (**r pointer plus integer *)133 | add_case_pi _ ty _ _ ⇒ (**r pointer plus integer *) 134 134 match v1 with 135 135 [ Vptr ptr1 ⇒ match v2 with 136 136 [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) n2)) 137 137 | _ ⇒ None ? ] 138 | Vnull r⇒ match v2 with139 [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r)else None ?140 | _ ⇒ None ? ] 141 | _ ⇒ None ? ] 142 | add_case_ip _ _ _ _ty ⇒ (**r integer plus pointer *)138 | Vnull ⇒ match v2 with 139 [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ? 140 | _ ⇒ None ? ] 141 | _ ⇒ None ? ] 142 | add_case_ip _ _ _ ty ⇒ (**r integer plus pointer *) 143 143 match v1 with 144 144 [ Vint sz1 n1 ⇒ match v2 with 145 145 [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) n1)) 146 | Vnull r ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r)else None ?146 | Vnull ⇒ if eq_bv ? n1 (zero ?) then Some ? Vnull else None ? 147 147 | _ ⇒ None ? ] 148 148 | _ ⇒ None ? ] … … 165 165 | _ ⇒ None ? ] 166 166 | _ ⇒ None ? ] 167 | sub_case_pi _ _ty _ _ ⇒ (**r pointer minus integer *)167 | sub_case_pi _ ty _ _ ⇒ (**r pointer minus integer *) 168 168 match v1 with 169 169 [ Vptr ptr1 ⇒ match v2 with 170 170 [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) n2)) 171 171 | _ ⇒ None ? ] 172 | Vnull r⇒ match v2 with173 [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r)else None ?174 | _ ⇒ None ? ] 175 | _ ⇒ None ? ] 176 | sub_case_pp _ _ _ ty __ ⇒ (**r pointer minus pointer *)172 | Vnull ⇒ match v2 with 173 [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? Vnull else None ? 174 | _ ⇒ None ? ] 175 | _ ⇒ None ? ] 176 | sub_case_pp _ _ ty _ ⇒ (**r pointer minus pointer *) 177 177 match v1 with 178 178 [ Vptr ptr1 ⇒ match v2 with … … 186 186 else None ? 187 187 | _ ⇒ None ? ] 188 | Vnull r ⇒ match v2 with [ Vnull r'⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]188 | Vnull ⇒ match v2 with [ Vnull ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ] 189 189 | _ ⇒ None ? ] 190 190 | sub_default _ _ ⇒ None ? … … 343 343 | _ ⇒ None ? 344 344 ] 345 | cmp_case_pp _ _ _⇒345 | cmp_case_pp _ _ ⇒ 346 346 match v1 with 347 347 [ Vptr ptr1 ⇒ … … 354 354 else sem_cmp_mismatch c 355 355 else None ? 356 | Vnull r2⇒ sem_cmp_mismatch c357 | _ ⇒ None ? ] 358 | Vnull r1⇒356 | Vnull ⇒ sem_cmp_mismatch c 357 | _ ⇒ None ? ] 358 | Vnull ⇒ 359 359 match v2 with 360 360 [ Vptr ptr2 ⇒ sem_cmp_mismatch c 361 | Vnull r2⇒ sem_cmp_match c361 | Vnull ⇒ sem_cmp_match c 362 362 | _ ⇒ None ? 363 363 ] … … 430 430 ]. 431 431 432 (* Only for full 8051 memory spaces 432 433 inductive type_region : type → region → Prop ≝ 433 434 | type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s 434 435 | type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s 435 (* XXXIs the following necessary? *)436 (* Is the following necessary? *) 436 437 | type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code. 438 *) 439 440 inductive type_ptr : type → Prop ≝ 441 | type_pointer : ∀t. type_ptr (Tpointer t) 442 | type_array : ∀t,n. type_ptr (Tarray t n) 443 | type_fun : ∀tys,ty. type_ptr (Tfunction tys ty). 437 444 438 445 inductive cast : mem → val → type → type → val → Prop ≝ … … 449 456 cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) 450 457 (Vfloat (cast_float_float sz2 f)) 451 | cast_pp: ∀m,ty,ty',ptr ,r'.452 type_region ty (ptype ptr) →458 | cast_pp: ∀m,ty,ty',ptr. 459 (* type_region ty (ptype ptr) → 453 460 type_region ty' r' → 454 461 ∀pc':pointer_compat (pblock ptr) r'. 455 cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr))) 456 | cast_ip_z: ∀m,sz,sg,ty',r. 457 type_region ty' r → 458 cast m (Vint sz (zero ?)) (Tint sz sg) ty' (Vnull r) 459 | cast_pp_z: ∀m,ty,ty',r,r'. 460 type_region ty r → 461 type_region ty' r' → 462 cast m (Vnull r) ty ty' (Vnull r'). 462 cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr)))*) 463 type_ptr ty → 464 type_ptr ty' → 465 cast m (Vptr ptr) ty ty' (Vptr ptr) 466 | cast_ip_z: ∀m,sz,sg,ty'. 467 (* type_region ty' r →*) 468 type_ptr ty' → 469 cast m (Vint sz (zero ?)) (Tint sz sg) ty' Vnull 470 | cast_pp_z: ∀m,ty,ty'. 471 (* type_region ty r → 472 type_region ty' r' →*) 473 type_ptr ty → 474 type_ptr ty' → 475 cast m Vnull ty ty' Vnull. 463 476 464 477 (* * * Operational semantics *) … … 486 499 let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝ 487 500 match access_mode ty with 488 [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer Any b ?ofs))489 | By_reference r ⇒490 match pointer_compat_dec b r with501 [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer b ofs)) 502 | By_reference ⇒ Some ? (Vptr (mk_pointer b ofs)) 503 (* match pointer_compat_dec b r with 491 504 [ inl p ⇒ Some ? (Vptr (mk_pointer r b p ofs)) 492 505 | inr _ ⇒ None ? 493 ] 506 ]*) 494 507 | By_nothing _ ⇒ None ? 495 508 ]. 496 cases b //497 qed. 509 (*cases b // 510 qed.*) 498 511 499 512 (* * Symmetrically, [store_value_of_type ty m b ofs v] returns the … … 504 517 let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝ 505 518 match access_mode ty_dest with 506 [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer Any loc ?ofs)) v507 | By_reference _⇒ None ?519 [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer loc ofs)) v 520 | By_reference ⇒ None ? 508 521 | By_nothing _ ⇒ None ? 509 522 ]. 510 cases loc //511 qed. 523 (*cases loc // 524 qed.*) 512 525 513 526 (* * Allocation of function-local variables. … … 526 539 | alloc_variables_cons: 527 540 ∀e,m,id,ty,vars,m1,b1,m2,e2. 528 alloc m 0 (sizeof ty) Any= 〈m1, b1〉 →541 alloc m 0 (sizeof ty) XData = 〈m1, b1〉 → 529 542 alloc_variables (add … e id (pi1 … b1)) m1 vars e2 m2 → 530 543 alloc_variables e m (〈id, ty〉 :: vars) e2 m2. … … 598 611 load_value_of_type ty m loc ofs = Some ? v → 599 612 eval_expr ge e m (Expr a ty) v tr 600 | eval_Eaddrof: ∀a,ty, r,loc,ofs,tr.613 | eval_Eaddrof: ∀a,ty,loc,ofs,tr. 601 614 eval_lvalue ge e m a loc ofs tr → 602 ∀pc:pointer_compat loc r. 603 eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr (mk_pointer r loc pc ofs)) tr615 (* ∀pc:pointer_compat loc r.*) 616 eval_expr ge e m (Expr (Eaddrof a) (Tpointer ty)) (Vptr (mk_pointer loc ofs)) tr 604 617 | eval_Esizeof: ∀ty',sz,sg. 605 618 eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0 … … 664 677 find_symbol … ge id = Some ? l → 665 678 eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 666 | eval_Ederef: ∀a,ty, r,l,p,ofs,tr.667 eval_expr ge e m a (Vptr (mk_pointer r l pofs)) tr →679 | eval_Ederef: ∀a,ty,l,ofs,tr. 680 eval_expr ge e m a (Vptr (mk_pointer l ofs)) tr → 668 681 eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr 669 682 (* Aside: note that each block of memory is entirely contained within one … … 685 698 (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) 686 699 (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) 687 (ead:∀a,ty, r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H))700 (ead:∀a,ty,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty loc ofs tr H)) 688 701 (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg)) 689 702 (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) … … 702 715 | eval_Econst_float f ty ⇒ ecF f ty 703 716 | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 704 | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H717 | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H 705 718 | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg 706 719 | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1) … … 722 735 (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H)) 723 736 (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2)) 724 (lde:∀a,ty, r,l,pc,ofs,tr,H. P ???? (eval_Ederef ge e m a ty r l pcofs tr H))737 (lde:∀a,ty,l,ofs,tr,H. P ???? (eval_Ederef ge e m a ty l ofs tr H)) 725 738 (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. P a l ofs tr H1 → P ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) 726 739 (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. P a l ofs tr H1 → P ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) … … 729 742 [ eval_Evar_local id l ty H ⇒ lvl id l ty H 730 743 | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 731 | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pcofs tr H744 | eval_Ederef a ty l ofs tr H ⇒ lde a ty l ofs tr H 732 745 | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1) 733 746 | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1) … … 793 806 (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) 794 807 (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) 795 (ead:∀a,ty, r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))808 (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H)) 796 809 (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg)) 797 810 (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) … … 807 820 (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) 808 821 (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) 809 (lde:∀a,ty, r,l,pc,ofs,tr,H. P a (Vptr (mk_pointer r l pc ofs)) tr H → Q ???? (eval_Ederef ge e m a ty r l pcofs tr H))822 (lde:∀a,ty,l,ofs,tr,H. P a (Vptr (mk_pointer l ofs)) tr H → Q ???? (eval_Ederef ge e m a ty l ofs tr H)) 810 823 (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) 811 824 (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) … … 816 829 | eval_Econst_float f ty ⇒ ecF f ty 817 830 | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1) 818 | eval_Eaddrof a ty r loc ofs tr H pc ⇒ ead a ty r loc pc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)831 | eval_Eaddrof a ty loc ofs tr H ⇒ ead a ty loc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H) 819 832 | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg 820 833 | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1) … … 835 848 (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) 836 849 (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) 837 (ead:∀a,ty, r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))850 (ead:∀a,ty,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty loc ofs tr H)) 838 851 (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg)) 839 852 (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2)) … … 849 862 (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) 850 863 (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) 851 (lde:∀a,ty, r,l,pc,ofs,tr,H. P a (Vptr (mk_pointer r l pc ofs)) tr H → Q ???? (eval_Ederef ge e m a ty r l pcofs tr H))864 (lde:∀a,ty,l,ofs,tr,H. P a (Vptr (mk_pointer l ofs)) tr H → Q ???? (eval_Ederef ge e m a ty l ofs tr H)) 852 865 (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3)) 853 866 (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2)) … … 856 869 [ eval_Evar_local id l ty H ⇒ lvl id l ty H 857 870 | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 858 | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr (mk_pointer r l pcofs)) tr H)871 | eval_Ederef a ty l ofs tr H ⇒ lde a ty l ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr (mk_pointer l ofs)) tr H) 859 872 | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1) 860 873 | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1) … … 1014 1027 | Tint a b ⇒ Tint a b 1015 1028 | Tfloat a ⇒ Tfloat a 1016 | Tpointer _ty ⇒ ty1017 | Tarray a b c ⇒ Tarray a b c1029 | Tpointer ty ⇒ ty 1030 | Tarray a b ⇒ Tarray a b 1018 1031 | Tfunction a b ⇒ Tfunction a b 1019 1032 | Tstruct a b ⇒ Tstruct a b 1020 1033 | Tunion a b ⇒ Tunion a b 1021 | Tcomp_ptr a b ⇒ Tcomp_ptr a b1034 | Tcomp_ptr a ⇒ Tcomp_ptr a 1022 1035 ]. 1023 1036
Note: See TracChangeset
for help on using the changeset viewer.