Module CFGAnalysis_proof

Correctness proof of the value analysis for CFG.

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 Memory.
Require Import Cminor.
Require Import CFG.
Require Import LatticeSignatures.
Require Import CfgIterator.
Require Import AbMemSignature.
Require Import Intervals.
Require Import CFGAnalysis.

Section abmem.
  Variable abmem: Type.
  Variable p : program.
  Let ge := Genv.globalenv p.

  Variable abdom: mem_dom (abmem+⊥).

  Let transfer := (transfer _ abdom).
  Let solve_pfp := (solve_pfp _ abdom).
  Instance abdom_dom : adom (abmem+⊥) memory := mem_adom _ abdom.

  Lemma solve_pfp_postfixpoint: forall f pc1 ins,
    f.(fn_code)!pc1 = Some ins -> forall pc2 tf,
      In (pc2,tf) (transfer pc1 ins) ->
      γ (tf (solve_pfp f pc1)) ⊆ γ (solve_pfp f pc2).
    apply (BourdoncleIterator.solve_pfp_postfixpoint abdom_dom
      f.(fn_entrypoint) f.(fn_code) transfer top _ _ H _ _ H0).
    apply H1.

  Lemma solve_pfp_entrypoint: forall f,
    γ top ⊆ γ (solve_pfp f f.(fn_entrypoint)).
    apply (BourdoncleIterator.solve_pfp_entrypoint abdom_dom
       f.(fn_entrypoint) f.(fn_code) transfer top); auto.

  Inductive gamma_stackframes: stackframe -> mem -> Prop :=
    gamma_stackframe_intro: forall res sp pc e f m b,
      (forall v, gamma (solve_pfp f pc) (set_optvar res v e,m)) ->
      sp = Vptr b ->
      gamma_stackframes (Stackframe res f sp pc e) m.

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

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

  Variable gamma_mem_insensitive : forall e m m' ab,
    gamma ab (e,m) -> gamma ab (e,m').

  Lemma gamma_sf_insensitive : forall sf m m',
    gamma_stackframes sf m -> gamma_stackframes sf m'.
    induction 1; econstructor; eauto.
  Hint Resolve gamma_sf_insensitive.

  Lemma transf_step_correct:
    forall s1 t s2,
      step ge s1 t s2 -> gamma_state s1 -> gamma_state s2.
    intros s1 t s2 Hstep Hg.
    inv Hstep; inv Hg; try constructor; eauto;
      try (apply (solve_pfp_postfixpoint _ _ _ H _ _ (eq_refl_left _ _)); auto).
    apply (assign_sound _ _ ge). exists e. exists m. eexists. exists v. intuition eauto.
    apply (store_sound _ _ ge). repeat econstructor; eauto.
    > simpl; destruct 1; auto.
      subst; econstructor; eauto.
      intros; destruct res; subst;
      apply (solve_pfp_postfixpoint _ _ _ H _ _ (eq_refl_left _ _)).
      apply forget_sound. repeat econstructor; eauto.
      > simpl; auto.
    > destruct res; simpl;
      apply (solve_pfp_postfixpoint _ _ _ H _ _ (eq_refl_left _ _)); eauto.
      apply gamma_mem_insensitive with m.
      apply forget_sound. repeat econstructor; eauto.
    > destruct b; eapply (solve_pfp_postfixpoint _ _ _ H).
      > simpl; left; reflexivity.
      > apply (assume_sound _ _ ge). eexists. exists v. intuition eauto.
      > simpl; right; left; reflexivity.
      > apply (assume_sound _ _ ge). eexists. eexists. intuition.
        > econstructor; eauto.
          destruct v; inv H1; simpl; eauto.
        > constructor; compute; congruence.
    > eapply (solve_pfp_postfixpoint _ _ _ H) with (tf:=(fun ab => ab)); simpl; auto.
      clear H MATCH STACKS H0.
      induction cases; simpl; auto.
      destruct a0.
      destruct IHcases.
      > injection H; clear H; intros.
        destruct Int.eq; auto.
        left; congruence.
      > destruct Int.eq; auto.
    > apply solve_pfp_entrypoint.
      apply gamma_top.
    > exploit STACKS; [left; eauto|intros T; inv T].
      econstructor; eauto. intuition.
  Theorem reach_gamma: forall (st:state),
    Reach p st -> gamma_state st.
    induction 1.
    > inv H; constructor; simpl; intuition.
    > eapply transf_step_correct; eauto.

End abmem.

Theorem value_analysis_correct_if_abmem_preserves_memory:
  forall (t:Type) (abm:mem_dom (t+⊥)),
    (forall (e:env) (m m':mem) (ab:t+⊥),
      @gamma _ _ (mem_adom _ abm) ab (e,m) ->
      @gamma _ _ (mem_adom _ abm) ab (e,m')) ->
    forall p s f sp pc e m,
      Reach p (State s f sp pc e m) ->
      match value_analysis _ abm f pc with
        | Bot => False
        | NotBot range =>
          forall x v,
            PTree.get x e = Some v ->
            match v with
              | Vint i
              | Vptr _ i => ints_in_range (range x) i
              | _ => True
  exploit reach_gamma; eauto.
  unfold value_analysis.
  intros G; inv G.
  destruct (range_sound _ abm (solve_pfp t abm f pc) e m MATCH) as
  (r & EQ & HR).
  rewrite EQ.
  intros x v H1.
  destruct v; auto; eapply HR; eauto.