source: src/common/FrontEndVal.ma @ 2286

Last change on this file since 2286 was 2286, checked in by tranquil, 7 years ago

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File size: 2.9 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
8let rec make_parts_aux (*r:region*) (n:nat) (H:lt n (size_pointer (*r*))) (tl:list (part (*r*))) on n : list (part (*r*)) ≝
9match 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/
14qed.
15
16definition make_parts : (*∀r:region.*) list (part (*r*)) ≝
17(*λr.*) make_parts_aux (*r*) (pred (size_pointer (*r*))) ? [ ].
18//
19qed.
20
21definition make_be_null : (*region →*) list beval ≝
22(*λr.*) map ?? (λp. BVnull (*r*) p) (make_parts (*r*)).
23
24let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝
25match 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
30definition 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  ⇒ make_be_null
37].
38cases sz in i ⊢ %; //
39qed.
40
41(* let rec check_be_ptr ptr n t on t ≝
42match 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
51let rec check_be_null  n t on t ≝
52match t with
53[ nil ⇒ eqb (size_pointer ) n
54| cons hd tl ⇒
55    match hd with
56    [ BVnull  pt ⇒  eqb (part_no  pt) n ∧ check_be_null  (S n) tl
57    | _ ⇒ false
58    ]
59].
60
61let rec build_integer (n:nat) (l:list beval) : option (BitVector (times n 8)) ≝
62match 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
76definition build_integer_val : typ → list beval → val ≝
77λt,l.
78match t with
79[ ASTint sz sg ⇒ option_map_def ?? (Vint sz) Vundef (build_integer (size_intsize sz) l)
80| _ ⇒ Vundef
81].
82
83definition 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    | BVnonzero ⇒ Vundef
90    | BVByte b ⇒ build_integer_val ty l
91    | BVptr _ _ _ ⇒
92      match pointer_of_bevals l with
93      [ OK ptr ⇒ Vptr ptr
94      | Error _ ⇒ Vundef
95      ]
96    | BVnull  pt ⇒ if eqb (part_no  pt) O ∧ check_be_null  (S O) t then Vnull  else Vundef
97    ]
98].
Note: See TracBrowser for help on using the repository browser.