[1551] | 1 | include "common/Values.ma". |
---|
| 2 | include "joint/BEValues.ma". |
---|
| 3 | include "common/Mem.ma". |
---|
| 4 | |
---|
| 5 | (* Transform between lists of "back-end" (i.e., byte by byte) values and the |
---|
| 6 | front-end values. Note that the memory_chunk arguments are mostly used to |
---|
| 7 | resolve the sizes; they are not strictly checked. *) |
---|
| 8 | |
---|
| 9 | let rec make_parts (r:region) (n:nat) (H:le n (size_pointer r)) on n : list (part r) ≝ |
---|
| 10 | match n return λn.le n ? → ? with |
---|
| 11 | [ O ⇒ λ_. [ ] |
---|
| 12 | | S m ⇒ λH'. mk_part r n H::(make_parts r m ?) |
---|
| 13 | ] H. |
---|
| 14 | /2/ |
---|
| 15 | qed. |
---|
| 16 | |
---|
| 17 | definition make_be_null : region → list beval ≝ |
---|
| 18 | λr. map ?? (λp. BVnull r p) (make_parts r (size_pointer r) ?). |
---|
| 19 | // |
---|
| 20 | qed. |
---|
| 21 | |
---|
| 22 | let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝ |
---|
| 23 | match n return λn. BitVector (n*8) → ? with |
---|
| 24 | [ O ⇒ λ_. [ ] |
---|
| 25 | | S m ⇒ λv. let 〈h,t〉 ≝ split ??? v in h::(bytes_of_bitvector m t) |
---|
| 26 | ] v. |
---|
| 27 | |
---|
[1873] | 28 | definition fe_to_be_values : typ → val → list beval ≝ |
---|
| 29 | λt,v. match v with |
---|
| 30 | [ Vundef ⇒ make_list ? BVundef (typesize t) |
---|
[1551] | 31 | | Vint sz i ⇒ map ?? (λb.BVByte b) (bytes_of_bitvector ? (i⌈bvint sz ↦ BitVector (size_intsize sz * 8)⌉)) |
---|
[1873] | 32 | | Vfloat _ ⇒ make_list ? BVundef (typesize t) (* unsupported *) |
---|
[1551] | 33 | | Vptr ptr ⇒ bevals_of_pointer ptr |
---|
| 34 | | Vnull r ⇒ make_be_null r |
---|
| 35 | ]. |
---|
| 36 | cases sz in i ⊢ %; // |
---|
| 37 | qed. |
---|
| 38 | |
---|
| 39 | let rec check_be_ptr ptr n t on t ≝ |
---|
| 40 | match t with |
---|
| 41 | [ nil ⇒ eqb (size_pointer (ptype ptr)) n |
---|
| 42 | | cons hd tl ⇒ |
---|
| 43 | match hd with |
---|
| 44 | [ BVptr ptr' pt ⇒ eq_pointer ptr ptr' ∧ eqb (part_no ? pt) n ∧ check_be_ptr ptr (S n) tl |
---|
| 45 | | _ ⇒ false |
---|
| 46 | ] |
---|
| 47 | ]. |
---|
| 48 | |
---|
| 49 | let rec check_be_null r n t on t ≝ |
---|
| 50 | match t with |
---|
| 51 | [ nil ⇒ eqb (size_pointer r) n |
---|
| 52 | | cons hd tl ⇒ |
---|
| 53 | match hd with |
---|
| 54 | [ BVnull r' pt ⇒ eq_region r r' ∧ eqb (part_no ? pt) n ∧ check_be_null r (S n) tl |
---|
| 55 | | _ ⇒ false |
---|
| 56 | ] |
---|
| 57 | ]. |
---|
| 58 | |
---|
| 59 | let rec build_integer (n:nat) (l:list beval) : option (BitVector (times n 8)) ≝ |
---|
| 60 | match n return λn. option (BitVector (n*8)) with |
---|
| 61 | [ O ⇒ match l with [ nil ⇒ Some ? [[ ]] | cons _ _ ⇒ None ? ] |
---|
| 62 | | S m ⇒ |
---|
| 63 | match l with |
---|
| 64 | [ nil ⇒ None ? |
---|
| 65 | | cons h t ⇒ |
---|
| 66 | match h with |
---|
| 67 | [ BVByte b ⇒ |
---|
| 68 | option_map ?? (λtl. b @@ tl) (build_integer m t) |
---|
| 69 | | _ ⇒ None ? |
---|
| 70 | ] |
---|
| 71 | ] |
---|
| 72 | ]. |
---|
| 73 | |
---|
[1873] | 74 | definition build_integer_val : typ → list beval → val ≝ |
---|
| 75 | λt,l. |
---|
| 76 | match t with |
---|
| 77 | [ ASTint sz sg ⇒ option_map_def ?? (Vint sz) Vundef (build_integer (size_intsize sz) l) |
---|
[1551] | 78 | | _ ⇒ Vundef |
---|
| 79 | ]. |
---|
| 80 | |
---|
[1873] | 81 | definition be_to_fe_value : typ → list beval → val ≝ |
---|
| 82 | λty,l. match l with |
---|
[1551] | 83 | [ nil ⇒ Vundef |
---|
| 84 | | cons h t ⇒ |
---|
| 85 | match h with |
---|
| 86 | [ BVundef ⇒ Vundef |
---|
[1873] | 87 | | BVByte b ⇒ build_integer_val ty l |
---|
[1551] | 88 | | BVptr ptr pt ⇒ if eqb (part_no ? pt) O ∧ check_be_ptr ptr (S O) t then Vptr ptr else Vundef |
---|
| 89 | | BVnull r pt ⇒ if eqb (part_no ? pt) O ∧ check_be_null r (S O) t then Vnull r else Vundef |
---|
| 90 | ] |
---|
| 91 | ]. |
---|