source: src/common/Pointers.ma @ 1971

Last change on this file since 1971 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 5.0 KB
Line 
1include "ASM/BitVectorZ.ma".
2include "common/AST.ma". (* For the regions *)
3include "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
21record block : Type[0] ≝
22{ block_region : region
23; block_id : Z
24}.
25
26definition eq_block ≝
27λb1,b2.
28  eq_region (block_region b1) (block_region b2) ∧
29  eqZb (block_id b1) (block_id b2)
30.
31
32lemma 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
36whd 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
41lemma eq_block_b_b : ∀b. eq_block b b = true.
42* * #z whd in ⊢ (??%?); >eqZb_z_z @refl
43qed.
44
45(* Characterise the memory regions which the pointer representations can
46   address.
47
48   pointer_compat <block> <pointer representation> *)
49
50inductive 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
55lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
56* * #id *;
57try ( %1 // )
58%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
59qed.
60
61definition 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? *)
68record offset : Type[0] ≝ { offv : Z }.
69
70definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
71
72lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
73 whd in match eq_offset; /2/
74qed.
75
76definition 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. *)
79definition 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)).
81definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
82  λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
83definition 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)).
85definition sub_offset : ∀n. offset → offset → BitVector n ≝
86  λn,x,y. bitvector_of_Z ? (offv x - offv y).
87definition zero_offset ≝ mk_offset OZ.
88definition 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. *)
92record pointer: Type[0] ≝ {
93   ptype: region;
94   pblock: block;
95   pok: pointer_compat pblock ptype;
96   poff: offset
97 }.
98
99definition 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 *)
103definition 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
106definition 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
109definition 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
112definition 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
117lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true.
118 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
119qed.
120
121lemma 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
125whd 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/
135qed.
Note: See TracBrowser for help on using the repository browser.