diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-27 07:35:49 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-07-27 07:35:49 +0000 |
commit | f4e106d4fc1cce484678b5cdd86ab57d7a43076a (patch) | |
tree | 3de9bddc63b80fb1b695bbdb8fa5bd6aa893a13a /arm/SelectOp.vp | |
parent | 04ff02a9f4bc4f766a450e5463729102ee26882e (diff) |
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
Diffstat (limited to 'arm/SelectOp.vp')
-rw-r--r-- | arm/SelectOp.vp | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index ad8a945..6102d82 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) => |