From c8a892a09e9f61c3af7dae30d39509558f77462a Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 28 May 2014 14:55:10 +0000 Subject: Instead of having two expansions of shrximm (one in SelectOp, one in Asmgen), move the most efficient expansion to Asmgen. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2504 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asmgen.v | 10 +++++--- arm/Asmgenproof1.v | 73 +++++++++++++++++++++++++++++++++-------------------- arm/SelectOp.vp | 9 +------ arm/SelectOpproof.v | 40 ++--------------------------- 4 files changed, 54 insertions(+), 78 deletions(-) (limited to 'arm') diff --git a/arm/Asmgen.v b/arm/Asmgen.v index fcc5061..2513a5e 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -376,10 +376,12 @@ Definition transl_op OK (Pmov r (transl_shift s r1) :: k) | Oshrximm n, a1 :: nil => do r <- ireg_of res; do r1 <- ireg_of a1; - OK (Pcmp r1 (SOimm Int.zero) :: - addimm IR14 r1 (Int.sub (Int.shl Int.one n) Int.one) - (Pmovc TCge IR14 (SOreg r1) :: - Pmov r (SOasrimm IR14 n) :: k)) + if Int.eq n Int.zero then + OK (Pmov r (SOreg r1) :: k) + else + OK (Pmov IR14 (SOasrimm r1 (Int.repr 31)) :: + Padd IR14 r1 (SOlsrimm IR14 (Int.sub Int.iwordsize n)) :: + Pmov r (SOasrimm IR14 n) :: k) | Onegf, a1 :: nil => do r <- freg_of res; do r1 <- freg_of a1; OK (Pfnegd r r1 :: k) diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index ec6d405..3e00217 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -981,34 +981,51 @@ Local Transparent destroyed_by_op. intros [rs' [A [B C]]]. exists rs'; auto with asmgen. (* Oshrximm *) - exploit Val.shrx_shr; eauto. intros [n [i' [ARG1 [ARG2 RES]]]]. - injection ARG2; intro ARG2'; subst i'; clear ARG2. - set (islt := Int.lt n Int.zero) in *. - set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero) m)). - assert (OTH1: forall r', data_preg r' = true -> rs1#r' = rs#r'). - { apply compare_int_inv; auto. } - exploit (addimm_correct IR14 x0 (Int.sub (Int.shl Int.one i) Int.one)). - intros [rs2 [EXEC2 [RES2 OTH2]]]. - set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))). - set (rs4 := nextinstr (rs3#x <- (Val.shr rs3#IR14 (Vint i)))). - exists rs4; split. - apply exec_straight_step with rs1 m. - simpl. rewrite ARG1. auto. auto. - eapply exec_straight_trans. eexact EXEC2. - apply exec_straight_two with rs3 m. - unfold exec_instr. - assert (TC: eval_testcond TCge rs2 = Some (negb islt)). - { simpl. rewrite ! OTH2 by auto with asmgen. simpl. - rewrite Int.lt_sub_overflow. fold islt. destruct islt; auto. } - rewrite TC. simpl. rewrite OTH2 by eauto with asmgen. rewrite OTH1. rewrite ARG1. - unfold rs3; destruct islt; reflexivity. - rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen. - reflexivity. - unfold rs3; destruct islt; reflexivity. - reflexivity. - split. unfold rs4; Simpl. unfold rs3. destruct islt. - Simpl. rewrite RES2. unfold rs1. Simpl. Simpl. congruence. - intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. + destruct (rs x0) eqn: X0; simpl in H0; try discriminate. + destruct (Int.ltu i (Int.repr 31)) eqn: LTU; inv H0. + revert EQ2. predSpec Int.eq Int.eq_spec i Int.zero; intros EQ2. + (* i = 0 *) + inv EQ2. econstructor. + split. apply exec_straight_one. simpl. reflexivity. auto. + split. Simpl. unfold Int.shrx. rewrite Int.shl_zero. unfold Int.divs. + change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed. auto. + intros. Simpl. + (* i <> 0 *) + inv EQ2. + assert (LTU': Int.ltu (Int.sub Int.iwordsize i) Int.iwordsize = true). + { + generalize (Int.ltu_inv _ _ LTU). intros. + unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. + rewrite Int.unsigned_repr. apply zlt_true. + assert (Int.unsigned i <> 0). + { red; intros; elim H. rewrite <- (Int.repr_unsigned i). rewrite H1; reflexivity. } + omega. + change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. + generalize Int.wordsize_max_unsigned; omega. + } + assert (LTU'': Int.ltu i Int.iwordsize = true). + { + generalize (Int.ltu_inv _ _ LTU). intros. + unfold Int.ltu. rewrite Int.unsigned_repr_wordsize. apply zlt_true. + change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. + omega. + } + set (j := Int.sub Int.iwordsize i) in *. + set (rs1 := nextinstr (rs#IR14 <- (Val.shr (Vint i0) (Vint (Int.repr 31))))). + set (rs2 := nextinstr (rs1#IR14 <- (Val.add (Vint i0) (Val.shru rs1#IR14 (Vint j))))). + set (rs3 := nextinstr (rs2#x <- (Val.shr rs2#IR14 (Vint i)))). + exists rs3; split. + apply exec_straight_three with rs1 m rs2 m. + simpl. rewrite X0; reflexivity. + simpl. f_equal. Simpl. replace (rs1 x0) with (rs x0). rewrite X0; reflexivity. + unfold rs1; Simpl. + reflexivity. + auto. auto. auto. + split. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. + simpl. change (Int.ltu (Int.repr 31) Int.iwordsize) with true. simpl. + rewrite LTU'; simpl. rewrite LTU''; simpl. + f_equal. symmetry. apply Int.shrx_shr_2. assumption. + intros. unfold rs3; Simpl. unfold rs2; Simpl. unfold rs1; Simpl. (* intoffloat *) econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. Transparent destroyed_by_op. diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index efd9e48..e4005c9 100644 --- a/arm/SelectOp.vp +++ b/arm/SelectOp.vp @@ -291,14 +291,7 @@ Definition divu_base (e1: expr) (e2: expr) := Eop Odivu (e1:::e2:::Enil). Definition modu_base := mod_aux Odivu. Definition shrximm (e1: expr) (n2: int) := - if Int.eq n2 Int.zero - then e1 - else Elet e1 - (shrimm - (add (Eletvar O) - (shruimm (shrimm (Eletvar O) (Int.repr 31)) - (Int.sub Int.iwordsize n2))) - n2). + if Int.eq n2 Int.zero then e1 else Eop (Oshrximm n2) (e1:::Enil). (** ** General shifts *) diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 4b89119..1dd2c20 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -542,49 +542,13 @@ Theorem eval_shrximm: Proof. intros. unfold shrximm. predSpec Int.eq Int.eq_spec n Int.zero. -- subst n. exists x; split; auto. + subst n. exists x; split; auto. destruct x; simpl in H0; try discriminate. destruct (Int.ltu Int.zero (Int.repr 31)); inv H0. replace (Int.shrx i Int.zero) with i. auto. unfold Int.shrx, Int.divs. rewrite Int.shl_zero. change (Int.signed Int.one) with 1. rewrite Z.quot_1_r. rewrite Int.repr_signed; auto. -- destruct x; simpl in H0; try discriminate. - destruct (Int.ltu n (Int.repr 31)) eqn:LT31; inv H0. - assert (A: eval_expr ge sp e m (Vint i :: le) (Eletvar 0) (Vint i)) - by (constructor; auto). - exploit (eval_shrimm (Int.repr 31)). eexact A. - intros [v [B LD]]. simpl in LD. - change (Int.ltu (Int.repr 31) Int.iwordsize) with true in LD. - simpl in LD; inv LD. - exploit (eval_shruimm (Int.sub Int.iwordsize n)). eexact B. - intros [v [C LD]]. simpl in LD. - assert (RANGE: Int.ltu (Int.sub Int.iwordsize n) Int.iwordsize = true). - { - generalize (Int.ltu_inv _ _ LT31). intros. - unfold Int.sub, Int.ltu. rewrite Int.unsigned_repr_wordsize. - rewrite Int.unsigned_repr. apply zlt_true. - assert (Int.unsigned n <> 0). - { red; intros; elim H1. rewrite <- (Int.repr_unsigned n). rewrite H2; reflexivity. } - omega. - change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. - generalize Int.wordsize_max_unsigned; omega. - } - rewrite RANGE in LD. inv LD. - exploit eval_add. eexact A. eexact C. intros [v [D LD]]. - simpl in LD. inv LD. - exploit (eval_shrimm n). eexact D. intros [v [E LD]]. - simpl in LD. - assert (RANGE2: Int.ltu n Int.iwordsize = true). - { - generalize (Int.ltu_inv _ _ LT31). intros. - unfold Int.ltu. rewrite Int.unsigned_repr_wordsize. apply zlt_true. - change (Int.unsigned (Int.repr 31)) with (Int.zwordsize - 1) in H0. - omega. - } - rewrite RANGE2 in LD. inv LD. - econstructor; split. econstructor. eassumption. eexact E. - rewrite Int.shrx_shr_2 by auto. - auto. + econstructor; split. EvalOp. auto. Qed. Theorem eval_shl: binary_constructor_sound shl Val.shl. -- cgit v1.2.3