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