1 | (* Type of values used in the dynamic semantics of the back-end intermediate |
---|
2 | languages, and the memory model for the whole compiler. Inspired by |
---|
3 | common/Values.ma, adapted from Compcert *) |
---|
4 | |
---|
5 | include "common/Pointers.ma". |
---|
6 | include "utilities/hide.ma". |
---|
7 | |
---|
8 | definition cpointer ≝ Σp.ptype p = Code. |
---|
9 | definition xpointer ≝ Σp.ptype p = XData. |
---|
10 | unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code). |
---|
11 | unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData). |
---|
12 | |
---|
13 | (* this is like a code pointer, but with unbounded offset. |
---|
14 | used only in the back-end, they become code pointers in LIN → ASM *) |
---|
15 | record program_counter : Type[0] ≝ |
---|
16 | { pc_block : Σb : block.block_region b = Code |
---|
17 | ; pc_offset : Pos |
---|
18 | }. |
---|
19 | |
---|
20 | definition eq_program_counter : program_counter → program_counter → bool ≝ |
---|
21 | λpc1,pc2.eq_block (pc_block pc1) (pc_block pc2) ∧ |
---|
22 | eqb (pc_offset pc1) (pc_offset pc2). |
---|
23 | |
---|
24 | lemma eq_program_counter_elim : ∀P:bool→Prop. |
---|
25 | ∀pc1,pc2.(pc1=pc2→P true)→(pc1≠pc2→P false)→P (eq_program_counter pc1 pc2). |
---|
26 | #P ** #bl1 #H1 #o1 ** #bl2 #H2 #o2 |
---|
27 | #Heq #Hneq whd in ⊢ (?%); |
---|
28 | @eq_block_elim #EQ1 |
---|
29 | [ @eqb_elim #EQ2 ] |
---|
30 | [ @Heq destruct % |
---|
31 | |*: @Hneq % #ABS destruct |
---|
32 | [ @(absurd ?? EQ2) | @(absurd ?? EQ1) ] % |
---|
33 | ] qed. |
---|
34 | |
---|
35 | lemma reflexive_eq_program_counter : ∀pc.eq_program_counter pc pc = true. |
---|
36 | ** #bl1 #H1 #o1 whd in ⊢ (??%?); >eq_block_b_b >eqb_n_n % qed. |
---|
37 | |
---|
38 | definition bitvector_from_pos : |
---|
39 | ∀n.Pos → BitVector n ≝ |
---|
40 | λn,p.bitvector_of_Z n (Zpred (pos p)). |
---|
41 | |
---|
42 | definition pos_from_bitvector : |
---|
43 | ∀n.BitVector n → Pos ≝ |
---|
44 | λn,v. |
---|
45 | match Zsucc (Z_of_unsigned_bitvector n v) |
---|
46 | return λx.Zsucc (Z_of_unsigned_bitvector n v) = x → ? |
---|
47 | with |
---|
48 | [ OZ ⇒ λprf.⊥ |
---|
49 | | pos x ⇒ λ_. x |
---|
50 | | neg x ⇒ λprf.⊥ |
---|
51 | ] (refl …). |
---|
52 | @hide_prf |
---|
53 | elim v in prf; |
---|
54 | [2,4: #n * #v #IH [2,4: assumption ]] normalize #ABS destruct(ABS) qed. |
---|
55 | |
---|
56 | definition cpointer_of_pc : program_counter → option cpointer ≝ |
---|
57 | λpc. |
---|
58 | let pc_off ≝ pc_offset pc in |
---|
59 | if leb pc_off (two_power_nat offset_size) then |
---|
60 | return «mk_pointer (pc_block pc) (mk_offset (bitvector_from_pos … pc_off)),?» |
---|
61 | else |
---|
62 | None ?. |
---|
63 | elim (pc_block pc) #bl #H @H qed. |
---|
64 | |
---|
65 | record part (*r: region*): Type[0] ≝ |
---|
66 | { part_no:> nat |
---|
67 | ; part_no_ok: part_no < size_pointer (*r*) |
---|
68 | }. |
---|
69 | |
---|
70 | definition part_from_sig : (Σn:ℕ.n<size_pointer) → part ≝ |
---|
71 | λn_sig : Σn.n<size_pointer.mk_part n_sig (pi2 … n_sig). |
---|
72 | |
---|
73 | coercion sig_to_part : ∀n_sig:Σn:ℕ.n<size_pointer.part ≝ |
---|
74 | part_from_sig on _n_sig:Σn.n<size_pointer to part. |
---|
75 | |
---|
76 | (* Byte-sized values used in the back-end. |
---|
77 | Values larger than a single Byte are represented via their parts. |
---|
78 | Values are either: |
---|
79 | - machine integers (Bytes) |
---|
80 | - parts of a pointer seen as a triple giving the representation of the |
---|
81 | pointer (in terms of the memory regions such a pointer could address), |
---|
82 | a memory address and an integer offset with respect to this address; |
---|
83 | - a null pointer: the region denotes the pointer size |
---|
84 | - the [BVundef] value denoting an arbitrary bit pattern, such as the |
---|
85 | value of an uninitialized variable |
---|
86 | - [BVXor] is a formal XOR between (possibly null) pointer parts |
---|
87 | - [BVnonzero] is any nonzero value |
---|
88 | *) |
---|
89 | |
---|
90 | inductive beval: Type[0] ≝ |
---|
91 | | BVundef: beval |
---|
92 | | BVnonzero: beval |
---|
93 | | BVXor: option pointer → option pointer → part → beval (* option pointer ≈ pointer + null *) |
---|
94 | | BVByte: Byte → beval |
---|
95 | | BVnull: (*∀r:region.*) part → beval |
---|
96 | | BVptr: pointer → part → beval |
---|
97 | | BVpc: program_counter → part → beval. (* only used in back end, needed to separate |
---|
98 | program counters that go in the stack from |
---|
99 | function pointers, as they are linked with |
---|
100 | different relations in some passes *) |
---|
101 | |
---|
102 | definition eq_bv_suffix : ∀n,m,p. |
---|
103 | BitVector (n + p) → BitVector (m + p) → bool ≝ |
---|
104 | λn,m,p,v1,v2. |
---|
105 | let b1 ≝ \snd (vsplit … v1) in |
---|
106 | let b2 ≝ \snd (vsplit … v2) in |
---|
107 | eq_bv … b1 b2. |
---|
108 | |
---|
109 | include alias "arithmetics/nat.ma". |
---|
110 | |
---|
111 | axiom CorruptedPointer: String. |
---|
112 | |
---|
113 | (* CSC: use vectors in place of lists? Or even better products of tuples |
---|
114 | (more easily pattern matchable in the finite case)? requires one more parameter *) |
---|
115 | definition pointer_of_bevals: list beval → res pointer ≝ |
---|
116 | λl. |
---|
117 | match l with |
---|
118 | [ nil ⇒ Error … [MSG CorruptedPointer] |
---|
119 | | cons bv1 tl ⇒ |
---|
120 | match tl with |
---|
121 | [ nil ⇒ Error … [MSG CorruptedPointer] |
---|
122 | | cons bv2 tl' ⇒ |
---|
123 | match tl' with |
---|
124 | [ cons _ _ ⇒ Error … [MSG CorruptedPointer] |
---|
125 | | nil ⇒ |
---|
126 | match bv1 with |
---|
127 | [ BVptr ptr1 p1 ⇒ |
---|
128 | match bv2 with |
---|
129 | [ BVptr ptr2 p2 ⇒ |
---|
130 | if eqb p1 0 ∧ eqb p2 1 ∧ eq_block (pblock ptr1) (pblock ptr2) ∧ |
---|
131 | eq_bv_suffix 8 8 8 (offv (poff ptr1)) (offv (poff ptr2)) |
---|
132 | then |
---|
133 | return ptr2 |
---|
134 | else Error … [MSG CorruptedPointer] |
---|
135 | | _ ⇒ Error … [MSG CorruptedPointer] |
---|
136 | ] |
---|
137 | | _ ⇒ Error … [MSG CorruptedPointer] |
---|
138 | ] |
---|
139 | ] |
---|
140 | ] |
---|
141 | ]. |
---|
142 | |
---|
143 | definition pc_of_bevals: list beval → res program_counter ≝ |
---|
144 | λl. |
---|
145 | match l with |
---|
146 | [ nil ⇒ Error … [MSG CorruptedPointer] |
---|
147 | | cons bv1 tl ⇒ |
---|
148 | match tl with |
---|
149 | [ nil ⇒ Error … [MSG CorruptedPointer] |
---|
150 | | cons bv2 tl' ⇒ |
---|
151 | match tl' with |
---|
152 | [ cons _ _ ⇒ Error … [MSG CorruptedPointer] |
---|
153 | | nil ⇒ |
---|
154 | match bv1 with |
---|
155 | [ BVpc ptr1 p1 ⇒ |
---|
156 | match bv2 with |
---|
157 | [ BVpc ptr2 p2 ⇒ |
---|
158 | if eqb p1 0 ∧ eqb p2 1 ∧ eq_program_counter ptr1 ptr2 then |
---|
159 | return ptr2 |
---|
160 | else Error … [MSG CorruptedPointer] |
---|
161 | | _ ⇒ Error … [MSG CorruptedPointer] |
---|
162 | ] |
---|
163 | | _ ⇒ Error … [MSG CorruptedPointer] |
---|
164 | ] |
---|
165 | ] |
---|
166 | ] |
---|
167 | ]. |
---|
168 | |
---|
169 | definition bevals_of_pointer ≝ |
---|
170 | λp:pointer. |
---|
171 | map ?? (λn_sig.BVptr p (part_from_sig n_sig)) (range_strong size_pointer). |
---|
172 | |
---|
173 | definition bevals_of_pc ≝ |
---|
174 | λp:program_counter. |
---|
175 | map ?? (λn_sig.BVpc p (part_from_sig n_sig)) (range_strong size_pointer). |
---|
176 | |
---|
177 | lemma pointer_of_bevals_bevals_of_pointer: |
---|
178 | ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p. |
---|
179 | #ptr |
---|
180 | whd in match (bevals_of_pointer ?); |
---|
181 | whd in ⊢ (??%?); |
---|
182 | >eq_block_b_b |
---|
183 | change with (eq_bv ???) in match (eq_bv_suffix ?????); |
---|
184 | >eq_bv_refl % |
---|
185 | qed. |
---|
186 | |
---|
187 | lemma pc_of_bevals_bevals_of_pc: |
---|
188 | ∀p. pc_of_bevals (bevals_of_pc p) = OK … p. |
---|
189 | #ptr |
---|
190 | whd in match (bevals_of_pc ?); |
---|
191 | whd in ⊢ (??%?); |
---|
192 | >reflexive_eq_program_counter |
---|
193 | % |
---|
194 | qed. |
---|
195 | |
---|
196 | (* CSC: move elsewhere *) |
---|
197 | (* CSC: Wrong data-type? Use products of products *) |
---|
198 | definition list_to_pair: ∀A:Type[0]. ∀l:list A. length … l = 2 → A × A. |
---|
199 | #A #l cases l [2: #a #tl cases tl [2: #b #tl' cases tl' [1: #_ @〈a,b〉 | #c #tl'']]] |
---|
200 | #abs normalize in abs; destruct |
---|
201 | qed. |
---|
202 | |
---|
203 | axiom NotATwoBytesPointer: String. |
---|
204 | |
---|
205 | (* Should fail if the address is not representable as a pair |
---|
206 | As we only have 16 bit addresses atm, it never fails *) |
---|
207 | definition beval_pair_of_pointer: pointer → (* res *) (beval × beval) ≝ |
---|
208 | λp.list_to_pair … (bevals_of_pointer p) (refl …). |
---|
209 | (* |
---|
210 | λp. match p with [ mk_pointer pty pbl pok poff ⇒ |
---|
211 | match pty with |
---|
212 | [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?) |
---|
213 | | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?) |
---|
214 | | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*) |
---|
215 | |
---|
216 | definition beval_pair_of_pc: program_counter → beval × beval ≝ |
---|
217 | λp. list_to_pair ? (bevals_of_pc p) (refl …). |
---|
218 | |
---|
219 | (* axiom NotACodePointer: String. |
---|
220 | definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝ |
---|
221 | λp. |
---|
222 | let 〈v1,v2〉 ≝ p in |
---|
223 | do p ← pointer_of_bevals [v1;v2] ; |
---|
224 | match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with |
---|
225 | [ Code ⇒ λE.OK ? (mk_Sig … p E) |
---|
226 | | _ ⇒ λ_.Error … [MSG NotACodePointer]] (refl …). *) |
---|
227 | |
---|
228 | axiom ValueNotABoolean: String. |
---|
229 | |
---|
230 | definition bool_of_beval: beval → res bool ≝ |
---|
231 | λv.match v with |
---|
232 | [ BVundef ⇒ Error … [MSG ValueNotABoolean] |
---|
233 | | BVXor _ _ _ ⇒ Error … [MSG ValueNotABoolean] (* even if in some cases we can |
---|
234 | tell the value, we will always |
---|
235 | call bool_of_beval after a |
---|
236 | series of XORs has been |
---|
237 | completed *) |
---|
238 | | BVpc _ _ ⇒ Error … [MSG ValueNotABoolean] (* we should never test on a pc *) |
---|
239 | | BVByte b ⇒ OK … (eq_bv … (zero …) b) |
---|
240 | | BVnull _ ⇒ OK … false |
---|
241 | | _ ⇒ OK ? true |
---|
242 | ]. |
---|
243 | |
---|
244 | definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *) |
---|
245 | λerr,b.match b with |
---|
246 | [ BVByte b ⇒ OK … b |
---|
247 | | _ ⇒ Error … [MSG err]]. |
---|
248 | |
---|
249 | axiom NotAnInt32Val: String. |
---|
250 | definition Word_of_list_beval: list beval → res int ≝ |
---|
251 | λl. |
---|
252 | let first_byte ≝ λl. |
---|
253 | match l with |
---|
254 | [ nil ⇒ Error ? [MSG NotAnInt32Val] |
---|
255 | | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in |
---|
256 | do 〈b1,l〉 ← first_byte l ; |
---|
257 | do 〈b2,l〉 ← first_byte l ; |
---|
258 | do 〈b3,l〉 ← first_byte l ; |
---|
259 | do 〈b4,l〉 ← first_byte l ; |
---|
260 | match l with |
---|
261 | [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1) |
---|
262 | | _ ⇒ Error ? [MSG NotAnInt32Val] ]. |
---|
263 | |
---|
264 | inductive bebit : Type[0] ≝ |
---|
265 | | BBbit : bool → bebit |
---|
266 | | BBundef : bebit |
---|
267 | | BBptrcarry : |
---|
268 | (* is add *) bool → pointer → ∀p : part.BitVector (8*S p) → bebit. |
---|
269 | |
---|
270 | definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *) |
---|
271 | λerr,b.match b with |
---|
272 | [ BBbit b ⇒ OK … b |
---|
273 | | _ ⇒ Error … [MSG err]]. |
---|