Support for 64-bit architectures: generic support

- Introduce Archi.ptr64 parameter.
- Define module Ptrofs of integers as wide as a pointer (64 if Archi.ptr64, 32 otherwise).
- Use Ptrofs.int as the offset type for Vptr values and anywhere pointer offsets are manipulated.
- Modify Val operations that handle pointers (e.g. Val.add, Val.sub, Val.cmpu) so that in 64-bit pointer mode it is the "long" operation (e.g. Val.addl, Val.subl, Val.cmplu) that handles pointers.
- Update the memory model accordingly.
- Modify C operations that handle pointers (e.g. addition, subtraction, comparisons) accordingly.
- Make it possible to turn off the splitting of 64-bit integers into pairs of 32-bit integers.
- Update the compiler front-end and back-end accordingly.

1 files changed, 35 insertions, 1 deletions

diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp
index a275a850..d708afb7 100644
--- a/backend/SelectDiv.vp
+++ b/backend/SelectDiv.vp
@@ -36,7 +36,7 @@ Fixpoint find_div_mul_params (fuel: nat) (nc: Z) (d: Z) (p: Z) : option (Z * Z)
   | S fuel' =>
       let twp := two_p p in
       if zlt (nc * (d - twp mod d)) twp
-      then Some(p - 32, (twp + d - twp mod d) / d)
+      then Some(p, (twp + d - twp mod d) / d)
       else find_div_mul_params fuel' nc d (p + 1)
   end.
 
@@ -47,6 +47,7 @@ Definition divs_mul_params (d: Z) : option (Z * Z) :=
           d 32 with
   | None => None
   | Some(p, m) =>
+      let p := p - 32 in
       if zlt 0 d
       && zlt (two_p (32 + p)) (m * d)
       && zle (m * d) (two_p (32 + p) + two_p (p + 1))
@@ -62,6 +63,7 @@ Definition divu_mul_params (d: Z) : option (Z * Z) :=
           d 32 with
   | None => None
   | Some(p, m) =>
+      let p := p - 32 in
       if zlt 0 d
       && zle (two_p (32 + p)) (m * d)
       && zle (m * d) (two_p (32 + p) + two_p p)
@@ -70,6 +72,38 @@ Definition divu_mul_params (d: Z) : option (Z * Z) :=
       then Some(p, m) else None
   end.
 
+Definition divls_mul_params (d: Z) : option (Z * Z) :=
+  match find_div_mul_params
+          Int64.wordsize
+          (Int64.half_modulus - Int64.half_modulus mod d - 1)
+          d 64 with
+  | None => None
+  | Some(p, m) =>
+      let p := p - 64 in
+      if zlt 0 d
+      && zlt (two_p (64 + p)) (m * d)
+      && zle (m * d) (two_p (64 + p) + two_p (p + 1))
+      && zle 0 m && zlt m Int64.modulus
+      && zle 0 p && zlt p 64
+      then Some(p, m) else None
+  end.
+
+Definition divlu_mul_params (d: Z) : option (Z * Z) :=
+  match find_div_mul_params
+          Int64.wordsize
+          (Int64.modulus - Int64.modulus mod d - 1)
+          d 64 with
+  | None => None
+  | Some(p, m) =>
+      let p := p - 64 in
+      if zlt 0 d
+      && zle (two_p (64 + p)) (m * d)
+      && zle (m * d) (two_p (64 + p) + two_p p)
+      && zle 0 m && zlt m Int64.modulus
+      && zle 0 p && zlt p 64
+      then Some(p, m) else None
+  end.
+
 Definition divu_mul (p: Z) (m: Z) :=
   shruimm (Eop Omulhu (Eletvar O ::: Eop (Ointconst (Int.repr m)) Enil ::: Enil))
           (Int.repr p).