From a8fc4625c2c172484341b9105c1aa8ea1c6a49f3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 17 Aug 2009 15:28:52 +0000 Subject: Refactoring of Constprop and Constpropproof into a machine-dependent part and a machine-independent part. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1126 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Constpropproof.v | 445 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 445 insertions(+) create mode 100644 backend/Constpropproof.v (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v new file mode 100644 index 00000000..e628d426 --- /dev/null +++ b/backend/Constpropproof.v @@ -0,0 +1,445 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(** Correctness proof for constant propagation. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Events. +Require Import Mem. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Op. +Require Import Registers. +Require Import RTL. +Require Import Lattice. +Require Import Kildall. +Require Import ConstpropOp. +Require Import Constprop. +Require Import ConstpropOpproof. + +(** * Correctness of the static analysis *) + +Section ANALYSIS. + +Variable ge: genv. + +Definition regs_match_approx (a: D.t) (rs: regset) : Prop := + forall r, val_match_approx ge (D.get r a) rs#r. + +Lemma regs_match_approx_top: + forall rs, regs_match_approx D.top rs. +Proof. + intros. red; intros. simpl. rewrite PTree.gempty. + unfold Approx.top, val_match_approx. auto. +Qed. + +Lemma regs_match_approx_increasing: + forall a1 a2 rs, + D.ge a1 a2 -> regs_match_approx a2 rs -> regs_match_approx a1 rs. +Proof. + unfold D.ge, regs_match_approx. intros. + apply val_match_approx_increasing with (D.get r a2); auto. +Qed. + +Lemma regs_match_approx_update: + forall ra rs a v r, + val_match_approx ge a v -> + regs_match_approx ra rs -> + regs_match_approx (D.set r a ra) (rs#r <- v). +Proof. + intros; red; intros. rewrite Regmap.gsspec. + case (peq r0 r); intro. + subst r0. rewrite D.gss. auto. + rewrite D.gso; auto. +Qed. + +Lemma approx_regs_val_list: + forall ra rs rl, + regs_match_approx ra rs -> + val_list_match_approx ge (approx_regs ra rl) rs##rl. +Proof. + induction rl; simpl; intros. + constructor. + constructor. apply H. auto. +Qed. + + +(** The correctness of the static analysis follows from the results + of module [ConstpropOpproof] and the fact that the result of + the static analysis is a solution of the forward dataflow inequations. *) + +Lemma analyze_correct_1: + forall f pc rs pc' i, + f.(fn_code)!pc = Some i -> + In pc' (successors_instr i) -> + regs_match_approx (transfer f pc (analyze f)!!pc) rs -> + regs_match_approx (analyze f)!!pc' rs. +Proof. + intros until i. unfold analyze. + caseEq (DS.fixpoint (successors f) (transfer f) + ((fn_entrypoint f, D.top) :: nil)). + intros approxs; intros. + apply regs_match_approx_increasing with (transfer f pc approxs!!pc). + eapply DS.fixpoint_solution; eauto. + unfold successors_list, successors. rewrite PTree.gmap. rewrite H0. auto. + auto. + intros. rewrite PMap.gi. apply regs_match_approx_top. +Qed. + +Lemma analyze_correct_3: + forall f rs, + regs_match_approx (analyze f)!!(f.(fn_entrypoint)) rs. +Proof. + intros. unfold analyze. + caseEq (DS.fixpoint (successors f) (transfer f) + ((fn_entrypoint f, D.top) :: nil)). + intros approxs; intros. + apply regs_match_approx_increasing with D.top. + eapply DS.fixpoint_entry; eauto. auto with coqlib. + apply regs_match_approx_top. + intros. rewrite PMap.gi. apply regs_match_approx_top. +Qed. + +End ANALYSIS. + +(** * Correctness of the code transformation *) + +(** We now show that the transformed code after constant propagation + has the same semantics as the original code. *) + +Section PRESERVATION. + +Variable prog: program. +Let tprog := transf_program prog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof. + intros; unfold ge, tge, tprog, transf_program. + apply Genv.find_symbol_transf. +Qed. + +Lemma functions_translated: + forall (v: val) (f: fundef), + Genv.find_funct ge v = Some f -> + Genv.find_funct tge v = Some (transf_fundef f). +Proof. + intros. + exact (Genv.find_funct_transf transf_fundef H). +Qed. + +Lemma function_ptr_translated: + forall (b: block) (f: fundef), + Genv.find_funct_ptr ge b = Some f -> + Genv.find_funct_ptr tge b = Some (transf_fundef f). +Proof. + intros. + exact (Genv.find_funct_ptr_transf transf_fundef H). +Qed. + +Lemma sig_function_translated: + forall f, + funsig (transf_fundef f) = funsig f. +Proof. + intros. destruct f; reflexivity. +Qed. + +Lemma transf_ros_correct: + forall ros rs f approx, + regs_match_approx ge approx rs -> + find_function ge ros rs = Some f -> + find_function tge (transf_ros approx ros) rs = Some (transf_fundef f). +Proof. + intros until approx; intro MATCH. + destruct ros; simpl. + intro. + exploit functions_translated; eauto. intro FIND. + caseEq (D.get r approx); intros; auto. + generalize (Int.eq_spec i0 Int.zero); case (Int.eq i0 Int.zero); intros; auto. + generalize (MATCH r). rewrite H0. intros [b [A B]]. + rewrite <- symbols_preserved in A. + rewrite B in FIND. rewrite H1 in FIND. + rewrite Genv.find_funct_find_funct_ptr in FIND. + simpl. rewrite A. auto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge i). + intro. apply function_ptr_translated. auto. + congruence. +Qed. + +(** The proof of semantic preservation is a simulation argument + based on diagrams of the following form: +<< + st1 --------------- st2 + | | + t| |t + | | + v v + st1'--------------- st2' +>> + The left vertical arrow represents a transition in the + original RTL code. The top horizontal bar is the [match_states] + invariant between the initial state [st1] in the original RTL code + and an initial state [st2] in the transformed code. + This invariant expresses that all code fragments appearing in [st2] + are obtained by [transf_code] transformation of the corresponding + fragments in [st1]. Moreover, the values of registers in [st1] + must match their compile-time approximations at the current program + point. + These two parts of the diagram are the hypotheses. In conclusions, + we want to prove the other two parts: the right vertical arrow, + which is a transition in the transformed RTL code, and the bottom + horizontal bar, which means that the [match_state] predicate holds + between the final states [st1'] and [st2']. *) + +Inductive match_stackframes: stackframe -> stackframe -> Prop := + match_stackframe_intro: + forall res c sp pc rs f, + c = f.(RTL.fn_code) -> + (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) -> + match_stackframes + (Stackframe res c sp pc rs) + (Stackframe res (transf_code (analyze f) c) sp pc rs). + +Inductive match_states: state -> state -> Prop := + | match_states_intro: + forall s c sp pc rs m f s' + (CF: c = f.(RTL.fn_code)) + (MATCH: regs_match_approx ge (analyze f)!!pc rs) + (STACKS: list_forall2 match_stackframes s s'), + match_states (State s c sp pc rs m) + (State s' (transf_code (analyze f) c) sp pc rs m) + | match_states_call: + forall s f args m s', + list_forall2 match_stackframes s s' -> + match_states (Callstate s f args m) + (Callstate s' (transf_fundef f) args m) + | match_states_return: + forall s s' v m, + list_forall2 match_stackframes s s' -> + match_states (Returnstate s v m) + (Returnstate s' v m). + +Ltac TransfInstr := + match goal with + | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ => + cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr)); + [ simpl + | unfold transf_code; rewrite PTree.gmap; + unfold option_map; rewrite H1; reflexivity ] + end. + +(** The proof of simulation proceeds by case analysis on the transition + taken in the source code. *) + +Lemma transf_step_correct: + forall s1 t s2, + step ge s1 t s2 -> + forall s1' (MS: match_states s1 s1'), + exists s2', step tge s1' t s2' /\ match_states s2 s2'. +Proof. + induction 1; intros; inv MS. + + (* Inop *) + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split. + TransfInstr; intro. eapply exec_Inop; eauto. + econstructor; eauto. + eapply analyze_correct_1 with (pc := pc); eauto. + simpl; auto. + unfold transfer; rewrite H. auto. + + (* Iop *) + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. + TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args); + intros op' args' OSR. + assert (eval_operation tge sp op' rs##args' = Some v). + rewrite (eval_operation_preserved symbols_preserved). + generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs + MATCH op args v). + rewrite OSR; simpl. auto. + generalize (eval_static_operation_correct ge op sp + (approx_regs (analyze f)!!pc args) rs##args v + (approx_regs_val_list _ _ _ args MATCH) H0). + case (eval_static_operation op (approx_regs (analyze f)!!pc args)); intros; + simpl in H2; + eapply exec_Iop; eauto; simpl. + congruence. + congruence. + elim H2; intros b [A B]. rewrite symbols_preserved. + rewrite A; rewrite B; auto. + econstructor; eauto. + eapply analyze_correct_1 with (pc := pc); eauto. + simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. + eapply eval_static_operation_correct; eauto. + apply approx_regs_val_list; auto. + + (* Iload *) + caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); + intros addr' args' ASR. + assert (eval_addressing tge sp addr' rs##args' = Some a). + rewrite (eval_addressing_preserved symbols_preserved). + generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs + MATCH addr args). + rewrite ASR; simpl. congruence. + TransfInstr. rewrite ASR. intro. + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split. + eapply exec_Iload; eauto. + econstructor; eauto. + eapply analyze_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. simpl; auto. + + (* Istore *) + caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); + intros addr' args' ASR. + assert (eval_addressing tge sp addr' rs##args' = Some a). + rewrite (eval_addressing_preserved symbols_preserved). + generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs + MATCH addr args). + rewrite ASR; simpl. congruence. + TransfInstr. rewrite ASR. intro. + exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split. + eapply exec_Istore; eauto. + econstructor; eauto. + eapply analyze_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. auto. + + (* Icall *) + exploit transf_ros_correct; eauto. intro FIND'. + TransfInstr; intro. + econstructor; split. + eapply exec_Icall; eauto. apply sig_function_translated; auto. + constructor; auto. constructor; auto. + econstructor; eauto. + intros. eapply analyze_correct_1; eauto. simpl; auto. + unfold transfer; rewrite H. + apply regs_match_approx_update; auto. simpl. auto. + + (* Itailcall *) + exploit transf_ros_correct; eauto. intros FIND'. + TransfInstr; intro. + econstructor; split. + eapply exec_Itailcall; eauto. apply sig_function_translated; auto. + constructor; auto. + + (* Icond, true *) + exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. + caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); + intros cond' args' CSR. + assert (eval_condition cond' rs##args' = Some true). + generalize (cond_strength_reduction_correct + ge (approx_reg (analyze f)!!pc) rs MATCH cond args). + rewrite CSR. intro. congruence. + TransfInstr. rewrite CSR. + caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)). + intros b ESC. + generalize (eval_static_condition_correct ge cond _ _ _ + (approx_regs_val_list _ _ _ args MATCH) ESC); intro. + replace b with true. intro; eapply exec_Inop; eauto. congruence. + intros. eapply exec_Icond_true; eauto. + econstructor; eauto. + eapply analyze_correct_1; eauto. + simpl; auto. + unfold transfer; rewrite H; auto. + + (* Icond, false *) + exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. + caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); + intros cond' args' CSR. + assert (eval_condition cond' rs##args' = Some false). + generalize (cond_strength_reduction_correct + ge (approx_reg (analyze f)!!pc) rs MATCH cond args). + rewrite CSR. intro. congruence. + TransfInstr. rewrite CSR. + caseEq (eval_static_condition cond (approx_regs (analyze f)!!pc args)). + intros b ESC. + generalize (eval_static_condition_correct ge cond _ _ _ + (approx_regs_val_list _ _ _ args MATCH) ESC); intro. + replace b with false. intro; eapply exec_Inop; eauto. congruence. + intros. eapply exec_Icond_false; eauto. + econstructor; eauto. + eapply analyze_correct_1; eauto. + simpl; auto. + unfold transfer; rewrite H; auto. + + (* Ireturn *) + exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split. + eapply exec_Ireturn; eauto. TransfInstr; auto. + constructor; auto. + + (* internal function *) + simpl. unfold transf_function. + econstructor; split. + eapply exec_function_internal; simpl; eauto. + simpl. econstructor; eauto. + apply analyze_correct_3; auto. + + (* external function *) + simpl. econstructor; split. + eapply exec_function_external; eauto. + constructor; auto. + + (* return *) + inv H3. inv H1. + econstructor; split. + eapply exec_return; eauto. + econstructor; eauto. +Qed. + +Lemma transf_initial_states: + forall st1, initial_state prog st1 -> + exists st2, initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inversion H. + exploit function_ptr_translated; eauto. intro FIND. + exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. + econstructor; eauto. + replace (prog_main tprog) with (prog_main prog). + rewrite symbols_preserved. eauto. + reflexivity. + rewrite <- H2. apply sig_function_translated. + replace (Genv.init_mem tprog) with (Genv.init_mem prog). + constructor. constructor. auto. + symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> final_state st1 r -> final_state st2 r. +Proof. + intros. inv H0. inv H. inv H4. constructor. +Qed. + +(** The preservation of the observable behavior of the program then + follows, using the generic preservation theorem + [Smallstep.simulation_step_preservation]. *) + +Theorem transf_program_correct: + forall (beh: program_behavior), not_wrong beh -> + exec_program prog beh -> exec_program tprog beh. +Proof. + unfold exec_program; intros. + eapply simulation_step_preservation; eauto. + eexact transf_initial_states. + eexact transf_final_states. + exact transf_step_correct. +Qed. + +End PRESERVATION. -- cgit