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

Separate out null values from integer zeros.

File:
1 edited

Legend:

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

    r483 r484  
    3333             memory regions such a pointer could address), a memory address and
    3434             an integer offset with respect to this address;
     35- a null pointer: the region denotes the representation (i.e., pointer size)
    3536- the [Vundef] value denoting an arbitrary bit pattern, such as the
    3637  value of an uninitialized variable.
     
    4142  | Vint: int → val
    4243  | Vfloat: float → val
     44  | Vnull: region → val
    4345  | Vptr: region → block → int → val.
    4446
     
    5860*)
    5961ndefinition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.
    60 
     62(*
    6163ndefinition has_type ≝ λv: val. λt: typ.
    6264  match v with
     
    7476               has_type v1 t1 ∧ has_type_list vs ts ]
    7577  ].
    76 
     78*)
    7779(* * Truth values.  Pointers and non-zero integers are treated as [True].
    7880  The integer 0 (also used to represent the null pointer) is [False].
     
    8991  match v with
    9092  [ Vint n ⇒ n = zero
     93  | Vnull _ ⇒ True
    9194  | _ ⇒ False
    9295  ].
     
    98101      bool_of_val (Vint zero) false
    99102  | bool_of_val_ptr:
    100       ∀pty,b,ofs. bool_of_val (Vptr pty b ofs) true.
     103      ∀r,b,ofs. bool_of_val (Vptr r b ofs) true
     104  | bool_of_val_null:
     105      ∀r. bool_of_val (Vnull r) true.
    101106
    102107ndefinition neg : val → val ≝ λv.
     
    154159  [ Vint n ⇒ of_bool (int_eq n zero)
    155160  | Vptr _ b ofs ⇒ Vfalse
     161  | Vnull _ ⇒ Vtrue
    156162  | _ ⇒ Vundef
    157163  ].
     
    175181  ].
    176182
     183(* TODO: add zero to null? *)
    177184ndefinition add ≝ λv1,v2: val.
    178185  match v1 with
     
    196203        if eqZb b1 b2 then Vint (sub ofs1 ofs2) else Vundef
    197204    | _ ⇒ Vundef ]
     205  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
    198206  | _ ⇒ Vundef ].
    199207
     
    342350  | _ ⇒ Vundef ].
    343351
     352ndefinition cmp_match : comparison → val ≝ λc.
     353  match c with
     354  [ Ceq ⇒ Vtrue
     355  | Cne ⇒ Vfalse
     356  | _   ⇒ Vundef
     357  ].
     358
    344359ndefinition cmp_mismatch : comparison → val ≝ λc.
    345360  match c with
     
    349364  ].
    350365
     366(* TODO: consider whether to check pointer representations *)
    351367ndefinition cmp ≝ λc: comparison. λv1,v2: val.
    352368  match v1 with
    353369  [ Vint n1 ⇒ match v2 with
    354370    [ Vint n2 ⇒ of_bool (cmp c n1 n2)
    355     | Vptr pty2 b2 ofs2 ⇒
    356         if eq n1 zero then cmp_mismatch c else Vundef
    357     | _ ⇒ Vundef ]
    358   | Vptr pty1 b1 ofs1 ⇒ match v2 with
    359     [ Vptr pty2 b2 ofs2 ⇒
     371    | _ ⇒ Vundef ]
     372  | Vptr r1 b1 ofs1 ⇒ match v2 with
     373    [ Vptr r2 b2 ofs2 ⇒
    360374        if eqZb b1 b2
    361375        then of_bool (cmp c ofs1 ofs2)
    362376        else cmp_mismatch c
    363     | Vint n2 ⇒
    364         if eq n2 zero then cmp_mismatch c else Vundef
    365     | _ ⇒ Vundef ]
     377    | Vnull r2 ⇒ cmp_mismatch c
     378    | _ ⇒ Vundef ]
     379  | Vnull r1 ⇒ match v2 with
     380    [ Vptr _ _ _ ⇒ cmp_mismatch c
     381    | Vnull r2 ⇒ cmp_match c
     382    | _ ⇒ Vundef
     383    ]
    366384  | _ ⇒ Vundef ].
    367385
     
    370388  [ Vint n1 ⇒ match v2 with
    371389    [ Vint n2 ⇒ of_bool (cmpu c n1 n2)
    372     | Vptr pty2 b2 ofs2 ⇒
    373         if eq n1 zero then cmp_mismatch c else Vundef
    374     | _ ⇒ Vundef ]
    375   | Vptr pty1 b1 ofs1 ⇒ match v2 with
    376     [ Vptr pty2 b2 ofs2 ⇒
     390    | _ ⇒ Vundef ]
     391  | Vptr r1 b1 ofs1 ⇒ match v2 with
     392    [ Vptr r2 b2 ofs2 ⇒
    377393        if eqZb b1 b2
    378394        then of_bool (cmpu c ofs1 ofs2)
    379395        else cmp_mismatch c
    380     | Vint n2 ⇒
    381         if eq n2 zero then cmp_mismatch c else Vundef
    382     | _ ⇒ Vundef ]
     396    | Vnull r2 ⇒ cmp_mismatch c
     397    | _ ⇒ Vundef ]
     398  | Vnull r1 ⇒ match v2 with
     399    [ Vptr _ _ _ ⇒ cmp_mismatch c
     400    | Vnull r2 ⇒ cmp_match c
     401    | _ ⇒ Vundef
     402    ]
    383403  | _ ⇒ Vundef ].
    384404
     
    408428    | Mint16unsigned ⇒ Vint (zero_ext 16 n)
    409429    | Mint32 ⇒ Vint n
    410     | Mpointer r ⇒ if eq n zero then Vint zero else Vundef
    411430    | _ ⇒ Vundef
    412431    ]
     
    414433    match chunk with
    415434    [ Mpointer r' ⇒ if eq_region r r' then Vptr r b ofs else Vundef
     435    | _ ⇒ Vundef
     436    ]
     437  | Vnull r ⇒
     438    match chunk with
     439    [ Mpointer r' ⇒ if eq_region r r' then Vnull r else Vundef
    416440    | _ ⇒ Vundef
    417441    ]
Note: See TracChangeset for help on using the changeset viewer.