Module CFGAnalysis_proof

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).

  Lemma solve_pfp_entrypoint: forall f,
    γ top ⊆ γ (solve_pfp f f.(fn_entrypoint)).

  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 Int.zero ->
      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 Int.zero) 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.

  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'.
  Hint Resolve gamma_sf_insensitive.

  Lemma transf_step_correct:
    forall s1 t s2,
      step ge s1 t s2 -> gamma_state s1 -> gamma_state s2.
  
  Theorem reach_gamma: forall (st:state),
    Reach p st -> gamma_state st.

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
            end
        end.