(**************************************************************************)
(*       ___                                                              *)
(*      ||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 "common/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. *)
definition store0 := empty.
definition store1block : mem × block ≝ alloc store0 0 4 Any.
definition store1 : mem ≝ fst ?? store1block.
definition block := snd ?? store1block.

(* write a value *)
definition store2 : mem.
  letin r ≝ (store Mint16unsigned store1 Any block 0 (Vint I16 (repr ? 1)));

  lapply (refl ? r); elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
  | #rr #_ @rr ] qed.

(* overwrite the first byte of the value *)
definition store3 : mem.
  letin r ≝ (store Mint8unsigned store1 Any block 0 (Vint I8 (repr ? 1)));

  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
  | #rr #_ @ rr ] qed.
  
(* The size checking rejects the read and gives us Some Vundef. *)
example vl_undef: load Mint16signed store3 Any block 0 = Some ? Vundef. @refl qed.

(* The read is successful and returns the value. *)
example vl_ok': load Mint8unsigned store3 Any block 0 = Some ? (Vint I8 (repr ? 1)). // qed.

(* NB: Double frees are allowed by the memory model (although not necessarily
       by the language). *)
definition store4 := free store3 block.
definition store5 : mem. letin r ≝ (free store3 block); whd in r @r qed.

(* No ordering is imposed on deallocation (even though alloc and free are only used for
   stack memory in the semantics. *)
definition storeA := empty.
definition storeBblkB := alloc storeA 0 4 Any.
definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 Any.
definition storeD := free (fst ?? storeCblkC) (snd ?? storeBblkB).
definition storeE : mem. letin r ≝ (free storeD (snd ?? storeCblkC)).
whd in r @r qed.

(* Access to the "object representation" (as the C standard puts it) is not specified. *)
definition storeI := empty.
definition storeIIblk := alloc storeA 0 4 Any.
definition storeIII : mem.
 letin r ≝ (store Mint32 (fst ?? storeIIblk) Any (snd ?? storeIIblk) 0 (Vint I32 (repr ? 1)));
  lapply (refl ? r) elim r in ⊢ (???% → ?) [ whd in ⊢ (??%? → ?) #H destruct
  | #rr #_ @rr ] qed.
definition byte := load Mint8unsigned storeIII Any (snd ?? storeIIblk) 0.
example byteundef: byte = Some ? Vundef. // qed. (* :( *)