Changeset 484 for Deliverables/D3.1/Csemantics/Csem.ma
 Timestamp:
 Jan 28, 2011, 2:41:49 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Csem.ma
r481 r484 39 39  is_false_int: ∀sz,sg. 40 40 is_false (Vint zero) (Tint sz sg) 41  is_false_pointer: ∀ s,t.42 is_false (V int zero) (Tpointer st)41  is_false_pointer: ∀r,r',t. 42 is_false (Vnull r) (Tpointer r' t) 43 43  is_false_float: ∀sz. 44 44 is_false (Vfloat Fzero) (Tfloat sz). … … 48 48 n ≠ zero → 49 49 is_true (Vint n) (Tint sz sg) 50  is_true_pointer_int: ∀psp,b,ofs,sz,sg.51 is_true (Vptr psp b ofs) (Tint sz sg)52  is_true_int_pointer: ∀n,s,t.53 n ≠ zero →54 is_true (Vint n) (Tpointer s t)55 50  is_true_pointer_pointer: ∀psp,b,ofs,s,t. 56 51 is_true (Vptr psp b ofs) (Tpointer s t) … … 136 131 [ Vptr pcl1 b1 ofs1 ⇒ match v2 with 137 132 [ Vint n2 ⇒ Some ? (Vptr pcl1 b1 (add ofs1 (mul (repr (sizeof ty)) n2))) 133  _ ⇒ None ? ] 134  Vnull r ⇒ match v2 with 135 [ Vint n2 ⇒ if eq n2 zero then Some ? (Vnull r) else None ? 138 136  _ ⇒ None ? ] 139 137  _ ⇒ None ? ] … … 176 174 else None ? 177 175  _ ⇒ None ? ] 176  Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero)  _ ⇒ None ? ] 178 177  _ ⇒ None ? ] 179 178  sub_default ⇒ None ? … … 299 298 ]. 300 299 300 nlet rec sem_cmp_match (c: comparison): option val ≝ 301 match c with 302 [ Ceq => Some ? Vtrue 303  Cne => Some ? Vfalse 304  _ => None ? 305 ]. 306 301 307 nlet rec sem_cmp (c:comparison) 302 308 (v1: val) (t1: type) (v2: val) (t2: type) … … 313 319 [ Vint n1 ⇒ match v2 with 314 320 [ Vint n2 ⇒ Some ? (of_bool (cmp c n1 n2)) 315  Vptr psp b ofs ⇒ if eq n1 zero then sem_cmp_mismatch c else None ?316 321  _ ⇒ None ? 317 322 ] 318  Vptr pcl1 b1 ofs1 ⇒323  Vptr r1 b1 ofs1 ⇒ 319 324 match v2 with 320 [ Vptr pcl2 b2 ofs2 ⇒321 if valid_pointer m pcl1 b1 (signed ofs1)322 ∧ valid_pointer m pcl2 b2 (signed ofs2) then325 [ Vptr r2 b2 ofs2 ⇒ 326 if valid_pointer m r1 b1 (signed ofs1) 327 ∧ valid_pointer m r2 b2 (signed ofs2) then 323 328 if eqZb b1 b2 324 329 then Some ? (of_bool (cmp c ofs1 ofs2)) 325 330 else sem_cmp_mismatch c 326 331 else None ? 327  Vint n ⇒ 328 if eq n zero then sem_cmp_mismatch c else None ? 332  Vnull r2 ⇒ sem_cmp_mismatch c 329 333  _ ⇒ None ? ] 334  Vnull r1 ⇒ 335 match v2 with 336 [ Vptr r2 b2 ofs2 ⇒ sem_cmp_mismatch c 337  Vnull r2 ⇒ sem_cmp_match c 338  _ ⇒ None ? 339 ] 330 340  _ ⇒ None ? ] 331 341  cmp_case_ff ⇒ … … 400 410 ]. 401 411 402 ninductive type_pointable : type → Prop ≝ 403 (* All integer sizes can represent at least one kind of pointer *) 404  type_ptr_pointer : ∀s,t. type_pointable (Tpointer s t) 405  type_ptr_array : ∀s,t,n. type_pointable (Tarray s t n) 406  type_ptr_function : ∀tys,ty. type_pointable (Tfunction tys ty). 407 408 ninductive type_space : type → region → Prop ≝ 409  type_spc_pointer : ∀s,t. type_space (Tpointer s t) s 410  type_spc_array : ∀s,t,n. type_space (Tarray s t n) s 412 ninductive type_region : type → region → Prop ≝ 413  type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s 414  type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s 411 415 (* XXX Is the following necessary? *) 412  type_ spc_code : ∀tys,ty. type_space(Tfunction tys ty) Code.416  type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code. 413 417 414 418 ninductive cast : mem → val → type → type → val → Prop ≝ … … 425 429 cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2) 426 430 (Vfloat (cast_float_float sz2 f)) 427  cast_pp: ∀m,psp,psp',ty,ty',b,ofs. 428 type_space ty psp → 429 type_space ty' psp' → 430 pointer_compat (block_space m b) psp' → 431 cast m (Vptr psp b ofs) ty ty' (Vptr psp' b ofs) 432  cast_ip_z: ∀m,sz,sg,ty'. 433 type_pointable ty' → 434 cast m (Vint zero) (Tint sz sg) ty' (Vint zero) 435  cast_pp_z: ∀m,ty,ty'. 436 type_pointable ty → 437 type_pointable ty' → 438 cast m (Vint zero) ty ty' (Vint zero). 439 (* Should probably also allow pointers to pass through sufficiently large 440 unsigned integers. *) 441 (* Perhaps a little too generous? For example, some integers may not 442 represent a valid generic pointer. 443  cast_pp_i: ∀m,n,ty,ty',t1,t2. (**r no change in data representation *) 444 type_pointable ty → 445 type_pointable ty' → 446 sizeof ty ≤ sizeof ty' → 447 cast m (Vint n) t1 t2 (Vint n). 448 *) 431  cast_pp: ∀m,r,r',ty,ty',b,ofs. 432 type_region ty r → 433 type_region ty' r' → 434 pointer_compat (block_space m b) r' → 435 cast m (Vptr r b ofs) ty ty' (Vptr r' b ofs) 436  cast_ip_z: ∀m,sz,sg,ty',r. 437 type_region ty' r → 438 cast m (Vint zero) (Tint sz sg) ty' (Vnull r) 439  cast_pp_z: ∀m,ty,ty',r,r'. 440 type_region ty r → 441 type_region ty' r' → 442 cast m (Vnull r) ty ty' (Vnull r'). 449 443 450 444 (* * * Operational semantics *)
Note: See TracChangeset
for help on using the changeset viewer.