include "common/GenMem.ma".
include "common/FrontEndVal.ma".

let rec loadn (m:mem) (ptr:pointer) (n:nat) on n : option (list beval) ≝
match n with
[ O ⇒ Some ? ([ ])
| S n' ⇒
  match beloadv m ptr with
  [ None ⇒ None ?
  | Some v ⇒ match loadn m (shift_pointer 2 ptr (bitvector_of_nat … 1)) n' with
             [ None ⇒ None ? 
             | Some vs ⇒ Some ? (v::vs) ]
  ]
].

definition load : typ → mem → pointer → option val ≝
λt,m,ptr.
  match loadn m ptr (typesize t) with
  [ None ⇒ None ?
  | Some vs ⇒ Some ? (be_to_fe_value t vs)
  ].

let rec loadv (t:typ) (m:mem) (addr:val) on addr : option val ≝
match addr with
[ Vptr ptr ⇒ load t m ptr
| _ ⇒ None ?
].

let rec storen (m:mem) (ptr:pointer) (vs:list beval) on vs : option mem ≝
match vs with
[ nil ⇒ Some ? m
| cons v tl ⇒
  match bestorev m ptr v with
  [ None ⇒ None ?
  | Some m' ⇒ storen m' (shift_pointer 2 ptr (bitvector_of_nat … 1)) tl
  ]
].

definition store : typ → mem → pointer → val → option mem ≝
λt,m,ptr,v. storen m ptr (fe_to_be_values t v).

definition storev : typ → mem → val → val → option mem ≝
λt,m,addr,v.
  match addr with
  [ Vptr ptr ⇒ store t m ptr v
  | _ ⇒ None ? ].

(* Only used by Clight semantics for pointer comparisons.  So in contrast to
   CompCert, we allow a pointer-to-one-off-the-end. *)

definition valid_pointer : mem → pointer → bool ≝
λm,ptr.
  let off ≝ Z_of_unsigned_bitvector … (offv (poff ptr)) in
  Zltb (block_id (pblock ptr)) (nextblock m) ∧
  Zleb (low_bound m (pblock ptr)) off ∧
  Zleb off (high_bound m (pblock ptr)).