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/CSE.v | 97 ++++++++++++++++++++------ backend/CSEproof.v | 175 +++++++++++++++++++++++++++++++++-------------- backend/Inliningproof.v | 10 +-- backend/Linearizeproof.v | 4 +- backend/Renumberproof.v | 6 +- backend/Selectionproof.v | 4 +- 6 files changed, 213 insertions(+), 83 deletions(-) (limited to 'backend') diff --git a/backend/CSE.v b/backend/CSE.v index d46afdce..e9613c92 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -27,6 +27,7 @@ Require Import Registers. Require Import RTL. Require Import RTLtyping. Require Import Kildall. +Require Import CombineOp. (** * Value numbering *) @@ -49,11 +50,13 @@ Require Import Kildall. Equations are of the form [valnum = rhs], where the right-hand sides [rhs] are either arithmetic operations or memory loads. *) +(* Definition valnum := positive. Inductive rhs : Type := | Op: operation -> list valnum -> rhs | Load: memory_chunk -> addressing -> list valnum -> rhs. +*) Definition eq_valnum: forall (x y: valnum), {x=y}+{x<>y} := peq. @@ -272,8 +275,8 @@ Definition add_store (n: numbering) (chunk: memory_chunk) (addr: addressing) | _ => n2 end. -(* [reg_valnum n vn] returns a register that is mapped to value number - [vn], or [None] if no such register exists. *) +(** [reg_valnum n vn] returns a register that is mapped to value number + [vn], or [None] if no such register exists. *) Definition reg_valnum (n: numbering) (vn: valnum) : option reg := match PMap.get vn n.(num_val) with @@ -281,10 +284,19 @@ Definition reg_valnum (n: numbering) (vn: valnum) : option reg := | r :: rs => Some r end. -(* [find_rhs] and its specializations [find_op] and [find_load] - return a register that already holds the result of the given arithmetic - operation or memory load, according to the given numbering. - [None] is returned if no such register exists. *) +Fixpoint regs_valnums (n: numbering) (vl: list valnum) : option (list reg) := + match vl with + | nil => Some nil + | v1 :: vs => + match reg_valnum n v1, regs_valnums n vs with + | Some r1, Some rs => Some (r1 :: rs) + | _, _ => None + end + end. + +(** [find_rhs] return a register that already holds the result of the given arithmetic + operation or memory load, according to the given numbering. + [None] is returned if no such register exists. *) Definition find_rhs (n: numbering) (rh: rhs) : option reg := match find_valnum_rhs rh n.(num_eqs) with @@ -292,15 +304,44 @@ Definition find_rhs (n: numbering) (rh: rhs) : option reg := | Some vres => reg_valnum n vres end. -Definition find_op - (n: numbering) (op: operation) (rs: list reg) : option reg := - let (n1, vl) := valnum_regs n rs in - find_rhs n1 (Op op vl). +(** Experimental: take advantage of known equations to select more efficient + forms of operations, addressing modes, and conditions. *) + +Section REDUCE. + +Variable A: Type. +Variable f: (valnum -> option rhs) -> A -> list valnum -> option (A * list valnum). +Variable n: numbering. + +Fixpoint reduce_rec (niter: nat) (op: A) (args: list valnum) : option(A * list reg) := + match niter with + | O => None + | S niter' => + match f (fun v => find_valnum_num v n.(num_eqs)) op args with + | None => None + | Some(op', args') => + match reduce_rec niter' op' args' with + | None => + match regs_valnums n args' with Some rl => Some(op', rl) | None => None end + | Some _ as res => + res + end + end + end. + +Definition reduce (op: A) (rl: list reg) (vl: list valnum) : A * list reg := + match reduce_rec 4%nat op vl with + | None => (op, rl) + | Some res => res + end. + +End REDUCE. -Definition find_load - (n: numbering) (chunk: memory_chunk) (addr: addressing) (rs: list reg) : option reg := - let (n1, vl) := valnum_regs n rs in - find_rhs n1 (Load chunk addr vl). +(* +Parameter combine_cond: (valnum -> option rhs) -> condition -> list valnum -> option (condition * list valnum). +Parameter combine_addr: (valnum -> option rhs) -> addressing -> list valnum -> option (addressing * list valnum). +Parameter combine_op: (valnum -> option rhs) -> operation -> list valnum -> option (operation * list valnum). +*) (** * The static analysis *) @@ -442,15 +483,31 @@ Definition transf_instr (n: numbering) (instr: instruction) := match instr with | Iop op args res s => if is_trivial_op op then instr else - match find_op n op args with - | None => instr - | Some r => Iop Omove (r :: nil) res s + let (n1, vl) := valnum_regs n args in + match find_rhs n1 (Op op vl) with + | Some r => + Iop Omove (r :: nil) res s + | None => + let (op', args') := reduce _ combine_op n1 op args vl in + Iop op' args' res s end | Iload chunk addr args dst s => - match find_load n chunk addr args with - | None => instr - | Some r => Iop Omove (r :: nil) dst s + let (n1, vl) := valnum_regs n args in + match find_rhs n1 (Load chunk addr vl) with + | Some r => + Iop Omove (r :: nil) dst s + | None => + let (addr', args') := reduce _ combine_addr n1 addr args vl in + Iload chunk addr' args' dst s end + | Istore chunk addr args src s => + let (n1, vl) := valnum_regs n args in + let (addr', args') := reduce _ combine_addr n1 addr args vl in + Istore chunk addr' args' src s + | Icond cond args s1 s2 => + let (n1, vl) := valnum_regs n args in + let (cond', args') := reduce _ combine_cond n1 cond args vl in + Icond cond' args' s1 s2 | _ => instr end. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index fa077161..49b213bd 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. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index c62e173a..f88ca81e 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -868,9 +868,10 @@ Proof. eauto. fold (saddr ctx addr). intros [a' [P Q]]. exploit Mem.loadv_inject; eauto. intros [v' [U V]]. + assert (eval_addressing tge (Vptr sp' Int.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a'). + rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved. left; econstructor; split. - eapply plus_one. eapply exec_Iload; eauto. erewrite eval_addressing_preserved; eauto. - exact symbols_preserved. + eapply plus_one. eapply exec_Iload; eauto. econstructor; eauto. apply match_stacks_inside_set_reg; auto. apply agree_set_reg; auto. @@ -885,9 +886,10 @@ Proof. fold saddr. intros [a' [P Q]]. exploit Mem.storev_mapped_inject; eauto. eapply agree_val_reg; eauto. intros [m1' [U V]]. + assert (eval_addressing tge (Vptr sp' Int.zero) (saddr ctx addr) rs' ## (sregs ctx args) = Some a'). + rewrite <- P. apply eval_addressing_preserved. exact symbols_preserved. left; econstructor; split. - eapply plus_one. eapply exec_Istore; eauto. erewrite eval_addressing_preserved; eauto. - exact symbols_preserved. + eapply plus_one. eapply exec_Istore; eauto. destruct a; simpl in H1; try discriminate. destruct a'; simpl in U; try discriminate. econstructor; eauto. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 50db0c65..b72268a6 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -641,7 +641,7 @@ Proof. econstructor; split. eapply plus_left'. eapply exec_Lcond_false; eauto. - change false with (negb true). apply eval_negate_condition; auto. + rewrite eval_negate_condition; rewrite H0; auto. eapply add_branch_correct; eauto. eapply is_tail_add_branch. eapply is_tail_cons_left. eapply is_tail_find_label. eauto. @@ -657,7 +657,7 @@ Proof. destruct (starts_with ifso c'). econstructor; split. apply plus_one. eapply exec_Lcond_true; eauto. - change true with (negb false). apply eval_negate_condition; auto. + rewrite eval_negate_condition; rewrite H0; auto. econstructor; eauto. econstructor; split. eapply plus_left'. diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index a1b32b8f..5ec29e25 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -171,13 +171,15 @@ Proof. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* load *) econstructor; split. - eapply exec_Iload; eauto. + assert (eval_addressing tge sp addr rs ## args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Iload; eauto. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* store *) econstructor; split. - eapply exec_Istore; eauto. + assert (eval_addressing tge sp addr rs ## args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply exec_Istore; eauto. constructor; auto. eapply reach_succ; eauto. simpl; auto. (* call *) econstructor; split. diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 4e67181a..0aa2b6bf 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -50,7 +50,7 @@ Proof. induction 1; simpl. constructor. constructor. - econstructor. eauto. apply eval_negate_condition. auto. + econstructor. eauto. rewrite eval_negate_condition. rewrite H0. auto. econstructor. eauto. destruct vb1; auto. Qed. @@ -124,7 +124,7 @@ Proof. intros. apply is_compare_neq_zero_correct with (negate_condition c). destruct c; simpl in H; simpl; try discriminate; destruct c; simpl; try discriminate; auto. - apply eval_negate_condition; auto. + rewrite eval_negate_condition. rewrite H0. auto. Qed. Lemma eval_condition_of_expr: -- cgit