source: src/Clight/test/memorymodel.ma

(**************************************************************************)
(*       ___                                                              *)
(*      ||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/FrontEndMem.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 × Σb:block.? ≝ alloc store0 0 4 XData.
definition store1 : mem ≝ fst ?? store1block.
definition block :block := pi1 … (snd ?? store1block).

(* write a value *)
definition store2 : mem.
  letin r ≝ (store (ASTint I16 Unsigned) store1 (mk_pointer block zero_offset) (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 (ASTint I8 Unsigned) store2 (mk_pointer block zero_offset) (Vint I8 (repr ? 1)))

  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
  | #rr #_ @ rr ] qed.
  
(* This is what happened under the original CompCert 1.6 ported memory model:
   The size checking rejects the read and gives us Some Vundef.
example vl_undef: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? Vundef. @refl qed.
*)
(* Now we do byte-wise values and get to see the altered integer. *)
example vl_changed: load (ASTint I16 Signed) store3 (mk_pointer block zero_offset) = Some ? (Vint I16 (repr ? 257)). @refl qed.

(* The read is successful and returns the value. *)
example vl_ok': load (ASTint I8 Unsigned) store3 (mk_pointer block zero_offset) = 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 XData.
definition storeCblkC := alloc (fst ?? storeBblkB) 0 8 XData.
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) was not specified,
   but can now split up integer values into bytes.  The front-end interface
   doesn't currently expose parts of pointers. *)
definition storeI := empty.
definition storeIIblk := alloc storeI 0 4 XData.
definition storeIII : mem.
 letin r ≝ (store (ASTint I32 Unsigned) (fst ?? storeIIblk) (mk_pointer (snd ?? storeIIblk) zero_offset) (Vint I32 (repr ? 1)));
  lapply (refl ? r) elim r in ⊢ (???% → ?); [ whd in ⊢ (??%? → ?); #H destruct
  | #rr #_ @rr ] qed.
definition byte := load (ASTint I8 Unsigned) storeIII (mk_pointer (snd ?? storeIIblk) zero_offset).
example byteundef: byte = Some ? (Vint I8 (repr ? 0)). // qed. (* :) *)