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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.