Ignore:
Timestamp:
Jan 28, 2011, 2:41:49 PM (9 years ago)
Author:
campbell
Message:

Separate out null values from integer zeros.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.1/C-semantics/Csem.ma

    r481 r484  
    3939  | is_false_int: ∀sz,sg.
    4040      is_false (Vint zero) (Tint sz sg)
    41   | is_false_pointer: ∀s,t.
    42       is_false (Vint zero) (Tpointer s t)
     41  | is_false_pointer: ∀r,r',t.
     42      is_false (Vnull r) (Tpointer r' t)
    4343 | is_false_float: ∀sz.
    4444      is_false (Vfloat Fzero) (Tfloat sz).
     
    4848      n ≠ zero →
    4949      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)
    5550  | is_true_pointer_pointer: ∀psp,b,ofs,s,t.
    5651      is_true (Vptr psp b ofs) (Tpointer s t)
     
    136131      [ Vptr pcl1 b1 ofs1 ⇒ match v2 with
    137132        [ 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 ?
    138136        | _ ⇒ None ? ]
    139137      | _ ⇒ None ? ]
     
    176174          else None ?
    177175        | _ ⇒ None ? ]
     176      | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint zero) | _ ⇒ None ? ]
    178177      | _ ⇒ None ? ]
    179178  | sub_default ⇒ None ?
     
    299298  ].
    300299
     300nlet rec sem_cmp_match (c: comparison): option val ≝
     301  match c with
     302  [ Ceq =>  Some ? Vtrue
     303  | Cne =>  Some ? Vfalse
     304  | _   => None ?
     305  ].
     306 
    301307nlet rec sem_cmp (c:comparison)
    302308                  (v1: val) (t1: type) (v2: val) (t2: type)
     
    313319      [ Vint n1 ⇒ match v2 with
    314320         [ 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 ?
    316321         | _ ⇒ None ?
    317322         ]
    318       | Vptr pcl1 b1 ofs1 ⇒
     323      | Vptr r1 b1 ofs1 ⇒
    319324        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) then
     325        [ Vptr r2 b2 ofs2 ⇒
     326          if valid_pointer m r1 b1 (signed ofs1)
     327          ∧ valid_pointer m r2 b2 (signed ofs2) then
    323328            if eqZb b1 b2
    324329            then Some ? (of_bool (cmp c ofs1 ofs2))
    325330            else sem_cmp_mismatch c
    326331          else None ?
    327         | Vint n ⇒
    328           if eq n zero then sem_cmp_mismatch c else None ?
     332        | Vnull r2 ⇒ sem_cmp_mismatch c
    329333        | _ ⇒ 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        ]
    330340      | _ ⇒ None ? ]
    331341  | cmp_case_ff ⇒
     
    400410  ].
    401411
    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
     412ninductive 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
    411415(* 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.
    413417
    414418ninductive cast : mem → val → type → type → val → Prop ≝
     
    425429      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
    426430           (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').
    449443
    450444(* * * Operational semantics *)
Note: See TracChangeset for help on using the changeset viewer.