Changeset 1545 for src/common


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

Use pointer record in front-end.

Location:
src/common
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndOps.ma

    r1516 r1545  
    8484      match find_symbol s with
    8585      [ None ⇒ None ?
    86       | Some b ⇒ Some ? (Vptr Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs)))
     86      | Some b ⇒ Some ? (Vptr (mk_pointer Any b (match b with [ mk_block r id ⇒ universal_compat r id ]) (shift_offset ? zero_offset (repr I16 ofs))))
    8787      ]
    8888  | Oaddrstack ofs ⇒
    89       Some ? (Vptr Any sp ? (shift_offset ? zero_offset (repr I16 ofs)))
     89      Some ? (Vptr (mk_pointer Any sp ? (shift_offset ? zero_offset (repr I16 ofs))))
    9090  ]. cases sp // qed.
    9191
     
    102102      match arg with
    103103      [ Vint sz1 n1 ⇒ Some ? (Vint sz (if (eq_bv ? n1 (zero ?)) then (repr ? 1) else (zero ?)))
    104       | Vptr _ _ _ _ ⇒ Some ? (Vint sz (zero ?))
     104      | Vptr _ ⇒ Some ? (Vint sz (zero ?))
    105105      | Vnull _ ⇒ Some ? (Vint sz (repr ? 1))
    106106      | _ ⇒ None ?
     
    125125[ ASTint sz sg ⇒ ∀i.P (Vint sz i)
    126126| ASTfloat sz ⇒ ∀f.P (Vfloat f)
    127 | ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr r b c o)
     127| ASTptr r ⇒ P (Vnull r) ∧ ∀b,c,o. P (Vptr (mk_pointer r b c o))
    128128] →
    129129P v.
     
    197197definition ev_addp ≝ λv1,v2: val.
    198198  match v1 with
    199   [ Vptr r b1 p ofs1 ⇒ match v2 with
    200     [ Vint sz2 n2 ⇒ Some ? (Vptr r b1 p (shift_offset ? ofs1 n2))
     199  [ Vptr ptr1 ⇒ match v2 with
     200    [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer ? ptr1 n2))
    201201    | _ ⇒ None ? ]
    202202  | Vnull r ⇒ match v2 with
     
    208208definition ev_subpi ≝ λv1,v2: val.
    209209  match v1 with
    210   [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    211     [ Vint sz2 n2 ⇒ Some ? (Vptr r1 b1 p1 (neg_shift_offset ? ofs1 n2))
     210  [ Vptr ptr1 ⇒ match v2 with
     211    [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer ? ptr1 n2))
    212212    | _ ⇒ None ? ]
    213213  | Vnull r ⇒ match v2 with [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ? | _ ⇒ None ? ]
     
    216216definition ev_subpp ≝ λsz. λv1,v2: val.
    217217  match v1 with
    218   [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    219     [ Vptr r2 b2 p2 ofs2 ⇒
    220         if eq_block b1 b2 then Some ? (Vint sz (sub_offset ? ofs1 ofs2)) else None ?
     218  [ Vptr ptr1 ⇒ match v2 with
     219    [ Vptr ptr2 ⇒
     220        if eq_block (pblock ptr1) (pblock ptr2)
     221          then Some ? (Vint sz (sub_offset ? (poff ptr1) (poff ptr2)))
     222          else None ?
    221223    | _ ⇒ None ? ]
    222224  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint sz (zero ?)) | _ ⇒ None ? ]
     
    384386definition ev_cmpp ≝ λc: comparison. λv1,v2: val.
    385387  match v1 with
    386   [ Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    387     [ Vptr r2 b2 p2 ofs2 ⇒
    388         if eq_block b1 b2
    389         then Some ? (of_bool (cmp_offset c ofs1 ofs2))
     388  [ Vptr ptr1 ⇒ match v2 with
     389    [ Vptr ptr2 ⇒
     390        if eq_block (pblock ptr1) (pblock ptr2)
     391        then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
    390392        else ev_cmp_mismatch c
    391393    | Vnull r2 ⇒ ev_cmp_mismatch c
    392394    | _ ⇒ None ? ]
    393395  | Vnull r1 ⇒ match v2 with
    394     [ Vptr _ _ _ _ ⇒ ev_cmp_mismatch c
     396    [ Vptr _ ⇒ ev_cmp_mismatch c
    395397    | Vnull r2 ⇒ ev_cmp_match c
    396398    | _ ⇒ None ?
  • src/common/Globalenvs.ma

    r1395 r1545  
    416416      | Some b' ⇒
    417417        match pointer_compat_dec b' r' with
    418         [ inl pc ⇒ store (Mpointer r') m r b p (Vptr r' b' pc (shift_offset ? zero_offset (repr I16 ofs)))
     418        [ inl pc ⇒ store (Mpointer r') m r b p (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
    419419        | inr _ ⇒ None ?
    420420        ]
     
    540540  init_mem_
    541541  (λF,ge. functions ? ge) (* find_funct_ptr *)
    542   (λF,ge,v. match v with [ Vptr _ b _ o ⇒ if eq_offset o zero_offset then functions ? ge b else None ? | _ ⇒ None ? ]) (* find_funct *)
     542  (λF,ge,v. match v with [ Vptr ptr ⇒ if eq_offset (poff ptr) zero_offset then functions ? ge (pblock ptr) else None ? | _ ⇒ None ? ]) (* find_funct *)
    543543  (λF,ge. symbols ? ge) (* find_symbol *)
    544544(*  ?
  • src/common/Mem.ma

    r1523 r1545  
    643643  given offset falls within the bounds of the corresponding block. *)
    644644
    645 definition valid_pointer : mem → region → block → offset → bool ≝
    646 λm,r,b,ofs. Zltb (block_id b) (nextblock m) ∧
    647   Zleb (low_bound m b) (offv ofs) ∧
    648   Zltb (offv ofs) (high_bound m b) ∧
    649   is_pointer_compat b r.
     645definition valid_pointer : mem → pointer → bool ≝
     646λm,ptr. Zltb (block_id (pblock ptr)) (nextblock m) ∧
     647  Zleb (low_bound m (pblock ptr)) (offv (poff ptr)) ∧
     648  Zltb (offv (poff ptr)) (high_bound m (pblock ptr)).
    650649
    651650(* [load chunk m r b ofs] perform a read in memory state [m], at address
     
    679678let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝
    680679  match addr with
    681   [ Vptr r b p ofs ⇒ load chunk m r b (offv ofs)
     680  [ Vptr ptr ⇒ load chunk m (ptype ptr) (pblock ptr) (offv (poff ptr))
    682681  | _ ⇒ None ? ].
    683682
     
    726725λchunk,m,addr,v.
    727726  match addr with
    728   [ Vptr r b p ofs ⇒ store chunk m r b (offv ofs) v
     727  [ Vptr ptr ⇒ store chunk m (ptype ptr) (pblock ptr) (offv (poff ptr)) v
    729728  | _ ⇒ None ? ].
    730729
     
    35153514  storev Mint8signed m a v = storev Mint8unsigned m a v.
    35163515#m #a #v whd in ⊢ (??%%); elim a //
    3517 #r #b #p #ofs whd in ⊢ (??%%);
     3516#ptr whd in ⊢ (??%%);
    35183517>(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //
    35193518qed.
     
    35233522  storev Mint16signed m a v = storev Mint16unsigned m a v.
    35243523#m #a #v whd in ⊢ (??%%); elim a //
    3525 #r #b #p #ofs whd in ⊢ (??%%);
     3524#ptr whd in ⊢ (??%%);
    35263525>(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //
    35273526qed.
  • src/common/Pointers.ma

    r1516 r1545  
    100100 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset n (poff p) i).
    101101
     102(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
     103definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
     104 λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset_n n (poff p) i j).
     105
    102106definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
    103107 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i).
     108
     109definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
     110 λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset_n n (poff p) i j).
    104111
    105112definition eq_pointer: pointer → pointer → bool ≝
  • 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.