Changeset 1545 for src/Clight/Csem.ma
 Timestamp:
 Nov 23, 2011, 6:03:07 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Csem.ma
r1231 r1545 47 47 n ≠ (zero ?) → 48 48 is_true (Vint sz n) (Tint sz sg) 49  is_true_pointer_pointer: ∀ r,b,pc,ofs,s,t.50 is_true (Vptr r b pc ofs) (Tpointer s t)49  is_true_pointer_pointer: ∀ptr,s,t. 50 is_true (Vptr ptr) (Tpointer s t) 51 51  is_true_float: ∀f,sz. 52 52 f ≠ Fzero → … … 103 103  Tpointer _ _ ⇒ 104 104 match v with 105 [ Vptr _ _ _ _⇒ Some ? Vfalse105 [ Vptr _ ⇒ Some ? Vfalse 106 106  Vnull _ ⇒ Some ? Vtrue 107 107  _ ⇒ None ? … … 132 132  add_case_pi ty ⇒ (**r pointer plus integer *) 133 133 match v1 with 134 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with135 [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (shift_offset_n ? ofs1 (sizeof ty) n2))134 [ Vptr ptr1 ⇒ match v2 with 135 [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) n2)) 136 136  _ ⇒ None ? ] 137 137  Vnull r ⇒ match v2 with … … 142 142 match v1 with 143 143 [ Vint sz1 n1 ⇒ match v2 with 144 [ Vptr r2 b2 p2 ofs2 ⇒ Some ? (Vptr r2 b2 p2 (shift_offset_n ? ofs2 (sizeof ty) n1))144 [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) n1)) 145 145  Vnull r ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ? 146 146  _ ⇒ None ? ] … … 166 166  sub_case_pi ty ⇒ (**r pointer minus integer *) 167 167 match v1 with 168 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with169 [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset_n ? ofs1 (sizeof ty) n2))168 [ Vptr ptr1 ⇒ match v2 with 169 [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) n2)) 170 170  _ ⇒ None ? ] 171 171  Vnull r ⇒ match v2 with … … 175 175  sub_case_pp ty ⇒ (**r pointer minus pointer *) 176 176 match v1 with 177 [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with178 [ Vptr r2 b2 p2 ofs2 ⇒179 if eq_block b1 b2then177 [ Vptr ptr1 ⇒ match v2 with 178 [ Vptr ptr2 ⇒ 179 if eq_block (pblock ptr1) (pblock ptr2) then 180 180 if eqb (sizeof ty) 0 then None ? 181 else match division_u ? (sub_offset ? ofs1 ofs2) (repr (sizeof ty)) with181 else match division_u ? (sub_offset ? (poff ptr1) (poff ptr2)) (repr (sizeof ty)) with 182 182 [ None ⇒ None ? 183 183  Some v ⇒ Some ? (Vint I32 v) (* XXX choose size from result type? *) … … 352 352  cmp_case_pp ⇒ 353 353 match v1 with 354 [ Vptr r1 b1 p1 ofs1 ⇒354 [ Vptr ptr1 ⇒ 355 355 match v2 with 356 [ Vptr r2 b2 p2 ofs2 ⇒357 if valid_pointer m r1 b1 ofs1358 ∧ valid_pointer m r2 b2 ofs2 then359 if eq_block b1 b2360 then Some ? (of_bool (cmp_offset c ofs1 ofs2))356 [ Vptr ptr2 ⇒ 357 if valid_pointer m ptr1 358 ∧ valid_pointer m ptr2 then 359 if eq_block (pblock ptr1) (pblock ptr2) 360 then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2))) 361 361 else sem_cmp_mismatch c 362 362 else None ? … … 365 365  Vnull r1 ⇒ 366 366 match v2 with 367 [ Vptr r2 b2 p2 ofs2 ⇒ sem_cmp_mismatch c367 [ Vptr ptr2 ⇒ sem_cmp_mismatch c 368 368  Vnull r2 ⇒ sem_cmp_match c 369 369  _ ⇒ None ? … … 456 456 cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) 457 457 (Vfloat (cast_float_float sz2 f)) 458  cast_pp: ∀m, r,r',ty,ty',b,pc,ofs.459 type_region ty r→458  cast_pp: ∀m,ty,ty',ptr,r'. 459 type_region ty (ptype ptr) → 460 460 type_region ty' r' → 461 ∀pc':pointer_compat br'.462 cast m (Vptr r b pc ofs) ty ty' (Vptr r' b pc' ofs)461 ∀pc':pointer_compat (pblock ptr) r'. 462 cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr))) 463 463  cast_ip_z: ∀m,sz,sg,ty',r. 464 464 type_region ty' r → … … 493 493 let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝ 494 494 match access_mode ty with 495 [ By_value chunk ⇒ loadv chunk m (Vptr Any b ? ofs)495 [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer Any b ? ofs)) 496 496  By_reference r ⇒ 497 497 match pointer_compat_dec b r with 498 [ inl p ⇒ Some ? (Vptr r b p ofs)498 [ inl p ⇒ Some ? (Vptr (mk_pointer r b p ofs)) 499 499  inr _ ⇒ None ? 500 500 ] … … 511 511 let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝ 512 512 match access_mode ty_dest with 513 [ By_value chunk ⇒ storev chunk m (Vptr Any loc ? ofs) v513 [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer Any loc ? ofs)) v 514 514  By_reference _ ⇒ None ? 515 515  By_nothing ⇒ None ? … … 608 608 eval_lvalue ge e m a loc ofs tr → 609 609 ∀pc:pointer_compat loc r. 610 eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr r loc pc ofs) tr610 eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr (mk_pointer r loc pc ofs)) tr 611 611  eval_Esizeof: ∀ty',sz,sg. 612 612 eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0 … … 672 672 eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0 673 673  eval_Ederef: ∀a,ty,r,l,p,ofs,tr. 674 eval_expr ge e m a (Vptr r l p ofs) tr →674 eval_expr ge e m a (Vptr (mk_pointer r l p ofs)) tr → 675 675 eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr 676 676 (* Aside: note that each block of memory is entirely contained within one … … 814 814 (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) 815 815 (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) 816 (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))816 (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 pc ofs tr H)) 817 817 (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)) 818 818 (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 856 (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H)) 857 857 (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2)) 858 (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))858 (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 pc ofs tr H)) 859 859 (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)) 860 860 (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)) … … 863 863 [ eval_Evar_local id l ty H ⇒ lvl id l ty H 864 864  eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2 865  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)865  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 pc ofs)) tr H) 866 866  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) 867 867  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.