Module RTL_AnalysisLib

Require Import ZArith List Maps Coqlib Lattice.
Require Import AST RTL Registers Op.
Require Import Linking Values Integers Memory Events Globalenvs.
Require Import AnalysisDomain.
Require Kildall MultiFixpoint Liveness.

Module RTL_IRspec <: IRspec.
  Definition function := RTL.function.
  Definition node := RTL.node.
  Definition fn_stacksize := RTL.fn_stacksize.
  Definition fn_params := RTL.fn_params.
  Definition fn_sig := RTL.fn_sig.
  Definition funsig := RTL.funsig.
End RTL_IRspec.

Module RTL_AbstractAnalysis (D : AADomain RTL_IRspec).
  Include D.

  Module DS := MultiFixpoint.Solver(Kildall.NodeSetForward)(D.VA).

Definition transfer_instr (pi : prog_info) (i : instruction) (aa : astate) : list (node * VA.t) :=
  match i with
  | Inop s => (s, Astate aa) :: nil
  | Iop op args res s => (s, transfer_op pi op args res aa) :: nil
  | Iload trap chunk addr args dst s => (s, transfer_load pi trap chunk addr args dst aa) :: nil
  | Istore chunk addr args src s => (s, transfer_store pi chunk addr args src aa) :: nil
  | Icall sig ros args res s => (s, transfer_call pi args res aa) :: nil
  | Itailcall sig ros args => nil
  | Ibuiltin ef args res s => (s, transfer_builtin pi ef args res aa) :: nil
  | Icond cond args s1 s2 _ =>
      let (aa1, aa2) := transfer_condition pi cond args aa in
      (s1, aa1) :: (s2, aa2) :: nil
  | Ijumptable arg tbl =>
      mapi (fun i exit => (exit, transfer_jumpi pi arg (Int.repr i) aa)) tbl
  | Ireturn arg =>
      nil
  | Iassert cond args s =>
      (s, Astate aa)::nil
  end.

Definition forget rl (xx : VA.t) : VA.t :=
  match filter_astate xx with
  | Some yy => Astate (eforget rl yy)
  | None => xx
  end.

Lemma forget_ge: forall rl xx, VA.ge (forget rl xx) xx.
  
Definition transfer0 (pi : prog_info) (f: function) (pc: node) (aa : VA.t) : list (node * VA.t) :=
  match filter_astate aa with
  | None => nil
  | Some aa =>
  match f.(fn_code)!pc with
  | None => nil
  | Some i => transfer_instr pi i aa
  end end.

Definition transfer lu pi f pc aa :=
  let zz := transfer0 pi f pc aa in
  match lu ! pc with
  | Some rl => List.map (fun pp => (fst pp, forget rl (snd pp))) zz
  | None => zz
  end.
  
Definition analyze (pi: prog_info) (f: function): PMap.t D.VA.t :=
  let lu := Liveness.last_uses f in
  match DS.solution_opt (widen_node f) (transfer lu pi f) ((f.(fn_entrypoint), entry_state f) :: nil) with
  | Some solution => solution
  | None => PMap.init default_top
  end.

Module AALemmas := AADomainLemmas(RTL_IRspec)(D).

Section SOUNDNESS.
Import AALemmas.

Section ANALYSIS.

Lemma transfer_strict lu pi f n:
  transfer lu pi f n VA.bot = nil.

Lemma analyze_successor [pi f n i aa n' aa']
  (ANALYZE : (analyze pi f)!!n = Astate aa)
  (AT : f.(fn_code)!n = Some i)
  (IN : In (n', aa') (transfer_instr pi i aa)):
  VA.ge (analyze pi f)!!n' aa'.

Lemma analyze_entrypoint [pi ge gh sp e m f s0]
  (ENTRY: entry_state f = Astate s0)
  (MATCH: asmatch pi ge gh sp e m s0):
  exists s1,
    (analyze pi f)!!(fn_entrypoint f) = Astate s1 /\
    asmatch pi ge gh sp e m s1.

Lemma analyze_succ [pi ge gh sp e m f n s0 i n' s1]
  (ANALYZE : (analyze pi f)!!n = Astate s0)
  (AT : f.(fn_code)!n = Some i)
  (IN : In (n', Astate s1) (transfer_instr pi i s0))
  (MATCH : asmatch pi ge gh sp e m s1):
  exists s2,
     (analyze pi f)!!n' = Astate s2 /\
     asmatch pi ge gh sp e m s2.

End ANALYSIS.

Section STEP.
Variable pi: prog_info.
Variable ge: genv.

Local Notation amatch := (asmatch pi ge).

Inductive sound_stack : ghost_env -> list stackframe -> mem -> block -> Prop :=
  | sound_stack_nil
        gh m bound:
        sound_stack gh nil m bound
  | sound_stack_call
        gh res f sp pc e stk m bound
        (MATCH : forall gh_ce1 m' vres
                   (VRS : valid_returnstate pi ge gh_ce1 m' vres)
                   (SUCC : succ_state pi ge bound gh m gh_ce1 m'),
                 exists aa gh1,
                   (analyze pi f) !! pc = Astate aa /\
                   amatch gh1 sp (e#res <- vres) m' aa /\
                   sound_stack gh1 stk m' sp):
        sound_stack gh (Stackframe res f (Vptr sp Ptrofs.zero) pc e :: stk) m bound.

Inductive sound_state_base (gh : ghost_env) : state -> Prop :=
  | sound_regular_state
        stk f sp pc e m aa
        (STK : sound_stack gh stk m sp)
        (AN : (analyze pi f)!!pc = Astate aa)
        (MATCH : amatch gh sp e m aa):
      sound_state_base gh (State stk f (Vptr sp Ptrofs.zero) pc e m)
  | sound_call_state
        stk fd args m
        (STK : sound_stack gh stk m (Mem.nextblock m))
        (VCS : valid_callstate pi ge gh m args):
      sound_state_base gh (Callstate stk fd args m)
  | sound_return_state
        stk v m bound
        (STK : sound_stack gh stk m bound)
        (VRS : valid_returnstate pi ge gh m v):
      sound_state_base gh (Returnstate stk v m).

Lemma sound_stack_succ_imp [gh gh' stk m m' bound bound']
  (STACK : sound_stack gh stk m bound)
  (IMP : forall gh1 m1, succ_state pi ge bound' gh' m' gh1 m1 -> succ_state pi ge bound gh m gh1 m1):
  sound_stack gh' stk m' bound'.

Lemma sound_stack_succ [gh gh' stk m m' bound]
  (SUCC : succ_state pi ge bound gh m gh' m')
  (STACK : sound_stack gh stk m bound):
  sound_stack gh' stk m' bound.


Lemma sound_succ_state gh pc s0 i s1 stk f sp pc' e' m'
  (ANALYZE : (analyze pi f)!!pc = Astate s0)
  (AT : f.(fn_code)!pc = Some i)
  (IN : In (pc', Astate s1) (transfer_instr pi i s0))
  (MATCH : amatch gh sp e' m' s1)
  (STACK : sound_stack gh stk m' sp):
  sound_state_base gh (State stk f (Vptr sp Ptrofs.zero) pc' e' m').

Theorem sound_step_base st t st' gh
  (STEP: RTL.step ge st t st')
  (SOUND: sound_state_base gh st):
  exists gh', sound_state_base gh' st'.

End STEP.

Section PROGRAM.
Variable prog: program.
Let ge := Genv.globalenv prog.

Inductive sound_state (st : state) : Prop :=
  | sound_state_intro
      (SOUND: forall cunit, linkorder cunit prog -> exists gh, sound_state_base (get_prog_info cunit) ge gh st).

Remark sound_state_inv st cunit:
  sound_state st -> linkorder cunit prog -> exists bc, sound_state_base (get_prog_info cunit) ge bc st.

Theorem sound_initial st
  (INIT : initial_state prog st):
  sound_state st.

Theorem sound_step st t st'
  (STEP : RTL.step ge st t st')
  (SOUND : sound_state st):
  sound_state st'.

End PROGRAM.

End SOUNDNESS.

End RTL_AbstractAnalysis.