(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "Mem.ma".


(* The memory model stores the entire value regardless of whether it fits in
   the amount of memory used.  Fortunately, it checks the size of the memory
   access, preventing you reading back more information than the memory can
   store. *)
ndefinition store0 := empty.
ndefinition store1block : mem × block ≝ alloc store0 0 4.
ndefinition store1 : mem ≝ fst ?? store1block.
ndefinition block := snd ?? store1block.

(* write a value *)
ndefinition store2 : mem.
  nletin r ≝ (store Mint16unsigned store1 block 0 (Vint one));

  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
  ##| #rr; #_; napply rr ##] nqed.

(* overwrite the first byte of the value *)
ndefinition store3 : mem.
  nletin r ≝ (store Mint8unsigned store1 block 0 (Vint one));

  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
  ##| #rr; #_; napply rr ##] nqed.
  
(* The size checking rejects the read and gives us Some Vundef. *)
nremark vl_undef: load Mint16signed store3 block 0 = Some ? Vundef. //; nqed.

(* The read is successful and returns a signed version of the value. *)
nremark vl_ok': load Mint8unsigned store3 block 0 = Some ? (Vint (zero_ext 8 one)). //; nqed.

(* NB: Double frees are allowed by the memory model (although not necessarily
       by the language). *)
ndefinition store4 := free store3 block.
ndefinition store5 : mem. nletin r ≝ (free store3 block); nwhd in r; napply r; nqed.

(* No ordering is imposed on deallocation (even though alloc and free are only used for
   stack memory in the semantics. *)
ndefinition storeA := empty.
ndefinition storeBblkB := alloc storeA 0 4.
ndefinition storeCblkC := alloc (fst ?? storeBblkB) 0 8.
ndefinition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
ndefinition storeE : mem. nletin r ≝ (free storeD (snd ?? storeCblkC)).
nwhd in r; napply r; nqed.

(* Access to the "object representation" (as the C standard puts it) is not specified. *)
ndefinition storeI := empty.
ndefinition storeIIblk := alloc storeA 0 4.
ndefinition storeIII : mem.
 nletin r ≝ (store Mint32 (fst ?? storeIIblk) (snd ?? storeIIblk) 0 (Vint one));
  nlapply (refl ? r); nelim r in ⊢ (???% → ?);##[ nwhd in ⊢ (??%? → ?); #H; ndestruct;
  ##| #rr; #_; napply rr ##] nqed.
ndefinition byte := load Mint8unsigned storeIII (snd ?? storeIIblk) 0.
nremark byteundef: byte = Some ? Vundef. //; nqed. (* :( *)