From 9475c5637c5d650f43955abe8f995797893affe1 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 14 Jan 2020 23:37:20 +0100 Subject: ARM generation of 2-instruction signed division by 2 (as opposed to 3-instruction) --- arm/Asmgenproof1.v | 24 +++++++++++++++++++++--- 1 file changed, 21 insertions(+), 3 deletions(-) (limited to 'arm/Asmgenproof1.v') diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 807e069d..2b125cda 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -1264,15 +1264,32 @@ Local Transparent destroyed_by_op. 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). + } + { (* i <> 0 *) + revert EQ2. predSpec Int.eq Int.eq_spec i Int.one; intros EQ2. + { + inv EQ2. + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. + { rewrite X0. + rewrite Int.shrx1_shr by reflexivity. + Simpl. + } + { intros. + Simpl. + } + } + clear H0. + 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. @@ -1306,6 +1323,7 @@ Local Transparent destroyed_by_op. 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. -- cgit