Module Mconvert


Require DebugAbMachineEnv NoError PointsTo.
Import
  Utf8
  String
  Coqlib
  AST
  Integers
  Floats
  Values
  Globalenvs
  Memory
  Cminor
  Csharpminor
  ToString
  Util
  AssocList
  ShareTree
  AdomLib
  AbMachineEnv
  TypesDomain
  PExpr
  NoError
  Cells
  PointsTo.

Local Unset Elimination Schemes.

Local Open Scope string_scope.

Module Nconvert(T:SHARETREE).

Module Import PT := PT T.

  Section nconvert.
    Variable ge: genv.
    Variable m: Mem.mem.
    Variable μ: ident.
    Variable ε: env.
    Variable tmp: temp_env.
    Variable σ : list (temp_env * env).
    Hypothesis Hμ : μ = plength σ.

    Variable var : Type.
    Variable var_dec : EqDec var.
    Variable elt2p: T.elt -> var.
    Variables num iter_num : Type.
    Variable NumDom : ab_machine_env (var := var) num iter_num.

    Definition convert_constant (cst: constant) : mexpr var :=
      match cst with
        | Ointconst n => MEconst _ (MNint n)
        | Olongconst n => MEconst _ (MNint64 n)
        | Ofloatconst f => MEconst _ (MNfloat f)
        | Osingleconst f => MEconst _ (MNsingle f)
        | Oaddrsymbol _ ofs => MEconst _ (MNint ofs)
      end.

    Inductive nconvert_msg_kind : Set :=
    | MSG_CONST_NOME
    | MSG_ILL_TYPED_UNOP
    | MSG_ILL_TYPED_BINOP
    | MSG_LARGE_PTSET
    | MSG_UNSAFE_NUM
    | MSG_VALID_PTR
    | MSG_EQ_BLOCKS
    | MSG_CMP_BLK_DK
    | MSG_CMP_OP
    | MSG_NULL
    .

    Definition nconvert_msg_type (k: nconvert_msg_kind) : Type :=
      match k with
      | MSG_CONST_NOME
      | MSG_LARGE_PTSET
        => string
      | MSG_NULL
      | MSG_UNSAFE_NUM
        => mexpr varstring
      | MSG_EQ_BLOCKS
      | MSG_CMP_BLK_DK
        => BlockSet.tBlockSet.tstring
      | MSG_ILL_TYPED_UNOP => Cminor.unary_operationAbTy.tstring
      | MSG_ILL_TYPED_BINOP => Cminor.binary_operationAbTy.tAbTy.tstring
      | MSG_VALID_PTR => boolBlockSet.tmexpr varstring
      | MSG_CMP_OP => comparisonstring
      end.

    Section STRING_OF_MEXPR.

    Import DebugAbMachineEnv DebugCminor.
 
    Local Instance AblockToString : ToString ablock := AblockToString ge.
    Existing Instances MN_ToString MNI_ToString.

    Context (nm: num).

    Fixpoint string_of_mexpr (e: mexpr var) {struct e} : string :=
      match e with
      | MEvar ty v => to_string (get_itv (MEvar ty v) nm)
      | MEconst c => to_string c
      | MEunop op e' => string_of_unop op ++ string_of_mexpr e'
      | MEbinop op x y => "(" ++ string_of_mexpr x ++ string_of_binop op ++ string_of_mexpr y ++ ")"
      end.

    Definition nconvert_msg (k: nconvert_msg_kind) : nconvert_msg_type k :=
      match k return nconvert_msg_type k with
      | MSG_CONST_NOME => "const None"
      | MSG_ILL_TYPED_UNOP => λ op ty, "ill-typed op: " ++ to_string op ++ to_string ty
      | MSG_ILL_TYPED_BINOP => λ op tyty₂, "ill-typed op: " ++ to_string ty₁ ++ to_string op ++ to_string ty
      | MSG_LARGE_PTSET => "too large points-to set in subtraction or comparison"
      | MSG_UNSAFE_NUM=> λ me, "cannot prove safe a numerical expression: " ++ string_of_mexpr me
      | MSG_VALID_PTR => λ weak bs me, "cannot prove pointer " ++ (if weak then "weakly " else "") ++ "valid: " ++ to_string bs ++ " " ++ string_of_mexpr me
      | MSG_EQ_BLOCKS => λ bsbs₂, "cannot prove blocks equal in subtraction " ++ to_string bs₁ ++ " and " ++ to_string bs
      | MSG_CMP_BLK_DK => λ bsbs₂, "cannot compare points-to sets " ++ to_string bs₁ ++ " and " ++ to_string bs
      | MSG_CMP_OP => λ c, "bad comparison operator: " ++ to_string c
      | MSG_NULL => λ me, "cannot prove definitely null: " ++ string_of_mexpr me
      end.
    Global Opaque nconvert_msg.

    End STRING_OF_MEXPR.

    Definition well_typed_unop (op: unary_operation) (ty: typ) : bool :=
      match op with
      | Ocast8unsigned
      | Ocast8signed
      | Ocast16unsigned
      | Ocast16signed
      | Onegint
      | Onotint
      | Ofloatofint
      | Ofloatofintu
      | Osingleofint
      | Osingleofintu
      | Olongofint
      | Olongofintu
          => eq_dec VI ty
      | Onegf
      | Oabsf
      | Osingleoffloat
      | Ointoffloat
      | Ointuoffloat
      | Olongoffloat
      | Olonguoffloat
          => eq_dec VF ty
      | Onegfs
      | Oabsfs
      | Ofloatofsingle
      | Ointofsingle
      | Ointuofsingle
      | Olongofsingle
      | Olonguofsingle
          => eq_dec VS ty
      | Onegl
      | Onotl
      | Ointoflong
      | Ofloatoflong
      | Ofloatoflongu
      | Osingleoflong
      | Osingleoflongu
          => eq_dec VL ty
      end.

    Inductive nconvert_binop_cases : Type :=
    | NBC_normal
    | NBC_ptr_sub
    | NBC_ptr_ptr_cmp `(comparison)
    | NBC_ptr_int_cmp `(bool) `(comparison)
    | NBC_wrong
    .

    Definition nbc_classify (op: binary_operation) (tyty₂: typ) : nconvert_binop_cases :=
      match ty₁, ty₂, op with
      | VI, (VIP | VP), Oadd | (VIP | VP), VI, Oadd
      | (VIP | VP), VI, Osub
      | VI, VI,
        (Oadd | Osub | Omul | Odiv | Odivu | Omod | Omodu | Oand
         | Oor | Oxor | Oshl | Oshr | Oshru | Ocmp _ | Ocmpu _)
      | VL, VL,
        (Oaddl | Osubl | Omull | Odivl | Odivlu | Omodl | Omodlu
         | Oandl | Oorl | Oxorl | Ocmpl _ | Ocmplu _)
      | VL, VI, (Oshll | Oshrl | Oshrlu)
      | VF, VF, (Oaddf | Osubf | Omulf | Odivf | Ocmpf _)
      | VS, VS, (Oaddfs | Osubfs | Omulfs | Odivfs | Ocmpfs _) =>
        NBC_normal
      | VP, VP, Osub => NBC_ptr_sub
      | VP, VP, Ocmpu c => NBC_ptr_ptr_cmp c
      | VP, VI, Ocmpu c => NBC_ptr_int_cmp false c
      | VI, VP, Ocmpu c => NBC_ptr_int_cmp true c
      | _, _, _ => NBC_wrong
      end.

    Lemma nbc_classify_intro :
      forall P : binary_operation -> typ -> typ -> nconvert_binop_cases -> Prop,

        (forall o x y, P o x y NBC_wrong) ->

        P Oadd VI VIP NBC_normal ->
        P Oadd VI VP NBC_normal ->
        P Oadd VIP VI NBC_normal ->
        P Oadd VP VI NBC_normal ->

        P Osub VIP VI NBC_normal ->
        P Osub VP VI NBC_normal ->

        P Oadd VI VI NBC_normal ->
        P Osub VI VI NBC_normal ->
        P Omul VI VI NBC_normal ->
        P Odiv VI VI NBC_normal ->
        P Odivu VI VI NBC_normal ->
        P Omod VI VI NBC_normal ->
        P Omodu VI VI NBC_normal ->
        P Oand VI VI NBC_normal ->
        P Oor VI VI NBC_normal ->
        P Oxor VI VI NBC_normal ->
        P Oshl VI VI NBC_normal ->
        P Oshr VI VI NBC_normal ->
        P Oshru VI VI NBC_normal ->
        (forall c, P (Ocmp c) VI VI NBC_normal) ->
        (forall c, P (Ocmpu c) VI VI NBC_normal) ->

        P Oaddl VL VL NBC_normal ->
        P Osubl VL VL NBC_normal ->
        P Omull VL VL NBC_normal ->
        P Odivl VL VL NBC_normal ->
        P Odivlu VL VL NBC_normal ->
        P Omodl VL VL NBC_normal ->
        P Omodlu VL VL NBC_normal ->
        P Oandl VL VL NBC_normal ->
        P Oorl VL VL NBC_normal ->
        P Oxorl VL VL NBC_normal ->
        (forall c, P (Ocmpl c) VL VL NBC_normal) ->
        (forall c, P (Ocmplu c) VL VL NBC_normal) ->

        P Oshll VL VI NBC_normal ->
        P Oshrl VL VI NBC_normal ->
        P Oshrlu VL VI NBC_normal ->

        P Oaddf VF VF NBC_normal ->
        P Osubf VF VF NBC_normal ->
        P Omulf VF VF NBC_normal ->
        P Odivf VF VF NBC_normal ->
        (forall c, P (Ocmpf c) VF VF NBC_normal) ->

        P Oaddfs VS VS NBC_normal ->
        P Osubfs VS VS NBC_normal ->
        P Omulfs VS VS NBC_normal ->
        P Odivfs VS VS NBC_normal ->
        (forall c, P (Ocmpfs c) VS VS NBC_normal) ->

        P Osub VP VP NBC_ptr_sub ->
        (forall c, P (Ocmpu c) VP VP (NBC_ptr_ptr_cmp c)) ->
        (forall c, P (Ocmpu c) VP VI (NBC_ptr_int_cmp false c)) ->
        (forall c, P (Ocmpu c) VI VP (NBC_ptr_int_cmp true c)) ->

        forall o x y, P o x y (nbc_classify o x y).
Proof.
      intros.
      destruct x, y, o; eauto.
    Qed.

    Context {MD: Type} (sz : ABTree.t (Z * MD)).
    Hypothesis SZ :
      ∀ b hi md b',
        ABTreeDom.get b sz = Just (hi, md) →
        block_of_ablock ge ((tmp, ε) :: σ) b = Some b' →
        Mem.range_perm m b' 0 hi Cur Nonempty.
    
    Variable nm : num.

    Definition is_valid_ptr (weak: bool) (bs: BlockSet.t) (off: mexpr var) : bool :=
      match min_size sz bs MaxSize with
      | MaxSize => false
      | Size (Zpos min) =>
        let i := Int.repr (Zpos (if weak then Pos.succ min else min)) in
        Pos.ltb min (Z.to_pos Int.max_unsigned) &&
                is_bot (assume (MEbinop (Ocmpu Clt) off (me_const_i _ i)) false nm)
      | Size _
      | MinSize => false
      end.

    Let is_null := is_null NumDom nm.

    Fixpoint nconvert (pt: points_to) (e:pexpr T.elt) : mexpr var + (option (mexpr var) * string) :=
      match e with
        | PEvar c ty =>
          match ty with
            | VI|VP|VIP => inl (MEvar MNTint (elt2p c))
            | VL => inl (MEvar MNTint64 (elt2p c))
            | VF => inl (MEvar MNTfloat (elt2p c))
            | VS => inl (MEvar MNTsingle (elt2p c))
          end
        | PElocal _ => inl (MEconst _ (MNint Int.zero))
        | PEconst (Some cst) _ => inl (convert_constant cst)
        | PEconst None _ => inr (None, nconvert_msg nm MSG_CONST_NOME)

        | PEunop op e _ =>
          let ty := pexpr_get_ty e in
          if well_typed_unop op ty
          then
            match nconvert pt e with
            | inl e' => inl (MEunop op e')
            | inr _ as e => e
            end
          else
            inr (None, nconvert_msg nm MSG_ILL_TYPED_UNOP op ty)

        | PEbinop op e1 e2 _ =>
          let ty₁ := pexpr_get_ty e1 in
          let ty₂ := pexpr_get_ty e2 in
          match nbc_classify op tytywith

          | NBC_normal =>
            match nconvert pt e1 with
            | inl e1' =>
              match nconvert pt e2 with
              | inl e2' => inl (MEbinop op e1' e2')
              | inr _ as e => e
              end
            | inr _ as e => e
            end

          | NBC_ptr_sub =>
            match nconvert pt e1 with
            | inl nx =>
              match nconvert pt e2 with
              | inl ny =>
                match pt_eval_pexpr ge μ pt e1, pt_eval_pexpr ge μ pt e2 with
                | Just xb, Just yb =>
                  let res := MEbinop op nx ny in
                  match cmp_blockset xb yb with
                  | Equal b => inl res
                  | _ => inr (Some res, nconvert_msg nm MSG_EQ_BLOCKS xb yb)
                  end
                | _, _ => inr(None, nconvert_msg nm MSG_LARGE_PTSET)
                end
              | inr _ as e => e
              end
            | inr _ as e => e
            end

          | NBC_ptr_ptr_cmp c =>
            match nconvert pt e1 with
            | inl nx =>
              match nconvert pt e2 with
              | inl ny =>
                match pt_eval_pexpr ge μ pt e1, pt_eval_pexpr ge μ pt e2 with
                | Just xb, Just yb =>
                  match cmp_blockset xb yb with
                  | Equal b =>
                    let res := MEbinop (Ocmpu c) nx ny in
                    if is_valid_ptr true xb nx
                    then if is_valid_ptr true yb ny
                         then inl res
                         else inr (Some res, nconvert_msg nm MSG_VALID_PTR true yb ny)
                    else inr (Some res, nconvert_msg nm MSG_VALID_PTR true xb nx)
                  | Disjoint =>
                    if noerror nx nm
                    then if noerror ny nm
                    then if is_valid_ptr false xb nx
                    then if is_valid_ptr false yb ny
                    then match c with
                         | Ceq => inl (MEconst _ (MNint Int.zero))
                         | Cne => inl (MEconst _ (MNint Int.one))
                         | _ => inr (None, nconvert_msg nm MSG_CMP_OP c)
                         end
                    else inr (None, nconvert_msg nm MSG_VALID_PTR false yb ny)
                    else inr (None, nconvert_msg nm MSG_VALID_PTR false xb nx)
                    else inr (None, nconvert_msg nm MSG_UNSAFE_NUM ny)
                    else inr (None, nconvert_msg nm MSG_UNSAFE_NUM nx)
                  | DontKnow => inr (None, nconvert_msg nm MSG_CMP_BLK_DK xb yb)
                  | Contradiction =>
                    if noerror nx nm
                    then if noerror ny nm
                    then inl (MEconst _ (MNint Int.one))
                    else inr (None, nconvert_msg nm MSG_UNSAFE_NUM ny)
                    else inr (None, nconvert_msg nm MSG_UNSAFE_NUM nx)
                  end
                | _, _ => inr (None, nconvert_msg nm MSG_LARGE_PTSET)
                end
              | inr _ as e => e
              end
            | inr _ as e => e
            end

          | NBC_ptr_int_cmp swapped c =>
            match nconvert pt e1 with
            | inl nx =>
              if noerror nx nm
              then
                match nconvert pt e2 with
                | inl ny =>
                  if noerror ny nm
                  then
                    if is_null (if swapped then nx else ny)
                    then
                      match pt_eval_pexpr ge μ pt (if swapped then e2 else e1) with
                      | Just bs =>
                        match c with
                        | (Ceq | Cne) =>
                          let res := MEconst _ (MNint match c with Ceq => Int.zero | _ => Int.one end) in
                          if is_valid_ptr true bs (if swapped then ny else nx) then inl res
                          else inr (Some res, nconvert_msg nm MSG_VALID_PTR true bs (if swapped then ny else nx))
                        | _ => inr (None, nconvert_msg nm MSG_CMP_OP c)
                        end
                      | _ => inr (None, nconvert_msg nm MSG_LARGE_PTSET)
                      end
                    else inr (None, nconvert_msg nm MSG_NULL (if swapped then nx else ny))
                  else inr (None, nconvert_msg nm MSG_UNSAFE_NUM ny)
                | inr _ as e => e
                end
              else inr (None, nconvert_msg nm MSG_UNSAFE_NUM nx)
            | inr _ as e => e
            end

          | NBC_wrong => inr (None, nconvert_msg nm MSG_ILL_TYPED_BINOP op tyty₂)
          end
      end.

    Lemma bind_inl {A B} (f: AA + B) (ab: A + B) (a': A):
      match ab with inl a' => f a' | inr b => inr b end = inl a' →
      ∃ a : A, ab = inl af a = inl a'.
Proof.
      destruct ab as [ a | b ]. vauto. intro; eq_some_inv.
    Qed.

    Local Ltac ncinv :=
      try match goal with H : _ = Some _ |- _ => apply do_opt_some_inv in H; hsplit end;
      repeat match goal with H : _ = inl _ |- _ => apply bind_inl in H; hsplit end;
      eq_some_inv; subst; simpl;
      repeat match goal with H : _, K : __ |- _ => specialize (K _ H) end.

    Lemma nconvert_fv pt pe :
      ∀ me, nconvert pt pe = inl me
      ∀ x, xme_free_var me → ∃ y, ype_free_var pex = elt2p y.
Proof.
      clear Hμ.
      induction pe; simpl; intros me Hme cc Hcc.
      - destruct t; eq_some_inv; subst me; simpl in Hcc; subst cc; vauto.
      - eq_some_inv; subst me. destruct Hcc.
      - destruct o as [[]|]; eq_some_inv; subst me; simpl in *; destruct Hcc.
      - destruct (well_typed_unop _ _); eq_some_inv.
        destruct (nconvert _ _); eq_some_inv.
        subst me. eauto.
      - destruct (nbc_classify _ _ _); eq_some_inv;
        repeat match goal with
        | H : (if ?b then _ else _) = inl _ |- _ =>
          destruct b; eq_some_inv
        | H : _ = inl _ |- _ => apply bind_inl in H; hsplit; eq_some_inv
        | H : appcontext[ pt_eval_pexpr ?ge ?μ ?pt ?pe ] |- _ =>
          destruct (pt_eval_pexpr ge μ pt pe); eq_some_inv
        | H : appcontext[ cmp_blockset ?x ?y ] |- _ =>
          destruct (cmp_blockset x y); eq_some_inv
        | H : match ?c with Ceq => _ | _ => _ end = inl _ |- _ =>
          destruct c; eq_some_inv
        end; subst;
        try (
        simpl in Hcc;
        destruct Hcc; ncinv; hsplit; vauto;
        fail).
    Qed.

    Definition ncompat : val -> mach_num -> Prop :=
      λ v, match v with
             | Vint i | Vptr _ i => eq (MNint i)
             | Vlong l => eq (MNint64 l)
             | Vsingle f => eq (MNsingle f)
             | Vfloat f => eq (MNfloat f)
             | Vundef => λ _, True
           end.

    Lemma ncompat_inv_int v i :
      ncompat v (MNint i) →
      v = Vint i ∨ (∃ b, v = Vptr b i) ∨ v = Vundef.
Proof.
      destruct v; inversion 1; vauto.
    Qed.

    Lemma ncompat_inv_int64 v i :
      ncompat v (MNint64 i) →
      v = Vlong iv = Vundef.
Proof.
      destruct v; inversion 1; vauto.
    Qed.

    Lemma ncompat_inv_float v f :
      ncompat v (MNfloat f) →
      v = Vfloat fv = Vundef.
Proof.
      destruct v; inversion 1; vauto.
    Qed.

    Lemma ncompat_inv_single v f :
      ncompat v (MNsingle f) →
      v = Vsingle fv = Vundef.
Proof.
      destruct v; inversion 1; vauto.
    Qed.

    Definition compat_fun (v:val) : mach_num :=
      match v with
      | Vptr _ i | Vint i => MNint i
      | Vlong l => MNint64 l
      | Vundef => MNint Int.zero
      | Vfloat f => MNfloat f
      | Vsingle f => MNsingle f
      end.

    Lemma ncompat_compat_fun v :
      ncompat v (compat_fun v).
Proof.
      destruct v; simpl; constructor.
    Qed.

    Ltac ncompat_inv H :=
      match type of H with
             | ncompat ?v (MNint ?i) =>
               destruct (ncompat_inv_int v i H) as [?|[(? & ?)|?]];
               clear H
             | ncompat ?v (MNint64 ?i) =>
               destruct (ncompat_inv_int64 v i H) as [?|?];
               clear H
             | ncompat ?v (MNfloat ?i) =>
               destruct (ncompat_inv_float v i H) as [?|?];
               clear H
             | ncompat ?v (MNsingle ?i) =>
               destruct (ncompat_inv_single v i H) as [?|?];
               clear H
             end.

    Definition wtype_num (v:mach_num) (tp:AbTy.t) : Prop :=
      match v, tp with
        | MNint _, (VI|VP|VIP)
        | MNint64 _, VL
        | MNfloat _, VF
        | MNsingle _, VS => True
        | _, _ => False
      end.

    Definition compatC:T.elt -> val) (ρ:var -> mach_num) : Prop :=
      forall c, ncompatC c) (ρ (elt2p c)).

    Variable ρC: T.elt -> val.
    Variable ρ: var -> mach_num.

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

    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) = (MNint i).
Proof.
      unfold Val.cmp, of_bool, Val.cmp_bool; intros.
      destruct Int.cmp; simpl; repeat econstructor.
    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) = MNint i.
Proof.
      unfold Val.cmpu, of_bool, Val.cmpu_bool; intros.
      destruct Int.cmpu; simpl; repeat econstructor.
    Qed.

    Lemma val_cmpf_exists_int: forall c f1 f2,
      exists i,
        Val.cmpf c (Vfloat f1) (Vfloat f2) = Vint i /\
        of_bool (Float.cmp c f1 f2) = MNint i.
Proof.
      unfold Val.cmpf, of_bool, Val.cmpf_bool; intros.
      destruct Float.cmp; simpl; repeat econstructor.
    Qed.

    Lemma val_cmpfs_exists_int: forall c f1 f2,
      exists i,
        Val.cmpfs c (Vsingle f1) (Vsingle f2) = Vint i /\
        of_bool (Float32.cmp c f1 f2) = MNint i.
Proof.
      unfold Val.cmpfs, of_bool, Val.cmpfs_bool; intros.
      destruct Float32.cmp; simpl; repeat econstructor.
    Qed.

    Lemma val_of_bool_exists_int: forall b,
      exists i,
        Val.of_bool b = Vint i /\
        of_bool b = MNint i.
Proof.
      unfold of_bool; intros.
      destruct b; repeat econstructor.
    Qed.

    Lemma ncompat_Vundef: forall n, ncompat Vundef n.
Proof.
      destruct n; constructor.
    Qed.
    Hint Resolve ncompat_Vundef.

    Lemma exist_ncompat_Vundef: forall P,
      (exists n, P n) ->
      exists n : mach_num, ncompat Vundef n /\ P n.
Proof.
      intros P (n & H).
      repeat econstructor; eauto.
    Qed.

    Lemma exist_ncompat_Vint: forall (P:mach_num -> Prop) i,
      P (MNint i) ->
      exists n : mach_num, ncompat (Vint i) n /\ P n.
Proof.
      intros P H.
      repeat econstructor; eauto.
    Qed.

    Lemma exist_ncompat_Vptr: forall (P:mach_num -> Prop) b i,
      P (MNint i) ->
      exists n : mach_num, ncompat (Vptr b i) n /\ P n.
Proof.
      intros P H.
      repeat econstructor; eauto.
    Qed.

    Lemma exist_ncompat_Vlong: forall (P:mach_num -> Prop) l,
      P (MNint64 l) ->
      exists n : mach_num, ncompat (Vlong l) n /\ P n.
Proof.
      intros P H.
      repeat econstructor; eauto.
    Qed.

    Lemma exist_ncompat_Vfloat: forall (P:mach_num -> Prop) f,
      P (MNfloat f) ->
      exists n : mach_num, ncompat (Vfloat f) n /\ P n.
Proof.
      intros P H.
      repeat econstructor; eauto.
    Qed.

    Lemma exist_ncompat_Vsingle: forall (P:mach_num -> Prop) f,
      P (MNsingle f) ->
      exists n : mach_num, ncompat (Vsingle f) n /\ P n.
Proof.
      intros P H.
      repeat econstructor; eauto.
    Qed.

    Lemma of_bool_MNint : forall b,
      exists i, of_bool b = MNint i.
Proof.
      unfold of_bool; destruct b; econstructor; reflexivity.
    Qed.

    Hypothesis block_of_ablock_inj :
      ∀ abbabb₂,
        block_of_ablock ge ((tmp, ε) :: σ) ab₁ = Some b₁ →
        block_of_ablock ge ((tmp, ε) :: σ) ab₂ = Some b₂ →
        ab₁ ≠ ab₂ →
        b₁ ≠ b₂.

    Local Ltac subs := repeat match goal with H : ?a = ?b |- _ => subst a || subst b end.

    Lemma nconvert_correct: forall e,
      forall v, eval_pexpr ge m ρC ε e v ->
      forall pt (PT: ρCpoints_to_gamma ge ((tmp, ε) :: σ) pt) e', nconvert pt e = inl e' ->
      vVundef
      exists n, ncompat v n /\
                eval_mexpr ρ e' n /\
                wtype_num n (pexpr_get_ty e).
Proof.
      intros e v Hv pt PT e' He' Hvundef.
      cut (∃ n : mach_num, ncompat v neval_mexpr ρ e' n).
      { intros (n & A & B). exists n. split. auto. split. auto.
        pose proof pexpr_get_ty_ok Hv Hvundef.
        destruct v, n, (pexpr_get_ty e); try contradiction; try congruence; constructor. }
      revert v Hv e' He' Hvundef. induction e; intros vv Hvv; eval_pexpr_inv; hsplit; subs; simpl.
      - intros. specialize (Hcompat v).
        exists (ρ (elt2p v)); repeat split; subs; auto.
        destruct t, (ρC v) eqn:EQρ; eq_some_inv; subs; try congruence;
        (constructor; [now auto|]); simpl in Hcompat; try (intuition; fail);
        rewrite <- Hcompat; constructor.
      - intros e' E' NB; eq_some_inv. subs. exists (MNint Int.zero).
        repeat (constructor; auto).
      - destruct o; eval_pexpr_inv; hsplit; subs; intros e' ?; eq_some_inv; subs.
        intros Hvundef.
        destruct c; simpl in *;
        (econstructor; split; [auto|repeat econstructor]);
        try apply Zle_refl.
        destruct Genv.find_symbol. reflexivity. elim (Hvundef eq_refl).
      - intros e' He' HB.
        assert (v' ≠ Vundef) as Hv1.
        { contradict HB. subs. destruct u; simpl in *; eq_some_inv; auto. }
        destruct H0 as [ Hty | Hty]. elim (HB Hty).
        assert (Hg:= pexpr_get_ty_ok Hvv Hv1).
        destruct (well_typed_unop _ _) eqn: Hwt. 2: eq_some_inv.
        destruct (nconvert _ _); eq_some_inv; subs;
        specialize (IHe _ Hvv _ eq_refl Hv1).
        destruct IHe as (() & E1 & E2);
        ncompat_inv E1; subs; try congruence;
        destruct u; simpl in *; eq_some_inv; hsplit; apply proj_sumbool_true in Hwt;
        rewrite <- Hwt in Hg; try (destruct Hg; fail); clear Hg; subs;
        repeat econstructor; simpl; eauto.
      - intros e' He' HB.
        destruct H1 as [ H1 | H1 ]. elim (HB H1); fail.
        assert (v₁ ≠ Vundef) as Hv1.
        { contradict HB. subs. clear -H0.
          destruct b; simpl in *;
          unfold Val.cmpl, Val.cmplu, Val.cmpl_bool, Val.cmplu_bool in *;
          eq_some_inv; hsplit; eq_some_inv; auto. }
        assert (Hg1:= pexpr_get_ty_ok Hvv Hv1). red in Hg1.
        assert (v₂ ≠ Vundef) as Hv2.
        { contradict HB. subs. clear -H0.
          destruct v₁, b; simpl in *; eq_some_inv; auto;
          unfold Val.cmpl, Val.cmplu, Val.cmpl_bool, Val.cmplu_bool in *;
          simpl in *; eq_some_inv; auto. }
        assert (Hg2:= pexpr_get_ty_ok H Hv2). red in Hg2.
        revert He'.
        generalize dependent (pexpr_get_ty e2). intros ty2.
        generalize dependent (pexpr_get_ty e1). intros ty1.
        generalize dependent b; intros b.
        apply nbc_classify_intro;
          [ intros o x y H0 Hg1 Hg2 He'; exact (inl_not_inr (eq_sym He') _) | .. ];
          ( intros c EV Hg1 Hg2 He' || intros EV Hg1 Hg2 He' );
        repeat match goal with
        | H : inr _ = inl _ |- _ => exact (inl_not_inr (eq_sym H) _)
        | H : match _ with inl _ => _ | _ => _ end = inl _ |- _ =>
          apply bind_inl in H; destruct H as (? & ? & H)
        | H : match ?x with All => _ | _ => _ end = inl _ |- _ =>
          destruct x eqn: ?
        | H : match cmp_blockset ?x ?y with _ => _ end = inl _ |- _ =>
          pose proof (cmp_blockset_correct x y);
            destruct (cmp_blockset x y)
        | H : (if noerror ?me _ then _ else _) = inl _ |- _ =>
          destruct (noerror me _)
        | H : (if is_null ?me then _ else _) = inl _ |- _ =>
          destruct (is_null me)
        | H : match ?c with Ceq => _ | _ => _ end = inl _ |- _ =>
          destruct c
        | H : (if is_valid_ptr ?w ?bs ?me then _ else _) = inl _ |- _ =>
          destruct (is_valid_ptr w bs me)
        end; eq_some_inv; subs;
        repeat match goal with
        | H : ∀ v, eval_pexpr _ _ _ _ ?pe v → ∀ me, nconvert _ ?pe = inl __ ,
          EV : eval_pexpr _ _ _ _ ?pe ?x, NC : nconvert _ ?pe = _,
          DEF : ?xVundef |- _ =>
          specialize (H _ EV _ NC DEF);
          let ne := fresh ne in
          let Hnc := fresh Hnc in
          let EV := fresh EV in
          destruct H as (ne & Hnc & EV)
        end; subs;

        destruct v₁; try (elim (Hv1 eq_refl)); simpl in *; eq_some_inv;
        destruct v₂; try (elim (Hv2 eq_refl)); simpl in *; eq_some_inv;
        subs;

        try (elim Hg1; discriminate); try (elim Hg2; discriminate);

      repeat match goal with
      | H : pt_eval_pexpr _ _ _ ?e = Just ?bs, EV : eval_pexpr _ _ _ _ ?pe _, X : _ |- _ =>
        generalize (pt_eval_pexpr_correct eq_refl PT EV); rewrite H; clear H;
        let Hbs := fresh Hbs in
        intros (? & Hbs & ?);
        (specialize (X _ Hbs) || specializeq, X _ q Hbs))
      end;
      try match goal with
      | X: block_of_ablock _ _ ?x = _,
        Y: block_of_ablock _ _ ?y = _,
        NE: ?x ≠ ?y |- _ =>
        pose proof (block_of_ablock_inj _ _ _ _ X Y NE)
      end;

        try (unfold Val.cmpl, Val.cmplu in *; simpl in *);
        eq_some_inv; subs;
        repeat match goal with
           | id: (if ?b then _ else _) = Some _ |- _ => destruct b eqn:?; inversion id; clear id; subs
           | id: (_ || _) = false |- _ => apply orb_false_elim in id; destruct id
           | id: (_ && _) = false |- _ => apply andb_false_iff in id
           | H: (_ && _) = true |- _ => apply andb_true_iff in H; destruct H
           | H: appcontext[eq_dec _ _] |- _ => apply proj_sumbool_true in H
           | |- appcontext [if ?b then _ else _] => destruct b eqn:?
         end;
        try match goal with
          | |- context[Oshl] => destruct (Int.ltu i0 Int.iwordsize) eqn:?
          | |- context[Oshr] => destruct (Int.ltu i0 Int.iwordsize) eqn:?
          | |- context[Oshru] => destruct (Int.ltu i0 Int.iwordsize) eqn:?
          | |- context[Oshll] => destruct (Int.ltu i0 Int64.iwordsize') eqn:?
          | |- context[Oshrl] => destruct (Int.ltu i0 Int64.iwordsize') eqn:?
          | |- context[Oshrlu] => destruct (Int.ltu i0 Int64.iwordsize') eqn:?
          | |- context[Val.cmp ?c (Vint ?i1) (Vint ?i2)] =>
            destruct (val_cmp_exists_int c i1 i2) as (bi & B1 & B2); rewrite B1
          | |- context[Val.cmpu ?m ?c (Vint ?i1) (Vint ?i2)] =>
            destruct (val_cmpu_exists_int m c i1 i2) as (bi & B1 & B2); rewrite B1
          | |- context[Val.cmpf ?c (Vfloat ?f1) (Vfloat ?f2)] =>
            destruct (val_cmpf_exists_int c f1 f2) as (bi & B1 & B2); rewrite B1
          | |- context[Val.cmpfs ?c (Vsingle ?f1) (Vsingle ?f2)] =>
            destruct (val_cmpfs_exists_int c f1 f2) as (bi & B1 & B2); rewrite B1
          | |- context[Val.of_bool ?b] =>
            destruct (val_of_bool_exists_int b) as (bi & B1 & B2); rewrite B1
        end;
        try (rewrite He_a1, He_a2);
        try (elim (HB eq_refl));
        try (apply exist_ncompat_Vundef; econstructor; split;
             [ econstructor; try eassumption; econstructor; eauto
             | try match goal with
                 | |- context[of_bool ?b] =>
                   destruct (of_bool_MNint b) as (nb & Hb); rewrite Hb
               end; simpl; auto]; fail);
        try (apply exist_ncompat_Vint;
             econstructor; try eassumption; try rewrite <- B2;
             econstructor; eauto; fail);
        try (match goal with b: block |- _ =>
             refine (exist_ncompat_Vptr _ b _ _);
             econstructor; try eassumption;
             (econstructor || rewrite Int.add_commut; econstructor); eauto; fail
             end);
        try (now repeat (econstructor (eauto))).
        idtac.
        hsplit; subs. unfold Val.cmpu in *.
        simpl in *. destruct (eq_block _ _). 2: congruence. subs.
        revert HB. bif. 2: intros X; elim (X eq_refl). intros _.
        match goal with |- appcontext[ Int.cmpu ?c ?x ?y] =>
                        exists (of_bool (Int.cmpu c x y))
        end. split. simpl. bif; reflexivity. vauto.
        unfold Val.cmpu in *. simpl in *. revert HB.
        case eq_block. congruence. intros _.
        bif'. 2: intros X; elim (X eq_refl). intros _. vauto.
        vauto2.
        unfold Val.cmpu in *. simpl in *. revert HB.
        case eq_block. congruence. intros _.
        bif'. 2: intros X; elim (X eq_refl). intros _. vauto.
        vauto2.
        unfold Val.cmpu in *. simpl in *. revert HB.
        bif'. 2: intros X; elim (X eq_refl). intros _. vauto2.
        unfold Val.cmpu in *. simpl in *. revert HB.
        bif'. 2: intros X; elim (X eq_refl). intros _. vauto2.
        unfold Val.cmpu in *. simpl in *. revert HB.
        bif'. 2: intros X; elim (X eq_refl). intros _. vauto2.
        unfold Val.cmpu in *. simpl in *. revert HB.
        bif'. 2: intros X; elim (X eq_refl). intros _. vauto2.
    Qed.

    Lemma is_valid_ptr_valid (NM: ρ ∈ γ nm) weak bs off :
      is_valid_ptr weak bs off = true
      ∀ ab, BlockSet.mem ab bs = true
      ∀ b, block_of_ablock ge ((tmp, ε) :: σ) ab = Some b
      ∀ i, eval_mexpr ρ off (MNint i) →
           (if weak
           then Mem.weak_valid_pointer m b (Int.unsigned i)
           else Mem.valid_pointer m b (Int.unsigned i)) = true.
Proof.
      unfold is_valid_ptr.
      generalize (min_size_min sz bs MaxSize). simpl.
      destruct (min_size sz bs MaxSize) as [|z|]; intros [H _] LT; eq_some_inv.
      destruct z as [|min|]; eq_some_inv.
      rewrite !andb_true_iff in LT. destruct LT as [Hz LT].
      rewrite Pos2Z.inj_ltb, Z.ltb_lt in Hz.
      pose proof (assume_bot NumDom _ _ LT NM) as K. clear LT.
      intros ab Hab b Hb i EV.
      specialize (H _ Hab). simpl in H.
      generalizehi md EQ, SZ ab hi md _ EQ Hb).
      unfold ABTreeDom.get. destruct (ABTree.get ab sz) as [(hi, md)|].
      2: exact (False_ind _ H).
      simpl in H.
      intros Hperm. specialize (Hperm _ _ eq_refl).
      unfold Mem.weak_valid_pointer, Mem.valid_pointer.
      destruct weak.
      *
      generalize (Int.unsigned_range i). intros [Hi Hi'].
      assert (0 < Int.unsigned i ∨ 0 = Int.unsigned i) as [Hi''|Hi'']. Psatz.lia.
      destruct (Mem.perm_dec _ _ (_ - 1) _ _) as [|Q]. rewrite orb_true_r. reflexivity.
      destruct (Int.cmpu Clt i (Int.repr (Zpos (Pos.succ min)))) eqn: Hmin.
      2: elim K; rewrite <- Hmin; vauto.
      elim Q; clear Q.
      simpl in Hmin. unfold Int.ltu in Hmin. rewrite Int.unsigned_repr in Hmin.
      2: change Int.max_unsigned with 4294967295; Psatz.lia.
      destruct (zlt (Int.unsigned i) _); eq_some_inv. clear Hmin.
      specialize (Hperm (Int.unsigned i - 1)).
      eapply Mem.perm_implies. eapply Hperm. Psatz.lia. destruct ab; vauto.
      destruct (Mem.perm_dec _ _ (Int.unsigned i) _ _) as [|Q]. reflexivity.
      destruct (Int.cmpu Clt i (Int.repr (Zpos (Pos.succ min)))) eqn: Hmin.
      2: elim K; rewrite <- Hmin; vauto.
      elim Q; clear Q.
      simpl in Hmin. unfold Int.ltu in Hmin. rewrite Int.unsigned_repr in Hmin.
      2: change Int.max_unsigned with 4294967295; Psatz.lia.
      destruct (zlt (Int.unsigned i) _); eq_some_inv. clear Hmin.
      specialize (Hperm (Int.unsigned i)).
      eapply Hperm. Psatz.lia.
       *
      destruct (Mem.perm_dec _ _ _ _ _) as [|Q]. reflexivity.
      elim Q; clear Q.
      destruct (Int.cmpu Clt i (Int.repr (Zpos min))) eqn: Hi.
      2: elim K; rewrite <- Hi; vauto. clear K.
      simpl in Hi. unfold Int.ltu in Hi. rewrite Int.unsigned_repr in Hi.
      2: change Int.max_unsigned with 4294967295; Psatz.lia.
      destruct (zlt (Int.unsigned i)); eq_some_inv. clear Hi.
      specialize (Hperm (Int.unsigned i)).
      eapply Hperm.
      hsplit. split. apply Int.unsigned_range. Psatz.lia.
    Qed.

    Fixpoint nconvert_def_pre (pe: pexpr T.elt) : Prop :=
      match pe with
      | PEvar v _ => ρC(v) ≠ Vundef
      | PElocal i => ε(i) ≠ None
      | PEconst (Some (Oaddrsymbol i _)) _ =>
        Genv.find_symbol ge iNone
      | PEconst _ _ => True
      | PEunop u pe' _ =>
        nconvert_def_pre pe'
      | PEbinop b pe1 pe2 _ =>
        nconvert_def_pre pe1
        nconvert_def_pre pe2
      end.

    Lemma nconvert_def (NM: ρ ∈ γ nm) pt (PT: ρCpoints_to_gamma ge ((tmp, ε) :: σ) pt) pe :
      nconvert_def_pre pe
      ∀ ne, nconvert pt pe = inl ne
      ¬ error_mexpr ρ ne
      ¬ error_pexpr ge m ρC ε pe.
Proof.
      induction pe; simpl; auto; intros PRE ne.
    - destruct o; intros K; eq_some_inv. subst ne.
      intros _. destruct c; auto.
    - specialize (IHpe PRE).
      pose proof (@pexpr_get_ty_ok _ _ _ ge m ρC ε pe) as TY.
      simpl.
      intros K NB.
      destruct (well_typed_unop _ _) eqn: Hwt. 2: eq_some_inv.
      destruct (nconvert _ _) as [ ne' | ] eqn: Hne; eq_some_inv. subst ne.
      asserterror_mexpr ρ ne') as NB' by (intro; elim NB; vauto).
      specialize (IHpe _ eq_refl NB').
      intros [ B | (? & EV & B) ].
      exact (IHpe B).
      assert (DEF := error_pexpr_def IHpe EV).
      specialize (TY _ EV DEF).
      destruct u; apply proj_sumbool_true in Hwt;
      rewrite <- Hwt in TY;
      match goal with
      | EV : eval_pexpr _ _ _ _ _ ?i,
        B : error_unop _ _ |- _ =>
        destruct i; destruct TY;
        try (inversion B; intuition eauto; discriminate);
        let CPT := fresh in
        edestruct (nconvert_correct _ _ EV _ PT _ Hne) as (? & CPT & ? & _); eauto;
        simpl in CPT; subs; inversion B; intuition eauto;
        apply NB; vauto
      end.
    - assert (nconvert_def_pre pe1) as PRE1 by apply PRE.
      specialize (IHpe1 PRE1). clear PRE1.
      assert (nconvert_def_pre pe2) as PRE2 by apply PRE.
      specialize (IHpe2 PRE2). clear PRE2.
      pose proof (@pexpr_get_ty_ok _ _ _ ge m ρC ε pe1) as TY1.
      pose proof (@pexpr_get_ty_ok _ _ _ ge m ρC ε pe2) as TY2.
      simpl.
      generalize dependent (pexpr_get_ty pe2). intros ty2.
      generalize dependent (pexpr_get_ty pe1). intros ty1.
      generalize dependent b; intros b.
      apply nbc_classify_intro;
        [ intros o x y TY1 TY2 H; exact (inl_not_inr (eq_sym H)_) | .. ];
      (intros c TY1 TY2 K NB X || intros TY1 TY2 K NB X); revert X;
      destruct (nconvert _ pe1) as [ ne1 | ] eqn: ME1; eq_some_inv;
      destruct (nconvert _ pe2) as [ ne2 | ] eqn: ME2; eq_some_inv;

      repeat match goal with
             | H : inr _ = inl _ |- _ => exact (inl_not_inr (eq_sym K) _)
             | H : (if is_null ?p then _ else _) = inl _ |- _ =>
               destruct (is_null p) eqn: Hnull
             | H : (if noerror ?ne ?nm then _ else _) = inl _ |- _ =>
               let K := fresh in
               destruct (noerror ne nm) eqn: K; [
                   pose proof (noerror_correct nm NM K)
                 | ]
             | H : match pt_eval_pexpr _ _ _ ?pe with All => _ | _ => _ end = inl _ |- _ =>
               destruct (pt_eval_pexpr _ _ _ pe) eqn: ?
             | H : match ?c with Ceq => _ | _ => _ end = inl _ |- _ =>
               destruct c
             | H : (if is_valid_ptr _ _ ?me then _ else _) = inl _ |- _ =>
               destruct (is_valid_ptr _ _ me) eqn: ?
             | H : match cmp_blockset ?x ?y with Contradiction => _ | _ => _ end = inl _ |- _ =>
               destruct (cmp_blockset x y) eqn: ?
             end;
      eq_some_inv; subst ne; subs;
      asserterror_mexpr ρ ne1) as NB1 by (assumption || intro; apply NB; vauto);
      specialize (IHpe1 _ eq_refl NB1); clear NB1;
      specialize (IHpe2 _ eq_refl);
      intros [ B | ( ? & EV1 & [ B | (? & EV2 & B ) ] ) ];
      eauto;
      match goal with
      | EV1: eval_pexpr _ _ _ _ pe1 ?i1 |- _ =>
        assert (DEF1 := error_pexpr_def IHpe1 EV1);
        specialize (TY1 _ EV1 DEF1);
        destruct i1; destruct TY1;
        let T := fresh in
        destruct (nconvert_correct pe1 _ EV1 _ PT _ ME1) as (? & T & ? & _);[ easy | simpl in T ]
      end;
      asserterror_mexpr ρ ne2) as NB2 by (assumption || intro; apply NB; vauto);
      specialize (IHpe2 NB2); clear NB2;
      eauto;
      match goal with
      | EV2: eval_pexpr _ _ _ _ pe2 ?i2 |- _ =>
        assert (DEF2 := error_pexpr_def IHpe2 EV2);
        specialize (TY2 _ EV2 DEF2);
        destruct i2; destruct TY2;
        let T := fresh in
        destruct (nconvert_correct pe2 _ EV2 _ PT _ ME2) as (? & T & ? & _);[ easy | simpl in T ]
      end;
      try (inversion B; auto; subs; apply NB; vauto2).
      Ltac q NM PT :=
      subs;
      repeat match goal with
      | H : pt_eval_pexpr _ _ _ ?pe = _, EV: eval_pexpr _ _ _ _ ?pe _ |- _ =>
        generalize (pt_eval_pexpr_correct eq_refl PT EV);
          rewrite H; clear H; intros (? & ? & ?)
      | H : cmp_blockset ?x ?y = _, X : _, Y : _ |- _ =>
        generalize (cmp_blockset_correct x y _ _ X Y); rewrite H; clear H; intro
      | H : is_valid_ptr ?w ?bs ?ne = true, X : _, Y : _, Z : eval_mexpr _ ?ne _ |- _ =>
        generalize (is_valid_ptr_valid NM w bs ne H _ X _ Y _ Z); clear H; intro H
      | H : is_null ?me = true, EV : eval_mexpr _ ?me _ |- _ =>
        generalize (is_null_correct NumDom nm NM H EV); clear H; intro H
      end; hsplit; subs.
      q NM PT. inversion B; auto; congruence.
      q NM PT. inversion B; auto; try congruence.
      unfold Mem.weak_valid_pointer in *. intuition congruence.
      q NM PT. inversion B; auto; try congruence.
      intuition congruence. subs.
      repeat match goal with X : Mem.valid_pointer _ _ _ = true |- _ => rewrite X in * end.
      simpl in *; intuition eq_some_inv.
      q NM PT. inversion B; auto; try congruence.
      intuition congruence. subs.
      repeat match goal with X : Mem.valid_pointer _ _ _ = true |- _ => rewrite X in * end.
      simpl in *; intuition eq_some_inv.
      q NM PT. inversion B; auto; try congruence.
      q NM PT. inversion B; clear B; auto; try congruence. discriminate.
      unfold Mem.weak_valid_pointer in *. intuition congruence.
      q NM PT. inversion B; auto; try congruence. discriminate.
      unfold Mem.weak_valid_pointer in *. intuition congruence.
      q NM PT. inversion B; auto; try congruence. discriminate.
      unfold Mem.weak_valid_pointer in *. intuition congruence.
      q NM PT. inversion B; auto; try congruence. discriminate.
      unfold Mem.weak_valid_pointer in *. intuition congruence.
    Qed.

  End nconvert.

  Import Utf8.

  Local Instance TeltEqDec : EqDec T.elt := T.elt_eq.
  Lemma compat_upd var `{EQ: EqDec var} f ρC ρ :
    (∀ x y, xyf xf y) →
    compat var f ρC ρ →
    ∀ x v n ρC',
      ncompat v n
      ρC' ∈ upd_spec ρC x v
      compat var f ρC' (upd ρ (f x) n).
Proof.
    intros INJ H x v n ρC' V UPD c. rewrite (UPD c). clear UPD.
    unfold upd. simpl.
    destruct (eq_dec c x). subst. rewrite dec_eq_true. assumption.
    rewrite dec_eq_false; auto.
  Qed.

End Nconvert.