Module NCells

Require Import Coqlib Classical.
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 IntOrPtrDomain AbNumDomain.
Require Import AbEnvironment.

Module Nconvert(T:TREE).

  Module TDom := WPFun T.
  Instance tree_adom : Adom.adom TDom.t (T.elt->val) :=
    TDom.makebot (Cell2Val.val_adom IOP.adom).

  Module Eval := Cell2Val.Eval T.

  Section nconvert.
    Variable ge: CFG.genv.
    Variable sp: block.
    Variable var : Type.
    Variable ρC: T.elt -> val.
    Variable ρ: var -> int.
    Variable tp: @TDom.t IOP.t.
    Variable tp_correct: γ tp ρC.

    Variable elt2p: T.elt -> var.

    Definition convert_constant (cst: constant) : nconstant :=
      match cst with
        | Ointconst n => NOintconst n
        | Ofloatconst n => NOintunknown
        | Oaddrsymbol _ ofs
        | Oaddrstack ofs => NOintconst ofs
      end.

    Import IOP.

    Definition type_expr e :=
      match Eval.eval_expr IOP.adom tp e with
        | Bot => VI
        | NotBot x => x
      end.

    Fixpoint nconvert (e:pexpr T.elt) : nexpr var :=
      match e with
        | PEvar c => NEvar (elt2p c)
        | PEconst cst => NEconst _ (convert_constant cst)
        | PEunop op e =>
          match type_expr e with
            | Top => NEconst _ NOintunknown
            | tp =>
              match op with
                | Onegf | Oabsf | Osingleoffloat | Ofloatofint
                | Ofloatofintu | Ointoffloat | Ointuoffloat =>
                  NEconst _ NOintunknown
                | Onotbool =>
                  match tp with
                    | VP => NEconst _ (NOintconst Int.zero)
                    | VI => NEunop op (nconvert e)
                    | Top => NEconst _ NOintunknown
                  end
                | Oboolval =>
                  match tp with
                    | VP => NEconst _ (NOintconst Int.one)
                    | VI => NEunop op (nconvert e)
                    | Top => NEconst _ NOintunknown
                  end
                | _ => NEunop op (nconvert e)
              end
          end
        | PEbinop op e1 e2 =>
          match op with
            | Oadd
            | Osub
            | Omul
            | Odiv
            | Odivu
            | Omod
            | Omodu
            | Oand
            | Oor
            | Oxor
            | Ocmp _ => NEbinop op (nconvert e1) (nconvert e2)
            | Oshl
            | Oshr
            | Oshru
            | Ocmpu _ =>
              match type_expr e1, type_expr e2 with
                | VI, VI => NEbinop op (nconvert e1) (nconvert e2)
                | _, _ => NEconst _ NOintunknown
              end
            | Oaddf
            | Osubf
            | Omulf
            | Odivf
            | Ocmpf _ => NEconst _ NOintunknown
          end
        | PEcond b l r =>
          match type_expr b with
            | VI => NEcondition (nconvert b) (nconvert l) (nconvert r)
            | VP => NEcondition (NEconst _ (NOintconst Int.one)) (nconvert l) (nconvert r)
            | Top => NEconst _ NOintunknown
          end
      end.

    Inductive ncompat : val -> int -> Prop :=
    | ncompat_int: forall i, ncompat (Vint i) i
    | ncompat_ptr: forall b i, ncompat (Vptr b i) i
    | ncompat_vundef: forall i, ncompat Vundef i
    | ncompat_float: forall f i, ncompat (Vfloat f) i.

    Definition compat (ρC:T.elt -> val) (ρ:var -> int) : Prop :=
      forall c, ncompat (ρC c) (ρ (elt2p c)).


    Variable Hcompat: compat ρC ρ.
    Hint Constructors ncompat.
    Hint Constructors is_bool.

    Lemma compat_unknown: forall v,
      exists n : int,
        ncompat v n /\ eval_nexpr ρ (NEconst _ NOintunknown) n.

Proof.

      destruct v.
      exists Int.zero; repeat constructor.
      exists i; repeat constructor.
      exists Int.zero; repeat constructor.
      exists i; repeat constructor.
    Qed.

    Hint Resolve compat_unknown.

    Lemma eval_pexpr_type_expr_ptr_VI: forall a b i,
      eval_pexpr ge (Vptr sp Int.zero) ρC a (Vptr b i) ->
      type_expr a = VI -> False.

Proof.

      unfold type_expr; intros.
      exploit (@Eval.eval_expr_correct _ adom ge sp tp ρC a); eauto; intros Hg.
      destruct @Eval.eval_expr; subst; simpl in *; intuition.
    Qed.

    Lemma eval_pexpr_type_expr_int_VP: forall a i,
      eval_pexpr ge (Vptr sp Int.zero) ρC a (Vint i) ->
      type_expr a = VP -> False.

Proof.

      unfold type_expr; intros.
      exploit (@Eval.eval_expr_correct _ adom ge sp tp ρC a); eauto; intros Hg.
      destruct @Eval.eval_expr; subst; simpl in *; intuition.
    Qed.

    Lemma eval_pexpr_type_expr_float_VI: forall a f,
      eval_pexpr ge (Vptr sp Int.zero) ρC a (Vfloat f) ->
      type_expr a = VI -> False.

Proof.

      unfold type_expr; intros.
      exploit (@Eval.eval_expr_correct _ adom ge sp tp ρC a); eauto; intros Hg.
      destruct @Eval.eval_expr; subst; simpl in *; intuition.
    Qed.

    Lemma val_cmp_exists_int: forall c i1 i2,
      exists i,
        Val.cmp c (Vint i1) (Vint i2) = Vint i /\
        of_bool (Int.cmp c i1 i2) = i.

Proof.

      unfold Val.cmp, of_bool, Val.cmp_bool; intros.
      destruct Int.cmp; simpl; repeat econstructor.
    Qed.

    Lemma val_cmp_vundef: forall c v1 v2,
      (forall i1, v1 <> Vint i1) \/ (forall i2, v2 <> Vint i2) ->
      Val.cmp c v1 v2 = Vundef.

Proof.

      destruct v1; destruct v2; intros; try intuition congruence;
        destruct c; unfold Val.cmp, Val.of_optbool; simpl; auto.
    Qed.

    Lemma val_cmpu_exists_int: forall f c i1 i2,
      exists i,
        Val.cmpu f c (Vint i1) (Vint i2) = Vint i /\
        of_bool (Int.cmpu c i1 i2) = i.

Proof.

      unfold Val.cmpu, of_bool, Val.cmpu_bool; intros.
      destruct Int.cmpu; simpl; repeat econstructor.
    Qed.

    Lemma val_cmpu_vundef: forall f c v1 v2,
      v1 = Vundef \/ v2 = Vundef ->
      Val.cmpu f c v1 v2 = Vundef.

Proof.

      destruct 1; subst; auto.
      destruct v1; auto.
    Qed.

Lemma ncompat_Vundef: forall n, ncompat Vundef n.

Proof.

destruct n; constructor.
Qed.

Hint Resolve ncompat_Vundef.

Lemma ncompat_Vfloat: forall f, ncompat (Vfloat f) ( Int.zero).

Proof.

constructor.
Qed.

    Hint Resolve ncompat_Vfloat.

    Lemma match_eval_nexpr_intunknown: forall v,
      match v with
        | Vundef => exists n : int, eval_nexpr ρ (NEconst _ NOintunknown) n
        | Vint i1 => eval_nexpr ρ (NEconst _ NOintunknown) (i1)
        | Vfloat _ => exists n : int, eval_nexpr ρ (NEconst _ NOintunknown) n
        | Vptr _ i1 => eval_nexpr ρ (NEconst _ NOintunknown) (i1)
      end.

Proof.

      destruct v.
      exists (Int.zero); constructor; constructor.
      constructor; constructor.
      exists (Int.zero); constructor; constructor.
      constructor; constructor.
    Qed.

    Lemma ncompat_eval_nexpr: forall e v,
      match v with
        | Vint i => eval_nexpr ρ e i
        | Vptr b i => eval_nexpr ρ e i
        | Vundef => exists n, eval_nexpr ρ e n
        | Vfloat f => exists n, eval_nexpr ρ e n
      end ->
      exists n : int,
        ncompat v n /\ eval_nexpr ρ e n.

Proof.

      destruct v; try (econstructor; split; eauto; fail).
      destruct 1; eauto.
      destruct 1; eauto.
    Qed.

    Lemma nconvert_correct: forall e v,
      eval_pexpr ge (Vptr sp Int.zero) ρC e v ->
      exists n, ncompat v n /\ eval_nexpr ρ (nconvert e) n.

Proof.

      induction 1; simpl.
      > exists (ρ (elt2p c)); split; subst; auto.
      constructor; auto.
      > destruct cst; inv H;
        (econstructor; split; [idtac|econstructor;econstructor]); auto.
      > destruct Genv.find_symbol; constructor.
      > rewrite Int.add_zero_l.
      constructor.
      > destruct IHeval_pexpr as (n & E1 & E2); auto.
      destruct (classic (type_expr a1 = Top)) as [Ht|Ht].
      > rewrite Ht.
      destruct op; inv E1; inv H0;
        try match goal with [|-context[Int.eq]] => destruct Int.eq; simpl end;
          try match goal with [id:context[Float.intoffloat]|-_] =>
                destruct Float.intoffloat; inv id end;
          try match goal with [id:context[Float.intuoffloat]|-_] =>
                destruct Float.intuoffloat; inv id end; auto.
      > exploit (@Eval.eval_expr_correct _ adom ge sp tp ρC a1); eauto; intros Hg.
      assert (Hg1: γ (type_expr a1) v1).
        unfold type_expr.
        destruct @Eval.eval_expr; simpl in *.
        intuition.
        auto.
      clear Hg.
      set (op':=op); unfold op';
        case_eq (type_expr a1); intros He_a1; rewrite He_a1 in *; try (elim Ht; congruence);
          destruct op; inv E1; inv H0; try (inv Hg1; fail);
            apply ncompat_eval_nexpr;
              unfold Val.of_bool;
              try match goal with [|-context[Int.eq ?x ?y]] => case_eq (Int.eq x y); intros Hi; simpl end;
                try match goal with [id:context[Float.intoffloat]|-_] =>
                      destruct Float.intoffloat; inv id end;
                try match goal with [id:context[Float.intuoffloat]|-_] =>
                      destruct Float.intuoffloat; inv id end;
                unfold Vfalse, Vtrue;
                  try match goal with
                        |[|-eval_nexpr _ _ _] => econstructor; try eassumption; econstructor
                      end;
                  try match goal with
                        |[|-is_bool _] => constructor
                      end;
                  try (exists (Int.zero); constructor; constructor; fail);
                    try (econstructor; econstructor; try eassumption; econstructor);
                      try (apply is_bool_true; fail).
      econstructor; eauto.
      replace (Int.zero) with (of_bool (negb (Int.eq n Int.zero))); [constructor|rewrite Hi; auto].
      econstructor; eauto.
      replace (Int.one) with (of_bool (negb (Int.eq n Int.zero))); [constructor|rewrite Hi; auto].
      econstructor; eauto.
      replace (Int.one) with (of_bool (Int.eq n Int.zero)); [constructor|rewrite Hi; auto].
      econstructor; eauto.
      replace (Int.zero) with (of_bool (Int.eq n Int.zero)); [constructor|rewrite Hi; auto].
      >
      destruct IHeval_pexpr1 as (n1 & E11 & E12); auto.
      destruct IHeval_pexpr2 as (n2 & E21 & E22); auto.
      set (op':=op); unfold op';
        destruct op; inv E11; inv E21; inv H1;
          try match goal with [|-context[zeq]] => destruct zeq end;
            apply ncompat_eval_nexpr;
              try match goal with
                    |[|-eval_nexpr _ _ _] => econstructor; try eassumption; econstructor
                  end;
              try match goal with
                    [|-context[(Int.ltu ?i0 Int.iwordsize)]] =>
                    case_eq (Int.ltu i0 Int.iwordsize); simpl; intros
                  end;
              repeat match goal with
                       [|-context[type_expr ?e]] => case_eq (type_expr e); intros; auto
                     end;
              try (eelim eval_pexpr_type_expr_ptr_VI; eauto; fail);
                try (eelim eval_pexpr_type_expr_float_VI; eauto; fail);
                  try (exists (Int.zero); constructor; constructor; constructor; fail);
                    try (econstructor; econstructor; try eassumption; econstructor; fail);
                      try apply match_eval_nexpr_intunknown.
      econstructor; try eassumption; rewrite Int.add_commut; constructor.

      revert H3; case_eq_bool_in_goal; try congruence.
      intros T; apply orb_false_elim in T.
      rewrite andb_false_iff in T.
      intros T1; inv T1.
      destruct T.
      econstructor; try eassumption; econstructor; eauto.

      revert H3; case_eq_bool_in_goal; try congruence.
      intros T T1; inv T1; simpl;
        econstructor; try eassumption; econstructor; eauto.

      revert H3; case_eq_bool_in_goal; try congruence.
      intros T; apply orb_false_elim in T.
      rewrite andb_false_iff in T.
      simpl; intros T1; inv T1.
      destruct T.
      econstructor; try eassumption; econstructor; eauto.

      revert H3; case_eq_bool_in_goal; try congruence.
      intros T T1; inv T1;
        econstructor; try eassumption; econstructor; eauto.

      econstructor; [eauto|eauto|econstructor solve[assumption]].
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).

      econstructor; [eauto|eauto|econstructor solve[assumption]].
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).

      econstructor; [eauto|eauto|econstructor solve[assumption]].
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).
      econstructor; case_eq (Int.ltu n2 Int.iwordsize); intros;
        (econstructor; try eassumption; econstructor solve[eassumption]).

      destruct val_cmp_exists_int with c n1 n2 as (ii & V1 & V2); rewrite V1.
      econstructor; try eassumption.
      rewrite <- V2; econstructor.

      destruct val_cmpu_exists_int with (Mem.valid_pointer m) c n1 n2 as (ii & V1 & V2); rewrite V1.
      econstructor; try eassumption.
      rewrite <- V2; econstructor.
      match goal with
        | H : _ \/ _ |- _ =>
          let U := fresh in destruct H as [U|U];
                           repeat match goal with K : _ |- _ => specialize (K U)
                                               | K : exists _, _ |- _ => destruct K
                                  end;
                           inv U
      end.
      pose proof (eval_pexpr_type_expr_int_VP _ _ H). destruct type_expr.
      exists x0. intuition. inv H1. econstructor; eauto; intuition.
      congruence.
      exists x0. intuition. repeat constructor.
      pose proof (eval_pexpr_type_expr_ptr_VI _ _ _ H). destruct type_expr.
      congruence.
      exists x0. intuition. inv H1. econstructor. repeat econstructor. intuition.
      pose proof (Int.one_not_zero). intuition.
      auto.
      exists x0. intuition. repeat constructor.
      pose proof (eval_pexpr_type_expr_int_VP _ _ H). destruct type_expr.
      exists x0. intuition. inv H3. econstructor. eauto.
      instantiate (1:= false). intuition. auto.
      congruence.
      exists x0. intuition. repeat constructor.
    Qed.

End nconvert.

End Nconvert.