Module AbMem

Require Import Coqlib Utf8.
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 Import Cells.
Require Import NCells.
Require Import IntOrPtrDomain.
Require Import AbNumDomain.
Require Import IntervalDomain.
Require Import AbEnvironment.

Section convert.
  Variable ge: CFG.genv.
  Variable sp: val.
  Variable m: mem.
  Variable e: env.

  Fixpoint convert (e:expr) : option (pexpr ident) :=
    match e with
      | Evar x => Some (PEvar x)
      | Econst c => Some (PEconst _ c)
      | Eunop o e =>
        match convert e with
          | None => None
          | Some e => Some (PEunop o e)
        end
      | Ebinop o e1 e2 =>
        match convert e1 with
          | None => None
          | Some e1 =>
            match convert e2 with
              | None => None
              | Some e2 => Some (PEbinop o e1 e2)
            end
        end
      | Eload chunk e => None
      | Econdition b r l =>
        match convert b, convert r, convert l with
          | Some b, Some r, Some l => Some (PEcond b r l)
          | _, _, _ => None
        end
    end.

  Import AbMemSignature.

  Definition compat (m:memory) (ρ:ident -> val) : Prop :=
    forall id,
      ρ id = match PTree.get id m#1 with
               | Some v => v
               | None => Vundef
             end.

  Lemma eval_expr_convert_expr : forall ρ,
    compat (e,m) ρ ->
    forall expr v,
      eval_expr ge sp e m expr v ->
      forall expr',
      convert expr = Some expr' ->
      eval_pexpr ge sp ρ expr' v.
Proof.
    induction 2; simpl; intros expr'.
    > intros T; inv T; constructor.
      generalize (H id); simpl; rewrite H0; auto.
    > intros T; inv T; constructor; auto.
    > case_eq (convert a1); try congruence; intros p Hp T; inv T.
      econstructor; auto.
    > case_eq (convert a1); try congruence; intros p Hp.
      case_eq (convert a2); try congruence; intros p2 Hp2 T; inv T.
      econstructor; eauto.
    > congruence.
    > case_eq (convert a1); try congruence; intros p Hp.
      case_eq (convert a2); try congruence; intros p2 Hp2.
      case_eq (convert a3); try congruence; intros p3 Hp3. intros X; injection X. intros. subst. clear X.
      econstructor; eauto; intros.
      apply IHeval_expr2. destruct b1; auto. inv H0; inv H1. congruence.
      destruct b1; auto. inv H0; inv H1. congruence.
      inv H0; intuition (econstructor). constructor. auto.
  Qed.

End convert.

Module Nconvert := Nconvert PTree.
Module TDom := Nconvert.TDom.
Module Eval := Cell2Val.Eval PTree.
Local Notation var := positive.

Definition nconvert (tp:(PTree.t IOP.t)+⊥) (e:pexpr var) : nexpr var :=
  Nconvert.nconvert _ tp (fun x => x) e.



Section abmem.
  Context {t_num : Type} {Val: Type} (D: num_dom Val).
  Variable dom_num: int_dom (t_num+⊥).

  Definition t := ((t_num+⊥)*((PTree.t IOP.t)+⊥))%type.

  Instance nadom : adom (t_num+⊥) (var->int) := id_adom.

  Definition compat_fun (v:val) : int :=
    match v with
      | Vptr _ i | Vint i => i
      | _ => Int.zero
    end.

  Section I.
  Import AbMemSignature.

  Definition gamma_mem (ab:t_num+⊥) (em: memory) :=
    let '(e,_) := em in
      ∃ ρ:var → int, ρ ∈ (γ ab) ∧
        (∀ x i, e ! x = Some i → Nconvert.ncompat i (ρ x)).

  Instance mem_nadom: adom (t_num+⊥) memory := {
    leb := leb;
    top := top;
    join := join;
    widen := widen;
    gamma := gamma_mem
  }.
Proof.
  > intros a1 a2 Ha (e,m) (ρ & H2 & H3).
    exists ρ; split; auto.
    exploit (@gamma_monotone _ _ nadom); eauto.
  > intros (ρ,C).
    exists (fun id =>
      match ρ ! id with
        | None => Int.zero
        | Some v => compat_fun v
      end).
    split; auto.
    intros x i ->.
    destruct i; constructor.
  > intros x y (e,m) [(r & H & R)|(r & H & R)]; exists r; intuition auto using @join_sound.
  Defined.

  Instance tpadom : adom ((PTree.t IOP.t)+⊥) (var->val) := Nconvert.tree_adom.

  Instance mem_tpadom: adom ((PTree.t IOP.t)+⊥) memory := {
    leb := leb;
    top := top;
    join := join;
    widen := widen;
    gamma := (fun ab m =>
        exists ρ,
          compat m ρ
          /\ γ ab ρ)
  }.
Proof.
  > intros a1 a2 Ha a (ρ & H2 & H3).
    exists ρ; split; auto.
    generalize (@gamma_monotone _ _ tpadom); eauto.
  > intros ρC.
    exists (fun id => match (ρC#1)!id with
                        | None => Vundef
                        | Some v => v
                      end); split; auto.
    intros id; auto.
  > intros x y a [(r & H & R)|(r & H & R)]; exists r; intuition auto using @join_sound.
  Defined.

  Instance adom : adom t memory := WProd.make mem_nadom mem_tpadom.

  End I.

  Definition forget (id:ident) (ab:t) : t :=
    let (nm,tp) := ab in
      (assign id (NEconst _ NOintunknown) nm,
       TDom.set tp id (NotBot IOP.Top)).

  Definition store (chunk:memory_chunk) (e a:expr) : t -> t :=
    fun ab => ab.

  Definition assign (id:ident) (e:expr) (ab:t) : t :=
    match convert e with
      | None => forget id ab
      | Some pe =>
        let (nm,tp) := ab in
          (assign id (nconvert tp pe) nm,
           TDom.set tp id (Eval.eval_expr IOP.adom tp pe))
    end.

  Definition assume (e:expr) (ab:t) : t :=
    match convert (Eunop Oboolval e) with
      | None => ab
      | Some pe =>
        let (nm,tp) := ab in
          (assume (nconvert tp pe) nm, tp)
    end.


  
  Definition itv (ab:t+⊥) : (ident-> sign_flag -> IntervalDomain.Interval.itv+⊥)+⊥ :=
    match ab with
      | Bot => Bot
      | NotBot (nm,tp) =>
        NotBot (fun x s => get_itv (NEvar x) nm s)
    end.

  Existing Instance adom.
  Lemma forget_correct: forall x ab e m v,
    γ ab (e, m) ->
    γ (forget x ab) (PTree.set x v e, m).
Proof.
    simpl.
    intros x (nm,tp) e m v ((ρ&R1&R2),H2).
    split.
    > exists (upd ρ x (compat_fun v)).
      split.
      > apply assign_correct; auto.
        constructor; constructor.
      > unfold upd.
        intros x0 i H.
        rewrite PTree.gsspec in H.
        destruct peq; subst; destruct eq_dec; intuition. inj.
        > destruct i; constructor.
    > destruct H2 as (ρC & T1 & T2).
      exists (fun y => if peq y x then v else ρC y).
      split.
      > intros id; simpl.
        rewrite PTree.gsspec; destruct peq.
        > congruence.
        > eauto.
      > apply TDom.gamma_set2; auto.
        simpl; constructor.
  Qed.

  Lemma assign_correct: forall (ge:CFG.genv) stp x a (ab:t) (e:env) (m:mem) v,
    γ ab (e, m) ->
    eval_expr ge (Vptr stp Int.zero) e m a v ->
    γ (assign x a ab) (PTree.set x v e, m).
Proof.
    intros.
    destruct ab as (nm, tp).
    unfold assign.
    case_eq (convert a); intros.
    > split.
      > destruct H as (T1 & T2).
        destruct T1 as (ρ & R1 & R2).
        destruct T2 as (ρC & R3 & R4).
        exploit eval_expr_convert_expr; eauto.
        intros He.
        edestruct (Nconvert.nconvert_correct ge stp _ ρC ρ tp R4 (fun x => x)) as (i & I1 & I2);
          eauto.
        > intros id.
          generalize (R3 id); simpl.
          case_eq (e!id); intros.
          > rewrite H2; eauto.
          > rewrite H2.
            constructor.
        > exists (upd ρ x i).
          split.
          > apply assign_correct; auto.
          > intros; unfold upd.
            simpl in H.
            rewrite PTree.gsspec in H.
            destruct peq; subst; destruct eq_dec; intuition. inj. auto.
      > destruct H as (T1 & T2).
        destruct T2 as (ρC & V1 & V2).
        exploit eval_expr_convert_expr; eauto.
        intros He.
        exists (fun y => if peq y x then v else ρC y).
        split.
        > intros id; simpl.
          rewrite PTree.gsspec; destruct peq; auto.
        > apply TDom.gamma_set2; auto.
          eapply Eval.eval_expr_correct; eauto.
    > apply forget_correct; auto.
  Qed.

  Lemma assume_correct: forall (ge:CFG.genv) stp a (ab:t) (e:env) (m:mem) v,
    γ ab (e, m) ->
    eval_expr ge (Vptr stp Int.zero) e m a v ->
    Val.bool_of_val v true ->
    γ (assume a ab) (e, m).
Proof.
    intros.
    assert (E1:eval_expr ge (Vptr stp Int.zero) e m (Eunop Oboolval a) (Val.boolval v)).
      econstructor; eauto.
    destruct ab as (nm, tp).
    unfold assume.
    case_eq (convert (Eunop Oboolval a)); intros; auto.
    split.
    > destruct H as (T1 & T2).
      destruct T1 as (ρ & R1 & R2).
      destruct T2 as (ρC & R3 & R4).
      exploit eval_expr_convert_expr; eauto.
      intros He.
      edestruct (Nconvert.nconvert_correct ge stp _ ρC ρ tp R4 (fun x => x)) as (i & I1 & I2);
        eauto.
      > intros id.
        generalize (R3 id); simpl.
        case_eq (e!id); intros.
        > rewrite H3; eauto.
        > rewrite H3.
          constructor.
      > exists ρ.
        split; auto.
        apply assume_correct; auto.
        replace Ntrue with i; auto.
        inv H1; simpl in I1.
        > rewrite Int.eq_false in I1; auto.
          inv I1; auto.
        > inv I1; auto.
    > destruct H as (T1 & T2).
      destruct T2 as (ρC & V1 & V2).
      exploit eval_expr_convert_expr; eauto.
      intros He.
      exists ρC.
      split; auto.
  Qed.

  Definition abmem : AbMemSignature.mem_dom (t+⊥).
    refine (AbMemSignature.Build_mem_dom (t+⊥)
      (lift_bot adom)
      itv _
      (fun x => botlift_fun1 (forget x)) _
      (fun x e => botlift_fun1 (assign x e)) _
      (fun κ a e => botlift_fun1 (store κ a e)) _
      (fun e => botlift_fun1 (assume e)) _
      ).
Proof.
      >
      intros [|(a,b)] e m; try (now intuition).
      intros ((ρ&A&B)&(ρ'&A'&B')).
      eexists. split. reflexivity.
      intros x i K.
      eapply get_itv_correct; eauto. econstructor; eauto.
      now destruct K as [K|(bb&K)]; specialize (B _ _ K); inv B.
      >
      intros x ab' (e,m') (e'&m&v&H&K). injection K; intros; subst; clear K.
      unfold botlift_fun1.
      case_eq ab'. intros ->. intuition.
      intros ab ->. simpl. apply forget_correct; auto.
      >
      intros ge x q ab' (e,m') (e'&m&sp&v&H&K&L). injection L; intros; subst; clear L.
      unfold botlift_fun1.
      case_eq ab'. intros ->. intuition.
      intros ab ->. simpl. eapply assign_correct; eauto.
      >
      intros ge κ l r ab' (e,m') (e'&m&v&H&K&L&M).
      unfold botlift_fun1.
      case_eq ab'. intros ->. intuition.
      intros (a,b) ->. unfold store. simpl in *. intuition.
      >
      intros ge q ab' (e,m') (sp&e'&m&v&H&_).
      unfold botlift_fun1.
      case_eq ab'. intros ->. intuition.
      intros ab ->. simpl. eapply assume_correct; eauto.
  Defined.

End abmem.

Import AbMemSignature.

Notation type_info := ((PTree.t IOP.t)+⊥).

Definition make {t:Type} : int_dom (t+⊥) -> mem_dom ((t+⊥ * type_info)+⊥) := abmem.
Generated by coq2html