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, 9 insertions, 0 deletions

diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index e6ba98a..fea0afd 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -31,6 +31,7 @@ Inductive approx : Type :=
                              no compile-time information is available. *)
   | I: int -> approx     (** A known integer value. *)
   | F: float -> approx   (** A known floating-point value. *)
+  | L: int64 -> approx   (** A know 64-bit integer value. *)
   | G: ident -> int -> approx
                          (** The value is the address of the given global
                              symbol plus the given integer offset. *)
@@ -130,6 +131,11 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Oshru, I n1 :: I n2 :: nil => if Int.ltu n2 Int.iwordsize then I(Int.shru n1 n2) else Unknown
   | Oshruimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.shru n1 n) else Unknown
   | Ororimm n, I n1 :: nil => if Int.ltu n Int.iwordsize then I(Int.ror n1 n) else Unknown
+  | Oshldimm n, I n1 :: I n2 :: nil =>
+      let n' := Int.sub Int.iwordsize n in
+      if Int.ltu n Int.iwordsize && Int.ltu n' Int.iwordsize
+      then I(Int.or (Int.shl n1 n) (Int.shru n2 n')) 
+      else Unknown
   | Olea mode, vl => eval_static_addressing mode vl
   | Onegf, F n1 :: nil => F(Float.neg n1)
   | Oabsf, F n1 :: nil => F(Float.abs n1)
@@ -140,6 +146,9 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
   | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1
   | Ofloatofint, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofint n1) else Unknown
+  | Omakelong, I n1 :: I n2 :: nil => L(Int64.ofwords n1 n2)
+  | Olowlong, L n :: nil => I(Int64.loword n)
+  | Ohighlong, L n :: nil => I(Int64.hiword n)
   | Ocmp c, vl => eval_static_condition_val c vl
   | _, _ => Unknown
   end.