Module AbMemSignature

Require Import Utf8 Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Cminor.
Require Import CFG.
Require Import Memory.
Require Export DLib.
Require Export LatticeSignatures.
Require Export AbEnvironment.
Require Export IntervalDomain.

Notation "m #1" := (fst m).
Notation "m #2" := (snd m).

Definition memory := (env * mem)%type.

Section GE.
  Variables (ge : genv).

  Definition Forget (x: positive) (E: ℘ memory) : ℘ memory :=
    fun m' => ∃ e, ∃ m, ∃ v,
      E (e, m) ∧ m' = (PTree.set x v e, m).

  Definition Assign (x: positive) (q: expr) (E: ℘ memory) : ℘ memory :=
    fun m' => ∃ e, ∃ m, ∃ sp, ∃ v,
      eval_expr ge (Vptr sp Int.zero) e m q v ∧
      E (e, m) ∧ m' = (PTree.set x v e, m).

  Definition Store (κ: memory_chunk) (addr: expr) (q: expr) (E: ℘ memory) : ℘ memory :=
    fun em' => let '(e,m') := em' in
      ∃ m, ∃ sp, ∃ vaddr, ∃ v,
      eval_expr ge (Vptr sp Int.zero) e m addr vaddr ∧
      eval_expr ge (Vptr sp Int.zero) e m q v ∧
      E (e, m) ∧ Mem.storev κ m vaddr v = Some m'.

  Definition Assume (q: expr) (E: ℘ memory) : ℘ memory :=
    fun m' => let '(e,m) := m' in
      ∃ sp, ∃ v,
      eval_expr ge (Vptr sp Int.zero) e m q v ∧
      Val.bool_of_val v true ∧
      E (e, m) ∧ m' = (e, m).
End GE.

Import Interval.

Unset Elimination Schemes.
Record mem_dom (t:Type) := {
  mem_adom: adom t (env * mem);
  range: t → (ident → sign_flag → itv+⊥)+⊥;
  range_sound: ∀ ab e m,
  (e,m) ∈ γ ab →
  ∃ r, range ab = NotBot r ∧
  ∀ x i,
    (e ! x = Some (Vint i) ∨ ∃ b, e ! x = Some (Vptr b i)) →
    i ∈ ints_in_range (r x);
  forget: ident → t → t;
  forget_sound: ∀ x ab, Forget x (γ ab) ⊆ γ (forget x ab);
  assign: ident → expr → t → t;
  assign_sound: ∀ ge x e ab, Assign ge x e (γ ab) ⊆ γ (assign x e ab);
  store: memory_chunk → expr → expr → t → t;
  store_sound: forall ge κ l r ab,
  Store ge κ l r (γ ab) ⊆ γ (store κ l r ab);
  assume: expr → t → t;
  assume_sound: ∀ ge e ab, Assume ge e (γ ab) ⊆ γ (assume e ab)
}.