source: src/common/FrontEndVal.ma @ 1651

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

Functions to translate between back-end and front-end values.

File size: 3.0 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 : memory_chunk → val → list beval ≝
29λc,v. match v with
30[ Vundef ⇒ make_list ? BVundef (size_chunk c)
31| Vint sz i ⇒ map ?? (λb.BVByte b) (bytes_of_bitvector ? (i⌈bvint sz ↦ BitVector (size_intsize sz * 8)⌉))
32| Vfloat _ ⇒ make_list ? BVundef (size_chunk c) (* 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 : memory_chunk → list beval → val ≝
75λc,l.
76match c with
77[ Mint8unsigned ⇒ option_map_def ?? (Vint I8) Vundef (build_integer 1 l)
78| Mint8signed ⇒ option_map_def ?? (Vint I8) Vundef (build_integer 1 l)
79| Mint16unsigned ⇒ option_map_def ?? (Vint I16) Vundef (build_integer 2 l)
80| Mint16signed ⇒ option_map_def ?? (Vint I16) Vundef (build_integer 2 l)
81| Mint32 ⇒ option_map_def ?? (Vint I32) Vundef (build_integer 4 l)
82| _ ⇒ Vundef
83].
84
85definition be_to_fe_value : memory_chunk → list beval → val ≝
86λc,l. match l with
87[ nil ⇒ Vundef
88| cons h t ⇒
89    match h with
90    [ BVundef ⇒ Vundef
91    | BVByte b ⇒ build_integer_val c l
92    | BVptr ptr pt ⇒ if eqb (part_no ? pt) O ∧ check_be_ptr ptr (S O) t then Vptr ptr else Vundef
93    | BVnull r pt ⇒ if eqb (part_no ? pt) O ∧ check_be_null r (S O) t then Vnull r else Vundef
94    ]
95].
Note: See TracBrowser for help on using the repository browser.