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, 66 insertions, 42 deletions

diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 40b51bd3..4e7aca8a 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -49,6 +49,9 @@ Definition make_floatconst (f: float) :=  Econst (Ofloatconst f).
 
 Definition make_singleconst (f: float32) :=  Econst (Osingleconst f).
 
+Definition make_ptrofsconst (n: Z) :=
+  if Archi.ptr64 then make_longconst (Int64.repr n) else make_intconst (Int.repr n).
+
 Definition make_singleoffloat (e: expr) := Eunop Osingleoffloat e.
 Definition make_floatofsingle (e: expr) := Eunop Ofloatofsingle e.
 
@@ -106,7 +109,7 @@ Definition make_longofsingle (e: expr) (sg: signedness) :=
   | Unsigned => Eunop Olonguofsingle e
   end.
 
-Definition make_cmp_ne_zero (e: expr) :=
+Definition make_cmpu_ne_zero (e: expr) :=
   match e with
   | Ebinop (Ocmp c) e1 e2 => e
   | Ebinop (Ocmpu c) e1 e2 => e
@@ -114,7 +117,7 @@ Definition make_cmp_ne_zero (e: expr) :=
   | Ebinop (Ocmpfs c) e1 e2 => e
   | Ebinop (Ocmpl c) e1 e2 => e
   | Ebinop (Ocmplu c) e1 e2 => e
-  | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero)
+  | _ => Ebinop (Ocmpu Cne) e (make_intconst Int.zero)
   end.
 
 (** Variants of [sizeof] and [alignof] that check that the given type is complete. *)
@@ -139,12 +142,12 @@ Definition make_cast_int (e: expr) (sz: intsize) (si: signedness) :=
   | I16, Signed => Eunop Ocast16signed e
   | I16, Unsigned => Eunop Ocast16unsigned e
   | I32, _ => e
-  | IBool, _ => make_cmp_ne_zero e
+  | IBool, _ => make_cmpu_ne_zero e
   end.
 
 Definition make_cast (from to: type) (e: expr) :=
   match classify_cast from to with
-  | cast_case_neutral => OK e
+  | cast_case_pointer => OK e
   | cast_case_i2i sz2 si2 => OK (make_cast_int e sz2 si2)
   | cast_case_f2f => OK e
   | cast_case_s2s => OK e
@@ -161,10 +164,10 @@ Definition make_cast (from to: type) (e: expr) :=
   | cast_case_l2s si1 => OK (make_singleoflong e si1)
   | cast_case_f2l si2 => OK (make_longoffloat e si2)
   | cast_case_s2l si2 => OK (make_longofsingle e si2)
+  | cast_case_i2bool => OK (make_cmpu_ne_zero e)
   | cast_case_f2bool => OK (Ebinop (Ocmpf Cne) e (make_floatconst Float.zero))
   | cast_case_s2bool => OK (Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero))
-  | cast_case_l2bool => OK (Ebinop (Ocmpl Cne) e (make_longconst Int64.zero))
-  | cast_case_p2bool => OK (Ebinop (Ocmpu Cne) e (make_intconst Int.zero))
+  | cast_case_l2bool => OK (Ebinop (Ocmplu Cne) e (make_longconst Int64.zero))
   | cast_case_struct id1 id2 => OK e
   | cast_case_union id1 id2 => OK e
   | cast_case_void => OK e
@@ -176,11 +179,10 @@ Definition make_cast (from to: type) (e: expr) :=
 
 Definition make_boolean (e: expr) (ty: type) :=
   match classify_bool ty with
-  | bool_case_i => make_cmp_ne_zero e
+  | bool_case_i => make_cmpu_ne_zero e
   | bool_case_f => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero)
   | bool_case_s => Ebinop (Ocmpfs Cne) e (make_singleconst Float32.zero)
-  | bool_case_p => Ebinop (Ocmpu Cne) e (make_intconst Int.zero)
-  | bool_case_l => Ebinop (Ocmpl Cne) e (make_longconst Int64.zero)
+  | bool_case_l => Ebinop (Ocmplu Cne) e (make_longconst Int64.zero)
   | bool_default => e   (**r should not happen *)
   end.
 
@@ -188,12 +190,11 @@ Definition make_boolean (e: expr) (ty: type) :=
 
 Definition make_notbool (e: expr) (ty: type) :=
   match classify_bool ty with
-  | bool_case_i => OK (Ebinop (Ocmp Ceq) e (make_intconst Int.zero))
+  | bool_case_i => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero))
   | bool_case_f => OK (Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero))
   | bool_case_s => OK (Ebinop (Ocmpfs Ceq) e (make_singleconst Float32.zero))
-  | bool_case_p => OK (Ebinop (Ocmpu Ceq) e (make_intconst Int.zero))
-  | bool_case_l => OK (Ebinop (Ocmpl Ceq) e (make_longconst Int64.zero))
-  | _ => Error (msg "Cshmgen.make_notbool")
+  | bool_case_l => OK (Ebinop (Ocmplu Ceq) e (make_longconst Int64.zero))
+  | bool_default => Error (msg "Cshmgen.make_notbool")
   end.
 
 Definition make_neg (e: expr) (ty: type) :=
@@ -202,7 +203,7 @@ Definition make_neg (e: expr) (ty: type) :=
   | neg_case_f => OK (Eunop Onegf e)
   | neg_case_s => OK (Eunop Onegfs e)
   | neg_case_l _ => OK (Eunop Onegl e)
-  | _ => Error (msg "Cshmgen.make_neg")
+  | neg_default => Error (msg "Cshmgen.make_neg")
   end.
 
 Definition make_absfloat (e: expr) (ty: type) :=
@@ -211,14 +212,14 @@ Definition make_absfloat (e: expr) (ty: type) :=
   | neg_case_f => OK (Eunop Oabsf e)
   | neg_case_s => OK (Eunop Oabsf (make_floatofsingle e))
   | neg_case_l sg => OK (Eunop Oabsf (make_floatoflong e sg))
-  | _ => Error (msg "Cshmgen.make_absfloat")
+  | neg_default => Error (msg "Cshmgen.make_absfloat")
   end.
 
 Definition make_notint (e: expr) (ty: type) :=
   match classify_notint ty with
   | notint_case_i _ => OK (Eunop Onotint e)
   | notint_case_l _ => OK (Eunop Onotl e)
-  | _ => Error (msg "Cshmgen.make_notint")
+  | notint_default => Error (msg "Cshmgen.make_notint")
   end.
 
 (** Binary operators *)
@@ -241,40 +242,52 @@ Definition make_binarith (iop iopu fop sop lop lopu: binary_operation)
 
 Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_add ty1 ty2 with
-  | add_case_pi ty =>
-      do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Oadd e1 (Ebinop Omul n e2))
-  | add_case_ip ty =>
+  | add_case_pi ty si =>
       do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Oadd e2 (Ebinop Omul n e1))
+      if Archi.ptr64 then
+        let n := make_longconst (Int64.repr sz) in
+        OK (Ebinop Oaddl e1 (Ebinop Omull n (make_longofint e2 si)))
+      else
+        let n := make_intconst (Int.repr sz) in
+        OK (Ebinop Oadd e1 (Ebinop Omul n e2))
   | add_case_pl ty =>
       do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2)))
-  | add_case_lp ty =>
-      do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1)))
+      if Archi.ptr64 then
+        let n := make_longconst (Int64.repr sz) in
+        OK (Ebinop Oaddl e1 (Ebinop Omull n e2))
+      else
+        let n := make_intconst (Int.repr sz) in
+        OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2)))
   | add_default =>
       make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2
   end.
 
 Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_sub ty1 ty2 with
-  | sub_case_pi ty =>
+  | sub_case_pi ty si =>
       do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Osub e1 (Ebinop Omul n e2))
+      if Archi.ptr64 then
+        let n := make_longconst (Int64.repr sz) in
+        OK (Ebinop Osubl e1 (Ebinop Omull n (make_longofint e2 si)))
+      else
+        let n := make_intconst (Int.repr sz) in
+        OK (Ebinop Osub e1 (Ebinop Omul n e2))
   | sub_case_pp ty =>
       do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Odiv (Ebinop Osub e1 e2) n)
+      if Archi.ptr64 then
+        let n := make_longconst (Int64.repr sz) in
+        OK (Ebinop Odivl (Ebinop Osubl e1 e2) n)
+      else
+        let n := make_intconst (Int.repr sz) in
+        OK (Ebinop Odiv (Ebinop Osub e1 e2) n)
   | sub_case_pl ty =>
       do sz <- sizeof ce ty;
-      let n := make_intconst (Int.repr sz) in
-      OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
+      if Archi.ptr64 then
+        let n := make_longconst (Int64.repr sz) in
+        OK (Ebinop Osubl e1 (Ebinop Omull n e2))
+      else
+        let n := make_intconst (Int.repr sz) in
+        OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
   | sub_default =>
       make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2
   end.
@@ -333,11 +346,20 @@ Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   | shift_default => Error (msg "Cshmgen.make_shr")
   end.
 
+Definition make_cmp_ptr (c: comparison) (e1 e2: expr) :=
+  Ebinop (if Archi.ptr64 then Ocmplu c else Ocmpu c) e1 e2.
+
 Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_cmp ty1 ty2 with
-  | cmp_case_pp => OK (Ebinop (Ocmpu c) e1 e2)
-  | cmp_case_pl => OK (Ebinop (Ocmpu c) e1 (Eunop Ointoflong e2))
-  | cmp_case_lp => OK (Ebinop (Ocmpu c) (Eunop Ointoflong e1) e2)
+  | cmp_case_pp => OK (make_cmp_ptr c e1 e2)
+  | cmp_case_pi si =>
+      OK (make_cmp_ptr c e1 (if Archi.ptr64 then make_longofint e2 si else e2))
+  | cmp_case_ip si =>
+      OK (make_cmp_ptr c (if Archi.ptr64 then make_longofint e1 si else e1) e2)
+  | cmp_case_pl =>
+      OK (make_cmp_ptr c e1 (if Archi.ptr64 then e2 else Eunop Ointoflong e2))
+  | cmp_case_lp =>
+      OK (make_cmp_ptr c (if Archi.ptr64 then e1 else Eunop Ointoflong e1) e2)
   | cmp_default =>
       make_binarith
         (Ocmp c) (Ocmpu c) (Ocmpf c) (Ocmpfs c) (Ocmpl c) (Ocmplu c)
@@ -421,7 +443,9 @@ Definition make_field_access (ce: composite_env) (ty: type) (f: ident) (a: expr)
           Error (MSG "Undefined struct " :: CTX id :: nil)
       | Some co =>
           do ofs <- field_offset ce f (co_members co);
-          OK (Ebinop Oadd a (make_intconst (Int.repr ofs)))
+          OK (if Archi.ptr64
+              then Ebinop Oaddl a (make_longconst (Int64.repr ofs))
+              else Ebinop Oadd a (make_intconst (Int.repr ofs)))
       end
   | Tunion id _ =>
       OK a
@@ -469,9 +493,9 @@ Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr
       do addr <- make_field_access ce (typeof b) i tb;
       make_load addr ty
   | Clight.Esizeof ty' ty =>
-      do sz <- sizeof ce ty'; OK(make_intconst (Int.repr sz))
+      do sz <- sizeof ce ty'; OK(make_ptrofsconst sz)
   | Clight.Ealignof ty' ty =>
-      do al <- alignof ce ty'; OK(make_intconst (Int.repr al))
+      do al <- alignof ce ty'; OK(make_ptrofsconst al)
   end
 
 (** [transl_lvalue a] returns the Csharpminor code that evaluates