From f4e106d4fc1cce484678b5cdd86ab57d7a43076a Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 27 Jul 2014 07:35:49 +0000
Subject: ARM port: add support for Thumb2.  To be tested.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2549 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 arm/SelectOp.vp | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'arm/SelectOp.vp')

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index ad8a9454..6102d82d 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -454,7 +454,7 @@ Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
   | Many64 => false
   end.
 
-Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
+Definition can_use_Aindexed2shift (chunk: memory_chunk) (s: shift): bool :=
   match chunk with
   | Mint8signed => false
   | Mint8unsigned => true
@@ -466,14 +466,20 @@ Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
   | Mfloat64 => false
   | Many32 => true
   | Many64 => false
-  end.
+  end &&
+  (if thumb tt then
+     match s with
+     | Slsl s => Int.ltu s (Int.repr 4)
+     | _      => false
+     end
+   else true).
 
 Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   match e with
   | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
   | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil)
   | Eop (Oaddshift s) (e1:::e2:::Enil) =>
-      if can_use_Aindexed2shift chunk
+      if can_use_Aindexed2shift chunk s
       then (Aindexed2shift s, e1:::e2:::Enil)
       else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil)
   | Eop Oadd (e1:::e2:::Enil) =>
-- 
cgit