(* 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 becontentT ≝ mk_contentT beval BVundef.
definition bemem ≝ mem becontentT.

(* This function should be moved to common/GenMem.ma and replaces in_bounds *)
definition do_if_in_bounds:
 ∀A:Type[0]. bemem → pointer → (block → block_contents becontentT → Z → A) → option A ≝
 λS,m,ptr,F.
  let b ≝ pblock ptr in
  if Zltb (block_id b) (nextblock … m) then
   let content ≝ blocks … m b in
   let off ≝ offv (poff ptr) in
   if andb (Zleb (low … content) off) (Zleb off (high … content)) then
    Some … (F b content off)
   else
    None ?
  else
   None ?.

definition beloadv: ∀m:bemem. ∀ptr:pointer. option beval ≝
 λm,ptr. do_if_in_bounds … m ptr (λb,content,off. contents … content off).

definition bestorev: ∀m:bemem. ∀ptr:pointer. beval → option bemem ≝
 λm,ptr,v. do_if_in_bounds … m ptr
  (λb,content,off.
    let contents ≝ update … off v (contents … content) in
    let content ≝ mk_block_contents (mk_contentT beval BVundef) (low … content) (high … content) contents in
    let blocks ≝ update_block … b content (blocks … m) in
     mk_mem … blocks (nextblock … m) (nextblock_pos … m)).

(* 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].
definition address_of_pointer: pointer → res address ≝ beval_pair_of_pointer.

definition code_pointer_of_address: address → res (Σp:pointer. ptype p = Code) ≝ code_pointer_of_beval_pair.
definition address_of_code_pointer: (Σp:pointer. ptype p = Code) → address ≝ beval_pair_of_code_pointer.

definition addr_add: address → nat → res address ≝
 λaddr,n.
  do ptr ← code_pointer_of_address addr ;
  OK … (address_of_code_pointer (shift_pointer 16 ptr (bitvector_of_nat … n))).
normalize cases ptr #p #E @E
qed.

definition addr_sub: address → nat → res address ≝
 λaddr,n.
  do ptr ← code_pointer_of_address addr ;
  OK … (address_of_code_pointer (neg_shift_pointer 16 ptr (bitvector_of_nat … n))).
normalize cases ptr #p #E @E
qed.