Ignore:
Timestamp:
Jul 12, 2012, 1:28:28 PM (8 years ago)
Author:
campbell
Message:

Remove memory spaces other than XData and Code; simplify pointers as a
result.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndVal.ma

    r2032 r2176  
    66   resolve the sizes; they are not strictly checked. *)
    77
    8 let rec make_parts_aux (r:region) (n:nat) (H:lt n (size_pointer r)) (tl:list (part r)) on n : list (part r) ≝
     8let rec make_parts_aux (*r:region*) (n:nat) (H:lt n (size_pointer (*r*))) (tl:list (part (*r*))) on n : list (part (*r*)) ≝
    99match 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)
     10[ O ⇒ λH'. (mk_part (*r*) O H')::tl
     11| S m ⇒ λH'. make_parts_aux (*r*) m ? ((mk_part (*r*) n H)::tl)
    1212] H.
    1313/2/
    1414qed.
    1515
    16 definition make_parts : ∀r:region. list (part r) ≝
    17 λr. make_parts_aux r (pred (size_pointer r)) ? [ ].
     16definition make_parts : (*∀r:region.*) list (part (*r*)) ≝
     17(*λr.*) make_parts_aux (*r*) (pred (size_pointer (*r*))) ? [ ].
    1818//
    1919qed.
    2020
    21 definition make_be_null : region → list beval ≝
    22 λr. map ?? (λp. BVnull r p) (make_parts r).
     21definition make_be_null : (*region →*) list beval ≝
     22(*λr.*) map ?? (λp. BVnull (*r*) p) (make_parts (*r*)).
    2323
    2424let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝
     
    3434| Vfloat _ ⇒ make_list ? BVundef (typesize t) (* unsupported *)
    3535| Vptr ptr ⇒ bevals_of_pointer ptr
    36 | Vnull r ⇒ make_be_null r
     36| Vnull  ⇒ make_be_null
    3737].
    3838cases sz in i ⊢ %; //
     
    4141let rec check_be_ptr ptr n t on t ≝
    4242match t with
    43 [ nil ⇒ eqb (size_pointer (ptype ptr)) n
     43[ nil ⇒ eqb (size_pointer (*ptype ptr*)) n
    4444| cons hd tl ⇒
    4545    match hd with
    46     [ BVptr ptr' pt ⇒ eq_pointer ptr ptr' ∧ eqb (part_no ? pt) n ∧ check_be_ptr ptr (S n) tl
     46    [ BVptr ptr' pt ⇒ eq_pointer ptr ptr' ∧ eqb (part_no pt) n ∧ check_be_ptr ptr (S n) tl
    4747    | _ ⇒ false
    4848    ]
    4949].
    5050
    51 let rec check_be_null r n t on t ≝
     51let rec check_be_null n t on t ≝
    5252match t with
    53 [ nil ⇒ eqb (size_pointer r) n
     53[ nil ⇒ eqb (size_pointer ) n
    5454| cons hd tl ⇒
    5555    match hd with
    56     [ BVnull r' pt ⇒ eq_region r r' ∧ eqb (part_no ? pt) n ∧ check_be_null r (S n) tl
     56    [ BVnull  pt ⇒  eqb (part_no  pt) n ∧ check_be_null (S n) tl
    5757    | _ ⇒ false
    5858    ]
     
    8888    [ BVundef ⇒ Vundef
    8989    | BVByte b ⇒ build_integer_val ty l
    90     | BVptr ptr pt ⇒ if eqb (part_no ? pt) O ∧ check_be_ptr ptr (S O) t then Vptr ptr else Vundef
    91     | BVnull r pt ⇒ if eqb (part_no ? pt) O ∧ check_be_null r (S O) t then Vnull r else Vundef
     90    | BVptr ptr pt ⇒ if eqb (part_no pt) O ∧ check_be_ptr ptr (S O) t then Vptr ptr else Vundef
     91    | BVnull  pt ⇒ if eqb (part_no  pt) O ∧ check_be_null  (S O) t then Vnull else Vundef
    9292    ]
    9393].
Note: See TracChangeset for help on using the changeset viewer.