diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 4ef34fe69a..296ce6e7c9 100644 --- a/.github/workflows/build.yml +++ b/.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 diff --git a/Makefile b/Makefile index 1626d11662..d44e3c3598 100644 --- a/Makefile +++ b/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 diff --git a/aarch64/Archi.v b/aarch64/Archi.v index e117625486..0a3c086da1 100644 --- a/aarch64/Archi.v +++ b/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. diff --git a/aarch64/Machregs.v b/aarch64/Machregs.v index 3687a744ad..72fd228d3c 100644 --- a/aarch64/Machregs.v +++ b/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. diff --git a/arm/Archi.v b/arm/Archi.v index 687053f3be..b13ef0f959 100644 --- a/arm/Archi.v +++ b/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. diff --git a/arm/Conventions1.v b/arm/Conventions1.v index dfb3372b2b..2e89f9a03a 100644 --- a/arm/Conventions1.v +++ b/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,7 +396,7 @@ 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 *. @@ -404,7 +404,7 @@ Proof. 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 *. @@ -412,19 +412,19 @@ Proof. 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 *. @@ -432,7 +432,7 @@ Proof. 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). diff --git a/arm/Machregs.v b/arm/Machregs.v index ab03af9a8e..07d9b46585 100644 --- a/arm/Machregs.v +++ b/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. diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 9334778a03..e0bc8842df 100644 --- a/backend/Inliningproof.v +++ b/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 *) diff --git a/backend/Locations.v b/backend/Locations.v index 0a9456ae78..e4ffc2f59f 100644 --- a/backend/Locations.v +++ b/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 diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 19aba4f683..850df53b8a 100644 --- a/backend/Regalloc.ml +++ b/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! *) diff --git a/backend/XTL.ml b/backend/XTL.ml index 843dccf8f0..6d0efb4fc0 100644 --- a/backend/XTL.ml +++ b/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) diff --git a/backend/XTL.mli b/backend/XTL.mli index 54988d4bb3..75515221cc 100644 --- a/backend/XTL.mli +++ b/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 diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 21a87fe485..932e1fe9fd 100644 --- a/cfrontend/Ctypes.v +++ b/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 *) diff --git a/common/Globalenvs.v b/common/Globalenvs.v index 7356ca31f2..3ad3045e23 100644 --- a/common/Globalenvs.v +++ b/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. diff --git a/common/Memdata.v b/common/Memdata.v index be8783d742..7f5f8cea6e 100644 --- a/common/Memdata.v +++ b/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. diff --git a/configure b/configure index 7e2d1d5061..ab7bee871b 100755 --- a/configure +++ b/configure @@ -49,8 +49,6 @@ Supported targets: armeb-eabi (ARM, EABI, big endian) armeb-eabihf (ARM, EABI using hardware FP registers, big endian) armeb-linux (ARM, EABI using hardware FP registers, big endian) - x86_32-linux (x86 32 bits, Linux) - x86_32-bsd (x86 32 bits, BSD) x86_64-linux (x86 64 bits, Linux) x86_64-bsd (x86 64 bits, BSD) x86_64-macos (x86 64 bits, MacOS X) @@ -61,7 +59,6 @@ Supported targets: aarch64-macos (AArch64, i.e. Apple silicon, MacOS) manual (edit configuration file by hand) -For x86 targets, the "x86_32-" prefix can also be written "ia32-" or "i386-". For x86 targets, the "x86_64-" prefix can also be written "amd64-". For AArch64 targets, the "aarch64-" prefix can also be written "arm64-". For RISC-V targets, the "rv32-" or "rv64-" prefix can also be written "riscv32-" or "riscv64-". @@ -182,8 +179,6 @@ case "$target" in arch="arm"; model="armv7r"; endianness="big"; bitsize=32;; armebv7m-*) arch="arm"; model="armv7m"; endianness="big"; bitsize=32;; - x86_32-*|ia32-*|i386-*) - arch="x86"; model="32sse2"; endianness="little"; bitsize=32;; x86_64-*|amd64-*) arch="x86"; model="64"; endianness="little"; bitsize=64;; powerpc-*|ppc-*) @@ -306,40 +301,6 @@ if test "$arch" = "powerpc"; then esac fi - -# -# x86 (32 bits) Target Configuration -# -if test "$arch" = "x86" -a "$bitsize" = "32"; then - - case "$target" in - bsd) - abi="standard" - cc="${toolprefix}cc" - cc_options="-m32" - casm="${toolprefix}cc" - casm_options="-m32 -c" - clinker="${toolprefix}cc" - clinker_options="-m32" - cprepro="${toolprefix}cc" - cprepro_options="-m32 -U__GNUC__ -E" - system="bsd" - ;; - linux) - abi="standard" - cc_options="-m32" - casm_options="-m32 -c" - clinker_options="-m32" - cprepro_options="-m32 -U__GNUC__ -E" - system="linux" - ;; - *) - echo "Error: invalid eabi/system '$target' for architecture IA32/X86_32." 1>&2 - echo "$usage" 1>&2 - exit 2;; - esac -fi - # # x86 (64 bits) Target Configuration # diff --git a/driver/Frontend.ml b/driver/Frontend.ml index 2355dce5c4..74178049ee 100644 --- a/driver/Frontend.ml +++ b/driver/Frontend.ml @@ -117,14 +117,7 @@ let init () = | "arm" -> if Configuration.is_big_endian then Machine.arm_bigendian else Machine.arm_littleendian - | "x86" -> if Configuration.model = "64" then - Machine.x86_64 - else - if Configuration.abi = "macos" - then Machine.x86_32_macos - else if Configuration.system = "bsd" - then Machine.x86_32_bsd - else Machine.x86_32 + | "x86" -> Machine.x86_64 | "riscV" -> if Configuration.model = "64" then Machine.rv64 else Machine.rv32 diff --git a/extraction/extraction.v b/extraction/extraction.v index 66f93fa185..7ae309254e 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -157,7 +157,7 @@ Separate Extraction Conventions1.allocatable_registers RTL.instr_defs RTL.instr_uses Machregs.mregs_for_operation Machregs.mregs_for_builtin - Machregs.two_address_op Machregs.is_stack_reg + Machregs.two_address_op Machregs.destroyed_at_indirect_call AST.signature_main Floats.Float32.from_parsed Floats.Float.from_parsed diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 5bb4cfe776..9f71f48c7f 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -24,9 +24,6 @@ Definition ptr64 := false. Definition big_endian := true. -Definition align_int64 := 8%Z. -Definition align_float64 := 8%Z. - (** Can we use the 64-bit extensions to the PowerPC architecture? *) Parameter ppc64 : bool. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index a82d7b7155..ade91894ed 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -303,7 +303,7 @@ Opaque list_nth_z. destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. lia. apply Z.divide_1_l. + subst. split. lia. apply align_divides; lia. eapply Y; eauto. lia. - (* long *) assert (ofs <= align ofs 2) by (apply align_le; lia). diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 373433623f..ef82703cc4 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -122,8 +122,6 @@ Module IndexedMreg <: INDEXED_TYPE. Qed. End IndexedMreg. -Definition is_stack_reg (r: mreg) : bool := false. - (** ** Names of registers *) Local Open Scope string_scope. diff --git a/riscV/Archi.v b/riscV/Archi.v index 52802f9c94..9405372f5a 100644 --- a/riscV/Archi.v +++ b/riscV/Archi.v @@ -24,9 +24,6 @@ Parameter ptr64 : bool. Definition big_endian := false. -Definition align_int64 := 8%Z. -Definition align_float64 := 8%Z. - Definition splitlong := negb ptr64. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. diff --git a/riscV/Machregs.v b/riscV/Machregs.v index 7299ccd8ac..58a2ab1073 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -125,8 +125,6 @@ Module IndexedMreg <: INDEXED_TYPE. Qed. End IndexedMreg. -Definition is_stack_reg (r: mreg) : bool := false. - (** ** Names of registers *) Local Open Scope string_scope. diff --git a/runtime/Makefile b/runtime/Makefile index a100656ebb..9ae5a8291e 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -2,14 +2,6 @@ include ../Makefile.config CFLAGS=-O1 -g -Wall -ifeq ($(ARCH),x86) -ifeq ($(MODEL),64) -ARCH=x86_64 -else -ARCH=x86_32 -endif -endif - ifeq ($(ARCH),powerpc) ifeq ($(MODEL),ppc64) ARCH=powerpc64 @@ -18,7 +10,7 @@ ARCH=powerpc64 endif endif -ifeq ($(ARCH),x86_64) +ifeq ($(ARCH),x86) OBJS=i64_dtou.o i64_utod.o i64_utof.o vararg.o else ifeq ($(ARCH),powerpc64) OBJS=i64_dtou.o i64_stof.o i64_utod.o i64_utof.o vararg.o diff --git a/runtime/x86_64/i64_dtou.S b/runtime/x86/i64_dtou.S similarity index 100% rename from runtime/x86_64/i64_dtou.S rename to runtime/x86/i64_dtou.S diff --git a/runtime/x86_64/i64_utod.S b/runtime/x86/i64_utod.S similarity index 100% rename from runtime/x86_64/i64_utod.S rename to runtime/x86/i64_utod.S diff --git a/runtime/x86_64/i64_utof.S b/runtime/x86/i64_utof.S similarity index 100% rename from runtime/x86_64/i64_utof.S rename to runtime/x86/i64_utof.S diff --git a/runtime/x86_64/sysdeps.h b/runtime/x86/sysdeps.h similarity index 100% rename from runtime/x86_64/sysdeps.h rename to runtime/x86/sysdeps.h diff --git a/runtime/x86_64/vararg.S b/runtime/x86/vararg.S similarity index 100% rename from runtime/x86_64/vararg.S rename to runtime/x86/vararg.S diff --git a/runtime/x86_32/i64_dtos.S b/runtime/x86_32/i64_dtos.S deleted file mode 100644 index ccc0013c91..0000000000 --- a/runtime/x86_32/i64_dtos.S +++ /dev/null @@ -1,60 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Conversion float -> signed long - -FUNCTION(__compcert_i64_dtos) - subl $4, %esp - // Change rounding mode to "round towards zero" - fnstcw 0(%esp) - movw 0(%esp), %ax - movb $12, %ah - movw %ax, 2(%esp) - fldcw 2(%esp) - // Convert - fldl 8(%esp) - fistpll 8(%esp) - // Restore rounding mode - fldcw 0(%esp) - // Load result in edx:eax - movl 8(%esp), %eax - movl 12(%esp), %edx - addl $4, %esp - ret -ENDFUNCTION(__compcert_i64_dtos) - diff --git a/runtime/x86_32/i64_dtou.S b/runtime/x86_32/i64_dtou.S deleted file mode 100644 index 1115328dc0..0000000000 --- a/runtime/x86_32/i64_dtou.S +++ /dev/null @@ -1,88 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Conversion float -> unsigned long - -FUNCTION(__compcert_i64_dtou) - subl $4, %esp - // Compare argument with 2^63 - fldl 8(%esp) - flds LC1 - fucomp - fnstsw %ax - sahf - jbe 1f // branch if not (ARG < 2^63) - // Argument < 2^63: convert as is - // Change rounding mode to "round towards zero" - fnstcw 0(%esp) - movw 0(%esp), %ax - movb $12, %ah - movw %ax, 2(%esp) - fldcw 2(%esp) - // Convert - fistpll 8(%esp) - movl 8(%esp), %eax - movl 12(%esp), %edx - // Restore rounding mode - fldcw 0(%esp) - addl $4, %esp - ret - // Argument > 2^63: offset ARG by -2^63, then convert, then offset RES by 2^63 -1: fsubs LC1 - // Change rounding mode to "round towards zero" - fnstcw 0(%esp) - movw 0(%esp), %ax - movb $12, %ah - movw %ax, 2(%esp) - fldcw 2(%esp) - // Convert - fistpll 8(%esp) - movl 8(%esp), %eax - movl 12(%esp), %edx - // Offset result by 2^63 - addl $0x80000000, %edx - // Restore rounding mode - fldcw 0(%esp) - addl $4, %esp - ret - - .p2align 2 -LC1: .long 0x5f000000 // 2^63 in single precision - -ENDFUNCTION(__compcert_i64_dtou) - \ No newline at end of file diff --git a/runtime/x86_32/i64_sar.S b/runtime/x86_32/i64_sar.S deleted file mode 100644 index d62d0d69e2..0000000000 --- a/runtime/x86_32/i64_sar.S +++ /dev/null @@ -1,60 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Shift right signed - -// Note: IA32 shift instructions treat their amount (in %cl) modulo 32 - -FUNCTION(__compcert_i64_sar) - movl 12(%esp), %ecx // ecx = shift amount, treated mod 64 - testb $32, %cl - jne 1f - // shift amount < 32 - movl 4(%esp), %eax - movl 8(%esp), %edx - shrdl %cl, %edx, %eax // eax = low(XH:XL >> amount) - sarl %cl, %edx // edx = XH >> amount (signed) - ret - // shift amount >= 32 -1: movl 8(%esp), %eax - movl %eax, %edx - sarl %cl, %eax // eax = XH >> (amount - 32) - sarl $31, %edx // edx = sign of X - ret -ENDFUNCTION(__compcert_i64_sar) - diff --git a/runtime/x86_32/i64_sdiv.S b/runtime/x86_32/i64_sdiv.S deleted file mode 100644 index 2da5706c09..0000000000 --- a/runtime/x86_32/i64_sdiv.S +++ /dev/null @@ -1,74 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Signed division - -FUNCTION(__compcert_i64_sdiv) - pushl %ebp - pushl %esi - pushl %edi - movl 20(%esp), %esi // esi = NH - movl %esi, %ebp // save sign of N in ebp - testl %esi, %esi - jge 1f // if N < 0, - negl 16(%esp) // N = -N - adcl $0, %esi - negl %esi - movl %esi, 20(%esp) -1: movl 28(%esp), %esi // esi = DH - xorl %esi, %ebp // sign of result in ebp - testl %esi, %esi - jge 2f // if D < 0, - negl 24(%esp) // D = -D - adcl $0, %esi - negl %esi - movl %esi, 28(%esp) -2: call GLOB(__compcert_i64_udivmod) - testl %ebp, %ebp // apply sign to result - jge 3f - negl %esi - adcl $0, %edi - negl %edi -3: movl %esi, %eax - movl %edi, %edx - popl %edi - popl %esi - popl %ebp - ret -ENDFUNCTION(__compcert_i64_sdiv) - diff --git a/runtime/x86_32/i64_shl.S b/runtime/x86_32/i64_shl.S deleted file mode 100644 index 78f32cd640..0000000000 --- a/runtime/x86_32/i64_shl.S +++ /dev/null @@ -1,59 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Shift left - -// Note: IA32 shift instructions treat their amount (in %cl) modulo 32 - -FUNCTION(__compcert_i64_shl) - movl 12(%esp), %ecx // ecx = shift amount, treated mod 64 - testb $32, %cl - jne 1f - // shift amount < 32 - movl 4(%esp), %eax - movl 8(%esp), %edx - shldl %cl, %eax, %edx // edx = high(XH:XL << amount) - shll %cl, %eax // eax = XL << amount - ret - // shift amount >= 32 -1: movl 4(%esp), %edx - shll %cl, %edx // edx = XL << (amount - 32) - xorl %eax, %eax // eax = 0 - ret -ENDFUNCTION(__compcert_i64_shl) - diff --git a/runtime/x86_32/i64_shr.S b/runtime/x86_32/i64_shr.S deleted file mode 100644 index 36d970fc8b..0000000000 --- a/runtime/x86_32/i64_shr.S +++ /dev/null @@ -1,59 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Shift right unsigned - -// Note: IA32 shift instructions treat their amount (in %cl) modulo 32 - -FUNCTION(__compcert_i64_shr) - movl 12(%esp), %ecx // ecx = shift amount, treated mod 64 - testb $32, %cl - jne 1f - // shift amount < 32 - movl 4(%esp), %eax - movl 8(%esp), %edx - shrdl %cl, %edx, %eax // eax = low(XH:XL >> amount) - shrl %cl, %edx // edx = XH >> amount - ret - // shift amount >= 32 -1: movl 8(%esp), %eax - shrl %cl, %eax // eax = XH >> (amount - 32) - xorl %edx, %edx // edx = 0 - ret -ENDFUNCTION(__compcert_i64_shr) - diff --git a/runtime/x86_32/i64_smod.S b/runtime/x86_32/i64_smod.S deleted file mode 100644 index f2069d69e7..0000000000 --- a/runtime/x86_32/i64_smod.S +++ /dev/null @@ -1,70 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Signed remainder - -FUNCTION(__compcert_i64_smod) - pushl %ebp - pushl %esi - pushl %edi - movl 20(%esp), %esi // esi = NH - movl %esi, %ebp // save sign of result in ebp - testl %esi, %esi - jge 1f // if N < 0, - negl 16(%esp) // N = -N - adcl $0, %esi - negl %esi - movl %esi, 20(%esp) -1: movl 28(%esp), %esi // esi = DH - testl %esi, %esi - jge 2f // if D < 0, - negl 24(%esp) // D = -D - adcl $0, %esi - negl %esi - movl %esi, 28(%esp) -2: call GLOB(__compcert_i64_udivmod) - testl %ebp, %ebp // apply sign to result - jge 3f - negl %eax - adcl $0, %edx - negl %edx -3: popl %edi - popl %esi - popl %ebp - ret -ENDFUNCTION(__compcert_i64_smod) diff --git a/runtime/x86_32/i64_smulh.S b/runtime/x86_32/i64_smulh.S deleted file mode 100644 index 618f40ba63..0000000000 --- a/runtime/x86_32/i64_smulh.S +++ /dev/null @@ -1,94 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris -// -// Copyright (c) 2016 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Multiply-high signed - -#define XL 12(%esp) -#define XH 16(%esp) -#define YL 20(%esp) -#define YH 24(%esp) - -// Hacker's Delight section 8.3: -// - compute high 64 bits of the unsigned product X * Y (see i64_umulh.S) -// - subtract X if Y < 0 -// - subtract Y if X < 0 - -FUNCTION(__compcert_i64_smulh) - pushl %esi - pushl %edi - movl XL, %eax - mull YL // EDX:EAX = 64-bit product XL.YL - movl %edx, %ecx - xorl %esi, %esi - xorl %edi, %edi // EDI:ESI:ECX accumulatesbits 127:32 of result - movl XH, %eax - mull YL // EDX:EAX = 64-bit product XH.YL - addl %eax, %ecx - adcl %edx, %esi - adcl $0, %edi - movl YH, %eax - mull XL // EDX:EAX = 64-bit product YH.XL - addl %eax, %ecx - adcl %edx, %esi - adcl $0, %edi - movl XH, %eax - mull YH // EDX:EAX = 64-bit product XH.YH - addl %eax, %esi - adcl %edx, %edi -// Here, EDI:ESI is the high 64 bits of the unsigned product X.Y - xorl %eax, %eax - xorl %edx, %edx - cmpl $0, XH - cmovl YL, %eax - cmovl YH, %edx // EDX:EAX = Y if X < 0, = 0 if X >= 0 - subl %eax, %esi - sbbl %edx, %edi // EDI:ESI -= Y if X < 0 - xorl %eax, %eax - xorl %edx, %edx - cmpl $0, YH - cmovl XL, %eax - cmovl XH, %edx // EDX:EAX = X if Y < 0, = 0 if Y >= 0 - subl %eax, %esi - sbbl %edx, %edi // EDI:ESI -= X if Y < 0 -// Now EDI:ESI contains the high 64 bits of the signed product X.Y - movl %esi, %eax - movl %edi, %edx - popl %edi - popl %esi - ret -ENDFUNCTION(__compcert_i64_smulh) diff --git a/runtime/x86_32/i64_stod.S b/runtime/x86_32/i64_stod.S deleted file mode 100644 index 8faf480f61..0000000000 --- a/runtime/x86_32/i64_stod.S +++ /dev/null @@ -1,49 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Conversion signed long -> double-precision float - -FUNCTION(__compcert_i64_stod) - fildll 4(%esp) - ret - // The result is in extended precision (80 bits) and therefore - // exact (64 bits of mantissa). It will be rounded to double - // precision by the caller, when transferring the result - // to an XMM register or a 64-bit stack slot. -ENDFUNCTION(__compcert_i64_stod) - diff --git a/runtime/x86_32/i64_stof.S b/runtime/x86_32/i64_stof.S deleted file mode 100644 index 4b5817ac9a..0000000000 --- a/runtime/x86_32/i64_stof.S +++ /dev/null @@ -1,49 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Conversion signed long -> single-precision float - -FUNCTION(__compcert_i64_stof) - fildll 4(%esp) - // The TOS is in extended precision and therefore exact. - // Force rounding to single precision - fstps 4(%esp) - flds 4(%esp) - ret -ENDFUNCTION(__compcert_i64_stof) - diff --git a/runtime/x86_32/i64_udiv.S b/runtime/x86_32/i64_udiv.S deleted file mode 100644 index c9ae64f62e..0000000000 --- a/runtime/x86_32/i64_udiv.S +++ /dev/null @@ -1,52 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Unsigned division - -FUNCTION(__compcert_i64_udiv) - pushl %ebp - pushl %esi - pushl %edi - call GLOB(__compcert_i64_udivmod) - movl %esi, %eax - movl %edi, %edx - popl %edi - popl %esi - popl %ebp - ret -ENDFUNCTION(__compcert_i64_udiv) diff --git a/runtime/x86_32/i64_udivmod.S b/runtime/x86_32/i64_udivmod.S deleted file mode 100644 index a5d42fa5b7..0000000000 --- a/runtime/x86_32/i64_udivmod.S +++ /dev/null @@ -1,104 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Division and remainder - -// Auxiliary function, never called directly from C code -// Input: 20(esp), 24(esp) is dividend N -// 28(esp), 32(esp) is divisor D -// Output: esi:edi is quotient Q -// eax:edx is remainder R -// ebp is preserved - -FUNCTION(__compcert_i64_udivmod) - cmpl $0, 32(%esp) // single-word divisor? (DH = 0) - jne 1f - // Special case 64 bits divided by 32 bits - movl 28(%esp), %ecx // divide NH by DL - movl 24(%esp), %eax // (will trap if D = 0) - xorl %edx, %edx - divl %ecx // eax = quotient, edx = remainder - movl %eax, %edi // high word of quotient in edi - movl 20(%esp), %eax // divide rem : NL by DL - divl %ecx // eax = quotient, edx = remainder - movl %eax, %esi // low word of quotient in esi */ - movl %edx, %eax // low word of remainder in eax - xorl %edx, %edx // high word of remainder is 0, in edx - ret - // The general case -1: movl 28(%esp), %ecx // esi:ecx = D - movl 32(%esp), %esi - movl 20(%esp), %eax // edx:eax = N - movl 24(%esp), %edx - // Scale D and N down, giving D' and N', until D' fits in 32 bits -2: shrl $1, %esi // shift D' right by one - rcrl $1, %ecx - shrl $1, %edx // shift N' right by one - rcrl $1, %eax - testl %esi, %esi // repeat until D'H = 0 - jnz 2b - // Divide N' by D' to get an approximate quotient - divl %ecx // eax = quotient, edx = remainder - movl %eax, %esi // save tentative quotient Q in esi - // Check for off by one quotient - // Compute Q * D -3: movl 32(%esp), %ecx - imull %esi, %ecx // ecx = Q * DH - movl 28(%esp), %eax - mull %esi // edx:eax = Q * DL - add %ecx, %edx // edx:eax = Q * D - jc 5f // overflow in addition means Q is too high - // Compare Q * D with N, computing the remainder in the process - movl %eax, %ecx - movl 20(%esp), %eax - subl %ecx, %eax - movl %edx, %ecx - movl 24(%esp), %edx - sbbl %ecx, %edx // edx:eax = N - Q * D - jnc 4f // no carry: N >= Q * D, we are fine - decl %esi // carry: N < Q * D, adjust Q down by 1 - addl 28(%esp), %eax // and remainder up by D - adcl 32(%esp), %edx - // Finished -4: xorl %edi, %edi // high half of quotient is 0 - ret - // Special case when Q * D overflows -5: decl %esi // adjust Q down by 1 - jmp 3b // and redo check & computation of remainder - -ENDFUNCTION(__compcert_i64_udivmod) diff --git a/runtime/x86_32/i64_umod.S b/runtime/x86_32/i64_umod.S deleted file mode 100644 index 241a687b33..0000000000 --- a/runtime/x86_32/i64_umod.S +++ /dev/null @@ -1,51 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Unsigned remainder - -FUNCTION(__compcert_i64_umod) - pushl %ebp - pushl %esi - pushl %edi - call GLOB(__compcert_i64_udivmod) - popl %edi - popl %esi - popl %ebp - ret -ENDFUNCTION(__compcert_i64_umod) - diff --git a/runtime/x86_32/i64_umulh.S b/runtime/x86_32/i64_umulh.S deleted file mode 100644 index 2dba097520..0000000000 --- a/runtime/x86_32/i64_umulh.S +++ /dev/null @@ -1,74 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris -// -// Copyright (c) 2016 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Multiply-high unsigned - -#define XL 12(%esp) -#define XH 16(%esp) -#define YL 20(%esp) -#define YH 24(%esp) - -// X * Y = 2^64 XH.YH + 2^32 (XH.YL + XL.YH) + XL.YL - -FUNCTION(__compcert_i64_umulh) - pushl %esi - pushl %edi - movl XL, %eax - mull YL // EDX:EAX = 64-bit product XL.YL - movl %edx, %ecx - xorl %esi, %esi - xorl %edi, %edi // EDI:ESI:ECX accumulate bits 127:32 of result - movl XH, %eax - mull YL // EDX:EAX = 64-bit product XH.YL - addl %eax, %ecx - adcl %edx, %esi - adcl $0, %edi - movl YH, %eax - mull XL // EDX:EAX = 64-bit product YH.XL - addl %eax, %ecx - adcl %edx, %esi - adcl $0, %edi - movl XH, %eax - mull YH // EDX:EAX = 64-bit product XH.YH - addl %esi, %eax - adcl %edi, %edx - popl %edi - popl %esi - ret -ENDFUNCTION(__compcert_i64_umulh) - diff --git a/runtime/x86_32/i64_utod.S b/runtime/x86_32/i64_utod.S deleted file mode 100644 index d7ec582f07..0000000000 --- a/runtime/x86_32/i64_utod.S +++ /dev/null @@ -1,55 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Conversion unsigned long -> double-precision float - -FUNCTION(__compcert_i64_utod) - fildll 4(%esp) // convert as if signed - cmpl $0, 8(%esp) // is argument >= 2^63? - jns 1f - fadds LC1 // adjust by 2^64 -1: ret - // The result is in extended precision (80 bits) and therefore - // exact (64 bits of mantissa). It will be rounded to double - // precision by the caller, when transferring the result - // to an XMM register or a 64-bit stack slot. - - .p2align 2 -LC1: .long 0x5f800000 // 2^64 in single precision - -ENDFUNCTION(__compcert_i64_utod) diff --git a/runtime/x86_32/i64_utof.S b/runtime/x86_32/i64_utof.S deleted file mode 100644 index 858caa37bb..0000000000 --- a/runtime/x86_32/i64_utof.S +++ /dev/null @@ -1,55 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for 64-bit integer arithmetic. IA32 version. - -#include "sysdeps.h" - -// Conversion unsigned long -> single-precision float - -FUNCTION(__compcert_i64_utof) - fildll 4(%esp) // convert as if signed - cmpl $0, 8(%esp) // is argument >= 2^63? - jns 1f - fadds LC1 // adjust by 2^64 - // The TOS is in extended precision and therefore exact. - // Force rounding to single precision -1: fstps 4(%esp) - flds 4(%esp) - ret - - .p2align 2 -LC1: .long 0x5f800000 // 2^64 in single precision - -ENDFUNCTION(__compcert_i64_utof) diff --git a/runtime/x86_32/sysdeps.h b/runtime/x86_32/sysdeps.h deleted file mode 100644 index c22ed7701d..0000000000 --- a/runtime/x86_32/sysdeps.h +++ /dev/null @@ -1,77 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// System dependencies - -#if defined(SYS_linux) || defined(SYS_bsd) - - .section .note.GNU-stack,"",%progbits - -#define GLOB(x) x -#define FUNCTION(f) \ - .text; \ - .globl f; \ - .align 16; \ -f: - -#define ENDFUNCTION(f) \ - .type f, @function; .size f, . - f - -#endif - -#if defined(SYS_macos) - -#define GLOB(x) _##x -#define FUNCTION(f) \ - .text; \ - .globl _##f; \ - .align 4; \ -_##f: - -#define ENDFUNCTION(f) - -#endif - -#if defined(SYS_cygwin) - -#define GLOB(x) _##x -#define FUNCTION(f) \ - .text; \ - .globl _##f; \ - .align 16; \ -_##f: - -#define ENDFUNCTION(f) - -#endif diff --git a/runtime/x86_32/vararg.S b/runtime/x86_32/vararg.S deleted file mode 100644 index 78666c7059..0000000000 --- a/runtime/x86_32/vararg.S +++ /dev/null @@ -1,81 +0,0 @@ -// ***************************************************************** -// -// The Compcert verified compiler -// -// Xavier Leroy, INRIA Paris-Rocquencourt -// -// Copyright (c) 2013 Institut National de Recherche en Informatique et -// en Automatique. -// -// Redistribution and use in source and binary forms, with or without -// modification, are permitted provided that the following conditions are met: -// * Redistributions of source code must retain the above copyright -// notice, this list of conditions and the following disclaimer. -// * Redistributions in binary form must reproduce the above copyright -// notice, this list of conditions and the following disclaimer in the -// documentation and/or other materials provided with the distribution. -// * Neither the name of the nor the -// names of its contributors may be used to endorse or promote products -// derived from this software without specific prior written permission. -// -// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS -// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT -// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR -// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, -// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, -// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR -// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF -// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING -// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS -// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. -// -// ********************************************************************* - -// Helper functions for variadic functions . IA32 version - -#include "sysdeps.h" - -// typedef void * va_list; -// unsigned int __compcert_va_int32(va_list * ap); -// unsigned long long __compcert_va_int64(va_list * ap); -// double __compcert_va_float64(va_list * ap); - -FUNCTION(__compcert_va_int32) - movl 4(%esp), %ecx // %ecx = ap parameter - movl 0(%ecx), %edx // %edx = current argument pointer - movl 0(%edx), %eax // load the int32 value there - addl $4, %edx // increment argument pointer by 4 - movl %edx, 0(%ecx) - ret -ENDFUNCTION(__compcert_va_int32) - -FUNCTION(__compcert_va_int64) - movl 4(%esp), %ecx // %ecx = ap parameter - movl 0(%ecx), %edx // %edx = current argument pointer - movl 0(%edx), %eax // load the int64 value there - movl 4(%edx), %edx - addl $8, 0(%ecx) // increment argument pointer by 8 - ret -ENDFUNCTION(__compcert_va_int64) - -FUNCTION(__compcert_va_float64) - movl 4(%esp), %ecx // %ecx = ap parameter - movl 0(%ecx), %edx // %edx = current argument pointer - fldl 0(%edx) // load the float64 value there - addl $8, %edx // increment argument pointer by 8 - movl %edx, 0(%ecx) - ret -ENDFUNCTION(__compcert_va_float64) - -FUNCTION(__compcert_va_composite) - movl 4(%esp), %ecx // %ecx = ap parameter - movl 8(%esp), %edx // %edx = size of composite in bytes - movl 0(%ecx), %eax // %eax = current argument pointer - leal 3(%eax, %edx), %edx // advance by size - andl $0xfffffffc, %edx // and round up to multiple of 4 - movl %edx, 0(%ecx) // update argument pointer - ret -ENDFUNCTION(__compcert_va_composite) - - diff --git a/test b/test index 081175df37..ddb2ea33a7 160000 --- a/test +++ b/test @@ -1 +1 @@ -Subproject commit 081175df374260304a5cd78dd3dfaded93dceb41 +Subproject commit ddb2ea33a776bb576edb79a4476b06280087fb84 diff --git a/tools/runner.sh b/tools/runner.sh index c2794feccf..4be55e8c6f 100755 --- a/tools/runner.sh +++ b/tools/runner.sh @@ -11,7 +11,6 @@ simu_armsf="qemu-arm -L /usr/arm-linux-gnueabi" simu_armhf="qemu-arm -L /usr/arm-linux-gnueabihf" simu_ppc32="qemu-ppc -L /usr/powerpc-linux-gnu -cpu G4" simu_rv64="qemu-riscv64 -L /usr/riscv64-linux-gnu" -# simu_x86_32="qemu-i386 -L /usr/i686-linux-gnu" # Fatal error @@ -58,18 +57,12 @@ System_install() { riscv,linux) Apt_install gcc-riscv64-linux-gnu ;; - x86_32,linux) - sudo apt-get update - sudo apt-get -y install gcc-multilib - ;; x86_64,linux) ;; aarch64,macos) ;; x86_64,macos) ;; - x86_32,windows) - ;; x86_64,windows) ;; esac @@ -104,9 +97,6 @@ Configure() { riscv,linux) ./configure $configopts -toolprefix riscv64-linux-gnu- rv64-linux ;; - x86_32,linux) - ./configure $configopts x86_32-linux - ;; x86_64,linux) ./configure $configopts -clightgen x86_64-linux ;; @@ -116,9 +106,6 @@ Configure() { x86_64,macos) ./configure $configopts x86_64-macos ;; - x86_32,windows) - ./configure $configopts x86_32-cygwin - ;; x86_64,windows) ./configure $configopts x86_64-cygwin ;; @@ -216,11 +203,6 @@ case "$target,$os" in 2) Rerun_test "$simu_rv64" "-fpic";; 3) Rerun_test "$simu_rv64" "-Os -fno-pie -no-pie";; esac;; - x86_32,*) - case "$1" in - 1) Run_test "" "";; - 2) Rerun_test "" "-Os";; - esac;; x86_64,*) case "$1" in 1) Run_test "" "";; diff --git a/x86_64/Archi.v b/x86/Archi.v similarity index 94% rename from x86_64/Archi.v rename to x86/Archi.v index 50cb16918c..7629292b2a 100644 --- a/x86_64/Archi.v +++ b/x86/Archi.v @@ -24,14 +24,11 @@ Definition ptr64 := true. Definition big_endian := false. -Definition align_int64 := 8%Z. -Definition align_float64 := 8%Z. - -Definition splitlong := negb ptr64. +Definition splitlong := false. Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. Proof. - unfold splitlong. destruct ptr64; simpl; congruence. + unfold splitlong, ptr64; congruence. Qed. Definition default_nan_64 := (true, iter_nat 51 _ xO xH). diff --git a/x86/Asm.v b/x86/Asm.v index 64a835e16a..82db3b653c 100644 --- a/x86/Asm.v +++ b/x86/Asm.v @@ -49,7 +49,6 @@ Inductive preg: Type := | PC: preg (**r program counter *) | IR: ireg -> preg (**r integer register *) | FR: freg -> preg (**r XMM register *) - | ST0: preg (**r top of FP stack *) | CR: crbit -> preg (**r bit of the flags register *) | RA: preg. (**r pseudo-reg representing return address *) @@ -122,10 +121,6 @@ Inductive instruction: Type := | Pmovss_fi (rd: freg) (n: float32) (**r [movss] (single 32-bit float) *) | Pmovss_fm (rd: freg) (a: addrmode) | Pmovss_mf (a: addrmode) (r1: freg) - | Pfldl_m (a: addrmode) (**r [fld] double precision *) - | Pfstpl_m (a: addrmode) (**r [fstp] double precision *) - | Pflds_m (a: addrmode) (**r [fld] simple precision *) - | Pfstps_m (a: addrmode) (**r [fstp] simple precision *) (** Moves with conversion *) | Pmovb_mr (a: addrmode) (rs: ireg) (**r [mov] (8-bit int) *) | Pmovw_mr (a: addrmode) (rs: ireg) (**r [mov] (16-bit int) *) @@ -417,7 +412,7 @@ Definition eval_addrmode64 (a: addrmode) (rs: regset) : val := end)). Definition eval_addrmode (a: addrmode) (rs: regset) : val := - if Archi.ptr64 then eval_addrmode64 a rs else eval_addrmode32 a rs. + eval_addrmode64 a rs. (** Performing a comparison *) @@ -581,10 +576,9 @@ Definition exec_load (chunk: memory_chunk) (m: mem) end. Definition exec_store (chunk: memory_chunk) (m: mem) - (a: addrmode) (rs: regset) (r1: preg) - (destroyed: list preg) := + (a: addrmode) (rs: regset) (r1: preg) := match Mem.storev chunk m (eval_addrmode a rs) (rs r1) with - | Some m' => Next (nextinstr_nf (undef_regs destroyed rs)) m' + | Some m' => Next (nextinstr_nf rs) m' | None => Stuck end. @@ -623,9 +617,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmovq_rm rd a => exec_load Mint64 m a rs rd | Pmovl_mr a r1 => - exec_store Mint32 m a rs r1 nil + exec_store Mint32 m a rs r1 | Pmovq_mr a r1 => - exec_store Mint64 m a rs r1 nil + exec_store Mint64 m a rs r1 | Pmovsd_ff rd r1 => Next (nextinstr (rs#rd <- (rs r1))) m | Pmovsd_fi rd n => @@ -633,26 +627,18 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pmovsd_fm rd a => exec_load Mfloat64 m a rs rd | Pmovsd_mf a r1 => - exec_store Mfloat64 m a rs r1 nil + exec_store Mfloat64 m a rs r1 | Pmovss_fi rd n => Next (nextinstr (rs#rd <- (Vsingle n))) m | Pmovss_fm rd a => exec_load Mfloat32 m a rs rd | Pmovss_mf a r1 => - exec_store Mfloat32 m a rs r1 nil - | Pfldl_m a => - exec_load Mfloat64 m a rs ST0 - | Pfstpl_m a => - exec_store Mfloat64 m a rs ST0 (ST0 :: nil) - | Pflds_m a => - exec_load Mfloat32 m a rs ST0 - | Pfstps_m a => - exec_store Mfloat32 m a rs ST0 (ST0 :: nil) + exec_store Mfloat32 m a rs r1 (** Moves with conversion *) | Pmovb_mr a r1 => - exec_store Mint8unsigned m a rs r1 nil + exec_store Mint8unsigned m a rs r1 | Pmovw_mr a r1 => - exec_store Mint16unsigned m a rs r1 nil + exec_store Mint16unsigned m a rs r1 | Pmovzb_rr rd r1 => Next (nextinstr (rs#rd <- (Val.zero_ext 8 rs#r1))) m | Pmovzb_rm rd a => @@ -935,13 +921,13 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (rs#PC <- (rs#RA)) m (** Saving and restoring registers *) | Pmov_rm_a rd a => - exec_load (if Archi.ptr64 then Many64 else Many32) m a rs rd + exec_load Many64 m a rs rd | Pmov_mr_a a r1 => - exec_store (if Archi.ptr64 then Many64 else Many32) m a rs r1 nil + exec_store Many64 m a rs r1 | Pmovsd_fm_a rd a => exec_load Many64 m a rs rd | Pmovsd_mf_a a r1 => - exec_store Many64 m a rs r1 nil + exec_store Many64 m a rs r1 (** Pseudo-instructions *) | Plabel lbl => Next (nextinstr rs) m @@ -1052,7 +1038,6 @@ Definition preg_of (r: mreg) : preg := | X13 => FR XMM13 | X14 => FR XMM14 | X15 => FR XMM15 - | FP0 => ST0 end. (** Undefine all registers except SP and callee-save registers *) @@ -1216,7 +1201,6 @@ Definition data_preg (r: preg) : bool := | PC => false | IR _ => true | FR _ => true - | ST0 => true | CR _ => false | RA => false end. diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index bf7b8dea91..b0a830f7a6 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -114,11 +114,6 @@ let emit_leaq r addr = emit (Pleaq (r, addr)); emit (Paddq_ri (r, delta)) -(* Pseudo "lea" instruction for 32/64 bit compatibility *) - -let emit_lea r addr = - if Archi.ptr64 then emit_leaq r addr else emit (Pleal (r, addr)) - (* Translate a builtin argument into an addressing mode *) let addressing_of_builtin_arg = function @@ -136,7 +131,7 @@ let addressing_of_builtin_arg = function let expand_builtin_memcpy_small sz al src dst = let rec copy src dst sz = - if sz >= 8 && Archi.ptr64 then begin + if sz >= 8 then begin emit (Pmovq_rm (RCX, src)); emit (Pmovq_mr (dst, RCX)); copy (offset_addressing src _8z) (offset_addressing dst _8z) (sz - 8) @@ -160,8 +155,8 @@ let expand_builtin_memcpy_small sz al src dst = copy (addressing_of_builtin_arg src) (addressing_of_builtin_arg dst) sz let expand_builtin_memcpy_big sz al src dst = - if src <> BA (IR RSI) then emit_lea RSI (addressing_of_builtin_arg src); - if dst <> BA (IR RDI) then emit_lea RDI (addressing_of_builtin_arg dst); + if src <> BA (IR RSI) then emit_leaq RSI (addressing_of_builtin_arg src); + if dst <> BA (IR RDI) then emit_leaq RDI (addressing_of_builtin_arg dst); (* TODO: movsq? *) emit (Pmovl_ri (RCX,coqint_of_camlint (Int32.of_int (sz / 4)))); emit Prep_movsl; @@ -190,15 +185,6 @@ let expand_builtin_vload_common chunk addr res = emit (Pmovl_rm (res,addr)) | Mint64, BR(IR res) -> emit (Pmovq_rm (res,addr)) - | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) -> - let addr' = offset_addressing addr _4z in - if not (Asmgen.addressing_mentions addr res2) then begin - emit (Pmovl_rm (res2,addr)); - emit (Pmovl_rm (res1,addr')) - end else begin - emit (Pmovl_rm (res1,addr')); - emit (Pmovl_rm (res2,addr)) - end | Mfloat32, BR(FR res) -> emit (Pmovss_fm (res,addr)) | Mfloat64, BR(FR res) -> @@ -213,15 +199,10 @@ let expand_builtin_vload chunk args res = | _ -> assert false -let expand_builtin_vstore_common chunk addr src tmp = +let expand_builtin_vstore_common chunk addr src = match chunk, src with | (Mbool | Mint8signed | Mint8unsigned), BA(IR src) -> - if Archi.ptr64 || Asmgen.low_ireg src then - emit (Pmovb_mr (addr,src)) - else begin - emit (Pmov_rr (tmp,src)); - emit (Pmovb_mr (addr,tmp)) - end + emit (Pmovb_mr (addr,src)) | (Mint16signed | Mint16unsigned), BA(IR src) -> emit (Pmovw_mr (addr,src)) | Mint32, BA(IR src) -> @@ -244,7 +225,6 @@ let expand_builtin_vstore chunk args = | [addr; src] -> let addr = addressing_of_builtin_arg addr in expand_builtin_vstore_common chunk addr src - (if Asmgen.addressing_mentions addr RAX then RCX else RAX) | _ -> assert false (* Handling of varargs *) @@ -263,16 +243,6 @@ let rec next_arg_locations ir fr ofs = function let current_function_stacksize = ref 0L -let expand_builtin_va_start_32 r = - if not (is_current_function_variadic ()) then - invalid_arg "Fatal error: va_start used in non-vararg function"; - let ofs = - Int32.(add (add !PrintAsmaux.current_function_stacksize 4l) - (mul 4l (Z.to_int32 (Conventions.size_arguments - (get_current_function_sig ()))))) in - emit (Pleal (RAX, linear_addr RSP (Z.of_uint32 ofs))); - emit (Pmovl_mr (linear_addr r _0z, RAX)) - let expand_builtin_va_start_elf64 r = if not (is_current_function_variadic ()) then invalid_arg "Fatal error: va_start used in non-vararg function"; @@ -350,11 +320,6 @@ let expand_builtin_inline name args res = if a1 <> res then emit (Pmov_rr (res,a1)); emit (Pbswap64 res) - | "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> - assert (ah = RAX && al = RDX && rh = RDX && rl = RAX); - emit (Pbswap32 RAX); - emit (Pbswap32 RDX) | "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> if a1 <> res then emit (Pmov_rr (res,a1)); @@ -363,13 +328,8 @@ let expand_builtin_inline name args res = emit (Pbsrl (res,a1)); emit (Pxorl_ri(res,coqint_of_camlint 31l)) | "__builtin_clzl", [BA(IR a1)], BR(IR res) -> - if not(Archi.ptr64) then begin - emit (Pbsrl (res,a1)); - emit (Pxorl_ri(res,coqint_of_camlint 31l)) - end else begin - emit (Pbsrq (res,a1)); - emit (Pxorl_ri(res,coqint_of_camlint 63l)) - end + emit (Pbsrq (res,a1)); + emit (Pxorl_ri(res,coqint_of_camlint 63l)) | "__builtin_clzll", [BA(IR a1)], BR(IR res) -> emit (Pbsrq (res,a1)); emit (Pxorl_ri(res,coqint_of_camlint 63l)) @@ -388,10 +348,7 @@ let expand_builtin_inline name args res = | "__builtin_ctz", [BA(IR a1)], BR(IR res) -> emit (Pbsfl (res,a1)) | "__builtin_ctzl", [BA(IR a1)], BR(IR res) -> - if not(Archi.ptr64) then - emit (Pbsfl (res,a1)) - else - emit (Pbsfq (res,a1)) + emit (Pbsfq (res,a1)) | "__builtin_ctzll", [BA(IR a1)], BR(IR res) -> emit (Pbsfq (res,a1)) | "__builtin_ctzll", [BA_splitlong(BA (IR ah), BA (IR al))], BR(IR res) -> @@ -428,29 +385,6 @@ let expand_builtin_inline name args res = (fun r1 r2 r3 -> Pfnmsub132(r1, r2, r3)) (fun r1 r2 r3 -> Pfnmsub213(r1, r2, r3)) (fun r1 r2 r3 -> Pfnmsub231(r1, r2, r3)) - (* 64-bit integer arithmetic *) - | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> - assert (ah = RDX && al = RAX && rh = RDX && rl = RAX); - emit (Pnegl RAX); - emit (Padcl_ri (RDX,_0)); - emit (Pnegl RDX) - | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al)); - BA_splitlong(BA(IR bh), BA(IR bl))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> - assert (ah = RDX && al = RAX && bh = RCX && bl = RBX && rh = RDX && rl = RAX); - emit (Paddl_rr (RAX,RBX)); - emit (Padcl_rr (RDX,RCX)) - | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al)); - BA_splitlong(BA(IR bh), BA(IR bl))], - BR_splitlong(BR(IR rh), BR(IR rl)) -> - assert (ah = RDX && al = RAX && bh = RCX && bl = RBX && rh = RDX && rl = RAX); - emit (Psubl_rr (RAX,RBX)); - emit (Psbbl_rr (RDX,RCX)) - | "__builtin_mull", [BA(IR a); BA(IR b)], - BR_splitlong(BR(IR rh), BR(IR rl)) -> - assert (a = RAX && b = RDX && rh = RDX && rl = RAX); - emit (Pmull_r RDX) (* Memory accesses *) | "__builtin_read16_reversed", [BA(IR a1)], BR(IR res) -> emit (Pmovzw_rm (res, linear_addr a1 _0)); @@ -473,9 +407,9 @@ let expand_builtin_inline name args res = (* Vararg stuff *) | "__builtin_va_start", [BA(IR a)], _ -> assert (a = RDX); - if Archi.win64 then expand_builtin_va_start_win64 a - else if Archi.ptr64 then expand_builtin_va_start_elf64 a - else expand_builtin_va_start_32 a + if Archi.win64 + then expand_builtin_va_start_win64 a + else expand_builtin_va_start_elf64 a (* Synchronization *) | "__builtin_membar", [], _ -> () @@ -520,11 +454,9 @@ let fixup_funcall_win64 sg = copy_fregs_to_iregs (proj_sig_args sg) [XMM0; XMM1; XMM2; XMM3] [RCX; RDX; R8; R9] let fixup_funcall sg = - if Archi.ptr64 - then if Archi.win64 - then fixup_funcall_win64 sg - else fixup_funcall_elf64 sg - else () + if Archi.win64 + then fixup_funcall_win64 sg + else fixup_funcall_elf64 sg (* Expansion of instructions *) @@ -547,7 +479,7 @@ let expand_instruction instr = emit_leaq RAX addr1; emit (Pmovq_mr (addr2, RAX)); current_function_stacksize := Int64.of_int (sz + 8) - end else if Archi.ptr64 then begin + end else begin let (sz, save_regs) = sp_adjustment_elf64 sz in (* Allocate frame *) let sz' = Z.of_uint sz in @@ -566,29 +498,14 @@ let expand_instruction instr = emit_leaq RAX addr1; emit (Pmovq_mr (addr2, RAX)); current_function_stacksize := Int64.of_int fullsz - end else begin - let sz = sp_adjustment_32 sz in - (* Allocate frame *) - let sz' = Z.of_uint sz in - emit (Psubl_ri (RSP, sz')); - emit (Pcfi_adjust sz'); - (* Stack chaining *) - let addr1 = linear_addr RSP (Z.of_uint (sz + 4)) in - let addr2 = linear_addr RSP ofs_link in - emit (Pleal (RAX,addr1)); - emit (Pmovl_mr (addr2,RAX)); - PrintAsmaux.current_function_stacksize := Int32.of_int sz end | Pfreeframe(sz, ofs_ra, ofs_link) -> if Archi.win64 then begin let sz = sp_adjustment_win64 sz in emit (Paddq_ri (RSP, Z.of_uint sz)) - end else if Archi.ptr64 then begin + end else begin let (sz, _) = sp_adjustment_elf64 sz in emit (Paddq_ri (RSP, Z.of_uint sz)) - end else begin - let sz = sp_adjustment_32 sz in - emit (Paddl_ri (RSP, Z.of_uint sz)) end | Pjmp_s(_, sg) | Pjmp_r(_, sg) | Pcall_s(_, sg) | Pcall_r(_, sg) -> fixup_funcall sg; @@ -613,18 +530,7 @@ let expand_instruction instr = end | _ -> emit instr -let int_reg_to_dwarf_32 = function - | RAX -> 0 - | RBX -> 3 - | RCX -> 1 - | RDX -> 2 - | RSI -> 6 - | RDI -> 7 - | RBP -> 5 - | RSP -> 4 - | _ -> assert false - -let int_reg_to_dwarf_64 = function +let int_reg_to_dwarf = function | RAX -> 0 | RDX -> 1 | RCX -> 2 @@ -642,21 +548,7 @@ let int_reg_to_dwarf_64 = function | R14 -> 14 | R15 -> 15 -let int_reg_to_dwarf = - if Archi.ptr64 then int_reg_to_dwarf_64 else int_reg_to_dwarf_32 - -let float_reg_to_dwarf_32 = function - | XMM0 -> 21 - | XMM1 -> 22 - | XMM2 -> 23 - | XMM3 -> 24 - | XMM4 -> 25 - | XMM5 -> 26 - | XMM6 -> 27 - | XMM7 -> 28 - | _ -> assert false - -let float_reg_to_dwarf_64 = function +let float_reg_to_dwarf = function | XMM0 -> 17 | XMM1 -> 18 | XMM2 -> 19 @@ -674,9 +566,6 @@ let float_reg_to_dwarf_64 = function | XMM14 -> 31 | XMM15 -> 32 -let float_reg_to_dwarf = - if Archi.ptr64 then float_reg_to_dwarf_64 else float_reg_to_dwarf_32 - let preg_to_dwarf = function | IR r -> int_reg_to_dwarf r | FR r -> float_reg_to_dwarf r diff --git a/x86/Asmgen.v b/x86/Asmgen.v index 59f94df995..33cda68f34 100644 --- a/x86/Asmgen.v +++ b/x86/Asmgen.v @@ -23,8 +23,6 @@ Local Open Scope error_monad_scope. - Argument and result registers are of the correct type. - For two-address instructions, the result and the first argument are in the same register. (True by construction in [RTLgen], and preserved by [Reload].) -- The top of the floating-point stack ([ST0], a.k.a. [FP0]) can only - appear in [mov] instructions, but never in arithmetic instructions. All these properties are true by construction, but it is painful to track them statically. Instead, we recheck them during code generation and fail if they do not hold. *) @@ -60,30 +58,6 @@ Definition mk_shrxlimm (n: int) (k: code) : res code := Pleaq RAX (Addrmode (Some RAX) (Some(RDX, 1)) (inl _ 0)) :: Psarq_ri RAX n :: k). -Definition low_ireg (r: ireg) : bool := - match r with RAX | RBX | RCX | RDX => true | _ => false end. - -Definition mk_intconv (mk: ireg -> ireg -> instruction) (rd rs: ireg) (k: code) := - if Archi.ptr64 || low_ireg rs then - OK (mk rd rs :: k) - else - OK (Pmov_rr RAX rs :: mk rd RAX :: k). - -Definition addressing_mentions (addr: addrmode) (r: ireg) : bool := - match addr with Addrmode base displ const => - match base with Some r' => ireg_eq r r' | None => false end - || match displ with Some(r', sc) => ireg_eq r r' | None => false end - end. - -Definition mk_storebyte (addr: addrmode) (rs: ireg) (k: code) := - if Archi.ptr64 || low_ireg rs then - OK (Pmovb_mr addr rs :: k) - else if addressing_mentions addr RAX then - OK (Pleal RCX addr :: Pmov_rr RAX rs :: - Pmovb_mr (Addrmode (Some RCX) None (inl _ 0)) RAX :: k) - else - OK (Pmov_rr RAX rs :: Pmovb_mr addr RAX :: k). - (** Accessing slots in the stack frame. *) Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := @@ -92,11 +66,8 @@ Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := | Tint, IR r => OK (Pmovl_rm r a :: k) | Tlong, IR r => OK (Pmovq_rm r a :: k) | Tsingle, FR r => OK (Pmovss_fm r a :: k) - | Tsingle, ST0 => OK (Pflds_m a :: k) | Tfloat, FR r => OK (Pmovsd_fm r a :: k) - | Tfloat, ST0 => OK (Pfldl_m a :: k) - | Tany32, IR r => if Archi.ptr64 then Error (msg "Asmgen.loadind1") else OK (Pmov_rm_a r a :: k) - | Tany64, IR r => if Archi.ptr64 then OK (Pmov_rm_a r a :: k) else Error (msg "Asmgen.loadind2") + | Tany64, IR r => OK (Pmov_rm_a r a :: k) | Tany64, FR r => OK (Pmovsd_fm_a r a :: k) | _, _ => Error (msg "Asmgen.loadind") end. @@ -107,11 +78,8 @@ Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) : | Tint, IR r => OK (Pmovl_mr a r :: k) | Tlong, IR r => OK (Pmovq_mr a r :: k) | Tsingle, FR r => OK (Pmovss_mf a r :: k) - | Tsingle, ST0 => OK (Pfstps_m a :: k) | Tfloat, FR r => OK (Pmovsd_mf a r :: k) - | Tfloat, ST0 => OK (Pfstpl_m a :: k) - | Tany32, IR r => if Archi.ptr64 then Error (msg "Asmgen.storeind1") else OK (Pmov_mr_a a r :: k) - | Tany64, IR r => if Archi.ptr64 then OK (Pmov_mr_a a r :: k) else Error (msg "Asmgen.storeind2") + | Tany64, IR r => OK (Pmov_mr_a a r :: k) | Tany64, FR r => OK (Pmovsd_mf_a a r :: k) | _, _ => Error (msg "Asmgen.storeind") end. @@ -157,7 +125,7 @@ Definition normalize_addrmode_64 (a: addrmode) := then (a, None) else (Addrmode base ofs (inl _ 0), Some (Int64.repr n)) | Addrmode base ofs (inr (id, delta)) => - if Op.ptroffset_in_range delta || negb Archi.ptr64 + if Op.ptroffset_in_range delta then (a, None) else (Addrmode base ofs (inr _ (id, Ptrofs.zero)), Some (Ptrofs.to_int64 delta)) end. @@ -279,7 +247,7 @@ Definition testcond_for_condition (cond: condition) : extcond := (** Acting upon extended conditions. *) -Definition mk_setcc_base (cond: extcond) (rd: ireg) (k: code) := +Definition mk_setcc (cond: extcond) (rd: ireg) (k: code) := match cond with | Cond_base c => Psetcc c rd :: k @@ -293,11 +261,6 @@ Definition mk_setcc_base (cond: extcond) (rd: ireg) (k: code) := else Psetcc c1 RAX :: Psetcc c2 rd :: Porl_rr rd RAX :: k end. -Definition mk_setcc (cond: extcond) (rd: ireg) (k: code) := - if Archi.ptr64 || low_ireg rd - then mk_setcc_base cond rd k - else mk_setcc_base cond RAX (Pmov_rr rd RAX :: k). - Definition mk_jcc (cond: extcond) (lbl: label) (k: code) := match cond with | Cond_base c => Pjcc c lbl :: k @@ -358,9 +321,9 @@ Definition transl_op do r <- ireg_of res; OK (Pmov_rs r id :: k) | Ocast8signed, a1 :: nil => - do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovsb_rr r r1 k + do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pmovsb_rr r r1 :: k) | Ocast8unsigned, a1 :: nil => - do r1 <- ireg_of a1; do r <- ireg_of res; mk_intconv Pmovzb_rr r r1 k + do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pmovzb_rr r r1 :: k) | Ocast16signed, a1 :: nil => do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pmovsw_rr r r1 :: k) | Ocast16unsigned, a1 :: nil => @@ -673,7 +636,7 @@ Definition transl_store (chunk: memory_chunk) do am <- transl_addressing addr args; match chunk with | Mint8unsigned => - do r <- ireg_of src; mk_storebyte am r k + do r <- ireg_of src; OK (Pmovb_mr am r :: k) | Mint16unsigned => do r <- ireg_of src; OK(Pmovw_mr am r :: k) | Mint32 => diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v index 67c42b2ba4..908e389ab1 100644 --- a/x86/Asmgenproof.v +++ b/x86/Asmgenproof.v @@ -139,22 +139,6 @@ Proof. Qed. Hint Resolve mk_shrxlimm_label: labels. -Remark mk_intconv_label: - forall f r1 r2 k c, mk_intconv f r1 r2 k = OK c -> - (forall r r', nolabel (f r r')) -> - tail_nolabel k c. -Proof. - unfold mk_intconv; intros. TailNoLabel. -Qed. -Hint Resolve mk_intconv_label: labels. - -Remark mk_storebyte_label: - forall addr r k c, mk_storebyte addr r k = OK c -> tail_nolabel k c. -Proof. - unfold mk_storebyte; intros. TailNoLabel. -Qed. -Hint Resolve mk_storebyte_label: labels. - Remark loadind_label: forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> @@ -171,20 +155,11 @@ Proof. unfold storeind; intros. destruct ty; try discriminate; destruct (preg_of src); TailNoLabel. Qed. -Remark mk_setcc_base_label: - forall xc rd k, - tail_nolabel k (mk_setcc_base xc rd k). -Proof. - intros. destruct xc; simpl; destruct (ireg_eq rd RAX); TailNoLabel. -Qed. - Remark mk_setcc_label: forall xc rd k, tail_nolabel k (mk_setcc xc rd k). Proof. - intros. unfold mk_setcc. destruct (Archi.ptr64 || low_ireg rd). - apply mk_setcc_base_label. - eapply tail_nolabel_trans. apply mk_setcc_base_label. TailNoLabel. + intros. destruct xc; simpl; destruct (ireg_eq rd RAX); TailNoLabel. Qed. Remark mk_jcc_label: @@ -857,7 +832,7 @@ Transparent destroyed_by_jumptable. apply agree_nextinstr. eapply agree_change_sp; eauto. Transparent destroyed_at_function_entry. apply agree_undef_regs with rs0; eauto. - simpl; intros. apply Pregmap.gso; auto with asmgen. tauto. + simpl; intros. apply Pregmap.gso; auto with asmgen. congruence. intros. Simplifs. eapply agree_sp; eauto. diff --git a/x86/Asmgenproof1.v b/x86/Asmgenproof1.v index ba3d5281ad..340a70ca45 100644 --- a/x86/Asmgenproof1.v +++ b/x86/Asmgenproof1.v @@ -268,88 +268,6 @@ Proof. intros. unfold rs5; Simplifs. unfold rs4; Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs. Qed. -(** Smart constructor for integer conversions *) - -Lemma mk_intconv_correct: - forall mk sem rd rs k c rs1 m, - mk_intconv mk rd rs k = OK c -> - (forall c rd rs r m, - exec_instr ge c (mk rd rs) r m = Next (nextinstr (r#rd <- (sem r#rs))) m) -> - exists rs2, - exec_straight ge fn c rs1 m k rs2 m - /\ rs2#rd = sem rs1#rs - /\ forall r, data_preg r = true -> r <> rd -> r <> RAX -> rs2#r = rs1#r. -Proof. - unfold mk_intconv; intros. destruct (Archi.ptr64 || low_ireg rs); monadInv H. - econstructor. split. apply exec_straight_one. rewrite H0. eauto. auto. - split. Simplifs. intros. Simplifs. - econstructor. split. eapply exec_straight_two. - simpl. eauto. apply H0. auto. auto. - split. Simplifs. intros. Simplifs. -Qed. - -(** Smart constructor for small stores *) - -Lemma addressing_mentions_correct: - forall a r (rs1 rs2: regset), - (forall (r': ireg), r' <> r -> rs1 r' = rs2 r') -> - addressing_mentions a r = false -> - eval_addrmode32 ge a rs1 = eval_addrmode32 ge a rs2. -Proof. - intros until rs2; intro AG. unfold addressing_mentions, eval_addrmode32. - destruct a. intros. destruct (orb_false_elim _ _ H). unfold proj_sumbool in *. - decEq. destruct base; auto. apply AG. destruct (ireg_eq r i); congruence. - decEq. destruct ofs as [[r' sc] | ]; auto. rewrite AG; auto. destruct (ireg_eq r r'); congruence. -Qed. - -Lemma mk_storebyte_correct: - forall addr r k c rs1 m1 m2, - mk_storebyte addr r k = OK c -> - Mem.storev Mint8unsigned m1 (eval_addrmode ge addr rs1) (rs1 r) = Some m2 -> - exists rs2, - exec_straight ge fn c rs1 m1 k rs2 m2 - /\ forall r, data_preg r = true -> preg_notin r (if Archi.ptr64 then nil else AX :: CX :: nil) -> rs2#r = rs1#r. -Proof. - unfold mk_storebyte; intros. - destruct (Archi.ptr64 || low_ireg r) eqn:E. -(* low reg *) - monadInv H. econstructor; split. apply exec_straight_one. - simpl. unfold exec_store. rewrite H0. eauto. auto. - intros; Simplifs. -(* high reg *) - InvBooleans. rewrite H1; simpl. destruct (addressing_mentions addr RAX) eqn:E; monadInv H. -(* RAX is mentioned. *) - assert (r <> RCX). { red; intros; subst r; discriminate H2. } - set (rs2 := nextinstr (rs1#RCX <- (eval_addrmode32 ge addr rs1))). - set (rs3 := nextinstr (rs2#RAX <- (rs1 r))). - econstructor; split. - apply exec_straight_three with rs2 m1 rs3 m1. - simpl. auto. - simpl. replace (rs2 r) with (rs1 r). auto. symmetry. unfold rs2; Simplifs. - simpl. unfold exec_store. unfold eval_addrmode; rewrite H1; simpl. rewrite Int.add_zero. - change (rs3 RAX) with (rs1 r). - change (rs3 RCX) with (eval_addrmode32 ge addr rs1). - replace (Val.add (eval_addrmode32 ge addr rs1) (Vint Int.zero)) - with (eval_addrmode ge addr rs1). - rewrite H0. eauto. - unfold eval_addrmode in *; rewrite H1 in *. - destruct (eval_addrmode32 ge addr rs1); simpl in H0; try discriminate H0. - simpl. rewrite H1. rewrite Ptrofs.add_zero; auto. - auto. auto. auto. - intros. destruct H4. Simplifs. unfold rs3; Simplifs. unfold rs2; Simplifs. -(* RAX is not mentioned *) - set (rs2 := nextinstr (rs1#RAX <- (rs1 r))). - econstructor; split. - apply exec_straight_two with rs2 m1. - simpl. auto. - simpl. unfold exec_store. unfold eval_addrmode in *; rewrite H1 in *. - rewrite (addressing_mentions_correct addr RAX rs2 rs1); auto. - change (rs2 RAX) with (rs1 r). rewrite H0. eauto. - intros. unfold rs2; Simplifs. - auto. auto. - intros. destruct H3. simpl. Simplifs. unfold rs2; Simplifs. -Qed. - (** Accessing slots in the stack frame *) Remark eval_addrmode_indexed: @@ -358,9 +276,8 @@ Remark eval_addrmode_indexed: eval_addrmode ge (Addrmode (Some base) None (inl _ (Ptrofs.unsigned ofs))) rs = Val.offset_ptr rs#base ofs. Proof. intros. destruct (rs#base) eqn:BASE; try contradiction. - intros; unfold eval_addrmode; destruct Archi.ptr64 eqn:SF; simpl; rewrite BASE; simpl; rewrite SF; simpl. -- apply f_equal. apply f_equal. rewrite Int64.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs. -- apply f_equal. apply f_equal. rewrite Int.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs. + intros; unfold eval_addrmode; simpl; rewrite BASE; simpl. change Archi.ptr64 with true. + apply f_equal. apply f_equal. rewrite Int64.add_zero_l. rewrite <- (Ptrofs.repr_unsigned ofs) at 2. auto with ptrofs. Qed. Ltac loadind_correct_solve := @@ -386,7 +303,8 @@ Proof. { apply eval_addrmode_indexed. destruct (rs base); auto || discriminate. } rewrite <- H1 in H0. exists (nextinstr_nf (rs#(preg_of dst) <- v)); split. -- loadind_correct_solve; apply exec_straight_one; auto; simpl in *; unfold exec_load; rewrite ?Heqb, ?H0; auto. +- unfold chunk_of_type in H0. + destruct ty, (preg_of dst); inv H; apply exec_straight_one; auto; simpl; unfold exec_load; rewrite H0; auto. - intuition Simplifs. Qed. @@ -403,10 +321,10 @@ Proof. assert (eval_addrmode ge addr rs = Val.offset_ptr rs#base ofs). { apply eval_addrmode_indexed. destruct (rs base); auto || discriminate. } rewrite <- H1 in H0. - loadind_correct_solve; simpl in H0; - (econstructor; split; - [apply exec_straight_one; [simpl; unfold exec_store; rewrite ?Heqb, H0;eauto|auto] - |simpl; intros; unfold undef_regs; repeat Simplifs]). + exists (nextinstr_nf rs); split. +- unfold chunk_of_type in H0. + destruct ty, (preg_of src); inv H; apply exec_straight_one; auto; simpl; unfold exec_store; rewrite H0; auto. +- intros. Simplifs. Qed. (** Translation of addressing modes *) @@ -476,9 +394,7 @@ Lemma transl_addressing_mode_correct: eval_addressing ge (rs RSP) addr (List.map rs (List.map preg_of args)) = Some v -> Val.lessdef v (eval_addrmode ge am rs). Proof. - unfold eval_addressing, eval_addrmode; intros. destruct Archi.ptr64. eapply transl_addressing_mode_64_correct; eauto. - eapply transl_addressing_mode_32_correct; eauto. Qed. Lemma normalize_addrmode_32_correct: @@ -498,8 +414,7 @@ Proof. intros; destruct am as [base ofs [n|[id delta]]]; simpl. - destruct (offset_in_range n); auto; simpl. rewrite ! Val.addl_assoc. apply f_equal. apply f_equal. simpl. rewrite Int64.add_zero_l; auto. -- destruct Archi.ptr64 eqn:SF; auto; simpl; - destruct (ptroffset_in_range delta); auto. simpl. +- destruct (ptroffset_in_range delta); auto. simpl. rewrite ! Val.addl_assoc. apply f_equal. apply f_equal. rewrite <- Genv.shift_symbol_address_64 by auto. f_equal. rewrite Ptrofs.add_zero_l, Ptrofs.of_int64_to_int64 by auto. auto. @@ -1067,10 +982,10 @@ Proof. intros. unfold eval_testcond. repeat rewrite Pregmap.gso; auto with asmgen. Qed. -Lemma mk_setcc_base_correct: +Lemma mk_setcc_correct: forall cond rd k rs1 m, exists rs2, - exec_straight ge fn (mk_setcc_base cond rd k) rs1 m k rs2 m + exec_straight ge fn (mk_setcc cond rd k) rs1 m k rs2 m /\ rs2#rd = Val.of_optbool(eval_extcond cond rs1) /\ forall r, data_preg r = true -> r <> RAX /\ r <> RCX -> r <> rd -> rs2#r = rs1#r. Proof. @@ -1147,21 +1062,6 @@ Proof. intros. destruct H0; Simplifs. Qed. -Lemma mk_setcc_correct: - forall cond rd k rs1 m, - exists rs2, - exec_straight ge fn (mk_setcc cond rd k) rs1 m k rs2 m - /\ rs2#rd = Val.of_optbool(eval_extcond cond rs1) - /\ forall r, data_preg r = true -> r <> RAX /\ r <> RCX -> r <> rd -> rs2#r = rs1#r. -Proof. - intros. unfold mk_setcc. destruct (Archi.ptr64 || low_ireg rd). -- apply mk_setcc_base_correct. -- exploit mk_setcc_base_correct. intros [rs2 [A [B C]]]. - econstructor; split. eapply exec_straight_trans. eexact A. apply exec_straight_one. - simpl. eauto. simpl. auto. - intuition Simplifs. -Qed. - Definition negate_extcond (xc: extcond) : extcond := match xc with | Cond_base c => Cond_base (negate_testcond c) @@ -1307,10 +1207,6 @@ Transparent destroyed_by_op. apply SAME. destruct (Float.eq_dec n Float.zero). subst n. TranslOp. TranslOp. (* singleconst *) apply SAME. destruct (Float32.eq_dec n Float32.zero). subst n. TranslOp. TranslOp. -(* cast8signed *) - apply SAME. eapply mk_intconv_correct; eauto. -(* cast8unsigned *) - apply SAME. eapply mk_intconv_correct; eauto. (* mulhs *) apply SAME. TranslOp. destruct H1. Simplifs. (* mulhu *) @@ -1500,28 +1396,10 @@ Proof. unfold transl_store; intros. monadInv H. exploit transl_addressing_mode_correct; eauto. intro EA. assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto. - rewrite <- EA' in H1. destruct chunk; ArgsInv. -(* int8unsigned *) - eapply mk_storebyte_correct; eauto. -(* int16unsigned *) - econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto. - intros. Simplifs. -(* int32 *) - econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto. - intros. Simplifs. -(* int64 *) - econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto. - intros. Simplifs. -(* float32 *) - econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto. - intros. Transparent destroyed_by_store. simpl in H2. simpl. Simplifs. -(* float64 *) - econstructor; split. - apply exec_straight_one. simpl. unfold exec_store. rewrite H1. eauto. auto. + rewrite <- EA' in H1. + exists (nextinstr_nf rs); split. + destruct chunk; ArgsInv; apply exec_straight_one; simpl; auto; + unfold exec_store; rewrite H1; auto. intros. Simplifs. Qed. diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 2ef11ff41c..c0e74e8e9d 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -23,7 +23,7 @@ Require Import AST Machregs Locations. - Callee-save registers, whose value is preserved across a function call. - Caller-save registers that can be modified during a function call. - We follow the x86-32 and x86-64 application binary interfaces (ABI) + We follow the x86-64 application binary interfaces (ABI) in our choice of callee- and caller-save registers. *) @@ -31,38 +31,31 @@ Definition is_callee_save (r: mreg) : bool := match r with | AX | CX | DX => false | BX | BP => true - | SI | DI => negb Archi.ptr64 || Archi.win64 (**r callee-save in ELF 64 bits *) + | SI | DI => Archi.win64 (**r callee-save in ELF 64 bits *) | R8 | R9 | R10 | R11 => false | R12 | R13 | R14 | R15 => true | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => false | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => Archi.win64 - | FP0 => false end. Definition int_caller_save_regs := - if Archi.ptr64 - then if Archi.win64 - then AX :: CX :: DX :: R8 :: R9 :: R10 :: R11 :: nil - else AX :: CX :: DX :: SI :: DI :: R8 :: R9 :: R10 :: R11 :: nil - else AX :: CX :: DX :: nil. + if Archi.win64 + then AX :: CX :: DX :: R8 :: R9 :: R10 :: R11 :: nil + else AX :: CX :: DX :: SI :: DI :: R8 :: R9 :: R10 :: R11 :: nil. Definition float_caller_save_regs := - if Archi.ptr64 - then if Archi.win64 - then X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: nil - else X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: - X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil - else X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: nil. + if Archi.win64 + then X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: nil + else X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: + X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil. Definition int_callee_save_regs := - if Archi.ptr64 - then if Archi.win64 - then BX :: SI :: DI :: BP :: R12 :: R13 :: R14 :: R15 :: nil - else BX :: BP :: R12 :: R13 :: R14 :: R15 :: nil - else BX :: SI :: DI :: BP :: nil. + if Archi.win64 + then BX :: SI :: DI :: BP :: R12 :: R13 :: R14 :: R15 :: nil + else BX :: BP :: R12 :: R13 :: R14 :: R15 :: nil. Definition float_callee_save_regs := - if Archi.ptr64 && Archi.win64 + if Archi.win64 then X6 :: X7 :: X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 :: nil else nil. @@ -74,7 +67,7 @@ Definition is_float_reg (r: mreg) := | AX | BX | CX | DX | SI | DI | BP | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 => false | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 - | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 | FP0 => true + | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => true end. Definition dummy_int_reg := AX. (**r Used in [Regalloc]. *) @@ -119,39 +112,23 @@ Definition allocatable_registers (_: unit) := (** ** Location of function result *) -(** In 32 bit mode, the result value of a function is passed back to the - caller in registers [AX] or [DX:AX] or [FP0], depending on the type - of the returned value. We treat a function without result as a - function with one integer result. *) - -Definition loc_result_32 (s: signature) : rpair mreg := - match proj_sig_res s with - | Tint | Tany32 => One AX - | Tfloat | Tsingle => One FP0 - | Tany64 => One X0 - | Tlong => Twolong DX AX - end. - -(** In 64 bit mode, he result value of a function is passed back to +(** The result value of a function is passed back to the caller in registers [AX] or [X0]. *) -Definition loc_result_64 (s: signature) : rpair mreg := +Definition loc_result (s: signature) : rpair mreg := match proj_sig_res s with | Tint | Tlong | Tany32 | Tany64 => One AX | Tfloat | Tsingle => One X0 end. -Definition loc_result := - if Archi.ptr64 then loc_result_64 else loc_result_32. - (** The result registers have types compatible with that given in the signature. *) Lemma loc_result_type: forall sig, subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true. Proof. - intros. unfold loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (proj_sig_res sig); auto. + intros. unfold loc_result, mreg_type; + destruct (proj_sig_res sig); auto. Qed. (** The result locations are caller-save registers *) @@ -160,8 +137,8 @@ Lemma loc_result_caller_save: forall (s: signature), forall_rpair (fun r => is_callee_save r = false) (loc_result s). Proof. - intros. unfold loc_result, loc_result_32, loc_result_64, is_callee_save; - destruct Archi.ptr64; destruct (proj_sig_res s); simpl; auto. + intros. unfold loc_result, is_callee_save; + destruct (proj_sig_res s); simpl; auto. Qed. (** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *) @@ -177,9 +154,7 @@ Lemma loc_result_pair: end. Proof. intros. - unfold loc_result, loc_result_32, loc_result_64, mreg_type; - destruct Archi.ptr64; destruct (proj_sig_res sg); auto. - split; auto. congruence. + unfold loc_result, mreg_type; destruct (proj_sig_res sg); auto. Qed. (** The location of the result depends only on the result part of the signature *) @@ -187,26 +162,12 @@ Qed. Lemma loc_result_exten: forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. Proof. - intros. unfold loc_result, loc_result_32, loc_result_64, proj_sig_res. - destruct Archi.ptr64; rewrite H; auto. + intros. unfold loc_result, proj_sig_res. + rewrite H; auto. Qed. (** ** Location of function arguments *) -(** In the x86-32 ABI, all arguments are passed on stack. (Snif.) *) - -Fixpoint loc_arguments_32 - (tyl: list typ) (ofs: Z) {struct tyl} : list (rpair loc) := - match tyl with - | nil => nil - | ty :: tys => - match ty with - | Tlong => Twolong (S Outgoing (ofs + 1) Tint) (S Outgoing ofs Tint) - | _ => One (S Outgoing ofs ty) - end - :: loc_arguments_32 tys (ofs + typesize ty) - end. - (** In the x86-64 ELF ABI: - The first 6 integer arguments are passed in registers [DI], [SI], [DX], [CX], [R8], [R9]. - The first 8 floating-point arguments are passed in registers [X0] to [X7]. @@ -278,11 +239,9 @@ Fixpoint loc_arguments_win64 when calling a function with signature [s]. *) Definition loc_arguments (s: signature) : list (rpair loc) := - if Archi.ptr64 - then if Archi.win64 - then loc_arguments_win64 (proj_sig_args s) 0 0 - else loc_arguments_elf64 (proj_sig_args s) 0 0 0 - else loc_arguments_32 (proj_sig_args s) 0. + if Archi.win64 + then loc_arguments_win64 (proj_sig_args s) 0 0 + else loc_arguments_elf64 (proj_sig_args s) 0 0 0. (** Argument locations are either caller-save registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -294,12 +253,6 @@ Definition loc_argument_acceptable (l: loc) : Prop := | _ => False end. -Definition loc_argument_32_charact (ofs: Z) (l: loc) : Prop := - match l with - | S Outgoing ofs' ty => ofs' >= ofs /\ typealign ty = 1 - | _ => False - end. - Definition loc_argument_elf64_charact (ofs: Z) (l: loc) : Prop := match l with | R r => In r int_param_regs_elf64 \/ In r float_param_regs_elf64 @@ -314,21 +267,6 @@ Definition loc_argument_win64_charact (ofs: Z) (l: loc) : Prop := | _ => False end. -Remark loc_arguments_32_charact: - forall tyl ofs p, - In p (loc_arguments_32 tyl ofs) -> forall_rpair (loc_argument_32_charact ofs) p. -Proof. - assert (X: forall ofs1 ofs2 l, loc_argument_32_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_32_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } - induction tyl as [ | ty tyl]; simpl loc_arguments_32; intros. -- contradiction. -- destruct H. -+ destruct ty; subst p; simpl; lia. -+ apply IHtyl in H. generalize (typesize_pos ty); intros. destruct p; simpl in *. -* eapply X; eauto; lia. -* destruct H; split; eapply X; eauto; lia. -Qed. - Remark loc_arguments_elf64_charact: forall tyl ir fr ofs p, In p (loc_arguments_elf64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_elf64_charact ofs) p. @@ -409,9 +347,9 @@ Lemma loc_arguments_acceptable: forall (s: signature) (p: rpair loc), In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p. Proof. - unfold loc_arguments; intros. destruct Archi.ptr64 eqn:SF; [destruct Archi.win64 eqn:W64|]. + unfold loc_arguments; intros. destruct Archi.win64 eqn:W64. - (* WIN 64 bits *) - assert (A: forall r, In r int_param_regs_win64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF; decide_goal). + assert (A: forall r, In r int_param_regs_win64 -> is_callee_save r = false) by (unfold is_callee_save; decide_goal). assert (B: forall r, In r float_param_regs_win64 -> is_callee_save r = false) by (unfold is_callee_save; decide_goal). assert (X: forall l, loc_argument_win64_charact 0 l -> loc_argument_acceptable l). { unfold loc_argument_win64_charact, loc_argument_acceptable. @@ -422,7 +360,7 @@ Proof. exploit loc_arguments_win64_charact; eauto using Z.divide_0_r. unfold forall_rpair; destruct p; intuition auto. - (* ELF 64 bits *) - assert (A: forall r, In r int_param_regs_elf64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite SF, W64; decide_goal). + assert (A: forall r, In r int_param_regs_elf64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite W64; decide_goal). assert (B: forall r, In r float_param_regs_elf64 -> is_callee_save r = false) by (unfold is_callee_save; rewrite W64; decide_goal). assert (X: forall l, loc_argument_elf64_charact 0 l -> loc_argument_acceptable l). { unfold loc_argument_elf64_charact, loc_argument_acceptable. @@ -432,12 +370,6 @@ Proof. } exploit loc_arguments_elf64_charact; eauto using Z.divide_0_r. unfold forall_rpair; destruct p; intuition auto. - -- (* 32 bits *) - assert (X: forall l, loc_argument_32_charact 0 l -> loc_argument_acceptable l). - { destruct l as [r | [] ofs ty]; simpl; intuition auto. rewrite H2; apply Z.divide_1_l. } - exploit loc_arguments_32_charact; eauto. - unfold forall_rpair; destruct p; intuition auto. Qed. Global Hint Resolve loc_arguments_acceptable: locs. @@ -445,7 +377,7 @@ Global Hint Resolve loc_arguments_acceptable: locs. Lemma loc_arguments_main: loc_arguments signature_main = nil. Proof. - unfold loc_arguments; destruct Archi.ptr64; auto; destruct Archi.win64; auto. + unfold loc_arguments; destruct Archi.win64; auto. Qed. (** ** Normalization of function results and parameters *) diff --git a/x86/Machregs.v b/x86/Machregs.v index 20cc8db745..e2a74af997 100644 --- a/x86/Machregs.v +++ b/x86/Machregs.v @@ -28,12 +28,10 @@ Require Import AST Integers Op. Inductive mreg: Type := (** Allocatable integer regs *) | AX | BX | CX | DX | SI | DI | BP - | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 (**r only in 64-bit mode *) + | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 (** Allocatable float regs *) | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 - | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 (**r only in 64-bit mode *) - (** Special float reg *) - | FP0. + | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15. Lemma mreg_eq: forall (r1 r2: mreg), {r1 = r2} + {r1 <> r2}. Proof. decide equality. Defined. @@ -44,7 +42,7 @@ Definition all_mregs := :: R8 :: R9 :: R10 :: R11 :: R12 :: R13 :: R14 :: R15 :: X0 :: X1 :: X2 :: X3 :: X4 :: X5 :: X6 :: X7 :: X8 :: X9 :: X10 :: X11 :: X12 :: X13 :: X14 :: X15 - :: FP0 :: nil. + :: nil. Lemma all_mregs_complete: forall (r: mreg), In r all_mregs. @@ -62,11 +60,10 @@ Global Instance Finite_mreg : Finite mreg := { Definition mreg_type (r: mreg): typ := match r with - | AX | BX | CX | DX | SI | DI | BP => if Archi.ptr64 then Tany64 else Tany32 + | AX | BX | CX | DX | SI | DI | BP => Tany64 | R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 => Tany64 | X0 | X1 | X2 | X3 | X4 | X5 | X6 | X7 => Tany64 | X8 | X9 | X10 | X11 | X12 | X13 | X14 | X15 => Tany64 - | FP0 => Tany64 end. Local Open Scope positive_scope. @@ -80,7 +77,6 @@ Module IndexedMreg <: INDEXED_TYPE. | R8 => 8 | R9 => 9 | R10 => 10 | R11 => 11 | R12 => 12 | R13 => 13 | R14 => 14 | R15 => 15 | X0 => 16 | X1 => 17 | X2 => 18 | X3 => 19 | X4 => 20 | X5 => 21 | X6 => 22 | X7 => 23 | X8 => 24 | X9 => 25 | X10 => 26 | X11 => 27 | X12 => 28 | X13 => 29 | X14 => 30 | X15 => 31 - | FP0 => 32 end. Lemma index_inj: forall r1 r2, index r1 = index r2 -> r1 = r2. @@ -89,9 +85,6 @@ Module IndexedMreg <: INDEXED_TYPE. Qed. End IndexedMreg. -Definition is_stack_reg (r: mreg) : bool := - match r with FP0 => true | _ => false end. - (** ** Names of registers *) Local Open Scope string_scope. @@ -107,7 +100,7 @@ Definition register_names := ("XMM4", X4) :: ("XMM5", X5) :: ("XMM6", X6) :: ("XMM7", X7) :: ("XMM8", X8) :: ("XMM9", X9) :: ("XMM10", X10) :: ("XMM11", X11) :: ("XMM12", X12) :: ("XMM13", X13) :: ("XMM14", X14) :: ("XMM15", X15) :: - ("ST0", FP0) :: nil. + nil. Definition register_by_name (s: string) : option mreg := let fix assoc (l: list (string * mreg)) : option mreg := @@ -144,10 +137,7 @@ Definition destroyed_by_load (chunk: memory_chunk) (addr: addressing): list mreg nil. Definition destroyed_by_store (chunk: memory_chunk) (addr: addressing): list mreg := - match chunk with - | Mbool | Mint8signed | Mint8unsigned => if Archi.ptr64 then nil else AX :: CX :: nil - | _ => nil - end. + nil. Definition destroyed_by_cond (cond: condition): list mreg := nil. @@ -169,8 +159,6 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := match ef with | EF_memcpy sz al => if zle sz 32 then CX :: X7 :: nil else CX :: SI :: DI :: nil - | EF_vstore (Mint8unsigned|Mint8signed) => - if Archi.ptr64 then nil else AX :: CX :: nil | EF_builtin name sg => if string_dec name "__builtin_va_start" then AX :: nil else if string_dec name "__builtin_write16_reversed" @@ -183,13 +171,10 @@ Definition destroyed_by_builtin (ef: external_function): list mreg := Definition destroyed_at_function_entry: list mreg := (* must include [destroyed_by_setstack ty] *) - AX :: FP0 :: nil. + AX :: nil. Definition destroyed_by_setstack (ty: typ): list mreg := - match ty with - | Tfloat | Tsingle => FP0 :: nil - | _ => nil - end. + nil. Definition destroyed_at_indirect_call: list mreg := AX :: nil. @@ -236,8 +221,6 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list (Some AX :: Some DX :: nil, Some DX :: Some AX :: nil) else if string_dec name "__builtin_va_start" then (Some DX :: nil, nil) - else if (negb Archi.ptr64) && string_dec name "__builtin_bswap64" then - (Some AX :: Some DX :: nil, Some DX :: Some AX :: nil) else (nil, nil) | _ => (nil, nil) diff --git a/x86/SelectLong.vp b/x86/SelectLong.vp index b213e23f87..a49d4d5c08 100644 --- a/x86/SelectLong.vp +++ b/x86/SelectLong.vp @@ -21,43 +21,34 @@ Require Import SelectOp SplitLong. Local Open Scope cminorsel_scope. Local Open Scope string_scope. -Section SELECT. - -Context {hf: helper_functions}. - Definition longconst (n: int64) : expr := - if Archi.splitlong then SplitLong.longconst n else Eop (Olongconst n) Enil. + Eop (Olongconst n) Enil. Definition is_longconst (e: expr) := - if Archi.splitlong then SplitLong.is_longconst e else match e with | Eop (Olongconst n) Enil => Some n | _ => None end. Definition intoflong (e: expr) := - if Archi.splitlong then SplitLong.intoflong e else match is_longconst e with | Some n => Eop (Ointconst (Int.repr (Int64.unsigned n))) Enil | None => Eop Olowlong (e ::: Enil) end. Definition longofint (e: expr) := - if Archi.splitlong then SplitLong.longofint e else match is_intconst e with | Some n => longconst (Int64.repr (Int.signed n)) | None => Eop Ocast32signed (e ::: Enil) end. Definition longofintu (e: expr) := - if Archi.splitlong then SplitLong.longofintu e else match is_intconst e with | Some n => longconst (Int64.repr (Int.unsigned n)) | None => Eop Ocast32unsigned (e ::: Enil) end. Nondetfunction notl (e: expr) := - if Archi.splitlong then SplitLong.notl e else match e with | Eop (Olongconst n) Enil => longconst (Int64.not n) | Eop Onotl (t1:::Enil) => t1 @@ -77,7 +68,6 @@ Nondetfunction andlimm (n1: int64) (e2: expr) := end. Nondetfunction andl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.andl e1 e2 else match e1, e2 with | Eop (Olongconst n1) Enil, t2 => andlimm n1 t2 | t1, Eop (Olongconst n2) Enil => andlimm n2 t1 @@ -94,7 +84,6 @@ Nondetfunction orlimm (n1: int64) (e2: expr) := end. Nondetfunction orl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.orl e1 e2 else match e1, e2 with | Eop (Olongconst n1) Enil, t2 => orlimm n1 t2 | t1, Eop (Olongconst n2) Enil => orlimm n2 t1 @@ -121,7 +110,6 @@ Nondetfunction xorlimm (n1: int64) (e2: expr) := end. Nondetfunction xorl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.xorl e1 e2 else match e1, e2 with | Eop (Olongconst n1) Enil, t2 => xorlimm n1 t2 | t1, Eop (Olongconst n2) Enil => xorlimm n2 t1 @@ -129,7 +117,6 @@ Nondetfunction xorl (e1: expr) (e2: expr) := end. Nondetfunction shllimm (e1: expr) (n: int) := - if Archi.splitlong then SplitLong.shllimm e1 n else if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int64.iwordsize') then Eop Oshll (e1:::Eop (Ointconst n) Enil:::Enil) @@ -153,7 +140,6 @@ Nondetfunction shllimm (e1: expr) (n: int) := end. Nondetfunction shrluimm (e1: expr) (n: int) := - if Archi.splitlong then SplitLong.shrluimm e1 n else if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int64.iwordsize') then Eop Oshrlu (e1:::Eop (Ointconst n) Enil:::Enil) @@ -170,7 +156,6 @@ Nondetfunction shrluimm (e1: expr) (n: int) := end. Nondetfunction shrlimm (e1: expr) (n: int) := - if Archi.splitlong then SplitLong.shrlimm e1 n else if Int.eq n Int.zero then e1 else if negb (Int.ltu n Int64.iwordsize') then Eop Oshrl (e1:::Eop (Ointconst n) Enil:::Enil) @@ -187,21 +172,18 @@ Nondetfunction shrlimm (e1: expr) (n: int) := end. Definition shll (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.shll e1 e2 else match is_intconst e2 with | Some n2 => shllimm e1 n2 | None => Eop Oshll (e1:::e2:::Enil) end. Definition shrl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.shrl e1 e2 else match is_intconst e2 with | Some n2 => shrlimm e1 n2 | None => Eop Oshrl (e1:::e2:::Enil) end. Definition shrlu (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.shrlu e1 e2 else match is_intconst e2 with | Some n2 => shrluimm e1 n2 | _ => Eop Oshrlu (e1:::e2:::Enil) @@ -216,7 +198,6 @@ Nondetfunction addlimm (n: int64) (e: expr) := end. Nondetfunction addl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.addl e1 e2 else match e1, e2 with | Eop (Olongconst n1) Enil, t2 => addlimm n1 t2 | t1, Eop (Olongconst n2) Enil => addlimm n2 t1 @@ -239,14 +220,12 @@ Nondetfunction addl (e1: expr) (e2: expr) := end. Definition negl (e: expr) := - if Archi.splitlong then SplitLong.negl e else match is_longconst e with | Some n => longconst (Int64.neg n) | None => Eop Onegl (e ::: Enil) end. Nondetfunction subl (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.subl e1 e2 else match e1, e2 with | t1, Eop (Olongconst n2) Enil => addlimm (Int64.neg n2) t1 | Eop (Oleal (Aindexed n1)) (t1:::Enil), Eop (Oleal (Aindexed n2)) (t2:::Enil) => @@ -270,8 +249,7 @@ Definition mullimm_base (n1: int64) (e2: expr) := end. Nondetfunction mullimm (n1: int64) (e2: expr) := - if Archi.splitlong then SplitLong.mullimm n1 e2 - else if Int64.eq n1 Int64.zero then longconst Int64.zero + if Int64.eq n1 Int64.zero then longconst Int64.zero else if Int64.eq n1 Int64.one then e2 else match e2 with | Eop (Olongconst n2) Enil => longconst (Int64.mul n1 n2) @@ -280,7 +258,6 @@ Nondetfunction mullimm (n1: int64) (e2: expr) := end. Nondetfunction mull (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.mull e1 e2 else match e1, e2 with | Eop (Olongconst n1) Enil, t2 => mullimm n1 t2 | t1, Eop (Olongconst n2) Enil => mullimm n2 t1 @@ -288,28 +265,24 @@ Nondetfunction mull (e1: expr) (e2: expr) := end. Definition mullhu (e1: expr) (n2: int64) := - if Archi.splitlong then SplitLong.mullhu e1 n2 else Eop Omullhu (e1 ::: longconst n2 ::: Enil). Definition mullhs (e1: expr) (n2: int64) := - if Archi.splitlong then SplitLong.mullhs e1 n2 else Eop Omullhs (e1 ::: longconst n2 ::: Enil). Definition shrxlimm (e: expr) (n: int) := - if Archi.splitlong then SplitLong.shrxlimm e n else if Int.eq n Int.zero then e else Eop (Oshrxlimm n) (e ::: Enil). Definition divlu_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.divlu_base e1 e2 else Eop Odivlu (e1:::e2:::Enil). + Eop Odivlu (e1:::e2:::Enil). Definition modlu_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.modlu_base e1 e2 else Eop Omodlu (e1:::e2:::Enil). + Eop Omodlu (e1:::e2:::Enil). Definition divls_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.divls_base e1 e2 else Eop Odivl (e1:::e2:::Enil). + Eop Odivl (e1:::e2:::Enil). Definition modls_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.modls_base e1 e2 else Eop Omodl (e1:::e2:::Enil). + Eop Omodl (e1:::e2:::Enil). Definition cmplu (c: comparison) (e1 e2: expr) := - if Archi.splitlong then SplitLong.cmplu c e1 e2 else match is_longconst e1, is_longconst e2 with | Some n1, Some n2 => Eop (Ointconst (if Int64.cmpu c n1 n2 then Int.one else Int.zero)) Enil @@ -319,7 +292,6 @@ Definition cmplu (c: comparison) (e1 e2: expr) := end. Definition cmpl (c: comparison) (e1 e2: expr) := - if Archi.splitlong then SplitLong.cmpl c e1 e2 else match is_longconst e1, is_longconst e2 with | Some n1, Some n2 => Eop (Ointconst (if Int64.cmp c n1 n2 then Int.one else Int.zero)) Enil @@ -329,19 +301,14 @@ Definition cmpl (c: comparison) (e1 e2: expr) := end. Definition longoffloat (e: expr) := - if Archi.splitlong then SplitLong.longoffloat e else Eop Olongoffloat (e:::Enil). Definition floatoflong (e: expr) := - if Archi.splitlong then SplitLong.floatoflong e else Eop Ofloatoflong (e:::Enil). Definition longofsingle (e: expr) := - if Archi.splitlong then SplitLong.longofsingle e else Eop Olongofsingle (e:::Enil). Definition singleoflong (e: expr) := - if Archi.splitlong then SplitLong.singleoflong e else Eop Osingleoflong (e:::Enil). -End SELECT. diff --git a/x86/SelectLongproof.v b/x86/SelectLongproof.v index 5f79b7aa4a..a935bc75d3 100644 --- a/x86/SelectLongproof.v +++ b/x86/SelectLongproof.v @@ -62,17 +62,14 @@ Definition partial_binary_constructor_sound (cstr: expr -> expr -> expr) (sem: v Theorem eval_longconst: forall le n, eval_expr ge sp e m le (longconst n) (Vlong n). Proof. - unfold longconst; intros; destruct Archi.splitlong. - apply SplitLongproof.eval_longconst. - EvalOp. + unfold longconst; intros; EvalOp. Qed. Lemma is_longconst_sound: forall v a n le, is_longconst a = Some n -> eval_expr ge sp e m le a v -> v = Vlong n. Proof with (try discriminate). - intros. unfold is_longconst in *. destruct Archi.splitlong. - eapply SplitLongproof.is_longconst_sound; eauto. + intros. unfold is_longconst in *. assert (a = Eop (Olongconst n) Enil). { destruct a... destruct o... destruct e0... congruence. } subst a. InvEval. auto. @@ -80,7 +77,7 @@ Qed. Theorem eval_intoflong: unary_constructor_sound intoflong Val.loword. Proof. - unfold intoflong; destruct Archi.splitlong. apply SplitLongproof.eval_intoflong. + unfold intoflong. red; intros. destruct (is_longconst a) as [n|] eqn:C. - TrivialExists. simpl. erewrite (is_longconst_sound x) by eauto. auto. - TrivialExists. @@ -88,7 +85,7 @@ Qed. Theorem eval_longofintu: unary_constructor_sound longofintu Val.longofintu. Proof. - unfold longofintu; destruct Archi.splitlong. apply SplitLongproof.eval_longofintu. + unfold longofintu. red; intros. destruct (is_intconst a) as [n|] eqn:C. - econstructor; split. apply eval_longconst. exploit is_intconst_sound; eauto. intros; subst x. auto. @@ -97,7 +94,7 @@ Qed. Theorem eval_longofint: unary_constructor_sound longofint Val.longofint. Proof. - unfold longofint; destruct Archi.splitlong. apply SplitLongproof.eval_longofint. + unfold longofint. red; intros. destruct (is_intconst a) as [n|] eqn:C. - econstructor; split. apply eval_longconst. exploit is_intconst_sound; eauto. intros; subst x. auto. @@ -106,7 +103,7 @@ Qed. Theorem eval_notl: unary_constructor_sound notl Val.notl. Proof. - unfold notl; destruct Archi.splitlong. apply SplitLongproof.eval_notl. + unfold notl. red; intros. destruct (notl_match a). - InvEval. econstructor; split. apply eval_longconst. auto. - InvEval. subst. exists v1; split; auto. destruct v1; simpl; auto. rewrite Int64.not_involutive; auto. @@ -130,7 +127,7 @@ Qed. Theorem eval_andl: binary_constructor_sound andl Val.andl. Proof. - unfold andl; destruct Archi.splitlong. apply SplitLongproof.eval_andl. + unfold andl. red; intros. destruct (andl_match a b). - InvEval. rewrite Val.andl_commut. apply eval_andlimm; auto. - InvEval. apply eval_andlimm; auto. @@ -152,7 +149,7 @@ Qed. Theorem eval_orl: binary_constructor_sound orl Val.orl. Proof. - unfold orl; destruct Archi.splitlong. apply SplitLongproof.eval_orl. + unfold orl. red; intros. assert (DEFAULT: exists v, eval_expr ge sp e m le (Eop Oorl (a:::b:::Enil)) v /\ Val.lessdef (Val.orl x y) v) by TrivialExists. assert (ROR: forall v n1 n2, @@ -196,7 +193,7 @@ Qed. Theorem eval_xorl: binary_constructor_sound xorl Val.xorl. Proof. - unfold xorl; destruct Archi.splitlong. apply SplitLongproof.eval_xorl. + unfold xorl. red; intros. destruct (xorl_match a b). - InvEval. rewrite Val.xorl_commut. apply eval_xorlimm; auto. - InvEval. apply eval_xorlimm; auto. @@ -205,7 +202,7 @@ Qed. Theorem eval_shllimm: forall n, unary_constructor_sound (fun e => shllimm e n) (fun v => Val.shll v (Vint n)). Proof. - intros; unfold shllimm. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shllimm; auto. + intros; unfold shllimm. red; intros. predSpec Int.eq Int.eq_spec n Int.zero. exists x; split; auto. subst n; destruct x; simpl; auto. @@ -234,7 +231,7 @@ Qed. Theorem eval_shrluimm: forall n, unary_constructor_sound (fun e => shrluimm e n) (fun v => Val.shrlu v (Vint n)). Proof. - intros; unfold shrluimm. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shrluimm; auto. + intros; unfold shrluimm. red; intros. predSpec Int.eq Int.eq_spec n Int.zero. exists x; split; auto. subst n; destruct x; simpl; auto. @@ -256,7 +253,7 @@ Qed. Theorem eval_shrlimm: forall n, unary_constructor_sound (fun e => shrlimm e n) (fun v => Val.shrl v (Vint n)). Proof. - intros; unfold shrlimm. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shrlimm; auto. + intros; unfold shrlimm. red; intros. predSpec Int.eq Int.eq_spec n Int.zero. exists x; split; auto. subst n; destruct x; simpl; auto. @@ -278,7 +275,7 @@ Qed. Theorem eval_shll: binary_constructor_sound shll Val.shll. Proof. - unfold shll. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shll; auto. + unfold shll. red; intros. destruct (is_intconst b) as [n2|] eqn:C. - exploit is_intconst_sound; eauto. intros EQ; subst y. apply eval_shllimm; auto. - TrivialExists. @@ -286,7 +283,7 @@ Qed. Theorem eval_shrlu: binary_constructor_sound shrlu Val.shrlu. Proof. - unfold shrlu. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shrlu; auto. + unfold shrlu. red; intros. destruct (is_intconst b) as [n2|] eqn:C. - exploit is_intconst_sound; eauto. intros EQ; subst y. apply eval_shrluimm; auto. - TrivialExists. @@ -294,7 +291,7 @@ Qed. Theorem eval_shrl: binary_constructor_sound shrl Val.shrl. Proof. - unfold shrl. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_shrl; auto. + unfold shrl. red; intros. destruct (is_intconst b) as [n2|] eqn:C. - exploit is_intconst_sound; eauto. intros EQ; subst y. apply eval_shrlimm; auto. - TrivialExists. @@ -302,7 +299,7 @@ Qed. Theorem eval_negl: unary_constructor_sound negl Val.negl. Proof. - unfold negl. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_negl; auto. + unfold negl. red; intros. destruct (is_longconst a) as [n|] eqn:C. - exploit is_longconst_sound; eauto. intros EQ; subst x. econstructor; split. apply eval_longconst. auto. @@ -331,8 +328,7 @@ Proof. Val.addl (Genv.symbol_address ge id ofs) (Vlong (Int64.repr n))). { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int64 (Int64.repr n)) by auto with ptrofs. apply Genv.shift_symbol_address_64; auto. } - unfold addl. destruct Archi.splitlong eqn:SL. - apply SplitLongproof.eval_addl. apply Archi.splitlong_ptr32; auto. + unfold addl. red; intros; destruct (addl_match a b); InvEval. - rewrite Val.addl_commut. apply eval_addlimm; auto. - apply eval_addlimm; auto. @@ -353,8 +349,7 @@ Qed. Theorem eval_subl: binary_constructor_sound subl Val.subl. Proof. - unfold subl. destruct Archi.splitlong eqn:SL. - apply SplitLongproof.eval_subl. apply Archi.splitlong_ptr32; auto. + unfold subl. red; intros; destruct (subl_match a b); InvEval. - rewrite Val.subl_addl_opp. apply eval_addlimm; auto. - subst. rewrite Val.subl_addl_l. rewrite Val.subl_addl_r. @@ -399,8 +394,6 @@ Qed. Theorem eval_mullimm: forall n, unary_constructor_sound (mullimm n) (fun v => Val.mull v (Vlong n)). Proof. unfold mullimm. intros; red; intros. - destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_mullimm; eauto. predSpec Int64.eq Int64.eq_spec n Int64.zero. exists (Vlong Int64.zero); split. apply eval_longconst. destruct x; simpl; auto. subst n; rewrite Int64.mul_zero; auto. @@ -420,7 +413,7 @@ Qed. Theorem eval_mull: binary_constructor_sound mull Val.mull. Proof. - unfold mull. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mull; auto. + unfold mull. red; intros; destruct (mull_match a b); InvEval. - rewrite Val.mull_commut. apply eval_mullimm; auto. - apply eval_mullimm; auto. @@ -430,14 +423,14 @@ Qed. Theorem eval_mullhu: forall n, unary_constructor_sound (fun a => mullhu a n) (fun v => Val.mullhu v (Vlong n)). Proof. - unfold mullhu; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhu; auto. + unfold mullhu; intros. red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto. Qed. Theorem eval_mullhs: forall n, unary_constructor_sound (fun a => mullhs a n) (fun v => Val.mullhs v (Vlong n)). Proof. - unfold mullhs; intros. destruct Archi.splitlong eqn:SL. apply SplitLongproof.eval_mullhs; auto. + unfold mullhs; intros. red; intros. TrivialExists. constructor. eauto. constructor. apply eval_longconst. constructor. auto. Qed. @@ -447,9 +440,8 @@ Theorem eval_shrxlimm: Val.shrxl x (Vint n) = Some z -> exists v, eval_expr ge sp e m le (shrxlimm a n) v /\ Val.lessdef z v. Proof. - unfold shrxlimm; intros. destruct Archi.splitlong eqn:SL. -+ eapply SplitLongproof.eval_shrxlimm; eauto using Archi.splitlong_ptr32. -+ predSpec Int.eq Int.eq_spec n Int.zero. + unfold shrxlimm; intros. + predSpec Int.eq Int.eq_spec n Int.zero. - subst n. destruct x; simpl in H0; inv H0. econstructor; split; eauto. change (Int.ltu Int.zero (Int.repr 63)) with true. simpl. rewrite Int64.shrx'_zero; auto. - TrivialExists. @@ -457,29 +449,25 @@ Qed. Theorem eval_divls_base: partial_binary_constructor_sound divls_base Val.divls. Proof. - unfold divls_base; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_divls_base; eauto. + unfold divls_base; red; intros. TrivialExists. Qed. Theorem eval_modls_base: partial_binary_constructor_sound modls_base Val.modls. Proof. - unfold modls_base; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_modls_base; eauto. + unfold modls_base; red; intros. TrivialExists. Qed. Theorem eval_divlu_base: partial_binary_constructor_sound divlu_base Val.divlu. Proof. - unfold divlu_base; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_divlu_base; eauto. + unfold divlu_base; red; intros. TrivialExists. Qed. Theorem eval_modlu_base: partial_binary_constructor_sound modlu_base Val.modlu. Proof. - unfold modlu_base; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_modlu_base; eauto. + unfold modlu_base; red; intros. TrivialExists. Qed. @@ -490,8 +478,7 @@ Theorem eval_cmplu: Val.cmplu (Mem.valid_pointer m) c x y = Some v -> eval_expr ge sp e m le (cmplu c a b) v. Proof. - unfold cmplu; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_cmplu; eauto using Archi.splitlong_ptr32. + unfold cmplu; intros. unfold Val.cmplu in H1. destruct (Val.cmplu_bool (Mem.valid_pointer m) c x y) as [vb|] eqn:C; simpl in H1; inv H1. destruct (is_longconst a) as [n1|] eqn:LC1; destruct (is_longconst b) as [n2|] eqn:LC2; @@ -511,8 +498,7 @@ Theorem eval_cmpl: Val.cmpl c x y = Some v -> eval_expr ge sp e m le (cmpl c a b) v. Proof. - unfold cmpl; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_cmpl; eauto. + unfold cmpl; intros. unfold Val.cmpl in H1. destruct (Val.cmpl_bool c x y) as [vb|] eqn:C; simpl in H1; inv H1. destruct (is_longconst a) as [n1|] eqn:LC1; destruct (is_longconst b) as [n2|] eqn:LC2; @@ -527,29 +513,25 @@ Qed. Theorem eval_longoffloat: partial_unary_constructor_sound longoffloat Val.longoffloat. Proof. - unfold longoffloat; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_longoffloat; eauto. + unfold longoffloat; red; intros. TrivialExists. Qed. Theorem eval_floatoflong: partial_unary_constructor_sound floatoflong Val.floatoflong. Proof. - unfold floatoflong; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_floatoflong; eauto. + unfold floatoflong; red; intros. TrivialExists. Qed. Theorem eval_longofsingle: partial_unary_constructor_sound longofsingle Val.longofsingle. Proof. - unfold longofsingle; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_longofsingle; eauto. + unfold longofsingle; red; intros. TrivialExists. Qed. Theorem eval_singleoflong: partial_unary_constructor_sound singleoflong Val.singleoflong. Proof. - unfold singleoflong; red; intros. destruct Archi.splitlong eqn:SL. - eapply SplitLongproof.eval_singleoflong; eauto. + unfold singleoflong; red; intros. TrivialExists. Qed. diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 610be0f5a1..9ba6ce8b76 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -504,14 +504,6 @@ module Target(System: SYSTEM):TARGET = fprintf oc " movss %a, %a\n" addressing a freg rd | Pmovss_mf(a, r1) -> fprintf oc " movss %a, %a\n" freg r1 addressing a - | Pfldl_m(a) -> - fprintf oc " fldl %a\n" addressing a - | Pfstpl_m(a) -> - fprintf oc " fstpl %a\n" addressing a - | Pflds_m(a) -> - fprintf oc " flds %a\n" addressing a - | Pfstps_m(a) -> - fprintf oc " fstps %a\n" addressing a (* Moves with conversion *) | Pmovb_mr(a, r1) -> fprintf oc " movb %a, %a\n" ireg8 r1 addressing a diff --git a/x86_32/Archi.v b/x86_32/Archi.v deleted file mode 100644 index 14c97e2b4a..0000000000 --- a/x86_32/Archi.v +++ /dev/null @@ -1,72 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris *) -(* Jacques-Henri Jourdan, INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU Lesser General Public License as *) -(* published by the Free Software Foundation, either version 2.1 of *) -(* the License, or (at your option) any later version. *) -(* This file is also distributed under the terms of the *) -(* INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Architecture-dependent parameters for x86 in 32-bit mode *) - -From Coq Require Import List ZArith. -From Flocq Require Import Binary Bits. - -Definition ptr64 := false. - -Definition big_endian := false. - -Definition align_int64 := 4%Z. -Definition align_float64 := 4%Z. - -Definition splitlong := negb ptr64. - -Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. -Proof. - unfold splitlong. destruct ptr64; simpl; congruence. -Qed. - -Definition default_nan_64 := (true, iter_nat 51 _ xO xH). -Definition default_nan_32 := (true, iter_nat 22 _ xO xH). - -(* Always choose the first NaN argument, if any *) - -Definition choose_nan_64 (l: list (bool * positive)) : bool * positive := - match l with nil => default_nan_64 | n :: _ => n end. - -Definition choose_nan_32 (l: list (bool * positive)) : bool * positive := - match l with nil => default_nan_32 | n :: _ => n end. - -Lemma choose_nan_64_idem: forall n, - choose_nan_64 (n :: n :: nil) = choose_nan_64 (n :: nil). -Proof. auto. Qed. - -Lemma choose_nan_32_idem: forall n, - choose_nan_32 (n :: n :: nil) = choose_nan_32 (n :: nil). -Proof. auto. Qed. - -Definition fma_order {A: Type} (x y z: A) := (x, y, z). - -Definition fma_invalid_mul_is_nan := false. - -Definition float_of_single_preserves_sNaN := false. - -Definition float_conversion_default_nan := false. - -(** Which ABI to use. *) -Parameter win64: bool. (* Always false in 32 bits *) - -Global Opaque ptr64 big_endian splitlong - default_nan_64 choose_nan_64 - default_nan_32 choose_nan_32 - fma_order fma_invalid_mul_is_nan - float_of_single_preserves_sNaN - float_conversion_default_nan.