source: src/common/Pointers.ma @ 2258

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.

definition block_eq : DeqSet ≝ mk_DeqSet block eq_block ?.
#x #y @eq_block_elim
[ #E destruct /2/
| * #NE % #E destruct cases (NE (refl ??))
] qed. 

(* This is only required for full 8051 memory spaces.

(* 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. *)

definition offset_size ≝ 8*size_pointer.

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

definition eq_offset ≝ λx,y. eq_bv ? (offv x) (offv y).

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

lemma eq_offset_elim : ∀P : bool → Prop.∀o1,o2.
  (o1 = o2 → P true) → (o1 ≠ o2 → P false) → P (eq_offset o1 o2).
#P * #o1 * #o2 #T #F
change with (eq_bv ???) in ⊢ (?%);
@eq_bv_elim
[ /2/
| * #FF @F % #E destruct /2/
] qed.

definition offset_of_Z : Z → offset ≝
λz. mk_offset (bitvector_of_Z … z).
definition shift_offset : ∀n. offset → BitVector n → offset ≝
  λn,o,i. mk_offset (addition_n ? (offv o) (sign_ext … 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 (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
  λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)).
definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
  λn,o,i,j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
definition sub_offset : ∀n. offset → offset → BitVector n ≝
  λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)).
definition zero_offset ≝ mk_offset (zero ?).
definition lt_offset : offset → offset → bool ≝
  λx,y. lt_u ? (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
 }.

(* As we don't have full memory space support, grab the region from the block
   instead. *)
definition ptype : pointer → region ≝ λp. block_region (pblock p).

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 * #b0 * #o0 * #b1 * #o1
#Ptrue #Pfalse
whd in match (eq_pointer ??);
@eq_block_elim #block_eq
[ @eq_offset_elim #offset_eq
  [ destruct @Ptrue %
  ]
]
@Pfalse % #EQ destruct /2 by absurd/
qed.