2-instruction signed division by two on Aarch64

3 files changed, 54 insertions, 24 deletions

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
index 875f3fd1..daea7dd5 100644
--- a/aarch64/Asmgen.v
+++ b/aarch64/Asmgen.v
@@ -268,18 +268,24 @@ Definition arith_extended
 Definition shrx32 (rd r1: ireg) (n: int) (k: code) : code :=
   if Int.eq n Int.zero then
     Pmov rd r1 :: k
-  else
-    Porr W X16 XZR r1 (SOasr (Int.repr 31)) ::
-    Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) ::
-    Porr W rd XZR X16 (SOasr n) :: k.
+  else if Int.eq n Int.one then
+         Padd W X16 r1 r1 (SOlsr (Int.repr 31)) ::
+         Porr W rd XZR X16 (SOasr n) :: k
+       else
+         Porr W X16 XZR r1 (SOasr (Int.repr 31)) ::
+         Padd W X16 r1 X16 (SOlsr (Int.sub Int.iwordsize n)) ::
+         Porr W rd XZR X16 (SOasr n) :: k.
 
 Definition shrx64 (rd r1: ireg) (n: int) (k: code) : code :=
   if Int.eq n Int.zero then
     Pmov rd r1 :: k
-  else
-    Porr X X16 XZR r1 (SOasr (Int.repr 63)) ::
-    Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) ::
-    Porr X rd XZR X16 (SOasr n) :: k.
+  else if Int.eq n Int.one then
+         Padd X X16 r1 r1 (SOlsr (Int.repr 63)) ::
+         Porr X rd XZR X16 (SOasr n) :: k
+       else
+         Porr X X16 XZR r1 (SOasr (Int.repr 63)) ::
+         Padd X X16 r1 X16 (SOlsr (Int.sub Int64.iwordsize' n)) ::
+         Porr X rd XZR X16 (SOasr n) :: k.
 
 (** Load the address [id + ofs] in [rd] *)
 
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index eeff1956..3f082b16 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -259,13 +259,13 @@ Proof.
 - apply logicalimm32_label; unfold nolabel; auto.
 - apply logicalimm32_label; unfold nolabel; auto.
 - apply logicalimm32_label; unfold nolabel; auto.
-- unfold shrx32. destruct Int.eq; TailNoLabel.
+- unfold shrx32. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel.
 - apply arith_extended_label; unfold nolabel; auto.
 - apply arith_extended_label; unfold nolabel; auto.
 - apply logicalimm64_label; unfold nolabel; auto.
 - apply logicalimm64_label; unfold nolabel; auto.
 - apply logicalimm64_label; unfold nolabel; auto.
-- unfold shrx64. destruct Int.eq; TailNoLabel.
+- unfold shrx64. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel.
 - eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel.
 - destruct (preg_of r); try discriminate; TailNoLabel;
   (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto | TailNoLabel]).
diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v
index 6d44bcc8..d004b715 100644
--- a/aarch64/Asmgenproof1.v
+++ b/aarch64/Asmgenproof1.v
@@ -754,16 +754,28 @@ Lemma exec_shrx32: forall (rd r1: ireg) (n: int) k v (rs: regset) m,
   /\ rs'#rd = v
   /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
-  unfold shrx32; intros. apply Val.shrx_shr_2 in H.
+  unfold shrx32; intros. apply Val.shrx_shr_3 in H.
   destruct (Int.eq n Int.zero) eqn:E.
 - econstructor; split. apply exec_straight_one; [simpl;eauto|auto]. 
   split. Simpl. subst v; auto. intros; Simpl.
-- econstructor; split. eapply exec_straight_three.
-  unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto.
-  simpl; eauto.
-  unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto.
-  auto. auto. auto.
-  split. subst v; Simpl. intros; Simpl.
+- generalize (Int.eq_spec n Int.one).
+  destruct (Int.eq n Int.one); intro ONE.
+  * subst n.
+    econstructor; split. eapply exec_straight_two.
+    all: simpl; auto.
+    split.
+    ** subst v; Simpl.
+       destruct (Val.add _ _); simpl; trivial.
+       change (Int.ltu Int.one Int.iwordsize) with true; simpl.
+       rewrite Int.or_zero_l.
+       reflexivity.
+    ** intros; Simpl.
+  * econstructor; split. eapply exec_straight_three.
+    unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto.
+    simpl; eauto.
+    unfold exec_instr. rewrite or_zero_eval_shift_op_int by congruence. eauto.
+    auto. auto. auto.
+    split. subst v; Simpl. intros; Simpl.
 Qed.
  
 Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m,
@@ -774,16 +786,28 @@ Lemma exec_shrx64: forall (rd r1: ireg) (n: int) k v (rs: regset) m,
   /\ rs'#rd = v
   /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r.
 Proof.
-  unfold shrx64; intros. apply Val.shrxl_shrl_2 in H.
+  unfold shrx64; intros. apply Val.shrxl_shrl_3 in H.
   destruct (Int.eq n Int.zero) eqn:E.
 - econstructor; split. apply exec_straight_one; [simpl;eauto|auto]. 
   split. Simpl. subst v; auto. intros; Simpl.
-- econstructor; split. eapply exec_straight_three.
-  unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto.
-  simpl; eauto.
-  unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto.
-  auto. auto. auto.
-  split. subst v; Simpl. intros; Simpl.
+- generalize (Int.eq_spec n Int.one).
+  destruct (Int.eq n Int.one); intro ONE.
+  * subst n.
+    econstructor; split. eapply exec_straight_two.
+    all: simpl; auto.
+    split.
+    ** subst v; Simpl.
+       destruct (Val.addl _ _); simpl; trivial.
+       change (Int.ltu Int.one Int64.iwordsize') with true; simpl.
+       rewrite Int64.or_zero_l.
+       reflexivity.
+    ** intros; Simpl.
+  * econstructor; split. eapply exec_straight_three.
+    unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto.
+    simpl; eauto.
+    unfold exec_instr. rewrite or_zero_eval_shift_op_long by congruence. eauto.
+    auto. auto. auto.
+    split. subst v; Simpl. intros; Simpl.
 Qed.
 
 (** Condition bits *)