source: src/common/Pointers.ma @ 2044

include "ASM/BitVectorZ.ma".
include "common/AST.ma". (* For the regions *)
include "utilities/extralib.ma".


(* To define pointers we need a few details about the memory model.

   There are several kinds of pointers, which differ in which regions of
   memory they address and the pointer's representation.
   
   Pointers are given as kind, block, offset triples, where a block identifies
   some memory in a given region with an arbitrary concrete address.  A proof
   is also required that the representation is suitable for the region the
   memory resides in.  Note that blocks cannot extend out of a region (in
   particular, a pdata pointer can address any byte in a pdata block - we never
   need to switch to a larger xdata pointer).
 *)

(* blocks - represented by the region the memory resides in and a unique id *)

record block : Type[0] ≝
{ block_region : region
; block_id : Z
}.

definition eq_block ≝
λb1,b2.
  eq_region (block_region b1) (block_region b2) ∧
  eqZb (block_id b1) (block_id b2)
.

lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
  P (eq_block b1 b2).
#P * #r1 #i1 * #r2 #i2 #H1 #H2
whd in ⊢ (?%); @eq_region_elim #H3
[ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
| @H2 % #E destruct elim H3 /2/
] qed.

lemma eq_block_b_b : ∀b. eq_block b b = true.
* * #z whd in ⊢ (??%?); >eqZb_z_z @refl
qed.

(* Characterise the memory regions which the pointer representations can
   address.

   pointer_compat <block> <pointer representation> *)

inductive pointer_compat : block → region → Prop ≝
|        same_compat : ∀s,id. pointer_compat (mk_block s id) s
|      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
|   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.

lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
* * #id *;
try ( %1 // )
%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
qed.

definition is_pointer_compat : block → region → bool ≝
λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].

(* Offsets into the block.  We allow integers like CompCert so that we have
   the option of extending blocks backwards. *)

(* CSC: why do we need this awful indirection? *)
record offset : Type[0] ≝ { offv : Z }.

definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).

lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
 whd in match eq_offset; /2/
qed.

definition shift_offset : ∀n. offset → BitVector n → offset ≝
  λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
  λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
  λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
  λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
definition sub_offset : ∀n. offset → offset → BitVector n ≝
  λn,x,y. bitvector_of_Z ? (offv x - offv y).
definition zero_offset ≝ mk_offset OZ.
definition lt_offset : offset → offset → bool ≝
  λx,y. Zltb (offv x) (offv y).

(*CSC: use this definition everywhere in Values.ma and Mem.ma. *)
record pointer: Type[0] ≝ {
   ptype: region;
   pblock: block;
   pok: pointer_compat pblock ptype;
   poff: offset
 }.

definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝
 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset n (poff p) i).

(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
 λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset_n n (poff p) i j).

definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
 λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i).

definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
 λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset_n n (poff p) i j).

definition eq_pointer: pointer → pointer → bool ≝
 λp1,p2.
  eq_region (ptype p1) (ptype p2) ∧ (eq_block (pblock p1) (pblock p2)) ∧
   eq_offset (poff p1) (poff p2).

lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true.
 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
qed.

lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1.
  (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1).
#P * #r0 #b0 #H0 * #o0 * #r1 #b1 #H1 * #o1
#Ptrue #Pfalse
whd in match (eq_pointer ??);
@eq_region_elim #reg_eq
[ @eq_block_elim #block_eq
  [ change with (eqZb ??) in match (eq_offset ??);
    @eqZb_elim #offset_eq
    [ destruct @Ptrue %
    ]
  ]
]
@Pfalse % #EQ destruct /2 by absurd/
qed.