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

1 files changed, 6 insertions, 0 deletions

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index 22ef88d..d81328b 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