Require Import Coqlib.
Require Import AST.
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 ConstpropOp.
Require Import Constprop.

Correctness of the static analysis

Section ANALYSIS.

Variable ge: genv.
Variable sp: val.


Definition val_match_approx (a: approx) (v: val) : Prop :=
  match a with
  | Unknown => True
  | I p => v = Vint p
  | F p => v = Vfloat p
  | G symb ofs => v = symbol_address ge symb ofs
  | S ofs => v = Val.add sp (Vint 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 (G _ _) ?v) |- _ =>
      simpl in H; (try subst v); SimplVMA
  | H: (val_match_approx (S _) ?v) |- _ =>
      simpl in H; (try subst v); SimplVMA
  | _ =>
      idtac
  end.

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


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

Remark shift_symbol_address:
  forall symb ofs n,
  symbol_address ge symb (Int.add ofs n) = Val.add (symbol_address ge symb ofs) (Vint n).

Lemma eval_static_addressing_correct:
  forall addr 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 al vl m v,
  val_list_match_approx al vl ->
  eval_operation ge sp op vl m = Some v ->
  val_match_approx (eval_static_operation op al) v.

Correctness of strength reduction

Section STRENGTH_REDUCTION.

Variable app: D.t.
Variable rs: regset.
Variable m: mem.
Hypothesis MATCH: forall r, val_match_approx (approx_reg app r) rs#r.

Ltac InvApproxRegs :=
  match goal with
  | [ H: _ :: _ = _ :: _ |- _ ] =>
        injection H; clear H; intros; InvApproxRegs
  | [ H: ?v = approx_reg app ?r |- _ ] =>
        generalize (MATCH r); rewrite <- H; clear H; intro; InvApproxRegs
  | _ => idtac
  end.

Lemma cond_strength_reduction_correct:
  forall cond args vl,
  vl = approx_regs app args ->
  let (cond', args') := cond_strength_reduction cond args vl in
  eval_condition cond' rs##args' m = eval_condition cond rs##args m.

Lemma addr_strength_reduction_correct:
  forall addr args vl,
  vl = approx_regs app args ->
  let (addr', args') := addr_strength_reduction addr args vl in
  eval_addressing ge sp addr' rs##args' = eval_addressing ge sp addr rs##args.

Lemma make_addimm_correct:
  forall n r,
  let (op, args) := make_addimm n r in
  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v.
  
Lemma make_shlimm_correct:
  forall n r1,
  let (op, args) := make_shlimm n r1 in
  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v.

Lemma make_shrimm_correct:
  forall n r1,
  let (op, args) := make_shrimm n r1 in
  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v.

Lemma make_shruimm_correct:
  forall n r1,
  let (op, args) := make_shruimm n r1 in
  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v.

Lemma make_mulimm_correct:
  forall n r1,
  let (op, args) := make_mulimm n r1 in
  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v.

Lemma make_divimm_correct:
  forall n r1 r2 v,
  Val.divs rs#r1 rs#r2 = Some v ->
  rs#r2 = Vint n ->
  let (op, args) := make_divimm n r1 r2 in
  exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.

Lemma make_divuimm_correct:
  forall n r1 r2 v,
  Val.divu rs#r1 rs#r2 = Some v ->
  rs#r2 = Vint n ->
  let (op, args) := make_divuimm n r1 r2 in
  exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.

Lemma make_moduimm_correct:
  forall n r1 r2 v,
  Val.modu rs#r1 rs#r2 = Some v ->
  rs#r2 = Vint n ->
  let (op, args) := make_moduimm n r1 r2 in
  exists w, eval_operation ge sp op rs##args m = Some w /\ Val.lessdef v w.

Lemma make_andimm_correct:
  forall n r,
  let (op, args) := make_andimm n r in
  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v.

Lemma make_orimm_correct:
  forall n r,
  let (op, args) := make_orimm n r in
  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v.

Lemma make_xorimm_correct:
  forall n r,
  let (op, args) := make_xorimm n r in
  exists v, eval_operation ge sp op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v.

Lemma op_strength_reduction_correct:
  forall op args vl v,
  vl = approx_regs app args ->
  eval_operation ge sp op rs##args m = Some v ->
  let (op', args') := op_strength_reduction op args vl in
  exists w, eval_operation ge sp op' rs##args' m = Some w /\ Val.lessdef v w.

Lemma builtin_strength_reduction_correct:
  forall ef args vl m t vres m',
  vl = approx_regs app args ->
  external_call ef ge rs##args m t vres m' ->
  let (ef', args') := builtin_strength_reduction ef args vl in
  external_call ef' ge rs##args' m t vres m'.

End STRENGTH_REDUCTION.

End ANALYSIS.