Changeset 500 for Deliverables/D3.1/Csemantics/Csem.ma
 Timestamp:
 Feb 11, 2011, 4:45:38 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Csem.ma
r499 r500 48 48 n ≠ zero → 49 49 is_true (Vint n) (Tint sz sg) 50  is_true_pointer_pointer: ∀ psp,b,ofs,s,t.51 is_true (Vptr psp bofs) (Tpointer s t)50  is_true_pointer_pointer: ∀r,b,pc,ofs,s,t. 51 is_true (Vptr r b pc ofs) (Tpointer s t) 52 52  is_true_float: ∀f,sz. 53 53 f ≠ Fzero → … … 96 96 match v with 97 97 [ Vint n ⇒ Some ? (of_bool (eq n zero)) 98  Vptr _ _ _ ⇒ Some ? Vfalse98  Vptr _ _ _ _ ⇒ Some ? Vfalse 99 99  _ ⇒ None ? 100 100 ] … … 102 102 match v with 103 103 [ Vint n ⇒ Some ? (of_bool (eq n zero)) 104  Vptr _ _ _ ⇒ Some ? Vfalse104  Vptr _ _ _ _ ⇒ Some ? Vfalse 105 105  _ ⇒ None ? 106 106 ] … … 129 129  add_case_pi ty ⇒ (**r pointer plus integer *) 130 130 match v1 with 131 [ Vptr pcl1 b1 ofs1 ⇒ match v2 with132 [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (add ofs1 (mul (repr (sizeof ty)) n2)))131 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 132 [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (add ofs1 (mul (repr (sizeof ty)) n2))) 133 133  _ ⇒ None ? ] 134 134  Vnull r ⇒ match v2 with … … 139 139 match v1 with 140 140 [ Vint n1 ⇒ match v2 with 141 [ Vptr pcl2 b2 ofs2 ⇒ Some ? (Vptr pcl2 b2 (add ofs2 (mul (repr (sizeof ty)) n1)))141 [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (add ofs2 (mul (repr (sizeof ty)) n1))) 142 142  _ ⇒ None ? ] 143 143  _ ⇒ None ? ] … … 161 161  sub_case_pi ty ⇒ (**r pointer minus integer *) 162 162 match v1 with 163 [ Vptr pcl1 b1 ofs1 ⇒ match v2 with164 [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (sub ofs1 (mul (repr (sizeof ty)) n2)))163 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 164 [ Vint n2 ⇒ Some ? (Vptr r1 b1 p1 (sub ofs1 (mul (repr (sizeof ty)) n2))) 165 165  _ ⇒ None ? ] 166 166  _ ⇒ None ? ] 167 167  sub_case_pp ty ⇒ (**r pointer minus pointer *) 168 168 match v1 with 169 [ Vptr pcl1 b1 ofs1 ⇒ match v2 with170 [ Vptr pcl2 b2 ofs2 ⇒169 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with 170 [ Vptr r2 b2 p2 ofs2 ⇒ 171 171 if eq_block b1 b2 then 172 172 if eq (repr (sizeof ty)) zero then None ? … … 321 321  _ ⇒ None ? 322 322 ] 323  Vptr r1 b1 ofs1 ⇒323  Vptr r1 b1 p1 ofs1 ⇒ 324 324 match v2 with 325 [ Vptr r2 b2 ofs2 ⇒325 [ Vptr r2 b2 p2 ofs2 ⇒ 326 326 if valid_pointer m r1 b1 (signed ofs1) 327 327 ∧ valid_pointer m r2 b2 (signed ofs2) then … … 334 334  Vnull r1 ⇒ 335 335 match v2 with 336 [ Vptr r2 b2 ofs2 ⇒ sem_cmp_mismatch c336 [ Vptr r2 b2 p2 ofs2 ⇒ sem_cmp_mismatch c 337 337  Vnull r2 ⇒ sem_cmp_match c 338 338  _ ⇒ None ? … … 429 429 cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) 430 430 (Vfloat (cast_float_float sz2 f)) 431  cast_pp: ∀m,r,r',ty,ty',b, ofs.431  cast_pp: ∀m,r,r',ty,ty',b,pc,ofs. 432 432 type_region ty r → 433 433 type_region ty' r' → 434 pointer_compat b r' →435 cast m (Vptr r b ofs) ty ty' (Vptr r' bofs)434 ∀pc':pointer_compat b r'. 435 cast m (Vptr r b pc ofs) ty ty' (Vptr r' b pc' ofs) 436 436  cast_ip_z: ∀m,sz,sg,ty',r. 437 437 type_region ty' r → … … 466 466 let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val ≝ 467 467 match access_mode ty with 468 [ By_value chunk ⇒ loadv chunk m (Vptr Any b ofs) 469  By_reference r ⇒ Some ? (Vptr r b ofs) 468 [ By_value chunk ⇒ loadv chunk m (Vptr Any b ? ofs) 469  By_reference r ⇒ 470 match pointer_compat_dec b r with 471 [ inl p ⇒ Some ? (Vptr r b p ofs) 472  inr _ ⇒ None ? 473 ] 470 474  By_nothing ⇒ None ? 471 475 ]. 476 cases b // 477 qed. 472 478 473 479 (* * Symmetrically, [store_value_of_type ty m b ofs v] returns the … … 478 484 let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem ≝ 479 485 match access_mode ty_dest with 480 [ By_value chunk ⇒ storev chunk m (Vptr Any loc ofs) v486 [ By_value chunk ⇒ storev chunk m (Vptr Any loc ? ofs) v 481 487  By_reference _ ⇒ None ? 482 488  By_nothing ⇒ None ? 483 489 ]. 490 cases loc // 491 qed. 484 492 485 493 (* * Allocation of functionlocal variables. … … 570 578  eval_Eaddrof: ∀a,ty,r,loc,ofs,tr. 571 579 eval_lvalue ge e m a loc ofs tr → 572 eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc ofs) tr 580 ∀pc:pointer_compat loc r. 581 eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr 573 582  eval_Esizeof: ∀ty',ty. 574 583 eval_expr ge e m (Expr (Esizeof ty') ty) (Vint (repr (sizeof ty'))) E0 … … 633 642 find_symbol ?? ge id = Some ? l → 634 643 eval_lvalue ge e m (Expr (Evar id) ty) l zero E0 635  eval_Ederef: ∀a,ty,r,l, ofs,tr.636 eval_expr ge e m a (Vptr r l ofs) tr →644  eval_Ederef: ∀a,ty,r,l,p,ofs,tr. 645 eval_expr ge e m a (Vptr r l p ofs) tr → 637 646 eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr 638 647 (* Aside: note that each block of memory is entirely contained within one … … 654 663 (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) 655 664 (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2)) 656 (ead:∀a,ty, psp,loc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))665 (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H)) 657 666 (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty)) 658 667 (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)) … … 671 680  eval_Econst_float f ty ⇒ ecF f ty 672 681  eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 673  eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp loc ofs tr H682  eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H 674 683  eval_Esizeof ty' ty ⇒ esz ty' ty 675 684  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) … … 691 700 (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H)) 692 701 (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2)) 693 (lde:∀a,ty, psp,l,ofs,tr,H. P ???? (eval_Ederef ge e m a ty psp lofs tr H))702 (lde:∀a,ty,r,l,pc,ofs,tr,H. P ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) 694 703 (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)) 695 704 (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)) … … 698 707 [ eval_Evar_local id l ty H ⇒ lvl id l ty H 699 708  eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 700  eval_Ederef a ty psp l ofs tr H ⇒ lde a ty psp lofs tr H709  eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H 701 710  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) 702 711  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) … … 762 771 (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) 763 772 (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)) 764 (ead:∀a,ty, psp,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))773 (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)) 765 774 (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty)) 766 775 (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)) … … 776 785 (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) 777 786 (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) 778 (lde:∀a,ty, psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ???? (eval_Ederef ge e m a ty psp lofs tr H))787 (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) 779 788 (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)) 780 789 (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)) … … 785 794  eval_Econst_float f ty ⇒ ecF f ty 786 795  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) 787  eval_Eaddrof a ty psp loc ofs tr H ⇒ ead a ty psp 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)796  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) 788 797  eval_Esizeof ty' ty ⇒ esz ty' ty 789 798  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) … … 804 813 (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty)) 805 814 (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)) 806 (ead:∀a,ty, psp,loc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty psp loc ofs tr H))815 (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)) 807 816 (esz:∀ty',ty. P ??? (eval_Esizeof ge e m ty' ty)) 808 817 (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)) … … 818 827 (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) 819 828 (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) 820 (lde:∀a,ty, psp,l,ofs,tr,H. P a (Vptr psp l ofs) tr H → Q ???? (eval_Ederef ge e m a ty psp lofs tr H))829 (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr r l pc ofs) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H)) 821 830 (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)) 822 831 (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)) … … 825 834 [ eval_Evar_local id l ty H ⇒ lvl id l ty H 826 835  eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 827  eval_Ederef a ty psp l ofs tr H ⇒ lde a ty psp 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 psp lofs) tr H)836  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 r l pc ofs) tr H) 828 837  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) 829 838  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)
Note: See TracChangeset
for help on using the changeset viewer.