(* Memory model used in the dynamic semantics of the back-end intermediate
   languages. Inspired by common/Mem.ma, adapted from Compcert *)

(* * This file develops the memory model that is used in the dynamic
  semantics of all the languages used in the compiler.
  It defines a type [mem] of memory states, the following 4 basic
  operations over memory states, and their properties:
- [load]: read a memory chunk at a given address;
- [store]: store a memory chunk at a given address;
- [alloc]: allocate a fresh memory block;
- [free]: invalidate a memory block.
*)

include "joint/BEValues.ma".
include "common/GenMem.ma".

definition bemem ≝ mem (mk_contentT beval BVundef).

axiom beloadv: ∀m:bemem. ∀ptr:pointer. option beval.
axiom bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem.

(* CSC: only pointers to XRAM or code memory ATM *)
definition address ≝ beval × beval.

definition eq_address: address → address → bool ≝
 λaddr1,addr2.
  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).

definition pointer_of_address: address → res pointer ≝
 λp. let 〈v1,v2〉 ≝ p in pointer_of_bevals [v1;v2].

(*CSC: for pointers of type Code and XData, the next function type can be
 strengthtened to never fail *)
definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.

definition addr_add: address → nat → res address ≝
 λaddr,n.
  do ptr ← pointer_of_address addr ;
  address_of_pointer (shift_pointer 16 ptr (bitvector_of_nat … n)).

definition addr_sub: address → nat → res address ≝
 λaddr,n.
  do ptr ← pointer_of_address addr ;
  address_of_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n)).