From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 20 Apr 2013 07:54:52 +0000
Subject: Big merge of the newregalloc-int64 branch.  Lots of changes in two
 directions: 1- new register allocator (+ live range splitting,
 spilling&reloading, etc)    based on a posteriori validation using the
 Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long
 long").

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

(limited to 'arm/SelectOp.vp')

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 22ef88d2..d81328b0 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -85,6 +85,8 @@ Nondetfunction add (e1: expr) (e2: expr) :=
   | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil))
   | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil)
   | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil)
+  | Eop Omul (t1:::t2:::Enil), t3 => Eop Omla (t1:::t2:::t3:::Enil)
+  | t1, Eop Omul (t2:::t3:::Enil) => Eop Omla (t2:::t3:::t1:::Enil)
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 
@@ -185,6 +187,7 @@ Nondetfunction mul (e1: expr) (e2: expr) :=
 
 Nondetfunction andimm (n1: int) (e2: expr) := 
   if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else
+  if Int.eq n1 Int.mone then e2 else
   match e2 with
   | Eop (Ointconst n2) Enil =>
       Eop (Ointconst (Int.and n1 n2)) Enil
@@ -215,6 +218,7 @@ Definition same_expr_pure (e1 e2: expr) :=
 
 Nondetfunction orimm (n1: int) (e2: expr) :=
   if Int.eq n1 Int.zero then e2 else
+  if Int.eq n1 Int.mone then Eop (Ointconst Int.mone) Enil else
   match e2 with
   | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil
   | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
@@ -407,6 +411,7 @@ Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
   | Mint16signed => true
   | Mint16unsigned => true
   | Mint32 => true
+  | Mint64 => false
   | Mfloat32 => false
   | Mfloat64 => false
   | Mfloat64al32 => false
@@ -419,6 +424,7 @@ Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
   | Mint16signed => false
   | Mint16unsigned => false
   | Mint32 => true
+  | Mint64 => false
   | Mfloat32 => false
   | Mfloat64 => false
   | Mfloat64al32 => false
-- 
cgit