From 9475c5637c5d650f43955abe8f995797893affe1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
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/Asmgen.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'arm/Asmgen.v')

diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 1a1e7f2f..0ec0a4d0 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -481,6 +481,9 @@ Definition transl_op
       do r <- ireg_of res; do r1 <- ireg_of a1;
       if Int.eq n Int.zero then
         OK (Pmov r (SOreg r1) :: k)
+      else if Int.eq n Int.one then
+        OK (Padd IR14 r1 (SOlsr r1 (Int.repr 31)) ::
+            Pmov r (SOasr IR14 n) :: k)
       else
         OK (Pmov IR14 (SOasr r1 (Int.repr 31)) ::
             Padd IR14 r1 (SOlsr IR14 (Int.sub Int.iwordsize n)) ::
-- 
cgit