source: src/common/Pointers.ma @ 2624

Last change on this file since 2624 was 2608, checked in by garnier, 8 years ago

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

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