source: src/common/FrontEndVal.ma @ 2533

Last change on this file since 2533 was 2468, checked in by garnier, 7 years ago

Floats are gone from the front-end. Some trace amount might remain in RTL/RTLabs, but this should be easily fixable.
Also, work-in-progress in Clight/memoryInjections.ma

File size: 2.5 KB
Line 
1include "common/Values.ma".
2include "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
8definition make_parts : list part ≝
9  map ?? part_from_sig (range_strong size_pointer).
10
11definition make_be_null : (*region →*) list beval ≝
12(*λr.*) map ?? (λp. BVnull (*r*) p) (make_parts (*r*)).
13
14let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝
15match n return λn. BitVector (n*8) → ? with
16[ O ⇒ λ_. [ ]
17| S m ⇒ λv. let 〈h,t〉 ≝ vsplit ??? v in h::(bytes_of_bitvector m t)
18] v.
19
20definition fe_to_be_values : typ → val → list beval ≝
21λt,v. match v with
22[ Vundef ⇒ make_list ? BVundef (typesize t)
23| Vint sz i ⇒ map ?? (λb.BVByte b) (bytes_of_bitvector ? (i⌈bvint sz ↦ BitVector (size_intsize sz * 8)⌉))
24(*| Vfloat _ ⇒ make_list ? BVundef (typesize t) *) (* unsupported *)
25| Vptr ptr ⇒ bevals_of_pointer ptr
26| Vnull  ⇒ make_be_null
27].
28cases sz in i ⊢ %; //
29qed.
30
31(* let rec check_be_ptr ptr n t on t ≝
32match t with
33[ nil ⇒ eqb (size_pointer (*ptype ptr*)) n
34| cons hd tl ⇒
35    match hd with
36    [ BVptr ptr' pt ⇒ eq_pointer ptr ptr' ∧ eqb (part_no  pt) n ∧ check_be_ptr ptr (S n) tl
37    | _ ⇒ false
38    ]
39]. *)
40
41let rec check_be_null  n t on t ≝
42match t with
43[ nil ⇒ eqb (size_pointer ) n
44| cons hd tl ⇒
45    match hd with
46    [ BVnull  pt ⇒  eqb (part_no  pt) n ∧ check_be_null  (S n) tl
47    | _ ⇒ false
48    ]
49].
50
51let rec build_integer (n:nat) (l:list beval) : option (BitVector (times n 8)) ≝
52match n return λn. option (BitVector (n*8)) with
53[ O ⇒ match l with [ nil ⇒ Some ? [[ ]] | cons _ _ ⇒ None ? ]
54| S m ⇒
55    match l with
56    [ nil ⇒ None ?
57    | cons h t ⇒
58        match h with
59        [ BVByte b ⇒
60            option_map ?? (λtl. b @@ tl) (build_integer m t)
61        | _ ⇒ None ?
62        ]
63    ]
64].
65
66definition build_integer_val : typ → list beval → val ≝
67λt,l.
68match t with
69[ ASTint sz sg ⇒ option_map_def ?? (Vint sz) Vundef (build_integer (size_intsize sz) l)
70| _ ⇒ Vundef
71].
72
73definition be_to_fe_value : typ → list beval → val ≝
74λty,l. match l with
75[ nil ⇒ Vundef
76| cons h t ⇒
77    match h with
78    [ BVByte b ⇒ build_integer_val ty l
79    | BVptr _ _ ⇒
80      match pointer_of_bevals l with
81      [ OK ptr ⇒ Vptr ptr
82      | Error _ ⇒ Vundef
83      ]
84    | BVnull  pt ⇒ if eqb (part_no  pt) O ∧ check_be_null  (S O) t then Vnull  else Vundef
85    | _ ⇒ Vundef
86    ]
87].
Note: See TracBrowser for help on using the repository browser.