kill useless moves (not yet connected)

1 files changed, 361 insertions, 0 deletions

diff --git a/backend/KillUselessMovesproof.v b/backend/KillUselessMovesproof.v
new file mode 100644
index 00000000..629aa6aa
--- /dev/null
+++ b/backend/KillUselessMovesproof.v
@@ -0,0 +1,361 @@
+(* *************************************************************)
+(*                                                             *)
+(*             The Compcert verified compiler                  *)
+(*                                                             *)
+(*           David Monniaux     CNRS, VERIMAG                  *)
+(*                                                             *)
+(*  Copyright VERIMAG. All rights reserved.                    *)
+(*  This file is distributed under the terms of the INRIA      *)
+(*  Non-Commercial License Agreement.                          *)
+(*                                                             *)
+(* *************************************************************)
+
+Require Import Axioms.
+Require Import FunInd.
+Require Import Coqlib Maps Errors Integers Floats Lattice Kildall.
+Require Import AST Linking.
+Require Import Values Memory Globalenvs Events Smallstep.
+Require Import Registers Op RTL.
+Require Import KillUselessMoves.
+
+
+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.
+
+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 senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_transf TRANSL).
+
+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.
+
+Lemma transf_function_at:
+  forall f pc i,
+  f.(fn_code)!pc = Some i ->
+  (transf_function f).(fn_code)!pc = Some(transf_instr pc i).
+Proof.
+  intros until i. intro Hcode.
+  unfold transf_function; simpl.
+  rewrite PTree.gmap.
+  unfold option_map.
+  rewrite Hcode.
+  reflexivity.
+Qed.
+
+Ltac TR_AT :=
+  match goal with
+  | [ A: (fn_code _)!_ = Some _ |- _ ] =>
+        generalize (transf_function_at _ _ _ A); intros
+  end.
+
+Section SAME_RS.
+  Context {A : Type}.
+  
+  Definition same_rs (rs rs' : Regmap.t A) :=
+    forall x, rs # x = rs' # x.
+
+  Lemma same_rs_refl : forall rs, same_rs rs rs.
+  Proof.
+    unfold same_rs.
+    reflexivity.
+  Qed.
+
+  Lemma same_rs_comm : forall rs rs', (same_rs rs rs') -> (same_rs rs' rs).
+  Proof.
+    unfold same_rs.
+    congruence.
+  Qed.
+
+  Lemma same_rs_trans : forall rs1 rs2 rs3,
+      (same_rs rs1 rs2) -> (same_rs rs2 rs3) -> (same_rs rs1 rs3).
+  Proof.
+    unfold same_rs.
+    congruence.
+  Qed.
+
+  Lemma same_rs_idem_write : forall rs r,
+      (same_rs rs (rs # r <- (rs # r))).
+  Proof.
+    unfold same_rs.
+    intros.
+    rewrite Regmap.gsident.
+    reflexivity.
+  Qed.
+
+  Lemma same_rs_read:
+    forall rs rs' r, (same_rs rs rs') -> rs # r = rs' # r.
+  Proof.
+    unfold same_rs.
+    auto.
+  Qed.
+  
+  Lemma same_rs_subst:
+    forall rs rs' l, (same_rs rs rs') -> rs ## l = rs' ## l.
+  Proof.
+    induction l; cbn; intuition congruence.
+  Qed.
+
+  Lemma same_rs_write: forall rs rs' r x,
+      (same_rs rs rs') -> (same_rs (rs # r <- x) (rs' # r <- x)).
+  Proof.
+    unfold same_rs.
+    intros.
+    destruct (peq r x0).
+    { subst x0.
+      rewrite Regmap.gss. rewrite Regmap.gss.
+      reflexivity.
+    }
+    rewrite Regmap.gso by congruence.
+    rewrite Regmap.gso by congruence.
+    auto.
+  Qed.
+
+  Lemma same_rs_setres:
+    forall rs rs' (SAME: same_rs rs rs') res vres,
+      same_rs (regmap_setres res vres rs) (regmap_setres res vres rs').
+  Proof.
+    induction res; cbn; auto using same_rs_write.
+  Qed.
+End SAME_RS.
+
+Lemma same_find_function: forall tge rs rs' (SAME: same_rs rs rs') ros,
+  find_function tge ros rs = find_function tge ros rs'.
+Proof.
+  destruct ros; cbn.
+  { rewrite (same_rs_read rs rs' r SAME).
+    reflexivity. }
+  reflexivity.
+Qed.
+
+Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop :=
+| match_frames_intro: forall res f sp pc rs rs' (SAME : same_rs rs rs'),
+    match_frames (Stackframe res f sp pc rs)
+                 (Stackframe res (transf_function f) sp pc rs').
+
+Inductive match_states: RTL.state -> RTL.state -> Prop :=
+  | match_regular_states: forall stk f sp pc rs rs' m stk'
+        (SAME: same_rs rs rs')
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (State stk f sp pc rs m)
+                   (State stk' (transf_function f) sp pc rs' m)
+  | match_callstates: forall stk f args m stk'
+        (STACKS: list_forall2 match_frames stk stk'),
+      match_states (Callstate stk f args m)
+                   (Callstate stk' (transf_fundef f) args m)
+  | 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 ge S1 t S2 ->
+  forall S1', match_states S1 S1' ->
+  exists S2', RTL.step 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.
+- (* op *)
+  cbn in H1.
+  destruct (_ && _) eqn:IS_MOVE in H1.
+  {
+    destruct eq_operation in IS_MOVE. 2: discriminate.
+    destruct list_eq_dec in IS_MOVE. 2: discriminate.
+    subst op. subst args.
+    clear IS_MOVE.
+    cbn in H0.
+    inv H0.
+    econstructor; split.
+    { eapply exec_Inop; eauto. }
+    constructor.
+    2: assumption.
+    eapply same_rs_trans.
+    { apply same_rs_comm.
+      apply same_rs_idem_write.
+    }
+    assumption.
+  }
+  econstructor; split.
+  eapply exec_Iop with (v := v); eauto.
+  rewrite <- H0.
+  rewrite (same_rs_subst rs rs' args SAME).
+  apply eval_operation_preserved. exact symbols_preserved.
+  constructor; auto using same_rs_write.
+(* load *)
+- econstructor; split.
+  assert (eval_addressing tge sp addr rs' ## args = Some a).
+  { rewrite <- H0.
+    rewrite (same_rs_subst rs rs' args SAME).
+    apply eval_addressing_preserved. exact symbols_preserved.
+  }
+  eapply exec_Iload; eauto.
+  constructor; auto using same_rs_write.
+- (* load notrap1 *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs' ## args = None).
+  { rewrite <- H0.
+    rewrite (same_rs_subst rs rs' args SAME).
+    apply eval_addressing_preserved. exact symbols_preserved.
+  }
+  eapply exec_Iload_notrap1; eauto.
+  constructor; auto using same_rs_write.
+- (* load notrap2 *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs' ## args = Some a).
+  { rewrite <- H0.
+    rewrite (same_rs_subst rs rs' args SAME).
+    apply eval_addressing_preserved. exact symbols_preserved.
+  }
+  eapply exec_Iload_notrap2; eauto.
+  constructor; auto using same_rs_write. 
+- (* store *)
+  econstructor; split.
+  assert (eval_addressing tge sp addr rs' ## args = Some a).
+  { rewrite <- H0.
+    rewrite (same_rs_subst rs rs' args SAME).
+    apply eval_addressing_preserved. exact symbols_preserved.
+  }
+  rewrite (same_rs_read rs rs' src SAME) in H1.
+  eapply exec_Istore; eauto.
+  constructor; auto.
+(* call *)
+- econstructor; split.
+  eapply exec_Icall with (fd := transf_fundef fd); eauto.
+  eapply find_function_translated; eauto.
+  { rewrite <- (same_find_function ge rs rs') by assumption.
+    assumption. }
+  apply sig_preserved.
+  rewrite (same_rs_subst rs rs' args SAME).  
+  constructor. constructor; auto. constructor; auto.
+(* tailcall *)
+- econstructor; split.
+  eapply exec_Itailcall with (fd := transf_fundef fd); eauto.
+    eapply find_function_translated; eauto.
+  { rewrite <- (same_find_function ge rs rs') by assumption.
+    assumption. }
+    apply sig_preserved.
+  rewrite (same_rs_subst rs rs' args SAME).  
+  constructor. auto.
+(* builtin *)
+- econstructor; split.
+  eapply exec_Ibuiltin; eauto.
+  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  {
+    replace (fun r : positive => rs' # r) with (fun r : positive => rs # r).
+    eassumption.
+    apply functional_extensionality.
+    auto using same_rs_read.
+  }
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  constructor; auto.
+  auto using same_rs_setres.
+(* cond *)
+- econstructor; split.
+  eapply exec_Icond; eauto.
+  rewrite <- (same_rs_subst rs rs' args SAME); eassumption.
+  constructor; auto.
+(* jumptbl *)
+- econstructor; split.
+  eapply exec_Ijumptable; eauto.
+  rewrite <- (same_rs_read rs rs' arg SAME); eassumption.
+  constructor; auto.
+(* return *)
+- econstructor; split.
+  eapply exec_Ireturn; eauto.
+  destruct or; cbn.
+  + rewrite <- (same_rs_read rs rs' r SAME) by auto.
+    constructor; auto.
+  + constructor; auto.
+(* internal function *)
+-  simpl. econstructor; split.
+  eapply exec_function_internal; eauto.
+  constructor; auto.
+  cbn.
+  apply same_rs_refl.
+(* external function *)
+- econstructor; split.
+  eapply exec_function_external; eauto.
+    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  constructor; auto.
+(* return *)
+- inv STACKS. inv H1.
+  econstructor; split.
+  eapply exec_return; eauto.
+  constructor; auto using same_rs_write.
+Qed.
+
+Lemma transf_initial_states:
+  forall S1, RTL.initial_state prog S1 ->
+  exists S2, RTL.initial_state 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.
+  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 prog) (RTL.semantics tprog).
+Proof.
+  eapply forward_simulation_step.
+  apply senv_preserved.
+  eexact transf_initial_states.
+  eexact transf_final_states.
+  exact step_simulation.
+Qed.
+
+End PRESERVATION.