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 | (* Characterise the memory regions which the pointer representations can |
---|
46 | address. |
---|
47 | |
---|
48 | pointer_compat <block> <pointer representation> *) |
---|
49 | |
---|
50 | inductive pointer_compat : block → region → Prop ≝ |
---|
51 | | same_compat : ∀s,id. pointer_compat (mk_block s id) s |
---|
52 | | pxdata_compat : ∀id. pointer_compat (mk_block PData id) XData |
---|
53 | | universal_compat : ∀r,id. pointer_compat (mk_block r id) Any. |
---|
54 | |
---|
55 | lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p. |
---|
56 | * * #id *; |
---|
57 | try ( %1 // ) |
---|
58 | %2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct |
---|
59 | qed. |
---|
60 | |
---|
61 | definition is_pointer_compat : block → region → bool ≝ |
---|
62 | λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true | inr _ ⇒ false ]. |
---|
63 | |
---|
64 | (* Offsets into the block. We allow integers like CompCert so that we have |
---|
65 | the option of extending blocks backwards. *) |
---|
66 | |
---|
67 | (* CSC: why do we need this awful indirection? *) |
---|
68 | record offset : Type[0] ≝ { offv : Z }. |
---|
69 | |
---|
70 | definition eq_offset ≝ λx,y. eqZb (offv x) (offv y). |
---|
71 | |
---|
72 | lemma reflexive_eq_offset: ∀x. eq_offset x x = true. |
---|
73 | whd in match eq_offset; /2/ |
---|
74 | qed. |
---|
75 | |
---|
76 | definition shift_offset : ∀n. offset → BitVector n → offset ≝ |
---|
77 | λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i). |
---|
78 | (* A version of shift_offset_n for multiplied addresses which avoids overflow. *) |
---|
79 | definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝ |
---|
80 | λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)). |
---|
81 | definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝ |
---|
82 | λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i). |
---|
83 | definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝ |
---|
84 | λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)). |
---|
85 | definition sub_offset : ∀n. offset → offset → BitVector n ≝ |
---|
86 | λn,x,y. bitvector_of_Z ? (offv x - offv y). |
---|
87 | definition zero_offset ≝ mk_offset OZ. |
---|
88 | definition lt_offset : offset → offset → bool ≝ |
---|
89 | λx,y. Zltb (offv x) (offv y). |
---|
90 | |
---|
91 | (*CSC: use this definition everywhere in Values.ma and Mem.ma. *) |
---|
92 | record pointer: Type[0] ≝ { |
---|
93 | ptype: region; |
---|
94 | pblock: block; |
---|
95 | pok: pointer_compat pblock ptype; |
---|
96 | poff: offset |
---|
97 | }. |
---|
98 | |
---|
99 | definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝ |
---|
100 | λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset n (poff p) i). |
---|
101 | |
---|
102 | (* multiply shift by a nat (i.e., sizeof) without danger of overflow *) |
---|
103 | definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝ |
---|
104 | λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (shift_offset_n n (poff p) i j). |
---|
105 | |
---|
106 | definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝ |
---|
107 | λn,p,i. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset n (poff p) i). |
---|
108 | |
---|
109 | definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝ |
---|
110 | λn,p,i,j. mk_pointer (ptype p) (pblock p) (pok p) (neg_shift_offset_n n (poff p) i j). |
---|
111 | |
---|
112 | definition eq_pointer: pointer → pointer → bool ≝ |
---|
113 | λp1,p2. |
---|
114 | eq_region (ptype p1) (ptype p2) ∧ (eq_block (pblock p1) (pblock p2)) ∧ |
---|
115 | eq_offset (poff p1) (poff p2). |
---|
116 | |
---|
117 | lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true. |
---|
118 | #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset // |
---|
119 | qed. |
---|
120 | |
---|
121 | lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1. |
---|
122 | (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1). |
---|
123 | #P * #r0 #b0 #H0 * #o0 * #r1 #b1 #H1 * #o1 |
---|
124 | #Ptrue #Pfalse |
---|
125 | whd in match (eq_pointer ??); |
---|
126 | @eq_region_elim #reg_eq |
---|
127 | [ @eq_block_elim #block_eq |
---|
128 | [ change with (eqZb ??) in match (eq_offset ??); |
---|
129 | @eqZb_elim #offset_eq |
---|
130 | [ destruct @Ptrue % |
---|
131 | ] |
---|
132 | ] |
---|
133 | ] |
---|
134 | @Pfalse % #EQ destruct /2 by absurd/ |
---|
135 | qed. |
---|