source: src/common/FrontEndVal.ma @ 1873

Last change on this file since 1873 was 1873, checked in by campbell, 8 years ago

Fix up earlier front-end value conversion work.

File size: 2.7 KB
Line 
1include "common/Values.ma".
2include "joint/BEValues.ma".
3include "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
9let rec make_parts (r:region) (n:nat) (H:le n (size_pointer r)) on n : list (part r) ≝
10match 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/
15qed.
16
17definition make_be_null : region → list beval ≝
18λr. map ?? (λp. BVnull r p) (make_parts r (size_pointer r) ?).
19//
20qed.
21
22let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝
23match 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
28definition fe_to_be_values : typ → val → list beval ≝
29λt,v. match v with
30[ Vundef ⇒ make_list ? BVundef (typesize t)
31| Vint sz i ⇒ map ?? (λb.BVByte b) (bytes_of_bitvector ? (i⌈bvint sz ↦ BitVector (size_intsize sz * 8)⌉))
32| Vfloat _ ⇒ make_list ? BVundef (typesize t) (* unsupported *)
33| Vptr ptr ⇒ bevals_of_pointer ptr
34| Vnull r ⇒ make_be_null r
35].
36cases sz in i ⊢ %; //
37qed.
38
39let rec check_be_ptr ptr n t on t ≝
40match 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
49let rec check_be_null r n t on t ≝
50match 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
59let rec build_integer (n:nat) (l:list beval) : option (BitVector (times n 8)) ≝
60match 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
74definition build_integer_val : typ → list beval → val ≝
75λt,l.
76match t with
77[ ASTint sz sg ⇒ option_map_def ?? (Vint sz) Vundef (build_integer (size_intsize sz) l)
78| _ ⇒ Vundef
79].
80
81definition be_to_fe_value : typ → list beval → val ≝
82λty,l. match l with
83[ nil ⇒ Vundef
84| cons h t ⇒
85    match h with
86    [ BVundef ⇒ Vundef
87    | BVByte b ⇒ build_integer_val ty l
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].
Note: See TracBrowser for help on using the repository browser.