Module ValueDomain


Require Import Coqlib.
Require Import Zwf.
Require Import Maps.
Require Import Compopts.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import ExprEval Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Lattice.
Require Import Kildall.
Require Import Registers.
Require Import RTL.
Require Import Values_symbolic.
Require Import Values_symbolictype.
Require Import Setoid.
Require Import Classical.

Inductive block_class : Type :=
  | BCinvalid
  | BCglob (id: ident)
  | BCstack
  | BCother.

Definition block_class_eq: forall (x y: block_class), {x=y} + {x<>y}.
Proof.
decide equality. apply peq. Defined.

Record block_classification : Type := BC {
  bc_img :> block -> block_class;
  bc_stack: forall b1 b2, bc_img b1 = BCstack -> bc_img b2 = BCstack -> b1 = b2;
  bc_glob: forall b1 b2 id, bc_img b1 = BCglob id -> bc_img b2 = BCglob id -> b1 = b2
}.

Definition bc_below (bc: block_classification) (bound: block) : Prop :=
  forall b, bc b <> BCinvalid -> Plt b bound.

Lemma bc_below_invalid:
  forall b bc bound, ~Plt b bound -> bc_below bc bound -> bc b = BCinvalid.
Proof.
  intros. destruct (block_class_eq (bc b) BCinvalid); auto.
  elim H. apply H0; auto.
Qed.

Hint Extern 2 (_ = _) => congruence: va.
Hint Extern 2 (_ <> _) => congruence : va.
Hint Extern 2 (_ < _) => xomega : va.
Hint Extern 2 (_ <= _) => xomega : va.
Hint Extern 2 (_ > _) => xomega : va.
Hint Extern 2 (_ >= _) => xomega : va.

Hint Extern 2 (_ = _) => congruence : va.
Hint Extern 2 (_ <> _) => congruence : va.
Hint Extern 2 (_ < _) => xomega : va.
Hint Extern 2 (_ <= _) => xomega : va.
Hint Extern 2 (_ > _) => xomega : va.
Hint Extern 2 (_ >= _) => xomega : va.


Definition val_no_ptr (v : val) : bool :=
  match v with
    | Vptr _ _ => false
    | _ => true
  end.

Inductive is_unop_trans : (expr_sym -> expr_sym) -> Prop :=
| is_unop_id : is_unop_trans (fun x => x)
| is_unop_const : forall v, val_no_ptr v = true -> is_unop_trans (fun x => Eval v)
| is_unop_eundef : forall b i, is_unop_trans (fun x => Eundef b i)
| is_unop_eunop : forall o s f
                           (Hunop : is_unop_trans f),
                      is_unop_trans (fun x => Eunop o s (f x))
| is_unop_ebinop : forall o s1 s2 f1 f2
                           (Hbinop1 : is_unop_trans f1)
                           (Hbinop2 : is_unop_trans f2),
                           is_unop_trans (fun x => Ebinop o s1 s2 (f1 x) (f2 x)).

Inductive is_binop_trans : (expr_sym -> expr_sym -> expr_sym) -> Prop :=
| is_binop_proj_1 : is_binop_trans (fun x y => x)
| is_binop_proj_2 : is_binop_trans (fun x y => y)
| is_binop_const : forall v, val_no_ptr v = true -> is_binop_trans (fun x y => Eval v)
| is_binop_eundef : forall b i, is_binop_trans (fun x y => Eundef b i)
| is_binop_eunop : forall o s f
                           (Hunop : is_binop_trans f),
                      is_binop_trans (fun x y => Eunop o s (f x y))
| is_binop_ebinop : forall o s1 s2 f1 f2
                           (Hbinop1 : is_binop_trans f1)
                           (Hbinop2 : is_binop_trans f2),
                           is_binop_trans (fun x y => Ebinop o s1 s2 (f1 x y) (f2 x y)).

Section MATCH.
Import NormaliseSpec.

Variable bc: block_classification.

Record same_except (b : block) (cm cm' : block -> int) : Prop :=
  {
    SAME : forall b', b <> b' -> cm b' = cm' b';
    DIFF : cm b <> cm' b
  }.

Definition no_forgery (mx :Z) (bound : block -> Z * Z) (align : block -> int) : Prop :=
  forall b, exists cm1, compat mx bound align cm1 /\
               exists cm2, compat mx bound align cm2 /\ same_except b cm1 cm2.


Concretisation of a constant
Import ExprEval.


Instance EquivExpr : Equivalence same_eval.
Proof.
  unfold same_eval.
  constructor; simpl.
  -
    unfold Reflexive.
    reflexivity.
  -
    unfold Symmetric.
    intuition.
  -
    unfold Transitive.
    intuition.
Qed.

Definition is_pointer (b : block) (ofs : int) (e : expr_sym) : Prop :=
  same_eval (Eval (Vptr b ofs)) e.

Definition is_constant (v : val) (e : expr_sym) : Prop :=
  same_eval (Eval v) e.



Add Parametric Morphism : is_pointer with signature ((@eq block) ==> @eq int ==> same_eval ==> iff) as is_pointer_same_eval_morph.
Proof.
  unfold is_pointer.
  intros.
  unfold same_eval ; split ; intros.
  rewrite <- H ; eauto.
  rewrite H ; eauto.
Qed.


Add Parametric Morphism : is_constant with signature ((@eq val) ==> same_eval ==> iff) as is_constant_same_eval_morph.
Proof.
  unfold is_constant.
  intros.
  unfold same_eval ; intuition.
Qed.

Add Parametric Morphism (o : binop_t) (t t' : styp) : (Ebinop o t t') with signature same_eval ==> same_eval ==> same_eval as binop_same_eval.
Proof.
  intros.
  unfold same_eval in *.
  intros.
  simpl.
  erewrite H0; eauto.
  erewrite H ; eauto.
Qed.

Add Parametric Morphism (o : unop_t) (t : styp) : (Eunop o t) with signature same_eval ==> same_eval as unop_same_eval.
Proof.
  unfold same_eval.
  intros.
  simpl.
  erewrite H; eauto.
Qed.

Abstracting the result of conditions (type option bool)


Inductive abool :=
  | Bnone (* always None (undefined) *)
  | Just (b: bool) (* always Some b (defined and known to be b) *)
  | Maybe (b: bool) (* either None or Some b (known to be b if defined) *)
  | Btop. (* unknown, all results are possible *)


Inductive cmatch: option bool -> abool -> Prop :=
  | cmatch_none: cmatch None Bnone
  | cmatch_just: forall b, cmatch (Some b) (Just b)
  | cmatch_maybe_none: forall b, cmatch None (Maybe b)
  | cmatch_maybe_some: forall b, cmatch (Some b) (Maybe b)
  | cmatch_top: forall ob, cmatch ob Btop.


Definition is_wk_constant (v : val) (e : expr_sym) : Prop :=
  forall a u,
    Values.Val.lessdef (eSexpr a u e) (eSval a v).


Definition is_bool (e : expr_sym) : Prop :=
  forall a u,
  exists i, Values.Val.lessdef (eSexpr a u e) (Vint i) /\
            (i = Int.zero \/ i = Int.one).


Definition val_of_bool (b:bool) :=
  if b then Vtrue else Vfalse.

Inductive ecmatch: expr_sym -> abool -> Prop :=
| ecmatch_none : forall e, is_constant Vundef e -> ecmatch e Bnone
| ecmatch_just : forall e b, is_constant (val_of_bool b) e -> ecmatch e (Just b)
| ecmatch_maybe : forall e b, is_wk_constant (val_of_bool b) e -> ecmatch e (Maybe b)
| ecmatch_top : forall e, is_bool e -> ecmatch e Btop.

Ltac rew_cst H :=
  unfold is_constant, is_pointer in H ;
  erewrite <- H in *; eauto.

Lemma is_constant_refl : forall v, is_constant v (Eval v).
Proof.
  repeat intro.
  reflexivity.
Qed.

Add Parametric Morphism : is_wk_constant with signature ((@eq val) ==> same_eval ==> iff) as is_wk_constant_same_eval_morph.
Proof.
  assert ( forall (y : val) (x y0 : expr_sym),
               same_eval x y0 -> (is_wk_constant y x -> is_wk_constant y y0)).
  {
    intros.
    unfold is_wk_constant in *.
    intros.
    rewrite <- H.
    eauto.
    }
  intros.
  split;
  apply H; auto.
  rewrite H0 ; reflexivity.
Qed.


Add Parametric Morphism : is_bool with signature (same_eval ==> iff) as is_bool_same_eval_morph.
Proof.
  assert (forall x y : expr_sym, same_eval x y -> (is_bool x -> is_bool y)).
  {
    intros.
    unfold is_bool in *.
    intros.
    destruct (H0 a u).
    exists x0 ; split ; auto.
    erewrite <- H; eauto. tauto.
    intuition.
  }
  intuition ; eapply H ; eauto.
  rewrite H0 ; auto.
  reflexivity.
Qed.
  
  
Add Parametric Morphism : ecmatch with signature (same_eval ==> @eq abool ==> iff) as cmatch_morph.
Proof.
  assert (
      forall x y,
        same_eval x y -> forall z : abool, ecmatch x z -> ecmatch y z).
  {
    intros.
    inv H0 ; try constructor;
    try (rewrite H in H1; auto; fail).
  }
  intros ; split ; apply H; auto.
  rewrite H0 ; reflexivity.
Qed.

Hint Constructors cmatch : va.

Definition club (x y: abool) : abool :=
  match x, y with
  | Bnone, Bnone => Bnone
  | Bnone, (Just b | Maybe b) => Maybe b
  | (Just b | Maybe b), Bnone => Maybe b
  | Just b1, Just b2 => if eqb b1 b2 then x else Btop
  | Maybe b1, Maybe b2 => if eqb b1 b2 then x else Btop
  | Maybe b1, Just b2 => if eqb b1 b2 then x else Btop
  | Just b1, Maybe b2 => if eqb b1 b2 then y else Btop
  | _, _ => Btop
  end.

Definition cge (b1 : abool) (b2 : abool) : Prop :=
  match b1, b2 with
    | Btop , _ => True
    | _ , Btop => False
    | Maybe x , (Maybe y | Just y) => x = y
    | Maybe _ , Bnone => True
    | _ , _ => b1 = b2
  end.


Ltac case_match :=
  match goal with
    | |- context[match ?X with
                   | _ => _
                 end] => case_eq X
  end.

Lemma is_bool_undef :
   is_bool (Eval Vundef).
Proof.
  repeat intro.
  exists Int.zero ; intuition constructor.
Qed.

Lemma is_bool_true :
   is_bool (Eval Vtrue).
Proof.
  repeat intro.
  exists Int.one ; intuition constructor.
Qed.

Lemma is_bool_false :
   is_bool (Eval Vfalse).
Proof.
  repeat intro.
  exists Int.zero ; intuition constructor.
Qed.

Lemma is_bool_val_of_bool :
  forall b,
    is_bool (Eval (val_of_bool b)).
Proof.
  repeat intro.
  destruct b ; simpl.
  exists Int.one ; intuition constructor.
  exists Int.zero ; intuition constructor.
Qed.

Lemma is_wk_constant_is_bool :
  forall b e,
    is_wk_constant (val_of_bool b) e ->
   is_bool e.
Proof.
  repeat intro.
  specialize (H a u).
  inv H.
  rewrite H2.
  destruct b ; [exists Int.one | exists Int.zero] ; intuition constructor.
  exists Int.zero ; intuition constructor.
Qed.


Hint Resolve is_bool_undef is_bool_true is_bool_false is_bool_val_of_bool is_wk_constant_is_bool : va.



Lemma ecmatch_cge :
  forall e x y,
    ecmatch e x -> cge y x -> ecmatch e y.
Proof.
  intros.
  destruct x ; destruct y ; simpl in H0 ; inv H ;
  try congruence ; try constructor ; unfold is_wk_constant ; intros ; eauto ; try tauto.
  -
    rew_cst H1 ; auto.
  -
    rew_cst H1.
    auto with va.
  -
    inv H0 ; auto.
  -
    rew_cst H3; auto.
  -
    rew_cst H3.
    auto with va.
  -
    eauto with va.
Qed.

Lemma club_ge_l : forall x y,
                  cge (club x y) x.
Proof.
  intros.
  case_eq x ; case_eq y ; simpl ; try tauto; intros; case_match ; simpl ; auto.
  intros.
  symmetry.
  apply eqb_prop ; auto.
Qed.


Lemma ecmatch_lub_l:
  forall ob x y, ecmatch ob x -> ecmatch ob (club x y).
Proof.
  intros.
  eapply ecmatch_cge ; eauto.
  apply club_ge_l.
Qed.

Lemma club_sym : forall x y, club x y = club y x.
Proof.
  intros.
  destruct x ; destruct y ; try reflexivity; simpl; rewrite Fcore_Raux.eqb_sym; case_match ; try reflexivity.
  - intros.
    apply eqb_prop in H ; congruence.
  -
    intros.
    apply eqb_prop in H ; congruence.
Qed.


Lemma ecmatch_lub_r:
  forall ob x y, ecmatch ob y -> ecmatch ob (club x y).
Proof.
  intros.
  eapply ecmatch_cge ; eauto.
  rewrite club_sym.
  apply club_ge_l.
Qed.

Definition cnot (x: abool) : abool :=
  match x with
  | Just b => Just (negb b)
  | Maybe b => Maybe (negb b)
  | _ => x
  end.


Lemma cnot_sound:
  forall ob x, cmatch ob x -> cmatch (option_map negb ob) (cnot x).
Proof.
  destruct 1; constructor.
Qed.

Lemma ecnot_sound:
  forall ob x, ecmatch ob x -> ecmatch (Val.notbool ob) (cnot x).
Proof.
  intros.
  inv H ; simpl ; try constructor.
  -
    unfold Val.notbool.
    rew_cst H0.
    repeat intro; reflexivity.
  -
    unfold Val.notbool.
    rew_cst H0.
    destruct b ; constructor.
  -
    unfold Val.notbool.
    unfold is_wk_constant in * ; intros.
    specialize (H0 a u).
    simpl.
    inv H0.
    rewrite H2.
    destruct b ; simpl ; constructor.
    simpl ; constructor.
  -
    unfold Val.notbool.
    repeat intro ; simpl.
    destruct (H0 a u).
    exists (Int.notbool x).
    destruct H.
    inv H.
    rewrite H4.
    intuition subst ; simpl ; constructor.
    intuition subst ; simpl ; constructor.
Qed.

Abstracting pointers


Inductive aptr : Type :=
  | Pbot (* bottom (empty set of expressions) *)
  | Pcst (* independant from memory *)
  | Gl (id: ident) (ofs: int) (* pointer into the block for global variable id at offset ofs *)
  | Glo (id: ident) (* pointer anywhere into the block for global id *)
  | Glob (* pointer into any global variable *)
  | Stk (ofs: int) (* pointer into the current stack frame at offset ofs *)
  | Stack (* pointer anywhere into the current stack frame *)
  | Nonstack (* pointer anywhere but into the current stack frame *)
  | Ptop. (* any valid pointer *)

Definition eq_aptr: forall (p1 p2: aptr), {p1=p2} + {p1<>p2}.
Proof.
  intros. generalize ident_eq, Int.eq_dec; intros. decide equality.
Defined.

Inductive pmatch (b: block) (ofs: int): aptr -> Prop :=
| pmatch_gl: forall id,
               bc b = BCglob id ->
               pmatch b ofs (Gl id ofs)
| pmatch_glo: forall id,
                bc b = BCglob id ->
                pmatch b ofs (Glo id)
| pmatch_glob: forall id,
                 bc b = BCglob id ->
                 pmatch b ofs Glob
| pmatch_stk:
    bc b = BCstack ->
    pmatch b ofs (Stk ofs)
| pmatch_stack:
    bc b = BCstack ->
    pmatch b ofs Stack
| pmatch_nonstack:
    bc b <> BCstack -> bc b <> BCinvalid ->
    pmatch b ofs Nonstack
| pmatch_top:
    bc b <> BCinvalid ->
    pmatch b ofs Ptop.

Definition singleton (b:block) : block -> Prop :=
  fun b' => b = b'.

Definition depends_on_block (b : block) (e : expr_sym) :=
  depends_on_blocks (singleton b) e.

Definition depends_on_nothing (e : expr_sym) :=
  depends_on_blocks (fun _ => False) e.

Inductive epmatch : expr_sym -> aptr -> Prop :=
| epmatch_cst : forall e, depends_on_nothing e -> epmatch e Pcst
| epmatch_gl: forall id b ofs e,
                bc b = BCglob id ->
                is_pointer b ofs e ->
                epmatch e (Gl id ofs)
| epmatch_glo: forall id e,
                 depends_on_blocks (fun b => bc b = BCglob id) e ->
                 epmatch e (Glo id)
| epmatch_glob: forall e,
                  depends_on_blocks (fun b => exists id, bc b = BCglob id) e ->
                  epmatch e Glob
| epmatch_stk: forall b ofs e,
                 bc b = BCstack ->
                 is_pointer b ofs e ->
                 epmatch e (Stk ofs)
| epmatch_stack: forall e,
                   depends_on_blocks (fun b => bc b = BCstack) e ->
                   epmatch e Stack
| epmatch_nonstack: forall e,
                      depends_on_blocks
                        (fun b =>
                           bc b <> BCstack /\ bc b <> BCinvalid) e ->
                      epmatch e Nonstack
| epmatch_top: forall e,
                 depends_on_blocks (fun b => bc b <> BCinvalid) e ->
                 epmatch e Ptop.

Hint Constructors pmatch: va.
Hint Constructors epmatch: va.

Inductive pge: aptr -> aptr -> Prop :=
  | pge_top: forall p, pge Ptop p
  | pge_bot: forall p, pge p Pbot
  | pge_refl: forall p, pge p p
  | pge_glo_gl: forall id ofs, pge (Glo id) (Gl id ofs)
  | pge_glob_gl: forall id ofs, pge Glob (Gl id ofs)
  | pge_glob_glo: forall id, pge Glob (Glo id)
  | pge_ns_gl: forall id ofs, pge Nonstack (Gl id ofs)
  | pge_ns_glo: forall id, pge Nonstack (Glo id)
  | pge_ns_glob: pge Nonstack Glob
  | pge_stack_stk: forall ofs, pge Stack (Stk ofs).

Hint Constructors pge: va.

Lemma pge_trans:
  forall p q, pge p q -> forall r, pge q r -> pge p r.
Proof.
  induction 1; intros r PM; inv PM; auto with va.
Qed.

Lemma pmatch_ge:
  forall b ofs p q, pge p q -> pmatch b ofs q -> pmatch b ofs p.
Proof.
  induction 1; intros PM; inv PM; eauto with va.
Qed.


Lemma eSexpr_same :
  forall A A' E e,
  (forall b, block_appears e b -> A b = A' b) ->
  eSexpr A E e = eSexpr A' E e.
Proof.
  induction e ; simpl; auto.
  - destruct v ; try tauto.
    simpl.
    intros.
    rewrite H ; auto.
  -
    intros.
    rewrite IHe ; auto.
  -
    intros.
    rewrite IHe1 ; auto.
    rewrite IHe2 ; auto.
Qed.
    

Definition deps_of_val (v : val) : block -> Prop :=
  match v with
    | Vptr b ofs => singleton b
    | _ => (fun _ => False)
  end.
                              
Add Parametric Morphism (S : block -> Prop) : (depends_on_blocks S) with
    signature same_eval ==> iff as depends_on_blocks_same_eval.
Proof.
  unfold depends_on_blocks.
  unfold same_eval ; intuition.
  repeat erewrite <- H ; eauto.
  repeat erewrite H ; eauto.
Qed.


Lemma is_constant_depends :
  forall v e, is_constant v e -> depends_on_blocks (deps_of_val v) e.
Proof.
  intros.
  unfold is_constant in H.
  rewrite <- H.
  repeat intro.
  destruct v ; simpl ; try reflexivity.
  rewrite H0; auto.
  simpl. unfold singleton; auto.
Qed.

Lemma is_pointer_depends :
  forall b o e, is_pointer b o e -> depends_on_blocks (singleton b) e.
Proof.
  intros.
  unfold is_pointer in H.
  rewrite <- H.
  repeat intro.
  simpl.
  rewrite H0. reflexivity.
  unfold singleton; auto.
Qed.

Lemma depends_on_blocks_le :
  forall (S S': block -> Prop) e,
    (forall b, S b -> S' b) ->
  depends_on_blocks S e -> depends_on_blocks S' e.
Proof.
  unfold depends_on_blocks.
  intros.
  eapply H0 ; eauto.
Qed.

Lemma depends_on_blocks_appears :
  forall (S: block -> Prop) e,
  (forall b, (block_appears e b -> S b)) ->
  depends_on_blocks S e.
Proof.
  unfold depends_on_blocks.
  intros.
  induction e ; simpl ; try reflexivity.
  -
    destruct v ; simpl in * ; try reflexivity.
    rewrite H0 ; auto.
  -
    rewrite IHe ; auto.
  -
    simpl in H.
    rewrite IHe1; auto.
    rewrite IHe2 ; auto.
Qed.
    
Add Parametric Morphism : epmatch with signature same_eval ==> @eq aptr ==> iff as epmatch_same_eval.
Proof.
  assert (forall x y, same_eval x y -> forall ptr, epmatch x ptr -> epmatch y ptr).
  {
    intros.
    inv H0; rewrite H in * ; econstructor ; eauto.
  }
  intros.
  intuition.
  eapply H ; eauto.
  eapply H ; eauto.
  rewrite H0 ; auto.
  reflexivity.
Qed.



Lemma depends_binop :
  forall (S: block -> Prop) o t t' e1 e2,
    depends_on_blocks S e1 ->
    depends_on_blocks S e2 ->
    depends_on_blocks S (Ebinop o t t' e1 e2).
Proof.
  unfold depends_on_blocks ; simpl.
  intros.
  erewrite H with (a':=a');eauto.
  erewrite H0 with (a':=a'); eauto.
Qed.

Lemma depends_unop :
  forall (S: block -> Prop) o t e1,
    depends_on_blocks S e1 ->
    depends_on_blocks S (Eunop o t e1).
Proof.
  unfold depends_on_blocks ; simpl.
  intros.
  erewrite H with (a':=a'); eauto.
Qed.



Ltac is_constant_depends :=
  match goal with
    | H : is_constant ?V ?E |- depends_on_blocks ?S ?E =>
      apply is_constant_depends in H
  end.

Ltac is_pointer_depends :=
  match goal with
    | H : is_pointer ?B ?O ?E |- depends_on_blocks ?S ?E =>
      apply is_pointer_depends in H
  end.


Ltac depends_on_blocks_le :=
  match goal with
    | H : depends_on_blocks ?S1 ?E |- depends_on_blocks ?S' ?E =>
      apply depends_on_blocks_le with (S:= S1)
  end.



Lemma depends_on_blocks_const :
  forall v S,
    val_no_ptr v = true ->
    depends_on_blocks S (Eval v).
Proof.
  intros.
  apply depends_on_blocks_appears.
  destruct v ; simpl in * ; intuition congruence.
Qed.



Ltac depends_on_blocks_const :=
  match goal with
    | |- depends_on_blocks _ (Eval ?V) =>
      let v := (eval compute in (val_no_ptr V)) in
      match v with
        | true => apply depends_on_blocks_const ; reflexivity
        | false => fail
      end
  end.


Ltac depends_prf :=
  unfold depends_on_nothing, depends_on_block in *;
  try (apply depends_binop; eauto);
  try (apply depends_unop ; eauto);
  (try is_constant_depends) ;
  (try is_pointer_depends) ;
  try (depends_on_blocks_const);
  try depends_on_blocks_le ; simpl; intros ;
  unfold singleton in * ; try tauto.

Hint Extern 2 (depends_on_blocks _ _) => depends_prf : va.

Lemma epmatch_top_def :
  forall v p,
    epmatch v p ->
    epmatch v Ptop.
Proof.
  intros; constructor.
  inv H; depends_prf; try congruence.
  destruct H ; congruence.
Qed.

Lemma epmatch_bot_def :
  forall v p,
    epmatch v Pbot ->
    epmatch v p.
Proof.
  intros.
  inv H.
Qed.

Definition epge (p q : aptr) : Prop :=
  match p, q with
    | Ptop , _ => True
    | Nonstack , (Nonstack| Glob | Glo _ | Gl _ _ | Pcst | Pbot) => True
    | Glob , (Glob | Glo _ | Gl _ _ | Pcst | Pbot) => True
    | Glo id , (Glo id' | Gl id' _) => id = id'
    | Glo _ , Pcst => True
    | Gl id o , Gl id' o' => id = id' /\ o = o'
    | Stack , (Stack | Stk _ | Pcst ) => True
    | Stk o , Stk o' => o = o'
    | Pbot , Pbot => True
    | _ , Pbot => True
    | Pbot , _ => False
    | Pcst , Pcst => True
    | _ , _ => False
  end.
      
Lemma epge_trans :
  forall p q r,
    epge p q -> epge q r -> epge p r.
Proof.
  intros.
  destruct p ; destruct q ; destruct r ; try (simpl in * ; intuition congruence).
Qed.
  
Lemma epmatch_ge:
  forall e p q, epge p q -> epmatch e q -> epmatch e p.
Proof.
  intros.
  destruct p, q ; simpl in H ; inv H0 ; try tauto; eauto with va.
  -
    intuition subst.
    econstructor; eauto.
  -
    econstructor ; depends_prf.
    exists id ; congruence.
  -
    econstructor ; depends_prf.
    destruct H0 ; intuition.
  -
    constructor ; depends_prf.
    destruct H0 ; intuition.
Qed.

Lemma epmatch_top': forall e p, epmatch e p -> epmatch e Ptop.
Proof.
  intros. apply epmatch_ge with p; auto with va.
  simpl ; exact I.
Qed.

Definition plub (p q: aptr) : aptr :=
  match p, q with
  | Pbot, _ => q
  | _, Pbot => p
  | Gl id1 ofs1, Gl id2 ofs2 =>
      if ident_eq id1 id2 then if Int.eq_dec ofs1 ofs2 then p else Glo id1 else Glob
  | Gl id1 ofs1, Glo id2 =>
      if ident_eq id1 id2 then q else Glob
  | Glo id1, Gl id2 ofs2 =>
      if ident_eq id1 id2 then p else Glob
  | Glo id1, Glo id2 =>
      if ident_eq id1 id2 then p else Glob
  | (Gl _ _ | Glo _ | Glob), Glob => Glob
  | Glob, (Gl _ _ | Glo _) => Glob
  | (Gl _ _ | Glo _ | Glob | Nonstack), Nonstack =>
      Nonstack
  | Nonstack, (Gl _ _ | Glo _ | Glob) =>
      Nonstack
  | Stk ofs1, Stk ofs2 =>
      if Int.eq_dec ofs1 ofs2 then p else Stack
  | (Stk _ | Stack), Stack =>
      Stack
  | Stack, Stk _ =>
      Stack
  | _, _ => Ptop
  end.


Definition eplub (p q: aptr) : aptr :=
  match p, q with
  | Pbot, _ => q
  | _, Pbot => p
  | Pcst , Pcst => Pcst
  | Pcst , Gl id _ | Gl id _, Pcst => Glo id
  | Pcst , Glo id | Glo id , Pcst => Glo id
  | Pcst , Glob | Glob , Pcst => Glob
  | Pcst , Stk _ | Stk _ , Pcst => Stack
  | Pcst , Stack | Stack , Pcst => Stack
  | Gl id1 ofs1, Gl id2 ofs2 =>
      if ident_eq id1 id2 then if Int.eq_dec ofs1 ofs2 then p else Glo id1 else Glob
  | Gl id1 ofs1, Glo id2 =>
      if ident_eq id1 id2 then q else Glob
  | Glo id1, Gl id2 ofs2 =>
      if ident_eq id1 id2 then p else Glob
  | Glo id1, Glo id2 =>
      if ident_eq id1 id2 then p else Glob
  | (Gl _ _ | Glo _ | Glob), Glob => Glob
  | Glob, (Gl _ _ | Glo _) => Glob
  | (Gl _ _ | Glo _ | Glob | Nonstack | Pcst), Nonstack =>
      Nonstack
  | Nonstack, (Gl _ _ | Glo _ | Glob | Pcst) =>
      Nonstack
  | Stk ofs1, Stk ofs2 =>
      if Int.eq_dec ofs1 ofs2 then p else Stack
  | (Stk _ | Stack), Stack =>
      Stack
  | Stack, Stk _ =>
      Stack
  | _ , _ => Ptop
  end.

Lemma eplub_comm:
  forall p q, eplub p q = eplub q p.
Proof.
  intros; unfold eplub; destruct p; destruct q; auto.
  destruct (ident_eq id id0). subst id0.
  rewrite dec_eq_true.
  destruct (Int.eq_dec ofs ofs0). subst ofs0. rewrite dec_eq_true. auto.
  rewrite dec_eq_false by auto. auto.
  rewrite dec_eq_false by auto. auto.
  destruct (ident_eq id id0). subst id0.
  rewrite dec_eq_true; auto.
  rewrite dec_eq_false; auto.
  destruct (ident_eq id id0). subst id0.
  rewrite dec_eq_true; auto.
  rewrite dec_eq_false; auto.
  destruct (ident_eq id id0). subst id0.
  rewrite dec_eq_true; auto.
  rewrite dec_eq_false; auto.
  destruct (Int.eq_dec ofs ofs0). subst ofs0. rewrite dec_eq_true; auto.
  rewrite dec_eq_false; auto.
Qed.



Lemma epge_lub_l:
  forall p q, epge (eplub p q) p.
Proof.
  unfold eplub; destruct p, q; auto with va ; try (simpl ; auto; fail);
  repeat case_match ; try (simpl;intuition; fail).
Qed.

Lemma epge_lub_r:
  forall p q, epge (eplub p q) q.
Proof.
  intros. rewrite eplub_comm. apply epge_lub_l.
Qed.

Lemma epmatch_lub_l:
  forall e p q, epmatch e p -> epmatch e (eplub p q).
Proof.
  intros. eapply epmatch_ge; eauto. apply epge_lub_l.
Qed.

Lemma epmatch_lub_r:
  forall e p q, epmatch e q -> epmatch e (eplub p q).
Proof.
  intros. eapply epmatch_ge; eauto. apply epge_lub_r.
Qed.


Lemma eplub_least:
  forall r p q, epge r p -> epge r q -> epge r (eplub p q).
Proof.
  intros.
  destruct r, p, q ; try (simpl in * ; try tauto ; repeat case_match ; intuition congruence).
Qed.

Definition pincl (p q: aptr) : bool :=
  match p, q with
  | Pbot, _ => true
  | Gl id1 ofs1, Gl id2 ofs2 => peq id1 id2 && Int.eq_dec ofs1 ofs2
  | Gl id1 ofs1, Glo id2 => peq id1 id2
  | Glo id1, Glo id2 => peq id1 id2
  | (Gl _ _ | Glo _ | Glob), Glob => true
  | (Gl _ _ | Glo _ | Glob | Nonstack), Nonstack => true
  | Stk ofs1, Stk ofs2 => Int.eq_dec ofs1 ofs2
  | Stk ofs1, Stack => true
  | Stack, Stack => true
  | _, Ptop => true
  | _, _ => false
  end.


Definition ege_bool (p q : aptr) : bool :=
  match p, q with
    | Ptop , _ => true
    | Nonstack , (Nonstack| Glob | Glo _ | Gl _ _ | Pcst | Pbot) => true
    | Glob , (Glob | Glo _ | Gl _ _ | Pcst | Pbot) => true
    | Glo id , (Glo id' | Gl id' _) => peq id id'
    | Glo _ , Pcst => true
    | Gl id o , Gl id' o' => peq id id' && Int.eq_dec o o'
    | Stack , (Stack | Stk _ | Pcst ) => true
    | Stk o , Stk o' => Int.eq_dec o o'
    | Pbot , Pbot => true
    | _ , Pbot => true
    | Pbot , _ => false
    | Pcst , Pcst => true
    | _ , _ => false
  end.

Definition epincl (p q : aptr) : bool := ege_bool q p.

Lemma epincl_ge: forall p q, epincl p q = true -> epge q p.
Proof.
  intros.
  destruct p , q ; simpl in * ; try discriminate ; auto with va;
  InvBooleans; subst; auto with va.
Qed.

Lemma pincl_ge_2: forall p q, epge p q -> epincl q p = true.
Proof.
  destruct p, q ; simpl ; try (intuition congruence).
  - intuition subst.
    rewrite ! proj_sumbool_is_true ; auto.
  - intro ; subst.
    rewrite ! proj_sumbool_is_true; auto.
  - intro ; subst.
    rewrite ! proj_sumbool_is_true; auto.
  -
    destruct (Int.eq_dec ofs ofs0) ; auto.
Qed.

Lemma epincl_sound:
  forall e p q,
  epincl p q = true -> epmatch e p -> epmatch e q.
Proof.
  intros. eapply epmatch_ge; eauto. apply epincl_ge; auto.
Qed.

Lemma depends_is_pointer :
  forall S b ofs align bound (NOFORGERY : no_forgery Int.max_unsigned bound align),
    depends_on_blocks S (Eval (Vptr b ofs)) -> S b.
Proof.
  unfold depends_on_blocks.
  intros. simpl in *.
  assert (NOF := NOFORGERY).
  destruct (NOFORGERY b) as [CM1 [COMPAT1 CM2EQ]].
  destruct (CM2EQ) as [CM2 [COMPAT2 SAMEX]].
  destruct (classic (S b)); auto.
  assert (Vint (Int.add (CM1 b) ofs) = Vint (Int.add (CM2 b) ofs)).
  {
    eapply H; eauto.
    intros.
    destruct (peq b b0) ; subst. tauto.
    apply (SAME _ _ _ SAMEX); auto.
    intros ; apply Byte.zero.
  }
  apply inj_vint in H1.
  rewrite Int.add_commut in H1.
  rewrite (Int.add_commut (CM2 b)) in H1.
  apply int_add_eq_l in H1.
  generalize (DIFF _ _ _ SAMEX); auto. congruence.
Qed.


Lemma depends_on_block_pointer :
  forall (S : block -> Prop) b ofs e
          align bound (NOFORGERY : no_forgery Int.max_unsigned bound align)
  ,
             (S b -> False) ->
       is_pointer b ofs e ->
       depends_on_blocks S e -> False.
Proof.
  repeat intro.
  rew_cst H0.
  eapply depends_is_pointer in H1; eauto.
Qed.

Lemma epincl_not_ge: forall p q, epincl p q = false -> ~ epge q p.
Proof.
 intros.
 intro. destruct p , q ; simpl in * ; try discriminate ; auto with va;
  InvBooleans; subst; auto with va.
  destruct H0 ; subst.
  unfold proj_sumbool in H.
  destruct (peq id id) ; try congruence.
  destruct (Int.eq_dec ofs ofs) ; simpl in * ; try congruence.
  destruct (peq id id) ; simpl in * ; congruence.
  destruct (peq id id) ; simpl in * ; congruence.
  destruct (Int.eq_dec ofs ofs) ; simpl in * ; try congruence.
Qed.

Definition padd (p: aptr) (n: int) : aptr :=
  match p with
  | Gl id ofs => Gl id (Int.add ofs n)
  | Stk ofs => Stk (Int.add ofs n)
  | _ => p
  end.



Ltac seval_prf :=
  unfold is_constant, Val.add, Val.sub in *;
  match goal with
    | H : same_eval ?X ?Y |- same_eval ?Z ?T =>
      match Z with
        | context[X] => rewrite H
        | context[Y] => rewrite <- H
      end
    | H : same_eval ?X ?Y |- same_eval ?Z ?T =>
      match T with
        | context[X] => rewrite H
        | context[Y] => rewrite <- H
      end; repeat intro ; simpl
  end.



Hint Extern 2 (same_eval _ _) => seval_prf : va.
Hint Extern 2 (depends_on_block _ _) => depends_prf : va.
Hint Extern 2 (depends_on_blocks _ _) => depends_prf : va.
 
Lemma is_pointer_add :
  forall b ofs e delta,
    is_pointer b ofs e ->
    is_pointer b (Int.add ofs delta) (Val.add e (Eval (Vint delta))).
Proof.
  unfold is_pointer ; intros.
  unfold Val.add.
  rewrite <- H.
  repeat intro ; simpl.
  rewrite Int.add_assoc.
  reflexivity.
Qed.
  
Lemma epadd_sound:
  forall e p delta,
  epmatch e p ->
  epmatch (Val.add e (Eval (Vint delta))) (padd p delta).
Proof.
  intros. inv H; simpl padd; econstructor ; unfold is_constant in * ; eauto with va.
  -
    depends_prf.
  -
    apply is_pointer_add; auto.
  -
    apply is_pointer_add; auto.
Qed.

Definition psub (p: aptr) (n: int) : aptr :=
  match p with
  | Gl id ofs => Gl id (Int.sub ofs n)
  | Stk ofs => Stk (Int.sub ofs n)
  | _ => p
  end.

Lemma psub_sound:
  forall b ofs p delta,
  pmatch b ofs p ->
  pmatch b (Int.sub ofs delta) (psub p delta).
Proof.
  intros. inv H; simpl psub; eauto with va.
Qed.

Lemma is_pointer_sub :
  forall b ofs e delta,
    is_pointer b ofs e ->
   is_pointer b (Int.sub ofs delta) (Val.sub e (Eval (Vint delta))).
Proof.
  unfold is_pointer ; intros.
  unfold Val.sub.
  rewrite <- H.
  repeat intro ; simpl.
  repeat rewrite Int.sub_add_opp.
  rewrite Int.add_assoc.
  reflexivity.
Qed.

Lemma epsub_sound:
  forall e p delta,
  epmatch e p ->
  epmatch (Val.sub e (Eval (Vint delta))) (psub p delta).
Proof.
  intros. inv H; simpl psub; unfold is_constant in * ; econstructor; eauto with va.
  -
    depends_prf.
  -
    eapply is_pointer_sub ; eauto.
  -
    eapply is_pointer_sub ; eauto.
Qed.


Definition poffset (p: aptr) : aptr :=
  match p with
  | Gl id ofs => Glo id
  | Stk ofs => Stack
  | _ => p
  end.

Lemma poffset_sound :
  forall e p,
    epmatch e p ->
    epmatch e (poffset p).
Proof.
  intros.
  inv H ; constructor ; auto with va.
Qed.

Hint Resolve poffset_sound : va.


Definition psub2 (p q: aptr) : option int :=
  match p, q with
  | Gl id1 ofs1, Gl id2 ofs2 =>
      if peq id1 id2 then Some (Int.sub ofs1 ofs2) else None
  | Stk ofs1, Stk ofs2 =>
      Some (Int.sub ofs1 ofs2)
  | _, _ =>
      None
  end.


Lemma psub2_sound:
  forall b1 ofs1 p1 b2 ofs2 p2 delta,
  psub2 p1 p2 = Some delta ->
  pmatch b1 ofs1 p1 ->
  pmatch b2 ofs2 p2 ->
  b1 = b2 /\ delta = Int.sub ofs1 ofs2.
Proof.
  intros. destruct p1; try discriminate; destruct p2; try discriminate; simpl in H.
- destruct (peq id id0); inv H. inv H0; inv H1.
  split. eapply bc_glob; eauto. reflexivity.
- inv H; inv H0; inv H1. split. eapply bc_stack; eauto. reflexivity.
Qed.

Lemma epsub2_sound:
  forall e1 p1 e2 p2 delta,
    psub2 p1 p2 = Some delta ->
    epmatch e1 p1 ->
    epmatch e2 p2 ->
    is_constant (Vint delta) (Val.sub e1 e2).
Proof.
  intros.
  assert (HDIFF : forall b b' ofs ofs',
                    b = b' ->
                    is_pointer b ofs e1 ->
                    is_pointer b' ofs' e2 ->
                    is_constant (Vint (Int.sub ofs ofs')) (Val.sub e1 e2)).
  {
    unfold is_constant,is_pointer in *.
    unfold Val.sub. intros.
    subst.
    rewrite <- H3.
    rewrite <- H4.
    repeat intro.
    simpl.
    apply f_equal.
    repeat rewrite Int.sub_add_opp.
    rewrite Int.neg_add_distr.
    rewrite (Int.add_commut (cm b')).
    rewrite Int.add_assoc.
    apply f_equal.
    rewrite <- Int.add_assoc.
    rewrite Int.add_neg_zero.
    rewrite Int.add_zero_l.
    reflexivity.
  }
  destruct p1; try discriminate; destruct p2; try discriminate; simpl in H.
  - destruct (peq id id0); inv H. inv H0; inv H1.
    eapply HDIFF with (b:=b) (b':=b0); eauto.
    eapply bc_glob ; eauto.
  -
    inv H; inv H0; inv H1.
    eapply HDIFF with (b:=b) (b':=b0); eauto.
    eapply bc_stack; eauto.
Qed.

Definition cmp_different_blocks (c: comparison) : abool :=
  match c with
  | Ceq => Maybe false
  | Cne => Maybe true
  | _ => Bnone
  end.

Definition cmp_in_bound_different_blocks (c: comparison) : abool :=
  match c with
  | Ceq => Just false
  | Cne => Just true
  | _ => Btop
  end.



Lemma cmp_different_blocks_none:
  forall c, cmatch None (cmp_different_blocks c).
Proof.
  intros; destruct c; constructor.
Qed.

Lemma cmp_different_blocks_sound:
  forall c, cmatch (Val.cmp_different_blocks c) (cmp_different_blocks c).
Proof.
  intros; destruct c; constructor.
Qed.

Definition in_boundb (o : Z) (itv : Z * Z) : bool :=
  (zle (fst itv) o) && (zlt o (snd itv)).

Lemma in_boundb_bound :
  forall o itv, in_boundb o itv = true <-> in_bound o itv.
Proof.
  intros.
  unfold in_boundb.
  rewrite andb_true_iff.
  unfold in_bound.
  destruct (zle (fst itv) o);
    destruct (zlt o (snd itv)); intuition.
Qed.
  
Definition in_bound_glob (id:ident) (ofs : int) : bool := false.

Definition in_bound_stack (ofs : int) : bool := false.

Definition pcmp (c: comparison) (p1 p2: aptr) : abool :=
  match p1, p2 with
  | Pbot, _ | _, Pbot => Bnone
  | Gl id1 ofs1, Gl id2 ofs2 =>
    if in_bound_glob id1 ofs1 && in_bound_glob id2 ofs2
    then
      if peq id1 id2 then Just (Int.cmpu c ofs1 ofs2)
      else cmp_in_bound_different_blocks c
    else Btop
  | Gl id1 ofs1, Glo id2 => Btop
  | Glo id1, Gl id2 ofs2 => Btop
  | Glo id1, Glo id2 => Btop
  | Stk ofs1, Stk ofs2 =>
    if in_bound_stack ofs1 && in_bound_stack ofs2
    then Just (Int.cmpu c ofs1 ofs2)
    else Btop
  | _, _ => Btop
  end.

Lemma no_overlap :
  forall a b1 b2 ofs1 ofs2 bound align
         (NEQ : b1 <> b2)
         (COMPAT : compat Int.max_unsigned bound align a)
         (BOUND1 : in_bound (Int.unsigned ofs1) (bound b1))
         (BOUND2 : in_bound (Int.unsigned ofs2) (bound b2)),
    Int.add (a b1) ofs1 = Int.add (a b2) ofs2 -> False.
Proof.
  intros.
  apply f_equal with (f:= Int.unsigned) in H.
  revert H.
  eapply overlap ; eauto.
Qed.

Lemma is_bool_cmpu_bool : forall c e1 e2,
                    is_bool (Val.cmpu_bool c e1 e2).
Proof.
  intros.
  repeat intro ; simpl.
  destruct (eSexpr a u e1) ; destruct (eSexpr a u e2) ; simpl;
  try (exists Int.zero ; simpl ; intuition constructor).
  destruct (Int.cmpu c i i0) ;
    try (exists Int.zero ; simpl ; intuition constructor);
    try (exists Int.one ; simpl ; intuition constructor).
Qed.


Lemma pcmp_sound:
  forall c e1 p1 e2 p2,
  epmatch e1 p1 -> epmatch e2 p2 ->
  ecmatch (Val.cmpu_bool c e1 e2) (pcmp c p1 p2).
Proof.
  intros.
  unfold pcmp; inv H ; inv H0; try (constructor ; apply is_bool_cmpu_bool; fail).
  Qed.

Definition pdisjoint (p1: aptr) (sz1: Z) (p2: aptr) (sz2: Z) : bool :=
  match p1, p2 with
  | Pbot, _ => true
  | _, Pbot => true
  | Gl id1 ofs1, Gl id2 ofs2 =>
      if peq id1 id2
      then zle (Int.unsigned ofs1 + sz1) (Int.unsigned ofs2)
           || zle (Int.unsigned ofs2 + sz2) (Int.unsigned ofs1)
      else true
  | Gl id1 ofs1, Glo id2 => negb(peq id1 id2)
  | Glo id1, Gl id2 ofs2 => negb(peq id1 id2)
  | Glo id1, Glo id2 => negb(peq id1 id2)
  | Stk ofs1, Stk ofs2 =>
      zle (Int.unsigned ofs1 + sz1) (Int.unsigned ofs2)
      || zle (Int.unsigned ofs2 + sz2) (Int.unsigned ofs1)
  | (Gl _ _ | Glo _ | Glob | Nonstack), (Stk _ | Stack) => true
  | (Stk _ | Stack), (Gl _ _ | Glo _ | Glob | Nonstack) => true
  | _, _ => false
  end.

Lemma pdisjoint_sound:
  forall sz1 b1 ofs1 p1 sz2 b2 ofs2 p2,
  pdisjoint p1 sz1 p2 sz2 = true ->
  pmatch b1 ofs1 p1 -> pmatch b2 ofs2 p2 ->
  b1 <> b2 \/ Int.unsigned ofs1 + sz1 <= Int.unsigned ofs2 \/ Int.unsigned ofs2 + sz2 <= Int.unsigned ofs1.
Proof.
  intros. inv H0; inv H1; simpl in H; try discriminate; try (left; congruence).
- destruct (peq id id0). subst id0. destruct (orb_true_elim _ _ H); InvBooleans; auto.
  left; congruence.
- destruct (peq id id0); try discriminate. left; congruence.
- destruct (peq id id0); try discriminate. left; congruence.
- destruct (peq id id0); try discriminate. left; congruence.
- destruct (orb_true_elim _ _ H); InvBooleans; auto.
Qed.

We need to prevent overflows + there is no way to ensure that stack and gl are disjoint. We would need the the size of the block! Lemma epdisjoint_sound : forall sz1 e1 p1 sz2 e1 p2, pdisjoint p1 sz1 p2 sz2 = true -> epmatch e1 p1 -> epmatch e2 p2 -> forall i j, i eSexpr


Abstracting values


Inductive aval : Type :=
  | I (n: int) (* exactly Vint n *)
  | Uns (p: aptr) (n: Z) (* a n-bit unsigned integer, or Vundef *)
  | Sgn (p: aptr) (n: Z) (* a n-bit signed integer, or Vundef *)
  | L (n: int64) (* exactly Vlong n *)
  | F (f: float) (* exactly Vfloat f *)
  | FS (f: float32) (* exactly Vsingle f *)
  | Ptr (p: aptr) (* a pointer from the set p, or Vundef *)
. (* a pointer from the set p, or a number, or Vundef *)

The "top" of the value domain is defined as any pointer, or any number, or Vundef.

Definition Vtop := Ptr Ptop.

The p parameter (an abstract pointer) to Uns and Sgn helps keeping track of pointers that leak through arithmetic operations such as shifts. See the section "Tracking leakage of pointers" below. In strict analysis mode, p is always Pbot.

Definition eq_aval: forall (v1 v2: aval), {v1=v2} + {v1<>v2}.
Proof.
  intros. generalize zeq Int.eq_dec Int64.eq_dec Float.eq_dec Float32.eq_dec eq_aptr; intros.
  decide equality.
Defined.

Definition is_uns (n: Z) (i: int) : Prop :=
  forall m, 0 <= m < Int.zwordsize -> m >= n -> Int.testbit i m = false.
Definition is_sgn (n: Z) (i: int) : Prop :=
  forall m, 0 <= m < Int.zwordsize -> m >= n - 1 -> Int.testbit i m = Int.testbit i (Int.zwordsize - 1).

Definition is_unsigned (n: Z) (e: expr_sym) : Prop :=
  forall a u
  ,
  exists i, Values.Val.lessdef (eSexpr a u e) (Vint i) /\ is_uns n i.

Definition is_signed (n: Z) (e: expr_sym) : Prop :=
  forall a u
  ,
  exists i, Values.Val.lessdef (eSexpr a u e) (Vint i) /\ is_sgn n i.

Add Parametric Morphism (n:Z) : (is_unsigned n) with signature (same_eval ==> iff) as is_unsigned_same_eval_morph.
Proof.
  assert (
      forall x y : expr_sym,
        same_eval x y -> (is_unsigned n x -> is_unsigned n y) ).
  {
  unfold is_unsigned.
  intros.
  intuition.
  destruct (H0 a u); auto.
  exists x0.
  erewrite <- H; eauto.
  }
  intuition ; eapply H ; eauto.
  rewrite H0 ; reflexivity.
Qed.

Add Parametric Morphism (n:Z) : (is_signed n) with signature (same_eval ==> iff) as is_signed_same_eval_morph.
Proof.
  assert ( forall x y : expr_sym, same_eval x y -> (is_signed n x -> is_signed n y)).
  {
  unfold is_signed.
  intros.
  intuition.
  destruct (H0 a u); auto.
  exists x0.
  erewrite <- H; eauto.
  }
  intuition ; eapply H ; eauto.
  rewrite H0 ; reflexivity.
Qed.




Inductive evmatch : expr_sym -> aval -> Prop :=
  | evmatch_i: forall i e, is_constant (Vint i) e -> evmatch e (I i)
  | evmatch_Uns: forall p e n, 0 <= n ->
                               is_unsigned n e ->
                               epmatch e p ->
                               evmatch e (Uns p n)
  | evmatch_Sgn: forall p e n, 0 < n ->
                               is_signed n e ->
                               epmatch e p ->
                               evmatch e (Sgn p n)
  | evmatch_l: forall e i, is_constant (Vlong i) e -> evmatch e (L i)
  | evmatch_f: forall e f, is_constant (Vfloat f) e -> evmatch e (F f)
  | evmatch_s: forall e f, is_constant (Vsingle f) e -> evmatch e (FS f)
  | evmatch_ptr: forall e p, epmatch e p -> evmatch e (Ptr p)
.

Add Parametric Morphism : evmatch with signature (same_eval ==> @eq aval ==> iff) as evmatch_same_eval_morph.
Proof.
  assert ( forall x y : expr_sym,
               same_eval x y -> forall y0 : aval, evmatch x y0 -> evmatch y y0).
  {
    intros.
    inv H0 ; try constructor; auto with va; try rewrite H in *; auto.
  }
  intuition ; eapply H ; eauto.
  rewrite H0 ; reflexivity.
Qed.




Hint Resolve epmatch_top_def : va.

Lemma evmatch_top: forall v x, evmatch v x -> evmatch v Vtop.
Proof.
  intros.
  constructor.
  inv H ; eauto with va ; unfold is_constant in * ; constructor.
Qed.

Hint Extern 1 (evmatch _ _) => constructor : va.


Lemma is_uns_mon: forall n1 n2 i, is_uns n1 i -> n1 <= n2 -> is_uns n2 i.
Proof.
  intros; red; intros. apply H; omega.
Qed.

Lemma is_sgn_mon: forall n1 n2 i, is_sgn n1 i -> n1 <= n2 -> is_sgn n2 i.
Proof.
  intros; red; intros. apply H; omega.
Qed.

Lemma is_uns_sgn: forall n1 n2 i, is_uns n1 i -> n1 < n2 -> is_sgn n2 i.
Proof.
  intros; red; intros. rewrite ! H by omega. auto.
Qed.

Definition usize := Int.size.

Definition ssize (i: int) := Int.size (if Int.lt i Int.zero then Int.not i else i) + 1.

Lemma is_uns_usize:
  forall i, is_uns (usize i) i.
Proof.
  unfold usize; intros; red; intros.
  apply Int.bits_size_2. omega.
Qed.

Lemma is_sgn_ssize:
  forall i, is_sgn (ssize i) i.
Proof.
  unfold ssize; intros; red; intros.
  destruct (Int.lt i Int.zero) eqn:LT.
- rewrite <- (negb_involutive (Int.testbit i m)).
  rewrite <- (negb_involutive (Int.testbit i (Int.zwordsize - 1))).
  f_equal.
  generalize (Int.size_range (Int.not i)); intros RANGE.
  rewrite <- ! Int.bits_not by omega.
  rewrite ! Int.bits_size_2 by omega.
  auto.
- rewrite ! Int.bits_size_2 by omega.
  auto.
Qed.

Lemma is_uns_zero_ext:
  forall n i, is_uns n i <-> Int.zero_ext n i = i.
Proof.
  intros; split; intros.
  Int.bit_solve. destruct (zlt i0 n); auto. symmetry; apply H; auto. omega.
  rewrite <- H. red; intros. rewrite Int.bits_zero_ext by omega. rewrite zlt_false by omega. auto.
Qed.

Lemma is_sgn_sign_ext:
  forall n i, 0 < n -> (is_sgn n i <-> Int.sign_ext n i = i).
Proof.
  intros; split; intros.
  Int.bit_solve. destruct (zlt i0 n); auto.
  transitivity (Int.testbit i (Int.zwordsize - 1)).
  apply H0; omega. symmetry; apply H0; omega.
  rewrite <- H0. red; intros. rewrite ! Int.bits_sign_ext by omega.
  f_equal. transitivity (n-1). destruct (zlt m n); omega.
  destruct (zlt (Int.zwordsize - 1) n); omega.
Qed.

Lemma is_zero_ext_uns:
  forall i n m,
  is_uns m i \/ n <= m -> is_uns m (Int.zero_ext n i).
Proof.
  intros. red; intros. rewrite Int.bits_zero_ext by omega.
  destruct (zlt m0 n); auto. destruct H. apply H; omega. omegaContradiction.
Qed.

Lemma is_zero_ext_sgn:
  forall i n m,
  n < m ->
  is_sgn m (Int.zero_ext n i).
Proof.
  intros. red; intros. rewrite ! Int.bits_zero_ext by omega.
  transitivity false. apply zlt_false; omega.
  symmetry; apply zlt_false; omega.
Qed.

Lemma is_sign_ext_uns:
  forall i n m,
  0 <= m < n ->
  is_uns m i ->
  is_uns m (Int.sign_ext n i).
Proof.
  intros; red; intros. rewrite Int.bits_sign_ext by omega.
  apply H0. destruct (zlt m0 n); omega. destruct (zlt m0 n); omega.
Qed.
  
Lemma is_sign_ext_sgn:
  forall i n m,
  0 < n -> 0 < m ->
  is_sgn m i \/ n <= m -> is_sgn m (Int.sign_ext n i).
Proof.
  intros. apply is_sgn_sign_ext; auto.
  destruct (zlt m n). destruct H1. apply is_sgn_sign_ext in H1; auto.
  rewrite <- H1. rewrite (Int.sign_ext_widen i) by omega. apply Int.sign_ext_idem; auto.
  omegaContradiction.
  apply Int.sign_ext_widen; omega.
Qed.

Hint Resolve is_uns_mon is_sgn_mon is_uns_sgn is_uns_usize is_sgn_ssize : va.

Lemma is_uns_1:
  forall n, is_uns 1 n -> n = Int.zero \/ n = Int.one.
Proof.
  intros. destruct (Int.testbit n 0) eqn:B0; [right|left]; apply Int.same_bits_eq; intros.
  rewrite Int.bits_one. destruct (zeq i 0). subst i; auto. apply H; omega.
  rewrite Int.bits_zero. destruct (zeq i 0). subst i; auto. apply H; omega.
Qed.

Tracking leakage of pointers through arithmetic operations. In the CompCert semantics, arithmetic operations (e.g. "xor") applied to pointer values are undefined or produce the Vundef result. So, in strict mode, we can abstract the result values of such operations as Ifptr Pbot, namely: Vundef, or any number, but not a pointer. In real code, such arithmetic over pointers occurs, so we need to be more prudent. The policy we take, inspired by that of GCC, is that "undefined" arithmetic operations involving pointer arguments can produce a pointer, but not any pointer: rather, a pointer to the same block, but possibly with a different offset. Hence, if the operation has a pointer to abstract region p as argument, the result value can be a pointer to abstract region poffset p. In other words, the result value is abstracted as Ifptr (poffset p). We encapsulate this reasoning in the following ntop1 and ntop2 functions ("numerical top").


Definition aptr_of_aval (x : aval) : aptr :=
  match x with
    | Ptr p | Uns p _ | Sgn p _ => p
    | I _ | L _ | F _ | FS _ => Pcst
  end.

Definition provenance (x: aval) : aptr :=
  poffset (aptr_of_aval x).

Definition ntop : aval := Ptr Pcst.

Definition ntop1 (x: aval) : aval := Ptr (provenance x).

Definition ntop2 (x y: aval) : aval := Ptr (eplub (provenance x) (provenance y)).


Smart constructors for Uns and Sgn.

Definition uns (p: aptr) (n: Z) : aval :=
  if zle n 1 then Uns p 1
  else if zle n 7 then Uns p 7
  else if zle n 8 then Uns p 8
  else if zle n 15 then Uns p 15
  else if zle n 16 then Uns p 16
  else Ptr p.

Definition sgn (p: aptr) (n: Z) : aval :=
  if zle n 8 then Sgn p 8 else if zle n 16 then Sgn p 16 else Ptr p.

Definition is_bot (v : aval) :=
           aptr_of_aval v = Pbot.


Inductive evge: aval -> aval -> Prop :=
  | evge_refl: forall v, evge v v
  | evge_uns_i: forall n p i, 0 <= n -> is_uns n i -> epge p Pcst ->
                             evge (Uns p n) (I i)
  | evge_p_i : forall p i, epge p Pcst -> evge (Ptr p) (I i)
  | evge_p_l : forall p i, epge p Pcst -> evge (Ptr p) (L i)
  | evge_p_f : forall p i, epge p Pcst -> evge (Ptr p) (F i)
  | evge_p_s : forall p i, epge p Pcst -> evge (Ptr p) (FS i)
  | evge_uns_uns: forall p1 n1 p2 n2, n1 >= n2 -> epge p1 p2 -> evge (Uns p1 n1) (Uns p2 n2)
  | evge_sgn_i: forall n p i, 0 < n -> is_sgn n i -> epge p Pcst -> evge (Sgn p n) (I i)
  | evge_sgn_sgn: forall p1 n1 p2 n2, n1 >= n2 -> epge p1 p2 -> evge (Sgn p1 n1) (Sgn p2 n2)
  | evge_sgn_uns: forall p1 n1 p2 n2, n1 > n2 -> epge p1 p2 -> evge (Sgn p1 n1) (Uns p2 n2)
  | evge_p_uns : forall p1 p2 n1, epge p1 p2 -> evge (Ptr p1) (Uns p2 n1)
  | evge_p_sgn : forall p1 p2 n1, epge p1 p2 -> evge (Ptr p1) (Sgn p2 n1)
  | evge_p_p: forall p q, epge p q -> evge (Ptr p) (Ptr q)
  | evge_top_v: forall v, evge (Ptr Ptop) v
  | evge_bot: forall v v', is_bot v' -> evge v v'
.

Lemma evge_top: forall v, evge Vtop v.
Proof.
  unfold Vtop.
  intro. apply evge_top_v.
Qed.

Hint Resolve evge_top : va.

Lemma epge_top : forall p, epge p Ptop -> p = Ptop.
Proof.
  intros.
  destruct p ; simpl in H ; tauto.
Qed.

Lemma epge_bot : forall p, epge Pbot p -> p = Pbot.
Proof.
  intros.
  destruct p ; simpl in H ; tauto.
Qed.



Lemma evge_trans: forall u v, evge u v -> forall w, evge v w -> evge u w.
Proof.
  induction 1; intros w V; inv V; unfold is_bot, aptr_of_aval in * ; subst;
  eauto using epge_trans with va ; try (constructor; auto; try omega; eauto using epge_trans ; eauto with va ; fail) ; (try (simpl in * ; tauto)).
  -
    apply epge_top in H. subst. constructor.
  - apply epge_bot in H1. subst. apply evge_bot. reflexivity.
  - apply epge_bot in H1. subst.
    apply evge_bot. reflexivity.
  - apply epge_bot in H1. subst.
    apply evge_bot. reflexivity.
  - apply epge_bot in H0. subst.
    apply evge_bot. reflexivity.
  - apply epge_bot in H0. subst.
    apply evge_bot. reflexivity.
  - apply epge_bot in H0. subst.
    apply evge_bot. reflexivity.
  - congruence.
Qed.


Lemma is_uns_unsigned :
  forall n i,
    is_uns n i ->
    is_unsigned n (Eval (Vint i)).
Proof.
  unfold is_unsigned.
  intros. exists i.
  simpl ; intuition.
Qed.

Lemma is_sgn_signed :
  forall n i,
    is_sgn n i ->
    is_signed n (Eval (Vint i)).
Proof.
  unfold is_signed.
  intros. exists i.
  simpl ; intuition.
Qed.

Lemma is_constant_unsigned :
  forall n i v,
    is_uns n i ->
    is_constant (Vint i) v ->
    is_unsigned n v.
Proof.
  intros.
  
  unfold is_constant in H0.
  rewrite <- H0.
  eapply is_uns_unsigned ; eauto.
Qed.

Lemma is_sgn_unsigned :
  forall n i,
    is_sgn n i ->
    is_signed n (Eval (Vint i)).
Proof.
  unfold is_signed.
  intros. exists i.
  simpl ; intuition.
Qed.

Lemma is_constant_signed :
  forall n i v,
    is_sgn n i ->
    is_constant (Vint i) v ->
    is_signed n v.
Proof.
  intros.
  unfold is_constant in H0.
  rewrite <- H0.
  eapply is_sgn_signed ; eauto.
Qed.

Hint Resolve is_constant_unsigned is_constant_signed : va.

Inductive valid_constant : val -> Prop :=
| vc_Vint : forall i, valid_constant (Vint i)
| vc_Vlong : forall l, valid_constant (Vlong l)
| vc_Vfloat : forall f, valid_constant (Vfloat f)
| vc_Vsingle : forall s, valid_constant (Vsingle s)
| vc_Vptr : forall b o, bc b <> BCinvalid -> valid_constant (Vptr b o).

Lemma is_constant_epmatch_top :
  forall c v,
    valid_constant c ->
    is_constant c v ->
    epmatch v Ptop.
Proof.
  intros.
  unfold is_constant in *.
  rewrite <- H0.
  constructor ; auto.
  apply depends_on_blocks_appears.
  intros.
  inv H ; simpl in H1 ; congruence.
Qed.

Ltac is_constant_epmatch_top :=
  match goal with
    | H : is_constant ?C ?V |- epmatch ?V Ptop => apply is_constant_epmatch_top with (c:=C) (2:= H) ; constructor
  end.

Hint Extern 2 (epmatch _ Ptop) => is_constant_epmatch_top : va.
Import NormaliseSpec.

Lemma is_unsigned_unsigned :
  forall n n' (Ti : int -> int) (Te : expr_sym -> expr_sym)
         (Hsame : forall a u e i, Values.Val.lessdef (eSexpr a u e) (Vint i) ->
                                   Values.Val.lessdef (eSexpr a u (Te e)) (Vint (Ti i))),
    (forall i, is_uns n i -> is_uns n' (Ti i)) ->
    (forall e, is_unsigned n e -> is_unsigned n' (Te e)).
Proof.
  intros.
  unfold is_unsigned in *.
  intros.
  destruct (H0 a u); auto.
  intuition.
  exists (Ti x).
  intuition.
Qed.

Lemma is_signed_signed :
  forall n n' (Ti : int -> int) (Te : expr_sym -> expr_sym)
         (Hsame : forall a u e i, Values.Val.lessdef (eSexpr a u e) (Vint i) ->
                                   Values.Val.lessdef (eSexpr a u (Te e)) (Vint (Ti i))),
    (forall i, is_sgn n i -> is_sgn n' (Ti i)) ->
    (forall e, is_signed n e -> is_signed n' (Te e)).
Proof.
  intros.
  unfold is_signed in *.
  intros.
  destruct (H0 a u); auto.
  intuition.
  exists (Ti x).
  intuition.
Qed.

Lemma is_unsigned_signed :
  forall n n' (Ti : int -> int) (Te : expr_sym -> expr_sym)
         (Hsame : forall a u e i, Values.Val.lessdef (eSexpr a u e) (Vint i) ->
                                   Values.Val.lessdef (eSexpr a u (Te e)) (Vint (Ti i))),
    (forall i, is_uns n i -> is_sgn n' (Ti i)) ->
    (forall e, is_unsigned n e -> is_signed n' (Te e)).
Proof.
  intros.
  unfold is_signed,is_unsigned in *.
  intros.
  destruct (H0 a u); auto.
  intuition.
  exists (Ti x).
  intuition.
Qed.

Lemma is_unsigned_mon :
  forall n1 n2 v,
    n1 >= n2 ->
    is_unsigned n2 v ->
    is_unsigned n1 v.
Proof.
  intros n1 n2 v Hge.
  revert v.
  apply is_unsigned_unsigned with (Ti := fun x => x) ; auto.
  intros. eapply is_uns_mon ; eauto with va.
Qed.

Lemma is_signed_mon :
  forall n1 n2 v,
    n1 >= n2 ->
    is_signed n2 v ->
    is_signed n1 v.
Proof.
  intros n1 n2 v Hge.
  revert v.
  apply is_signed_signed with (Ti := fun x => x) ; auto.
  intros. eapply is_sgn_mon ; eauto with va.
Qed.

Lemma is_unsigned_signed_mon :
  forall n1 n2 i,
    n1 < n2 ->
    is_unsigned n1 i ->
    is_signed n2 i.
Proof.
  intros n1 n2 i Hge.
  revert i.
  apply is_unsigned_signed with (Ti := fun x => x) ; auto.
  intros. eapply is_uns_sgn ; eauto with va.
Qed.

Hint Resolve is_unsigned_mon is_signed_mon is_unsigned_signed_mon : va.


Lemma evmatch_ge:
  forall v x y, evge x y -> evmatch v y -> evmatch v x.
Proof.
  induction 1; intros V; inv V;
  unfold is_bot,aptr_of_aval in *; subst;
  eauto using epmatch_ge with va ; try constructor ; eauto using epmatch_ge with va ; try omega;
  try congruence.
  -
    unfold is_constant in H4.
    rewrite <- H4.
    destruct p ; simpl in * ; try tauto ;
    constructor; depends_prf.
  -
    unfold is_constant in H2.
    rewrite <- H2.
    destruct p ; simpl in * ; try tauto ;
    constructor ; depends_prf.
  -
    unfold is_constant in H2.
    rewrite <- H2.
    destruct p ; simpl in * ; try tauto ;
    constructor ; depends_prf.
  -
    unfold is_constant in H2.
    rewrite <- H2.
    destruct p ; simpl in * ; try tauto ;
    constructor ; depends_prf.
  -
    unfold is_constant in H2.
    rewrite <- H2.
    destruct p ; simpl in * ; try tauto ;
    constructor ; depends_prf.
  -
    unfold is_constant in H4.
    rewrite <- H4.
    destruct p ; simpl in * ; try tauto ;
    constructor ; depends_prf.
  -
    eapply is_unsigned_signed_mon ; eauto.
    omega.
  - inv H2.
  - inv H2.
  - inv H0.
Qed.

Least upper bound

Definition evlub (v w: aval) : aval :=
  match v, w with
  | I i1, I i2 =>
      if Int.eq i1 i2 then v else
      if Int.lt i1 Int.zero || Int.lt i2 Int.zero
      then sgn Pcst (Z.max (ssize i1) (ssize i2))
      else uns Pcst (Z.max (usize i1) (usize i2))
  | I i, Uns p n | Uns p n, I i =>
      if Int.lt i Int.zero
      then sgn (eplub p Pcst) (Z.max (ssize i) (n + 1))
      else uns (eplub p Pcst) (Z.max (usize i) n)
  | I i, Sgn p n | Sgn p n, I i =>
      sgn (eplub p Pcst) (Z.max (ssize i) n)
  | I i, Ptr p | Ptr p , I i => Ptr (eplub p Pcst)
  | Uns p1 n1, Uns p2 n2 => Uns (eplub p1 p2) (Z.max n1 n2)
  | Uns p1 n1, Sgn p2 n2 => sgn (eplub p1 p2) (Z.max (n1 + 1) n2)
  | Sgn p1 n1, Uns p2 n2 => sgn (eplub p1 p2) (Z.max n1 (n2 + 1))
  | Sgn p1 n1, Sgn p2 n2 => sgn (eplub p1 p2) (Z.max n1 n2)
  | F f1, F f2 =>
      if Float.eq_dec f1 f2 then v else Vtop
  | FS f1, FS f2 =>
      if Float32.eq_dec f1 f2 then v else Vtop
  | L i1, L i2 =>
      if Int64.eq i1 i2 then v else Vtop
  | Ptr p1, Ptr p2 => Ptr(eplub p1 p2)
  | Ptr p1 , (Uns p2 _ | Sgn p2 _) => Ptr(eplub p1 p2)
  | (Uns p1 _ | Sgn p1 _), (Ptr p2 ) => Ptr(eplub p1 p2)
  | _, (Ptr p ) | (Ptr p ), _ => Vtop
  | _, _ => Vtop
  end.

Lemma evlub_comm:
  forall v w, evlub v w = evlub w v.
Proof.
  intros. unfold evlub; destruct v; destruct w; auto.
- rewrite Int.eq_sym. predSpec Int.eq Int.eq_spec n0 n.
  congruence.
  rewrite orb_comm.
  destruct (Int.lt n0 Int.zero || Int.lt n Int.zero); f_equal; apply Z.max_comm.
- f_equal. apply eplub_comm. apply Z.max_comm.
- f_equal. apply eplub_comm. apply Z.max_comm.
- f_equal; apply eplub_comm.
- rewrite eplub_comm. rewrite Z.max_comm. reflexivity.
- rewrite eplub_comm. rewrite Z.max_comm. reflexivity.
- f_equal. apply eplub_comm.
- rewrite Int64.eq_sym. predSpec Int64.eq Int64.eq_spec n0 n; congruence.
- rewrite dec_eq_sym. destruct (Float.eq_dec f0 f). congruence. auto.
- rewrite dec_eq_sym. destruct (Float32.eq_dec f0 f). congruence. auto.
- f_equal; apply eplub_comm.
- f_equal; apply eplub_comm.
- f_equal; apply eplub_comm.
Qed.



Lemma epge_refl : forall p, epge p p.
Proof.
  destruct p ; simpl ; intuition.
Qed.

Hint Resolve epge_refl : va.


Definition is_dep (p : aptr) : Prop :=
  match p with
    | Gl _ _ | Stk _ | Pbot => False
    | _ => True
  end.

Lemma epge_poffset_Pcst :
  forall v p,
    epmatch v p ->
    epge (poffset p) Pcst.
Proof.
  intros.
  inv H ; simpl ; constructor ; auto.
Qed.

Lemma epge_poffset : forall p, epge (poffset p) p.
Proof.
  destruct p ; simpl ; repeat constructor.
Qed.

Hint Resolve epge_poffset epge_poffset_Pcst : va.

Lemma evge_uns_uns': forall p n, evge (uns p n) (Uns p n).
Proof.
  unfold uns; intros.
  destruct (zle n 1). constructor ; auto with va.
  destruct (zle n 7). constructor ; auto with va.
  destruct (zle n 8). constructor ; auto with va.
  destruct (zle n 15). constructor ; auto with va.
  destruct (zle n 16); auto with va.
  constructor ; auto with va.
  constructor; auto with va.
Qed.

Lemma evge_uns_i': forall p n i, 0 <= n -> is_uns n i -> epge p Pcst -> evge (uns p n) (I i).
Proof.
  intros. apply evge_trans with (Uns p n). apply evge_uns_uns'.
  constructor; auto.
Qed.


Lemma evge_sgn_sgn': forall p n, evge (sgn p n) (Sgn p n).
Proof.
  unfold sgn; intros.
  destruct (zle n 8). constructor; auto with va.
  destruct (zle n 16); constructor ; auto with va.
Qed.

Lemma evge_sgn_i': forall p n i, 0 < n -> is_sgn n i -> epge p Pcst -> evge (sgn p n) (I i).
Proof.
  intros. apply evge_trans with (Sgn p n). apply evge_sgn_sgn'.
  constructor; auto with va.
Qed.


Hint Resolve evge_uns_uns' evge_uns_i' evge_sgn_sgn' evge_sgn_i' : va.

Lemma usize_pos: forall n, 0 <= usize n.
Proof.
  unfold usize; intros. generalize (Int.size_range n); omega.
Qed.

Lemma ssize_pos: forall n, 0 < ssize n.
Proof.
  unfold ssize; intros.
  generalize (Int.size_range (if Int.lt n Int.zero then Int.not n else n)); omega.
Qed.
Definition Vbot := Ptr Pbot.

Hint Constructors evmatch : va.

Lemma eplub_bot :
      forall p q, eplub p q = Pbot -> p = Pbot /\ q = Pbot.
Proof.
 destruct p, q ; simpl ; intuition try congruence;
 try destruct (ident_eq id id0) ;
 try destruct (Int.eq_dec ofs ofs0) ; try congruence.
Qed.

Lemma evge_lub_l:
  forall x y, evge (evlub x y) x.
Proof.
  assert (IFSTRICT: forall (cond: bool) x1 x2 y, evge x1 y -> evge x2 y -> evge (if cond then x1 else x2) y).
  { destruct cond; auto with va. }
  unfold evlub; destruct x, y; simpl ; try (constructor ; eauto using epge_lub_l with va; try reflexivity;fail).
  - predSpec Int.eq Int.eq_spec n n0. apply evge_refl.
  destruct (Int.lt n Int.zero || Int.lt n0 Int.zero).
  apply evge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va.
  reflexivity.
  apply evge_uns_i'. generalize (usize_pos n); xomega. eauto with va.
  reflexivity.
  - destruct (Int.lt n Int.zero).
  apply evge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va.
  apply epge_lub_r.
  apply evge_uns_i'. generalize (usize_pos n); xomega. eauto with va.
  apply epge_lub_r.
  - apply evge_sgn_i'. generalize (ssize_pos n); xomega. eauto with va.
    apply epge_lub_r.
  - constructor.
    apply epge_lub_r.
  -
    destruct (Int.lt n0 Int.zero).
  eapply evge_trans. apply evge_sgn_sgn'.
  apply evge_trans with (Sgn p (n + 1)); constructor ; eauto with va.
  apply epge_lub_l.
  eapply evge_trans. apply evge_uns_uns'. constructor ; eauto with va.
  apply epge_lub_l.
  - eapply evge_trans. apply evge_sgn_sgn'.
    apply evge_trans with (Sgn p (n + 1)); constructor ; eauto using epge_lub_l with va.
  -
    eapply evge_trans. apply evge_sgn_sgn'. constructor ; eauto with va.
    apply epge_lub_l.
  - eapply evge_trans. apply evge_sgn_sgn'. constructor ; eauto using epge_lub_l with va.
  - eapply evge_trans. apply evge_sgn_sgn'. constructor ; eauto using epge_lub_l with va.
  - destruct (Int64.eq n n0); constructor.
    constructor.
  - destruct (Float.eq_dec f f0); repeat constructor.
  - destruct (Float32.eq_dec f f0); repeat constructor.
Qed.


Lemma evmatch_lub_l:
  forall v x y, evmatch v x -> evmatch v (evlub x y).
Proof.
  intros. eapply evmatch_ge; eauto. apply evge_lub_l.
Qed.

Lemma evmatch_lub_r:
  forall v x y, evmatch v y -> evmatch v (evlub x y).
Proof.
  intros. rewrite evlub_comm. apply evmatch_lub_l; auto.
Qed.

In the CompCert semantics, a memory load or store succeeds only if the address is a pointer value. Hence, in strict mode, aptr_of_aval x returns Pbot (no pointer value) if x denotes a number or Vundef. However, in real code, memory addresses are sometimes synthesized from integers, e.g. an absolute address for a hardware device. It is a reasonable assumption that these absolute addresses do not point within the stack block, however. Therefore, in relaxed mode, aptr_of_aval x returns Nonstack (any pointer outside the stack) when x denotes a number.

Definition is_bot_bool (v : aval) :=
 match aptr_of_aval v with
 | Pbot => true
 | _ => false
end.

Definition evge_bool (v w : aval) : bool :=
  match v , w with
    | I i , I j => if Int.eq_dec i j then true else false
    | L l , L l' => if Int64.eq_dec l l' then true else false
    | F f , F f' => if Float.eq_dec f f' then true else false
    | Ptr p , Ptr q => ege_bool p q
    | Uns p n, I i => Int.eq_dec (Int.zero_ext n i) i && zle 0 n && epincl Pcst p
    | Sgn p n, I i => Int.eq_dec (Int.sign_ext n i) i && zlt 0 n && epincl Pcst p
    | Uns q m , Uns p n => zle n m && epincl p q
    | Sgn q m, Uns p n => zlt n m && epincl p q
    | Sgn q m , Sgn p n => zle n m && epincl p q
    | _ , x => is_bot_bool x
  end.

Lemma evge_bool_ge: forall v w, evge_bool w v = true -> evge w v.
Proof.
  unfold evge_bool; destruct v; destruct w; unfold is_bot_bool,aptr_of_aval in *;
  intros; try discriminate; try InvBooleans; try subst; try (constructor ; auto using epincl_ge with va ; fail); try (destruct p ; try congruence; apply evge_bot; reflexivity).
  -
    destruct (Int.eq_dec n0 n) ; try congruence; subst ; constructor.
  - constructor; auto.
    rewrite is_uns_zero_ext; auto. apply epincl_ge; auto.
  - constructor ; auto.
     rewrite is_sgn_sign_ext; auto. apply epincl_ge ; auto.
  - destruct (Int64.eq_dec n0 n) ; try congruence; subst ; constructor.
  - destruct (Float.eq_dec f0 f) ; try congruence; subst ; constructor.
Qed.

Definition vincl (v w: aval) : bool := evge_bool w v.

Lemma evincl_ge: forall v w, vincl v w = true -> evge w v.
Proof.
  unfold vincl. apply evge_bool_ge.
Qed.

Loading constants

Definition genv_match (ge: genv) : Prop :=
  (forall id b, Genv.find_symbol ge id = Some b <-> bc b = BCglob id)
/\(forall b, Plt b (Genv.genv_next ge) -> bc b <> BCinvalid /\ bc b <> BCstack).

Lemma symbol_address_sound:
  forall ge id ofs b e,
    genv_match ge ->
    Genv.symbol_address ge id ofs = (Vptr b ofs) ->
    is_pointer b ofs e ->
    evmatch e (Ptr (Gl id ofs)).
Proof.
  intros. unfold Genv.symbol_address in H0. destruct (Genv.find_symbol ge id) as [b'|] eqn:F.
  -
    inv H0.
    rew_cst H1.
    constructor.
    econstructor.
    apply H;eauto.
    repeat intro. reflexivity.
  - discriminate.
Qed.

Lemma vmatch_ptr_gl:
  forall ge v id ofs,
  genv_match ge ->
  evmatch v (Ptr (Gl id ofs)) ->
  Val.lessdef v (Eval (Genv.symbol_address ge id ofs)).
Proof.
  intros. unfold Genv.symbol_address. inv H0.
  - inv H3. replace (Genv.find_symbol ge id) with (Some b).
    repeat intro.
    simpl. unfold is_pointer in H5.
    rewrite <- H5.
    simpl. constructor.
    symmetry. apply H; auto.
Qed.

Lemma vmatch_ptr_stk:
  forall v ofs sp,
  evmatch v (Ptr(Stk ofs)) ->
  bc sp = BCstack ->
  Val.lessdef v (Eval (Vptr sp ofs)).
Proof.
  intros. inv H.
  - inv H3.
    assert (b = sp) by (eapply bc_stack; eauto).
    subst.
    unfold is_pointer in H4.
    unfold Val.lessdef.
    simpl.
    intros.
    erewrite <- H4; eauto.
Qed.

Lemma is_pointer_eval :
  forall b ofs b' ofs',
    is_pointer b ofs (Eval (Vptr b' ofs')) ->
    b = b' /\ ofs = ofs'.
Proof.
  intros.
  unfold is_pointer in H.
  unfold same_eval in H.
  generalize (H (fun _ => Int.zero) (fun _ _ => Byte.zero)).
  simpl.
  intros. apply inj_vint in H0.
  repeat rewrite Int.add_zero_l in H0. subst.
  split ; auto.
  generalize (H (fun (b':block) => if eq_block b b' then Int.one else Int.zero) (fun _ _ => Byte.zero)).
  simpl.
  intros. apply inj_vint in H0.
  destruct (eq_block b b') ; auto.
  destruct (eq_block b b) ; try congruence.
  generalize (add_one_zero_diff ofs' ofs') ; intuition.
  repeat rewrite Int.add_zero_l in *. intuition.
Qed.


Lemma aptr_of_aval_stack:
  forall b o r av i,
    aptr_of_aval av = Stk i ->
    evmatch r av ->
    is_pointer b o r -> bc b = BCstack /\ i = o.
Proof.
  intros.
  rew_cst H1. clear H1.
  inv H0 ; simpl in H ; try congruence ; subst.
  - inv H3.
    apply is_pointer_eval in H5.
    intuition.
  - inv H3.
    apply is_pointer_eval in H5.
    intuition.
  - inv H1.
    apply is_pointer_eval in H3.
    intuition.
Qed.



Generic operations that just do constant propagation.



Definition unop_int (sem: int -> int) (x: aval) :=
  match x with I n => I (sem n) | _ => ntop1 x end.

Hint Resolve poffset_sound : va.

Lemma aptr_of_aval_sound :
  forall v x,
    evmatch v x ->
   epmatch v (aptr_of_aval x).
Proof.
  intros.
  inv H; simpl ; try constructor ; depends_prf.
Qed.



Hint Resolve aptr_of_aval : va.



Lemma epmatch_cst_Pcst :
  forall v,
    val_no_ptr v = true ->
    epmatch (Eval v) Pcst.
Proof.
  intros.
  destruct v ; simpl in * ; constructor ; red ; intros ; simpl ; depends_prf.
  congruence.
Qed.



Lemma evmatch_unop_ntop1 :
  forall o s v x,
    evmatch v x ->
    evmatch (Eunop o s v) (ntop1 x).
Proof.
    unfold ntop1 in *.
    intros.
    unfold provenance in *.
    constructor.
    inv H ; simpl ; try constructor ; depends_prf.
    -
      inv H2 ; simpl ; try constructor ; depends_prf; congruence.
    -
    inv H2 ; simpl ; try constructor ; depends_prf; congruence.
    -
    inv H0 ; simpl ; try constructor ; depends_prf; congruence.
Qed.

Lemma epmatch_binop_lub :
  forall o s1 s2 v w x y,
    epmatch v x ->
    epmatch w y ->
    epmatch (Ebinop o s1 s2 v w) (eplub (poffset x) (poffset y)).
Proof.
  intros.
  apply poffset_sound in H.
  apply poffset_sound in H0.
  apply epmatch_lub_l with (q := poffset y) in H.
  apply epmatch_lub_l with (q := poffset x) in H0.
  rewrite eplub_comm in H0.
  inv H ; inv H0 ; try constructor; try congruence; depends_prf ; try congruence.
  -
    rewrite <- H1 in H.
    destruct x ; destruct y ; simpl in H1; try discriminate;
    destruct (ident_eq id1 id2) ; congruence.
  -
    destruct x ; destruct y ; simpl in H1; try discriminate;
    destruct (ident_eq id id0) ; congruence.
Qed.

Lemma evmatch_ntop1 :
  forall T v x,
    is_unop_trans T ->
    (evmatch v x) ->
    evmatch (T v) (ntop1 x).
Proof.
  induction 1.
  - unfold ntop1.
    apply evmatch_ge.
    unfold provenance.
    destruct x ; simpl ; repeat constructor ; eauto with va.
  -
    intros.
    unfold ntop1.
    unfold provenance.
    constructor.
    apply epmatch_ge with (q:= Pcst).
    inv H0 ; simpl ; eauto with va.
    constructor.
    destruct v0 ; simpl ; depends_prf.
    simpl in H ; congruence.
  -
    intros.
    unfold ntop1.
    unfold provenance.
    constructor.
    apply epmatch_ge with (q:= Pcst).
    inv H ; simpl ; eauto with va.
    constructor.
    depends_prf.
    repeat intro.
    reflexivity.
  -
    intros.
    specialize (IHis_unop_trans H0).
    revert IHis_unop_trans.
    generalize (f v).
    intros.
    unfold ntop1 in *.
    inv IHis_unop_trans.
    constructor.
    revert H3.
    unfold provenance in *.
    generalize (aptr_of_aval x).
    intros.
    destruct a ; inv H3 ; simpl ; repeat constructor ; depends_prf.
  -
    intros.
    specialize (IHis_unop_trans1 H1).
    specialize (IHis_unop_trans2 H1).
    revert IHis_unop_trans1 IHis_unop_trans2.
    generalize (f1 v) (f2 v).
    unfold ntop1 in *.
    intros.
    constructor.
    inv IHis_unop_trans1.
    inv IHis_unop_trans2.
    unfold provenance in *.
    revert H4 H5.
    generalize (aptr_of_aval x).
    intros.
    destruct a ; inv H4 ; inv H5 ; repeat constructor; depends_prf.
Qed.


Lemma eplub_poffset :
  forall x y,
    eplub (poffset x) (poffset y) =
    poffset (eplub x y).
Proof.
  destruct x ; destruct y ; simpl ; auto; intros;
  repeat case_match ; simpl ; auto.
  congruence.
Qed.
  
Lemma poffset_idem :
  forall x, poffset (poffset x) = poffset x.
Proof.
  destruct x ; try reflexivity.
Qed.

Lemma eplub_idem : forall x, eplub x x = x.
Proof.
  destruct x ; try reflexivity; simpl;
    repeat case_match ; congruence.
Qed.


Lemma epmatch_poffset :
  forall v p T
         (HT : is_unop_trans T)
         (HM : epmatch v p),
    epmatch (T v) (poffset p).
Proof.
  induction 1.
  - apply poffset_sound.
  -
    intros.
    apply epmatch_ge with (q:= Pcst).
    inv HM ; simpl ; eauto with va.
    constructor.
    destruct v0 ; simpl ; depends_prf.
    simpl in H ; congruence.
  -
    intros.
    apply epmatch_ge with (q:= Pcst).
    inv HM ; simpl ; eauto with va.
    constructor.
    depends_prf.
    repeat intro.
    reflexivity.
  -
    intros.
    specialize (IHHT HM).
    revert IHHT.
    generalize (f v).
    intros.
    inv IHHT ; try constructor ; depends_prf.
    destruct p ; simpl in H ; congruence.
    destruct p ; simpl in H ; congruence.
  -
    intros.
    specialize (IHHT1 HM).
    specialize (IHHT2 HM).
    revert IHHT1 IHHT2.
    generalize (f1 v) (f2 v).
    intros.
    rewrite <- eplub_idem.
    rewrite <- (poffset_idem p).
    apply epmatch_binop_lub; auto.
Qed.

Lemma eunop_int_sound:
  forall sem Esem e x
         (HSem : is_unop_trans Esem),
    (forall a u i, eSexpr a u e = Vint i -> eSexpr a u (Esem e) = Vint (sem i)) ->
    evmatch e x ->
    evmatch (Esem e) (unop_int sem x).
Proof.
  intros.
  unfold unop_int.
  destruct x ; auto; try apply evmatch_ntop1 ; auto.
  -
    inv H0. constructor.
    unfold is_constant in *.
    repeat intro.
    simpl.
    symmetry. apply H.
    erewrite <-H3 ; eauto.
Qed.

Definition binop_int (sem: int -> int -> int) (x y: aval) :=
  match x, y with I n, I m => I (sem n m) | _, _ => ntop2 x y end.


  


Lemma evmatch_binop_ntop2 :
  forall v w x y o s1 s2,
    (evmatch v x) ->
    (evmatch w y) ->
    evmatch (Ebinop o s1 s2 v w) (ntop2 x y).
Proof.
  intros.
  unfold ntop2.
  constructor.
  unfold provenance.
  apply epmatch_binop_lub.
  clear H0.
  inv H ; simpl ; auto; constructor ; depends_prf.
  inv H0 ; simpl ; auto; constructor ; depends_prf.
Qed.



Lemma evmatch_ntop2 :
  forall T v w x y
  (HT : is_binop_trans T),
    (evmatch v x) ->
    (evmatch w y) ->
    evmatch (T v w) (ntop2 x y).
Proof.
  induction 1.
  - unfold ntop2.
    intros.
    unfold provenance.
    apply aptr_of_aval_sound in H.
    constructor.
    apply epmatch_ge with (q:= (poffset (aptr_of_aval x))).
    apply epge_lub_l.
    apply poffset_sound ; auto.
  -
    unfold ntop2.
    intros.
    unfold provenance.
    apply aptr_of_aval_sound in H0.
    constructor.
    apply epmatch_ge with (q:= (poffset (aptr_of_aval y))).
    apply epge_lub_r.
    apply poffset_sound ; auto.
  -
    intros.
    constructor.
    unfold provenance.
    apply epmatch_lub_r.
    apply epmatch_ge with (q:= Pcst).
    eapply epge_poffset_Pcst ; eauto with va.
    apply aptr_of_aval_sound ; eauto.
    apply epmatch_cst_Pcst ; auto.
  -
    intros.
    unfold ntop2.
    unfold provenance.
    constructor.
    apply epmatch_lub_r.
    apply epmatch_ge with (q:= Pcst).
    +
    eapply epge_poffset_Pcst ; eauto with va.
    apply aptr_of_aval_sound ; eauto.
    +
    constructor. repeat intro ; reflexivity.
  -
    intros.
    specialize (IHHT H H0).
    apply evmatch_unop_ntop1 with (o:=o) (s:=s) in IHHT.
    eapply evmatch_ge ; eauto.
    unfold ntop2,ntop1.
    constructor.
    unfold provenance.
    unfold aptr_of_aval at 3.
    rewrite eplub_poffset.
    rewrite poffset_idem.
    apply epge_refl.
  -
    intros.
    specialize (IHHT1 H H0).
    specialize (IHHT2 H H0).
    apply evmatch_ge with (y:= ntop2 (ntop2 x y) (ntop2 x y)).
    unfold ntop2.
    unfold provenance.
    constructor.
    rewrite eplub_poffset.
    unfold aptr_of_aval at 3.
    unfold aptr_of_aval at 5.
    rewrite poffset_idem.
    rewrite eplub_poffset.
    rewrite eplub_idem.
    apply epge_refl.
    apply evmatch_binop_ntop2; auto.
Qed.


Lemma ebinop_int_sound:
  forall sem Esem e1 e2 x y
         (HSem : is_binop_trans Esem)
  ,
    (forall a u i j, eSexpr a u e1 = Vint i ->
                   eSexpr a u e2 = Vint j ->
                   eSexpr a u (Esem e1 e2) = Vint (sem i j)) ->
    evmatch e1 x ->
    evmatch e2 y ->
    evmatch (Esem e1 e2) (binop_int sem x y).
Proof.
  intros.
  unfold binop_int.
  destruct x ; auto; try apply evmatch_ntop2; auto.
  -
    destruct y ; try apply evmatch_ntop2 ; auto.
    inv H0 ; inv H1.
    unfold is_constant in *.
    repeat intro.
    simpl.
    constructor.
    unfold is_constant in *.
    repeat intro.
    symmetry. apply H.
    erewrite <- H4 ; eauto.
    erewrite <- H3 ; eauto.
Qed.


Definition unop_float (sem: float -> float) (x: aval) :=
  match x with F n => F (sem n) | _ => ntop1 x end.


Lemma eunop_float_sound:
  forall sem Esem e x
         (HSem : is_unop_trans Esem),
    (forall a u i, eSexpr a u e = Vfloat i -> eSexpr a u (Esem e) = Vfloat (sem i)) ->
    evmatch e x ->
    evmatch (Esem e) (unop_float sem x).
Proof.
  intros.
  unfold unop_float.
  destruct x ; auto; try apply evmatch_ntop1 ; auto.
  -
    inv H0. constructor.
    unfold is_constant in *.
    repeat intro.
    simpl.
    symmetry. apply H.
    erewrite <- H3 ; eauto.
Qed.

Definition binop_float (sem: float -> float -> float) (x y: aval) :=
  match x, y with F n, F m => F (sem n m) | _, _ => ntop2 x y end.


Lemma ebinop_float_sound:
  forall sem Esem e1 e2 x y
         (HSem : is_binop_trans Esem)
  ,
    (forall a u i j, eSexpr a u e1 = Vfloat i ->
                   eSexpr a u e2 = Vfloat j ->
                   eSexpr a u (Esem e1 e2) = Vfloat (sem i j)) ->
    evmatch e1 x ->
    evmatch e2 y ->
    evmatch (Esem e1 e2) (binop_float sem x y).
Proof.
  intros.
  unfold binop_float.
  specialize (evmatch_ntop2 _ _ _ _ _ HSem H0 H1).
  destruct x ; auto.
  destruct y ; auto.
  -
    inv H0 ; inv H1 ; constructor; auto.
    unfold is_constant in *.
    repeat intro.
    simpl.
    symmetry. apply H.
    erewrite <- H4 ; eauto.
    erewrite <- H3 ; eauto.
Qed.


Definition unop_single (sem: float32 -> float32) (x: aval) :=
  match x with FS n => FS (sem n) | _ => ntop1 x end.

Lemma eunop_single_sound:
  forall sem Esem e x
         (HSem : is_unop_trans Esem),
    (forall a u i, eSexpr a u e = Vsingle i -> eSexpr a u (Esem e) = Vsingle (sem i)) ->
    evmatch e x ->
    evmatch (Esem e) (unop_single sem x).
Proof.
  intros.
  unfold unop_single.
  destruct x ; auto; try apply evmatch_ntop1 ; auto.
  -
    inv H0. constructor.
    unfold is_constant in *.
    repeat intro.
    simpl.
    symmetry. apply H.
    erewrite <- H3 ; eauto.
Qed.


Definition binop_single (sem: float32 -> float32 -> float32) (x y: aval) :=
  match x, y with FS n, FS m => FS (sem n m) | _, _ => ntop2 x y end.

Lemma ebinop_single_sound:
  forall sem Esem e1 e2 x y
         (HSem : is_binop_trans Esem)
  ,
    (forall a u i j, eSexpr a u e1 = Vsingle i ->
                   eSexpr a u e2 = Vsingle j ->
                   eSexpr a u (Esem e1 e2) = Vsingle (sem i j)) ->
    evmatch e1 x ->
    evmatch e2 y ->
    evmatch (Esem e1 e2) (binop_single sem x y).
Proof.
  intros.
  unfold binop_single.
  specialize (evmatch_ntop2 _ _ _ _ _ HSem H0 H1).
  destruct x ; auto. destruct y ; auto.
  -
    inv H0 ; inv H1 ; constructor; auto.
    unfold is_constant in *.
    repeat intro.
    simpl.
    symmetry. apply H.
    erewrite <- H4 ; eauto.
    erewrite <- H3 ; eauto.
Qed.





  
Logical operations

Definition shl (v w: aval) :=
  match w with
  | I amount =>
      if Int.ltu amount Int.iwordsize then
        match v with
        | I i => I (Int.shl i amount)
        | Uns p n => uns (poffset p) (n + Int.unsigned amount)
        | Sgn p n => sgn (poffset p) (n + Int.unsigned amount)
        | _ => ntop1 v
        end
      else ntop1 v
  | _ => ntop2 v w
  end.

Lemma evmatch_uns':
  forall p e n, is_unsigned (Zmax 0 n) e -> epmatch e p -> evmatch e (uns p n).
Proof.
  intros.
  assert (A: forall n', n' >= 0 -> n' >= n -> is_unsigned n' e).
  {
    intros.
    assert (n' >= Z.max 0 n) by auto with va.
    eapply is_unsigned_mon; eauto.
  }
  unfold uns.
  destruct (zle n 1). auto with va.
  destruct (zle n 7). auto with va.
  destruct (zle n 8). auto with va.
  destruct (zle n 15). auto with va.
  destruct (zle n 16). auto with va.
  constructor ; auto.
Qed.

Lemma evmatch_uns:
  forall p e n, is_unsigned n e -> epmatch e p -> evmatch e (uns p n).
Proof.
  intros. apply evmatch_uns';auto.
  eapply is_unsigned_mon ; eauto with va.
  auto with va.
Qed.

Lemma evmatch_sgn':
  forall p e n, is_signed (Zmax 1 n) e -> epmatch e p -> evmatch e (sgn p n).
Proof.
  intros.
  assert (A: forall n', n' >= 1 -> n' >= n -> is_signed n' e).
  {
    intros.
    eapply is_signed_mon with (n2 := Z.max 1 n); eauto.
    eauto with va.
  }
  unfold sgn.
  destruct (zle n 8). constructor; eauto with va.
  destruct (zle n 16); constructor ; eauto with va.
Qed.

Lemma vmatch_sgn:
  forall p e n, is_signed n e -> epmatch e p -> evmatch e (sgn p n).
Proof.
  intros. apply evmatch_sgn'; auto with va.
  eapply is_signed_mon ; eauto.
  zify; omega.
Qed.


Lemma inv_lessdef : forall x y, Values.Val.lessdef x y ->
                                x = Vundef \/ x = y.
Proof.
  intros.
  inv H ; intuition.
Qed.
  

Ltac lessdef :=
  match goal with
    | H : Values.Val.lessdef ?X ?V |-
      Values.Val.lessdef ?Y ?W =>
      match Y with
        | context[X] => apply inv_lessdef in H ;
            let LD := fresh "LD" in
            destruct H as [LD | LD] ; rewrite LD in * ; simpl ; try constructor
      end
  end.


Lemma shl_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.shl v w) (shl x y).
Proof.
  intros.
  assert (DEFAULT: evmatch (Val.shl v w) (ntop2 x y)).
  {
    apply evmatch_ntop2 ; auto.
    repeat constructor ; auto.
  }
  destruct y; auto. simpl. inv H0. unfold Val.shl.
  destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto.
  -
  exploit Int.ltu_inv; eauto. intros RANGE.
  inv H; auto with va.
  +
  constructor.
  unfold is_constant in H3.
  rewrite <- H3.
  unfold is_constant in H0.
  rewrite <- H0.
  repeat intro. simpl.
  rewrite LTU. reflexivity.
  +
    apply evmatch_uns'.
    *
      unfold is_constant in H3. rewrite <- H3.
      revert H1.
      apply is_unsigned_unsigned with
      (Ti := fun v => Int.shl v n)
      (Te := (fun v => (Ebinop OpShl Tint Tint v (Eval (Vint n))))).
      simpl. intros.
      lessdef.
      rewrite LTU. constructor.
      red ; intros. rewrite Int.bits_shl by omega.
      destruct (zlt m (Int.unsigned n)). auto. apply H; xomega.
    *
      apply epmatch_ge with (q := eplub (poffset p) (poffset Pcst)).
      inv H2 ; try (simpl ; auto ; fail).
      apply epmatch_binop_lub; auto.
      constructor.
      depends_prf.
  +
    apply evmatch_sgn'.
    *
      unfold is_constant in H3. rewrite <- H3.
      revert H1.
      apply is_signed_signed with
      (Ti := fun v => Int.shl v n)
      (Te := (fun v => (Ebinop OpShl Tint Tint v (Eval (Vint n))))).
      simpl. intros.
      lessdef.
      rewrite LTU. constructor.
      red ; intros. zify.
      rewrite ! Int.bits_shl by omega.
      rewrite ! zlt_false by omega.
      rewrite H by omega. symmetry. rewrite H by omega. auto.
    *
      apply epmatch_ge with (q := eplub (poffset p) (poffset Pcst)).
      inv H2 ; try (simpl ; auto ; fail).
      apply epmatch_binop_lub; auto.
      constructor.
      depends_prf.
  +
    unfold is_constant in H3.
    rewrite <- H3.
    apply evmatch_ntop1 with (T := fun v => (Ebinop OpShl Tint Tint v (Eval (Vint n)))).
    repeat constructor. constructor ; auto.
  -
    unfold is_constant in H3.
    rewrite <- H3.
    apply evmatch_ntop1 with (T := fun v => (Ebinop OpShl Tint Tint v (Eval (Vint n)))).
    repeat constructor. auto.
Qed.


Definition shru (v w: aval) :=
  match w with
  | I amount =>
      if Int.ltu amount Int.iwordsize then
        match v with
        | I i => I (Int.shru i amount)
        | Uns p n => uns (poffset p) (n - Int.unsigned amount)
        | _ => uns (provenance v) (Int.zwordsize - Int.unsigned amount)
        end
      else ntop1 v
  | _ => ntop2 v w
  end.

Lemma inj_unsigned :
  forall x y,
    x <> y -> Int.unsigned x <> Int.unsigned y.
Proof.
  intros.
  destruct x ; destruct y ; simpl in *.
  intro.
  subst.
  assert (intrange = intrange0) by apply Axioms.proof_irr.
  congruence.
Qed.
  

Lemma is_constant_int_ptr :
  forall i b o e ,
    is_constant (Vint i) e ->
    is_constant (Vptr b o) e ->
False.
Proof.
  intros.
  unfold is_constant in *.
  unfold same_eval in *.
  generalize (H (fun _ => Int.zero) (fun _ _ => Byte.zero)).
  generalize (H (fun _ => Int.one) (fun _ _ => Byte.zero)).
  generalize (H0 (fun _ => Int.zero) (fun _ _ => Byte.zero)).
  generalize (H0 (fun _ => Int.one) (fun _ _ => Byte.zero)).
  simpl.
  generalize (eSexpr (fun _ => Int.zero) (fun (_ : block) (_ : int) => Byte.zero) e).
  generalize (eSexpr (fun _ => Int.one) (fun (_ : block) (_ : int) => Byte.zero) e).
  intros ; subst.
  rewrite H4 in H3.
  clear H4.
  apply inj_vint in H3.
  rewrite Int.add_zero_l in H3.
  generalize (add_one_zero_diff o o).
  intuition.
  rewrite Int.add_zero_l in H2. intuition.
Qed.

Lemma is_constant_epmatch_epge :
  forall i e x,
    is_constant (Vint i) e -> epmatch e x ->
   epge x Pcst.
Proof.
  intros.
  inv H0 ; simpl ; auto.
  eapply is_constant_int_ptr ; eauto.
  eapply is_constant_int_ptr ; eauto.
Qed.



Lemma is_constant_epmatch_Pcst :
  forall i e,
    is_constant (Vint i) e ->
   epmatch e Pcst.
Proof.
  intros.
  rew_cst H.
  constructor.
  depends_prf.
Qed.


Lemma eSexpr_rew :
  forall a ud e ,
    eSexpr a ud e =
    match e with
      | Eval v => eSval a v
      | Eundef p i => Vint (Int.repr (Byte.unsigned (ud p i)))
      | Eunop u t e => fun_of_unop u t (eSexpr a ud e)
      | Ebinop b t1 t2 e1 e2 => fun_of_binop b t1 t2 (eSexpr a ud e1) (eSexpr a ud e2)
    end.
Proof.
  destruct e ; auto.
Qed.

Lemma evmatch_epge :
  forall v x,
    evmatch v x ->
    epge (poffset (aptr_of_aval x))
         (eplub (poffset (aptr_of_aval x)) (poffset Pcst)).
Proof.
  intros.
  inv H ; try (simpl ; auto ; fail).
  simpl. inv H2 ; try (simpl ; auto ; fail).
  simpl. inv H2 ; try (simpl ; auto ; fail).
  simpl. inv H0 ; try (simpl ; auto ; fail).
Qed.

Lemma shru_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.shru v w) (shru x y).
Proof.
  intros.
  assert (DEFAULT: evmatch (Val.shru v w) (ntop2 x y)).
  {
    apply evmatch_ntop2 ; auto.
    repeat constructor.
  }
  destruct y; auto. inv H0. unfold shru, Val.shru in *.
  unfold is_constant in H3. rewrite <- H3 in *. clear H3.
  destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto.
  exploit Int.ltu_inv; eauto. intros RANGE. change (Int.unsigned Int.iwordsize) with Int.zwordsize in RANGE.
  assert (DEFAULT2: evmatch (Val.shru v (Eval (Vint n))) (uns (provenance x) (Int.zwordsize - Int.unsigned n))).
  {
    intros. apply evmatch_uns. red; intros.
    -
      unfold Val.shru.
      rewrite eSexpr_rew.
      case_eq (eSexpr a u v); intros ; try (exists Int.zero ; split ; [constructor|]);
      try (red ; intros ; rewrite Int.bits_zero ; reflexivity).
      exists (Int.shru i n).
      repeat rewrite eSexpr_rew.
      split. unfold fun_of_binop.
      unfold shr_t. simpl.
      rewrite LTU.
      constructor.
      red ; intros.
      rewrite Int.bits_shru by omega. apply zlt_false. omega.
    -
      unfold provenance.
      unfold Val.shru.
      apply epmatch_ge with (q := eplub (poffset (aptr_of_aval x)) (poffset Pcst)).
      eapply evmatch_epge; eauto.
      apply epmatch_binop_lub; auto.
      eapply aptr_of_aval_sound ; eauto.
      constructor.
      depends_prf.
  }
  inv H; eauto with va.
  -
    constructor.
    unfold is_constant in *.
    rewrite <- H0.
    repeat intro ; simpl.
    rewrite LTU. reflexivity.
  -
    apply evmatch_uns'.
    revert H1.
    apply is_unsigned_unsigned with
    (Te := fun v => (Ebinop (OpShr SEUnsigned) Tint Tint v (Eval (Vint n))))
      (Ti := fun x => Int.shru x n).
    + simpl. intros.
      lessdef. rewrite LTU. constructor.
    +
    red; intros. zify.
    rewrite Int.bits_shru by omega.
    destruct (zlt (m + Int.unsigned n) Int.zwordsize); auto.
    apply H; omega.
    +
      apply epmatch_ge with (q := eplub (poffset p) (poffset Pcst)).
      inv H2 ; try (simpl ; auto ; fail).
      apply epmatch_binop_lub; auto.
      constructor.
      depends_prf.
  -
    apply evmatch_ntop1 with (T := (fun v => (Ebinop (OpShr SEUnsigned) Tint Tint v (Eval (Vint n))))).
    repeat constructor. auto.
Qed.

Definition shr (v w: aval) :=
  match w with
  | I amount =>
      if Int.ltu amount Int.iwordsize then
        match v with
        | I i => I (Int.shr i amount)
        | Uns p n => sgn (poffset p) (n + 1 - Int.unsigned amount)
        | Sgn p n => sgn (poffset p) (n - Int.unsigned amount)
        | _ => sgn (provenance v) (Int.zwordsize - Int.unsigned amount)
        end
      else ntop1 v
  | _ => ntop2 v w
  end.

Lemma shr_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.shr v w) (shr x y).
Proof.
  intros.
  assert (DEFAULT: evmatch (Val.shr v w) (ntop2 x y)).
  {
    apply evmatch_ntop2 ; auto.
    repeat constructor.
  }
  destruct y; auto. inv H0. unfold shr, Val.shr.
  destruct (Int.ltu n Int.iwordsize) eqn:LTU; auto.
  exploit Int.ltu_inv; eauto. intros RANGE. change (Int.unsigned Int.iwordsize) with Int.zwordsize in RANGE.
  assert (DEFAULT2: evmatch (Val.shr v (Eval (Vint n))) (sgn (provenance x) (Int.zwordsize - Int.unsigned n))).
  {
    intros. apply vmatch_sgn. red ; intros.
    -
      unfold Val.shr.
      rewrite eSexpr_rew.
      case_eq (eSexpr a u v); intros ; try (exists Int.zero ; split ; [constructor|]);
      try (red ; intros ; rewrite Int.bits_zero ; reflexivity).
      exists (Int.shr i n).
      repeat rewrite eSexpr_rew.
      split. unfold fun_of_binop.
      unfold shr_t. simpl.
      rewrite LTU.
      constructor.
      red; intros.
      rewrite ! Int.bits_shr by omega. f_equal.
      destruct (zlt (m + Int.unsigned n) Int.zwordsize);
        destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize);
        omega.
    -
      unfold provenance.
      unfold Val.shr.
      apply epmatch_ge with (q := eplub (poffset (aptr_of_aval x)) (poffset Pcst)).
      eapply evmatch_epge; eauto.
      apply epmatch_binop_lub; auto.
      eapply aptr_of_aval_sound ; eauto.
      constructor.
      depends_prf.
  }
  assert (SGN: forall p, is_signed p v -> 0 < p ->
                         evmatch (Val.shr v (Eval (Vint n))) (sgn (provenance x) (p - Int.unsigned n))).
  {
    intros. apply evmatch_sgn'.
    -
      revert H0.
      apply is_signed_signed with (Te := fun e => (Val.shr e (Eval (Vint n)))) (Ti := fun i =>
                                                                                        Int.shr i n).
      +
      intros.
      simpl. lessdef.
      rewrite LTU. constructor.
      +
        red; intros. zify.
        rewrite ! Int.bits_shr by omega.
        transitivity (Int.testbit i (Int.zwordsize - 1)).
        destruct (zlt (m + Int.unsigned n) Int.zwordsize).
        apply H0; omega.
        auto.
        symmetry.
        destruct (zlt (Int.zwordsize - 1 + Int.unsigned n) Int.zwordsize).
        apply H0; omega.
        auto.
    -
      unfold provenance.
      unfold Val.shr.
      apply epmatch_ge with (q := eplub (poffset (aptr_of_aval x)) (poffset Pcst)).
      eapply evmatch_epge; eauto.
      apply epmatch_binop_lub; auto.
      eapply aptr_of_aval_sound ; eauto.
      constructor.
      depends_prf.
  }
  unfold is_constant in H3.
  rewrite <- H3.
  unfold Val.shr in SGN.
  unfold provenance in SGN.
  inv H; simpl in SGN ; eauto with va.
  -
    constructor.
    unfold is_constant in *.
    rewrite <- H0.
    repeat intro ; simpl.
    rewrite LTU. reflexivity.
  -
    apply SGN.
    revert H1.
    apply is_unsigned_signed with (Te := (fun v => v)) (Ti := fun v => v); auto.
    intros.
    eapply is_uns_sgn ; eauto.
    omega.
    omega.
  -
    unfold is_constant in H3.
    rewrite <- H3.
    eapply evmatch_ntop1 with (T :=fun v => (Ebinop (OpShr SESigned) Tint Tint v (Eval (Vint n)))).
    repeat constructor ; auto.
    auto.
Qed.

Definition and (v w: aval) := ntop2 v w.



Lemma and_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.and v w) (and x y).
Proof.
  intros.
  eapply evmatch_ntop2 ; eauto.
  repeat constructor.
Qed.


Definition or (v w:aval):= ntop2 v w.

Lemma or_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.or v w) (or x y).
Proof.
  intros.
  eapply evmatch_ntop2 ; eauto.
  repeat constructor.
Qed.


Definition same_pointer (p q : aptr) : bool :=
match p , q with
     | Stk i , Stk j => Int.eq i j
     | Gl id1 o1 , Gl id2 o2 => ident_eq id1 id2 && Int.eq o1 o2
     | _ , _ => false
   end.

Definition xor (v w: aval) :=
  match v, w with
  | I i1, I i2 => I (Int.xor i1 i2)
  | I i, Uns p n | Uns p n, I i => uns (poffset p) (Z.max n (usize i))
  | Uns p1 n1, Uns p2 n2 => uns (eplub (poffset p1) (poffset p2)) (Z.max n1 n2)
  | Sgn p1 n1, Sgn p2 n2 => sgn (eplub (poffset p1) (poffset p2)) (Z.max n1 n2)
  | Ptr p , Ptr q => if same_pointer p q then I (Int.zero)
                      else ntop2 v w
  | _, _ => ntop2 v w
  end.

Lemma is_constant_usize : forall i v,
     is_constant (Vint i) v ->
     is_unsigned (usize i) v.
Proof.
  intros.
  rew_cst H.
  repeat intro ; simpl.
  exists i ; intuition.
Qed.

Lemma evge_uns : forall p q i,
    epge p q ->
    evge (uns p i) (uns q i).
Proof.
  unfold uns.
  intros.
  repeat case_match; constructor; try xomega; auto.
Qed.



Lemma xor_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.xor v w) (xor x y).
Proof.
  intros.
  assert (UNS :
            forall n m p p',
              is_unsigned n v ->
              is_unsigned m w ->
              epmatch w p ->
              epmatch v p' ->
              evmatch (Val.xor v w) (uns (eplub (poffset p') (poffset p)) (Z.max n m))).
  {
    intros.
    unfold Val.xor.
    apply evmatch_uns.
    repeat intro.
    destruct (H1 a u) as [v1 [LD1 UNS1]].
    destruct (H2 a u) as [v2 [LD2 UNS2]].
    simpl.
    inv LD1 ; inv LD2.
    - rewrite H7 ; rewrite H8.
    exists (Int.xor v1 v2).
    intuition.
    intros; red; intros. rewrite Int.bits_xor by auto.
    rewrite UNS1 by xomega.
    rewrite UNS2 by xomega. auto.
    - exists Int.zero.
      rewrite H7.
      intuition.
      repeat intro. rewrite Int.bits_zero.
      reflexivity.
    - exists Int.zero.
      intuition.
      repeat intro. rewrite Int.bits_zero.
      reflexivity.
    - exists Int.zero.
      intuition.
      repeat intro. rewrite Int.bits_zero.
      reflexivity.
    - apply epmatch_binop_lub; auto.
  }
  assert (SGN :
            forall n m p p',
              is_signed n v ->
              is_signed m w ->
              epmatch w p ->
              epmatch v p' ->
              evmatch (Val.xor v w) (sgn (eplub (poffset p') (poffset p)) (Z.max n m))).
  {
    intros.
    unfold Val.xor.
    apply evmatch_sgn'.
    repeat intro.
    destruct (H1 a u) as [v1 [LD1 UNS1]].
    destruct (H2 a u) as [v2 [LD2 UNS2]].
    simpl.
    inv LD1 ; inv LD2.
    - rewrite H7 ; rewrite H8.
    exists (Int.xor v1 v2).
    intuition.
    intros; red; intros.
    rewrite ! Int.bits_xor by xomega.
    rewrite UNS1 by xomega.
    rewrite UNS2 by xomega. auto.
    - exists Int.zero.
      rewrite H7.
      intuition.
      repeat intro. rewrite Int.bits_zero.
      reflexivity.
    - exists Int.zero.
      intuition.
      repeat intro. rewrite Int.bits_zero.
      reflexivity.
    - exists Int.zero.
      intuition.
      repeat intro. rewrite Int.bits_zero.
      reflexivity.
    - apply epmatch_binop_lub; auto.
  }
  assert (TOP : evmatch (Val.xor v w) (ntop2 x y)).
  {
    eapply evmatch_ntop2 ; eauto.
    repeat constructor.
  }
  assert (SAMEPTR: forall b o,
             is_pointer b o v ->
             is_pointer b o w ->
             evmatch (Val.xor v w) (I Int.zero)).
  {
    constructor.
    unfold Val.xor; simpl.
    rew_cst H1. rew_cst H2.
    repeat intro ; simpl.
    rewrite Int.xor_idem. reflexivity.
  }
  inv H ; inv H0 ; auto.
  - simpl ; constructor.
    unfold Val.xor.
    repeat intro ; simpl.
    rew_cst H1. rew_cst H.
  - simpl.
    clear TOP.
    assert (UNSI := H1).
    apply is_constant_usize in UNSI.
    apply is_constant_epmatch_Pcst in H1.
    exploit UNS ; eauto.
    eapply evmatch_ge.
    rewrite Z.max_comm.
    apply evge_uns.
    inv H3 ; simpl; auto.
  - simpl.
    clear TOP.
    assert (UNSI := H).
    apply is_constant_usize in UNSI.
    apply is_constant_epmatch_Pcst in H.
    exploit UNS ; eauto.
    eapply evmatch_ge.
    apply evge_uns.
    inv H3 ; simpl; auto.
  - simpl.
    eauto.
  - simpl.
    eauto.
  -
    simpl.
    case_eq (same_pointer p p0) ; auto.
    intros.
    unfold same_pointer in H0.
    destruct p ; destruct p0 ; try congruence.
    +
      InvBooleans.
      generalize (Int.eq_spec ofs ofs0).
      rewrite H3. intuition subst.
      inv H ; inv H1.
      assert (b = b0) by (eapply bc_glob ; eauto).
      subst ; eauto.
    +
      generalize (Int.eq_spec ofs ofs0).
      rewrite H0. intuition subst.
      inv H ; inv H1.
      assert (b = b0) by (eapply bc_stack ; eauto).
      subst ; eauto.
Qed.

Definition notint (v:aval) := ntop1 v.

Lemma notint_sound:
  forall v x, evmatch v x -> evmatch (Val.notint v) (notint x).
Proof.
  intros. eapply evmatch_ntop1 ; repeat constructor;auto.
Qed.


Definition ror (x y: aval) := ntop2 x y.

Lemma ror_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.ror v w) (ror x y).
Proof.
  intros.
  eapply evmatch_ntop2 ; eauto.
  repeat constructor.
Qed.



Definition rolm (x: aval) (amount mask: int) := ntop1 x.

Lemma rolm_sound:
  forall v x amount mask,
  evmatch v x -> evmatch (Val.rolm v amount mask) (rolm x amount mask).
Proof.
 repeat intro.
 eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.



Integer arithmetic operations

Definition neg := unop_int Int.neg.

Lemma neg_sound:
  forall v x, evmatch v x -> evmatch (Val.neg v) (neg x).
Proof.
  intros.
  apply eunop_int_sound ; auto.
  -
  repeat constructor.
  -
    unfold Val.neg.
    intros.
    simpl.
    rewrite H0.
    reflexivity.
Qed.
    
Definition add (x y: aval) :=
  match x, y with
  | I i, I j => I (Int.add i j)
  | Ptr p, I i | I i, Ptr p => Ptr (padd p i)
  | _, _ => ntop2 x y
  end.

Lemma add_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.add v w) (add x y).
Proof.
  intros.
  assert (evmatch (Val.add v w) (ntop2 x y)).
  {
    apply evmatch_ntop2 ; auto.
    repeat constructor.
  }
  unfold Val.add, add; inv H; inv H0; auto.
  -
    constructor.
    rew_cst H2.
    rew_cst H.
    repeat intro.
    reflexivity.
  -
    constructor.
    unfold is_constant in H2.
    rewrite <- H2.
    rewrite epmatch_same_eval with (y:= (Ebinop OpAdd Tint Tint w (Eval (Vint i)))) ; eauto.
    apply epadd_sound; auto.
    red ; intros ; simpl.
    destruct (eSexpr cm em w) ; try reflexivity.
    rewrite Int.add_commut. reflexivity.
  -
    constructor.
    unfold is_constant in H.
    rewrite <- H.
    apply epadd_sound ; auto.
Qed.

Definition sub (v w: aval) :=
  match v, w with
  | I i1, I i2 => I (Int.sub i1 i2)
  | Ptr p, I i => Ptr (psub p i)
  | Ptr p1, Ptr p2 => match psub2 p1 p2 with Some n => I n | _ => ntop2 v w end
  | _, _ => ntop2 v w
  end.

Lemma sub_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.sub v w) (sub x y).
Proof.
  intros.
  assert (evmatch (Val.sub v w) (ntop2 x y)).
  {
    apply evmatch_ntop2 ; auto.
    repeat constructor.
  }
  unfold Val.sub, sub; inv H; inv H0; auto.
  -
    constructor.
    rew_cst H2.
    rew_cst H.
    repeat intro ; reflexivity.
  -
    constructor.
    unfold is_constant in H.
    rewrite <- H.
    apply epsub_sound ; auto.
  -
    case_eq (psub2 p p0).
    +
    intros.
    assert (is_constant (Vint i) (Val.sub v w)).
    eapply epsub2_sound ; eauto.
    unfold is_constant in H3.
    rewrite <- H3.
    constructor.
    seval_prf.
    reflexivity.
    +
      auto.
Qed.

Definition mul := binop_int Int.mul.

Lemma mul_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.mul v w) (mul x y).
Proof.
  intros.
  apply ebinop_int_sound ; auto.
  repeat constructor.
  intros.
  unfold Val.mul ; simpl.
  rewrite H1 ; rewrite H2.
  reflexivity.
Qed.
  

Definition mulhs := binop_int Int.mulhs.

Lemma mulhs_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.mulhs v w) (mulhs x y).
Proof.
  intros.
  apply ebinop_int_sound ; auto.
  repeat constructor.
  intros.
  unfold Val.mulhs ; simpl.
  rewrite H1 ; rewrite H2.
  reflexivity.
Qed.

Definition mulhu := binop_int Int.mulhu.

Lemma mulhu_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.mulhu v w) (mulhu x y).
Proof.
  intros.
  apply ebinop_int_sound ; auto.
  repeat constructor.
  intros.
  unfold Val.mulhu ; simpl.
  rewrite H1 ; rewrite H2.
  reflexivity.
Qed.

Definition divs (v w: aval) :=
  match w, v with
  | I i2, I i1 =>
      if Int.eq i2 Int.zero
      || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
      then Ptr Pcst
      else I (Int.divs i1 i2)
  | _, _ => ntop2 v w
  end.

Lemma divs_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.divs v w) (divs x y).
Proof.
  intros.
  assert (DEFAULT : evmatch (Val.divs v w) (ntop2 x y)).
  {
    apply evmatch_ntop2; repeat constructor ; auto.
  }
  unfold divs. destruct x ; destruct y ; auto.
  inv H ; inv H0.
  unfold is_constant in *.
  unfold Val.divs.
  rewrite <- H3 ; rewrite <- H2.
  destruct (Int.eq n0 Int.zero
                   || Int.eq n (Int.repr Int.min_signed) && Int.eq n0 Int.mone) eqn:E.
  +
  constructor.
  constructor.
  depends_prf.
  +
    constructor.
    unfold is_constant.
    red ; intros.
    simpl.
    rewrite E. reflexivity.
Qed.

Definition divu (v w: aval) :=
  match w, v with
  | I i2, I i1 =>
      if Int.eq i2 Int.zero
       then Ptr Pcst
      else I (Int.divu i1 i2)
  | _, _ => ntop2 v w
  end.

Lemma divu_sound:
  forall v w x y, evmatch v x -> evmatch w y ->
                    evmatch (Val.divu v w) (divu x y).
Proof.
  intros.
  assert (DEFAULT : evmatch (Val.divu v w) (ntop2 x y)).
  {
    apply evmatch_ntop2; repeat constructor ; auto.
  }
  unfold divu. destruct x ; destruct y ; auto.
  inv H ; inv H0.
  unfold is_constant in *.
  unfold Val.divu.
  rewrite <- H3 ; rewrite <- H2.
  destruct (Int.eq n0 Int.zero) eqn:E.
  +
  constructor.
  constructor.
  depends_prf.
  +
    constructor.
    unfold is_constant.
    red ; intros.
    simpl.
    rewrite E. reflexivity.
Qed.

Definition mods (v w: aval) :=
  match w, v with
  | I i2, I i1 =>
      if Int.eq i2 Int.zero
      || Int.eq i1 (Int.repr Int.min_signed) && Int.eq i2 Int.mone
      then Ptr Pcst
      else I (Int.mods i1 i2)
  | _, _ => ntop2 v w
  end.

Lemma mods_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.mods v w) (mods x y).
Proof.
  intros.
  assert (DEFAULT : evmatch (Val.mods v w) (ntop2 x y)).
  {
    apply evmatch_ntop2; repeat constructor ; auto.
  }
  unfold mods. destruct x ; destruct y ; auto.
  inv H ; inv H0.
  unfold is_constant in *.
  unfold Val.mods.
  rewrite <- H3 ; rewrite <- H2.
  case_match; intro E.
  +
  constructor.
  constructor.
  depends_prf.
  +
    constructor.
    unfold is_constant.
    red ; intros.
    simpl.
    rewrite E. reflexivity.
Qed.

Definition modu (v w: aval) :=
  match w, v with
  | I i2, I i1 =>
      if Int.eq i2 Int.zero
      then Ptr Pcst
      else I (Int.modu i1 i2)
  | I i2, _ => uns (provenance v) (usize i2)
  | _, _ => ntop2 v w
  end.

Lemma modu_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.modu v w) (modu x y).
Proof.
  assert (UNS: forall i j, j <> Int.zero -> is_uns (usize j) (Int.modu i j)).
  {
    intros. apply is_uns_mon with (usize (Int.modu i j)); auto with va.
    unfold usize, Int.size. apply Int.Zsize_monotone.
    generalize (Int.unsigned_range_2 j); intros RANGE.
    assert (Int.unsigned j <> 0).
    { red; intros; elim H. rewrite <- (Int.repr_unsigned j). rewrite H0. auto. }
    exploit (Z_mod_lt (Int.unsigned i) (Int.unsigned j)). omega. intros MOD.
    unfold Int.modu. rewrite Int.unsigned_repr. omega. omega.
  }
  intros.
  assert (DEFAULT2 : forall i,
            evmatch (Val.modu v (Eval (Vint i))) (uns (provenance x) (usize i))).
  {
    unfold provenance.
    clear H0.
    intros.
    eapply evmatch_uns'.
    unfold Val.modu.
    red ; intros.
    simpl.
    assert (HZ : is_uns (Z.max 0 (usize i)) Int.zero).
    { red ; intros. rewrite Int.bits_zero. reflexivity. }
    case_eq (eSexpr a u v) ; simpl;
    try (exists Int.zero ; split ; [ constructor |]) ; auto.
    intros.
    destruct (Int.eq i Int.zero) eqn:Z.
    +
      exists Int.zero ; split ; [constructor | auto].
    +
      exists (Int.modu i0 i).
      split ; [constructor | auto].
      eapply is_uns_mon; eauto.
      apply UNS.
      (generalize (Int.eq_spec i Int.zero); rewrite Z; auto).
      zify ; omega.
    +
      assert (evmatch (Val.modu v (Eval (Vint i))) (ntop1 x)).
      {
        apply evmatch_ntop1 with (T:= fun v => (Val.modu v (Eval (Vint i)))).
        repeat constructor.
        auto.
      }
      unfold ntop1 in H0.
      inv H0.
      apply H3.
  }
  assert (DEFAULT : evmatch (Val.modu v w) (ntop2 x y)).
  {
    apply evmatch_ntop2 ; repeat constructor ; auto.
  }
  unfold modu.
  destruct y ; auto.
  -
    inv H0.
    unfold is_constant in H3.
    unfold Val.modu in *.
    rewrite <- H3.
    inv H ; eauto.
    destruct (Int.eq n Int.zero) eqn:Z.
    +
      constructor.
      constructor.
      unfold Val.modu.
      depends_prf.
    +
      assert (n <> Int.zero) by (generalize (Int.eq_spec n Int.zero); rewrite Z; auto).
      unfold Val.modu.
      constructor.
      unfold is_constant in *.
      rewrite <- H0.
      repeat intro ; simpl.
      rewrite Z. reflexivity.
Qed.

Definition shrx (v w: aval) :=
  match v, w with
  | I i, I j => if Int.ltu j (Int.repr 31) then I(Int.shrx i j) else ntop
  | _, _ => ntop2 v w
  end.


Lemma shrx_sound:
  forall v w x y,
    evmatch v x -> evmatch w y ->
    evmatch (Val.shrx v w) (shrx x y).
Proof.
  intros.
  assert (evmatch (Val.shrx v w) (ntop2 x y)).
  {
    apply evmatch_ntop2; auto.
    repeat constructor.
  }
  inv H ; inv H0 ; auto.
  unfold Val.shrx.
  rew_cst H2.
  rew_cst H.
  simpl.
  destruct (Int.ltu i0 (Int.repr 31)) eqn:LTU.
  -
    constructor.
    clear H2 H.
    repeat intro.
    simpl. rewrite LTU ; reflexivity.
  -
    unfold ntop.
    constructor.
    constructor.
    depends_prf.
Qed.

Floating-point arithmetic operations

Definition negf := unop_float Float.neg.

Lemma negf_sound:
  forall v x, evmatch v x -> evmatch (Val.negf v) (negf x).
Proof.
  intros.
  apply eunop_float_sound ; auto.
  - repeat constructor.
  - unfold Val.negf.
    simpl.
    intros. rewrite H0 ; reflexivity.
Qed.

Definition absf := unop_float Float.abs.

Lemma absf_sound:
  forall v x, evmatch v x -> evmatch (Val.absf v) (absf x).
Proof.
  intros.
  apply eunop_float_sound ; auto.
  - repeat constructor.
  - unfold Val.absf.
    simpl.
    intros. rewrite H0 ; reflexivity.
Qed.

Definition addf := binop_float Float.add.

Lemma addf_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.addf v w) (addf x y).
Proof.
  intros.
  apply ebinop_float_sound ; auto.
  - repeat constructor.
  - unfold Val.addf.
    simpl.
    intros. rewrite H1 ; rewrite H2; reflexivity.
Qed.

Definition subf := binop_float Float.sub.

Lemma subf_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.subf v w) (subf x y).
Proof.
  intros.
  apply ebinop_float_sound ; auto.
  - repeat constructor.
  - unfold Val.subf.
    simpl.
    intros. rewrite H1 ; rewrite H2; reflexivity.
Qed.

Definition mulf := binop_float Float.mul.

Lemma mulf_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.mulf v w) (mulf x y).
Proof.
  intros.
  apply ebinop_float_sound ; auto.
  - repeat constructor.
  - unfold Val.mulf.
    simpl.
    intros. rewrite H1 ; rewrite H2; reflexivity.
Qed.

Definition divf := binop_float Float.div.

Lemma divf_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.divf v w) (divf x y).
Proof.
  intros.
  apply ebinop_float_sound ; auto.
  - repeat constructor.
  - unfold Val.mulf.
    simpl.
    intros. rewrite H1 ; rewrite H2; reflexivity.
Qed.

Definition negfs := unop_single Float32.neg.

Lemma negfs_sound:
  forall v x, evmatch v x -> evmatch (Val.negfs v) (negfs x).
Proof.
  intros.
  apply eunop_single_sound ; auto.
  - repeat constructor.
  - unfold Val.negfs.
    simpl.
    intros. rewrite H0 ; reflexivity.
Qed.

Definition absfs := unop_single Float32.abs.

Lemma absfs_sound:
  forall v x, evmatch v x -> evmatch (Val.absfs v) (absfs x).
Proof.
  intros.
  apply eunop_single_sound ; auto.
  - repeat constructor.
  - unfold Val.absfs.
    simpl.
    intros. rewrite H0 ; reflexivity.
Qed.

Definition addfs := binop_single Float32.add.

Lemma addfs_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.addfs v w) (addfs x y).
Proof.
  intros.
  apply ebinop_single_sound ; auto.
  - repeat constructor.
  - unfold Val.addfs.
    simpl.
    intros. rewrite H1 ; rewrite H2; reflexivity.
Qed.

Definition subfs := binop_single Float32.sub.

Lemma subfs_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.subfs v w) (subfs x y).
Proof.
  intros.
  apply ebinop_single_sound ; auto.
  - repeat constructor.
  - unfold Val.subfs.
    simpl.
    intros. rewrite H1 ; rewrite H2; reflexivity.
Qed.

Definition mulfs := binop_single Float32.mul.

Lemma mulfs_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.mulfs v w) (mulfs x y).
Proof.
  intros.
  apply ebinop_single_sound ; auto.
  - repeat constructor.
  - unfold Val.mulfs.
    simpl.
    intros. rewrite H1 ; rewrite H2; reflexivity.
Qed.

Definition divfs := binop_single Float32.div.

Lemma divfs_sound:
  forall v x w y, evmatch v x -> evmatch w y -> evmatch (Val.divfs v w) (divfs x y).
Proof.
  intros.
  apply ebinop_single_sound ; auto.
  - repeat constructor.
  - unfold Val.divfs.
    simpl.
    intros. rewrite H1 ; rewrite H2; reflexivity.
Qed.

Conversions

Definition not_int (v : aval) : bool :=
  match v with
    | L _ | F _ | FS _ => true
    | _ => false
  end.


Definition zero_ext (nbits: Z) (v: aval) :=
  if zlt nbits Int.zwordsize || not_int v
  then
    match v with
      | I i => I (Int.zero_ext nbits i)
      | Ptr p => uns (provenance v) nbits
      | Uns p n => uns (poffset p) (Z.min n nbits)
      | _ => uns (provenance v) nbits
    end
  else v.

Lemma is_uns_zwordsize :
  forall n i, n >= Int.zwordsize -> is_uns n i.
Proof.
  intros.
  unfold is_uns.
  intros.
  omega.
Qed.

Lemma zero_ext_zero :
  forall nbits, Int.zero_ext nbits Int.zero = Int.zero.
Proof.
  intros.
  rewrite <- is_uns_zero_ext.
  repeat intro.
  apply Int.bits_zero.
Qed.
  
Lemma epmatch_zero_ext :
  forall v p nbits
         (MATCH : epmatch v p)
         (GE : nbits >= Int.zwordsize),
   epmatch (Val.zero_ext nbits v) p.
Proof.
  intros.
  inv MATCH ; try constructor ; depends_prf.
  *
    rewrite epmatch_same_eval with (y:=v) (y0 := Gl id ofs).
    econstructor ; eauto.
    unfold Val.zero_ext.
    rew_cst H0.
    repeat intro.
    simpl. rewrite Int.zero_ext_above;auto.
    reflexivity.
  *
    rewrite epmatch_same_eval with (y:=v) (y0 := Stk ofs).
    econstructor ; eauto.
    unfold Val.zero_ext.
    rew_cst H0.
    repeat intro.
    simpl. rewrite Int.zero_ext_above;auto.
    reflexivity.
Qed.

  
Lemma zero_ext_sound:
  forall nbits v x, evmatch v x -> evmatch (Val.zero_ext nbits v) (zero_ext nbits x).
Proof.
  assert (DFL: forall nbits i, is_uns nbits (Int.zero_ext nbits i)).
  {
    intros; red; intros. rewrite Int.bits_zero_ext by omega. apply zlt_false; auto.
  }
  assert (DEFAULTMX :
            forall nbits v p ,
              epmatch v p ->
              evmatch (Val.zero_ext nbits v) (uns (poffset p) Int.zwordsize)).
  {
    intros.
    apply evmatch_uns.
    unfold is_unsigned.
    unfold Val.zero_ext.
    simpl.
    intros.
    case_eq (eSexpr a u v) ; simpl ; intros;
    try
      (exists (Int.zero_ext nbits Int.zero);
        split;[constructor | auto]); try (apply is_uns_zwordsize;omega).
    exists (Int.zero_ext nbits i).
    split ; simpl ; auto.
    apply is_uns_zwordsize; omega.
    apply epmatch_poffset ; auto.
    repeat constructor.
  }
  assert (DEFAULT2 :
            forall nbits v p ,
              epmatch v p ->
              evmatch (Val.zero_ext nbits v) (uns (poffset p) nbits)).
  {
    intros.
    apply evmatch_uns.
    unfold is_unsigned.
    unfold Val.zero_ext.
    simpl.
    intros.
    case_eq (eSexpr a u v) ; simpl ; intros;
    try
      (exists (Int.zero_ext nbits Int.zero);
        split;[constructor | auto]).
    exists (Int.zero_ext nbits i).
    split ; simpl ; auto.
    apply epmatch_poffset ; auto.
    repeat constructor.
  }
  assert (DEFAULT : forall n nbits v p
                           (HLE : 0 <= n),
                      is_unsigned n v ->
                      epmatch v p ->
                      evmatch (Val.zero_ext nbits v) (uns (poffset p) (Z.min n nbits))).
  {
    intros.
    apply evmatch_uns.
    revert H.
    apply is_unsigned_unsigned with (Ti := fun i => Int.zero_ext nbits i).
    -
      intros.
      unfold Val.zero_ext.
      simpl.
      inv H; try constructor.
      rewrite H3.
      constructor.
    -
      intros.
      red; intros. zify.
      rewrite Int.bits_zero_ext by omega.
      destruct (zlt m nbits); auto. apply H; omega.
    -
      apply epmatch_poffset ; auto.
      repeat constructor.
  }
  intros.
  unfold zero_ext.
  case_eq ((zlt nbits Int.zwordsize) || not_int x); intro CASE.
  inv H; simpl; unfold provenance, aptr_of_aval ; auto with va.
  - constructor.
     unfold Val.zero_ext.
     rew_cst H0.
     repeat intro.
     simpl. reflexivity.
  -
    apply DEFAULT2; auto.
    constructor; auto. depends_prf.
  -
    apply DEFAULT2; auto.
    constructor; auto. depends_prf.
  - apply DEFAULT2 ; auto.
    constructor; auto. depends_prf.
  -
    rewrite orb_false_iff in CASE.
    destruct CASE as [C1 C2].
    unfold proj_sumbool in C1.
    destruct (zlt nbits Int.zwordsize); try congruence.
    inv H ; constructor; try omega ; simpl in C2 ; try congruence.
    +
      unfold Val.zero_ext.
      rew_cst H0.
      repeat intro.
      simpl.
      rewrite Int.zero_ext_above ; auto.
    +
      revert H1.
      apply is_unsigned_unsigned with (Ti := fun x => Int.zero_ext nbits x);
        unfold Val.zero_ext.
      *
        repeat intro; simpl.
        inv H. rewrite H4 ; simpl ; constructor.
        constructor.
      *
        intros.
        rewrite Int.zero_ext_above ; auto.
    +
      apply epmatch_zero_ext ; auto.
    +
      revert H1.
      apply is_signed_signed with (Ti := fun x => Int.zero_ext nbits x);
        unfold Val.zero_ext.
      *
        repeat intro; simpl.
        inv H. rewrite H4 ; simpl ; constructor.
        constructor.
      *
        intros.
        rewrite Int.zero_ext_above ; auto.
    +
      apply epmatch_zero_ext ; auto.
    +
      apply epmatch_zero_ext ; auto.
Qed.

Definition sign_ext (nbits: Z) (v: aval) :=
  match v with
  | I i => I (Int.sign_ext nbits i)
  | Ptr p => if zlt nbits Int.zwordsize then sgn (provenance v) nbits
               else Ptr p
  | Uns p n => if zlt nbits Int.zwordsize
               then
                 if zlt n nbits then Uns (poffset p) n
                 else sgn (poffset p) nbits
               else Uns p n
  | Sgn p n => if zlt nbits Int.zwordsize
               then sgn (poffset p) (Z.min n nbits)
               else Sgn p n
  | _ => sgn (provenance v) nbits
  end.

Lemma sign_ext_deflt :
  forall nbits,
    0 < nbits ->
    forall p v,
      epmatch v p->
      evmatch (Val.sign_ext nbits v) (sgn (poffset p) nbits).
Proof.
  intros. apply vmatch_sgn.
  repeat intro.
  unfold Val.sign_ext.
  simpl.
  case_eq (eSexpr a u v) ; intros ; simpl;
  try
    (exists Int.zero;
            split ; [constructor|
                     red ; intros;
                     repeat rewrite Int.bits_zero ;auto]).
  exists (Int.sign_ext nbits i).
    split. simpl; constructor.
    apply is_sign_ext_sgn; auto with va.
    apply epmatch_poffset; auto. repeat constructor ; auto.
Qed.

Lemma sign_ext_zwordsize :
  forall v p nbits,
    epmatch v p ->
    nbits >= Int.zwordsize ->
   epmatch (Val.sign_ext nbits v) p.
Proof.
  intros.
  inv H ; try constructor ; depends_prf.
  -
    rewrite epmatch_same_eval with (y:=v) (y0 := Gl id ofs).
    econstructor ; eauto.
    unfold Val.sign_ext.
    rew_cst H2.
    repeat intro.
    simpl. rewrite Int.sign_ext_above;auto.
    reflexivity.
  -
    rewrite epmatch_same_eval with (y:=v) (y0 := Stk ofs).
    econstructor ; eauto.
    unfold Val.sign_ext.
    rew_cst H2.
    repeat intro.
    simpl. rewrite Int.sign_ext_above;auto.
    reflexivity.
Qed.

Lemma sign_ext_sound:
  forall nbits v x, 0 < nbits -> evmatch v x -> evmatch (Val.sign_ext nbits v) (sign_ext nbits x).
Proof.
  assert (DFL:= sign_ext_deflt).
  intros. inv H0; simpl; auto with va.
  -
    unfold Val.sign_ext.
    rew_cst H1.
    constructor.
    repeat intro; simpl.
    reflexivity.
  -
    destruct (zlt nbits Int.zwordsize).
    +
    destruct (zlt n nbits); eauto with va.
    constructor; auto.
    revert H2.
    apply is_unsigned_unsigned with (Ti := fun i => Int.sign_ext nbits i).
    *
      intros.
      unfold Val.sign_ext; simpl.
      inv H0.
      rewrite H5. simpl ; constructor.
      simpl ; constructor.
    * intros.
      eapply is_sign_ext_uns; eauto with va.
    *
      apply epmatch_poffset ; auto.
      repeat constructor.
    +
      constructor ; auto.
      revert H2.
      apply is_unsigned_unsigned with (Ti := fun i => Int.sign_ext nbits i).
      *
        intros.
        unfold Val.sign_ext; simpl.
        inv H0.
        rewrite H5. simpl ; constructor.
        simpl ; constructor.
      * intros.
        repeat intro.
        rewrite Int.sign_ext_above ; auto.
      *
        apply sign_ext_zwordsize ; auto.
  -
    destruct (zlt nbits Int.zwordsize).
    +
    apply vmatch_sgn.
    revert H2.
    apply is_signed_signed with (Ti := fun i => Int.sign_ext nbits i).
      intros.
      unfold Val.sign_ext; simpl.
      inv H0.
      rewrite H5. simpl ; constructor.
      simpl ; constructor.
    * intros.
      eapply is_sign_ext_sgn; eauto with va.
      apply Z.min_case; auto with va.
    *
      apply epmatch_poffset ; auto ; repeat constructor.
    +
      constructor; auto.
      revert H2.
      apply is_signed_signed with (Ti := fun i => Int.sign_ext nbits i).
      *
        intros.
        unfold Val.sign_ext; simpl.
        inv H0.
        rewrite H5. simpl ; constructor.
        simpl ; constructor.
      * intros.
        repeat intro.
        rewrite Int.sign_ext_above ; auto.
      *
        apply sign_ext_zwordsize ; auto.
  -
    unfold provenance.
    apply DFL; auto.
    simpl. constructor ; depends_prf.
  -
    unfold provenance.
    apply DFL; auto.
    simpl. constructor ; depends_prf.
  -
    unfold provenance.
    apply DFL; auto.
    simpl. constructor ; depends_prf.
  -
    unfold provenance.
    destruct (zlt nbits Int.zwordsize).
    apply DFL; auto.
    constructor.
    apply sign_ext_zwordsize; auto.
Qed.

Definition singleoffloat (v: aval) :=
  match v with
  | F f => FS (Float.to_single f)
  | _ => ntop1 v
  end.

Lemma singleoffloat_sound:
  forall v x, evmatch v x -> evmatch (Val.singleoffloat v) (singleoffloat x).
Proof.
  intros.
  assert (DEFAULT: evmatch (Val.singleoffloat v) (ntop1 x)).
  {
    apply evmatch_ntop1; auto.
    repeat constructor; auto.
  }
  destruct x; auto. inv H. constructor.
  repeat intro.
  simpl.
  rew_cst H2; auto.
Qed.

Definition floatofsingle (v: aval) :=
  match v with
  | FS f => F (Float.of_single f)
  | _ => ntop1 v
  end.

Lemma floatofsingle_sound:
  forall v x, evmatch v x -> evmatch (Val.floatofsingle v) (floatofsingle x).
Proof.
  intros.
  assert (DEFAULT: evmatch (Val.floatofsingle v) (ntop1 x)).
  {
    apply evmatch_ntop1 ; auto.
    repeat constructor.
  }
  destruct x; auto. inv H. constructor.
  repeat intro.
  simpl. rew_cst H2; auto.
Qed.

Definition intoffloat (x:aval) := ntop1 x.

Lemma intoffloat_sound:
  forall v x, evmatch v x -> evmatch (Val.intoffloat v) (intoffloat x).
Proof.
  intros. eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.



Definition intuoffloat (x: aval) := ntop1 x.

Lemma intuoffloat_sound:
  forall v x, evmatch v x -> evmatch (Val.intuoffloat v) (intuoffloat x).
Proof.
 intros.
 eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.


Definition floatofint (x: aval) := ntop1 x.

Lemma floatofint_sound:
  forall v x, evmatch v x -> evmatch (Val.floatofint v) (floatofint x).
Proof.
 intros.
 eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.


Definition floatofintu (x: aval) := ntop1 x.

Lemma floatofintu_sound:
  forall v x, evmatch v x -> evmatch (Val.floatofintu v) (floatofintu x).
Proof.
 intros.
 eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.


Definition intofsingle (x: aval) := ntop1 x.

Lemma intofsingle_sound:
  forall v x, evmatch v x -> evmatch (Val.intofsingle v) (intofsingle x).
Proof.
 intros.
 eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.


Definition intuofsingle (x: aval) := ntop1 x.

Lemma intuofsingle_sound:
  forall v x, evmatch v x -> evmatch (Val.intuofsingle v) (intuofsingle x).
Proof.
 intros.
 eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.


Definition singleofint (x: aval) := ntop1 x.

Lemma singleofint_sound:
  forall v x, evmatch v x -> evmatch (Val.singleofint v) (singleofint x).
Proof.
 intros.
 eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.


Definition singleofintu (x: aval) := ntop1 x.
 
Lemma singleofintu_sound:
  forall v x, evmatch v x -> evmatch (Val.singleofintu v) (singleofintu x).
Proof.
 intros.
 eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.



Definition floatofwords (x y: aval) := ntop2 x y.

Lemma floatofwords_sound:
  forall v x y w, evmatch v x -> evmatch w y -> evmatch (Val.floatofwords v w) (floatofwords x y).
Proof.
 intros.
 eapply evmatch_ntop2 ; repeat constructor ; auto.
Qed.



Definition longofwords (x y : aval) := ntop2 x y.

Lemma longofwords_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.longofwords v w) (longofwords x y).
Proof.
 intros.
 eapply evmatch_ntop2 ; repeat constructor ; auto.
Qed.


Definition loword (x: aval) := ntop1 x.

Lemma loword_sound: forall v x, evmatch v x -> evmatch (Val.loword v) (loword x).
Proof.
 intros.
 eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.


Definition hiword (x: aval) := ntop1 x.

Lemma hiword_sound: forall v x, evmatch v x -> evmatch (Val.hiword v) (hiword x).
Proof.
 intros.
 eapply evmatch_ntop1 ; repeat constructor ; auto.
Qed.


Comparisons and variation intervals

Definition cmp_intv (c: comparison) (i: Z * Z) (n: Z) : abool :=
  let (lo, hi) := i in
  match c with
  | Ceq => if zlt n lo || zlt hi n then Maybe false else Btop
  | Cne => Btop
  | Clt => if zlt hi n then Maybe true else if zle n lo then Maybe false else Btop
  | Cle => if zle hi n then Maybe true else if zlt n lo then Maybe false else Btop
  | Cgt => if zlt n lo then Maybe true else if zle hi n then Maybe false else Btop
  | Cge => if zle n lo then Maybe true else if zlt hi n then Maybe false else Btop
  end.

Definition zcmp (c: comparison) (n1 n2: Z) : bool :=
  match c with
  | Ceq => zeq n1 n2
  | Cne => negb (zeq n1 n2)
  | Clt => zlt n1 n2
  | Cle => zle n1 n2
  | Cgt => zlt n2 n1
  | Cge => zle n2 n1
  end.

Lemma zcmp_intv_sound:
  forall c i x n,
  fst i <= x <= snd i ->
  cmatch (Some (zcmp c x n)) (cmp_intv c i n).
Proof.
  intros c [lo hi] x n; simpl; intros R.
  destruct c; unfold zcmp, proj_sumbool.
-
  destruct (zlt n lo). rewrite zeq_false by omega. constructor.
  destruct (zlt hi n). rewrite zeq_false by omega. constructor.
  constructor.
-
  constructor.
-
  destruct (zlt hi n). rewrite zlt_true by omega. constructor.
  destruct (zle n lo). rewrite zlt_false by omega. constructor.
  constructor.
-
  destruct (zle hi n). rewrite zle_true by omega. constructor.
  destruct (zlt n lo). rewrite zle_false by omega. constructor.
  constructor.
-
  destruct (zlt n lo). rewrite zlt_true by omega. constructor.
  destruct (zle hi n). rewrite zlt_false by omega. constructor.
  constructor.
-
  destruct (zle n lo). rewrite zle_true by omega. constructor.
  destruct (zlt hi n). rewrite zle_false by omega. constructor.
  constructor.
Qed.

Lemma cmp_intv_None:
  forall c i n, cmatch None (cmp_intv c i n).
Proof.
  unfold cmp_intv; intros. destruct i as [lo hi].
  destruct c.
-
  destruct (zlt n lo). constructor. destruct (zlt hi n); constructor.
-
  constructor.
-
  destruct (zlt hi n). constructor. destruct (zle n lo); constructor.
-
  destruct (zle hi n). constructor. destruct (zlt n lo); constructor.
-
  destruct (zlt n lo). constructor. destruct (zle hi n); constructor.
-
  destruct (zle n lo). constructor. destruct (zlt hi n); constructor.
Qed.

Definition uintv (v: aval) : Z * Z :=
  match v with
  | I n => (Int.unsigned n, Int.unsigned n)
  | Uns _ n => if zlt n Int.zwordsize then (0, two_p n - 1) else (0, Int.max_unsigned)
  | _ => (0, Int.max_unsigned)
  end.

Lemma is_unsigned_const :
  forall n i align bound
         (NOFORGERY : no_forgery Int.max_unsigned bound align)
  ,
    is_unsigned n (Eval (Vint i)) ->
    is_uns n i.
Proof.
  intros.
  unfold is_unsigned in H.
  destruct (NOFORGERY xH) as [cm [COMPAT HH]].
  destruct (H cm (fun _ _ => Byte.zero) ); auto.
  simpl in H0.
  destruct H0. inv H0. auto.
Qed.


Lemma uintv_sound:
  forall e v (MATCH : evmatch e v)
         a
         u i
         (EVAL : eSexpr a u e = Vint i)
  ,
    (fst (uintv v)) <= Int.unsigned i <= (snd (uintv v)).
Proof.
  intros.
  assert (DFL : 0 <= Int.unsigned i <= Int.max_unsigned).
  {
    apply Int.unsigned_range_2.
  }
    inv MATCH; simpl; try apply DFL.
  -
    rew_cst H;auto.
    simpl in EVAL. inv EVAL ; omega.
  - destruct (zlt n Int.zwordsize); simpl.
  +
    unfold is_unsigned in H0.
    destruct (H0 a u ).
    destruct H2. rewrite EVAL in H2.
    inv H2.
    rewrite is_uns_zero_ext in H3. rewrite <- H3. rewrite Int.zero_ext_mod by omega.
  exploit (Z_mod_lt (Int.unsigned x) (two_p n)). apply two_p_gt_ZERO; auto. omega.
  +
    apply DFL.
Qed.

Lemma cmpu_intv_sound:
  forall c e v1 n2,
    evmatch e v1 ->
    ecmatch (Val.cmpu_bool c e (Eval (Vint n2))) (cmp_intv c (uintv v1) (Int.unsigned n2)).
Proof.
  intros.
  assert (HUNINT := uintv_sound e v1 H).
  destruct (uintv v1) as [lb ub].
  clear H.
  simpl in *.
  destruct c.
  -
    case_eq (zlt (Int.unsigned n2) lb || zlt ub (Int.unsigned n2)) ; constructor.
    simpl.
    repeat intro.
    simpl.
    case_eq (eSexpr a u e) ; simpl ; try constructor.
    intros.
    predSpec Int.eq Int.eq_spec i n2 ; try constructor.
    exfalso.
    subst.
    rewrite orb_true_iff in H.
    unfold proj_sumbool in H.
    specialize (HUNINT a u _ H0).
    destruct H.
    destruct (zlt (Int.unsigned n2) lb) ; try congruence.
    omega.
    destruct (zlt ub (Int.unsigned n2)) ; try congruence.
    omega.
    apply is_bool_cmpu_bool.
  -
  constructor. apply is_bool_cmpu_bool.
-
  destruct (zlt ub (Int.unsigned n2)).
  constructor.
  repeat intro. simpl.
  case_eq (eSexpr a u e) ; simpl ; try constructor.
  unfold Int.ltu.
  intros. eapply HUNINT in H ; eauto.
  destruct (zlt (Int.unsigned i) (Int.unsigned n2) ) ; try constructor.
  omega.
  destruct (zle (Int.unsigned n2) lb) ; try constructor.
  repeat intro ; simpl.
  case_eq (eSexpr a u e) ; simpl ; try constructor.
  unfold Int.ltu.
  intros. eapply HUNINT in H ; eauto.
  destruct (zlt (Int.unsigned i) (Int.unsigned n2) ) ; try constructor.
  omega.
  apply is_bool_cmpu_bool.
-
  destruct (zle ub (Int.unsigned n2)).
  +
  constructor.
  repeat intro. simpl.
  case_eq (eSexpr a u e) ; simpl ; try constructor.
  unfold Int.ltu.
  intros. eapply HUNINT in H ; eauto.
  destruct (zlt (Int.unsigned n2) (Int.unsigned i) ) ; try constructor.
  omega.
  +
    destruct (zlt (Int.unsigned n2) lb );
    constructor.
    repeat intro. simpl.
    case_eq (eSexpr a u e) ; simpl ; try constructor.
    unfold Int.ltu.
    intros. eapply HUNINT in H ; eauto.
    destruct (zlt (Int.unsigned n2) (Int.unsigned i) ) ; try constructor.
    omega.
    apply is_bool_cmpu_bool.
-
  destruct (zlt (Int.unsigned n2) lb) ; try constructor.
  repeat intro;simpl.
  case_eq (eSexpr a u e) ; simpl ; try constructor.
  unfold Int.ltu.
  intros. eapply HUNINT in H ; eauto.
  destruct (zlt (Int.unsigned n2) (Int.unsigned i) ) ; try constructor.
  omega.
  destruct (zle ub (Int.unsigned n2)) ; try constructor.
  repeat intro;simpl.
  case_eq (eSexpr a u e) ; simpl ; try constructor.
  unfold Int.ltu.
  intros. eapply HUNINT in H ; eauto.
  destruct (zlt (Int.unsigned n2) (Int.unsigned i) ) ; try constructor.
  omega. apply is_bool_cmpu_bool.
-
  destruct (zle (Int.unsigned n2) lb) ; try constructor.
  repeat intro;simpl.
  case_eq (eSexpr a u e) ; simpl ; try constructor.
  unfold Int.ltu.
  intros. eapply HUNINT in H ; eauto.
  destruct (zlt (Int.unsigned i) (Int.unsigned n2) ) ; try constructor.
  omega.
  destruct (zlt ub (Int.unsigned n2)) ; try constructor.
  repeat intro;simpl.
  case_eq (eSexpr a u e) ; simpl ; try constructor.
  unfold Int.ltu.
  intros. eapply HUNINT in H ; eauto.
  destruct (zlt (Int.unsigned i) (Int.unsigned n2) ) ; try constructor.
  omega.
  apply is_bool_cmpu_bool.
Qed.


Lemma cmpu_intv_sound_2:
  forall c e v1 n2,
  evmatch e v1 ->
  ecmatch (Val.cmpu_bool c (Eval (Vint n2)) e) (cmp_intv (swap_comparison c) (uintv v1) (Int.unsigned n2)).
Proof.
  intros.
  rewrite cmatch_morph with (y := Val.cmpu_bool (swap_comparison c) e (Eval (Vint n2))).
  apply cmpu_intv_sound.
  apply H.
  repeat intro.
  simpl.
  destruct (eSexpr cm em e) ; destruct c ; simpl ; try reflexivity.
  -
  rewrite Int.eq_sym. reflexivity.
  - rewrite Int.eq_sym. reflexivity.
  - reflexivity.
Qed.

Definition sintv (v: aval) : Z * Z :=
  match v with
  | I n => (Int.signed n, Int.signed n)
  | Uns _ n =>
      if zlt n Int.zwordsize then (0, two_p n - 1) else (Int.min_signed, Int.max_signed)
  | Sgn _ n =>
      if zlt n Int.zwordsize
      then (let x := two_p (n-1) in (-x, x-1))
      else (Int.min_signed, Int.max_signed)
  | _ => (Int.min_signed, Int.max_signed)
  end.

Comparisons
Definition not_a_pointer (i : int) : bool :=
  Int.eq i Int.zero || Int.eq i Int.mone.

Definition ceq (i : int) : abool :=
  if not_a_pointer i
  then Just false
  else Btop.

Definition clt (i : int) : abool :=
  if Int.eq i Int.mone
  then Just true
  else if Int.eq i Int.zero
       then Just false
       else Btop.

Definition cmeet (b1 b2 : abool) : abool :=
  match b1, b2 with
    | Btop , x | x , Btop => x
    | Maybe b1 , Just b2
    | Just b2 , Maybe b1 => if eqb b1 b2 then Just b2 else Bnone
    | Bnone , _ | _ , Bnone => Bnone
    | Just b1 , Just b2 => if eqb b1 b2 then Just b1 else Bnone
    | Maybe b1 , Maybe b2 => if eqb b1 b2 then Maybe b1 else Bnone
  end.

Lemma eval_expr_val_of_bool :
  forall b b' a u,
    eSexpr a u (Eval (val_of_bool b)) =
    eSexpr a u (Eval (val_of_bool b')) ->
    b = b'.
Proof.
  intros.
  simpl in H.
  assert (Vtrue <> Vfalse).
  { unfold Vtrue, Vfalse.
      generalize Int.one_not_zero.
      congruence.
  }
  destruct b ; destruct b' ; simpl in H ; try congruence.
Qed.


Lemma same_eval_val_of_bool :
  forall b b',
    same_eval (Eval (val_of_bool b)) (Eval (val_of_bool b')) ->
    b = b'.
Proof.
  intros.
  unfold same_eval in H.
  eapply eval_expr_val_of_bool with (a:=(fun _ => Int.zero)) (u :=fun _ _ => Byte.zero);
    eauto.
Qed.
  
Lemma is_wk_cst_bool :
  forall b b' e
         (WK : is_wk_constant (val_of_bool b) e)
         (CST : is_constant (val_of_bool b') e),
   ecmatch e (if eqb b b' then Just b' else Bnone).
Proof.
  unfold is_constant, is_wk_constant in *.
  intros.
  case_eq (eqb b b') ; constructor.
  -
    rewrite eqb_true_iff in H.
    subst.
    repeat intro.
    unfold same_eval in CST.
    generalize (CST cm em).
    generalize (WK cm em).
    intros. auto.
  -
    rewrite eqb_false_iff in H.
    repeat intro.
    unfold same_eval in CST.
    generalize (CST cm em).
    generalize (WK cm em).
    intros.
    inv H0; auto.
    rewrite <- H1 in H4.
    apply eval_expr_val_of_bool in H4.
    congruence.
Qed.
    
Lemma eqb_sym : forall b b', eqb b b' = eqb b' b.
Proof.
  destruct b ; destruct b' ; reflexivity.
Qed.
  


Definition cor (b b' : abool) : abool :=
  match b , b' with
    | Bnone , _ | _ , Bnone => Bnone
    | Just b, Just b' => Just (b || b')
    | Maybe b , Maybe b' => Maybe (b || b')
    | Just b , Maybe b' | Maybe b' , Just b => Maybe (b || b')
    | _ , Btop | Btop , _ => Btop

  end.


Definition ccomp (c : comparison) (i:int) : abool :=
  match c with
    | Ceq => ceq i
    | Cne => cnot (ceq i)
    | Clt => clt i
    | Cle => cor (clt i) (ceq i)
    | Cgt => cnot (cor (clt i) (ceq i) )
    | Cge => cnot (clt i)
  end.
    
Definition pcmp_int (c : comparison) (p : aptr) (i : int) : abool :=
  match p with
    | Pbot => Bnone
    | Pcst => Btop
    | Gl id ofs => if in_bound_glob id ofs
                   then ccomp c i
                   else Btop
    | Stk ofs => if in_bound_stack ofs
                   then ccomp c i
                   else Btop
    | _ => Btop
  end.

Definition cmpu_bool (c: comparison) (v w: aval) : abool :=
  match v, w with
  | I i1, I i2 => Just (Int.cmpu c i1 i2)
  | Ptr p, I i => pcmp_int c p i
  | I i, Ptr p => pcmp_int (swap_comparison c) p i
  | Ptr p1, Ptr p2 => pcmp c p1 p2
  | Ptr p1, ( Uns p2 _ | Sgn p2 _) =>
    Btop
  | ( Uns p1 _ | Sgn p1 _), Ptr p2 => Btop
  | _, I i => (cmp_intv c (uintv v) (Int.unsigned i))
  | I i, _ => (cmp_intv (swap_comparison c) (uintv w) (Int.unsigned i))
  | _, _ => Btop
  end.

Lemma not_a_pointer_sound :
  forall ofs b a align bound
         (BD : in_bound (Int.unsigned ofs) (bound b))
         (COMPAT : compat Int.max_unsigned bound align a)
         (NOTPTR : not_a_pointer (Int.add (a b) ofs) = true),
    False.
Proof.
  intros.
  exploit addr_space ; eauto.
  unfold not_a_pointer in NOTPTR.
  rewrite orb_true_iff in NOTPTR.
  destruct NOTPTR;
    apply Cop.int_eq_true in H;
    rewrite H.
  rewrite Int.unsigned_zero. omega.
  unfold Int.max_unsigned.
  rewrite Int.unsigned_mone.
  compute. intuition congruence.
Qed.

Lemma cmpu_bool_negate :
  forall c e e',
         same_eval
         (Val.cmpu_bool c e e')
         (Val.notbool (Val.cmpu_bool (negate_comparison c) e e')).
Proof.
  repeat intro.
  unfold Val.cmpu_bool, Val.notbool.
  simpl.
  unfold ExprEval.cmpu_bool.
  destruct (eSexpr cm em e) ; destruct (eSexpr cm em e') ; try reflexivity.
  rewrite Int.negate_cmpu.
  simpl.
  destruct (Int.cmpu c i i0); auto.
Qed.


Lemma same_eval_cmpu_le :
  forall x y,
  same_eval
    (Val.cmpu_bool Cle x y)
    (Val.or (Val.cmpu_bool Clt x y)
            (Val.cmpu_bool Ceq x y)).
Proof.
  repeat intro.
  simpl.
  destruct (eSexpr cm em x) , (eSexpr cm em y) ; simpl ; try reflexivity.
  unfold Int.ltu.
  destruct (zlt (Int.unsigned i0) (Int.unsigned i)) ; try reflexivity.
  destruct (zlt (Int.unsigned i) (Int.unsigned i0)) ; try reflexivity.
  omega.
  predSpec Int.eq Int.eq_spec i i0; try reflexivity.
  simpl. subst. omega.
  simpl.
  destruct (zlt (Int.unsigned i) (Int.unsigned i0)) ; try reflexivity.
  predSpec Int.eq Int.eq_spec i i0; try reflexivity.
  predSpec Int.eq Int.eq_spec i i0; try reflexivity.
  assert (Int.unsigned i = Int.unsigned i0) by omega.
  apply inj_unsigned in H0; auto.
  tauto.
Qed.

Definition is_val_bool (v : val) :=
  v = Vundef \/ v = Vfalse \/ v = Vtrue.

Lemma is_bool_or :
  forall e1 e2
  ,
    is_bool e1 -> is_bool e2 ->
    is_bool (Val.or e1 e2).
Proof.
  repeat intro.
  simpl.
  destruct (H a u).
  destruct (H0 a u).
  destruct H1 ; destruct H2.
  destruct (eSexpr a u e1), (eSexpr a u e2) ;
    try (exists Int.zero ; intuition constructor);
    try (exists Int.one ; intuition constructor).
  simpl.
  inv H1.
  inv H2.
  intuition subst ;
  try (exists Int.zero ; intuition constructor);
    try (exists Int.one ; intuition constructor).
Qed.
  
Lemma or_bool_sound : forall e1 v1 e2 v2,
                        ecmatch e1 v1 ->
                        ecmatch e2 v2 ->
                        ecmatch (Val.or e1 e2) (cor v1 v2).
Proof.
  intros.
  inv H ; simpl ; try constructor; unfold Val.or.
  -
    rew_cst H1 ; repeat intro ; reflexivity.
  -
    rew_cst H1.
    inv H0 ; try constructor.
    +
    rew_cst H.
    repeat intro ; simpl.
    destruct (eSval cm (val_of_bool b)) ; reflexivity.
    +
    rew_cst H.
    repeat intro ; try reflexivity.
    destruct b ; destruct b0 ; reflexivity.
    +
      repeat intro.
      specialize (H a u).
      inv H.
      simpl. rewrite H3.
      destruct b ; destruct b0 ; constructor.
      simpl. rewrite <- H2.
      destruct b ; destruct b0 ; constructor.
    + apply is_bool_or; auto with va.
  -
    inv H0 ; constructor.
    +
    rew_cst H.
    repeat intro ; simpl.
    destruct (eSexpr cm em e1) ; reflexivity.
    +
    repeat intro.
    simpl.
    rew_cst H.
    specialize (H1 a u).
    inv H1.
    erewrite H; eauto. erewrite <- H ; eauto.
    rewrite H3.
    destruct b ; destruct b0 ; constructor.
    auto.
    +
    repeat intro.
    specialize (H1 a u).
    specialize (H a u).
    simpl.
    inv H1 ; inv H ; try constructor.
    rewrite H3 ; rewrite H2 ; simpl.
    destruct b ; destruct b0 ; constructor.
    rewrite H3.
    destruct b ; simpl ; constructor.
    +
      apply is_bool_or; auto.
      eapply is_wk_constant_is_bool ; eauto.
  -
    inv H0 ; constructor.
    rew_cst H.
    repeat intro ; simpl.
    destruct (eSexpr cm em e1) ; reflexivity.
    apply is_bool_or ; eauto with va.
    rew_cst H ; auto with va.
    apply is_bool_or ; eauto with va.
    apply is_bool_or ; eauto with va.
Qed.

    
Lemma cmpu_pointer_int_sound :
  forall v p i w c
         (PMATCH : epmatch v p)
         (CONST : is_constant (Vint i) w),
    ecmatch (Val.cmpu_bool c v w) (pcmp_int c p i).
Proof.
  intros.
  unfold Val.cmpu_bool.
  rew_cst CONST.
  clear CONST.
  inv PMATCH ; simpl; try constructor; try apply is_bool_cmpu_bool.
Qed.

  
Lemma cmpu_bool_swap_comparison :
  forall c e e',
         same_eval
         (Val.cmpu_bool c e e')
         (Val.cmpu_bool (swap_comparison c) e' e).
Proof.
  repeat intro.
  unfold Val.cmpu_bool.
  simpl.
  unfold ExprEval.cmpu_bool.
  destruct (eSexpr cm em e) ; destruct (eSexpr cm em e') ; try reflexivity.
  rewrite Int.swap_cmpu.
  reflexivity.
Qed.




Lemma cmpu_bool_sound:
  forall c v w x y, evmatch v x -> evmatch w y -> ecmatch (Val.cmpu_bool c v w) (cmpu_bool c x y).
Proof.
  intros.
  inv H ; inv H0 ; unfold cmpu_bool; try (simpl ; constructor; fail);
  try (constructor ; apply is_bool_cmpu_bool ; eauto with va);
  try (unfold Val.cmpu_bool; rew_cst H1;apply cmpu_intv_sound_2; constructor ; auto; fail);
  try (unfold Val.cmpu_bool; rew_cst H;apply cmpu_intv_sound; constructor ; auto; fail).
  -
    constructor.
    unfold Val.cmpu_bool.
    rew_cst H1. rew_cst H.
    repeat intro.
    simpl.
    destruct (Int.cmpu c i i0) ; reflexivity.
  -
    rewrite cmpu_bool_swap_comparison.
    eapply cmpu_pointer_int_sound ; eauto.
  - eapply cmpu_pointer_int_sound ; eauto.
  -
    eapply pcmp_sound; auto.
Qed.

Definition cmp_bool (c: comparison) (v w: aval) := Btop.

Lemma cmp_bool_sound:
  forall c v w x y, evmatch v x -> evmatch w y -> ecmatch (Val.cmp_bool c v w) (cmp_bool c x y).
Proof.
 intros.
 unfold cmp_bool.
 constructor.
 repeat intro.
 unfold Val.cmp_bool. simpl.
 destruct (eSexpr a u v); destruct (eSexpr a u w) ; simpl;
 try ( exists Int.zero ; repeat constructor; fail).
 destruct (Int.cmp c i i0).
 exists Int.one ; repeat split. constructor. tauto.
 exists Int.zero ; repeat split. constructor. tauto.
Qed.



Lemma eSval_bool : forall b a,
   eSval a (val_of_bool b) =
   (if b then Vtrue else Vfalse).
Proof.
  destruct b ; reflexivity.
Qed.

Definition cmpf_bool (c: comparison) (v w: aval) : abool :=
  match v, w with
  | F f1, F f2 => Just (Float.cmp c f1 f2)
  | _, _ => Btop
  end.

Lemma cmpf_is_bool :
  forall c v w, is_bool (Val.cmpf_bool c v w).
Proof.
  unfold Val.cmpf_bool.
  repeat intro ; simpl.
  generalize ((Values.Val.cmpf_bool c (eSexpr a u v) (eSexpr a u w))).
  intros.
  destruct o ; simpl.
  destruct b;
    try (exists Int.zero ; intuition constructor);
    try (exists Int.one ; intuition constructor).
  exists Int.zero ; intuition.
Qed.
  
Lemma cmpf_bool_sound:
  forall c v w x y, evmatch v x -> evmatch w y -> ecmatch (Val.cmpf_bool c v w) (cmpf_bool c x y).
Proof.
  intros.
  generalize (cmpf_is_bool c v w).
  inv H; try constructor; inv H0; try constructor;
  unfold Val.cmpf_bool in * ; auto.
  rew_cst H1.
  rew_cst H.
  repeat intro; simpl.
  apply eSval_bool.
Qed.


Definition cmpfs_bool (c: comparison) (v w: aval) : abool :=
  match v, w with
  | FS f1, FS f2 => Just (Float32.cmp c f1 f2)
  | _, _ => Btop
  end.

Lemma cmpfs_is_bool :
  forall c v w, is_bool (Val.cmpfs_bool c v w).
Proof.
  unfold Val.cmpfs_bool.
  repeat intro ; simpl.
  generalize ((Values.Val.cmpfs_bool c (eSexpr a u v) (eSexpr a u w))).
  intros.
  destruct o ; simpl.
  destruct b;
    try (exists Int.zero ; intuition constructor);
    try (exists Int.one ; intuition constructor).
  exists Int.zero ; intuition.
Qed.


Lemma cmpfs_bool_sound:
  forall c v w x y, evmatch v x -> evmatch w y -> ecmatch (Val.cmpfs_bool c v w) (cmpfs_bool c x y).
Proof.
  intros.
  generalize (cmpfs_is_bool c v w).
  inv H; try constructor; inv H0; try constructor;
  unfold Val.cmpfs_bool in * ; auto.
  rew_cst H1.
  rew_cst H.
  repeat intro; simpl.
  apply eSval_bool.
Qed.


Definition maskzero (x: aval) (mask: int) : abool :=
  match x with
  | I i => Just (Int.eq (Int.and i mask) Int.zero)
  | Uns p n => if Int.eq (Int.zero_ext n mask) Int.zero then Maybe true else Btop
  | _ => Btop
  end.

Lemma is_bool_of_optbool :
  forall v,
  exists i : int,
     Values.Val.lessdef
       (Val.of_optbool v) (Vint i) /\ (i = Int.zero \/ i = Int.one).
Proof.
  intros.
  destruct v; simpl ; try destruct b ;
  try (exists Int.zero ; intuition constructor);
  try (exists Int.one ; intuition constructor).
Qed.

Lemma maskzero_is_bool : forall v m,
   is_bool (Val.maskzero_bool v m).
Proof.
  intros.
  repeat intro.
  unfold Val.maskzero_bool.
  apply is_bool_of_optbool.
Qed.

  
Lemma maskzero_sound:
  forall mask v x,
  evmatch v x ->
  ecmatch (Val.maskzero_bool v mask) (maskzero x mask).
Proof.
  intros.
  assert (MSK := maskzero_is_bool v mask).
  unfold Val.maskzero_bool in *.
  inv H; simpl; auto with va; try constructor; auto.
  -
    unfold Val.maskzero_bool.
    rew_cst H0.
    repeat intro.
    simpl.
    apply eSval_bool.
  -
    predSpec Int.eq Int.eq_spec (Int.zero_ext n mask) Int.zero; auto with va;
    constructor.
    repeat intro.
    unfold is_unsigned in H1.
    destruct (H1 a u); intuition.
    rewrite is_uns_zero_ext in H5.
    inversion H4 ; clear H4; subst v0 ; simpl ; try constructor.
    rewrite H7 ; simpl.
    predSpec Int.eq Int.eq_spec (Int.and x mask) Int.zero; auto with va.
    exfalso.
    apply H3.
    rewrite Int.zero_ext_and in * by auto.
    rewrite <- H5.
    rewrite Int.and_assoc.
    rewrite Int.and_commut in H.
    rewrite H.
    rewrite Int.and_zero; auto.
    rewrite <- H6.
    simpl. constructor.
    auto.
Qed.

Definition of_optbool (p : aptr) (ab: abool) : aval :=
  match ab with
  | Just b => I (if b then Int.one else Int.zero)
  | _ => Uns p 1
  end.

Lemma ecmatch_is_bool :
  forall ob ab,
    ecmatch ob ab -> is_bool ob.
Proof.
  intros.
  inv H ; eauto with va.
  rew_cst H0. auto with va.
  rew_cst H0. auto with va.
Qed.
  
Lemma of_optbool_sound:
  forall ob ab p (PMATCH : epmatch ob p), ecmatch ob ab -> evmatch ob (of_optbool p ab).
Proof.
  intros.
  assert (DEFAULT: evmatch ob (Uns p 1)).
  {
    constructor; auto.
    omega.
    repeat intro.
    apply ecmatch_is_bool in H.
    destruct (H a u).
    exists x ; intuition subst.
    unfold is_uns. intros. rewrite Int.bits_zero.
    reflexivity.
    unfold is_uns. intros. rewrite Int.bits_one.
    unfold proj_sumbool.
    destruct (zeq m 0); try omega.
    reflexivity.
  }
  inv H ; simpl ; auto.
  - rew_cst H0.
    constructor.
    destruct b ; repeat intro ; reflexivity.
Qed.

Definition resolve_branch (ab: abool) : option bool :=
  match ab with
  | Just b => Some b
  | Maybe b => Some b
  | _ => None
  end.

Lemma resolve_branch_sound:
  forall e ab b',
    ecmatch e ab ->
    resolve_branch ab = Some b' -> is_wk_constant (val_of_bool b') e.
Proof.
  intros. inv H; simpl in H0; try congruence.
  inv H0 ; auto with va.
  rew_cst H1.
  destruct b' ; constructor.
  inv H0 ; assumption.
Qed.

Normalization at load time

Definition vnormalize (chunk: memory_chunk) (v: aval) :=
  match chunk, v with
  | Mint8signed, v => sign_ext 8 v
  | Mint8unsigned, v => zero_ext 8 v
  | Mint16signed, v => sign_ext 16 v
  | Mint16unsigned, v => zero_ext 16 v
  | Mint32, v => sign_ext 32 v
  | Mint64, L _ => v
  | Mint64, (Ptr p | Uns p _ | Sgn p _) => Ptr (poffset p)
  | Mfloat32, FS f => v
  | Mfloat64, F f => v
  | Many32, (I _ | Uns _ _ | Sgn _ _ | Ptr _ | FS _) => v
  | Many64, _ => v
  | _, v => ntop1 v
  end.

Lemma epmatch_undef_wt_expr :
  forall v p
         (WT : ~ wt_expr v Tint)
         (PTR : epmatch v p),
   epmatch (Eval Vundef) p.
Proof.
  intros.
  inv PTR; try constructor ; depends_prf.
  -
  econstructor ; eauto.
  repeat intro.
  unfold is_pointer,same_eval in H0.
  specialize (H0 cm em).
  simpl in H0.
  symmetry in H0.
  apply expr_nu_type with (t:= Tint) in H0; simpl ; auto; try congruence.
  -
  econstructor ; eauto.
  repeat intro.
  specialize (H0 cm em).
  simpl in H0.
  symmetry in H0.
  apply expr_nu_type with (t:= Tint) in H0; simpl ; auto; try congruence.
Qed.

Lemma vnormalize_sound:
  forall chunk v x (VMATCH : evmatch v x),
    evmatch (Val.load_result chunk v) (vnormalize chunk x).
Proof.
  intros.
  generalize sign_ext_sound.
  generalize zero_ext_sound.
  assert (DEFAULT: evmatch (Val.load_result chunk v) (ntop1 x)).
  {
    unfold Val.load_result.
    destruct chunk ;
      try (apply evmatch_ntop1 ; auto ; repeat constructor ; auto;fail).
    destruct (wt_expr_dec v Tint) ; auto.
    apply evmatch_ntop1 with (T:= fun x => x); repeat constructor; auto.
    destruct (wt_expr_dec v Tsingle) ; auto.
    apply evmatch_ntop1 with (T:= fun x => x); repeat constructor; auto.
    apply evmatch_ntop1 with (T:= fun v => (Eval Vundef)) (v:=v); repeat constructor; auto.
    apply evmatch_ntop1 with (T:= fun x => x); repeat constructor; auto.
  }
  intros.
  case_eq chunk; simpl ; intros ; eauto.
  -
    apply H0 ; auto. omega.
  - apply H0 ; auto. omega.
  - apply H0 ; auto ; omega.
  -
    subst.
    destruct x ; try apply DEFAULT.
    constructor.
    inv VMATCH.
    rew_cst H3.
    repeat intro.
    simpl.
    rewrite Int64.sign_ext_above.
    reflexivity.
    compute. congruence.
  -
    subst.
    destruct x ; try apply DEFAULT.
    constructor.
    inv VMATCH.
    rew_cst H3.
    repeat intro.
    reflexivity.
  -
    subst.
    destruct x ; try apply DEFAULT.
    constructor.
    inv VMATCH.
    rew_cst H3.
    repeat intro.
    reflexivity.
  -
    subst.
    simpl in DEFAULT.
    destruct (wt_expr_dec v Tint).
    +
    destruct x ; try apply DEFAULT ; auto.
    +
      destruct (wt_expr_dec v Tsingle).
      destruct x ; try apply DEFAULT ; auto.
      {
      destruct x ; try apply DEFAULT ; auto.
      -
      inv VMATCH.
      unfold is_constant in H3.
      constructor.
      repeat intro.
      simpl.
      specialize (H3 cm em).
      simpl in H3.
      symmetry in H3.
      apply expr_nu_type with (t:= Tint) in H3; simpl ; auto; try congruence.
      -
      inv VMATCH.
      constructor; auto.
      repeat intro.
      unfold is_unsigned in H5.
      destruct (H5 a u).
      destruct H1.
      simpl. exists x ; simpl ; repeat constructor ; auto.
      eapply epmatch_undef_wt_expr ; eauto.
      -
      inv VMATCH.
      constructor; auto.
      repeat intro.
      destruct (H5 a u).
      destruct H1.
      simpl. exists x ; simpl ; repeat constructor ; auto.
      eapply epmatch_undef_wt_expr ; eauto.
      -
        inv VMATCH.
        constructor.
        repeat intro.
        simpl.
        specialize (H3 cm em).
        simpl in H3.
        symmetry in H3.
        apply expr_nu_type with (t:= Tsingle) in H3; simpl ; auto; try congruence.
      -
        inv VMATCH.
        constructor.
        eapply epmatch_undef_wt_expr ; eauto.
      }

Qed.


Lemma vnormalize_cast_ptr:
  forall chunk m b ofs v p,
  Mem.load chunk m b ofs = Some v ->
  epmatch v p ->
  evmatch v (vnormalize chunk (Ptr p)).
Proof.
  intros.
  exploit Mem.load_cast; eauto.
  exploit Mem.load_type; eauto.
  intros.
  assert (MATCH : evmatch v (Ptr p)).
   constructor ; auto.
   clear H0.
  destruct chunk; unfold vnormalize;
  try rewrite H2; try apply sign_ext_sound ;
  try apply zero_ext_sound ; auto ; try omega.
  -
  inv MATCH ; constructor. apply poffset_sound; auto.
  -
  apply evmatch_ntop1 with (T :=fun x => x);
  repeat constructor; auto. inv MATCH ; auto.
  -
  inv MATCH.
  apply evmatch_ntop1 with (T :=fun x => x);
    repeat constructor; auto.
Qed.

Lemma vnormalize_cast:
  forall chunk m b ofs v p,
  Mem.load chunk m b ofs = Some v ->
  evmatch v p ->
  evmatch v (vnormalize chunk p).
Proof.
  intros.
  exploit Mem.load_cast; eauto.
  exploit Mem.load_type; eauto.
  assert (PTR := vnormalize_cast_ptr chunk m b ofs v).
  assert (TOP : evmatch v (ntop1 p)).
   apply evmatch_ntop1 with (T:= fun x => x).
   constructor. auto.
  intros.
  destruct chunk; unfold vnormalize;
  try rewrite H2; try apply sign_ext_sound ;
  try apply zero_ext_sound ; auto ; try omega.
  -
    destruct p ; try apply TOP.
    constructor.
    inv H0; auto.
  -
    destruct p ; try apply TOP.
    constructor.
    inv H0; auto.
  -
    destruct p ; try apply TOP.
    constructor.
    inv H0; auto.
  -
    destruct p ; try apply TOP; auto.
Qed.


Remark poffset_monotone:
  forall p q, epge p q -> epge (poffset p) (poffset q).
Proof.

  intros.
  destruct p ; destruct q ; simpl in * ; tauto.
Qed.


Lemma epge_poffset_Pcst' :
  forall p,
    epge p Pcst ->
    epge (poffset p) Pcst.
Proof.
  destruct p ; simpl ; auto.
Qed.

Hint Resolve epge_poffset_Pcst epge_poffset_Pcst' poffset_monotone : va.
Hint Resolve epge_refl : va.
Hint Resolve evge_refl : va.

Lemma sgn_mono :
  forall p q n n',
    n >= n' ->
    epge p q ->
    evge (sgn p n) (sgn q n').
Proof.
  intros.
  unfold sgn.
  intros.
  repeat case_match ; intros ; try constructor ; auto with va ; omega.
Qed.

Lemma uns_mono :
  forall p q n n',
    n >= n' ->
    epge p q ->
    evge (uns p n) (uns q n').
Proof.
  unfold uns.
  intros.
  repeat case_match ; try constructor ; auto ; intros ; try omega.
Qed.


Hint Resolve sgn_mono uns_mono : va.

Lemma is_bot_sgn : forall n,
     is_bot (sgn Pbot n).
Proof.
   unfold sgn.
   intros.
   repeat case_match ; reflexivity.
Qed .


Lemma sign_ext_mono :
  forall x y n,
    n > 0 ->
    evge x y ->
    evge (sign_ext n x) (sign_ext n y).
Proof with
(eauto with va).
  intros. unfold sign_ext.
  inv H0 ; simpl; try (constructor ; auto ; fail).
  -
    destruct (zlt n Int.zwordsize).
    destruct (zlt n0 n).
  +
    constructor; auto.
    apply is_sign_ext_uns...
    eapply epge_poffset_Pcst'; eauto.
  +
    eapply evge_trans with (v := Sgn (poffset p) n).
    apply evge_sgn_sgn'.
    constructor ; auto.
    omega.
    apply is_sign_ext_sgn ; auto with va.
    eapply epge_poffset_Pcst'; eauto.
  +
    constructor ; auto with va.
    repeat intro.
    rewrite Int.sign_ext_above ; auto.
  -
    destruct (zlt n Int.zwordsize).
    eapply evge_trans with (v := Sgn (provenance (Ptr p)) n).
    apply evge_sgn_sgn'.
    constructor ; auto.
    omega.
    apply is_sign_ext_sgn ; auto with va.
    eapply epge_poffset_Pcst'; eauto.
    constructor; auto.
  -
    destruct (zlt n Int.zwordsize).
    apply sgn_mono. omega.
    unfold provenance ; simpl...
    unfold sgn ; repeat case_match ; try constructor...
  -
    destruct (zlt n Int.zwordsize).
    apply sgn_mono; try omega. unfold provenance ; simpl...
    unfold sgn ; repeat case_match ; try constructor...
  -
    destruct (zlt n Int.zwordsize).
    apply sgn_mono ; try omega. unfold provenance ; simpl...
    unfold sgn ; repeat case_match ; try constructor...
  -
    unfold sgn.
    repeat case_match ; try constructor ; intros; try xomega...
  -
    destruct (zlt n Int.zwordsize).
    + unfold sgn.
    repeat case_match ; try constructor...
    apply is_sign_ext_sgn ; try omega.
    assert (n0 <= 8 \/ n <= 8) by (zify ; omega).
    destruct H4 ; auto.
    left.
    eapply is_sgn_mon; eauto.
    apply is_sign_ext_sgn ; try omega.
    assert (n0 <= 16 \/ n <= 16) by (zify ; omega).
    destruct H5 ; auto.
    left.
    eapply is_sgn_mon; eauto.
    +
      constructor; auto.
      apply is_sign_ext_sgn ; auto with va.
  -
    destruct (zlt n Int.zwordsize); auto with va.
    constructor; auto.
  -
    destruct (zlt n Int.zwordsize) ; try (constructor; auto with va;fail).
    destruct (zlt n2 n).
    +
      eapply evge_trans with (v := Sgn (poffset p1) (Z.min n1 n)).
      apply evge_sgn_sgn'.
      constructor; auto with va.
    +
      apply sgn_mono...
  -
    destruct (zlt n Int.zwordsize) ; try (constructor ; auto with va; fail).
    destruct (zlt n1 n).
    +
      eapply evge_trans with (v := Sgn (poffset p1) n).
      apply evge_sgn_sgn'.
      constructor; auto with va.
    +
      apply sgn_mono...
      unfold provenance.
      simpl...
  -
    destruct (zlt n Int.zwordsize) ; try (constructor ; auto with va; fail).
    apply sgn_mono...
    unfold provenance; simpl...
  -
    destruct (zlt n Int.zwordsize) ; try (constructor ; auto with va; fail).
    apply sgn_mono...
    unfold provenance; simpl...
  -
    destruct (zlt n Int.zwordsize) ; try (constructor ; auto with va; fail).
    destruct y ; try apply sgn_mono; unfold provenance; simpl...
    apply evge_sgn_i'...
    apply is_sign_ext_sgn ; try omega.
    intuition.
    constructor.
    destruct (zlt n0 n)...
    apply evge_trans with (v:= Sgn Ptop n).
    apply evge_sgn_sgn'.
    constructor; auto...
    constructor.
    apply sgn_mono...
    constructor.
  - unfold is_bot in H1.
    unfold aptr_of_aval in H1.
    destruct y ; subst ; try congruence.
    constructor. repeat case_match ; try reflexivity. simpl.
    intros. apply is_bot_sgn.
    constructor.
    repeat case_match ; try reflexivity. simpl.
    intros. apply is_bot_sgn.
    constructor.
    repeat case_match ; try reflexivity. simpl.
    intros. apply is_bot_sgn.
Qed.
    Require Import Psatz.


Lemma is_bot_uns : forall n,
     is_bot (uns Pbot n).
Proof.
   unfold uns.
   intros.
   repeat case_match ; reflexivity.
Qed .

Lemma zero_ext_bot :
      forall n x, is_bot x ->
      is_bot (zero_ext n x).
Proof.
 intros.
 unfold is_bot, aptr_of_aval in H.
 destruct x ; try congruence ; try reflexivity;
 unfold zero_ext.
 - subst.
  case_eq (zlt n Int.zwordsize || not_int (Uns Pbot n0)).
  simpl. intros.
  apply is_bot_uns.
  simpl. reflexivity.
 - subst.
   repeat case_match; simpl; try reflexivity.
   intros.
   apply is_bot_uns.
 - subst.
   repeat case_match; simpl; try reflexivity.
   intros.
   apply is_bot_uns.
Qed.

Lemma is_bot_bool_true_iff : forall x, is_bot_bool x = true <-> is_bot x.
Proof.
  unfold is_bot_bool, is_bot.
  intro. destruct (aptr_of_aval x) ; simpl ; intuition congruence.
Qed.

Lemma is_bot_bool_false_iff : forall x, is_bot_bool x = false <-> ~ is_bot x.
Proof.
  unfold is_bot_bool, is_bot.
  intro. destruct (aptr_of_aval x) ; simpl ; intuition congruence.
Qed.


Lemma zero_ext_mono :
  forall x y n,
    n > 0 ->
    evge x y ->
    evge (zero_ext n x) (zero_ext n y).
Proof with
(eauto with va).
  intros.
  case_eq (is_bot_bool y).
  * intros.
    apply is_bot_bool_true_iff in H1.
    apply zero_ext_bot with (n:= n) in H1.
    apply evge_trans with (v:= Ptr Pbot).
    constructor. reflexivity.
    constructor. auto.
  *
  intro.
  apply is_bot_bool_false_iff in H1.
  rename H1 into NBOT.
  unfold zero_ext.
  case_eq (zlt n Int.zwordsize || not_int x) ;
    case_eq (zlt n Int.zwordsize || not_int y).
  intros.
  rewrite orb_true_iff in H1.
  rewrite orb_true_iff in H2.
  inv H0 ; simpl ; try (constructor ; eauto with va ; fail).
  -
    apply evge_uns_i'...
    apply is_zero_ext_uns.
    zify. intuition (subst ; try omega); intuition auto.
  -
    apply evge_uns_i'...
    apply is_zero_ext_uns...
    unfold provenance ; simpl...
  -
    apply uns_mono ; unfold provenance ; simpl...
  -
    apply uns_mono ; unfold provenance ; simpl...
  -
    apply uns_mono ; unfold provenance ; simpl...
  -
    apply uns_mono ; unfold provenance ; simpl...
  -
    apply evge_uns_i'...
    simpl in *.
    apply is_zero_ext_uns...
    unfold provenance ; simpl...
  -
    eapply uns_mono; try omega.
    unfold provenance ; simpl...
  -
    eapply uns_mono; try lia.
    unfold provenance ; simpl...
  -
    eapply uns_mono; try lia.
    unfold provenance ; simpl...
  -
    eapply <