source: src/common/Pointers.ma @ 2541

Last change on this file since 2541 was 2296, checked in by campbell, 7 years ago

Tidy up some ill-placed definitions.

File size: 5.9 KB
RevLine 
[1213]1include "ASM/BitVectorZ.ma".
2include "common/AST.ma". (* For the regions *)
3include "utilities/extralib.ma".
4
5
6(* To define pointers we need a few details about the memory model.
7
8   There are several kinds of pointers, which differ in which regions of
9   memory they address and the pointer's representation.
10   
11   Pointers are given as kind, block, offset triples, where a block identifies
12   some memory in a given region with an arbitrary concrete address.  A proof
13   is also required that the representation is suitable for the region the
14   memory resides in.  Note that blocks cannot extend out of a region (in
15   particular, a pdata pointer can address any byte in a pdata block - we never
16   need to switch to a larger xdata pointer).
17 *)
18
19(* blocks - represented by the region the memory resides in and a unique id *)
20
21record block : Type[0] ≝
22{ block_region : region
23; block_id : Z
24}.
25
26definition eq_block ≝
27λb1,b2.
28  eq_region (block_region b1) (block_region b2) ∧
29  eqZb (block_id b1) (block_id b2)
30.
31
32lemma eq_block_elim : ∀P:bool → Prop. ∀b1,b2.
33  (b1 = b2 → P true) → (b1 ≠ b2 → P false) →
34  P (eq_block b1 b2).
35#P * #r1 #i1 * #r2 #i2 #H1 #H2
[1516]36whd in ⊢ (?%); @eq_region_elim #H3
37[ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
[1213]38| @H2 % #E destruct elim H3 /2/
39] qed.
40
41lemma eq_block_b_b : ∀b. eq_block b b = true.
[1516]42* * #z whd in ⊢ (??%?); >eqZb_z_z @refl
[1213]43qed.
44
[2218]45definition block_eq : DeqSet ≝ mk_DeqSet block eq_block ?.
46#x #y @eq_block_elim
47[ #E destruct /2/
48| * #NE % #E destruct cases (NE (refl ??))
49] qed.
50
[2296]51unification hint 0 ≔ ; D ≟ block_eq
52(*-----------------------------------------------------*)⊢
53block ≡ carr D.
54
55
[2176]56(* This is only required for full 8051 memory spaces.
57
[1213]58(* Characterise the memory regions which the pointer representations can
59   address.
60
61   pointer_compat <block> <pointer representation> *)
62
63inductive pointer_compat : block → region → Prop ≝
64|        same_compat : ∀s,id. pointer_compat (mk_block s id) s
65|      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
66|   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
67
68lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
69* * #id *;
70try ( %1 // )
71%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
72qed.
73
74definition is_pointer_compat : block → region → bool ≝
75λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
[2176]76*)
[1213]77
78(* Offsets into the block.  We allow integers like CompCert so that we have
79   the option of extending blocks backwards. *)
80
[2185]81definition offset_size ≝ 8*size_pointer.
82
[1213]83(* CSC: why do we need this awful indirection? *)
[2185]84record offset : Type[0] ≝ { offv : BitVector offset_size }.
[1213]85
[2185]86definition eq_offset ≝ λx,y. eq_bv ? (offv x) (offv y).
[1213]87
88lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
[1516]89 whd in match eq_offset; /2/
[1213]90qed.
91
[2185]92lemma eq_offset_elim : ∀P : bool → Prop.∀o1,o2.
93  (o1 = o2 → P true) → (o1 ≠ o2 → P false) → P (eq_offset o1 o2).
94#P * #o1 * #o2 #T #F
95change with (eq_bv ???) in ⊢ (?%);
96@eq_bv_elim
97[ /2/
98| * #FF @F % #E destruct /2/
99] qed.
100
101definition offset_of_Z : Z → offset ≝
102λz. mk_offset (bitvector_of_Z … z).
[1213]103definition shift_offset : ∀n. offset → BitVector n → offset ≝
[2185]104  λn,o,i. mk_offset (addition_n ? (offv o) (sign_ext … i)).
[1213]105(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
106definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
[2185]107  λn,o,i,j. mk_offset (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
[1213]108definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
[2185]109  λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)).
[1213]110definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
[2185]111  λn,o,i,j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
[1213]112definition sub_offset : ∀n. offset → offset → BitVector n ≝
[2185]113  λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)).
114definition zero_offset ≝ mk_offset (zero ?).
[1213]115definition lt_offset : offset → offset → bool ≝
[2185]116  λx,y. lt_u ? (offv x) (offv y).
[1213]117
118(*CSC: use this definition everywhere in Values.ma and Mem.ma. *)
119record pointer: Type[0] ≝ {
[2176]120(*   ptype: region;*)
[1213]121   pblock: block;
[2176]122(*   pok: pointer_compat pblock ptype;*)
[1213]123   poff: offset
124 }.
125
[2176]126(* As we don't have full memory space support, grab the region from the block
127   instead. *)
128definition ptype : pointer → region ≝ λp. block_region (pblock p).
129
[1215]130definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝
[2176]131 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset n (poff p) i).
[1215]132
[1545]133(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
134definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
[2176]135 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) i j).
[1545]136
[1215]137definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
[2176]138 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset n (poff p) i).
[1215]139
[1545]140definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
[2176]141 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) i j).
[1545]142
[1213]143definition eq_pointer: pointer → pointer → bool ≝
144 λp1,p2.
[2176]145  (*eq_region (ptype p1) (ptype p2) ∧*) (eq_block (pblock p1) (pblock p2)) ∧
[1213]146   eq_offset (poff p1) (poff p2).
147
148lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true.
[1516]149 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
[1882]150qed.
151
152lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1.
153  (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1).
[2176]154#P * #b0 * #o0 * #b1 * #o1
[1882]155#Ptrue #Pfalse
156whd in match (eq_pointer ??);
[2176]157@eq_block_elim #block_eq
[2185]158[ @eq_offset_elim #offset_eq
[2176]159  [ destruct @Ptrue %
[1882]160  ]
161]
162@Pfalse % #EQ destruct /2 by absurd/
[2218]163qed.
Note: See TracBrowser for help on using the repository browser.