From c7c1bafec40f7824da76e832ec09a628412e29da Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Fri, 16 Oct 2020 12:07:44 +0200 Subject: kill useless moves (not yet connected) --- backend/KillUselessMovesproof.v | 361 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 361 insertions(+) create mode 100644 backend/KillUselessMovesproof.v (limited to 'backend/KillUselessMovesproof.v') 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. -- cgit