Module ConstpropOpproof

Require Import Coqlib.
Require Import Compopts.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Globalenvs.
Require Import Events.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import Values_symbolic.
Require Import Values_symbolictype.
Require Import ValueDomain.
Require Import ConstpropOp.
Require Import Setoid.
Require Import Psatz.




Add Parametric Morphism : Val.sub with signature same_eval ==> same_eval ==> same_eval as sub_lessdef.

Add Parametric Morphism : Val.and with signature same_eval ==> same_eval ==> same_eval as and_lessdef.

Add Parametric Morphism : Val.modu with signature same_eval ==> same_eval ==> same_eval as modu_lessdef.

Add Parametric Morphism : Val.or with signature same_eval ==> same_eval ==> same_eval as or_lessdef.

Add Parametric Morphism : Val.xor with signature same_eval ==> same_eval ==> same_eval as xor_lessdef.

Add Parametric Morphism : Val.divs with signature same_eval ==> same_eval ==> same_eval as divs_lessdef.

Add Parametric Morphism : Val.divu with signature same_eval ==> same_eval ==> same_eval as divu_lessdef.

Add Parametric Morphism : Val.shru with signature same_eval ==> same_eval ==> same_eval as shru_lessdef.


Add Parametric Morphism : Val.shrx with signature same_eval ==> same_eval ==> same_eval as shrx_lessdef.



Lemma val_mul_commut :
  forall x y,
    same_eval (Val.mul x y) (Val.mul y x).


Lemma val_and_commut :
  forall x y,
    same_eval (Val.and x y) (Val.and y x).

Lemma val_or_commut :
  forall x y,
    same_eval (Val.or x y) (Val.or y x).



Section STRENGTH_REDUCTION.

Variable bc: block_classification.
Variable ge: genv.
Hypothesis GENV: genv_match bc ge.
Variable sp: block.
Hypothesis STACK: bc sp = BCstack.
Variable ae: AE.t.
Variable e: regset.
Variable m: mem.
Hypothesis MATCH: ematch bc e ae.

Lemma match_G:
  forall r id ofs,
  AE.get r ae = Ptr(Gl id ofs) -> Val.lessdef e#r (Eval (Genv.symbol_address ge id ofs)).

Lemma match_S:
  forall r ofs,
  AE.get r ae = Ptr(Stk ofs) -> Val.lessdef e#r (Eval (Vptr sp ofs)).

Lemma inj_hd : forall (A : Type) (e:A) l e' l',
    e :: l = e' :: l' -> e = e'.

Lemma inj_tl : forall (A : Type) (e:A) l e' l',
    e :: l = e' :: l' -> l = l'.

Lemma inj_some : forall (A : Type) (x y : A),
    Some x = Some y -> x = y.
  
Ltac InvApproxRegs :=
  match goal with
  | [H : ?A :: nil = ?B :: nil |- _ ] =>
     generalize (inj_hd _ A nil B nil H);
       clear H; intros; InvApproxRegs
    | [ H: ?A :: ?B = ?C :: ?D |- _ ] =>
    generalize (inj_tl _ A B C D H);
      generalize (inj_hd _ A B C D H) ;
      clear H; intros; InvApproxRegs
  | [ H: ?v = AE.get ?r ae |- _ ] =>
        generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs
  | [H : Some ?A = Some ?B |- _ ] => apply inj_some in H ; InvApproxRegs
  | _ => idtac
  end.

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


Lemma swap_cmp_bool : forall c e1 e2,
    same_eval (Val.cmp_bool (swap_comparison c) e1 e2) (Val.cmp_bool c e2 e1).

Add Parametric Morphism (c : comparison) :
  (Val.cmp_bool c) with signature (same_eval ==> same_eval ==> same_eval) as cmp_bool_morph.

Add Parametric Morphism (c : comparison) :
  (Val.cmpu_bool c) with signature (same_eval ==> same_eval ==> same_eval) as cmpu_bool_morph.

Existing Instance Op.EquiOptSameEval.

Lemma shift_symbol_address' :
  forall id ofs F e
  ,
    
    evmatch bc e (Ptr (Gl id ofs)) ->
    exists b, Genv.symbol_address' ge id (F ofs) = Some (Eval (Vptr b (F ofs)))
              /\ bc b = BCglob id.

Ltac get_shift_symbol_match :=
  match goal with
  | H : evmatch _ ?E (Ptr (Gl ?id ?ofs)) |-
    context [Genv.symbol_address' _ _ ?F = Some _] => constr:(F,E,H,ofs)
  | H : evmatch _ ?E (Ptr (Gl ?id ?ofs)) |-
     exists res' : expr_sym,
       option_map _
                  (Genv.symbol_address' _ _ ?F) = Some _ /\ _ => constr:(F,E,H,ofs)
  end.


Ltac shift_symbol' :=
    let R := get_shift_symbol_match in
    match R with
      (?F,?E,?H,?ofs) =>
    let xx := fresh in
    set (xx := F) ; pattern ofs in xx ;
    match goal with
    | xx := ?F ofs |- _ =>
      let B := fresh "B" in
      let EQ := fresh "EQ" in
      let BC := fresh "BC" in
      destruct (shift_symbol_address' _ _ F E H) as [B [EQ BC]] ;
        unfold xx ; clear xx ; rewrite EQ;
        inv H ;
        match goal with
        | H1 : epmatch _ E _ |- _ => inv H1
        end
    end
  end.


Lemma vmatch_ptr_stk :
  forall v ofs b,
         bc b = BCstack ->
         evmatch bc v (Ptr (Stk ofs)) ->
         is_pointer b ofs v.
  

Ltac SimplVM :=
  match goal with
  | [ H: evmatch _ ?v (I ?n) |- _ ] =>
      let E := fresh in
      assert (E: is_constant (Vint n) v) by (inversion H; auto);
      try rew_cst E ; clear H; SimplVM
  | [ H: evmatch _ ?v (F ?n) |- _ ] =>
      let E := fresh in
      assert (E: v = Vfloat n) by (inversion H; auto);
      rewrite E in *; clear H; SimplVM
  | [ H: evmatch _ ?v (FS ?n) |- _ ] =>
      let E := fresh in
      assert (E: v = Vsingle n) by (inversion H; auto);
      rewrite E in *; clear H; SimplVM
  | [ _: evmatch _ ?v (Ptr(Gl ?id ?ofs)) |- _ ] =>
    shift_symbol'; SimplVM
  | [ H: evmatch _ ?v (Ptr(Stk ?ofs)) |- _ ] =>
      assert (E: is_pointer sp ofs v) by (eapply vmatch_ptr_stk; eauto);
      clear H; SimplVM
  | _ => idtac
  end.

Unset Ltac Debug.

Lemma cond_strength_reduction_correct:
  forall cond args vl,
  vl = map (fun r => AE.get r ae) args ->
  let (cond', args') := cond_strength_reduction cond args vl in
  opt_same_eval (eval_condition cond' e##args') (eval_condition cond e##args).

Lemma is_unop_trans_same_eval :
  forall G x y
        (Unop : is_unop_trans G)
        (Same : same_eval x y),
    same_eval (G x) (G y).
    



Ltac find_trans X V :=
  set (x := X) ; pattern V in x ;
  match goal with
  | x := ?F V |- _ => change x with (F V) ; clear x
  end.


Unset Ltac Debug.

Lemma same_eval_lessdef :
  forall x y, same_eval x y -> Val.lessdef x y.

Add Parametric Morphism : Val.lessdef with signature same_eval ==> same_eval ==> iff as same_eval_lessdef_morph.
    
  Add Parametric Morphism (bo : binop_t) (st st' : styp) :
  (Ebinop bo st st') with signature (same_eval ==> same_eval ==> Val.lessdef) as Ebinop_same_eval_lessdef.

  Add Parametric Morphism :
  (Val.add) with signature (same_eval ==> same_eval ==> same_eval) as add_same_eval.

  Add Parametric Morphism :
  (Val.add) with signature (same_eval ==> same_eval ==> Val.lessdef) as add_lessdef.



Instance lessdefRef : Reflexive Val.lessdef.

Instance lessdefTrans : Transitive Val.lessdef.

Lemma same_eval_add_Eval : forall b o o',
    same_eval (Val.add (Eval (Vptr b o)) (Eval (Vint o'))) (Eval (Vptr b (Int.add o o'))).

Lemma same_eval_mul_Eval : forall o o',
    same_eval (Val.mul (Eval (Vint o)) (Eval (Vint o'))) (Eval (Vint (Int.mul o o'))).



Add Parametric Morphism : Val.mul with signature same_eval ==> same_eval ==> same_eval as mul_same_eval.

Add Parametric Morphism : Val.shl with signature same_eval ==> same_eval ==> same_eval as shl_same_eval.

Add Parametric Morphism : Val.shr with signature same_eval ==> same_eval ==> same_eval as shr_same_eval.

Add Parametric Morphism : Val.shru with signature same_eval ==> same_eval ==> same_eval as shru_same_eval.


Add Parametric Morphism : Val.mul with signature same_eval ==> same_eval ==> Val.lessdef as mul_lessdef.


Add Parametric Morphism : Val.mulf with signature same_eval ==> same_eval ==> same_eval as mulf_same_eval.


Add Parametric Morphism : Val.mulfs with signature same_eval ==> same_eval ==> same_eval as mulfs_same_eval.




Lemma addr_strength_reduction_correct:
  forall addr args vl res,
  vl = map (fun r => AE.get r ae) args ->
  eval_addressing ge (Eval (Vptr sp Int.zero)) addr e##args = Some res ->
  let (addr', args') := addr_strength_reduction addr args vl in
  exists res', eval_addressing ge (Eval (Vptr sp Int.zero)) addr' e##args' = Some res' /\ Val.lessdef res res'.


Inductive opt_lessdef : option expr_sym -> option expr_sym -> Prop :=
| opt_lessdef_None : opt_lessdef None None
| opt_lessdef_Some : forall e e',
    Val.lessdef e e' ->
    opt_lessdef (Some e) (Some e').


Lemma make_cmp_base_correct:
  forall c args vl,
  vl = map (fun r => AE.get r ae) args ->
  let (op', args') := make_cmp_base c args vl in
  opt_lessdef (eval_condition c e##args)
              (eval_operation ge (Eval (Vptr sp Int.zero)) op' e##args').

Lemma vincl_Ptop_one :
  forall r1 ae F G
         (MATCH : ematch bc e ae)
         (INCL : vincl (AE.get r1 ae) (Uns Ptop 1) = true)
         (FEQ : forall a em v,
             (ExprEval.eSexpr a em v = Vundef \/
              ExprEval.eSexpr a em v = Vint Int.zero \/
              ExprEval.eSexpr a em v = Vint Int.one)->
            ExprEval.eSexpr a em (F v) = ExprEval.eSexpr a em (G v)),
    Val.lessdef (F (e # r1)) (G (e # r1)).
  
Lemma make_cmp_correct:
  forall c args vl,
  vl = map (fun r => AE.get r ae) args ->
  let (op', args') := make_cmp c args vl in
  opt_lessdef (eval_condition c e##args) (eval_operation ge (Eval (Vptr sp Int.zero)) op' e##args').

Ltac lessdef_dest x :=
  let a := fresh "a" in
  let u := fresh "u" in
  intros a u ; simpl ; destruct (ExprEval.eSexpr a u x) ; simpl; auto.
  

Lemma make_addimm_correct:
  forall n r c,
    is_constant (Vint n) c ->
    let (op, args) := make_addimm n r in
    opt_lessdef (Some (Val.add e#r c)) (eval_operation ge (Eval (Vptr sp Int.zero)) op e##args).
  
Lemma make_shlimm_correct:
  forall n r1 r2,
    is_constant (Vint n) e#r2 ->
  let (op, args) := make_shlimm n r1 r2 in
  opt_lessdef (Some (Val.shl e#r1 e #r2)) (eval_operation ge (Eval (Vptr sp Int.zero)) op e##args).

Lemma make_shrimm_correct:
  forall n r1 r2,
    is_constant (Vint n) e#r2 ->
  let (op, args) := make_shrimm n r1 r2 in
  opt_lessdef (Some ((Val.shr e#r1 e#r2))) (eval_operation ge (Eval (Vptr sp Int.zero)) op e##args).

Lemma make_shruimm_correct:
  forall n r1 r2,
    is_constant (Vint n) e#r2 ->
  let (op, args) := make_shruimm n r1 r2 in
  opt_lessdef (Some (Val.shru e#r1 e # r2)) (eval_operation ge (Eval (Vptr sp Int.zero)) op e##args).

Lemma val_mul_pow2 :
  forall x y (n logn : int),
    is_constant (Vint n) y ->
    Int.is_power2 n = Some logn ->
    same_eval (Val.mul x y) (Val.shl x (Eval (Vint logn))).


Lemma make_mulimm_correct:
  forall n r1 en,
    is_constant (Vint n) en ->
  let (op, args) := make_mulimm n r1 in
  opt_lessdef (Some (Val.mul e#r1 en)) (eval_operation ge (Eval(Vptr sp Int.zero)) op e##args).

Lemma val_divs_pow2
     : forall x (n logn : int),
       Int.is_power2 n = Some logn ->
       Int.ltu logn (Int.repr 31) = true ->
       same_eval (Val.divs x (Eval (Vint n)))
                 (Val.shrx x (Eval (Vint logn))).
  
Lemma make_divimm_correct:
  forall n r1 r2,
  is_constant (Vint n) e#r2 ->
  let (op, args) := make_divimm n r1 r2 in
  opt_lessdef (Some (Val.divs e#r1 e#r2)) (eval_operation ge (Eval(Vptr sp Int.zero)) op e##args).

Lemma val_divu_pow2
     : forall x (n logn : int),
       Int.is_power2 n = Some logn ->
       same_eval (Val.divu x (Eval (Vint n)))
                 (Val.shru x (Eval (Vint logn))).

Lemma make_divuimm_correct:
  forall n r1 r2,
  is_constant (Vint n) e#r2 ->
  let (op, args) := make_divuimm n r1 r2 in
  opt_lessdef (Some (Val.divu e#r1 e#r2)) (eval_operation ge (Eval (Vptr sp Int.zero)) op e##args).

Lemma val_modu_pow2 :
  forall x n logn,
    Int.is_power2 n = Some logn ->
    same_eval (Val.modu x (Eval (Vint n))) (Val.and x (Eval (Vint (Int.sub n Int.one)))).
  

Lemma make_moduimm_correct:
  forall n r1 r2,
  is_constant (Vint n) e#r2 ->
  let (op, args) := make_moduimm n r1 r2 in
  opt_lessdef (Some (Val.modu e#r1 e#r2)) (eval_operation ge (Eval (Vptr sp Int.zero)) op e##args).

Lemma and_zero : forall x,
    Val.lessdef (Val.and x (Eval (Vint Int.zero))) (Eval (Vint Int.zero)).

Lemma and_mone : forall x,
    Val.lessdef (Val.and x (Eval (Vint Int.mone))) x.


Lemma make_andimm_correct:
  forall n r x v,
  evmatch bc e#r x ->
  is_constant (Vint n) v ->
  let (op, args) := make_andimm n r x in
  opt_lessdef (Some (Val.and e#r v)) (eval_operation ge (Eval (Vptr sp Int.zero)) op e##args).

Lemma make_orimm_correct:
  forall n r x,
    is_constant (Vint n) x ->
    let (op, args) := make_orimm n r in
    opt_lessdef (Some (Val.or e#r x)) (eval_operation ge (Eval(Vptr sp Int.zero)) op e##args).

Lemma make_xorimm_correct:
  forall n r x,
    is_constant (Vint n) x ->
    let (op, args) := make_xorimm n r in
  opt_lessdef (Some (Val.xor e#r x)) (eval_operation ge (Eval (Vptr sp Int.zero)) op e##args).


Lemma make_mulfimm_correct:
  forall n r1 r2,
  is_constant (Vfloat n) e#r2 ->
  let (op, args) := make_mulfimm n r1 r1 r2 in
  opt_lessdef (Some (Val.mulf e#r1 e#r2))
              (eval_operation ge (Eval(Vptr sp Int.zero)) op e##args).

Lemma make_mulfimm_correct_2:
  forall n r1 r2,
  is_constant (Vfloat n) e#r1 ->
  let (op, args) := make_mulfimm n r2 r1 r2 in
  opt_lessdef (Some (Val.mulf e#r1 e#r2)) (eval_operation ge (Eval(Vptr sp Int.zero)) op e##args).

Lemma make_mulfsimm_correct:
  forall n r1 r2,
    is_constant (Vsingle n) e#r2 ->
  let (op, args) := make_mulfsimm n r1 r1 r2 in
  opt_lessdef (Some (Val.mulfs e#r1 e#r2))
              (eval_operation ge (Eval(Vptr sp Int.zero)) op e##args).


Lemma make_mulfsimm_correct_2:
  forall n r1 r2,
  is_constant (Vsingle n) e#r1 ->
  let (op, args) := make_mulfsimm n r2 r1 r2 in
  opt_lessdef (Some (Val.mulfs e#r1 e#r2)) (eval_operation ge (Eval (Vptr sp Int.zero)) op e##args).


Lemma make_cast8signed_correct:
  forall r x,
  evmatch bc e#r x ->
  let (op, args) := make_cast8signed r x in
  opt_lessdef (Some (Val.sign_ext 8 e#r)) (eval_operation ge (Eval(Vptr sp Int.zero)) op e##args).

Lemma make_cast8unsigned_correct:
  forall r x,
  evmatch bc e#r x ->
  let (op, args) := make_cast8unsigned r x in
  opt_lessdef (Some (Val.zero_ext 8 e#r)) (eval_operation ge (Eval(Vptr sp Int.zero)) op e##args).

Lemma make_cast16signed_correct:
  forall r x,
  evmatch bc e#r x ->
  let (op, args) := make_cast16signed r x in
  opt_lessdef (Some (Val.sign_ext 16 e#r)) (eval_operation ge (Eval(Vptr sp Int.zero)) op e##args).


Lemma make_cast16unsigned_correct:
  forall r x,
  evmatch bc e#r x ->
  let (op, args) := make_cast16unsigned r x in
  opt_lessdef (Some (Val.zero_ext 16 e#r)) (eval_operation ge (Eval(Vptr sp Int.zero)) op e##args).

Lemma val_sub_add_opp :
  forall x y n,
    is_constant (Vint n) y ->
    same_eval (Val.sub x y) (Val.add x (Val.neg y)).


Lemma xor_commut :
  forall x y, same_eval (Val.xor x y) (Val.xor y x).
     


Lemma same_eval_opt_lessdef : forall x y z,
    same_eval x y ->
    (opt_lessdef (Some x) z <-> opt_lessdef (Some y) z).

Lemma move_let :
  forall v (F:operation * list reg) ,
  (let (op', args') := F in
   opt_lessdef (Some v) (eval_operation ge (Eval(Vptr sp Int.zero)) op' e##args')) <->
  opt_lessdef (Some v) (let (op', args') := F in
                         eval_operation ge (Eval(Vptr sp Int.zero)) op' e##args').

Lemma op_strength_reduction_correct_opt:
  forall op args vl v,
  vl = map (fun r => AE.get r ae) args ->
  eval_operation ge (Eval(Vptr sp Int.zero)) op e##args = Some v ->
  let (op', args') := op_strength_reduction op args vl in
  opt_lessdef (Some v) (eval_operation ge (Eval(Vptr sp Int.zero)) op' e##args').

Lemma op_strength_reduction_correct:
  forall op args vl v,
  vl = map (fun r => AE.get r ae) args ->
  eval_operation ge (Eval(Vptr sp Int.zero)) op e##args = Some v ->
  let (op', args') := op_strength_reduction op args vl in
  exists w, eval_operation ge (Eval(Vptr sp Int.zero)) op' e##args' = Some w /\ Val.lessdef v w.

  


End STRENGTH_REDUCTION.