include "common/Values.ma". include "common/ByteValues.ma". (* Transform between lists of "back-end" (i.e., byte by byte) values and the front-end values. Note that the memory_chunk arguments are mostly used to resolve the sizes; they are not strictly checked. *) let rec make_parts_aux (*r:region*) (n:nat) (H:lt n (size_pointer (*r*))) (tl:list (part (*r*))) on n : list (part (*r*)) ≝ match n return λn.lt n ? → ? with [ O ⇒ λH'. (mk_part (*r*) O H')::tl | S m ⇒ λH'. make_parts_aux (*r*) m ? ((mk_part (*r*) n H)::tl) ] H. /2/ qed. definition make_parts : (*∀r:region.*) list (part (*r*)) ≝ (*λr.*) make_parts_aux (*r*) (pred (size_pointer (*r*))) ? [ ]. // qed. definition make_be_null : (*region →*) list beval ≝ (*λr.*) map ?? (λp. BVnull (*r*) p) (make_parts (*r*)). let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝ match n return λn. BitVector (n*8) → ? with [ O ⇒ λ_. [ ] | S m ⇒ λv. let 〈h,t〉 ≝ vsplit ??? v in h::(bytes_of_bitvector m t) ] v. definition fe_to_be_values : typ → val → list beval ≝ λt,v. match v with [ Vundef ⇒ make_list ? BVundef (typesize t) | Vint sz i ⇒ map ?? (λb.BVByte b) (bytes_of_bitvector ? (i⌈bvint sz ↦ BitVector (size_intsize sz * 8)⌉)) | Vfloat _ ⇒ make_list ? BVundef (typesize t) (* unsupported *) | Vptr ptr ⇒ bevals_of_pointer ptr | Vnull ⇒ make_be_null ]. cases sz in i ⊢ %; // qed. (* let rec check_be_ptr ptr n t on t ≝ match t with [ nil ⇒ eqb (size_pointer (*ptype ptr*)) n | cons hd tl ⇒ match hd with [ BVptr ptr' pt ⇒ eq_pointer ptr ptr' ∧ eqb (part_no pt) n ∧ check_be_ptr ptr (S n) tl | _ ⇒ false ] ]. *) let rec check_be_null n t on t ≝ match t with [ nil ⇒ eqb (size_pointer ) n | cons hd tl ⇒ match hd with [ BVnull pt ⇒ eqb (part_no pt) n ∧ check_be_null (S n) tl | _ ⇒ false ] ]. let rec build_integer (n:nat) (l:list beval) : option (BitVector (times n 8)) ≝ match n return λn. option (BitVector (n*8)) with [ O ⇒ match l with [ nil ⇒ Some ? [[ ]] | cons _ _ ⇒ None ? ] | S m ⇒ match l with [ nil ⇒ None ? | cons h t ⇒ match h with [ BVByte b ⇒ option_map ?? (λtl. b @@ tl) (build_integer m t) | _ ⇒ None ? ] ] ]. definition build_integer_val : typ → list beval → val ≝ λt,l. match t with [ ASTint sz sg ⇒ option_map_def ?? (Vint sz) Vundef (build_integer (size_intsize sz) l) | _ ⇒ Vundef ]. definition be_to_fe_value : typ → list beval → val ≝ λty,l. match l with [ nil ⇒ Vundef | cons h t ⇒ match h with [ BVundef ⇒ Vundef | BVnonzero ⇒ Vundef | BVByte b ⇒ build_integer_val ty l | BVptr _ _ _ ⇒ match pointer_of_bevals l with [ OK ptr ⇒ Vptr ptr | Error _ ⇒ Vundef ] | BVnull pt ⇒ if eqb (part_no pt) O ∧ check_be_null (S O) t then Vnull else Vundef ] ].