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}.

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.

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.


Import ExprEval.


Instance EquivExpr : Equivalence same_eval.

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.


Add Parametric Morphism : is_constant with signature ((@eq val) ==> same_eval ==> iff) as is_constant_same_eval_morph.

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.

Add Parametric Morphism (o : unop_t) (t : styp) : (Eunop o t) with signature same_eval ==> same_eval as unop_same_eval.

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).

Add Parametric Morphism : is_wk_constant with signature ((@eq val) ==> same_eval ==> iff) as is_wk_constant_same_eval_morph.


Add Parametric Morphism : is_bool with signature (same_eval ==> iff) as is_bool_same_eval_morph.
  
  
Add Parametric Morphism : ecmatch with signature (same_eval ==> @eq abool ==> iff) as cmatch_morph.

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).

Lemma is_bool_true :
   is_bool (Eval Vtrue).

Lemma is_bool_false :
   is_bool (Eval Vfalse).

Lemma is_bool_val_of_bool :
  forall b,
    is_bool (Eval (val_of_bool b)).

Lemma is_wk_constant_is_bool :
  forall b e,
    is_wk_constant (val_of_bool b) e ->
   is_bool e.


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.

Lemma club_ge_l : forall x y,
                  cge (club x y) x.


Lemma ecmatch_lub_l:
  forall ob x y, ecmatch ob x -> ecmatch ob (club x y).

Lemma club_sym : forall x y, club x y = club y x.


Lemma ecmatch_lub_r:
  forall ob x y, ecmatch ob y -> ecmatch ob (club x y).

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).

Lemma ecnot_sound:
  forall ob x, ecmatch ob x -> ecmatch (Val.notbool ob) (cnot x).

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}.

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.

Lemma pmatch_ge:
  forall b ofs p q, pge p q -> pmatch b ofs q -> pmatch b ofs p.


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.
    

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.


Lemma is_constant_depends :
  forall v e, is_constant v e -> depends_on_blocks (deps_of_val v) e.

Lemma is_pointer_depends :
  forall b o e, is_pointer b o e -> depends_on_blocks (singleton b) e.

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.

Lemma depends_on_blocks_appears :
  forall (S: block -> Prop) e,
  (forall b, (block_appears e b -> S b)) ->
  depends_on_blocks S e.
    
Add Parametric Morphism : epmatch with signature same_eval ==> @eq aptr ==> iff as epmatch_same_eval.



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).

Lemma depends_unop :
  forall (S: block -> Prop) o t e1,
    depends_on_blocks S e1 ->
    depends_on_blocks S (Eunop o t e1).



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).



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.

Lemma epmatch_bot_def :
  forall v p,
    epmatch v Pbot ->
    epmatch v p.

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.
  
Lemma epmatch_ge:
  forall e p q, epge p q -> epmatch e q -> epmatch e p.

Lemma epmatch_top': forall e p, epmatch e p -> epmatch e Ptop.

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.



Lemma epge_lub_l:
  forall p q, epge (eplub p q) p.

Lemma epge_lub_r:
  forall p q, epge (eplub p q) q.

Lemma epmatch_lub_l:
  forall e p q, epmatch e p -> epmatch e (eplub p q).

Lemma epmatch_lub_r:
  forall e p q, epmatch e q -> epmatch e (eplub p q).


Lemma eplub_least:
  forall r p q, epge r p -> epge r q -> epge r (eplub p q).

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.

Lemma pincl_ge_2: forall p q, epge p q -> epincl q p = true.

Lemma epincl_sound:
  forall e p q,
  epincl p q = true -> epmatch e p -> epmatch e q.

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.


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.

Lemma epincl_not_ge: forall p q, epincl p q = false -> ~ epge q p.

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))).
  
Lemma epadd_sound:
  forall e p delta,
  epmatch e p ->
  epmatch (Val.add e (Eval (Vint delta))) (padd p delta).

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).

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))).

Lemma epsub_sound:
  forall e p delta,
  epmatch e p ->
  epmatch (Val.sub e (Eval (Vint delta))) (psub p delta).


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).

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.

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).

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).

Lemma cmp_different_blocks_sound:
  forall c, cmatch (Val.cmp_different_blocks c) (cmp_different_blocks c).

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.
  
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.

Lemma is_bool_cmpu_bool : forall c e1 e2,
                    is_bool (Val.cmpu_bool c e1 e2).


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).

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.

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 *)
.


Definition Vtop := Ptr Ptop.


Definition eq_aval: forall (v1 v2: aval), {v1=v2} + {v1<>v2}.

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.

Add Parametric Morphism (n:Z) : (is_signed n) with signature (same_eval ==> iff) as is_signed_same_eval_morph.




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.




Hint Resolve epmatch_top_def : va.

Lemma evmatch_top: forall v x, evmatch v x -> evmatch v Vtop.

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


Lemma is_uns_mon: forall n1 n2 i, is_uns n1 i -> n1 <= n2 -> is_uns n2 i.

Lemma is_sgn_mon: forall n1 n2 i, is_sgn n1 i -> n1 <= n2 -> is_sgn n2 i.

Lemma is_uns_sgn: forall n1 n2 i, is_uns n1 i -> n1 < n2 -> is_sgn n2 i.

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.

Lemma is_sgn_ssize:
  forall i, is_sgn (ssize i) i.

Lemma is_uns_zero_ext:
  forall n i, is_uns n i <-> Int.zero_ext n i = i.

Lemma is_sgn_sign_ext:
  forall n i, 0 < n -> (is_sgn n i <-> Int.sign_ext n i = i).

Lemma is_zero_ext_uns:
  forall i n m,
  is_uns m i \/ n <= m -> is_uns m (Int.zero_ext n i).

Lemma is_zero_ext_sgn:
  forall i n m,
  n < m ->
  is_sgn m (Int.zero_ext n i).

Lemma is_sign_ext_uns:
  forall i n m,
  0 <= m < n ->
  is_uns m i ->
  is_uns m (Int.sign_ext n i).
  
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).

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.



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)).



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.

Hint Resolve evge_top : va.

Lemma epge_top : forall p, epge p Ptop -> p = Ptop.

Lemma epge_bot : forall p, epge Pbot p -> p = Pbot.



Lemma evge_trans: forall u v, evge u v -> forall w, evge v w -> evge u w.


Lemma is_uns_unsigned :
  forall n i,
    is_uns n i ->
    is_unsigned n (Eval (Vint i)).

Lemma is_sgn_signed :
  forall n i,
    is_sgn n i ->
    is_signed n (Eval (Vint i)).

Lemma is_constant_unsigned :
  forall n i v,
    is_uns n i ->
    is_constant (Vint i) v ->
    is_unsigned n v.

Lemma is_sgn_unsigned :
  forall n i,
    is_sgn n i ->
    is_signed n (Eval (Vint i)).

Lemma is_constant_signed :
  forall n i v,
    is_sgn n i ->
    is_constant (Vint i) v ->
    is_signed n v.

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.

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)).

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)).

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)).

Lemma is_unsigned_mon :
  forall n1 n2 v,
    n1 >= n2 ->
    is_unsigned n2 v ->
    is_unsigned n1 v.

Lemma is_signed_mon :
  forall n1 n2 v,
    n1 >= n2 ->
    is_signed n2 v ->
    is_signed n1 v.

Lemma is_unsigned_signed_mon :
  forall n1 n2 i,
    n1 < n2 ->
    is_unsigned n1 i ->
    is_signed n2 i.

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.


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.



Lemma epge_refl : forall p, epge p p.

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.

Lemma epge_poffset : forall p, epge (poffset p) p.

Hint Resolve epge_poffset epge_poffset_Pcst : va.

Lemma evge_uns_uns': forall p n, evge (uns p n) (Uns p n).

Lemma evge_uns_i': forall p n i, 0 <= n -> is_uns n i -> epge p Pcst -> evge (uns p n) (I i).


Lemma evge_sgn_sgn': forall p n, evge (sgn p n) (Sgn p n).

Lemma evge_sgn_i': forall p n i, 0 < n -> is_sgn n i -> epge p Pcst -> evge (sgn p n) (I i).


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

Lemma usize_pos: forall n, 0 <= usize n.

Lemma ssize_pos: forall n, 0 < ssize n.
Definition Vbot := Ptr Pbot.

Hint Constructors evmatch : va.

Lemma eplub_bot :
      forall p q, eplub p q = Pbot -> p = Pbot /\ q = Pbot.

Lemma evge_lub_l:
  forall x y, evge (evlub x y) x.


Lemma evmatch_lub_l:
  forall v x y, evmatch v x -> evmatch v (evlub x y).

Lemma evmatch_lub_r:
  forall v x y, evmatch v y -> evmatch v (evlub x y).


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.

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

Lemma evincl_ge: forall v w, vincl v w = true -> evge w v.


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)).

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)).

Lemma vmatch_ptr_stk:
  forall v ofs sp,
  evmatch v (Ptr(Stk ofs)) ->
  bc sp = BCstack ->
  Val.lessdef v (Eval (Vptr sp ofs)).

Lemma is_pointer_eval :
  forall b ofs b' ofs',
    is_pointer b ofs (Eval (Vptr b' ofs')) ->
    b = b' /\ ofs = ofs'.


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.


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).



Hint Resolve aptr_of_aval : va.



Lemma epmatch_cst_Pcst :
  forall v,
    val_no_ptr v = true ->
    epmatch (Eval v) Pcst.

Lemma epmatch_unop_provenance :
  forall o s v x,
    epmatch v x ->
    epmatch (Eunop o s v) (poffset x).
      

Lemma evmatch_unop_ntop1 :
  forall o s v x,
    evmatch v x ->
    evmatch (Eunop o s v) (ntop1 x).

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)).

Lemma evmatch_ntop1 :
  forall T v x,
    is_unop_trans T ->
    (evmatch v x) ->
    evmatch (T v) (ntop1 x).


Lemma eplub_poffset :
  forall x y,
    eplub (poffset x) (poffset y) =
    poffset (eplub x y).
  
Lemma poffset_idem :
  forall x, poffset (poffset x) = poffset x.

Lemma eplub_idem : forall x, eplub x x = x.


Lemma epmatch_poffset :
  forall v p T
         (HT : is_unop_trans T)
         (HM : epmatch v p),
    epmatch (T v) (poffset p).

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).

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).


Lemma poffset_Pcst : forall p, p <> Pbot -> eplub (poffset p) Pcst = poffset p.

Lemma pointer_bot : forall p, p = Pbot \/ p <> Pbot.

Lemma epmatch_eplub_poffset :
  forall T v w x y
         (HT : is_binop_trans T),
    (epmatch v x) ->
    (epmatch w y) ->
    epmatch (T v w) (eplub (poffset x) (poffset y)).

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).


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).


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).

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).

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).

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).

Definition lift_aptr (ap : aptr -> aptr -> aval) (v w : aval) : aptr :=
  aptr_of_aval (ap (aptr_of_aval v) (aptr_of_aval w)).


Definition binop_gen (C : int -> int -> int)
           (u : Z -> Z -> Z)
           (s : Z -> Z -> Z)
           (ap : aptr -> aptr -> aval)
           (v w: aval) :=
  match v , w with
  | I i , I j => I (C i j)
  | I i , Uns p n => uns (lift_aptr ap v w) (u (usize i) n)
  | Uns p n , I i => uns (lift_aptr ap v w) (u n (usize i))
  | Uns p n , Uns p' n' => uns (lift_aptr ap v w) (u n n')
  | Sgn p n , Sgn p' n' => sgn (lift_aptr ap v w) (s n n')
  | _ , _ => ap (aptr_of_aval v) (aptr_of_aval w)
  end.


Definition less_def_eval (S : expr_sym -> expr_sym -> expr_sym) (C : int -> int -> int) :=
  forall v w (i1 i2 : int) (a : mem) (u : block -> int -> byte),
    Values.Val.lessdef (eSexpr a u v) (Vint i1) ->
    Values.Val.lessdef (eSexpr a u w) (Vint i2) ->
    Values.Val.lessdef (eSexpr a u (S v w))
                       (Vint (C i1 i2)).

Definition same_def_eval (S : expr_sym -> expr_sym -> expr_sym) (C : int -> int -> int) :=
  forall v w (i1 i2 : int) ,
    same_eval v (Eval (Vint i1)) ->
    same_eval w (Eval (Vint i2)) ->
    same_eval (S v w) (Eval (Vint (C i1 i2))).

Lemma evmatch_uns':
  forall p e n, is_unsigned (Zmax 0 n) e -> epmatch e p -> evmatch e (uns p n).

Lemma evmatch_uns:
  forall p e n, is_unsigned n e -> epmatch e p -> evmatch e (uns p n).

Lemma evmatch_sgn':
  forall p e n, is_signed (Zmax 1 n) e -> epmatch e p -> evmatch e (sgn p n).

Lemma evmatch_sgn:
  forall p e n, is_signed n e -> epmatch e p -> evmatch e (sgn p n).

Lemma is_unsigned_bin :
  forall n1 v1 n2 v2 A S (C: int -> int -> int)
         (SE : less_def_eval S C)
         (AC : forall n1 n2 i1 i2, is_uns n1 i1 ->
                             is_uns n2 i2 ->
                             is_uns (A n1 n2) (C i1 i2)),
    is_unsigned n1 v1 ->
    is_unsigned n2 v2 ->
    is_unsigned (A n1 n2) (S v1 v2).

Lemma is_signed_bin :
  forall n1 v1 n2 v2 A S (C: int -> int -> int)
         (SE : less_def_eval S C)
         (AC : forall n1 n2 i1 i2, is_sgn n1 i1 ->
                             is_sgn n2 i2 ->
                             is_sgn (A n1 n2) (C i1 i2)),
    is_signed n1 v1 ->
    is_signed n2 v2 ->
    is_signed (A n1 n2) (S v1 v2).


Definition eval_sym (S : expr_sym -> expr_sym -> expr_sym) (C : int -> int -> int) :=
  forall x y cm em,
    Vint (C x y) = eSexpr cm em (S (Eval (Vint x)) (Eval (Vint y))).

Lemma eval_symb_less_def_eval : forall S C,
    is_binop_trans S ->
    eval_sym S C ->
    less_def_eval S C.


Lemma evmatch_epge :
  forall v x,
    evmatch v x ->
    epge (poffset (aptr_of_aval x))
         (eplub (poffset (aptr_of_aval x)) (poffset Pcst)).
    
Lemma is_binop_trans_same_eval : forall S ,
    is_binop_trans S ->
    forall x x' y y',
      same_eval x x' -> same_eval y y' ->
      same_eval (S x y) (S x' y').

Lemma binop_sound :
  forall v w x y S C u s ap
         (BINOP : is_binop_trans S)
         (EQ : eval_sym S C)
         (UNS :
            forall (n1 n2 : Z) (i1 i2 : int),
              is_uns n1 i1 -> is_uns n2 i2 -> is_uns (u n1 n2) (C i1 i2))
         (SGN :
            forall (n1 n2 : Z) (i1 i2 : int),
              is_sgn n1 i1 -> is_sgn n2 i2 -> is_sgn (s n1 n2) (C i1 i2))
         (PTR : forall v p w q, epmatch v p -> epmatch w q -> evmatch (S v w) (ap p q))
  ,
    evmatch v x -> evmatch w y ->
    evmatch (S v w) (binop_gen C u s ap x y).

    

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 inv_lessdef : forall x y, Values.Val.lessdef x y ->
                                x = Vundef \/ x = y.
  





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).


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.
  

Lemma is_constant_int_ptr :
  forall i b o e ,
    is_constant (Vint i) e ->
    is_constant (Vptr b o) e ->
False.

Lemma is_constant_epmatch_epge :
  forall i e x,
    is_constant (Vint i) e -> epmatch e x ->
   epge x Pcst.



Lemma is_constant_epmatch_Pcst :
  forall i e,
    is_constant (Vint i) e ->
   epmatch e Pcst.

Lemma is_constant_any_epmatch_Pcst :
  forall i e,
    val_no_ptr i = true ->
    is_constant i e ->
   epmatch e Pcst.

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.

Lemma shru_sound:
  forall v w x y, evmatch v x -> evmatch w y -> evmatch (Val.shru v w) (shru x y).

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).

Definition and_cst (i:int) (p: aptr) (n : Z) :=
  if zle n Int.zwordsize
  then
    let msk := Int.repr ((two_p n) - 1) in
    let p' := if Int.eq (Int.and i msk) msk
               then p else poffset p in
    uns p' (Z.min (usize i) n)
  else ntop1 (Ptr p).


Definition neq_offset_ptr (p p' : aptr) : aptr :=
  if eq_aptr p p' then p
  else eplub (poffset p) (poffset p').

Definition and (v w: aval) :=
  match v, w with
  | I i1, I i2 => I (Int.and i1 i2)
  | I i, Uns p n | Uns p n, I i => and_cst i p n
  | Uns p1 n1, Uns p2 n2 => uns (neq_offset_ptr p1 p2) (Z.min n1 n2)
  | Sgn p1 n1, Sgn p2 n2 => sgn (neq_offset_ptr p1 p2) (Z.max n1 n2)
  | _, _ => Ptr (neq_offset_ptr (aptr_of_aval v) (aptr_of_aval w))
  end.

Add Parametric Morphism : Val.and with signature (same_eval ==> same_eval ==> same_eval) as and_morph.

Lemma is_constant_is_unsigned : forall i v,
    is_constant (Vint i) v ->
    is_unsigned (usize i) v.


Lemma less_def_eval_and : less_def_eval Val.and Int.and.
    
Hint Resolve less_def_eval_and.

Lemma UNS_l: forall i j n, is_uns n i -> is_uns n (Int.and i j).

Lemma UNS_r: forall i j n, is_uns n i -> is_uns n (Int.and j i).
  intros. rewrite Int.and_commut.
  eapply UNS_l ; eauto.
Qed.