Remove support for x86 32 bits

.github/workflows/build.yml

@@ -12,7 +12,7 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        target: [aarch64, arm, ppc, riscv, x86_32, x86_64]
+        target: [aarch64, arm, ppc, riscv, x86_64]
     env:
       target: ${{ matrix.target }}
       os: linux

Makefile

@@ -22,13 +22,7 @@ BUILDNR ?= $(buildnr)
 TAG ?= $(tag)
 BRANCH ?= $(branch)
 
-ifeq ($(wildcard $(ARCH)_$(BITSIZE)),)
-ARCHDIRS=$(ARCH)
-else
-ARCHDIRS=$(ARCH)_$(BITSIZE) $(ARCH)
-endif
-
-DIRS := lib common $(ARCHDIRS) backend cfrontend driver cparser
+DIRS := lib common $(ARCH) backend cfrontend driver cparser
 
 ifeq ($(CLIGHTGEN),true)
 DIRS += export

aarch64/Archi.v

@@ -23,9 +23,6 @@ Definition ptr64 := true.
 
 Definition big_endian := false.
 
-Definition align_int64 := 8%Z.
-Definition align_float64 := 8%Z.
-
 Definition splitlong := false.
 
 Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.

aarch64/Machregs.v

@@ -94,8 +94,6 @@ Module IndexedMreg <: INDEXED_TYPE.
   Qed.
 End IndexedMreg.
 
-Definition is_stack_reg (r: mreg) : bool := false.
-
 (** ** Names of registers *)
 
 Local Open Scope string_scope.

arm/Archi.v

@@ -24,9 +24,6 @@ Definition ptr64 := false.
 
 Parameter big_endian: bool.
 
-Definition align_int64 := 8%Z.
-Definition align_float64 := 8%Z.
-
 Definition splitlong := true.
 
 Lemma splitlong_ptr32: splitlong = true -> ptr64 = false.

arm/Conventions1.v

@@ -308,7 +308,7 @@ Definition loc_argument_acceptable (l: loc) : Prop :=
 Definition loc_argument_charact (ofs: Z) (l: loc) : Prop :=
   match l with
   | R r => is_callee_save r = false
-  | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1
+  | S Outgoing ofs' ty => ofs' >= ofs /\ (typealign ty | ofs')
   | _ => False
   end.
 
@@ -343,42 +343,42 @@ Proof.
   destruct a.
 - (* int *)
   destruct (zlt ir 4); destruct H.
-  subst. apply ireg_param_caller_save.
-  eapply IHtyl; eauto.
-  subst. split; [lia | auto].
-  eapply Y; eauto. lia.
+  + subst. apply ireg_param_caller_save.
+  + eapply IHtyl; eauto.
+  + subst. split; simpl. lia. apply Z.divide_1_l.
+  + eapply Y; eauto. lia.
 - (* float *)
   destruct (zlt fr 8); destruct H.
-  subst. apply freg_param_caller_save.
-  eapply IHtyl; eauto.
-  subst. split. apply Z.le_ge. apply align_le. lia. auto.
-  eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; lia. lia.
+  + subst. apply freg_param_caller_save.
+  + eapply IHtyl; eauto.
+  + subst. split. apply Z.le_ge. apply align_le. lia. apply align_divides. lia.
+  + eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; lia. lia.
 - (* long *)
   set (ir' := align ir 2) in *.
   assert (ofs <= align ofs 2) by (apply align_le; lia).
-  destruct (zlt ir' 4).
-  destruct H. subst p. split; apply ireg_param_caller_save.
-  eapply IHtyl; eauto.
-  destruct H. subst p. split; destruct Archi.big_endian; (split; [ lia | auto ]).
-  eapply Y. eapply IHtyl; eauto. lia.
+  destruct (zlt ir' 4); destruct H.
+  + subst p. split; apply ireg_param_caller_save.
+  + eapply IHtyl; eauto.
+  + subst p. split; destruct Archi.big_endian; (split; [ lia | apply Z.divide_1_l ]).
+  + eapply Y. eapply IHtyl; eauto. lia.
 - (* single *)
   destruct (zlt fr 8); destruct H.
-  subst. apply freg_param_caller_save.
-  eapply IHtyl; eauto.
-  subst. split; [lia|auto].
-  eapply Y; eauto. lia.
+  + subst. apply freg_param_caller_save.
+  + eapply IHtyl; eauto.
+  + subst. split; [lia | apply Z.divide_1_l].
+  + eapply Y; eauto. lia.
 - (* any32 *)
   destruct (zlt ir 4); destruct H.
-  subst. apply ireg_param_caller_save.
-  eapply IHtyl; eauto.
-  subst. split; [lia | auto].
-  eapply Y; eauto. lia.
+  + subst. apply ireg_param_caller_save.
+  + eapply IHtyl; eauto.
+  + subst. split; [lia | apply Z.divide_1_l].
+  + eapply Y; eauto. lia.
 - (* any64 *)
   destruct (zlt fr 8); destruct H.
-  subst. apply freg_param_caller_save.
-  eapply IHtyl; eauto.
-  subst. split. apply Z.le_ge. apply align_le. lia. auto.
-  eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; lia. lia.
+  + subst. apply freg_param_caller_save.
+  + eapply IHtyl; eauto.
+  + subst. split. apply Z.le_ge. apply align_le. lia. apply Z.divide_1_l.
+  + eapply Y; eauto. apply Z.le_trans with (align ofs 2). apply align_le; lia. lia.
 Qed.
 
 Remark loc_arguments_sf_charact:
@@ -396,43 +396,43 @@ Proof.
   destruct H.
   destruct (zlt ofs 0); subst p.
   apply ireg_param_caller_save.
-  split; [extlia|auto].
+  split; [extlia | apply Z.divide_1_l].
   eapply Y; eauto. lia.
 - (* float *)
   set (ofs' := align ofs 2) in *.
   assert (ofs <= ofs') by (apply align_le; lia).
   destruct H.
   destruct (zlt ofs' 0); subst p.
   apply freg_param_caller_save.
-  split; [extlia|auto].
+  split; [extlia | apply align_divides; lia].
   eapply Y. eapply IHtyl; eauto. lia.
 - (* long *)
   set (ofs' := align ofs 2) in *.
   assert (ofs <= ofs') by (apply align_le; lia).
   destruct H.
   destruct (zlt ofs' 0); subst p.
   split; apply ireg_param_caller_save.
-  split; destruct Archi.big_endian; (split; [extlia|auto]).
+  split; destruct Archi.big_endian; (split; [extlia|apply Z.divide_1_l]).
   eapply Y. eapply IHtyl; eauto. lia.
 - (* single *)
   destruct H.
   destruct (zlt ofs 0); subst p.
   apply freg_param_caller_save.
-  split; [extlia|auto].
+  split; [extlia | apply Z.divide_1_l].
   eapply Y; eauto. lia.
 - (* any32 *)
   destruct H.
   destruct (zlt ofs 0); subst p.
   apply ireg_param_caller_save.
-  split; [extlia|auto].
+  split; [extlia| apply Z.divide_1_l].
   eapply Y; eauto. lia.
 - (* any64 *)
   set (ofs' := align ofs 2) in *.
   assert (ofs <= ofs') by (apply align_le; lia).
   destruct H.
   destruct (zlt ofs' 0); subst p.
   apply freg_param_caller_save.
-  split; [extlia|auto].
+  split; [extlia | apply Z.divide_1_l].
   eapply Y. eapply IHtyl; eauto. lia.
 Qed.
 
@@ -441,9 +441,6 @@ Lemma loc_arguments_acceptable:
   In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p.
 Proof.
   unfold loc_arguments; intros.
-  assert (X: forall l, loc_argument_charact 0 l -> loc_argument_acceptable l).
-  { unfold loc_argument_charact, loc_argument_acceptable.
-    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 (proj_sig_args s) (-4)) -> forall_rpair loc_argument_acceptable p).

arm/Machregs.v

@@ -92,8 +92,6 @@ Module IndexedMreg <: INDEXED_TYPE.
   Qed.
 End IndexedMreg.
 
-Definition is_stack_reg (r: mreg) : bool := false.
-
 (** ** Names of registers *)
 
 Local Open Scope string_scope.

backend/Inliningproof.v

@@ -769,7 +769,6 @@ Proof.
     auto.
   destruct chunk; simpl in *; auto using Z.divide_1_l.
   apply H2; lia.
-  apply H2; lia.
 Qed.
 
 (** Preservation by external calls *)

backend/Locations.v

@@ -85,7 +85,7 @@ Definition typealign (ty: typ) : Z :=
   match ty with
   | Tint => 1
   | Tlong => 2
-  | Tfloat => 1
+  | Tfloat => 2
   | Tsingle => 1
   | Tany32 => 1
   | Tany64 => 1

backend/Regalloc.ml

@@ -85,11 +85,7 @@ let rec constrain_regs vl cl =
 let move v1 v2 k =
   if v1 = v2 then
     k
-  else if XTL.is_stack_reg v1 then begin
-    let t = new_temp (typeof v2) in Xmove(v1, t) :: Xmove(t, v2) :: k
-  end else if XTL.is_stack_reg v2 then begin
-    let t = new_temp (typeof v1) in Xmove(v1, t) :: Xmove(t, v2) :: k
-  end else
+  else
     Xmove(v1, v2) :: k
 
 let rec movelist vl1 vl2 k =
@@ -355,7 +351,7 @@ let rec vset_removeres r after =
 let live_before instr after =
   match instr with
   | Xmove(src, dst) | Xspill(src, dst) | Xreload(src, dst) ->
-      if VSet.mem dst after || XTL.is_stack_reg src
+      if VSet.mem dst after
       then VSet.add src (VSet.remove dst after)
       else after
   | Xparmove(srcs, dsts, itmp, ftmp) ->
@@ -432,7 +428,7 @@ let rec dce_parmove srcs dsts after =
   | [], [] -> [], []
   | src1 :: srcs, dst1 :: dsts ->
       let (srcs', dsts') = dce_parmove srcs dsts after in
-      if VSet.mem dst1 after || XTL.is_stack_reg src1
+      if VSet.mem dst1 after
       then (src1 :: srcs', dst1 :: dsts')
       else (srcs', dsts')
   | _, _ -> assert false
@@ -446,7 +442,7 @@ let rec keep_builtin_arg after = function
 let dce_instr instr after k =
   match instr with
   | Xmove(src, dst) ->
-      if VSet.mem dst after || XTL.is_stack_reg src
+      if VSet.mem dst after
       then instr :: k
       else k
   | Xparmove(srcs, dsts, itmp, ftmp) ->
@@ -521,23 +517,9 @@ let spill_costs f =
   let charge_ros amount ros =
     match ros with Coq_inl v -> charge amount 1 v | Coq_inr id -> () in
 
-  let force_stack_allocation v =
-    match v with
-    | L l -> ()
-    | V(r, ty) ->
-        let st = get_stats r in
-        assert (st.cost < max_int);
-        st.cost <- (-1) in
-
   let charge_instr = function
     | Xmove(src, dst) ->
-        if XTL.is_stack_reg src then
-          force_stack_allocation dst
-        else if XTL.is_stack_reg dst then
-          force_stack_allocation src
-        else begin
-          charge 1 1 src; charge 1 1 dst
-        end
+        charge 1 1 src; charge 1 1 dst
     | Xreload(src, dst) ->
         charge 1 1 src; charge max_int 1 dst
         (* dest must not be spilled! *)

backend/XTL.ml

@@ -69,12 +69,6 @@ let rec vlocpairs = function
   | One l :: ll -> L l :: vlocpairs ll
   | Twolong(l1, l2) :: ll -> L l1 :: L l2 :: vlocpairs ll
 
-(* Tests over variables *)
-
-let is_stack_reg = function
-  | L(R r) -> Machregs.is_stack_reg r
-  | _      -> false
-
 (* Sets of variables *)
 
 module VSet = Set.Make(struct type t = var let compare = compare end)

backend/XTL.mli

@@ -66,10 +66,6 @@ val vmreg: mreg -> var
 val vmregs: mreg list -> var list
 val vlocpairs: loc rpair list -> var list
 
-(* Tests over variables *)
-
-val is_stack_reg: var -> bool
-
 (* Sets of variables *)
 
 module VSet: Set.S with type elt = var

cfrontend/Ctypes.v

@@ -333,9 +333,9 @@ Fixpoint alignof (env: composite_env) (t: type) : Z :=
       | Tint I16 _ _ => 2
       | Tint I32 _ _ => 4
       | Tint IBool _ _ => 1
-      | Tlong _ _ => Archi.align_int64
+      | Tlong _ _ => 8
       | Tfloat F32 _ => 4
-      | Tfloat F64 _ => Archi.align_float64
+      | Tfloat F64 _ => 8
       | Tpointer _ _ => if Archi.ptr64 then 8 else 4
       | Tarray t' _ _ => alignof env t'
       | Tfunction _ _ _ => 1
@@ -363,10 +363,10 @@ Proof.
     exists 1%nat; auto.
     exists 2%nat; auto.
     exists 0%nat; auto.
-    unfold Archi.align_int64. destruct Archi.ptr64; ((exists 2%nat; reflexivity) || (exists 3%nat; reflexivity)).
+    exists 3%nat; auto.
   destruct f.
     exists 2%nat; auto.
-    unfold Archi.align_float64. destruct Archi.ptr64; ((exists 2%nat; reflexivity) || (exists 3%nat; reflexivity)).
+    exists 3%nat; auto.
   exists (if Archi.ptr64 then 3%nat else 2%nat); destruct Archi.ptr64; auto.
   apply IHt.
   exists 0%nat; auto.
@@ -435,14 +435,8 @@ Fixpoint naturally_aligned (t: type) : Prop :=
 Lemma sizeof_alignof_compat:
   forall env t, naturally_aligned t -> (alignof env t | sizeof env t).
 Proof.
-  induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl.
-- apply Z.divide_refl.
-- destruct i; apply Z.divide_refl.
-- exists (8 / Archi.align_int64). unfold Archi.align_int64; destruct Archi.ptr64; reflexivity.
-- destruct f. apply Z.divide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity.
-- apply Z.divide_refl.
+  induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl; auto using Z.divide_refl.
 - apply Z.divide_mul_l; auto.
-- apply Z.divide_refl.
 - destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r.
 - destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r.
 Qed.
@@ -1004,16 +998,10 @@ Proof.
     rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. lia.
     apply Z.divide_refl.
   }
-  induction ty; simpl.
-  apply Z.divide_refl.
-  apply Z.divide_refl.
-  apply Z.divide_refl.
-  apply Z.divide_refl.
-  apply Z.divide_refl.
-  apply Z.divide_mul_l. auto.
-  apply Z.divide_refl.
-  destruct (env!i). apply X. apply Z.divide_0_r.
-  destruct (env!i). apply X. apply Z.divide_0_r.
+  induction ty; simpl; auto using Z.divide_refl.
+- apply Z.divide_mul_l. auto.
+- destruct (env!i). apply X. apply Z.divide_0_r.
+- destruct (env!i). apply X. apply Z.divide_0_r.
 Qed.
 
 (** Type ranks *)

common/Globalenvs.v

@@ -1462,7 +1462,7 @@ Definition init_data_alignment (i: init_data) : Z :=
   | Init_int32 n => 4
   | Init_int64 n => 8
   | Init_float32 n => 4
-  | Init_float64 n => 4
+  | Init_float64 n => 8
   | Init_addrof symb ofs => if Archi.ptr64 then 8 else 4
   | Init_space n => 1
   end.

common/Memdata.v

@@ -92,7 +92,7 @@ Definition align_chunk (chunk: memory_chunk) : Z :=
   | Mint32 => 4
   | Mint64 => 8
   | Mfloat32 => 4
-  | Mfloat64 => 4
+  | Mfloat64 => 8
   | Many32 => 4
   | Many64 => 4
   end.