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, 5 insertions, 5 deletions

diff --git a/backend/CSE.v b/backend/CSE.v
index d6b89557..4fa1bd6c 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -327,14 +327,14 @@ Definition kill_loads_after_storebytes
 Definition shift_memcpy_eq (src sz delta: Z) (e: equation) :=
   match e with
   | Eq l strict (Load chunk (Ainstack i) _) =>
-      let i := Int.unsigned i in
+      let i := Ptrofs.unsigned i in
       let j := i + delta in
       if zle src i
       && zle (i + size_chunk chunk) (src + sz)
       && zeq (Zmod delta (align_chunk chunk)) 0
       && zle 0 j
-      && zle j Int.max_unsigned
-      then Some(Eq l strict (Load chunk (Ainstack (Int.repr j)) nil))
+      && zle j Ptrofs.max_unsigned
+      then Some(Eq l strict (Load chunk (Ainstack (Ptrofs.repr j)) nil))
       else None
   | _ => None
   end.
@@ -353,8 +353,8 @@ Definition add_memcpy (n1 n2: numbering) (asrc adst: aptr) (sz: Z) :=
   match asrc, adst with
   | Stk src, Stk dst =>
       {| num_next := n2.(num_next);
-         num_eqs  := add_memcpy_eqs (Int.unsigned src) sz
-                                    (Int.unsigned dst - Int.unsigned src)
+         num_eqs  := add_memcpy_eqs (Ptrofs.unsigned src) sz
+                                    (Ptrofs.unsigned dst - Ptrofs.unsigned src)
                                     n1.(num_eqs) n2.(num_eqs);
          num_reg  := n2.(num_reg);
          num_val  := n2.(num_val) |}