source: src/common/Pointers.ma @ 3367

Last change on this file since 3367 was 2641, checked in by piccolo, 7 years ago

defined dummy block code equals to 0

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