source: src/common/Pointers.ma @ 2185

Last change on this file since 2185 was 2185, checked in by campbell, 8 years ago

Use bitvectors for offsets.

File size: 5.6 KB
Line 
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
36whd in ⊢ (?%); @eq_region_elim #H3
37[ whd in ⊢ (?%); @eqZb_elim [ /2/ | * #NE @H2 % #E @NE destruct % ]
38| @H2 % #E destruct elim H3 /2/
39] qed.
40
41lemma eq_block_b_b : ∀b. eq_block b b = true.
42* * #z whd in ⊢ (??%?); >eqZb_z_z @refl
43qed.
44
45(* This is only required for full 8051 memory spaces.
46
47(* Characterise the memory regions which the pointer representations can
48   address.
49
50   pointer_compat <block> <pointer representation> *)
51
52inductive pointer_compat : block → region → Prop ≝
53|        same_compat : ∀s,id. pointer_compat (mk_block s id) s
54|      pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData
55|   universal_compat : ∀r,id. pointer_compat (mk_block r id) Any.
56
57lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
58* * #id *;
59try ( %1 // )
60%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
61qed.
62
63definition is_pointer_compat : block → region → bool ≝
64λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ].
65*)
66
67(* Offsets into the block.  We allow integers like CompCert so that we have
68   the option of extending blocks backwards. *)
69
70definition offset_size ≝ 8*size_pointer.
71
72(* CSC: why do we need this awful indirection? *)
73record offset : Type[0] ≝ { offv : BitVector offset_size }.
74
75definition eq_offset ≝ λx,y. eq_bv ? (offv x) (offv y).
76
77lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
78 whd in match eq_offset; /2/
79qed.
80
81lemma eq_offset_elim : ∀P : bool → Prop.∀o1,o2.
82  (o1 = o2 → P true) → (o1 ≠ o2 → P false) → P (eq_offset o1 o2).
83#P * #o1 * #o2 #T #F
84change with (eq_bv ???) in ⊢ (?%);
85@eq_bv_elim
86[ /2/
87| * #FF @F % #E destruct /2/
88] qed.
89
90definition offset_of_Z : Z → offset ≝
91λz. mk_offset (bitvector_of_Z … z).
92definition shift_offset : ∀n. offset → BitVector n → offset ≝
93  λn,o,i. mk_offset (addition_n ? (offv o) (sign_ext … i)).
94(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
95definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
96  λn,o,i,j. mk_offset (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
97definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
98  λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)).
99definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
100  λn,o,i,j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
101definition sub_offset : ∀n. offset → offset → BitVector n ≝
102  λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)).
103definition zero_offset ≝ mk_offset (zero ?).
104definition lt_offset : offset → offset → bool ≝
105  λx,y. lt_u ? (offv x) (offv y).
106
107(*CSC: use this definition everywhere in Values.ma and Mem.ma. *)
108record pointer: Type[0] ≝ {
109(*   ptype: region;*)
110   pblock: block;
111(*   pok: pointer_compat pblock ptype;*)
112   poff: offset
113 }.
114
115(* As we don't have full memory space support, grab the region from the block
116   instead. *)
117definition ptype : pointer → region ≝ λp. block_region (pblock p).
118
119definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝
120 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset n (poff p) i).
121
122(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
123definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
124 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) i j).
125
126definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
127 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset n (poff p) i).
128
129definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
130 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) i j).
131
132definition eq_pointer: pointer → pointer → bool ≝
133 λp1,p2.
134  (*eq_region (ptype p1) (ptype p2) ∧*) (eq_block (pblock p1) (pblock p2)) ∧
135   eq_offset (poff p1) (poff p2).
136
137lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true.
138 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
139qed.
140
141lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1.
142  (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1).
143#P * #b0 * #o0 * #b1 * #o1
144#Ptrue #Pfalse
145whd in match (eq_pointer ??);
146@eq_block_elim #block_eq
147[ @eq_offset_elim #offset_eq
148  [ destruct @Ptrue %
149  ]
150]
151@Pfalse % #EQ destruct /2 by absurd/
152qed.
Note: See TracBrowser for help on using the repository browser.