Module RTLpast

Require Import Coqlib Maps List.
Import ListNotations.
Require Import AST Integers Values Events Memory Globalenvs Smallstep.
Require Import Op Registers.
Require Import RTL.
Require Import Kildall.

Lemma step_state_same_function : forall ge stk f res pc rs m t stk' f' res' pc' rs' m',
    step ge (RTL.State stk f res pc rs m) t (RTL.State stk' f' res' pc' rs' m') ->
    stk' = stk /\ f' = f /\ res' = res.


Definition predecessors f :=
  make_predecessors (fn_code f) successors_instr.

Lemma prev_state_in_preds : forall ge stk f sp pc rs m t stk' f' sp' pc' rs' m',
    step ge (State stk f sp pc rs m) t (State stk' f' sp' pc' rs' m') ->
    In pc ((predecessors f)!!!pc').

Definition predecessors' code :=
  make_predecessors code successors_instr.

Definition is_predecessor code p pc := In p ((predecessors' code)!!!pc).

Definition one_predecessor code pc p :=
  forall p', is_predecessor code p' pc -> p' = p.

Definition two_predecessors code pc p1 p2 :=
  forall p', is_predecessor code p' pc -> p' = p1 \/ p' = p2.


Lemma prev_state_not_callstate : forall ge st t stk' f' sp' pc' rs' m',
    step ge st t (State stk' f' sp' pc' rs' m') ->
    fn_entrypoint f' <> pc' ->
    (forall stk f args m, st <> Callstate stk f args m).

From Coq Require Import Program.

Definition stack (st: state) :=
  match st with
  | State stk _ _ _ _ _
  | Callstate stk _ _ _
  | Returnstate stk _ _ => stk
  end.

Lemma return_has_predecessor_call : forall prog st0 t res f sp pc' rs stk v m,
    initial_state prog st0 ->
    star' step (Genv.globalenv prog) st0 t (Returnstate (Stackframe res f sp pc' rs :: stk) v m) ->
    exists pc sig ros args,
      (fn_code f)!pc = Some (Icall sig ros args res pc').

Ltac falsify_callstate :=
  exfalso;
  match goal with
  | STEP: step _ (RTL.Callstate _ _ _ _) _ _ |- _ =>
      eapply prev_state_not_callstate in STEP; eauto; try extlia; congruence
  end.

Ltac simplify_predecessors :=
  subst; unfold predecessors, predecessors' in *;
  match goal with
  | IN: In _ match ?preds with Some _ => _ | None => [] end |- _ =>
      destruct preds eqn:?PRED; [|inv IN]
  | IN: In _ ?preds, PREDS:(make_predecessors _ _)!?pc = Some _, ONE:one_predecessor _ ?pc _ |- _ =>
      unfold one_predecessor, is_predecessor, predecessors', successors_list in ONE;
      rewrite PREDS in ONE;
      apply ONE in IN; subst
  | IN: In _ ?preds, PREDS:(make_predecessors _ _)!?pc = Some _, TWO:two_predecessors _ ?pc _ _ |- _ =>
      unfold two_predecessors, is_predecessor, predecessors', successors_list in TWO;
      rewrite PREDS in TWO;
      apply TWO in IN; subst
  | H: _ \/ _ |- _ => destruct H; subst; auto
  | EQ1: _ ! ?x = _, EQ2: _ ! ?x = _ |- _ =>
      setoid_rewrite EQ1 in EQ2; inv EQ2
  | EQ: ?pred = Some _, M: context[?pred] |- _ => rewrite EQ in M
  end.

Ltac falsify_returnstate :=
  exfalso;
  repeat
    match goal with
    | STEP: step _ (RTL.Returnstate _ _ _) _ (RTL.State _ _ _ _ _ _) |- _ =>
        inv STEP
    | STEPS: star' _ _ _ _ (RTL.Returnstate _ _ _) |- _ =>
        eapply return_has_predecessor_call in STEPS as (?&?&?&?&CALL); eauto;
        eapply make_predecessors_correct_2 with (successors:=successors_instr) in CALL as PREDS;
        eauto; [|simpl; eauto];
        destruct PREDS as (?&PRED&IN);
        repeat simplify_predecessors; try congruence
    end.

Ltac step_back_simplify :=
  simpl in *;
  match goal with
  | H: extcall_observe_sem _ _ _ _ _ _ |- _ => inv H
  end.

Ltac step_back' :=
  match goal with
  | EQ1: (fn_code _) ! ?x = _, EQ2: (fn_code _) ! ?x = _ |- _ =>
      rewrite EQ1 in EQ2; inv EQ2
  | STEP: step _ (RTL.State _ _ _ _ _ _) _ _ |- _ =>
      apply step_state_same_function in STEP as EQ; destruct EQ as (?&?&?); subst;
      eapply prev_state_in_preds in STEP as PRED; unfold successors_list in PRED;
      repeat simplify_predecessors;
      inv STEP; try congruence
  | STEP: step _ ?st1 _ _ |- _ =>
      destruct st1; [|now falsify_callstate|now falsify_returnstate]
  | STEPS: star' step _ ?st0 _ _, INIT: RTL.initial_state _ ?st0 |- _ =>
      inv STEPS; [now inv INIT|]
  end.

Ltac step_back :=
  rewrite ? star_star' in *; do 4 step_back';
  repeat step_back_simplify.

Definition in_stack st f :=
  match st with
  | Callstate stk (Internal f') _ _
  | State stk f' _ _ _ _ =>
      f' = f \/ exists r v pc rs, In (Stackframe r f v pc rs) stk
  | Callstate stk _ _ _
  | Returnstate stk _ _ =>
      exists r v pc rs, In (Stackframe r f v pc rs) stk
  end.

Lemma steps_has_function : forall prog st0 t st1 f,
    RTL.initial_state prog st0 ->
    star step (Genv.globalenv prog) st0 t st1 ->
    in_stack st1 f ->
    exists ros rs, find_function (Genv.globalenv prog) ros rs = Some (Internal f).