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