Module BTL_SEsimplifyMem

Require Import Coqlib AST Values Integers Memory Maps.
Require Import RelationClasses.
Require Import OptionMonad.
Require Import Op.
Require Import BTL BTL_SEtheory BTL_SEsimuref.
Require Import ValueDomain.
Require Import Impure.ImpHCons.

Import SvalNotations.
Import ListNotations.
Local Open Scope option_monad_scope.
Local Open Scope lazy_bool_scope.


Section IsIndexedAddr.

  Definition is_indexed_addr (addr : addressing) (ofs : ptrofs) : Prop :=
    forall F V (genv: Globalenvs.Genv.t F V) (sp: val) (args: list val)
(rb : Values.block) (rofs : ptrofs),
    eval_addressing genv sp addr args = Some (Vptr rb rofs) <->
    exists bofs, args = Vptr rb bofs :: nil /\ rofs = Ptrofs.add bofs ofs.

  Local Obligation Tactic := simpl; intros.
  Local Transparent Archi.ptr64.
  Program Definition test_is_indexed (addr : addressing):
    {ofs : ptrofs | is_indexed_addr addr ofs} + {True} :=
    match addr with
    | Aindexed iofs => inleft (exist _ _ _)
    | _ => inright _
    end.
  Local Obligation Tactic := program_simpl.
  Solve All Obligations.
  Local Opaque Archi.ptr64.
  Global Opaque test_is_indexed.

  Lemma is_indexed_addr_case [addr ofs] (ADDR : is_indexed_addr addr ofs)
    [F V] (genv: Globalenvs.Genv.t F V) sp args
    :
    (exists b bofs,
      eval_addressing genv sp addr args = Some (Vptr b (Ptrofs.add bofs ofs)) /\
      args = Vptr b bofs :: nil) \/
    (match eval_addressing genv sp addr args with
     | Some (Vptr b rofs) => False
     | _ => True
     end).

  Lemma is_indexed_addr_eval [addr ofs] (ADDR : is_indexed_addr addr ofs)
    [F V] (genv: Globalenvs.Genv.t F V) sp b bofs:
    eval_addressing genv sp addr (Vptr b bofs :: nil) = Some (Vptr b (Ptrofs.add bofs ofs)).

End IsIndexedAddr.


Section LemmasMemory.

  Lemma store_success_iff chk m b ofs v:
    Mem.store chk m b ofs v <> None <-> Mem.valid_access m chk b ofs Writable.

  Lemma store_fail_iff chk m b ofs v:
    Mem.store chk m b ofs v = None <-> ~Mem.valid_access m chk b ofs Writable.
  
  Lemma load_success_iff chk m b ofs:
    Mem.load chk m b ofs <> None <-> Mem.valid_access m chk b ofs Readable.

  Lemma perm_store_iff [chunk m1 b ofs v m2]:
    Mem.store chunk m1 b ofs v = Some m2 ->
    forall (b' : Values.block) (ofs' : Z) (k : perm_kind) (p : permission),
    Mem.perm m1 b' ofs' k p <-> Mem.perm m2 b' ofs' k p.

  Lemma store_valid_access_iff [chunk m1 b ofs v m2]:
    Mem.store chunk m1 b ofs v = Some m2 ->
    forall (chunk' : memory_chunk) (b' : Values.block) (ofs' : Z) (p : permission),
    Mem.valid_access m1 chunk' b' ofs' p <-> Mem.valid_access m2 chunk' b' ofs' p.

  Section Equiv_on.

    Definition memct_t := PMap.t (ZMap.t memval).

    Definition memct_get (b : Values.block) (ofs : Z) (m : memct_t) : memval :=
      ZMap.get ofs (PMap.get b m).

    Definition is_Some [A] (x : option A) : bool :=
      match x with
      | Some _ => true
      | None => false
      end.

    Definition memct_get_str1 (b : Values.block) (m : memct_t) : bool :=
      is_Some (PTree.get b (snd m)).

    Definition memct_get_str2 (b : Values.block) (ofs: Z) (m : memct_t) : bool :=
       is_Some (PTree.get (ZIndexed.index ofs) (snd (PMap.get b m))).

    Definition memct_set (b : Values.block) (ofs : Z) (v : memval) (m : memct_t) : memct_t :=
      PMap.set b (ZMap.set ofs v (PMap.get b m)) m.


    Definition eq_on_frame : Type := (Values.block -> Prop) * (Values.block -> Z -> Prop).
    Variable P : eq_on_frame.
  
    Record memct_equiv_on (m0 m1 : memct_t) : Prop :=
      mk_memct_equiv_on {
        EQ_MCT1 : forall b, fst P b -> memct_get_str1 b m0 = memct_get_str1 b m1;
        EQ_MCT2 : forall b ofs, snd P b ofs -> memct_get b ofs m0 = memct_get b ofs m1 /\
                                               memct_get_str2 b ofs m0 = memct_get_str2 b ofs m1;
      }.

    Record mem_equiv_on (m0 m1 : mem) : Prop :=
      mk_mem_equiv_on {
        EQ_ACCESS : Mem.mem_access m0 = Mem.mem_access m1;
        EQ_NEXTBLOCK : Mem.nextblock m0 = Mem.nextblock m1;
        EQ_CTDEF : fst (Mem.mem_contents m0) = fst (Mem.mem_contents m1);
        EQ_CTNT : memct_equiv_on (Mem.mem_contents m0) (Mem.mem_contents m1);
    }.

    Lemma mem_equiv_on_perm [m0 m1] (E: mem_equiv_on m0 m1) b ofs k p:
      Mem.perm m0 b ofs k p <-> Mem.perm m1 b ofs k p.

    Lemma mem_equiv_on_valid_access [m0 m1] (E : mem_equiv_on m0 m1) chk b ofs p:
      Mem.valid_access m0 chk b ofs p <-> Mem.valid_access m1 chk b ofs p.

    Lemma mem_equiv_on_get [m0 m1] (E : mem_equiv_on m0 m1) b ofs
      (H : snd P b ofs):
      ZMap.get ofs (PMap.get b (Mem.mem_contents m0)) =
      ZMap.get ofs (PMap.get b (Mem.mem_contents m1)).

    Lemma zindex_surjective n:
      exists i, ZIndexed.index i = n.

    Lemma mem_equiv_on_all m0 m1
      (ALL1 : forall b, fst P b)
      (ALL2 : forall b i,snd P b i)
      (EQ : mem_equiv_on m0 m1):
      m0 = m1.

    Lemma load_equiv_on m0 m1 chk b ofs:
      mem_equiv_on m0 m1 ->
      (forall i, ofs <= i < ofs + size_chunk chk -> snd P b i) ->
      Mem.load chk m0 b ofs = Mem.load chk m1 b ofs.
  End Equiv_on.

  Local Instance memct_equiv_on_Equivalence {P}:
    Equivalence (memct_equiv_on P).

  Global Instance mem_equiv_on_Equivalence {P}:
    Equivalence (mem_equiv_on P).

  Lemma memct_equiv_on_weaken (P0 P1 : eq_on_frame) m0 m1
    (E : memct_equiv_on P0 m0 m1)
    (HP0 : forall b, fst P1 b -> fst P0 b)
    (HP1 : forall b p, snd P1 b p -> snd P0 b p):
    memct_equiv_on P1 m0 m1.

  Lemma mem_equiv_on_weaken (P0 P1 : eq_on_frame) m0 m1
    (E : mem_equiv_on P0 m0 m1)
    (HP0 : forall b, fst P1 b -> fst P0 b)
    (HP1 : forall b p, snd P1 b p -> snd P0 b p):
    mem_equiv_on P1 m0 m1.


  Lemma memct_gsspec b ofs v m0 b' ofs':
    memct_get b' ofs' (memct_set b ofs v m0) =
    if peq b' b && zeq ofs' ofs then v else memct_get b' ofs' m0.

  Lemma memct_gs1spec b ofs v m0 b':
    memct_get_str1 b' (memct_set b ofs v m0) =
    peq b' b || memct_get_str1 b' m0.
  
  Lemma memct_gs2spec b ofs v m0 b' ofs':
    memct_get_str2 b' ofs' (memct_set b ofs v m0) =
    (peq b' b && zeq ofs' ofs) || memct_get_str2 b' ofs' m0.

  Lemma memct_set_eq1 b ofs v m0:
    memct_equiv_on (fun b' => b' <> b, fun b' ofs' => ~(b' = b /\ ofs' = ofs)) m0 (memct_set b ofs v m0).

  Lemma memct_set_eq2 P b ofs v m0 m1
    (E : memct_equiv_on P m0 m1):
    memct_equiv_on
      (fun b' => fst P b' \/ b' = b, fun b' ofs' => snd P b' ofs' \/ (b' = b /\ ofs' = ofs))
      (memct_set b ofs v m0) (memct_set b ofs v m1).

  Fixpoint memct_setN (b : Values.block) (vl : list memval) (p : Z) (m : memct_t) : memct_t :=
    match vl with
    | nil => m
    | v :: vl => memct_setN b vl (p + 1) (memct_set b p v m)
    end.

  Lemma mem_setN_ctnt (m : memct_t) (mb : ZMap.t memval) (b : Values.block) (vl : list memval) (p : Z):
    PMap.set b (Mem.setN vl p mb) m = memct_setN b vl p (PMap.set b mb m).

  Lemma store_equiv_on1 chk m b p v m'
    (ST : Mem.store chk m b p v = Some m'):
    mem_equiv_on (fun b' => b' <> b, fun b' p' => ~(b' = b /\ p <= p' < p + size_chunk chk)) m m'.
  
  Lemma store_equiv_on2 P chk m0 m1 b p v m0' m1'
    (E : mem_equiv_on P m0 m1)
    (ST0 : Mem.store chk m0 b p v = Some m0')
    (ST1 : Mem.store chk m1 b p v = Some m1'):
    mem_equiv_on
      (fun b' => fst P b' \/ b' = b,
       fun b' p' => snd P b' p' \/ (b' = b /\ p <= p' < p + size_chunk chk)) m0' m1'.
  
  Lemma store_morph_equiv_on P chk m0 m1 b ofs v m0' m1'
    (E : mem_equiv_on P m0 m1)
    (ST0 : Mem.store chk m0 b ofs v = Some m0')
    (ST1 : Mem.store chk m1 b ofs v = Some m1'):
    mem_equiv_on P m0' m1'.

End LemmasMemory.

Record address := mk_addr {
  a_chunk: memory_chunk;
  a_addr: addressing;
  a_args: list_sval;
  a_aval: option aval
}.

Definition eval_address (ctx : iblock_common_context) (a : address): option (Values.block * ptrofs) :=
  SOME args <- eval_list_sval ctx (a_args a) IN
  SOME v <- eval_addressing (cge ctx) (csp ctx) (a_addr a) args IN
  ASSERT (if_Some_dec (a_aval a) (vmatch_dec (cbc ctx) v)) IN
  match v with
  | Vptr b o => Some (b, o)
  | _ => None
  end.

Section DisjointnessCriteria.


  Definition vaddr_disjoint (v0 : Values.block * ptrofs) (sz0 : Z)
                            (v1 : Values.block * ptrofs) (sz1 : Z): Prop :=
    let (b0, ofs0) := v0 in
    let (b1, ofs1) := v1 in
    b0 <> b1 \/
    Ptrofs.unsigned ofs0 + sz0 <= Ptrofs.unsigned ofs1 \/
    Ptrofs.unsigned ofs1 + sz1 <= Ptrofs.unsigned ofs0.

  Definition addr_disjoint (ctx : iblock_common_context) (a0 a1 : address) :=
    if_Some (eval_address ctx a0) (fun v0 =>
    if_Some (eval_address ctx a1) (fun v1 =>
    vaddr_disjoint v0 (size_chunk (a_chunk a0)) v1 (size_chunk (a_chunk a1)))).



  Let u := Ptrofs.unsigned.

  Definition offset_chunk_lt (ofs0 : ptrofs) (chk0 : memory_chunk)
                             (ofs1 : ptrofs) (chk1 : memory_chunk)
    := (u ofs0 + size_chunk chk0) <= u ofs1 /\
       (u ofs1 + size_chunk chk1) <= u ofs0 + Ptrofs.modulus.

  Definition offset_disjoint (ofs0 : ptrofs) (chk0 : memory_chunk)
                                   (ofs1 : ptrofs) (chk1 : memory_chunk)
    := offset_chunk_lt ofs0 chk0 ofs1 chk1 \/ offset_chunk_lt ofs1 chk1 ofs0 chk0.

  Lemma disjoint_interval_modulo (m : Z) (a b : Z) (al bl : Z) (c : Z):
    0 < m ->
    0 <= al -> 0 <= bl ->
    a + al <= b ->
    b + bl <= a + m ->
    (c + a) mod m + al <= (c + b) mod m \/ (c + b) mod m + bl <= (c + a) mod m.

  Lemma offset_disjoint_computed_addr (bo : Z) ofs0 chk0 ofs1 chk1:
    offset_disjoint ofs0 chk0 ofs1 chk1 ->
    (bo + u ofs0) mod Ptrofs.modulus + size_chunk chk0 <= (bo + u ofs1) mod Ptrofs.modulus \/
    (bo + u ofs1) mod Ptrofs.modulus + size_chunk chk1 <= (bo + u ofs0) mod Ptrofs.modulus.

  Lemma offset_disjoint_sound ctx a0 ofs0 a1 ofs1
    (A0: is_indexed_addr (a_addr a0) ofs0)
    (A1: is_indexed_addr (a_addr a1) ofs1)
    (B: list_sval_equiv ctx (a_args a0) (a_args a1))
    (D: offset_disjoint ofs0 (a_chunk a0) ofs1 (a_chunk a1)):
    addr_disjoint ctx a0 a1.


  Lemma abs_disjoint_sound ctx a0 a1 aa0 aa1
    (AA0 : a_aval a0 = Some aa0)
    (AA1 : a_aval a1 = Some aa1)
    (D: vdisjoint aa0 (size_chunk (a_chunk a0))
                  aa1 (size_chunk (a_chunk a1)) = true):
    addr_disjoint ctx a0 a1.

End DisjointnessCriteria.

Section RewritingRules.

Definition aSload sm trap chk addr args aaddr :=
  fSmayUndef_opt
    (SOME aaddr <- aaddr IN Some (fOKaddrMatch addr args aaddr))
    (fSload sm trap chk addr args).

Definition eval_aSload_def_0 trap (v : option val) : option val :=
  match v with
  | Some v => Some v
  | None =>
      match trap with
      | TRAP => None
      | NOTRAP => Some Vundef
      end
  end.

Definition eval_aSload_def_1 ctx trap chk addr args m :=
  SOME args <- eval_list_sval ctx args IN
  match trap with
  | TRAP =>
      SOME v <- eval_addressing (cge ctx) (csp ctx) addr args IN
      match v with
      | Vptr b ofs =>
          match Mem.load chk m b (Ptrofs.unsigned ofs) with
          | Some v => Some Vundef
          | None => None
          end
      | _ => None
      end
  | NOTRAP => Some Vundef
  end.

Lemma eval_aSload_def_1_unchanged ctx trap chk addr args m0 m1
  (EQ_PERM : forall b ofs k p, Mem.perm m0 b ofs k p <-> Mem.perm m1 b ofs k p):
  eval_aSload_def_1 ctx trap chk addr args m0 = eval_aSload_def_1 ctx trap chk addr args m1.

Lemma eval_aSload_eq ctx sm m trap chk addr args aaddr
  (MEM : eval_smem ctx sm = Some m):
  eval_sval ctx (aSload sm trap chk addr args aaddr) =
  match eval_address ctx (mk_addr chk addr args aaddr) with
  | Some (b, ofs) => eval_aSload_def_0 trap (Mem.load chk m b (Ptrofs.unsigned ofs))
  | None => eval_aSload_def_1 ctx trap chk addr args m
  end.

Definition eval_aSstore_eq ctx sm chk addr args sinfo sv hc:
  eval_smem ctx (Sstore sm chk addr args sinfo sv hc) =
  SOME a <- eval_address ctx (mk_addr chk addr args (store_aaddr sinfo)) IN
  let (b, ofs) := a in
  SOME v <- eval_sval ctx sv IN
  SOME m <- eval_smem ctx sm IN
  Mem.store chk m b (Ptrofs.unsigned ofs) v.

Lemma rewrite_load_store ctx (sm : smem) (trap : trapping_mode) (chk0 chk1 : memory_chunk)
  (addr0 addr1 : addressing) (args0 args1 : list_sval) (sv1 : sval) aaddr0 sinfo1 hc0
  (DJ : addr_disjoint ctx (mk_addr chk0 addr0 args0 aaddr0)
                          (mk_addr chk1 addr1 args1 (store_aaddr sinfo1))):
  let sm' := Sstore sm chk1 addr1 args1 sinfo1 sv1 hc0 in
  alive (eval_smem ctx sm') ->
  sval_equiv ctx
    (aSload sm' trap chk0 addr0 args0 aaddr0)
    (aSload sm trap chk0 addr0 args0 aaddr0).

Lemma rewrite_store_store ctx (sm : smem) (chk0 chk1 : memory_chunk)
  addr0 addr1 (args0 args1 : list_sval) (sv0 sv1 : sval) sinfo0 sinfo1 hc0 hc1
  (DJ : addr_disjoint ctx (mk_addr chk0 addr0 args0 (store_aaddr sinfo0))
                          (mk_addr chk1 addr1 args1 (store_aaddr sinfo1))):
  smem_equiv ctx
    (Sstore (Sstore sm chk1 addr1 args1 sinfo1 sv1 hc1) chk0 addr0 args0 sinfo0 sv0 hc0)
    (fSstore (fSstore sm chk0 addr0 args0 sinfo0 sv0 ) chk1 addr1 args1 sinfo1 sv1).


Inductive smem_equiv_on (P : eq_on_frame) (ctx : iblock_common_context) (sm0 sm1 : smem)
  : Prop
  := Smem_equiv_on m0 m1
      (EVAL_M0 : eval_smem ctx sm0 = Some m0)
      (EVAL_M1 : eval_smem ctx sm1 = Some m1)
      (EQ_ON : mem_equiv_on P m0 m1).

Lemma smem_equiv_on_refl P ctx sm:
  alive (eval_smem ctx sm) ->
  smem_equiv_on P ctx sm sm.

Global Instance smem_equiv_on_PER {P ctx}: PER (smem_equiv_on P ctx).

Lemma apply_store_smem_equiv_on P ctx sm0 sm1 chk addr sargs sinfo sv hc0 hc1:
  smem_equiv_on P ctx sm0 sm1 ->
  let sm0' := Sstore sm0 chk addr sargs sinfo sv hc0 in
  let sm1' := Sstore sm1 chk addr sargs sinfo sv hc1 in
  alive (eval_smem ctx sm0') ->
  smem_equiv_on P ctx sm0' sm1'.

Definition store_crange (ctx : iblock_common_context) (a : address) : eq_on_frame :=
  (fun b' => if_Some (eval_address ctx a) (fun av => let (b, _) := av in
                b' <> b),
   fun b' p' => if_Some (eval_address ctx a) (fun av => let (b, ofs) := av in
                let p := Ptrofs.unsigned ofs in
                ~(b' = b /\ p <= p' < p + size_chunk (a_chunk a)))).

Lemma rewrite_store_equiv_on ctx sm0 sm1 chk addr sargs sinfo sv hc0 hc1:
  let a := mk_addr chk addr sargs (store_aaddr sinfo) in
  let sm0' := Sstore sm0 chk addr sargs sinfo sv hc0 in
  let sm1' := Sstore sm1 chk addr sargs sinfo sv hc1 in
  smem_equiv_on (store_crange ctx a) ctx sm0 sm1 ->
  smem_equiv ctx sm0' sm1'.

Lemma remove_store_smem_equiv_on ctx sm0 chk addr sargs sinfo sv hc:
  let a := mk_addr chk addr sargs (store_aaddr sinfo) in
  let sm1 := Sstore sm0 chk addr sargs sinfo sv hc in
  forall (MALIVE: alive (eval_smem ctx sm1)),
  smem_equiv_on (store_crange ctx a) ctx sm0 sm1.

Definition load_range (ctx : iblock_common_context) (a : address) : eq_on_frame :=
  (fun _ => False,
   fun b i => exists ofs, eval_address ctx a = Some (b, ofs) /\
                          Ptrofs.unsigned ofs <= i < Ptrofs.unsigned ofs + size_chunk (a_chunk a)).

Lemma rewrite_load_equiv_on ctx sm0 sm1 trap chk addr sargs aaddr:
  let a := mk_addr chk addr sargs aaddr in
  smem_equiv_on (load_range ctx a) ctx sm0 sm1 ->
  sval_equiv ctx (aSload sm0 trap chk addr sargs aaddr)
                 (aSload sm1 trap chk addr sargs aaddr).

Lemma disjoint_store_smem_equiv_on ctx a sm0 chk addr sargs sinfo sv hc
  (DJ : addr_disjoint ctx a (mk_addr chk addr sargs (store_aaddr sinfo))):
  let range := load_range ctx a in
  let sm1 := Sstore sm0 chk addr sargs sinfo sv hc in
  forall (MALIVE: alive (eval_smem ctx sm1)),
  smem_equiv_on range ctx sm0 sm1.

End RewritingRules.


Section DisjointnessTest.


Program Definition test_offset_lt (ofs0 : ptrofs) (chk0 : memory_chunk)
                                  (ofs1 : ptrofs) (chk1 : memory_chunk)
  : {offset_chunk_lt ofs0 chk0 ofs1 chk1}+{True} :=
  if zle (Ptrofs.unsigned ofs0 + size_chunk chk0) (Ptrofs.unsigned ofs1)
  then if zle (Ptrofs.unsigned ofs1 + size_chunk chk1) (Ptrofs.unsigned ofs0 + Ptrofs.modulus)
  then left _ else right _ else right _.

Program Definition test_offset_disjoint (ofs0 : ptrofs) (chk0 : memory_chunk)
                                        (ofs1 : ptrofs) (chk1 : memory_chunk)
  : {offset_disjoint ofs0 chk0 ofs1 chk1}+{True} :=
  if test_offset_lt ofs0 chk0 ofs1 chk1
  then left _
  else if test_offset_lt ofs1 chk1 ofs0 chk0
  then left _ else right _.
Solve All Obligations with (unfold offset_disjoint; auto).

Definition pure_fast_eq [A] (h : A -> hashcode) (x0 x1 : A) : {x0 = x1}+{True}.

Program Definition test_disjoint_rel (a0 a1 : address)
  : {forall ctx, addr_disjoint ctx a0 a1}+{True} :=
  if pure_fast_eq list_sval_get_hid (a_args a0) (a_args a1)
  then
    match test_is_indexed (a_addr a0) with
    | inright _ => right _
    | inleft ofs0 =>
    match test_is_indexed (a_addr a1) with
    | inright _ => right _
    | inleft ofs1 => if test_offset_disjoint ofs0 (a_chunk a0) ofs1 (a_chunk a1)
                     then left _ else right _
    end end
  else right _.
Global Opaque test_disjoint_rel.


Definition test_disjoint_abs (a0 a1 : address)
  : {forall ctx, addr_disjoint ctx a0 a1}+{True}.
  case (a_aval a0) as [aa0|] eqn:AA0; [|right; trivial].
  case (a_aval a1) as [aa1|] eqn:AA1; [|right; trivial].
  case (vdisjoint aa0 (size_chunk (a_chunk a0))
                  aa1 (size_chunk (a_chunk a1))) eqn:D;
    [|right; trivial].
  left; intros.
  eapply abs_disjoint_sound; eauto.
Defined.