Update all the ports

aarch64/Conventions1.v

@@ -263,7 +263,7 @@ Definition fixed_arguments (s: signature) : Z :=
   when calling a function with signature [s].  *)
 
 Definition loc_arguments (s: signature) : list (rpair loc) :=
-  loc_arguments_rec s.(sig_args) (fixed_arguments s) 0 0 0.
+  loc_arguments_rec (proj_sig_args s) (fixed_arguments s) 0 0 0.
 
 (** Argument locations are either caller-save registers or [Outgoing]
   stack slots at nonnegative offsets. *)
@@ -375,12 +375,12 @@ Qed.
     normalization is needed.
  *)
 
-Definition return_value_needs_normalization (t: rettype) : bool :=
+Definition return_value_needs_normalization (t: xtype) : bool :=
   match Archi.abi with
   | Archi.Apple => false
   | Archi.AAPCS64 =>
       match t with
-      | Tbool | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true
+      | Xbool | Xint8signed | Xint8unsigned | Xint16signed | Xint16unsigned => true
       | _ => false
       end
   end.

arm/Asmexpand.ml

@@ -469,7 +469,7 @@ module FixupEABI = struct
     in fixup 0 tyl
 
   let fixup_arguments dir sg =
-    fixup_conventions dir sg.sig_args
+    fixup_conventions dir (proj_sig_args sg)
 
   let fixup_result dir sg =
     fixup_conventions dir (proj_sig_res sg :: [])
@@ -556,7 +556,7 @@ module FixupHF = struct
     if sg.sig_cc.cc_vararg <> None then
       FixupEABI.fixup_arguments dir sg
     else begin
-      let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in
+      let act = fixup_actions (Array.make 16 false) 0 (proj_sig_args sg) in
       match dir with
       | Outgoing -> fixup_outgoing act
       | Incoming -> fixup_incoming act

arm/Conventions1.v

@@ -288,11 +288,11 @@ Fixpoint loc_arguments_sf
 Definition loc_arguments (s: signature) : list (rpair loc) :=
   match Archi.abi with
   | Archi.Softfloat =>
-      loc_arguments_sf s.(sig_args) (-4)
+      loc_arguments_sf (proj_sig_args s) (-4)
   | Archi.Hardfloat =>
       if s.(sig_cc).(cc_vararg)
-      then loc_arguments_sf s.(sig_args) (-4)
-      else loc_arguments_hf s.(sig_args) 0 0 0
+      then loc_arguments_sf (proj_sig_args s) (-4)
+      else loc_arguments_hf (proj_sig_args s) 0 0 0
   end.
 
 (** Argument locations are either non-temporary registers or [Outgoing]
@@ -446,9 +446,9 @@ Proof.
     destruct l as [r | [] ofs ty]; auto. intros (A & B); split; auto. rewrite B; apply Z.divide_1_l. }
   assert (Y: forall p, forall_rpair (loc_argument_charact 0) p -> forall_rpair loc_argument_acceptable p).
   { destruct p0; simpl; intuition auto. }
-  assert (In p (loc_arguments_sf (sig_args s) (-4)) -> forall_rpair loc_argument_acceptable p).
+  assert (In p (loc_arguments_sf (proj_sig_args s) (-4)) -> forall_rpair loc_argument_acceptable p).
   { intros. exploit loc_arguments_sf_charact; eauto. }
-  assert (In p (loc_arguments_hf (sig_args s) 0 0 0) -> forall_rpair loc_argument_acceptable p).
+  assert (In p (loc_arguments_hf (proj_sig_args s) 0 0 0) -> forall_rpair loc_argument_acceptable p).
   { intros. exploit loc_arguments_hf_charact; eauto. }
   destruct Archi.abi; [ | destruct (cc_vararg (sig_cc s)) ]; auto.
 Qed.
@@ -466,5 +466,5 @@ Qed.
 
 (** No normalization needed. *)
 
-Definition return_value_needs_normalization (t: rettype) := false.
-Definition parameter_needs_normalization (t: rettype) := false.
+Definition return_value_needs_normalization (t: xtype) := false.
+Definition parameter_needs_normalization (t: xtype) := false.

cfrontend/Ctyping.v

@@ -1783,7 +1783,7 @@ Proof.
   constructor; unfold wt_int; auto.
 - destruct v; try contradiction; constructor; auto.
 - destruct f; destruct v; try contradiction; constructor.
-- destruct v; destruct Archi.ptr64 eqn:P64; try contradiction; constructor; auto.
+- destruct v; try contradiction; constructor; auto.
 - destruct v; contradiction || constructor.
 - destruct v; contradiction || constructor.
 - destruct v; contradiction || constructor.

powerpc/Asmexpand.ml

@@ -822,7 +822,7 @@ let expand_builtin_inline name args res =
 
 let set_cr6 sg =
   if (sg.sig_cc.cc_vararg <> None) || sg.sig_cc.cc_unproto then begin
-    if List.exists (function Tfloat | Tsingle -> true | _ -> false) sg.sig_args
+    if List.exists (function Xfloat | Xsingle -> true | _ -> false) sg.sig_args
     then emit (Pcreqv(CRbit_6, CRbit_6, CRbit_6))
     else emit (Pcrxor(CRbit_6, CRbit_6, CRbit_6))
   end
@@ -847,7 +847,7 @@ let expand_instruction instr =
       if variadic then begin
         emit (Pmflr GPR0);
         emit (Pbl(intern_string "__compcert_va_saveregs",
-                  {sig_args = []; sig_res = Tvoid; sig_cc = cc_default}));
+                  {sig_args = []; sig_res = Xvoid; sig_cc = cc_default}));
         emit (Pmtlr GPR0)
       end;
       current_function_stacksize := sz;

powerpc/Builtins1.v

@@ -19,6 +19,7 @@
 Require Import String Coqlib.
 Require Import AST Integers Floats Values.
 Require Import Builtins0.
+Local Open Scope asttyp_scope.
 
 Inductive platform_builtin : Type :=
   | BI_isel
@@ -48,15 +49,15 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
 Definition platform_builtin_sig (b: platform_builtin) : signature :=
   match b with
   | BI_isel | BI_uisel =>
-     mksignature (Tint :: Tint :: Tint :: nil) Tint cc_default
+     [Xint; Xint; Xint ---> Xint]
   | BI_isel64 | BI_uisel64 =>
-     mksignature (Tint :: Tlong :: Tlong :: nil) Tlong cc_default
+     [Xint; Xlong; Xlong ---> Xlong]
   | BI_bsel =>
-     mksignature (Tint :: Tint :: Tint :: nil) Tbool cc_default
+     [Xint; Xint; Xint ---> Xbool]
   | BI_mulhw | BI_mulhwu =>
-     mksignature (Tint :: Tint :: nil) Tint cc_default
+     [Xint; Xint ---> Xint]
   | BI_mulhd | BI_mulhdu =>
-     mksignature (Tlong :: Tlong :: nil) Tlong cc_default
+     [Xlong; Xlong ---> Xlong]
   end.
 
 Definition isel {A: Type} (c: int) (n1 n2: A) : A :=
@@ -68,17 +69,17 @@ Program Definition bsel (c n1 n2: int) : { n : int | n = Int.zero \/ n = Int.one
 Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
   match b with
   | BI_isel | BI_uisel =>
-    mkbuiltin_n3t Tint Tint Tint Tint isel
+    mkbuiltin_n3t Tint Tint Tint Xint isel
   | BI_isel64 | BI_uisel64 =>
-    mkbuiltin_n3t Tint Tlong Tlong Tlong isel
+    mkbuiltin_n3t Tint Tlong Tlong Xlong isel
   | BI_bsel =>
-    mkbuiltin_n3t Tint Tint Tint Tbool bsel
+    mkbuiltin_n3t Tint Tint Tint Xbool bsel
   | BI_mulhw =>
-    mkbuiltin_n2t Tint Tint Tint Int.mulhs
+    mkbuiltin_n2t Tint Tint Xint Int.mulhs
   | BI_mulhwu =>
-    mkbuiltin_n2t Tint Tint Tint Int.mulhu
+    mkbuiltin_n2t Tint Tint Xint Int.mulhu
   | BI_mulhd =>
-    mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs
+    mkbuiltin_n2t Tlong Tlong Xlong Int64.mulhs
   | BI_mulhdu =>
-    mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu
+    mkbuiltin_n2t Tlong Tlong Xlong Int64.mulhu
   end.

powerpc/Conventions1.v

@@ -260,7 +260,7 @@ Fixpoint loc_arguments_rec
   when calling a function with signature [s].  *)
 
 Definition loc_arguments (s: signature) : list (rpair loc) :=
-  loc_arguments_rec s.(sig_args) 0 0 0.
+  loc_arguments_rec (proj_sig_args s) 0 0 0.
 
 (** Argument locations are either caller-save registers or [Outgoing]
   stack slots at nonnegative offsets. *)
@@ -370,5 +370,5 @@ Qed.
 
 (** No normalization needed. *)
 
-Definition return_value_needs_normalization (t: rettype) := false.
-Definition parameter_needs_normalization (t: rettype) := false.
+Definition return_value_needs_normalization (t: xtype) := false.
+Definition parameter_needs_normalization (t: xtype) := false.

riscV/Asmexpand.ml

@@ -123,7 +123,7 @@ let fixup_gen single double sg =
         end
     | _, _ -> ()
   in
-    List.iter2 fixup sg.sig_args (Conventions1.loc_arguments sg)
+    List.iter2 fixup (proj_sig_args sg) (Conventions1.loc_arguments sg)
 
 let fixup_call sg =
   fixup_gen move_single_arg move_double_arg sg
@@ -394,7 +394,7 @@ let rec args_size l ri rf ofs =
    but not arguments passed in FP registers. *)
 
 let arguments_size sg =
-  let (ri, _, ofs) = args_size sg.sig_args 0 0 0 in
+  let (ri, _, ofs) = args_size (proj_sig_args sg) 0 0 0 in
   ri + ofs
 
 let save_arguments first_reg base_ofs =

riscV/Conventions1.v

@@ -320,7 +320,7 @@ Definition fixed_arguments (s: signature) : Z :=
   when calling a function with signature [s].  *)
 
 Definition loc_arguments (s: signature) : list (rpair loc) :=
-  loc_arguments_rec s.(sig_args) (fixed_arguments s) 0 0 0.
+  loc_arguments_rec (proj_sig_args s) (fixed_arguments s) 0 0 0.
 
 (** Argument locations are either non-temporary registers or [Outgoing]
   stack slots at nonnegative offsets. *)
@@ -434,5 +434,5 @@ Qed.
 
 (** No normalization needed. *)
 
-Definition return_value_needs_normalization (t: rettype) := false.
-Definition parameter_needs_normalization (t: rettype) := false.
+Definition return_value_needs_normalization (t: xtype) := false.
+Definition parameter_needs_normalization (t: xtype) := false.