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

1 files changed, 445 insertions, 0 deletions

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.