source: src/common/Pointers.ma @ 2530

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

Tidy up some ill-placed definitions.

File size: 5.9 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
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
51unification hint 0 ≔ ; D ≟ block_eq
52(*-----------------------------------------------------*)⊢
53block ≡ carr D.
54
55
56(* This is only required for full 8051 memory spaces.
57
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 ].
76*)
77
78(* Offsets into the block.  We allow integers like CompCert so that we have
79   the option of extending blocks backwards. *)
80
81definition offset_size ≝ 8*size_pointer.
82
83(* CSC: why do we need this awful indirection? *)
84record offset : Type[0] ≝ { offv : BitVector offset_size }.
85
86definition eq_offset ≝ λx,y. eq_bv ? (offv x) (offv y).
87
88lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
89 whd in match eq_offset; /2/
90qed.
91
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).
103definition shift_offset : ∀n. offset → BitVector n → offset ≝
104  λn,o,i. mk_offset (addition_n ? (offv o) (sign_ext … i)).
105(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
106definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
107  λn,o,i,j. mk_offset (addition_n ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
108definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
109  λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)).
110definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
111  λn,o,i,j. mk_offset (subtraction ? (offv o) (short_multiplication ? (bitvector_of_nat … i) (sign_ext … j))).
112definition sub_offset : ∀n. offset → offset → BitVector n ≝
113  λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)).
114definition zero_offset ≝ mk_offset (zero ?).
115definition lt_offset : offset → offset → bool ≝
116  λx,y. lt_u ? (offv x) (offv y).
117
118(*CSC: use this definition everywhere in Values.ma and Mem.ma. *)
119record pointer: Type[0] ≝ {
120(*   ptype: region;*)
121   pblock: block;
122(*   pok: pointer_compat pblock ptype;*)
123   poff: offset
124 }.
125
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
130definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝
131 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset n (poff p) i).
132
133(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
134definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
135 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) i j).
136
137definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
138 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset n (poff p) i).
139
140definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
141 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) i j).
142
143definition eq_pointer: pointer → pointer → bool ≝
144 λp1,p2.
145  (*eq_region (ptype p1) (ptype p2) ∧*) (eq_block (pblock p1) (pblock p2)) ∧
146   eq_offset (poff p1) (poff p2).
147
148lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true.
149 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
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).
154#P * #b0 * #o0 * #b1 * #o1
155#Ptrue #Pfalse
156whd in match (eq_pointer ??);
157@eq_block_elim #block_eq
158[ @eq_offset_elim #offset_eq
159  [ destruct @Ptrue %
160  ]
161]
162@Pfalse % #EQ destruct /2 by absurd/
163qed.
Note: See TracBrowser for help on using the repository browser.