Ignore:
Timestamp:
Feb 22, 2011, 4:23:13 PM (9 years ago)
Author:
campbell
Message:

Abstract pointer offsets a little, similar to the changes for the prototype
proposed in Bologna.

File:
1 edited

Legend:

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

    r500 r583  
    6060λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
    6161
     62record offset : Type[0] ≝ { offv : Z }.
     63
     64definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
     65definition shift_offset : offset → int → offset ≝
     66  λo,i. mk_offset (offv o + signed i).
     67definition neg_shift_offset : offset → int → offset ≝
     68  λo,i. mk_offset (offv o - signed i).
     69definition sub_offset : offset → offset → int ≝
     70  λx,y. repr (offv x - offv y).
     71definition zero_offset ≝ mk_offset OZ.
     72definition lt_offset : offset → offset → bool ≝
     73  λx,y. Zltb (offv x) (offv y).
     74
    6275(* * A value is either:
    6376- a machine integer;
     
    7689  | Vfloat: float → val
    7790  | Vnull: region → val
    78   | Vptr: ∀r:region. ∀b:block. pointer_compat b r → int → val.
     91  | Vptr: ∀r:region. ∀b:block. pointer_compat b r → offset → val.
    7992
    8093definition Vzero: val ≝ Vint zero.
     
    219232  [ Vint n1 ⇒ match v2 with
    220233    [ Vint n2 ⇒ Vint (add n1 n2)
    221     | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (add ofs2 n1)
     234    | Vptr r b2 p ofs2 ⇒ Vptr r b2 p (shift_offset ofs2 n1)
    222235    | _ ⇒ Vundef ]
    223236  | Vptr r b1 p ofs1 ⇒ match v2 with
    224     [ Vint n2 ⇒ Vptr r b1 p (add ofs1 n2)
     237    [ Vint n2 ⇒ Vptr r b1 p (shift_offset ofs1 n2)
    225238    | _ ⇒ Vundef ]
    226239  | _ ⇒ Vundef ].
     
    232245    | _ ⇒ Vundef ]
    233246  | Vptr r1 b1 p1 ofs1 ⇒ match v2 with
    234     [ Vint n2 ⇒ Vptr r1 b1 p1 (sub ofs1 n2)
     247    [ Vint n2 ⇒ Vptr r1 b1 p1 (neg_shift_offset ofs1 n2)
    235248    | Vptr r2 b2 p2 ofs2 ⇒
    236         if eq_block b1 b2 then Vint (sub ofs1 ofs2) else Vundef
     249        if eq_block b1 b2 then Vint (sub_offset ofs1 ofs2) else Vundef
    237250    | _ ⇒ Vundef ]
    238251  | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Vint zero | _ ⇒ Vundef ]
     
    397410  ].
    398411
    399 (* TODO: consider whether to check pointer representations *)
     412definition cmp_offset ≝
     413λc: comparison. λx,y:offset.
     414  match c with
     415  [ Ceq ⇒  eq_offset x y
     416  | Cne ⇒ ¬eq_offset x y
     417  | Clt ⇒  lt_offset x y
     418  | Cle ⇒ ¬lt_offset y x
     419  | Cgt ⇒  lt_offset y x
     420  | Cge ⇒ ¬lt_offset x y
     421  ].
     422
    400423definition cmp ≝ λc: comparison. λv1,v2: val.
    401424  match v1 with
     
    406429    [ Vptr r2 b2 p2 ofs2 ⇒
    407430        if eq_block b1 b2
    408         then of_bool (cmp c ofs1 ofs2)
     431        then of_bool (cmp_offset c ofs1 ofs2)
    409432        else cmp_mismatch c
    410433    | Vnull r2 ⇒ cmp_mismatch c
     
    425448    [ Vptr r2 b2 p2 ofs2 ⇒
    426449        if eq_block b1 b2
    427         then of_bool (cmpu c ofs1 ofs2)
     450        then of_bool (cmp_offset c ofs1 ofs2)
    428451        else cmp_mismatch c
    429452    | Vnull r2 ⇒ cmp_mismatch c
Note: See TracChangeset for help on using the changeset viewer.