1 | include "ASM/BitVectorZ.ma". |
---|
2 | include "common/AST.ma". (* For the /s/regions/size_pointer/ *) |
---|
3 | include "utilities/extralib.ma". |
---|
4 | include "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 | |
---|
22 | record block : Type[0] ≝ |
---|
23 | { (* block_region : region ; *) |
---|
24 | block_id : Z |
---|
25 | }. |
---|
26 | |
---|
27 | definition block_region : block → region ≝ |
---|
28 | λb. |
---|
29 | if Zleb (block_id b) OZ then |
---|
30 | Code |
---|
31 | else |
---|
32 | XData. |
---|
33 | |
---|
34 | definition dummy_block_code : block ≝ |
---|
35 | mk_block OZ. |
---|
36 | |
---|
37 | definition eq_block ≝ |
---|
38 | λb1,b2. |
---|
39 | (* eq_region (block_region b1) (block_region b2) ∧*) |
---|
40 | eqZb (block_id b1) (block_id b2) |
---|
41 | . |
---|
42 | |
---|
43 | lemma 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 ] |
---|
50 | qed. |
---|
51 | (* |
---|
52 | #P * #r1 #i1 * #r2 #i2 #H1 #H2 |
---|
53 | whd 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 | |
---|
58 | lemma eq_block_b_b : ∀b. eq_block b b = true. |
---|
59 | * #z whd in ⊢ (??%?); >eqZb_z_z @refl |
---|
60 | qed. |
---|
61 | |
---|
62 | definition 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 | |
---|
68 | unification hint 0 ≔ ; D ≟ block_eq |
---|
69 | (*-----------------------------------------------------*)⊢ |
---|
70 | block ≡ 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 | |
---|
80 | inductive 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 | |
---|
85 | lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p. |
---|
86 | * * #id *; |
---|
87 | try ( %1 // ) |
---|
88 | %2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct |
---|
89 | qed. |
---|
90 | |
---|
91 | definition 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 | |
---|
98 | definition offset_size ≝ 8*size_pointer. |
---|
99 | |
---|
100 | (* CSC: why do we need this awful indirection? *) |
---|
101 | record offset : Type[0] ≝ { offv : BitVector offset_size }. |
---|
102 | |
---|
103 | definition eq_offset ≝ λx,y. eq_bv ? (offv x) (offv y). |
---|
104 | |
---|
105 | lemma reflexive_eq_offset: ∀x. eq_offset x x = true. |
---|
106 | whd in match eq_offset; /2/ |
---|
107 | qed. |
---|
108 | |
---|
109 | lemma 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 |
---|
112 | change with (eq_bv ???) in ⊢ (?%); |
---|
113 | @eq_bv_elim |
---|
114 | [ /2/ |
---|
115 | | * #FF @F % #E destruct /2/ |
---|
116 | ] qed. |
---|
117 | |
---|
118 | definition offset_of_Z : Z → offset ≝ |
---|
119 | λz. mk_offset (bitvector_of_Z … z). |
---|
120 | definition 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. *) |
---|
123 | definition 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]))). |
---|
125 | definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝ |
---|
126 | λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)). |
---|
127 | definition 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]))). |
---|
129 | definition sub_offset : ∀n. offset → offset → BitVector n ≝ |
---|
130 | λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)). |
---|
131 | definition zero_offset ≝ mk_offset (zero ?). |
---|
132 | definition 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. *) |
---|
136 | record 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. *) |
---|
145 | definition ptype : pointer → region ≝ λp. block_region (pblock p). |
---|
146 | |
---|
147 | definition 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 *) |
---|
151 | definition 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 | |
---|
154 | definition 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 | |
---|
157 | definition 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 | |
---|
160 | definition 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 | |
---|
165 | lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true. |
---|
166 | #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset // |
---|
167 | qed. |
---|
168 | |
---|
169 | lemma 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 |
---|
173 | whd 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/ |
---|
180 | qed. |
---|