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 | record part (*r: region*): Type[0] ≝ |
---|
9 | { part_no:> nat |
---|
10 | ; part_no_ok: part_no < size_pointer (*r*) |
---|
11 | }. |
---|
12 | |
---|
13 | (* Byte-sized values used in the back-end. |
---|
14 | Values larger than a single Byte are represented via their parts. |
---|
15 | Values are either: |
---|
16 | - machine integers (Bytes) |
---|
17 | - parts of a pointer seen as a triple giving the representation of the |
---|
18 | pointer (in terms of the memory regions such a pointer could address), |
---|
19 | a memory address and an integer offset with respect to this address; |
---|
20 | - a null pointer: the region denotes the pointer size |
---|
21 | - the [BVundef] value denoting an arbitrary bit pattern, such as the |
---|
22 | value of an uninitialized variable |
---|
23 | - the [BVnonzero] value denoting an arbitrary but non-zero bit pattern, |
---|
24 | which arise in the RTLabs → RTL pass when translating equality comparisons |
---|
25 | between pointers (which get translated to multiple XORs between pointer |
---|
26 | parts). |
---|
27 | *) |
---|
28 | |
---|
29 | inductive beval: Type[0] ≝ |
---|
30 | | BVundef: beval |
---|
31 | | BVnonzero: beval |
---|
32 | | BVByte: Byte → beval |
---|
33 | | BVnull: (*∀r:region.*) part → beval |
---|
34 | | BVptr: block → ∀p:part.Vector Byte (S p) → beval. |
---|
35 | |
---|
36 | definition eq_beval: beval → beval → bool ≝ |
---|
37 | λv1,v2. |
---|
38 | match v1 with |
---|
39 | [ BVundef ⇒ match v2 with [ BVundef ⇒ true | _ ⇒ false ] |
---|
40 | | BVnonzero ⇒ match v2 with [ BVnonzero ⇒ true | _ ⇒ false ] |
---|
41 | | BVByte b1 ⇒ match v2 with [ BVByte b2 ⇒ eq_bv … b1 b2 | _ ⇒ false ] |
---|
42 | | BVnull p1 ⇒ match v2 with [ BVnull p2 ⇒ eqb p1 p2 | _ ⇒ false ] |
---|
43 | | BVptr b1 p1 o1 ⇒ |
---|
44 | match v2 with |
---|
45 | [ BVptr b2 p2 o2 ⇒ |
---|
46 | eq_block … b1 b2 ∧ eqb p1 p2 ∧ |
---|
47 | (* equivalent to equality if p1 = p2 *) |
---|
48 | vprefix … (eq_bv 8) o1 o2 |
---|
49 | | _ ⇒ false |
---|
50 | ] |
---|
51 | ]. |
---|
52 | |
---|
53 | include alias "arithmetics/nat.ma". |
---|
54 | |
---|
55 | axiom CorruptedPointer: String. |
---|
56 | |
---|
57 | let rec pointer_of_bevals_aux (b:block) (part: nat) (acc : BitVector (part*8)) |
---|
58 | (l: list beval) on l : res pointer ≝ |
---|
59 | match l with |
---|
60 | [ nil ⇒ |
---|
61 | If eqb part (size_pointer (*ptype p*)) then with prf do |
---|
62 | return mk_pointer b (mk_offset (acc⌈BitVector (part*8)↦?⌉)) |
---|
63 | else |
---|
64 | Error … [MSG CorruptedPointer] |
---|
65 | | cons v tl ⇒ |
---|
66 | match v with |
---|
67 | [ BVptr b' part' o' ⇒ |
---|
68 | let acc' ≝ vflatten … o' in |
---|
69 | if eq_block b b' ∧ |
---|
70 | eqb part part' ∧ |
---|
71 | vsuffix … eq_b acc acc' then |
---|
72 | pointer_of_bevals_aux b (S part') acc' tl |
---|
73 | else |
---|
74 | Error … [MSG CorruptedPointer] |
---|
75 | | _ ⇒ Error … [MSG CorruptedPointer] |
---|
76 | ] |
---|
77 | ]. |
---|
78 | @hide_prf |
---|
79 | >commutative_times_fast |
---|
80 | lapply prf @(eqb_elim part) #H * >H % qed. |
---|
81 | |
---|
82 | (* CSC: use vectors in place of lists? Or even better products of tuples |
---|
83 | (more easily pattern matchable in the finite case)? requires one more parameter *) |
---|
84 | definition pointer_of_bevals: list beval → res pointer ≝ |
---|
85 | λl. |
---|
86 | match l with |
---|
87 | [ nil ⇒ Error … [MSG CorruptedPointer] |
---|
88 | | cons he tl ⇒ |
---|
89 | match he with |
---|
90 | [ BVptr b part o ⇒ |
---|
91 | if eqb part 0 then |
---|
92 | pointer_of_bevals_aux b (S part) (vflatten … o) tl |
---|
93 | else Error … [MSG CorruptedPointer] |
---|
94 | | _ ⇒ Error … [MSG CorruptedPointer] |
---|
95 | ] |
---|
96 | ]. |
---|
97 | |
---|
98 | (* CSC: use vectors in place of lists? Or even better products of tuples |
---|
99 | (more easily pattern matchable in the finite case)? *) |
---|
100 | let rec bevals_of_pointer_aux (p:pointer) (part: nat) (n: nat) on n: n + part = size_pointer (*ptype p*) → list beval ≝ |
---|
101 | match n with |
---|
102 | [ O ⇒ λ_.[] |
---|
103 | | S m ⇒ λpr': S m + part = ?. |
---|
104 | let postfix ≝ rvsplit … (\snd (vsplit bool (m*8) (S part*8) (offv (poff p) ⌈BitVector ?↦?⌉))) in |
---|
105 | (BVptr (pblock p) (mk_part … part …) postfix)::bevals_of_pointer_aux p (S part) m ? |
---|
106 | ]. |
---|
107 | @hide_prf |
---|
108 | [3: change with (?*?) in match offset_size; |
---|
109 | <pr' >(commutative_times_fast ? 8) >(commutative_times_fast ? 8) |
---|
110 | <distributive_times_plus_fast <plus_n_Sm_fast % |
---|
111 | ] -postfix |
---|
112 | /3 by lt_plus_to_minus_r, lt_plus_to_lt_l/ qed. |
---|
113 | |
---|
114 | definition bevals_of_pointer: pointer → list beval ≝ |
---|
115 | λp. bevals_of_pointer_aux p 0 (size_pointer (*ptype p*)) …. |
---|
116 | @hide_prf @plus_n_O qed. |
---|
117 | |
---|
118 | lemma pointer_of_bevals_bevals_of_pointer: |
---|
119 | ∀p. pointer_of_bevals (bevals_of_pointer p) = OK … p. |
---|
120 | * #pbl * #voff |
---|
121 | whd in match (bevals_of_pointer ?); |
---|
122 | @vsplit_elim #pre #post |
---|
123 | normalize nodelta |
---|
124 | #EQ >EQ |
---|
125 | whd in match (bevals_of_pointer_aux ????); |
---|
126 | @vsplit_elim #pre' #post' |
---|
127 | normalize nodelta |
---|
128 | >(Vector_O … pre') #EQ' normalize in EQ'; <EQ' -pre' -post' |
---|
129 | whd in ⊢ (??%?); |
---|
130 | >eq_block_b_b >eqb_n_n |
---|
131 | >vflatten_rvsplit >vflatten_rvsplit |
---|
132 | >vsuffix_true |
---|
133 | [2: change with (bool_to_Prop (eq_bv ???)) >eq_bv_refl % ] |
---|
134 | normalize nodelta % |
---|
135 | qed. |
---|
136 | |
---|
137 | (* CSC: move elsewhere *) |
---|
138 | (* CSC: Wrong data-type? Use products of products *) |
---|
139 | definition list_to_pair: ∀A:Type[0]. ∀l:list A. length … l = 2 → A × A. |
---|
140 | #A #l cases l [2: #a #tl cases tl [2: #b #tl' cases tl' [1: #_ @〈a,b〉 | #c #tl'']]] |
---|
141 | #abs normalize in abs; destruct |
---|
142 | qed. |
---|
143 | |
---|
144 | axiom NotATwoBytesPointer: String. |
---|
145 | |
---|
146 | (* Fails if the address is not representable as a pair *) |
---|
147 | definition beval_pair_of_pointer: pointer → res (beval × beval) ≝ |
---|
148 | λp. OK … (list_to_pair … (bevals_of_pointer p) ?). |
---|
149 | (* |
---|
150 | λp. match p with [ mk_pointer pty pbl pok poff ⇒ |
---|
151 | match pty with |
---|
152 | [ XData ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer XData pbl pok poff)) ?) |
---|
153 | | Code ⇒ λpok. OK … (list_to_pair … (bevals_of_pointer (mk_pointer Code pbl pok poff)) ?) |
---|
154 | | _ ⇒ λ_. Error … [MSG NotATwoBytesPointer]] pok].*) |
---|
155 | % qed. |
---|
156 | |
---|
157 | definition beval_pair_of_code_pointer: (Σp:pointer. ptype p = Code) → beval × beval ≝ |
---|
158 | λp. list_to_pair ? (bevals_of_pointer p) ?. |
---|
159 | (* |
---|
160 | λp. match p return λp. ptype p = Code → ? with [ mk_pointer pty pbl pok poff ⇒ |
---|
161 | match pty return λpty. ? → pty = Code → ? with |
---|
162 | [ Code ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer Code pbl ? poff)) ? |
---|
163 | | _ ⇒ λpok'.λabs. ⊥] pok] ?. |
---|
164 | [@(pi2 … p) |7: // |8: %] destruct (abs)*) % |
---|
165 | qed. |
---|
166 | |
---|
167 | |
---|
168 | axiom NotACodePointer: String. |
---|
169 | definition code_pointer_of_beval_pair: beval × beval → res (Σp:pointer. ptype p = Code) ≝ |
---|
170 | λp. |
---|
171 | let 〈v1,v2〉 ≝ p in |
---|
172 | do p ← pointer_of_bevals [v1;v2] ; |
---|
173 | match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = Code) with |
---|
174 | [ Code ⇒ λE.OK ? (mk_Sig … p ?) |
---|
175 | | _ ⇒ λ_.Error … [MSG NotACodePointer]] ?. |
---|
176 | // qed. |
---|
177 | |
---|
178 | axiom ValueNotABoolean: String. |
---|
179 | |
---|
180 | definition bool_of_beval: beval → res bool ≝ |
---|
181 | λv.match v with |
---|
182 | [ BVundef ⇒ Error … [MSG ValueNotABoolean] |
---|
183 | | BVnonzero ⇒ OK … true |
---|
184 | | BVByte b ⇒ OK … (eq_bv … (zero …) b) |
---|
185 | | BVnull y ⇒ OK … false |
---|
186 | | BVptr p q o ⇒ OK ? true ]. |
---|
187 | |
---|
188 | definition Byte_of_val: String → beval → res Byte ≝ (*CSC: move elsewhere *) |
---|
189 | λerr,b.match b with |
---|
190 | [ BVByte b ⇒ OK … b |
---|
191 | | _ ⇒ Error … [MSG err]]. |
---|
192 | |
---|
193 | axiom NotAnInt32Val: String. |
---|
194 | definition Word_of_list_beval: list beval → res int ≝ |
---|
195 | λl. |
---|
196 | let first_byte ≝ λl. |
---|
197 | match l with |
---|
198 | [ nil ⇒ Error ? [MSG NotAnInt32Val] |
---|
199 | | cons hd tl ⇒ do b ← Byte_of_val NotAnInt32Val hd ; OK ? 〈b,tl〉 ] in |
---|
200 | do 〈b1,l〉 ← first_byte l ; |
---|
201 | do 〈b2,l〉 ← first_byte l ; |
---|
202 | do 〈b3,l〉 ← first_byte l ; |
---|
203 | do 〈b4,l〉 ← first_byte l ; |
---|
204 | match l with |
---|
205 | [ nil ⇒ OK ? (b4 @@ b3 @@ b2 @@ b1) |
---|
206 | | _ ⇒ Error ? [MSG NotAnInt32Val] ]. |
---|
207 | |
---|
208 | inductive bebit : Type[0] ≝ |
---|
209 | | BBbit : bool → bebit |
---|
210 | | BBundef : bebit |
---|
211 | | BBptrcarry : |
---|
212 | (* is add *) bool → block → ∀p : part.Vector Byte (S p) → Vector Byte (S p) → bebit. |
---|
213 | |
---|
214 | definition eq_bebit: bebit → bebit → bool ≝ |
---|
215 | λv1,v2. |
---|
216 | match v1 with |
---|
217 | [ BBundef ⇒ match v2 with [ BBundef ⇒ true | _ ⇒ false ] |
---|
218 | | BBbit b1 ⇒ match v2 with [ BBbit b2 ⇒ eq_b b1 b2 | _ ⇒ false ] |
---|
219 | | BBptrcarry is_add1 b1 p1 o1 by1 ⇒ |
---|
220 | match v2 with |
---|
221 | [ BBptrcarry is_add2 b2 p2 o2 by2 ⇒ |
---|
222 | eq_b is_add1 is_add2 ∧ eq_block … b1 b2 ∧ eqb p1 p2 ∧ |
---|
223 | (* equivalent to equality if p1 = p2 *) |
---|
224 | vprefix … (eq_bv 8) o1 o2 ∧ |
---|
225 | vprefix … (eq_bv 8) by1 by2 |
---|
226 | | _ ⇒ false |
---|
227 | ] |
---|
228 | ]. |
---|
229 | |
---|
230 | definition Bit_of_val: String → bebit → res Bit ≝ (*CSC: move elsewhere *) |
---|
231 | λerr,b.match b with |
---|
232 | [ BBbit b ⇒ OK … b |
---|
233 | | _ ⇒ Error … [MSG err]]. |
---|