1 | include "ASM/BitVectorZ.ma". |
---|
2 | include "common/AST.ma". (* For the regions *) |
---|
3 | include "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 | |
---|
21 | record block : Type[0] ≝ |
---|
22 | { block_region : region |
---|
23 | ; block_id : Z |
---|
24 | }. |
---|
25 | |
---|
26 | definition eq_block ≝ |
---|
27 | λb1,b2. |
---|
28 | eq_region (block_region b1) (block_region b2) ∧ |
---|
29 | eqZb (block_id b1) (block_id b2) |
---|
30 | . |
---|
31 | |
---|
32 | lemma 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 |
---|
36 | whd 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 | |
---|
41 | lemma eq_block_b_b : ∀b. eq_block b b = true. |
---|
42 | * * #z whd in ⊢ (??%?); >eqZb_z_z @refl |
---|
43 | qed. |
---|
44 | |
---|
45 | definition 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 | |
---|
51 | unification hint 0 ≔ ; D ≟ block_eq |
---|
52 | (*-----------------------------------------------------*)⊢ |
---|
53 | block ≡ 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 | |
---|
63 | inductive 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 | |
---|
68 | lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p. |
---|
69 | * * #id *; |
---|
70 | try ( %1 // ) |
---|
71 | %2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct |
---|
72 | qed. |
---|
73 | |
---|
74 | definition 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 | |
---|
81 | definition offset_size ≝ 8*size_pointer. |
---|
82 | |
---|
83 | (* CSC: why do we need this awful indirection? *) |
---|
84 | record offset : Type[0] ≝ { offv : BitVector offset_size }. |
---|
85 | |
---|
86 | definition eq_offset ≝ λx,y. eq_bv ? (offv x) (offv y). |
---|
87 | |
---|
88 | lemma reflexive_eq_offset: ∀x. eq_offset x x = true. |
---|
89 | whd in match eq_offset; /2/ |
---|
90 | qed. |
---|
91 | |
---|
92 | lemma 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 |
---|
95 | change with (eq_bv ???) in ⊢ (?%); |
---|
96 | @eq_bv_elim |
---|
97 | [ /2/ |
---|
98 | | * #FF @F % #E destruct /2/ |
---|
99 | ] qed. |
---|
100 | |
---|
101 | definition offset_of_Z : Z → offset ≝ |
---|
102 | λz. mk_offset (bitvector_of_Z … z). |
---|
103 | definition 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. *) |
---|
106 | definition 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))). |
---|
108 | definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝ |
---|
109 | λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)). |
---|
110 | definition 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))). |
---|
112 | definition sub_offset : ∀n. offset → offset → BitVector n ≝ |
---|
113 | λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)). |
---|
114 | definition zero_offset ≝ mk_offset (zero ?). |
---|
115 | definition 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. *) |
---|
119 | record 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. *) |
---|
128 | definition ptype : pointer → region ≝ λp. block_region (pblock p). |
---|
129 | |
---|
130 | definition 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 *) |
---|
134 | definition 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 | |
---|
137 | definition 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 | |
---|
140 | definition 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 | |
---|
143 | definition 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 | |
---|
148 | lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true. |
---|
149 | #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset // |
---|
150 | qed. |
---|
151 | |
---|
152 | lemma 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 |
---|
156 | whd 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/ |
---|
163 | qed. |
---|