Require Import Coqlib.
Require Import Ast.
Require Import Integers.
Require Import Pointers.
Require Import Floats.
Require Import Values.
Require Import Mem.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import ConstpropOp.
Require Import Constprop.

Correctness of the static analysis

Section ANALYSIS.

Variable ge: genv.


Definition val_match_approx (a: approx) (v: val) : Prop :=
  match a with
  | Unknown => True
  | I p => v = Vint p
  | F p => v = Vfloat p
  | S symb ofs => exists b, Genv.find_symbol ge symb = Some b /\ v = Vptr (Ptr.add b ofs)
  | _ => False
  end.

Inductive val_list_match_approx: list approx -> list val -> Prop :=
  | vlma_nil:
      val_list_match_approx nil nil
  | vlma_cons:
      forall a al v vl,
      val_match_approx a v ->
      val_list_match_approx al vl ->
      val_list_match_approx (a :: al) (v :: vl).

Ltac SimplVMA :=
  match goal with
  | H: (val_match_approx (I _) ?v) |- _ =>
      simpl in H; (try subst v); SimplVMA
  | H: (val_match_approx (F _) ?v) |- _ =>
      simpl in H; (try subst v); SimplVMA
  | H: (val_match_approx (S _ _) ?v) |- _ =>
      simpl in H;
      (try (elim H;
            let b := fresh "b" in let A := fresh in let B := fresh in
            (intros b [A B]; subst v; clear H)));
      SimplVMA
  | _ =>
      idtac
  end.

Ltac InvVLMA :=
  match goal with
  | H: (val_list_match_approx nil ?vl) |- _ =>
      inversion H
  | H: (val_list_match_approx (?a :: ?al) ?vl) |- _ =>
      inversion H ; SimplVMA; InvVLMA
  | _ =>
      idtac
  end.


Lemma eval_static_condition_correct:
  forall cond al vl b,
  val_list_match_approx al vl ->
  eval_static_condition cond al = Some b ->
  eval_condition cond vl = Some b.

Ltac FZSimpPtr :=
  match goal with
| H: (match ?v with | Ptr _ _ => _ end) = Some _ |- _ =>
  destruct v as [b' ofs']; inv H
end.

Ltac FZSimplGenv :=
 match goal with
   | [ H : Genv.find_symbol _ _ |- _ ] =>
      match goal with
        | [ H' : Genv.find_symbol _ _ |- _ ] =>
            try ( rewrite H' in H )
      end
end.

Ltac FZSimplVMA :=
  match goal with
 | H: (val_match_approx (I _) ?v) |- _ =>
      simpl in H; (try subst v); FZSimplVMA
  | H: (val_match_approx (F _) ?v) |- _ =>
      simpl in H; (try subst v); FZSimplVMA
  | H: (val_match_approx (S _ _) ?v) |- _ =>
      simpl in H;
      elim H;
        let b := fresh "b" in let A := fresh in let B := fresh in
            (intros b [A B]; (try subst v); clear H);
      FZSimplVMA
 | _ =>
      idtac
  end.
  

Ltac FZInvVLMA :=
  match goal with
  | H: (val_list_match_approx (?a :: ?al) ?vl) |- _ =>
      inversion H; FZSimplVMA
  end.

Ltac FZsimplify :=
  try FZSimpPtr; try FZInvVLMA; try FZInvVLMA; try clarify.

Lemma eval_static_addressing_correct:
  forall addr sp al vl v,
  val_list_match_approx al vl ->
  eval_addressing ge sp addr vl = Some v ->
  val_match_approx (eval_static_addressing addr al) v.


Lemma eval_static_operation_correct:
  forall op sp al vl v,
  val_list_match_approx al vl ->
  eval_operation ge sp op vl = Some v ->
  val_match_approx (eval_static_operation op al) v.

Correctness of strength reduction

Section STRENGTH_REDUCTION.

Variable app: reg -> approx.
Variable sp: option pointer.
Variable rs: regset.
Hypothesis MATCH: forall r, val_match_approx (app r) rs#r.

Lemma intval_correct:
  forall r n,
  intval app r = Some n -> rs#r = Vint n.

Lemma cond_strength_reduction_correct:
  forall cond args,
  let (cond', args') := cond_strength_reduction app cond args in
  eval_condition cond' rs##args' = eval_condition cond rs##args.

Ltac KnownApprox :=
  match goal with
  | H: ?approx ?r = ?a |- _ =>
      generalize (MATCH r); rewrite H; intro; clear H; KnownApprox
  | _ => idtac
  end.
 
Lemma addr_strength_reduction_correct:
  forall addr args,
  let (addr', args') := addr_strength_reduction app addr args in
  eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args.

Lemma make_shlimm_correct:
  forall n r v,
  let (op, args) := make_shlimm n r in
  eval_operation ge sp Oshl (rs#r :: Vint n :: nil) = Some v ->
  eval_operation ge sp op rs##args = Some v.

Lemma make_shrimm_correct:
  forall n r v,
  let (op, args) := make_shrimm n r in
  eval_operation ge sp Oshr (rs#r :: Vint n :: nil) = Some v ->
  eval_operation ge sp op rs##args = Some v.

Lemma make_shruimm_correct:
  forall n r v,
  let (op, args) := make_shruimm n r in
  eval_operation ge sp Oshru (rs#r :: Vint n :: nil) = Some v ->
  eval_operation ge sp op rs##args = Some v.

Lemma make_mulimm_correct:
  forall n r v,
  let (op, args) := make_mulimm n r in
  eval_operation ge sp Omul (rs#r :: Vint n :: nil) = Some v ->
  eval_operation ge sp op rs##args = Some v.

Lemma make_andimm_correct:
  forall n r v,
  let (op, args) := make_andimm n r in
  eval_operation ge sp Oand (rs#r :: Vint n :: nil) = Some v ->
  eval_operation ge sp op rs##args = Some v.

Lemma make_orimm_correct:
  forall n r v,
  let (op, args) := make_orimm n r in
  eval_operation ge sp Oor (rs#r :: Vint n :: nil) = Some v ->
  eval_operation ge sp op rs##args = Some v.

Lemma make_xorimm_correct:
  forall n r v,
  let (op, args) := make_xorimm n r in
  eval_operation ge sp Oxor (rs#r :: Vint n :: nil) = Some v ->
  eval_operation ge sp op rs##args = Some v.

Lemma op_strength_reduction_correct:
  forall op args v,
  let (op', args') := op_strength_reduction app op args in
  eval_operation ge sp op rs##args = Some v ->
  eval_operation ge sp op' rs##args' = Some v.

End STRENGTH_REDUCTION.

End ANALYSIS.