Changeset 1874 for src/common


Ignore:
Timestamp:
Apr 4, 2012, 6:48:25 PM (8 years ago)
Author:
campbell
Message:

First cut at using back-end memory model throughout.
Note the correction to BEValues.

Location:
src/common
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/FrontEndVal.ma

    r1873 r1874  
    11include "common/Values.ma".
    22include "joint/BEValues.ma".
    3 include "common/Mem.ma".
    43
    54(* Transform between lists of "back-end" (i.e., byte by byte) values and the
     
    76   resolve the sizes; they are not strictly checked. *)
    87
    9 let rec make_parts (r:region) (n:nat) (H:le n (size_pointer r)) on n : list (part r) ≝
    10 match n return λn.le n ? → ? with
    11 [ O ⇒ λ_. [ ]
    12 | S m ⇒ λH'. mk_part r n H::(make_parts r m ?)
     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)
    1312] H.
    1413/2/
    1514qed.
    1615
    17 definition make_be_null : region → list beval
    18 λr. map ?? (λp. BVnull r p) (make_parts r (size_pointer r) ?).
     16definition make_parts : ∀r:region. list (part r)
     17λr. make_parts_aux r (pred (size_pointer r)) ? [ ].
    1918//
    2019qed.
     20
     21definition make_be_null : region → list beval ≝
     22λr. map ?? (λp. BVnull r p) (make_parts r).
    2123
    2224let rec bytes_of_bitvector (n:nat) (v:BitVector (times n 8)) : list Byte ≝
  • src/common/Globalenvs.ma

    r1872 r1874  
    404404     addresses of the memory region in question - here there are no real
    405405     pointers, so use the real region. *)
    406   let r ≝ block_region m b in
     406  let ptr ≝ mk_pointer (block_region ? m b) b ? (mk_offset p) in
    407407  match id with
    408   [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m r b p (Vint I8 n)
    409   | Init_int16 n ⇒ store (ASTint I16 Unsigned) m r b p (Vint I16 n)
    410   | Init_int32 n ⇒ store (ASTint I32 Unsigned) m r b p (Vint I32 n)
    411   | Init_float32 n ⇒ store (ASTfloat F32) m r b p (Vfloat n)
    412   | Init_float64 n ⇒ store (ASTfloat F64) m r b p (Vfloat n)
     408  [ Init_int8 n ⇒ store (ASTint I8 Unsigned) m ptr (Vint I8 n)
     409  | Init_int16 n ⇒ store (ASTint I16 Unsigned) m ptr (Vint I16 n)
     410  | Init_int32 n ⇒ store (ASTint I32 Unsigned) m ptr (Vint I32 n)
     411  | Init_float32 n ⇒ store (ASTfloat F32) m ptr (Vfloat n)
     412  | Init_float64 n ⇒ store (ASTfloat F64) m ptr (Vfloat n)
    413413  | Init_addrof r' symb ofs ⇒
    414414      match (*find_symbol ge symb*) symbols ? ge symb with
     
    416416      | Some b' ⇒
    417417        match pointer_compat_dec b' r' with
    418         [ inl pc ⇒ store (ASTptr r') m r b p (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
     418        [ inl pc ⇒ store (ASTptr r') m ptr (Vptr (mk_pointer r' b' pc (shift_offset ? zero_offset (repr I16 ofs))))
    419419        | inr _ ⇒ None ?
    420420        ]
    421421      ]
    422422  | Init_space n ⇒ Some ? m
    423   | Init_null r' ⇒ store (ASTptr r') m r b p (Vnull r')
     423  | Init_null r' ⇒ store (ASTptr r') m ptr (Vnull r')
    424424  ].
     425cases b //
     426qed.
    425427
    426428definition size_init_data : init_data → nat ≝
     
    471473*)
    472474
     475(* TODO: why doesn't this use alloc? *)
    473476definition alloc_init_data : mem → list init_data → region → mem × block ≝
    474477  λm,i_data,r.
    475   let b ≝ mk_block r (nextblock m) in
    476   〈mk_mem (update_block ? b
    477                  (mk_block_contents OZ (size_init_data_list i_data) (λ_.Undef))
    478                  (blocks m))
    479          (Zsucc (nextblock m))
    480          (succ_nextblock_pos m),
     478  let b ≝ mk_block r (nextblock ? m) in
     479  〈mk_mem ? (update_block ? b
     480                 (mk_block_contents becontentT OZ (size_init_data_list i_data) (λ_.BVundef))
     481                 (blocks ? m))
     482         (Zsucc (nextblock ? m))
     483         (succ_nextblock_pos ? m),
    481484   b〉.
    482485
     
    520523λF,V,init_info,p.
    521524  add_globals … init_info
    522    〈add_functs ? (empty …) (prog_funct F ? p), empty_mem
     525   〈add_functs ? (empty …) (prog_funct F ? p), empty_mem ?
    523526   (prog_vars ?? p).
    524527
  • src/common/Mem.ma

    r1872 r1874  
     1include "joint/BEMem.ma".
     2include "common/FrontEndVal.ma".
     3
     4definition mem ≝ bemem.
     5
     6let rec loadn (m:bemem) (ptr:pointer) (n:nat) on n : option (list beval) ≝
     7match n with
     8[ O ⇒ Some ? ([ ])
     9| S n' ⇒
     10  match beloadv m ptr with
     11  [ None ⇒ None ?
     12  | Some v ⇒ match loadn m (shift_pointer 2 ptr (bitvector_of_nat … 1)) n' with
     13             [ None ⇒ None ?
     14             | Some vs ⇒ Some ? (v::vs) ]
     15  ]
     16].
     17
     18definition load : typ → mem → pointer → option val ≝
     19λt,m,ptr.
     20  match loadn m ptr (typesize t) with
     21  [ None ⇒ None ?
     22  | Some vs ⇒ Some ? (be_to_fe_value t vs)
     23  ].
     24
     25let rec loadv (t:typ) (m:bemem) (addr:val) on addr : option val ≝
     26match addr with
     27[ Vptr ptr ⇒ load t m ptr
     28| _ ⇒ None ?
     29].
     30
     31let rec storen (m:bemem) (ptr:pointer) (vs:list beval) on vs : option bemem ≝
     32match vs with
     33[ nil ⇒ Some ? m
     34| cons v tl ⇒
     35  match bestorev m ptr v with
     36  [ None ⇒ None ?
     37  | Some m' ⇒ storen m' (shift_pointer 2 ptr (bitvector_of_nat … 1)) tl
     38  ]
     39].
     40
     41definition store : typ → bemem → pointer → val → option bemem ≝
     42λt,m,ptr,v. storen m ptr (fe_to_be_values t v).
     43
     44definition storev : typ → bemem → val → val → option bemem ≝
     45λt,m,addr,v.
     46  match addr with
     47  [ Vptr ptr ⇒ store t m ptr v
     48  | _ ⇒ None ? ].
     49
     50(* Only used by Clight semantics for pointer comparisons.  So in contrast to
     51   CompCert, we allow a pointer-to-one-off-the-end. *)
     52
     53definition valid_pointer : mem → pointer → bool ≝
     54λm,ptr. Zltb (block_id (pblock ptr)) (nextblock ? m) ∧
     55  Zleb (low_bound ? m (pblock ptr)) (offv (poff ptr)) ∧
     56  Zleb (offv (poff ptr)) (high_bound ? m (pblock ptr)).
     57
     58
     59(*
    160(* *********************************************************************)
    261(*                                                                     *)
     
    35183577qed.
    35193578*)
     3579*)
Note: See TracChangeset for help on using the changeset viewer.