From 132e36fa0be63eb5672eda9168403d3fb74af2fa Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 26 May 2012 07:32:01 +0000 Subject: CSE: add recognition of some combined operators, conditions, and addressing modes (cf. CombineOp.v) Memory model: cleaning up Memdata Inlining and new Constprop: updated for ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1902 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/CSEproof.v | 175 +++++++++++++++++++++++++++++++++++++---------------- 1 file changed, 122 insertions(+), 53 deletions(-) (limited to 'backend/CSEproof.v') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index fa07716..49b213b 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -28,6 +28,8 @@ Require Import Registers. Require Import RTL. Require Import RTLtyping. Require Import Kildall. +Require Import CombineOp. +Require Import CombineOpproof. Require Import CSE. (** * Semantic properties of value numberings *) @@ -708,7 +710,7 @@ Proof. eapply VAL. rewrite Heql. auto with coqlib. Qed. -(** Correctness of [find_op] and [find_load]: if successful and in a +(** Correctness of [find_rhs]: if successful and in a satisfiable numbering, the returned register does contain the result value of the operation or memory load. *) @@ -730,42 +732,73 @@ Proof. discriminate. Qed. -Lemma find_op_correct: - forall rs m n op args r, - wf_numbering n -> - numbering_satisfiable ge sp rs m n -> - find_op n op args = Some r -> - eval_operation ge sp op rs##args m = Some rs#r. +(** Correctness of operator reduction *) + +Section REDUCE. + +Variable A: Type. +Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum). +Variable V: Type. +Variable rs: regset. +Variable m: mem. +Variable sem: A -> list val -> option V. +Hypothesis f_sound: + forall eqs valu op args op' args', + (forall v rhs, eqs v = Some rhs -> equation_holds valu ge sp m v rhs) -> + f eqs op args = Some(op', args') -> + sem op' (map valu args') = sem op (map valu args). +Variable n: numbering. +Variable valu: valnum -> val. +Hypothesis n_holds: numbering_holds valu ge sp rs m n. +Hypothesis n_wf: wf_numbering n. + +Lemma regs_valnums_correct: + forall vl rl, regs_valnums n vl = Some rl -> rs##rl = map valu vl. Proof. - intros until r. intros WF [valu NH]. - unfold find_op. caseEq (valnum_regs n args). intros n' vl VR FIND. - assert (WF': wf_numbering n') by (eapply wf_valnum_regs; eauto). - generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR). - intros [valu2 [NH2 [EQ AG]]]. - rewrite <- EQ. - change (rhs_evals_to valu2 (Op op vl) m rs#r). - eapply find_rhs_correct; eauto. + induction vl; simpl; intros. + inv H. auto. + destruct (reg_valnum n a) as [r1|]_eqn; try discriminate. + destruct (regs_valnums n vl) as [rx|]_eqn; try discriminate. + inv H. simpl; decEq; auto. + eapply (proj2 n_holds); eauto. eapply reg_valnum_correct; eauto. Qed. -Lemma find_load_correct: - forall rs m n chunk addr args r, - wf_numbering n -> - numbering_satisfiable ge sp rs m n -> - find_load n chunk addr args = Some r -> - exists a, - eval_addressing ge sp addr rs##args = Some a /\ - Mem.loadv chunk m a = Some rs#r. +Lemma reduce_rec_sound: + forall niter op args op' rl' res, + reduce_rec A f n niter op args = Some(op', rl') -> + sem op (map valu args) = Some res -> + sem op' (rs##rl') = Some res. Proof. - intros until r. intros WF [valu NH]. - unfold find_load. caseEq (valnum_regs n args). intros n' vl VR FIND. - assert (WF': wf_numbering n') by (eapply wf_valnum_regs; eauto). - generalize (valnum_regs_holds _ _ _ _ _ _ _ WF NH VR). - intros [valu2 [NH2 [EQ AG]]]. - rewrite <- EQ. - change (rhs_evals_to valu2 (Load chunk addr vl) m rs#r). - eapply find_rhs_correct; eauto. + induction niter; simpl; intros. + discriminate. + destruct (f (fun v : valnum => find_valnum_num v (num_eqs n)) op args) + as [[op1 args1] | ]_eqn. + assert (sem op1 (map valu args1) = Some res). + rewrite <- H0. eapply f_sound; eauto. + simpl; intros. apply (proj1 n_holds). eapply find_valnum_num_correct; eauto. + destruct (reduce_rec A f n niter op1 args1) as [[op2 rl2] | ]_eqn. + inv H. eapply IHniter; eauto. + destruct (regs_valnums n args1) as [rl|]_eqn. + inv H. erewrite regs_valnums_correct; eauto. + discriminate. + discriminate. Qed. +Lemma reduce_sound: + forall op rl vl op' rl' res, + reduce A f n op rl vl = (op', rl') -> + map valu vl = rs##rl -> + sem op rs##rl = Some res -> + sem op' rs##rl' = Some res. +Proof. + unfold reduce; intros. + destruct (reduce_rec A f n 4%nat op vl) as [[op1 rl1] | ]_eqn; inv H. + eapply reduce_rec_sound; eauto. congruence. + auto. +Qed. + +End REDUCE. + End SATISFIABILITY. (** The numberings associated to each instruction by the static analysis @@ -942,17 +975,27 @@ Proof. (* Iop *) exists (State s' (transf_function' f approx) sp pc' (rs#res <- v) m); split. - assert (eval_operation tge sp op rs##args m = Some v). - rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. destruct (is_trivial_op op) as []_eqn. - eapply exec_Iop'; eauto. - destruct (find_op approx!!pc op args) as [r|]_eqn. - eapply exec_Iop'; eauto. simpl. - assert (eval_operation ge sp op rs##args m = Some rs#r). - eapply find_op_correct; eauto. - eapply wf_analyze; eauto. - congruence. eapply exec_Iop'; eauto. + rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. + destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. + destruct SAT as [valu1 NH1]. + exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. + assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + destruct (find_rhs n1 (Op op vl)) as [r|]_eqn. + (* replaced by move *) + assert (EV: rhs_evals_to ge sp valu2 (Op op vl) m rs#r). eapply find_rhs_correct; eauto. + assert (RES: rs#r = v). red in EV. congruence. + eapply exec_Iop'; eauto. simpl. congruence. + (* possibly simplified *) + destruct (reduce operation combine_op n1 op args vl) as [op' args']_eqn. + assert (RES: eval_operation ge sp op' rs##args' m = Some v). + eapply reduce_sound with (sem := fun op vl => eval_operation ge sp op vl m); eauto. + intros; eapply combine_op_sound; eauto. + eapply exec_Iop'; eauto. + rewrite <- RES. apply eval_operation_preserved. exact symbols_preserved. + (* state matching *) econstructor; eauto. apply wt_regset_assign; auto. generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI. @@ -966,17 +1009,25 @@ Proof. (* Iload *) exists (State s' (transf_function' f approx) sp pc' (rs#dst <- v) m); split. - assert (eval_addressing tge sp addr rs##args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - destruct (find_load approx!!pc chunk addr args) as [r|]_eqn. - eapply exec_Iop'; eauto. simpl. - assert (exists a, eval_addressing ge sp addr rs##args = Some a - /\ Mem.loadv chunk m a = Some rs#r). - eapply find_load_correct; eauto. - eapply wf_analyze; eauto. - destruct H3 as [a' [A B]]. - congruence. - eapply exec_Iload'; eauto. + destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. + destruct SAT as [valu1 NH1]. + exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. + assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + destruct (find_rhs n1 (Load chunk addr vl)) as [r|]_eqn. + (* replaced by move *) + assert (EV: rhs_evals_to ge sp valu2 (Load chunk addr vl) m rs#r). eapply find_rhs_correct; eauto. + assert (RES: rs#r = v). red in EV. destruct EV as [a' [EQ1 EQ2]]. congruence. + eapply exec_Iop'; eauto. simpl. congruence. + (* possibly simplified *) + destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn. + assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). + eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. + intros; eapply combine_addr_sound; eauto. + assert (ADDR': eval_addressing tge sp addr' rs##args' = Some a). + rewrite <- ADDR. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. + (* state matching *) econstructor; eauto. generalize (wt_instrs _ _ WTF pc _ H); intro WTI; inv WTI. apply wt_regset_assign. auto. rewrite H8. eapply type_of_chunk_correct; eauto. @@ -986,8 +1037,17 @@ Proof. (* Istore *) exists (State s' (transf_function' f approx) sp pc' rs m'); split. - assert (eval_addressing tge sp addr rs##args = Some a). - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. + destruct SAT as [valu1 NH1]. + exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. + assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + destruct (reduce addressing combine_addr n1 addr args vl) as [addr' args']_eqn. + assert (ADDR: eval_addressing ge sp addr' rs##args' = Some a). + eapply reduce_sound with (sem := fun addr vl => eval_addressing ge sp addr vl); eauto. + intros; eapply combine_addr_sound; eauto. + assert (ADDR': eval_addressing tge sp addr' rs##args' = Some a). + rewrite <- ADDR. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Istore; eauto. econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. @@ -1035,6 +1095,15 @@ Proof. eapply kill_loads_satisfiable; eauto. (* Icond *) + destruct (valnum_regs approx!!pc args) as [n1 vl]_eqn. + assert (wf_numbering approx!!pc). eapply wf_analyze; eauto. + elim SAT; intros valu1 NH1. + exploit valnum_regs_holds; eauto. intros [valu2 [NH2 [EQ AG]]]. + assert (wf_numbering n1). eapply wf_valnum_regs; eauto. + destruct (reduce condition combine_cond n1 cond args vl) as [cond' args']_eqn. + assert (RES: eval_condition cond' rs##args' m = Some b). + eapply reduce_sound with (sem := fun cond vl => eval_condition cond vl m); eauto. + intros; eapply combine_cond_sound; eauto. econstructor; split. eapply exec_Icond; eauto. econstructor; eauto. -- cgit v1.2.3