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 | (* 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 | |
---|
52 | inductive 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 | |
---|
57 | lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p. |
---|
58 | * * #id *; |
---|
59 | try ( %1 // ) |
---|
60 | %2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct |
---|
61 | qed. |
---|
62 | |
---|
63 | definition 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 | |
---|
70 | definition offset_size ≝ 8*size_pointer. |
---|
71 | |
---|
72 | (* CSC: why do we need this awful indirection? *) |
---|
73 | record offset : Type[0] ≝ { offv : BitVector offset_size }. |
---|
74 | |
---|
75 | definition eq_offset ≝ λx,y. eq_bv ? (offv x) (offv y). |
---|
76 | |
---|
77 | lemma reflexive_eq_offset: ∀x. eq_offset x x = true. |
---|
78 | whd in match eq_offset; /2/ |
---|
79 | qed. |
---|
80 | |
---|
81 | lemma 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 |
---|
84 | change with (eq_bv ???) in ⊢ (?%); |
---|
85 | @eq_bv_elim |
---|
86 | [ /2/ |
---|
87 | | * #FF @F % #E destruct /2/ |
---|
88 | ] qed. |
---|
89 | |
---|
90 | definition offset_of_Z : Z → offset ≝ |
---|
91 | λz. mk_offset (bitvector_of_Z … z). |
---|
92 | definition 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. *) |
---|
95 | definition 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))). |
---|
97 | definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝ |
---|
98 | λn,o,i. mk_offset (subtraction ? (offv o) (sign_ext … i)). |
---|
99 | definition 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))). |
---|
101 | definition sub_offset : ∀n. offset → offset → BitVector n ≝ |
---|
102 | λn,x,y. sign_ext … (subtraction ? (offv x) (offv y)). |
---|
103 | definition zero_offset ≝ mk_offset (zero ?). |
---|
104 | definition 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. *) |
---|
108 | record 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. *) |
---|
117 | definition ptype : pointer → region ≝ λp. block_region (pblock p). |
---|
118 | |
---|
119 | definition 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 *) |
---|
123 | definition 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 | |
---|
126 | definition 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 | |
---|
129 | definition 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 | |
---|
132 | definition 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 | |
---|
137 | lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true. |
---|
138 | #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset // |
---|
139 | qed. |
---|
140 | |
---|
141 | lemma 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 |
---|
145 | whd 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/ |
---|
152 | qed. |
---|