Changeset 1545 for src/common/Values.ma


Ignore:
Timestamp:
Nov 23, 2011, 6:03:07 PM (8 years ago)
Author:
campbell
Message:

Use pointer record in front-end.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Values.ma

    r1510 r1545  
    3939  | Vfloat: float → val
    4040  | Vnull: region → val
    41   | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.
     41  | Vptr: pointer → val.
    4242
    4343definition Vzero : intsize → val ≝ λsz. Vint sz (zero ?).
     
    5454  | VTfloat: ∀sz,f. val_typ (Vfloat f) (ASTfloat sz)
    5555  | VTnull: ∀r. val_typ (Vnull r) (ASTptr r)
    56   | VTptr: ∀r,b,c,o. val_typ (Vptr r b c o) (ASTptr r).
     56  | VTptr: ∀r,b,c,o. val_typ (Vptr (mk_pointer r b c o)) (ASTptr r).
    5757
    5858(*
     
    6464*)
    6565definition of_bool : bool → val ≝ λb. if b then Vtrue else Vfalse.
    66 (*
    67 definition has_type ≝ λv: val. λt: typ.
    68   match v with
    69   [ Vundef ⇒ True
    70   | Vint _ ⇒ match t with [ ASTint ⇒ True | _ ⇒ False ]
    71   | Vfloat _ ⇒ match t with [ ASTfloat ⇒ True | _ ⇒ False ]
    72   | Vptr _ _ _ ⇒ match t with [ ASTptr ⇒ True | _ ⇒ False ]
    73   | _ ⇒ False
    74   ].
    75 
    76 let rec has_type_list (vl: list val) (tl: list typ) on vl : Prop ≝
    77   match vl with
    78   [ nil ⇒ match tl with [ nil ⇒ True | _ ⇒ False ]
    79   | cons v1 vs ⇒ match tl with [ nil ⇒ False | cons t1 ts ⇒
    80                has_type v1 t1 ∧ has_type_list vs ts ]
    81   ].
    82 *)
     66
    8367(* * Truth values.  Pointers and non-zero integers are treated as [True].
    8468  The integer 0 (also used to represent the null pointer) is [False].
     
    8872  match v with
    8973  [ Vint _ n ⇒ n ≠ (zero ?)
    90   | Vptr _ b _ ofs ⇒ True
     74  | Vptr _ ⇒ True
    9175  | _ ⇒ False
    9276  ].
     
    10589      ∀sz. bool_of_val (Vzero sz) false
    10690  | bool_of_val_ptr:
    107       ∀r,b,p,ofs. bool_of_val (Vptr r b p ofs) true
     91      ∀p. bool_of_val (Vptr p) true
    10892  | bool_of_val_null:
    10993      ∀r. bool_of_val (Vnull r) true.
     
    11599[ Vint _ i ⇒ OK ? (notb (eq_bv ? i (zero ?)))
    116100| Vnull _ ⇒ OK ? false
    117 | Vptr _ _ _ _ ⇒ OK ? true
     101| Vptr _ ⇒ OK ? true
    118102| _ ⇒ Error ? (msg ValueNotABoolean)
    119103].
     
    170154  match v with
    171155  [ Vint sz n ⇒ of_bool (eq_bv ? n (zero ?))
    172   | Vptr _ b _ ofs ⇒ Vfalse
     156  | Vptr _ ⇒ Vfalse
    173157  | Vnull _ ⇒ Vtrue
    174158  | _ ⇒ Vundef
     
    200184                    (λn1. Vint sz2 (addition_n ? n1 n2))
    201185                    Vundef
    202     | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ? ofs2 n1)
    203     | _ ⇒ Vundef ]
    204   | Vptr r b1 p ofs1 ⇒ match v2 with
    205     [ Vint _ n2 ⇒ Vptr r b1 p (shift_offset ? ofs1 n2)
     186    | Vptr ptr ⇒ Vptr (shift_pointer ? ptr n1)
     187    | _ ⇒ Vundef ]
     188  | Vptr ptr ⇒ match v2 with
     189    [ Vint _ n2 ⇒ Vptr (shift_pointer ? ptr n2)
    206190    | _ ⇒ Vundef ]
    207191  | _ ⇒ Vundef ].
     
    216200                    Vundef
    217201    | _ ⇒ Vundef ]
    218   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    219     [ Vint sz2 n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2)
    220     | Vptr r2 b2 p2 ofs2 ⇒
    221         if eq_block b1 b2 then Vint I32 (sub_offset ? ofs1 ofs2) else Vundef
     202  | Vptr ptr1 ⇒ match v2 with
     203    [ Vint sz2 n2 ⇒ Vptr (neg_shift_pointer ? ptr1 n2)
     204    | Vptr ptr2 ⇒
     205        if eq_block (pblock ptr1) (pblock ptr2)
     206          then Vint I32 (sub_offset ? (poff ptr1) (poff ptr2))
     207          else Vundef
    222208    | _ ⇒ Vundef ]
    223209  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vzero I32 | _ ⇒ Vundef ]
     
    430416                    Vundef
    431417    | _ ⇒ Vundef ]
    432   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    433     [ Vptr r2 b2 p2 ofs2 ⇒
    434         if eq_block b1 b2
    435         then of_bool (cmp_offset c ofs1 ofs2)
     418  | Vptr ptr1 ⇒ match v2 with
     419    [ Vptr ptr2 ⇒
     420        if eq_block (pblock ptr1) (pblock ptr2)
     421        then of_bool (cmp_offset c (poff ptr1) (poff ptr2))
    436422        else cmp_mismatch c
    437423    | Vnull r2 ⇒ cmp_mismatch c
    438424    | _ ⇒ Vundef ]
    439425  | Vnull r1 ⇒ match v2 with
    440     [ Vptr _ _ _ _ ⇒ cmp_mismatch c
     426    [ Vptr _ ⇒ cmp_mismatch c
    441427    | Vnull r2 ⇒ cmp_match c
    442428    | _ ⇒ Vundef
     
    451437                    Vundef
    452438    | _ ⇒ Vundef ]
    453   | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    454     [ Vptr r2 b2 p2 ofs2 ⇒
    455         if eq_block b1 b2
    456         then of_bool (cmp_offset c ofs1 ofs2)
     439  | Vptr ptr1 ⇒ match v2 with
     440    [ Vptr ptr2 ⇒
     441        if eq_block (pblock ptr1) (pblock ptr2)
     442        then of_bool (cmp_offset c (poff ptr1) (poff ptr2))
    457443        else cmp_mismatch c
    458444    | Vnull r2 ⇒ cmp_mismatch c
    459445    | _ ⇒ Vundef ]
    460446  | Vnull r1 ⇒ match v2 with
    461     [ Vptr _ _ _ _ ⇒ cmp_mismatch c
     447    [ Vptr _ ⇒ cmp_mismatch c
    462448    | Vnull r2 ⇒ cmp_match c
    463449    | _ ⇒ Vundef
     
    495481    | _ ⇒ Vundef
    496482    ]
    497   | Vptr r b p ofs
     483  | Vptr ptr
    498484    match chunk with
    499     [ Mpointer r' ⇒ if eq_region r r' then Vptr r b p ofs else Vundef
     485    [ Mpointer r ⇒ if eq_region (ptype ptr) r then Vptr ptr else Vundef
    500486    | _ ⇒ Vundef
    501487    ]
Note: See TracChangeset for help on using the changeset viewer.