Module ValueAnalysis_proof

Correctness proof of the value analysis.

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import RTL.
Require Import LatticeSignatures.
Require Import CfgIterator.
Require Import ValueAnalysis.
Require Import DLib.

Definition gamma (a: t) (rs: regset) : Prop :=
  BWLattice.gamma bwlat a rs.

Lemma analyze_postfixpoint: forall f pc1 ins,
  f.(fn_code)!pc1 = Some ins -> forall pc2 tf,
    In (pc2,tf) (transfer ins) ->
    gamma (tf (analyze f pc1)) ⊆ gamma (analyze f pc2).
Proof.
  intros; unfold gamma, analyze.
  apply (BourdoncleIterator.analyze_postfixpoint
    bwlat f transfer (BWLattice.top bwlat) _ _ H _ _ H0).
Qed.

Lemma analyze_entrypoint: forall f,
  gamma (BWLattice.top bwlat) ⊆ gamma (analyze f f.(fn_entrypoint)).
Proof.
  intros; unfold gamma, analyze.
  apply (BourdoncleIterator.analyze_entrypoint
    bwlat f transfer (BWLattice.top bwlat)).
Qed.

Lemma eval_condition_Ccomp_neg : forall c l m,
  eval_condition (Ccomp c) l m = Some false ->
  eval_condition (Ccomp (neg_cmp c)) l m = Some true.
Proof.
  destruct c; destruct l; simpl;
  repeat match goal with
      [ |- context[match ?l with nil => _ | cons _ _ => _ end]] => destruct l
     end;
  try congruence;
  destruct v; simpl; try congruence;
  destruct v0; simpl; try congruence;
  match goal with
      [ |- context[negb ?b]] => destruct b; simpl; congruence
  end.
Qed.

Lemma eval_condition_Ccompimm_neg : forall c n l m,
  eval_condition (Ccompimm c n) l m = Some false ->
  eval_condition (Ccompimm (neg_cmp c) n) l m = Some true.
Proof.
  destruct c; destruct l; simpl;
  repeat match goal with
      [ |- context[match ?l with nil => _ | cons _ _ => _ end]] => destruct l
     end;
  try congruence;
  destruct v; simpl; try congruence;
  match goal with
      [ |- context[negb ?b]] => destruct b; simpl; congruence
  end.
Qed.

Lemma eval_condition_Ccompu_neg : forall c l m,
  eval_condition (Ccompu c) l m = Some false ->
  eval_condition (Ccompu (neg_cmp c)) l m = Some true.
Proof.
  destruct c; destruct l; simpl;
  repeat match goal with
      [ |- context[match ?l with nil => _ | cons _ _ => _ end]] => destruct l
     end;
  try congruence;
  destruct v; simpl; try congruence;
  destruct v0; simpl; try congruence;
  intros m;
  try destruct_bool_in_goal; try congruence;
  repeat match goal with
      [ |- context[negb ?b]] => destruct b; simpl
  end; try congruence;
  try destruct_bool_in_goal; try congruence.
Qed.

Lemma eval_condition_Ccompuimm_neg : forall c n l m,
  eval_condition (Ccompuimm c n) l m = Some false ->
  eval_condition (Ccompuimm (neg_cmp c) n) l m = Some true.
Proof.
  destruct c; destruct l; simpl;
  repeat match goal with
      [ |- context[match ?l with nil => _ | cons _ _ => _ end]] => destruct l
     end;
  try congruence;
  destruct v; simpl; try congruence;
  try destruct_bool_in_goal; try congruence;
  repeat match goal with
      [ |- context[negb ?b]] => destruct b; simpl
  end; try congruence;
  try destruct_bool_in_goal; try congruence.
Qed.

Lemma eval_condition_neg_cond: forall c args m,
  eval_condition c args m = Some false ->
  (forall args ab, assume (neg_cond c) args ab = ab) \/
  eval_condition (neg_cond c) args m = Some true.
Proof.
  destruct c; intros; try (left; reflexivity); right.
  apply eval_condition_Ccomp_neg; auto.
  apply eval_condition_Ccompu_neg; auto.
  apply eval_condition_Ccompimm_neg; auto.
  apply eval_condition_Ccompuimm_neg; auto.
Qed.

Lemma gamma_set2 : forall app rs ab v x,
  gamma app rs ->
  BWLattice.gamma Val.bwlat ab v ->
  gamma (WPMap.set app x ab) (rs # x <- v).
Proof.
  unfold gamma, Val.bwlat, bwlat; intros; simpl.
  eapply WPMap.gamma_set2; auto.
Qed.

Lemma gamma_set1 : forall app rs ab x,
  gamma app rs ->
  BWLattice.gamma Val.bwlat ab (rs#x) ->
  gamma (WPMap.set app x ab) rs.
Proof.
  unfold gamma, Val.bwlat, bwlat; intros; simpl.
  eapply WPMap.gamma_set1; auto.
Qed.

Lemma upd_top_correct : forall ab rs dst v,
  gamma ab rs ->
  gamma (WPMap.set ab dst (BWLattice.top Val.bwlat)) (rs # dst <- v).
Proof.
  intros.
  apply gamma_set2; auto.
Qed.

Section PRESERVATION.
  
  Variable ge: genv.

  Lemma get_list_bot_False: forall ab rs args,
    gamma ab rs ->
    get_list ab args = GL_Bot -> False.
Proof.
    induction args; simpl.
    congruence.
    case_eq (WPMap.get Val.wlat ab a).
    destruct t.
    destruct t0; try congruence.
    case_eq (get_list ab args); intros; try congruence; eauto.
    intros.
    generalize (H0 a); rewrite H; auto.
  Qed.

  Inductive all_Vint : list val -> Prop :=
  | all_Vint_nil: all_Vint nil
  | all_Vint_cons: forall i l
    (AV:all_Vint l),
    all_Vint (Vint i :: l).

  Inductive gamma_list : list Interval.t -> list val -> Prop :=
  | gamma_list_nil : gamma_list nil nil
  | gamma_list_cons : forall v ab l abl
    (GL:gamma_list abl l)
    (GLV:WLattice.gamma Interval.wlat ab v),
    gamma_list (ab::abl) (v::l).

  Lemma get_list_some_all_Vint: forall ab rs args l,
    gamma ab rs ->
    get_list ab args = GL_Some l ->
    all_Vint rs ## args /\ gamma_list l rs ## args.
Proof.
    induction args; simpl.
    intros.
    inv H0; split; constructor.
    case_eq (WPMap.get Val.wlat ab a); try congruence.
    destruct t; destruct t0; try congruence.
    case_eq (get_list ab args); try congruence.
    intros.
    inv H2.
    generalize (H1 a); rewrite H0; destruct 1.
    destruct (rs#a); inv H3.
    edestruct IHargs; eauto.
    split; constructor; eauto.
  Qed.

  Lemma eval_operation_all_int: forall sp op args m v,
    eval_operation ge sp op args m = Some v ->
    all_Vint args ->
    eval_op_gives_VInt op (length args) = true ->
    exists i, v = Vint i.
Proof.
    intros.
    set (op':=op).
    destruct op; simpl in H;
    inv H0; try congruence;
    try (inv AV; try congruence);
    try (inv AV0; try congruence);
      simpl in *;
    repeat match goal with [ _: context[if ?x then _ else _] |- _] => destruct x end;
      try congruence;
    repeat match goal with [ id: context[Some _ = Some _] |- _] => inv id end;
      eauto;
    try (destruct a; simpl in H; inv H1; congruence);
    try (destruct a; simpl in H; inv H1; try congruence; inv H; eauto; fail);
    destruct c; try congruence; simpl;
    try (destruct_bool_in_goal; unfold Vtrue, Vfalse; eauto).
  Qed.

  Ltac inv_list :=
    repeat match goal with
      | id: all_Vint _ |- _ => inv id; try clear id
      | id: gamma_list _ _ |- _ => inv id; try clear id
    end.

  Lemma ab_operation_correct : forall l sp op args m i,
    all_Vint args ->
    gamma_list l args ->
    eval_operation ge sp op args m = Some (Vint i) ->
    WLattice.gamma Interval.wlat (ab_operation op l) (Vint i).
Proof.
    intros l sp op args m i Ha Hg He.
    destruct op; simpl in He; FuncInv; simpl ab_operation;
    try match goal with
        id : eval_addressing _ _ ?a _ = Some _ |- _ =>
          destruct a; simpl in He; FuncInv
        end;
      try apply (WLattice.gamma_top Interval.wlat).
    inv_list; simpl; auto.
    inv_list; simpl; omega.
    inv_list; simpl ab_operation.
    case_eq (cast_int8s ab); unfold cast_int8s; intros; auto.
    simpl in H.
    rewrite (@sign_ext_same 7%nat 24%nat) in H; auto with zarith.
    inv H; auto.
    apply Interval.is_in_interval_correct with (1:=H0); intuition.
    apply (WLattice.gamma_top Interval.wlat).
    inv_list; simpl ab_operation.
    case_eq (cast_int8u ab); unfold cast_int8u; intros; auto.
    simpl in H.
    rewrite (@zero_ext_same 8%nat 24%nat) in H; auto with zarith.
    inv H; auto.
    apply Interval.is_in_interval_correct with (1:=H0); intuition.
    apply (WLattice.gamma_top Interval.wlat).
    inv_list; simpl ab_operation.
    case_eq (cast_int16s ab); unfold cast_int16s; intros; auto.
    simpl in H.
    rewrite (@sign_ext_same 15%nat 16%nat) in H; auto with zarith.
    inv H; auto.
    apply Interval.is_in_interval_correct with (1:=H0); intuition.
    apply (WLattice.gamma_top Interval.wlat).
    inv_list; simpl ab_operation.
    case_eq (cast_int16u ab); unfold cast_int16s; intros; auto.
    simpl in H.
    rewrite (@zero_ext_same 16%nat 16%nat) in H; auto with zarith.
    inv H; auto.
    apply Interval.is_in_interval_correct with (1:=H0); intuition.
    apply (WLattice.gamma_top Interval.wlat).
    inv_list; simpl ab_operation.
    simpl in H; inv H.
    apply Interval.neg_correct; auto.
    inv_list; simpl ab_operation.
    inv H.
    apply Interval.sub_correct; auto.
    inv_list; simpl ab_operation.
    inv_list; simpl ab_operation.
    inv H.
    apply Interval.mul_correct; auto.
    inv_list; simpl ab_operation.
    inv H.
    apply Interval.mul_correct; auto.
    inv_list; simpl ab_operation; inv H;
      apply Interval.add_correct; auto.
    inv_list; simpl ab_operation; inv H;
      apply Interval.add_correct; auto.
      apply Interval.add_correct; auto.
    inv_list; simpl ab_operation; inv H;
      apply Interval.add_correct; auto.
      apply Interval.mul_correct; auto.
    inv_list; simpl ab_operation; inv H;
      apply Interval.add_correct; auto.
      apply Interval.add_correct; auto.
      apply Interval.mul_correct; auto.
    destruct (eval_condition c args m); inv H.
    destruct b; inv H1; simpl.
    apply Interval.bool_correct_one.
    apply Interval.bool_correct_zero.
  Qed.

  Lemma length_get_list: forall ab args l,
    get_list ab args = GL_Some l ->
    length args = length l.
Proof.
    induction args; simpl; intros.
    > inv H; auto.
    > destruct (WPMap.get Val.wlat ab a); try congruence.
      destruct t; try congruence.
      destruct t0; try congruence.
      case_eq (get_list ab args); intros.
      rewrite H0 in H; inv H.
      rewrite H0 in H; inv H.
      generalize (IHargs l0); rewrite H0 in *.
      inv H; simpl in *.
      f_equal; auto.
  Qed.

  Lemma ab_op_correct : forall sp op rs args m v ab res,
    eval_operation ge sp op (rs ## args) m = Some v ->
    gamma ab rs ->
    gamma (ab_op op args res ab) (rs # res <- v).
Proof.
    intros.
    unfold ab_op.
    case_eq (get_list ab args); intros.
    eelim get_list_bot_False; eauto.
    apply gamma_set2; auto.
    destruct ab; auto.
    case_eq (eval_op_gives_VInt op (length l)); intros;
    apply gamma_set2; auto.
    edestruct get_list_some_all_Vint as [G1 G2]; eauto.
    edestruct eval_operation_all_int as [i Hi]; eauto.
    exploit length_get_list; eauto; intros Hl.
    rewrite map_length; simpl; unfold reg in *; congruence.
    subst v.
    split; [idtac | simpl; auto].
    eapply ab_operation_correct; eauto.
  Qed.

Lemma swap_prop: forall A (x y:A*A), swap x = y -> x = swap y.
Proof.
  destruct x; destruct y; simpl; congruence.
Qed.

Lemma gamma_backward_cmp: forall c it1 it2 it1' it2' i1 i2,
  backward_cmp c it1 it2 = (it1',it2') ->
  WLattice.gamma Interval.wlat it1 (Vint i1) ->
  WLattice.gamma Interval.wlat it2 (Vint i2) ->
  Int.cmp c i1 i2 = true ->
  BWLattice.gamma Interval.bwlat it1' (Vint i1) /\
  BWLattice.gamma Interval.bwlat it2' (Vint i2).
Proof.
  destruct c; intros.
  exploit Interval.gamma_backward_eq; eauto.
  exploit Interval.gamma_backward_ne; eauto.
  exploit Interval.gamma_backward_lt; eauto.
  exploit Interval.gamma_backward_le; eauto.
  apply swap_prop in H; simpl in H.
  exploit Interval.gamma_backward_lt; eauto; intuition.
  apply swap_prop in H; simpl in H.
  exploit Interval.gamma_backward_le; eauto; intuition.
Qed.

Lemma gamma_backward_cmpu: forall c it1 it2 it1' it2' i1 i2,
  backward_cmpu c it1 it2 = (it1',it2') ->
  WLattice.gamma Interval.wlat it1 (Vint i1) ->
  WLattice.gamma Interval.wlat it2 (Vint i2) ->
  Int.cmpu c i1 i2 = true ->
  BWLattice.gamma Interval.bwlat it1' (Vint i1) /\
  BWLattice.gamma Interval.bwlat it2' (Vint i2).
Proof.
  destruct c; intros.
  exploit Interval.gamma_backward_eq; eauto.
  exploit Interval.gamma_backward_ne; eauto.
  exploit Interval.gamma_backward_ltu; eauto.
  exploit Interval.gamma_backward_leu; eauto.
  apply swap_prop in H; simpl in H.
  exploit Interval.gamma_backward_ltu; eauto; intuition.
  apply swap_prop in H; simpl in H.
  exploit Interval.gamma_backward_leu; eauto; intuition.
Qed.

  Lemma assume_correct : forall cond rs args m ab,
    eval_condition cond rs ## args m = Some true ->
    gamma ab rs ->
    gamma (assume cond args ab) rs.
Proof.
    destruct cond; intros;
    destruct args as [|r1 [|r2 [|r3 L]]]; simpl; auto.
    generalize dependent H; simpl.
    case_eq (rs#r1); try congruence;
    case_eq (rs#r2); try congruence; intros;
    simpl in H2; try congruence.
    unfold backward_cmp_var_var, backward2.
    generalize (H0 r1).
    case_eq ((WPMap.get Val.wlat ab r1)); intros; [idtac|elim H4].
    generalize (H0 r2).
    case_eq ((WPMap.get Val.wlat ab r2)); intros; [idtac|elim H6].
    rewrite H in *; rewrite H1 in *.
    destruct t; destruct t1; auto.
    destruct t0; destruct t1; auto.
    destruct H6; destruct H4.
    case_eq (backward_cmp c t t0); intros.
    inv H2.
    exploit gamma_backward_cmp; eauto.
    intros [G1 G2].
    destruct i1; try (elim G1; fail).
    destruct i2; try (elim G2; fail).
    apply gamma_set1.
    apply gamma_set1; auto.
    rewrite H1; split; auto.
    rewrite H; split; auto.
    generalize dependent H; simpl.
    case_eq (rs#r1); try congruence;
    case_eq (rs#r2); try congruence; intros;
    simpl in H2; try congruence;
    unfold backward_cmpu_var_var, backward2.
    generalize (H0 r1).
    case_eq ((WPMap.get Val.wlat ab r1)); intros; [idtac|elim H4].
    generalize (H0 r2).
    case_eq ((WPMap.get Val.wlat ab r2)); intros; [idtac|elim H6].
    rewrite H in *; rewrite H1 in *.
    destruct t; destruct t1; auto.
    destruct t0; destruct t1; auto.
    destruct H6; destruct H4.
    case_eq (backward_cmpu c t t0); intros.
    inv H2.
    exploit gamma_backward_cmpu; eauto.
    intros [G1 G2].
    destruct i1; try (elim G1; fail).
    destruct i2; try (elim G2; fail).
    apply gamma_set1.
    apply gamma_set1; auto.
    rewrite H1; split; auto.
    rewrite H; split; auto.
    generalize (H0 r1).
    case_eq ((WPMap.get Val.wlat ab r1)); intros; [idtac|elim H4].
    generalize (H0 r2).
    case_eq ((WPMap.get Val.wlat ab r2)); intros; [idtac|elim H6].
    rewrite H in *; rewrite H1 in *.
    destruct t; destruct t1; auto.
    destruct t0; destruct t1; auto.
    destruct H6; destruct H4.
    inv H7.
    generalize (H0 r1).
    case_eq ((WPMap.get Val.wlat ab r1)); intros; [idtac|elim H4].
    generalize (H0 r2).
    case_eq ((WPMap.get Val.wlat ab r2)); intros; [idtac|elim H6].
    rewrite H in *; rewrite H1 in *.
    destruct t; destruct t1; auto.
    destruct t0; destruct t1; auto.
    destruct H6; destruct H4.
    inv H8.
    generalize (H0 r1).
    case_eq ((WPMap.get Val.wlat ab r1)); intros; [idtac|elim H4].
    generalize (H0 r2).
    case_eq ((WPMap.get Val.wlat ab r2)); intros; [idtac|elim H6].
    rewrite H in *; rewrite H1 in *.
    destruct t; destruct t1; auto.
    destruct t0; destruct t1; auto.
    destruct H6; destruct H4.
    inv H8.
    generalize dependent H; simpl.
    case_eq (rs#r1); try congruence; intros;
    simpl in H1; try congruence;
    unfold backward_cmp_var_cst, backward1.
    generalize (H0 r1).
    case_eq ((WPMap.get Val.wlat ab r1)); intros; [idtac|elim H3].
    rewrite H in *.
    destruct t; destruct t0; auto.
    case_eq (backward_cmp c t (Interval.signed i)); intros.
    inv H1; destruct H3.
    exploit gamma_backward_cmp; eauto.
    apply Interval.signed_correct.
    intros [G1 G2].
    destruct i1; try (elim G1; fail).
    destruct i2; try (elim G2; fail).
    apply gamma_set1; auto.
    rewrite H; split; auto.
    generalize dependent H; simpl.
    case_eq (rs#r1); try congruence; intros;
    simpl in H1; try congruence;
    unfold backward_cmpu_var_cst, backward1.
    generalize (H0 r1).
    case_eq ((WPMap.get Val.wlat ab r1)); intros; [idtac|elim H3].
    rewrite H in *.
    destruct t; destruct t0; auto.
    case_eq (backward_cmpu c t (Interval.signed i)); intros.
    inv H1; destruct H3.
    exploit gamma_backward_cmpu; eauto.
    apply Interval.signed_correct.
    intros [G1 G2].
    destruct i1; try (elim G1; fail).
    destruct i2; try (elim G2; fail).
    apply gamma_set1; auto.
    rewrite H; split; auto.
    generalize (H0 r1).
    case_eq ((WPMap.get Val.wlat ab r1)); intros; [idtac|elim H3].
    rewrite H in *.
    destruct t; destruct t0; auto.
    destruct H3.
    inv H4.
  Qed.

  Inductive gamma_stackframes: stackframe -> Prop :=
    gamma_stackframe_intro: forall res sp pc rs f,
      (forall v, gamma (analyze f pc) (rs#res <- v)) ->
      gamma_stackframes(Stackframe res f sp pc rs).

  Inductive gamma_state: state -> Prop :=
  | gamma_state_intro:
    forall s sp pc rs m f
      (MATCH: gamma (analyze f pc) rs)
      (STACKS: forall sf, In sf s -> gamma_stackframes sf),
      gamma_state (State s f sp pc rs m)
  | gamma_state_call:
    forall s f args m
      (STACKS: forall sf, In sf s -> gamma_stackframes sf),
      gamma_state (Callstate s f args m)
  | gamma_state_return:
    forall s v m
      (STACKS: forall sf, In sf s -> gamma_stackframes sf),
      gamma_state (Returnstate s v m).


  Lemma eq_refl_left: forall A (x:A), x = x \/ False.
Proof.
auto. Qed.

  Lemma transf_step_correct:
    forall s1 t s2,
      step ge s1 t s2 -> gamma_state s1 -> gamma_state s2.
Proof.
    intros s1 t s2 Hstep Hg.
    inv Hstep; inv Hg; constructor; auto;
    try (apply (analyze_postfixpoint _ _ _ H _ _ (eq_refl_left _ _)); auto).
    eapply ab_op_correct; eauto.
    case_eq (analyze f pc); [intros t H' | intros H']; rewrite H' in MATCH.
    eapply upd_top_correct; eauto.
    unfold gamma in MATCH.
    specialize (MATCH dst); inv MATCH.
    simpl; intro sf; destruct 1; auto.
    subst; constructor; intros.
    apply (analyze_postfixpoint _ _ _ H _ _ (eq_refl_left _ _)).
    case_eq (analyze f pc); [intros t H' | intros H']; rewrite H' in MATCH.
    eapply upd_top_correct; eauto.
    unfold gamma in MATCH.
    specialize (MATCH res); inv MATCH.
    case_eq (analyze f pc); [intros t' H' | intros H']; rewrite H' in MATCH.
    eapply upd_top_correct; eauto.
    unfold gamma in MATCH.
    specialize (MATCH res); inv MATCH.
    destruct b.
    eapply (analyze_postfixpoint _ _ _ H); simpl; eauto.
    eapply assume_correct; eauto.
    eapply (analyze_postfixpoint _ _ _ H); simpl; eauto.
    eelim eval_condition_neg_cond; eauto; intros HE.
    rewrite HE; auto.
    eapply assume_correct; eauto.
    eapply (analyze_postfixpoint _ _ _ H); simpl.
    eapply (in_map (fun j : node => (j, fun ab => ab))).
    eapply list_nth_z_in; eauto.
    auto.
    apply analyze_entrypoint.
    apply BWLattice.gamma_top.
    assert (gamma_stackframes (Stackframe res f sp pc rs)) by auto with datatypes.
    inv H; auto.
  Qed.

End PRESERVATION.


Definition In_interval (z : Z) (itv : interval) :=
  (itv_min itv <= z <= itv_max itv)%Z.

Lemma itv_wf:
  forall itv,
    (itv_max itv >= itv_min itv)%Z.
Proof.
  destruct itv; auto.
Qed.

Require Import CountingSem.
Section PRESERVATION2.
  
  Variable ge: genv.

  Inductive gamma_cstate f: state -> Prop :=
  | gamma_cstate_intro:
    forall pc rs m
      (MATCH: gamma (analyze f pc) rs),
      gamma_cstate f (State pc rs m).
  
Lemma transf_cstep_correct:
  forall f sp s1 t s2,
    step ge f sp s1 t s2 -> gamma_cstate f s1 -> gamma_cstate f s2.
Proof.
  intros f sp s1 t s2 Hstep Hg.
  inv Hstep; inv Hg; try destruct b; try constructor; auto;
  try (apply (analyze_postfixpoint _ _ _ H _ _ (eq_refl_left _ _)); auto).
  eapply ab_op_correct; eauto.
  case_eq (analyze f pc); [intros t H' | intros H']; rewrite H' in MATCH.
  eapply upd_top_correct; eauto.
  unfold gamma in MATCH.
  specialize (MATCH dst); inv MATCH.
  case_eq (analyze f pc); [intros t' H' | intros H']; rewrite H' in MATCH.
  eapply upd_top_correct; eauto.
  unfold gamma in MATCH.
  specialize (MATCH res); inv MATCH.
  eapply (analyze_postfixpoint _ _ _ H); simpl; eauto.
  eapply assume_correct; eauto.
  eapply (analyze_postfixpoint _ _ _ H); simpl; eauto.
  eelim eval_condition_neg_cond; eauto; intros HE.
  rewrite HE; auto.
  eapply assume_correct; eauto.
  eapply (analyze_postfixpoint _ _ _ H); simpl.
  eapply (in_map (fun j : node => (j, fun ab => ab))).
  eapply list_nth_z_in; eauto.
  auto.
Qed.

Require Import Errors.

Theorem gamma_reach:
  forall rs m f fsc sp s,
    Reach ge f sp fsc rs m s -> gamma_cstate f s.
Proof.
  induction 1.
  > unfold init_st; constructor.
    unfold gamma.
    apply (analyze_entrypoint f).
    apply BWLattice.gamma_top.
  > inv H0; simpl in *.
    eapply transf_cstep_correct; eauto.
Qed.

variable_domains_are_safe states the correctness of the value analysis. It is later used to show the correctness of the local bound analysis.
Theorem variable_domains_are_safe:
  forall rs m f fsc sp s,
    Reach ge f sp fsc rs m s ->
    forall x itv,
      value f (get_pc s) x = OK itv ->
      exists i, (get_rs s) # x = Vint i /\
        In_interval (Int.signed i) itv.
Proof.
    intros.
    exploit gamma_reach; eauto.
    intros.
    inv H1.
    unfold value in *.
    subst; simpl in *.
    rewrite <- H3 in H0; simpl in H0.
    destruct (analyze f pc); inv H0.
    unfold gamma in MATCH.
    simpl in MATCH.
    generalize (MATCH x); simpl.
    destruct (t!x); try congruence.
    destruct t0.
    destruct t1; try congruence.
    destruct 1.
    destruct (rs0#x); inv H1.
    econstructor; split; eauto.
    destruct t0; simpl in H2.
    unfold make_interval in *.
    destruct Z_ge_dec; try congruence.
    inv H2; simpl in *.
    split; simpl; omega.
  Qed.

End PRESERVATION2.

Generated by coq2html