Correctness proof for CFG generation.

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Smallstep.
Require Import Globalenvs.
Require Import Switch.
Require Import Cminor.
Require Import CFG.
Require Import CFGgen.
Require Import CFGgenspec.

The simulation argument

Require Import Errors.

Section CORRECTNESS.

Variable prog: Cminor.program.
Variable tprog: CFG.program.
Hypothesis TRANSL: transl_program prog = OK tprog.

Let ge : Cminor.genv := Genv.globalenv prog.
Let tge : CFG.genv := Genv.globalenv tprog.

Relationship between the global environments for the original Cminor program and the generated CFG program.

Lemma symbols_preserved:
  forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
Proof
  (Genv.find_symbol_transf_partial transl_fundef _ TRANSL).

Lemma function_ptr_translated:
  forall (b: block) (f: Cminor.fundef),
  Genv.find_funct_ptr ge b = Some f ->
  exists tf,
  Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
Proof
  (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL).

Lemma functions_translated:
  forall (v: val) (f: Cminor.fundef),
  Genv.find_funct ge v = Some f ->
  exists tf,
  Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
Proof
  (Genv.find_funct_transf_partial transl_fundef _ TRANSL).

Lemma functions_translated_back:
  forall (v: val) (tf: CFG.fundef),
  Genv.find_funct tge v = Some tf ->
  exists f,
  Genv.find_funct ge v = Some f /\ transl_fundef f = OK tf.
Proof
  (Genv.find_funct_rev_transf_partial transl_fundef _ TRANSL).

Lemma sig_transl_function:
  forall (f: Cminor.fundef) (tf: CFG.fundef),
  transl_fundef f = OK tf ->
  CFG.funsig tf = Cminor.funsig f.

Proof.

  intros until tf. unfold transl_fundef, transf_partial_fundef.
  case f; intro.
  unfold transl_function.
  destruct (reserve_labels (fn_body f0) (PTree.empty node, init_state)) as [ngoto s0].
  case (transl_fun f0 ngoto s0); simpl; intros.
  discriminate.
  simpl in H. inversion H. reflexivity.
  intro. inversion H. reflexivity.
Qed.

Lemma varinfo_preserved:
  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
Proof
  (Genv.find_var_info_transf_partial transl_fundef _ TRANSL).

Lemma eval_expr_preserved:
  forall sp e m a v,
    eval_expr ge sp e m a v -> eval_expr tge sp e m a v.

Proof.

induction 1; econstructor; eauto.
destruct cst; auto. simpl. rewrite symbols_preserved. auto.
Qed.

Lemma eval_expr_preserved_back:
forall sp e m a v,
eval_expr tge sp e m a v -> eval_expr ge sp e m a v.

Proof.

induction 1; econstructor; eauto.
destruct cst; auto. simpl. rewrite <- symbols_preserved. auto.
Qed.

Lemma eval_exprlist_preserved:
forall sp el m a vl,
eval_exprlist ge sp el m a vl -> eval_exprlist tge sp el m a vl.

Proof.

  induction 1; econstructor.
  apply eval_expr_preserved. auto.
  auto.
Qed.

Lemma eval_exprlist_preserved_back:
forall sp el m a vl,
eval_exprlist tge sp el m a vl -> eval_exprlist ge sp el m a vl.

Proof.

  induction 1; econstructor.
  apply eval_expr_preserved_back. auto.
  auto.
Qed.

Measure over Cminor states

Open Local Scope nat_scope.

Fixpoint size_stmt (s: stmt) : nat :=
  match s with
  | Sskip => 0
  | Sseq s1 s2 => (size_stmt s1 + size_stmt s2 + 1)
  | Sifthenelse e s1 s2 => (size_stmt s1 + size_stmt s2 + 1)
  | Sloop s1 => (size_stmt s1 + 1)
  | Sblock s1 => (size_stmt s1 + 1)
  | Sexit n => 0
  | Slabel lbl s1 => (size_stmt s1 + 1)
  | _ => 1
  end.

Fixpoint size_cont (k: cont) : nat :=
  match k with
  | Kseq s k1 => (size_stmt s + size_cont k1 + 1)
  | Kblock k1 => (size_cont k1 + 1)
  | _ => 0%nat
  end.

Definition measure_state (S: Cminor.state) :=
  match S with
  | Cminor.State _ s k _ _ _ => (size_stmt s + size_cont k, size_stmt s)
  | _ => (0, 0)
  end.

Definition lt_state (S1 S2: Cminor.state) :=
  lex_ord lt lt (measure_state S1) (measure_state S2).

Lemma lt_state_intro:
  forall f1 s1 k1 sp1 e1 m1 f2 s2 k2 sp2 e2 m2,
  size_stmt s1 + size_cont k1 < size_stmt s2 + size_cont k2
  \/ (size_stmt s1 + size_cont k1 = size_stmt s2 + size_cont k2
      /\ size_stmt s1 < size_stmt s2) ->
  lt_state (Cminor.State f1 s1 k1 sp1 e1 m1)
           (Cminor.State f2 s2 k2 sp2 e2 m2).

Proof.

  intros. unfold lt_state. simpl. destruct H as [A | [A B]].
  left. auto.
  rewrite A. right. auto.
Qed.

Ltac Lt_state :=
apply lt_state_intro; simpl; try omega.

Require Import Wellfounded.

Lemma lt_state_wf:
well_founded lt_state.

Proof.

unfold lt_state. apply wf_inverse_image with (f := measure_state).
apply wf_lex_ord. apply lt_wf. apply lt_wf.
Qed.

Auxiliary lemma about the translation of switches.

Lemma transl_switch_target:
  forall nexits cases ncases default ndefault n,
    tr_cases nexits cases ncases ->
    nth_error nexits default = Some ndefault ->
    nth_error nexits (switch_target n default cases) =
    Some (switch_target n ndefault ncases).

Proof.

  induction 1.
  eauto.
  intro. destruct x, y, H. simpl in H, H2. subst.
  simpl. destruct (Int.eq n i0); auto.
Qed.

Semantic preservation for the translation of statements

The simulation diagram for the translation of statements and functions is a "star" diagram of the form:

           I                         I
     S1 ------- R1             S1 ------- R1
     |          |              |          |
   t |        + | t      or  t |        * | t    and |S2| < |S1|
     v          v              v          |
     S2 ------- R2             S2 ------- R2
           I                         I

where I is the match_states predicate defined below. It includes:

Agreement between the Cminor statement under consideration and the current program point in the CFG control-flow graph, as captured by the tr_stmt predicate.
Agreement between the Cminor continuation and the CFG control-flow graph and call stack, as captured by the tr_cont predicate below.
Agreement between Cminor environments and CFG register environments, as captured by match_envs.

Inductive tr_fun (tf: CFG.function) (f: Cminor.function) (ngoto: labelmap) : Prop :=
  | tr_fun_intro: forall nentry nret,
      tr_stmt tf.(fn_code) f.(fn_body) nentry nret nil ngoto ->
      tf.(fn_stacksize) = f.(fn_stackspace) ->
      tf.(fn_code)!nret = Some(Ireturn None) ->
      (forall lbl n, ngoto!lbl = Some n ->
       forall k, exists stmt, exists k',
       find_label lbl f.(Cminor.fn_body) k = Some (stmt, k')) ->
      tr_fun tf f ngoto.

Inductive tr_cont: CFG.code ->
                   Cminor.cont -> node -> list node -> labelmap ->
                   list CFG.stackframe -> Prop :=
  | tr_Kseq: forall c s k nd nexits ngoto cs n,
      tr_stmt c s nd n nexits ngoto ->
      tr_cont c k n nexits ngoto cs ->
      tr_cont c (Kseq s k) nd nexits ngoto cs
  | tr_Kblock: forall c k nd nexits ngoto cs,
      tr_cont c k nd nexits ngoto cs ->
      tr_cont c (Kblock k) nd (nd :: nexits) ngoto cs
  | tr_Kstop: forall c nd ngoto cs,
      c!nd = Some(Ireturn None) ->
      match_stacks Kstop cs ->
      tr_cont c Kstop nd nil ngoto cs
  | tr_Kcall: forall c nd optid f sp e k ngoto cs,
      c!nd = Some(Ireturn None) ->
      match_stacks (Kcall optid f sp e k) cs ->
      tr_cont c (Kcall optid f sp e k) nd nil ngoto cs

with match_stacks: Cminor.cont -> list CFG.stackframe -> Prop :=
  | match_stacks_stop:
      match_stacks Kstop nil
  | match_stacks_call: forall optid f sp e k tf n cs nexits ngoto,
      tr_fun tf f ngoto ->
      tr_cont tf.(fn_code) k n nexits ngoto cs ->
      match_stacks (Kcall optid f sp e k) (Stackframe optid tf sp n e :: cs).

Inductive match_states: Cminor.state -> CFG.state -> Prop :=
  | match_state:
      forall f s k sp e m cs tf ns ncont nexits ngoto
        (TS: tr_stmt tf.(fn_code) s ns ncont nexits ngoto)
        (TF: tr_fun tf f ngoto)
        (TK: tr_cont tf.(fn_code) k ncont nexits ngoto cs),
      match_states (Cminor.State f s k sp e m)
                   (CFG.State cs tf sp ns e m)
  | match_callstate:
      forall f args k m cs tf
        (TF: transl_fundef f = OK tf)
        (MS: match_stacks k cs),
      match_states (Cminor.Callstate f args k m)
                   (CFG.Callstate cs tf args m)
  | match_returnstate:
      forall v k m cs
        (MS: match_stacks k cs),
      match_states (Cminor.Returnstate v k m)
                   (CFG.Returnstate cs v m).

Lemma match_stacks_call_cont:
  forall c k ncont nexits ngoto cs,
  tr_cont c k ncont nexits ngoto cs ->
  match_stacks (call_cont k) cs.

Proof.

induction 1; simpl; auto.
Qed.

Lemma tr_cont_call_cont:
  forall c k ncont nexits ngoto cs nret,
    tr_cont c k ncont nexits ngoto cs ->
    c!nret = Some(Ireturn None) ->
    tr_cont c (call_cont k) nret nil ngoto cs.

Proof.

induction 1; simpl; eauto; econstructor; eauto.
Qed.

Lemma tr_find_label:
  forall c lbl n (ngoto: labelmap) s' k' cs,
  ngoto!lbl = Some n ->
  forall s k ns1 nd1 nexits1,
  find_label lbl s k = Some (s', k') ->
  tr_stmt c s ns1 nd1 nexits1 ngoto ->
  tr_cont c k nd1 nexits1 ngoto cs ->
  exists ns2, exists nd2, exists nexits2,
     c!n = Some(Iskip ns2)
  /\ tr_stmt c s' ns2 nd2 nexits2 ngoto
  /\ tr_cont c k' nd2 nexits2 ngoto cs.

Proof.

  induction s; intros until nexits1; simpl; try congruence.
  caseEq (find_label lbl s1 (Kseq s2 k)); intros.
  inv H1. inv H2. eapply IHs1; eauto. econstructor; eauto.
  inv H2. eapply IHs2; eauto.
  caseEq (find_label lbl s1 k); intros.
  inv H1. inv H2. eapply IHs1; eauto.
  inv H2. eapply IHs2; eauto.
  intros. inversion H1; subst.
  eapply IHs; eauto. econstructor; eauto. econstructor; eauto.
  intros. inv H1.
  eapply IHs; eauto. econstructor; eauto.
  destruct (ident_eq lbl l); intros.
  inv H0. inv H1.
  assert (n0 = n). change positive with node in H4. congruence. subst n0.
  exists ns1; exists nd1; exists nexits1; auto.
  inv H1. eapply IHs; eauto.
Qed.

Theorem transl_step_correct:
  forall S1 t S2, Cminor.step ge S1 t S2 ->
  forall R1, match_states S1 R1 ->
  exists R2,
  (plus CFG.step tge R1 t R2 \/ (star CFG.step tge R1 t R2 /\ lt_state S2 S1))
  /\ match_states S2 R2.

Proof.

  induction 1; intros R1 MSTATE; inv MSTATE.

  inv TS. inv TK. econstructor; split.
  right; split. apply star_refl. Lt_state.
  econstructor; eauto.

  inv TS. inv TK. econstructor; split.
  right; split. apply star_refl. Lt_state.
  econstructor; eauto. constructor.

  inv TS.
  assert ((fn_code tf)!ncont = Some(Ireturn None)
          /\ match_stacks k cs).
    inv TK; simpl in H; try contradiction; auto.
  assert (fn_stacksize tf = fn_stackspace f).
     inv TF. auto.
  destruct H1.
  econstructor; split.
  left; apply plus_one. apply step_return_0. eauto.
  rewrite H2. eauto.
  constructor; auto.

  inv TS.
  econstructor; split.
  left; apply plus_one. eapply step_assign. eauto.
  apply eval_expr_preserved. eauto.
  econstructor; eauto. constructor.

  inv TS.
  econstructor; split.
  left; apply plus_one. eapply step_store; eauto.
  apply eval_expr_preserved. eauto.
  apply eval_expr_preserved. eauto.
  econstructor; eauto. constructor.

  inv TS.
  exploit functions_translated. eauto.
  intros [tf0 [A B]].
  econstructor; split.
  left; apply plus_one. eapply step_call; eauto.
  apply eval_expr_preserved. eauto.
  apply eval_exprlist_preserved. eauto.
  apply sig_transl_function. auto.
  econstructor; eauto. econstructor; eauto.

  inv TS.
  exploit functions_translated. eauto.
  intros [tf0 [A B]].
  econstructor; split.
  left; apply plus_one. eapply step_tailcall; eauto.
  apply eval_expr_preserved. eauto.
  apply eval_exprlist_preserved. eauto.
  apply sig_transl_function. auto.
  inv TF. rewrite H4. eauto.
  econstructor; eauto.
  eapply match_stacks_call_cont; eauto.

  inv TS.
  econstructor; split.
  left. eapply plus_one. eapply step_builtin. eauto.
  apply eval_exprlist_preserved; eauto.
  eapply external_call_symbols_preserved; eauto.
  exact symbols_preserved. exact varinfo_preserved.
  econstructor; eauto. constructor.

  inv TS.
  econstructor; split.
  right; split. apply star_refl. Lt_state.
  econstructor; eauto. econstructor; eauto.

  inv TS.
  econstructor; split.
  left. eapply plus_one. eapply step_ifthenelse; eauto.
  apply eval_expr_preserved. eauto.
  econstructor; eauto. destruct b; eauto.

  inversion TS; subst.
  econstructor; split.
  left. apply plus_one. eapply step_skip; eauto.
  econstructor; eauto.
  econstructor; eauto.
  econstructor; eauto.

  inv TS.
  econstructor; split.
  right; split. apply star_refl. Lt_state.
  econstructor; eauto. econstructor; eauto.

  inv TS. inv TK.
  econstructor; split.
  right; split. apply star_refl. Lt_state.
  econstructor; eauto. econstructor; eauto.

  inv TS. inv TK. simpl in H0. inv H0.
  econstructor; split.
  right; split. apply star_refl. Lt_state.
  econstructor; eauto. econstructor; eauto.

  inv TS. inv TK. simpl in H0.
  econstructor; split.
  right; split. apply star_refl. Lt_state.
  econstructor; eauto. econstructor; eauto.

  inv TS.
  econstructor; split.
  left. eapply plus_one. eapply step_switch. eauto.
  apply eval_expr_preserved. eauto.
  reflexivity.
  econstructor; eauto.
  constructor. apply transl_switch_target; auto.

  inv TS.
  econstructor; split.
  left; apply plus_one. eapply step_return_0. eauto.
  destruct TF. rewrite H2. eauto.
  constructor. eapply match_stacks_call_cont; eauto.

  inv TS.
  econstructor; split.
  left; apply plus_one. eapply step_return_1. eauto.
  apply eval_expr_preserved. eauto.
  destruct TF. rewrite H3. eauto.
  constructor. eapply match_stacks_call_cont; eauto.

  inv TS.
  econstructor; split.
  right; split. apply star_refl. Lt_state.
  econstructor; eauto.

  inv TS. inversion TF; subst.
  exploit tr_find_label; eauto.
  eapply tr_cont_call_cont; eauto.
  intros [ns2 [nd2 [nexits2 [A [B C]]]]].
  econstructor; split.
  left; apply plus_one. eapply step_skip; eauto.
  econstructor; eauto.

  monadInv TF. exploit transl_function_charact; eauto. intro TRF.
  inversion TRF. subst f0.
  econstructor; split.
  left; apply plus_one. eapply step_function_internal; simpl; eauto.
  simpl. econstructor; eauto.
  econstructor; eauto.
  inversion MS; subst; econstructor; eauto.

  monadInv TF.
  econstructor; split.
  left; apply plus_one. eapply step_function_external; eauto.
  eapply external_call_symbols_preserved; eauto.
  exact symbols_preserved. exact varinfo_preserved.
  constructor; auto.

  inv MS.
  econstructor; split.
  left; apply plus_one; constructor.
  econstructor; eauto. constructor.
Qed.

Lemma transl_initial_states:
forall S, Cminor.initial_state prog S ->
exists R, CFG.initial_state tprog R /\ match_states S R.

Proof.

  induction 1.
  exploit function_ptr_translated; eauto. intros [tf [A B]].
  econstructor; split.
  econstructor. apply (Genv.init_mem_transf_partial _ _ TRANSL); eauto.
  rewrite (transform_partial_program_main _ _ TRANSL). fold tge.
  rewrite symbols_preserved. eauto.
  eexact A.
  rewrite <- H2. apply sig_transl_function; auto.
  constructor. auto. constructor.
Qed.

Lemma transl_final_states:
forall S R r,
match_states S R -> Cminor.final_state S r -> CFG.final_state R r.

Proof.

intros. inv H0. inv H. inv MS. constructor.
Qed.

Theorem transf_program_correct:
forward_simulation (Cminor.semantics prog) (CFG.semantics tprog).

Proof.

  eapply forward_simulation_star_wf with (order := lt_state).
  eexact symbols_preserved.
  eexact transl_initial_states.
  eexact transl_final_states.
  apply lt_state_wf.
  exact transl_step_correct.
Qed.

Theorem transl_step_preserves_stuck:
  forall R1 t R2, CFG.step tge R1 t R2 ->
  forall S1, match_states S1 R1 ->
  exists S2, exists t', Cminor.step ge S1 t' S2.

Proof.

  intros R1 t R2 STEP S1 MSTATE.
  destruct MSTATE.
  inv TS.

  inv TK.
  eexists; eexists. constructor.
  eexists; eexists. constructor.
  inv STEP; try congruence.
  eexists; eexists. constructor.
  simpl; eauto.
  inv TF. rewrite <- H2. eauto.
  inv STEP; try congruence.
  eexists; eexists. constructor.
  simpl; eauto.
  inv TF. rewrite <- H2. eauto.

  inv STEP; try congruence.
  rewrite H8 in H. inv H.
  eexists; eexists. constructor.
  apply eval_expr_preserved_back. eauto.

  inv STEP; try congruence.
  rewrite H8 in H. inv H.
  eexists; eexists.
  econstructor; eauto; apply eval_expr_preserved_back; eauto.

  inv STEP; try congruence.
  rewrite H8 in H. inv H.
  exploit functions_translated_back; eauto. intros [f0 [A B]].
  eexists; eexists. econstructor.
  apply eval_expr_preserved_back; eauto.
  apply eval_exprlist_preserved_back; eauto.
  eauto.
  erewrite <- sig_transl_function; eauto.

  inv STEP; try congruence.
  rewrite H6 in H. inv H.
  exploit functions_translated_back; eauto. intros [f0 [A B]].
  eexists; eexists. econstructor.
  apply eval_expr_preserved_back; eauto.
  apply eval_exprlist_preserved_back; eauto.
  eauto.
  erewrite <- sig_transl_function; eauto.
  inv TF. rewrite <- H0. eauto.

  inv STEP; try congruence.
  rewrite H8 in H. inv H.
  eexists; eexists. econstructor.
  apply eval_exprlist_preserved_back; eauto.
  eapply external_call_symbols_preserved. eauto.
  symmetry. apply symbols_preserved.
  symmetry. apply varinfo_preserved.

  eexists; eexists. econstructor.

  inv STEP; try congruence.
  rewrite H10 in H1. inv H1.
  eexists; eexists. eapply Cminor.step_ifthenelse with (b:=b).
  apply eval_expr_preserved_back. eauto.
  eauto.

  eexists; eexists. econstructor.

  eexists; eexists. econstructor.

  inv TK.
  eexists; eexists. econstructor.
  destruct n; eexists; eexists; econstructor.
  destruct n; discriminate.
  destruct n; discriminate.

  inv STEP; try congruence.
  rewrite H10 in H1. inv H1.
  eexists; eexists. econstructor.
  apply eval_expr_preserved_back. eauto.

  inv STEP; try congruence.
  rewrite H8 in H. inv H.
  eexists; eexists. econstructor.
  inv TF. rewrite <- H0. eauto.
  rewrite H8 in H. inv H.
  eexists; eexists. econstructor.
  apply eval_expr_preserved_back. eauto.
  inv TF. rewrite <- H0. eauto.

  eexists; eexists. econstructor.

  inv TF.
  edestruct H3 as [stmt' [k' A]]; eauto.
  eexists; eexists. econstructor. eauto.

  inv STEP.
  destruct f.
  monadInv TF. exploit transl_function_charact; eauto.
  intro TRF. inv TRF. simpl in H5.
  eexists; eexists. econstructor; eauto.
  discriminate.
  destruct f. monadInv TF.
  inv TF.
  eexists; eexists. econstructor.
  eapply external_call_symbols_preserved. eauto.
  symmetry. apply symbols_preserved.
  symmetry. apply varinfo_preserved.

  destruct MS. inv STEP.
  eexists; eexists. econstructor; eauto.
Qed.

Theorem transf_program_preserve_wrong:
  forall s1, Nostep (Cminor.semantics prog) s1 ->
             (forall r, ~Cminor.final_state s1 r) ->
  forall s2, match_states s1 s2 ->
             Nostep (CFG.semantics tprog) s2 /\
             (forall r, ~CFG.final_state s2 r).

Proof.

  split.
  intros t s' S.
  exploit transl_step_preserves_stuck; eauto. intros [S2 [t' STEP]].
  exploit H; eauto.

  intro. specialize (H0 r). contradict H0.
  destruct H0.
  inv H1. inv MS. constructor.
Qed.

End CORRECTNESS.

Module CFGgenproof

The simulation argument

Measure over Cminor states

Auxiliary lemma about the translation of switches.

Semantic preservation for the translation of statements