source: src/common/Pointers.ma @ 2176

Last change on this file since 2176 was 2176, checked in by campbell, 7 years ago

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File size: 5.1 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(* 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
52inductive 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
57lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p.
58* * #id *;
59try ( %1 // )
60%2 % #H inversion H #e1 #e2 try #e3 try #e4 destruct
61qed.
62
63definition 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(* CSC: why do we need this awful indirection? *)
71record offset : Type[0] ≝ { offv : Z }.
72
73definition eq_offset ≝ λx,y. eqZb (offv x) (offv y).
74
75lemma reflexive_eq_offset: ∀x. eq_offset x x = true.
76 whd in match eq_offset; /2/
77qed.
78
79definition shift_offset : ∀n. offset → BitVector n → offset ≝
80  λn,o,i. mk_offset (offv o + Z_of_signed_bitvector ? i).
81(* A version of shift_offset_n for multiplied addresses which avoids overflow. *)
82definition shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
83  λn,o,i,j. mk_offset (offv o + (Z_of_nat i)*(Z_of_signed_bitvector ? j)).
84definition neg_shift_offset : ∀n. offset → BitVector n → offset ≝
85  λn,o,i. mk_offset (offv o - Z_of_signed_bitvector ? i).
86definition neg_shift_offset_n : ∀n. offset → nat → BitVector n → offset ≝
87  λn,o,i,j. mk_offset (offv o - (Z_of_nat i) * (Z_of_signed_bitvector ? j)).
88definition sub_offset : ∀n. offset → offset → BitVector n ≝
89  λn,x,y. bitvector_of_Z ? (offv x - offv y).
90definition zero_offset ≝ mk_offset OZ.
91definition lt_offset : offset → offset → bool ≝
92  λx,y. Zltb (offv x) (offv y).
93
94(*CSC: use this definition everywhere in Values.ma and Mem.ma. *)
95record pointer: Type[0] ≝ {
96(*   ptype: region;*)
97   pblock: block;
98(*   pok: pointer_compat pblock ptype;*)
99   poff: offset
100 }.
101
102(* As we don't have full memory space support, grab the region from the block
103   instead. *)
104definition ptype : pointer → region ≝ λp. block_region (pblock p).
105
106definition shift_pointer: ∀n. pointer → BitVector n → pointer ≝
107 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset n (poff p) i).
108
109(* multiply shift by a nat (i.e., sizeof) without danger of overflow *)
110definition shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
111 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (shift_offset_n n (poff p) i j).
112
113definition neg_shift_pointer: ∀n. pointer → BitVector n → pointer ≝
114 λn,p,i. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset n (poff p) i).
115
116definition neg_shift_pointer_n: ∀n. pointer → nat → BitVector n → pointer ≝
117 λn,p,i,j. mk_pointer (*ptype p*) (pblock p) (*pok p*) (neg_shift_offset_n n (poff p) i j).
118
119definition eq_pointer: pointer → pointer → bool ≝
120 λp1,p2.
121  (*eq_region (ptype p1) (ptype p2) ∧*) (eq_block (pblock p1) (pblock p2)) ∧
122   eq_offset (poff p1) (poff p2).
123
124lemma reflexive_eq_pointer: ∀p. eq_pointer p p = true.
125 #p whd in ⊢ (??%?); >eq_block_b_b >reflexive_eq_region >reflexive_eq_offset //
126qed.
127
128lemma eq_pointer_elim : ∀P : bool → Prop.∀p0,p1.
129  (p0 = p1 → P true) → (p0 ≠ p1 → P false) → P (eq_pointer p0 p1).
130#P * #b0 * #o0 * #b1 * #o1
131#Ptrue #Pfalse
132whd in match (eq_pointer ??);
133@eq_block_elim #block_eq
134[ change with (eqZb ??) in match (eq_offset ??);
135  @eqZb_elim #offset_eq
136  [ destruct @Ptrue %
137  ]
138]
139@Pfalse % #EQ destruct /2 by absurd/
140qed.
Note: See TracBrowser for help on using the repository browser.