Module Renumberproof

Postorder renumbering of RTL control-flow graphs.

Require Import Coqlib Maps Postorder.
Require Import AST Linking.
Require Import Values Memory Globalenvs Events Smallstep.
Require Import Op Registers RTL Renumber.

Definition match_prog (p tp: RTL.program) :=
match_program (fun ctx f tf => tf = transf_fundef f) eq p tp.

Lemma transf_program_match:
forall p, match_prog p (transf_program p).

Proof.

intros. eapply match_transform_program; eauto.
Qed.

Section PRESERVATION.
Context `{external_calls_prf: ExternalCalls}.

Variable fn_stack_requirements: ident -> Z.

Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma functions_translated:
  forall v f,
  Genv.find_funct ge v = Some f ->
  Genv.find_funct tge v = Some (transf_fundef f).
Proof (Genv.find_funct_transf TRANSL).

Lemma function_ptr_translated:
  forall v f,
  Genv.find_funct_ptr ge v = Some f ->
  Genv.find_funct_ptr tge v = Some (transf_fundef f).
Proof (Genv.find_funct_ptr_transf TRANSL).

Lemma symbols_preserved:
  forall id,
  Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (Genv.find_symbol_transf TRANSL).

Lemma ros_is_function_translated:
  forall ros rs i,
    ros_is_function ge ros rs i ->
    ros_is_function tge ros rs i.

Proof.

  destruct ros; simpl; intros.
  rewrite symbols_preserved; eauto.
  auto.
Qed.

Lemma senv_preserved:
Senv.equiv ge tge.
Proof (Genv.senv_transf TRANSL).

Lemma genv_next_preserved:
Genv.genv_next tge = Genv.genv_next ge.

Proof.

apply senv_preserved.
Qed.

Lemma sig_preserved:
forall f, funsig (transf_fundef f) = funsig f.

Proof.

destruct f; reflexivity.
Qed.

Lemma find_function_translated:
  forall ros rs fd,
  find_function ge ros rs = Some fd ->
  find_function tge ros rs = Some (transf_fundef fd).

Proof.

  unfold find_function; intros. destruct ros as [r|id].
  eapply functions_translated; eauto.
  rewrite symbols_preserved. destruct (Genv.find_symbol ge id); try congruence.
  eapply function_ptr_translated; eauto.
Qed.

Effect of an injective renaming of nodes on a CFG.

Section RENUMBER.

Variable f: PTree.t positive.

Hypothesis f_inj: forall x1 x2 y, f!x1 = Some y -> f!x2 = Some y -> x1 = x2.

Lemma renum_cfg_nodes:
forall c x y i,
c!x = Some i -> f!x = Some y -> (renum_cfg f c)!y = Some(renum_instr f i).

Proof.

  set (P := fun (c c': code) =>
              forall x y i, c!x = Some i -> f!x = Some y -> c'!y = Some(renum_instr f i)).
  intros c0. change (P c0 (renum_cfg f c0)). unfold renum_cfg.
  apply PTree_Properties.fold_rec; unfold P; intros.
extensionality *)  eapply H0; eauto. rewrite H; auto.
base *)  rewrite PTree.gempty in H; congruence.
induction *)  rewrite PTree.gsspec in H2. unfold renum_node. destruct (peq x k).
  inv H2. rewrite H3. apply PTree.gss.
  destruct f!k as [y'|] eqn:?.
  rewrite PTree.gso. eauto. red; intros; subst y'. elim n. eapply f_inj; eauto.
  eauto.
Qed.

End RENUMBER.

Definition pnum (f: function) := postorder (successors_map f) f.(fn_entrypoint).

Definition reach (f: function) (pc: node) := reachable (successors_map f) f.(fn_entrypoint) pc.

Lemma transf_function_at:
  forall f pc i,
  f.(fn_code)!pc = Some i ->
  reach f pc ->
  (transf_function f).(fn_code)!(renum_pc (pnum f) pc) = Some(renum_instr (pnum f) i).

Proof.

  intros.
  destruct (postorder_correct (successors_map f) f.(fn_entrypoint)) as [A B].
  fold (pnum f) in *.
  unfold renum_pc. destruct (pnum f)! pc as [pc'|] eqn:?.
  simpl. eapply renum_cfg_nodes; eauto.
  elim (B pc); auto. unfold successors_map. rewrite PTree.gmap1. rewrite H. simpl. congruence.
Qed.

Ltac TR_AT :=
  match goal with
  | [ A: (fn_code _)!_ = Some _ , B: reach _ _ |- _ ] =>
        generalize (transf_function_at _ _ _ A B); simpl renum_instr; intros
  end.

Lemma reach_succ:
  forall f pc i s,
  f.(fn_code)!pc = Some i -> In s (successors_instr i) ->
  reach f pc -> reach f s.

Proof.

unfold reach; intros. econstructor; eauto.
unfold successors_map. rewrite PTree.gmap1. rewrite H. auto.
Qed.

Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
  | match_frames_intro: forall res f sp pc rs
        (REACH: reach f pc),
      match_frames (Stackframe res f sp pc rs)
                   (Stackframe res (transf_function f) sp (renum_pc (pnum f) pc) rs).

Inductive match_states: RTL.state -> RTL.state -> Prop :=
  | match_regular_states: forall stk f sp pc rs m stk'
        (STACKS: list_forall2 match_frames stk stk')
        (REACH: reach f pc),
      match_states (State stk f sp pc rs m)
                   (State stk' (transf_function f) sp (renum_pc (pnum f) pc) rs m)
  | match_callstates: forall stk f args m stk' sz
        (STACKS: list_forall2 match_frames stk stk'),
      match_states (Callstate stk f args m sz)
                   (Callstate stk' (transf_fundef f) args m sz)
  | match_returnstates: forall stk v m stk'
        (STACKS: list_forall2 match_frames stk stk'),
      match_states (Returnstate stk v m)
                   (Returnstate stk' v m).

Lemma step_simulation:
  forall S1 t S2, RTL.step fn_stack_requirements ge S1 t S2 ->
  forall S1', match_states S1 S1' ->
  exists S2', RTL.step fn_stack_requirements tge S1' t S2' /\ match_states S2 S2'.

Proof.

  induction 1; intros S1' MS; inv MS; try TR_AT.
nop *)  econstructor; split. eapply exec_Inop; eauto.
  constructor; auto. eapply reach_succ; eauto. simpl; auto.
op *)  econstructor; split.
  eapply exec_Iop; eauto.
  instantiate (1 := v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved.
  constructor; auto. eapply reach_succ; eauto. simpl; auto.
load *)  econstructor; split.
  assert (eval_addressing tge sp addr rs ## args = Some a).
  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
  eapply exec_Iload; eauto.
  constructor; auto. eapply reach_succ; eauto. simpl; auto.
store *)  econstructor; split.
  assert (eval_addressing tge sp addr rs ## args = Some a).
  rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved.
  eapply exec_Istore; eauto.
  constructor; auto. eapply reach_succ; eauto. simpl; auto.
call *)  econstructor; split.
  eapply exec_Icall with (fd0 := transf_fundef fd); eauto.
    eapply ros_is_function_translated; eauto.
    eapply find_function_translated; eauto.
    apply sig_preserved.
  constructor. constructor; auto. constructor. eapply reach_succ; eauto. simpl; auto.
tailcall *)  econstructor; split.
  eapply exec_Itailcall with (fd0 := transf_fundef fd); eauto.
    eapply ros_is_function_translated; eauto.
    eapply find_function_translated; eauto.
    apply sig_preserved.
  constructor. auto.
builtin *)  econstructor; split.
  eapply exec_Ibuiltin; eauto.
    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
  constructor; auto. eapply reach_succ; eauto. simpl; auto.
cond *)  econstructor; split.
  eapply exec_Icond; eauto.
  replace (if b then renum_pc (pnum f) ifso else renum_pc (pnum f) ifnot)
     with (renum_pc (pnum f) (if b then ifso else ifnot)).
  constructor; auto. eapply reach_succ; eauto. simpl. destruct b; auto.
  destruct b; auto.
jumptbl *)  econstructor; split.
  eapply exec_Ijumptable; eauto. rewrite list_nth_z_map. rewrite H1. simpl; eauto.
  constructor; auto. eapply reach_succ; eauto. simpl. eapply list_nth_z_in; eauto.
return *)  econstructor; split.
  eapply exec_Ireturn; eauto.
  constructor; auto.
internal function *)  simpl. econstructor; split.
  eapply exec_function_internal; eauto.
  constructor; auto. unfold reach. constructor.
external function *)  econstructor; split.
  eapply exec_function_external; eauto.
    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
  constructor; auto.
return *)  inv STACKS. inv H2.
  econstructor; split.
  eapply exec_return; eauto.
  constructor; auto.
Qed.

Lemma transf_initial_states:
forall S1, RTL.initial_state fn_stack_requirements prog S1 ->
exists S2, RTL.initial_state fn_stack_requirements tprog S2 /\ match_states S1 S2.

Proof.

  intros. inv H. econstructor; split.
  econstructor.
  eapply (Genv.init_mem_transf TRANSL); eauto.
  rewrite symbols_preserved. rewrite (match_program_main TRANSL). eauto.
  eapply function_ptr_translated; eauto.
  rewrite <- H3; apply sig_preserved.
  eauto. eauto.
  destruct TRANSL as (_ & A & _); rewrite A. constructor. constructor.
Qed.

Lemma transf_final_states:
forall S1 S2 r, match_states S1 S2 -> RTL.final_state S1 r -> RTL.final_state S2 r.

Proof.

intros. inv H0. inv H. inv STACKS. constructor.
Qed.

Theorem transf_program_correct:
forward_simulation (RTL.semantics fn_stack_requirements prog) (RTL.semantics fn_stack_requirements tprog).

Proof.

  eapply forward_simulation_step.
  apply senv_preserved.
  eexact transf_initial_states.
  eexact transf_final_states.
  exact step_simulation.
Qed.

End PRESERVATION.