diff options
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Archi.v | 17 | ||||
| -rw-r--r-- | aarch64/Asm.v | 10 | ||||
| -rw-r--r-- | aarch64/Asmexpand.ml | 52 | ||||
| -rw-r--r-- | aarch64/Asmgen.v | 5 | ||||
| -rw-r--r-- | aarch64/Asmgenproof.v | 25 | ||||
| -rw-r--r-- | aarch64/Asmgenproof1.v | 110 | ||||
| -rw-r--r-- | aarch64/Builtins1.v | 9 | ||||
| -rw-r--r-- | aarch64/CBuiltins.ml | 35 | ||||
| -rw-r--r-- | aarch64/ConstpropOp.vp | 4 | ||||
| -rw-r--r-- | aarch64/ConstpropOpproof.v | 2 | ||||
| -rw-r--r-- | aarch64/Conventions1.v | 246 | ||||
| -rw-r--r-- | aarch64/Op.v | 8 | ||||
| -rw-r--r-- | aarch64/SelectLongproof.v | 24 | ||||
| -rw-r--r-- | aarch64/SelectOp.vp | 10 | ||||
| -rw-r--r-- | aarch64/SelectOpproof.v | 66 | ||||
| -rw-r--r-- | aarch64/Stacklayout.v | 44 | ||||
| -rw-r--r-- | aarch64/TargetPrinter.ml | 364 | ||||
| -rw-r--r-- | aarch64/extractionMachdep.v | 27 |
18 files changed, 671 insertions, 387 deletions
diff --git a/aarch64/Archi.v b/aarch64/Archi.v index 42500e70..4911db73 100644 --- a/aarch64/Archi.v +++ b/aarch64/Archi.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 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. *) +(* 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. *) (* *) (* *********************************************************************) @@ -85,6 +86,10 @@ Global Opaque ptr64 big_endian splitlong fma_order fma_invalid_mul_is_nan float_of_single_preserves_sNaN. -(** Whether to generate position-independent code or not *) +(** Which ABI to implement *) -Parameter pic_code: unit -> bool. +Inductive abi_kind: Type := + | AAPCS64 (**r ARM's standard as used in Linux and other ELF platforms *) + | Apple. (**r the variant used in macOS and iOS *) + +Parameter abi: abi_kind. diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 5ac577b1..b5f4c838 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -970,9 +970,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfmov rd r1 => Next (nextinstr (rs#rd <- (rs#r1))) m | Pfmovimms rd f => - Next (nextinstr (rs#rd <- (Vsingle f))) m + Next (nextinstr (rs#X16 <- Vundef #rd <- (Vsingle f))) m | Pfmovimmd rd f => - Next (nextinstr (rs#rd <- (Vfloat f))) m + Next (nextinstr (rs#X16 <- Vundef #rd <- (Vfloat f))) m | Pfmovi S rd r1 => Next (nextinstr (rs#rd <- (float32_of_bits rs##r1))) m | Pfmovi D rd r1 => @@ -1097,7 +1097,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Vint n => match list_nth_z tbl (Int.unsigned n) with | None => Stuck - | Some lbl => goto_label f lbl (rs#X16 <- Vundef #X17 <- Vundef) m + | Some lbl => goto_label f lbl (rs#X16 <- Vundef) m end | _ => Stuck end @@ -1212,7 +1212,7 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge vargs m t vres m' -> rs' = nextinstr (set_res res vres - (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) -> + (undef_regs (IR X16 :: IR X30 :: map preg_of (destroyed_by_builtin ef)) rs)) -> step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', @@ -1293,7 +1293,7 @@ Ltac Equalities := split. auto. intros. destruct B; auto. subst. auto. - (* trace length *) red; intros. inv H; simpl. - omega. + lia. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. - (* initial states *) diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index 1ba754dd..d24a9ef6 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -47,17 +47,28 @@ let expand_storeptr (src: ireg) (base: iregsp) ofs = (* Determine the number of int registers, FP registers, and stack locations used to pass the fixed parameters. *) +let align n a = (n + a - 1) land (-a) + +let typesize = function + | Tint | Tany32 | Tsingle -> 4 + | Tlong | Tany64 | Tfloat -> 8 + +let reserve_stack stk ty = + match Archi.abi with + | Archi.AAPCS64 -> stk + 8 + | Archi.Apple -> align stk (typesize ty) + typesize ty + let rec next_arg_locations ir fr stk = function | [] -> (ir, fr, stk) - | (Tint | Tlong | Tany32 | Tany64) :: l -> + | (Tint | Tlong | Tany32 | Tany64 as ty) :: l -> if ir < 8 then next_arg_locations (ir + 1) fr stk l - else next_arg_locations ir fr (stk + 8) l - | (Tfloat | Tsingle) :: l -> + else next_arg_locations ir fr (reserve_stack stk ty) l + | (Tfloat | Tsingle as ty) :: l -> if fr < 8 then next_arg_locations ir (fr + 1) stk l - else next_arg_locations ir fr (stk + 8) l + else next_arg_locations ir fr (reserve_stack stk ty) l (* Allocate memory on the stack and use it to save the registers used for parameter passing. As an optimization, do not save @@ -86,6 +97,8 @@ let save_parameter_registers ir fr = emit (Pstrd(float_param_regs.(i), ADimm(XSP, Z.of_uint pos))) done +let current_function_stacksize = ref 0L + (* Initialize a va_list as per va_start. Register r points to the following struct: @@ -98,11 +111,7 @@ let save_parameter_registers ir fr = } *) -let current_function_stacksize = ref 0L - -let expand_builtin_va_start r = - if not (is_current_function_variadic ()) then - invalid_arg "Fatal error: va_start used in non-vararg function"; +let expand_builtin_va_start_aapcs64 r = let (ir, fr, stk) = next_arg_locations 0 0 0 (get_current_function_args ()) in let stack_ofs = Int64.(add !current_function_stacksize (of_int stk)) @@ -127,6 +136,25 @@ let expand_builtin_va_start r = expand_loadimm32 X16 (coqint_of_camlint (Int32.of_int vr_offs)); emit (Pstrw(X16, ADimm(RR1 r, coqint_of_camlint64 28L))) +(* In macOS, va_list is just a pointer (char * ) and all variadic arguments + are passed on the stack. *) + +let expand_builtin_va_start_apple r = + let (ir, fr, stk) = + next_arg_locations 0 0 0 (get_current_function_args ()) in + let stk = align stk 8 in + let stack_ofs = Int64.(add !current_function_stacksize (of_int stk)) in + (* *va = sp + stack_ofs *) + expand_addimm64 (RR1 X16) XSP (coqint_of_camlint64 stack_ofs); + emit (Pstrx(X16, ADimm(RR1 r, coqint_of_camlint64 0L))) + +let expand_builtin_va_start r = + if not (is_current_function_variadic ()) then + invalid_arg "Fatal error: va_start used in non-vararg function"; + match Archi.abi with + | Archi.AAPCS64 -> expand_builtin_va_start_aapcs64 r + | Archi.Apple -> expand_builtin_va_start_apple r + (* Handling of annotations *) let expand_annot_val kind txt targ args res = @@ -327,8 +355,12 @@ let expand_builtin_inline name args res = (* Synchronization *) | "__builtin_membar", [], _ -> () + (* No operation *) | "__builtin_nop", [], _ -> emit Pnop + (* Optimization hint *) + | "__builtin_unreachable", [], _ -> + () (* Byte swap *) | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) -> emit (Prev(W, res, a1)) @@ -380,7 +412,7 @@ let expand_instruction instr = match instr with | Pallocframe (sz, ofs) -> emit (Pmov (RR1 X29, XSP)); - if is_current_function_variadic() then begin + if is_current_function_variadic() && Archi.abi = Archi.AAPCS64 then begin let (ir, fr, _) = next_arg_locations 0 0 0 (get_current_function_args ()) in save_parameter_registers ir fr; diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 875f3fd1..baaab6c4 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -15,6 +15,7 @@ Require Import Recdef Coqlib Zwf Zbits. Require Import Errors AST Integers Floats Op. Require Import Locations Mach Asm. +Require SelectOp. Local Open Scope string_scope. Local Open Scope list_scope. @@ -284,7 +285,7 @@ Definition shrx64 (rd r1: ireg) (n: int) (k: code) : code := (** Load the address [id + ofs] in [rd] *) Definition loadsymbol (rd: ireg) (id: ident) (ofs: ptrofs) (k: code) : code := - if Archi.pic_code tt then + if SelectOp.symbol_is_relocatable id then if Ptrofs.eq ofs Ptrofs.zero then Ploadsymbol rd id :: k else @@ -946,7 +947,7 @@ Definition transl_addressing (sz: Z) (addr: Op.addressing) (args: list mreg) OK (arith_extended Paddext (Padd X) X16 r1 r2 x a (insn (ADimm X16 Int64.zero) :: k)) | Aglobal id ofs, nil => - assertion (negb (Archi.pic_code tt)); + assertion (negb (SelectOp.symbol_is_relocatable id)); if Ptrofs.eq (Ptrofs.modu ofs (Ptrofs.repr sz)) Ptrofs.zero && symbol_is_aligned id sz then OK (Padrp X16 id ofs :: insn (ADadr X16 id ofs) :: k) else OK (loadsymbol X16 id ofs (insn (ADimm X16 Int64.zero) :: k)) diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index eeff1956..dc0bc509 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -67,7 +67,7 @@ Lemma transf_function_no_overflow: transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned. Proof. intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. - omega. + lia. Qed. Lemma exec_straight_exec: @@ -208,7 +208,7 @@ Qed. Remark loadsymbol_label: forall r id ofs k, tail_nolabel k (loadsymbol r id ofs k). Proof. intros; unfold loadsymbol. - destruct (Archi.pic_code tt); TailNoLabel. destruct Ptrofs.eq; TailNoLabel. + destruct (SelectOp.symbol_is_relocatable id); TailNoLabel. destruct Ptrofs.eq; TailNoLabel. Qed. Hint Resolve loadsymbol_label: labels. @@ -424,8 +424,8 @@ Proof. split. unfold goto_label. rewrite P. rewrite H1. auto. split. rewrite Pregmap.gss. constructor; auto. rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. - auto. omega. - generalize (transf_function_no_overflow _ _ H0). omega. + auto. lia. + generalize (transf_function_no_overflow _ _ H0). lia. intros. apply Pregmap.gso; auto. Qed. @@ -831,13 +831,16 @@ Local Transparent destroyed_by_op. econstructor; eauto. instantiate (2 := tf); instantiate (1 := x). unfold nextinstr. rewrite Pregmap.gss. - rewrite set_res_other. rewrite undef_regs_other_2. + rewrite set_res_other. rewrite undef_regs_other. rewrite <- H1. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. - rewrite preg_notin_charact. intros. auto with asmgen. + simpl; intros. destruct H4. congruence. destruct H4. congruence. + exploit list_in_map_inv; eauto. intros (mr & U & V). subst. + auto with asmgen. auto with asmgen. apply agree_nextinstr. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. + eapply agree_undef_regs; eauto. intros. + simpl. rewrite undef_regs_other_2; auto. Simpl. congruence. - (* Mgoto *) @@ -879,7 +882,7 @@ Local Transparent destroyed_by_op. exploit functions_transl; eauto. intro FN. generalize (transf_function_no_overflow _ _ H5); intro NOOV. exploit find_label_goto_label. eauto. eauto. - instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef). + instantiate (2 := rs0#X16 <- Vundef). Simpl. eauto. eauto. intros [tc' [rs' [A [B C]]]]. @@ -946,10 +949,10 @@ Local Transparent destroyed_by_op. rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity. reflexivity. eexact U. } - exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor. + exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor. intros (ofs' & X & Y). left; exists (State rs3 m3'); split. - eapply exec_straight_steps_1; eauto. omega. constructor. + eapply exec_straight_steps_1; eauto. lia. constructor. econstructor; eauto. rewrite X; econstructor; eauto. apply agree_exten with rs2; eauto with asmgen. @@ -978,7 +981,7 @@ Local Transparent destroyed_at_function_entry. simpl. - (* return *) inv STACKS. simpl in *. - right. split. omega. split. auto. + right. split. lia. split. auto. rewrite <- ATPC in H5. econstructor; eauto. congruence. Qed. diff --git a/aarch64/Asmgenproof1.v b/aarch64/Asmgenproof1.v index 6d44bcc8..93c1f1ed 100644 --- a/aarch64/Asmgenproof1.v +++ b/aarch64/Asmgenproof1.v @@ -26,7 +26,7 @@ Lemma preg_of_iregsp_not_PC: forall r, preg_of_iregsp r <> PC. Proof. destruct r; simpl; congruence. Qed. -Hint Resolve preg_of_iregsp_not_PC: asmgen. +Global Hint Resolve preg_of_iregsp_not_PC: asmgen. Lemma preg_of_not_X16: forall r, preg_of r <> X16. Proof. @@ -44,7 +44,7 @@ Proof. intros. apply ireg_of_not_X16 in H. congruence. Qed. -Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen. +Global Hint Resolve preg_of_not_X16 ireg_of_not_X16 ireg_of_not_X16': asmgen. (** Useful simplification tactic *) @@ -81,8 +81,8 @@ Local Opaque Zzero_ext. induction N as [ | N]; simpl; intros. - constructor. - set (frag := Zzero_ext 16 (Z.shiftr n p)) in *. destruct (Z.eqb frag 0). -+ apply IHN. omega. -+ econstructor. reflexivity. omega. apply IHN; omega. ++ apply IHN. lia. ++ econstructor. reflexivity. lia. apply IHN; lia. Qed. Fixpoint recompose_int (accu: Z) (l: list (Z * Z)) : Z := @@ -100,43 +100,43 @@ Lemma decompose_int_correct: if zlt i p then Z.testbit accu i else Z.testbit n i). Proof. induction N as [ | N]; intros until accu; intros PPOS ABOVE i RANGE. -- simpl. rewrite zlt_true; auto. xomega. +- simpl. rewrite zlt_true; auto. extlia. - rewrite inj_S in RANGE. simpl. set (frag := Zzero_ext 16 (Z.shiftr n p)). assert (FRAG: forall i, p <= i < p + 16 -> Z.testbit n i = Z.testbit frag (i - p)). - { unfold frag; intros. rewrite Zzero_ext_spec by omega. rewrite zlt_true by omega. - rewrite Z.shiftr_spec by omega. f_equal; omega. } + { unfold frag; intros. rewrite Zzero_ext_spec by lia. rewrite zlt_true by lia. + rewrite Z.shiftr_spec by lia. f_equal; lia. } destruct (Z.eqb_spec frag 0). + rewrite IHN. -* destruct (zlt i p). rewrite zlt_true by omega. auto. +* destruct (zlt i p). rewrite zlt_true by lia. auto. destruct (zlt i (p + 16)); auto. - rewrite ABOVE by omega. rewrite FRAG by omega. rewrite e, Z.testbit_0_l. auto. -* omega. -* intros; apply ABOVE; omega. -* xomega. + rewrite ABOVE by lia. rewrite FRAG by lia. rewrite e, Z.testbit_0_l. auto. +* lia. +* intros; apply ABOVE; lia. +* extlia. + simpl. rewrite IHN. * destruct (zlt i (p + 16)). -** rewrite Zinsert_spec by omega. unfold proj_sumbool. - rewrite zlt_true by omega. +** rewrite Zinsert_spec by lia. unfold proj_sumbool. + rewrite zlt_true by lia. destruct (zlt i p). - rewrite zle_false by omega. auto. - rewrite zle_true by omega. simpl. symmetry; apply FRAG; omega. -** rewrite Z.ldiff_spec, Z.shiftl_spec by omega. - change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by omega. - rewrite zlt_false by omega. rewrite zlt_false by omega. apply andb_true_r. -* omega. -* intros. rewrite Zinsert_spec by omega. unfold proj_sumbool. - rewrite zle_true by omega. rewrite zlt_false by omega. simpl. - apply ABOVE. omega. -* xomega. + rewrite zle_false by lia. auto. + rewrite zle_true by lia. simpl. symmetry; apply FRAG; lia. +** rewrite Z.ldiff_spec, Z.shiftl_spec by lia. + change 65535 with (two_p 16 - 1). rewrite Ztestbit_two_p_m1 by lia. + rewrite zlt_false by lia. rewrite zlt_false by lia. apply andb_true_r. +* lia. +* intros. rewrite Zinsert_spec by lia. unfold proj_sumbool. + rewrite zle_true by lia. rewrite zlt_false by lia. simpl. + apply ABOVE. lia. +* extlia. Qed. Corollary decompose_int_eqmod: forall N n, eqmod (two_power_nat (N * 16)%nat) (recompose_int 0 (decompose_int N n 0)) n. Proof. intros; apply eqmod_same_bits; intros. - rewrite decompose_int_correct. apply zlt_false; omega. - omega. intros; apply Z.testbit_0_l. xomega. + rewrite decompose_int_correct. apply zlt_false; lia. + lia. intros; apply Z.testbit_0_l. extlia. Qed. Corollary decompose_notint_eqmod: forall N n, @@ -145,8 +145,8 @@ Corollary decompose_notint_eqmod: forall N n, Proof. intros; apply eqmod_same_bits; intros. rewrite Z.lnot_spec, decompose_int_correct. - rewrite zlt_false by omega. rewrite Z.lnot_spec by omega. apply negb_involutive. - omega. intros; apply Z.testbit_0_l. xomega. omega. + rewrite zlt_false by lia. rewrite Z.lnot_spec by lia. apply negb_involutive. + lia. intros; apply Z.testbit_0_l. extlia. lia. Qed. Lemma negate_decomposition_wf: @@ -156,7 +156,7 @@ Proof. instantiate (1 := (Z.lnot m)). apply equal_same_bits; intros. rewrite H. change 65535 with (two_p 16 - 1). - rewrite Z.lxor_spec, !Zzero_ext_spec, Z.lnot_spec, Ztestbit_two_p_m1 by omega. + rewrite Z.lxor_spec, !Zzero_ext_spec, Z.lnot_spec, Ztestbit_two_p_m1 by lia. destruct (zlt i 16). apply xorb_true_r. auto. @@ -167,7 +167,7 @@ Lemma Zinsert_eqmod: eqmod (two_power_nat n) x1 x2 -> eqmod (two_power_nat n) (Zinsert x1 y p l) (Zinsert x2 y p l). Proof. - intros. apply eqmod_same_bits; intros. rewrite ! Zinsert_spec by omega. + intros. apply eqmod_same_bits; intros. rewrite ! Zinsert_spec by lia. destruct (zle p i && zlt i (p + l)); auto. apply same_bits_eqmod with n; auto. Qed. @@ -178,12 +178,12 @@ Lemma Zinsert_0_l: Z.shiftl (Zzero_ext l y) p = Zinsert 0 (Zzero_ext l y) p l. Proof. intros. apply equal_same_bits; intros. - rewrite Zinsert_spec by omega. unfold proj_sumbool. - destruct (zlt i p); [rewrite zle_false by omega|rewrite zle_true by omega]; simpl. + rewrite Zinsert_spec by lia. unfold proj_sumbool. + destruct (zlt i p); [rewrite zle_false by lia|rewrite zle_true by lia]; simpl. - rewrite Z.testbit_0_l, Z.shiftl_spec_low by auto. auto. -- rewrite Z.shiftl_spec by omega. +- rewrite Z.shiftl_spec by lia. destruct (zlt i (p + l)); auto. - rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by omega. auto. + rewrite Zzero_ext_spec, zlt_false, Z.testbit_0_l by lia. auto. Qed. Lemma recompose_int_negated: @@ -193,12 +193,12 @@ Proof. induction 1; intros accu; simpl. - auto. - rewrite <- IHwf_decomposition. f_equal. apply equal_same_bits; intros. - rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by omega. + rewrite Z.lnot_spec, ! Zinsert_spec, Z.lxor_spec, Z.lnot_spec by lia. unfold proj_sumbool. destruct (zle p i); simpl; auto. destruct (zlt i (p + 16)); simpl; auto. change 65535 with (two_p 16 - 1). - rewrite Ztestbit_two_p_m1 by omega. rewrite zlt_true by omega. + rewrite Ztestbit_two_p_m1 by lia. rewrite zlt_true by lia. apply xorb_true_r. Qed. @@ -219,7 +219,7 @@ Proof. (Zinsert accu n p 16)) as (rs' & P & Q & R). Simpl. rewrite ACCU. simpl. f_equal. apply Int.eqm_samerepr. - apply Zinsert_eqmod. auto. omega. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. + apply Zinsert_eqmod. auto. lia. apply Int.eqm_sym; apply Int.eqm_unsigned_repr. exists rs'; split. eapply exec_straight_opt_step_opt. simpl; eauto. auto. exact P. split. exact Q. intros; Simpl. rewrite R by auto. Simpl. @@ -244,7 +244,7 @@ Proof. unfold rs1; Simpl. exists rs2; split. eapply exec_straight_opt_step; eauto. - simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. + simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; lia. reflexivity. split. exact Q. intros. rewrite R by auto. unfold rs1; Simpl. @@ -272,7 +272,7 @@ Proof. exists rs2; split. eapply exec_straight_opt_step; eauto. simpl. unfold rs1. do 5 f_equal. - unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. + unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; lia. reflexivity. split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. intros. rewrite R by auto. unfold rs1; Simpl. @@ -302,8 +302,8 @@ Proof. apply Int.eqm_samerepr. apply decompose_notint_eqmod. apply Int.repr_unsigned. } destruct Nat.leb. -+ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; omega. -+ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; omega. ++ rewrite <- A. apply exec_loadimm_z_w. apply decompose_int_wf; lia. ++ rewrite <- B. apply exec_loadimm_n_w. apply decompose_int_wf; lia. Qed. Lemma exec_loadimm_k_x: @@ -323,7 +323,7 @@ Proof. (Zinsert accu n p 16)) as (rs' & P & Q & R). Simpl. rewrite ACCU. simpl. f_equal. apply Int64.eqm_samerepr. - apply Zinsert_eqmod. auto. omega. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr. + apply Zinsert_eqmod. auto. lia. apply Int64.eqm_sym; apply Int64.eqm_unsigned_repr. exists rs'; split. eapply exec_straight_opt_step_opt. simpl; eauto. auto. exact P. split. exact Q. intros; Simpl. rewrite R by auto. Simpl. @@ -348,7 +348,7 @@ Proof. unfold rs1; Simpl. exists rs2; split. eapply exec_straight_opt_step; eauto. - simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; omega. + simpl. unfold rs1. do 5 f_equal. unfold accu0. rewrite H. apply Zinsert_0_l; lia. reflexivity. split. exact Q. intros. rewrite R by auto. unfold rs1; Simpl. @@ -376,7 +376,7 @@ Proof. exists rs2; split. eapply exec_straight_opt_step; eauto. simpl. unfold rs1. do 5 f_equal. - unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; omega. + unfold accu0. f_equal. rewrite H. apply Zinsert_0_l; lia. reflexivity. split. unfold accu0 in Q; rewrite recompose_int_negated in Q by auto. exact Q. intros. rewrite R by auto. unfold rs1; Simpl. @@ -406,8 +406,8 @@ Proof. apply Int64.eqm_samerepr. apply decompose_notint_eqmod. apply Int64.repr_unsigned. } destruct Nat.leb. -+ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; omega. -+ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; omega. ++ rewrite <- A. apply exec_loadimm_z_x. apply decompose_int_wf; lia. ++ rewrite <- B. apply exec_loadimm_n_x. apply decompose_int_wf; lia. Qed. (** Add immediate *) @@ -426,14 +426,14 @@ Lemma exec_addimm_aux_32: Proof. intros insn sem SEM ASSOC; intros. unfold addimm_aux. set (nlo := Zzero_ext 12 (Int.unsigned n)). set (nhi := Int.unsigned n - nlo). - assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; omega). + assert (E: Int.unsigned n = nhi + nlo) by (unfold nhi; lia). rewrite <- (Int.repr_unsigned n). destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)]. - econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. + split. Simpl. do 3 f_equal; lia. intros; Simpl. - econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. + split. Simpl. do 3 f_equal; lia. intros; Simpl. - econstructor; split. eapply exec_straight_two. apply SEM. apply SEM. Simpl. Simpl. @@ -484,14 +484,14 @@ Lemma exec_addimm_aux_64: Proof. intros insn sem SEM ASSOC; intros. unfold addimm_aux. set (nlo := Zzero_ext 12 (Int64.unsigned n)). set (nhi := Int64.unsigned n - nlo). - assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; omega). + assert (E: Int64.unsigned n = nhi + nlo) by (unfold nhi; lia). rewrite <- (Int64.repr_unsigned n). destruct (Z.eqb_spec nhi 0); [|destruct (Z.eqb_spec nlo 0)]. - econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. + split. Simpl. do 3 f_equal; lia. intros; Simpl. - econstructor; split. apply exec_straight_one. apply SEM. Simpl. - split. Simpl. do 3 f_equal; omega. + split. Simpl. do 3 f_equal; lia. intros; Simpl. - econstructor; split. eapply exec_straight_two. apply SEM. apply SEM. Simpl. Simpl. @@ -594,13 +594,13 @@ Qed. (** Load address of symbol *) Lemma exec_loadsymbol: forall rd s ofs k rs m, - rd <> X16 \/ Archi.pic_code tt = false -> + rd <> X16 \/ SelectOp.symbol_is_relocatable s = false -> exists rs', exec_straight ge fn (loadsymbol rd s ofs k) rs m k rs' m /\ rs'#rd = Genv.symbol_address ge s ofs /\ forall r, data_preg r = true -> r <> rd -> rs'#r = rs#r. Proof. - unfold loadsymbol; intros. destruct (Archi.pic_code tt). + unfold loadsymbol; intros. destruct (SelectOp.symbol_is_relocatable s). - predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero. + subst ofs. econstructor; split. apply exec_straight_one; [simpl; eauto | reflexivity]. @@ -1833,4 +1833,4 @@ Proof. intros. Simpl. Qed. -End CONSTRUCTORS.
\ No newline at end of file +End CONSTRUCTORS. diff --git a/aarch64/Builtins1.v b/aarch64/Builtins1.v index 53c83d7e..cd6f8cc4 100644 --- a/aarch64/Builtins1.v +++ b/aarch64/Builtins1.v @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 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. *) +(* 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. *) (* *) (* *********************************************************************) diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml index e2a9c87a..80d66310 100644 --- a/aarch64/CBuiltins.ml +++ b/aarch64/CBuiltins.ml @@ -6,10 +6,11 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 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. *) +(* 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. *) (* *) (* *********************************************************************) @@ -17,16 +18,28 @@ open C -(* va_list is a struct of size 32 and alignment 8, passed by reference *) +(* AAPCS64: + va_list is a struct of size 32 and alignment 8, passed by reference + Apple: + va_list is a pointer (size 8, alignment 8), passed by reference *) -let va_list_type = TArray(TInt(IULong, []), Some 4L, []) -let size_va_list = 32 -let va_list_scalar = false +let (va_list_type, size_va_list, va_list_scalar) = + match Archi.abi with + | Archi.AAPCS64 -> (TArray(TInt(IULong, []), Some 4L, []), 32, false) + | Archi.Apple -> (TPtr(TVoid [], []), 8, true) + +(* Some macOS headers use the GCC built-in types "__int128_t" and + "__uint128_t" unconditionally. Provide a dummy definition. *) + +let int128_type = TArray(TInt(IULong, []), Some 2L, []) let builtins = { - builtin_typedefs = [ - "__builtin_va_list", va_list_type - ]; + builtin_typedefs = + [ "__builtin_va_list", va_list_type ] @ + (if Configuration.system = "macos" then + [ "__int128_t", int128_type; + "__uint128_t", int128_type ] + else []); builtin_functions = [ (* Synchronization *) "__builtin_fence", diff --git a/aarch64/ConstpropOp.vp b/aarch64/ConstpropOp.vp index c0a2c6bf..f2d17a51 100644 --- a/aarch64/ConstpropOp.vp +++ b/aarch64/ConstpropOp.vp @@ -13,11 +13,11 @@ (** Strength reduction for operators and conditions. This is the machine-dependent part of [Constprop]. *) -Require Archi. Require Import Coqlib Compopts. Require Import AST Integers Floats. Require Import Op Registers. Require Import ValueDomain ValueAOp. +Require SelectOp. (** * Converting known values to constants *) @@ -375,7 +375,7 @@ Nondetfunction op_strength_reduction Nondetfunction addr_strength_reduction (addr: addressing) (args: list reg) (vl: list aval) := match addr, args, vl with - | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil => + | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil ?? negb (SelectOp.symbol_is_relocatable symb) => (Aglobal symb (Ptrofs.add n1 (Ptrofs.of_int64 n)), nil) | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil => (Ainstack (Ptrofs.add n1 (Ptrofs.of_int64 n)), nil) diff --git a/aarch64/ConstpropOpproof.v b/aarch64/ConstpropOpproof.v index deab7cd4..7f5f1e06 100644 --- a/aarch64/ConstpropOpproof.v +++ b/aarch64/ConstpropOpproof.v @@ -391,7 +391,7 @@ Proof. Int.bit_solve. destruct (zlt i0 n0). replace (Int.testbit n i0) with (negb (Int.testbit Int.zero i0)). rewrite Int.bits_zero. simpl. rewrite andb_true_r. auto. - rewrite <- EQ. rewrite Int.bits_zero_ext by omega. rewrite zlt_true by auto. + rewrite <- EQ. rewrite Int.bits_zero_ext by lia. rewrite zlt_true by auto. rewrite Int.bits_not by auto. apply negb_involutive. rewrite H6 by auto. auto. econstructor; split; eauto. auto. diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v index efda835d..f401458c 100644 --- a/aarch64/Conventions1.v +++ b/aarch64/Conventions1.v @@ -24,7 +24,12 @@ Require Archi. - Caller-save registers that can be modified during a function call. We follow the Procedure Call Standard for the ARM 64-bit Architecture - (AArch64) document: R19-R28 and F8-F15 are callee-save. *) + (AArch64) document: R19-R28 and F8-F15 are callee-save. + + X16 is reserved as a temporary for asm generation. + X18 is reserved as the platform register. + X29 is reserved as the frame pointer register. + X30 is reserved as the return address register. *) Definition is_callee_save (r: mreg): bool := match r with @@ -154,9 +159,23 @@ Qed. (** - The first 8 integer arguments are passed in registers [R0...R7]. - The first 8 FP arguments are passed in registers [F0...F7]. -- Extra arguments are passed on the stack, in [Outgoing] slots of size - 64 bits (2 words), consecutively assigned, starting at word offset 0. -**) +- Extra arguments are passed on the stack, in [Outgoing] slots, + consecutively assigned, starting at word offset 0. + +In the standard AAPCS64, all stack slots are 8-byte wide (2 words). + +In the Apple variant, a stack slot has the size of the type of the +corresponding argument, and is aligned accordingly. We use 8-byte +slots (2 words) for C types [long] and [double], and 4-byte slots +(1 word) for C types [int] and [float]. For full conformance, we should +use 1-byte slots for [char] types and 2-byte slots for [short] types, +but this cannot be expressed in CompCert's type algebra, so we +incorrectly use 4-byte slots. + +Concerning variable arguments to vararg functions: +- In the AAPCS64 standard, they are passed like regular, fixed arguments. +- In the Apple variant, they are always passed on stack, in 8-byte slots. +*) Definition int_param_regs := R0 :: R1 :: R2 :: R3 :: R4 :: R5 :: R6 :: R7 :: nil. @@ -164,31 +183,70 @@ Definition int_param_regs := Definition float_param_regs := F0 :: F1 :: F2 :: F3 :: F4 :: F5 :: F6 :: F7 :: nil. +Definition stack_arg (ty: typ) (ir fr ofs: Z) + (rec: Z -> Z -> Z -> list (rpair loc)) := + match Archi.abi with + | Archi.AAPCS64 => + let ofs := align ofs 2 in + One (S Outgoing ofs ty) :: rec ir fr (ofs + 2) + | Archi.Apple => + let ofs := align ofs (typesize ty) in + One (S Outgoing ofs ty) :: rec ir fr (ofs + typesize ty) + end. + +Definition int_arg (ty: typ) (ir fr ofs: Z) + (rec: Z -> Z -> Z -> list (rpair loc)) := + match list_nth_z int_param_regs ir with + | None => + stack_arg ty ir fr ofs rec + | Some ireg => + One (R ireg) :: rec (ir + 1) fr ofs + end. + +Definition float_arg (ty: typ) (ir fr ofs: Z) + (rec: Z -> Z -> Z -> list (rpair loc)) := + match list_nth_z float_param_regs fr with + | None => + stack_arg ty ir fr ofs rec + | Some freg => + One (R freg) :: rec ir (fr + 1) ofs + end. + +Fixpoint loc_arguments_stack (tyl: list typ) (ofs: Z) {struct tyl} : list (rpair loc) := + match tyl with + | nil => nil + | ty :: tys => One (S Outgoing ofs Tany64) :: loc_arguments_stack tys (ofs + 2) + end. + Fixpoint loc_arguments_rec - (tyl: list typ) (ir fr ofs: Z) {struct tyl} : list (rpair loc) := + (tyl: list typ) (fixed ir fr ofs: Z) {struct tyl} : list (rpair loc) := match tyl with | nil => nil - | (Tint | Tlong | Tany32 | Tany64) as ty :: tys => - match list_nth_z int_param_regs ir with - | None => - One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + 2) - | Some ireg => - One (R ireg) :: loc_arguments_rec tys (ir + 1) fr ofs - end - | (Tfloat | Tsingle) as ty :: tys => - match list_nth_z float_param_regs fr with - | None => - One (S Outgoing ofs ty) :: loc_arguments_rec tys ir fr (ofs + 2) - | Some freg => - One (R freg) :: loc_arguments_rec tys ir (fr + 1) ofs + | ty :: tys => + if zle fixed 0 then loc_arguments_stack tyl (align ofs 2) else + match ty with + | Tint | Tlong | Tany32 | Tany64 => + int_arg ty ir fr ofs (loc_arguments_rec tys (fixed - 1)) + | Tfloat | Tsingle => + float_arg ty ir fr ofs (loc_arguments_rec tys (fixed - 1)) end end. +(** Number of fixed arguments for a function with signature [s]. + For AAPCS64, all arguments are treated as fixed, even for a vararg + function. *) + +Definition fixed_arguments (s: signature) : Z := + match Archi.abi, s.(sig_cc).(cc_vararg) with + | Archi.Apple, Some n => n + | _, _ => list_length_z s.(sig_args) + end. + (** [loc_arguments s] returns the list of locations where to store arguments when calling a function with signature [s]. *) Definition loc_arguments (s: signature) : list (rpair loc) := - loc_arguments_rec s.(sig_args) 0 0 0. + loc_arguments_rec s.(sig_args) (fixed_arguments s) 0 0 0. (** Argument locations are either caller-save registers or [Outgoing] stack slots at nonnegative offsets. *) @@ -200,49 +258,73 @@ Definition loc_argument_acceptable (l: loc) : Prop := | _ => False end. -Definition loc_argument_charact (ofs: Z) (l: loc) : Prop := - match l with - | R r => In r int_param_regs \/ In r float_param_regs - | S Outgoing ofs' ty => ofs' >= ofs /\ (2 | ofs') - | _ => False - end. - -Remark loc_arguments_rec_charact: - forall tyl ir fr ofs p, - In p (loc_arguments_rec tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_charact ofs) p. +Lemma loc_arguments_rec_charact: + forall tyl fixed ri rf ofs p, + ofs >= 0 -> + In p (loc_arguments_rec tyl fixed ri rf ofs) -> forall_rpair loc_argument_acceptable p. Proof. - assert (X: forall ofs1 ofs2 l, loc_argument_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } - assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_charact ofs1) p). - { destruct p; simpl; intuition eauto. } - assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). - { intros. apply Z.divide_add_r; auto. apply Z.divide_refl. } -Opaque list_nth_z. - induction tyl; simpl loc_arguments_rec; intros. -- contradiction. -- assert (A: forall ty, In p - match list_nth_z int_param_regs ir with - | Some ireg => One (R ireg) :: loc_arguments_rec tyl (ir + 1) fr ofs - | None => One (S Outgoing ofs ty) :: loc_arguments_rec tyl ir fr (ofs + 2) - end -> - forall_rpair (loc_argument_charact ofs) p). - { intros. destruct (list_nth_z int_param_regs ir) as [r|] eqn:E; destruct H1. - subst. left. eapply list_nth_z_in; eauto. - eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } - assert (B: forall ty, In p - match list_nth_z float_param_regs fr with - | Some ireg => One (R ireg) :: loc_arguments_rec tyl ir (fr + 1) ofs - | None => One (S Outgoing ofs ty) :: loc_arguments_rec tyl ir fr (ofs + 2) - end -> - forall_rpair (loc_argument_charact ofs) p). - { intros. destruct (list_nth_z float_param_regs fr) as [r|] eqn:E; destruct H1. - subst. right. eapply list_nth_z_in; eauto. - eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } - destruct a; eauto. + set (OK := fun (l: list (rpair loc)) => + forall p, In p l -> forall_rpair loc_argument_acceptable p). + set (OKF := fun (f: Z -> Z -> Z -> list (rpair loc)) => + forall ri rf ofs, ofs >= 0 -> OK (f ri rf ofs)). + assert (CSI: forall r, In r int_param_regs -> is_callee_save r = false). + { decide_goal. } + assert (CSF: forall r, In r float_param_regs -> is_callee_save r = false). + { decide_goal. } + assert (ALP: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0). + { intros. + assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos). + lia. } + assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))). + { intros. apply Z.divide_trans with (typesize ty). apply typealign_typesize. apply align_divides. apply typesize_pos. } + assert (ALP2: forall ofs, ofs >= 0 -> align ofs 2 >= 0). + { intros. + assert (ofs <= align ofs 2) by (apply align_le; lia). + lia. } + assert (ALD2: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs 2)). + { intros. eapply Z.divide_trans with 2. + exists (2 / typealign ty). destruct ty; reflexivity. + apply align_divides. lia. } + assert (STK: forall tyl ofs, + ofs >= 0 -> OK (loc_arguments_stack tyl ofs)). + { induction tyl as [ | ty tyl]; intros ofs OO; red; simpl; intros. + - contradiction. + - destruct H. + + subst p. split. auto. simpl. apply Z.divide_1_l. + + apply IHtyl with (ofs := ofs + 2). lia. auto. + } + assert (A: forall ty ri rf ofs f, + OKF f -> ofs >= 0 -> OK (stack_arg ty ri rf ofs f)). + { intros until f; intros OF OO; red; unfold stack_arg; intros. + destruct Archi.abi; destruct H. + - subst p; simpl; auto. + - eapply OF; [|eauto]. apply ALP2 in OO. lia. + - subst p; simpl; auto. + - eapply OF; [|eauto]. apply (ALP ofs ty) in OO. generalize (typesize_pos ty). lia. + } + assert (B: forall ty ri rf ofs f, + OKF f -> ofs >= 0 -> OK (int_arg ty ri rf ofs f)). + { intros until f; intros OF OO; red; unfold int_arg; intros. + destruct (list_nth_z int_param_regs ri) as [r|] eqn:NTH; [destruct H|]. + - subst p; simpl. apply CSI. eapply list_nth_z_in; eauto. + - eapply OF; eauto. + - eapply A; eauto. + } + assert (C: forall ty ri rf ofs f, + OKF f -> ofs >= 0 -> OK (float_arg ty ri rf ofs f)). + { intros until f; intros OF OO; red; unfold float_arg; intros. + destruct (list_nth_z float_param_regs rf) as [r|] eqn:NTH; [destruct H|]. + - subst p; simpl. apply CSF. eapply list_nth_z_in; eauto. + - eapply OF; eauto. + - eapply A; eauto. + } + cut (forall tyl fixed ri rf ofs, ofs >= 0 -> OK (loc_arguments_rec tyl fixed ri rf ofs)). + unfold OK. eauto. + induction tyl as [ | ty1 tyl]; intros until ofs; intros OO; simpl. +- red; simpl; tauto. +- destruct (zle fixed 0). + + apply (STK (ty1 :: tyl)); auto. + + unfold OKF in *; destruct ty1; eauto. Qed. Lemma loc_arguments_acceptable: @@ -250,19 +332,10 @@ Lemma loc_arguments_acceptable: In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p. Proof. unfold loc_arguments; intros. - assert (A: forall r, In r int_param_regs -> is_callee_save r = false) by decide_goal. - assert (B: forall r, In r float_param_regs -> is_callee_save r = false) by decide_goal. - 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 [C|C]; auto. - intros [C D]. split; auto. apply Z.divide_trans with 2; auto. - exists (2 / typealign ty); destruct ty; reflexivity. - } - exploit loc_arguments_rec_charact; eauto using Z.divide_0_r. - unfold forall_rpair; destruct p; intuition auto. + eapply loc_arguments_rec_charact; eauto. lia. Qed. -Hint Resolve loc_arguments_acceptable: locs. +Global Hint Resolve loc_arguments_acceptable: locs. Lemma loc_arguments_main: loc_arguments signature_main = nil. @@ -270,16 +343,29 @@ Proof. unfold loc_arguments; reflexivity. Qed. -(** ** Normalization of function results *) +(** ** Normalization of function results and parameters *) (** According to the AAPCS64 ABI specification, "padding bits" in the return - value of a function have unpredictable values and must be ignored. - Consequently, we force normalization of return values of small integer - types (8- and 16-bit integers), so that the top bits (the "padding bits") - are proper sign- or zero-extensions of the small integer value. *) + value of a function or in a function parameter have unpredictable + values and must be ignored. Consequently, we force normalization + of return values and of function parameters when they have small + integer types (8- and 16-bit integers), so that the top bits (the + "padding bits") are proper sign- or zero-extensions of the small + integer value. + + The Apple variant of the AAPCS64 requires the callee to return a normalized + value, and the caller to pass normalized parameters, hence no + normalization is needed. + *) Definition return_value_needs_normalization (t: rettype) : bool := - match t with - | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true - | _ => false + match Archi.abi with + | Archi.Apple => false + | Archi.AAPCS64 => + match t with + | Tint8signed | Tint8unsigned | Tint16signed | Tint16unsigned => true + | _ => false + end end. + +Definition parameter_needs_normalization := return_value_needs_normalization. diff --git a/aarch64/Op.v b/aarch64/Op.v index a7483d56..f8d2510e 100644 --- a/aarch64/Op.v +++ b/aarch64/Op.v @@ -957,25 +957,25 @@ End SHIFT_AMOUNT. Program Definition mk_amount32 (n: int): amount32 := {| a32_amount := Int.zero_ext 5 n |}. Next Obligation. - apply mk_amount_range. omega. reflexivity. + apply mk_amount_range. lia. reflexivity. Qed. Lemma mk_amount32_eq: forall n, Int.ltu n Int.iwordsize = true -> a32_amount (mk_amount32 n) = n. Proof. - intros. eapply mk_amount_eq; eauto. omega. reflexivity. + intros. eapply mk_amount_eq; eauto. lia. reflexivity. Qed. Program Definition mk_amount64 (n: int): amount64 := {| a64_amount := Int.zero_ext 6 n |}. Next Obligation. - apply mk_amount_range. omega. reflexivity. + apply mk_amount_range. lia. reflexivity. Qed. Lemma mk_amount64_eq: forall n, Int.ltu n Int64.iwordsize' = true -> a64_amount (mk_amount64 n) = n. Proof. - intros. eapply mk_amount_eq; eauto. omega. reflexivity. + intros. eapply mk_amount_eq; eauto. lia. reflexivity. Qed. (** Recognition of move operations. *) diff --git a/aarch64/SelectLongproof.v b/aarch64/SelectLongproof.v index b051369c..aee09b12 100644 --- a/aarch64/SelectLongproof.v +++ b/aarch64/SelectLongproof.v @@ -225,8 +225,8 @@ Proof. intros. unfold Int.ltu; apply zlt_true. apply Int.ltu_inv in H. apply Int.ltu_inv in H0. change (Int.unsigned Int64.iwordsize') with Int64.zwordsize in *. - unfold Int.sub; rewrite Int.unsigned_repr. omega. - assert (Int64.zwordsize < Int.max_unsigned) by reflexivity. omega. + unfold Int.sub; rewrite Int.unsigned_repr. lia. + assert (Int64.zwordsize < Int.max_unsigned) by reflexivity. lia. Qed. Theorem eval_shrluimm: @@ -242,13 +242,13 @@ Local Opaque Int64.zwordsize. + destruct (Int.ltu n a) eqn:L2. * assert (L3: Int.ltu (Int.sub a n) Int64.iwordsize' = true). { apply sub_shift_amount; auto using a64_range. - apply Int.ltu_inv in L2. omega. } + apply Int.ltu_inv in L2. lia. } econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto. simpl. rewrite L. rewrite Int64.shru'_shl', L2 by auto using a64_range. auto. * assert (L3: Int.ltu (Int.sub n a) Int64.iwordsize' = true). { apply sub_shift_amount; auto using a64_range. - unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. } + unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. } econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto. simpl. rewrite L. rewrite Int64.shru'_shl', L2 by auto using a64_range. auto. @@ -261,11 +261,11 @@ Local Opaque Int64.zwordsize. * econstructor; split. EvalOp. rewrite mk_amount64_eq by auto. destruct v1; simpl; auto. rewrite ! L; simpl. set (s' := s - Int.unsigned n). - replace s with (s' + Int.unsigned n) by (unfold s'; omega). - rewrite Int64.shru'_zero_ext. auto. unfold s'; omega. + replace s with (s' + Int.unsigned n) by (unfold s'; lia). + rewrite Int64.shru'_zero_ext. auto. unfold s'; lia. * econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite ! L; simpl. - rewrite Int64.shru'_zero_ext_0 by omega. auto. + rewrite Int64.shru'_zero_ext_0 by lia. auto. + econstructor; eauto using eval_shrluimm_base. - intros; TrivialExists. Qed. @@ -290,13 +290,13 @@ Proof. + destruct (Int.ltu n a) eqn:L2. * assert (L3: Int.ltu (Int.sub a n) Int64.iwordsize' = true). { apply sub_shift_amount; auto using a64_range. - apply Int.ltu_inv in L2. omega. } + apply Int.ltu_inv in L2. lia. } econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto. simpl. rewrite L. rewrite Int64.shr'_shl', L2 by auto using a64_range. auto. * assert (L3: Int.ltu (Int.sub n a) Int64.iwordsize' = true). { apply sub_shift_amount; auto using a64_range. - unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. } + unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. } econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite mk_amount64_eq, L3, a64_range by auto. simpl. rewrite L. rewrite Int64.shr'_shl', L2 by auto using a64_range. auto. @@ -309,8 +309,8 @@ Proof. * InvBooleans. econstructor; split. EvalOp. rewrite mk_amount64_eq by auto. destruct v1; simpl; auto. rewrite ! L; simpl. set (s' := s - Int.unsigned n). - replace s with (s' + Int.unsigned n) by (unfold s'; omega). - rewrite Int64.shr'_sign_ext. auto. unfold s'; omega. unfold s'; omega. + replace s with (s' + Int.unsigned n) by (unfold s'; lia). + rewrite Int64.shr'_sign_ext. auto. unfold s'; lia. unfold s'; lia. * econstructor; split; [|eauto]. apply eval_shrlimm_base; auto. EvalOp. + econstructor; eauto using eval_shrlimm_base. - intros; TrivialExists. @@ -392,7 +392,7 @@ Proof. - TrivialExists. - destruct (zlt (Int.unsigned a0) sz). + econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite a64_range; simpl. - apply Val.lessdef_same. f_equal. rewrite Int64.shl'_zero_ext by omega. f_equal. omega. + apply Val.lessdef_same. f_equal. rewrite Int64.shl'_zero_ext by lia. f_equal. lia. + TrivialExists. - TrivialExists. Qed. diff --git a/aarch64/SelectOp.vp b/aarch64/SelectOp.vp index 5bd96987..b5a03989 100644 --- a/aarch64/SelectOp.vp +++ b/aarch64/SelectOp.vp @@ -536,10 +536,18 @@ Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) := (** ** Recognition of addressing modes for load and store operations *) +(** Some symbols are relocatable (e.g. external symbols in macOS) + and cannot be used with [Aglobal] addressing mode. *) + +Parameter symbol_is_relocatable: ident -> bool. + Nondetfunction addressing (chunk: memory_chunk) (e: expr) := match e with | Eop (Oaddrstack n) Enil => (Ainstack n, Enil) - | Eop (Oaddrsymbol id ofs) Enil => (Aglobal id ofs, Enil) + | Eop (Oaddrsymbol id ofs) Enil => + if symbol_is_relocatable id + then (Aindexed (Ptrofs.to_int64 ofs), Eop (Oaddrsymbol id Ptrofs.zero) Enil ::: Enil) + else (Aglobal id ofs, Enil) | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed n, e1:::Enil) | Eop (Oaddlshift Slsl a) (e1:::e2:::Enil) => (Aindexed2shift a, e1:::e2:::Enil) | Eop (Oaddlext x a) (e1:::e2:::Enil) => (Aindexed2ext x a, e1:::e2:::Enil) diff --git a/aarch64/SelectOpproof.v b/aarch64/SelectOpproof.v index b78a5ed8..ccc4c0f1 100644 --- a/aarch64/SelectOpproof.v +++ b/aarch64/SelectOpproof.v @@ -243,8 +243,8 @@ Remark sub_shift_amount: Proof. intros. unfold Int.ltu; apply zlt_true. rewrite Int.unsigned_repr_wordsize. apply Int.ltu_iwordsize_inv in H. apply Int.ltu_iwordsize_inv in H0. - unfold Int.sub; rewrite Int.unsigned_repr. omega. - generalize Int.wordsize_max_unsigned; omega. + unfold Int.sub; rewrite Int.unsigned_repr. lia. + generalize Int.wordsize_max_unsigned; lia. Qed. Theorem eval_shruimm: @@ -260,13 +260,13 @@ Local Opaque Int.zwordsize. + destruct (Int.ltu n a) eqn:L2. * assert (L3: Int.ltu (Int.sub a n) Int.iwordsize = true). { apply sub_shift_amount; auto using a32_range. - apply Int.ltu_inv in L2. omega. } + apply Int.ltu_inv in L2. lia. } econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto. simpl. rewrite L. rewrite Int.shru_shl, L2 by auto using a32_range. auto. * assert (L3: Int.ltu (Int.sub n a) Int.iwordsize = true). { apply sub_shift_amount; auto using a32_range. - unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. } + unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. } econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto. simpl. rewrite L. rewrite Int.shru_shl, L2 by auto using a32_range. auto. @@ -279,11 +279,11 @@ Local Opaque Int.zwordsize. * econstructor; split. EvalOp. rewrite mk_amount32_eq by auto. destruct v1; simpl; auto. rewrite ! L; simpl. set (s' := s - Int.unsigned n). - replace s with (s' + Int.unsigned n) by (unfold s'; omega). - rewrite Int.shru_zero_ext. auto. unfold s'; omega. + replace s with (s' + Int.unsigned n) by (unfold s'; lia). + rewrite Int.shru_zero_ext. auto. unfold s'; lia. * econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite ! L; simpl. - rewrite Int.shru_zero_ext_0 by omega. auto. + rewrite Int.shru_zero_ext_0 by lia. auto. + econstructor; eauto using eval_shruimm_base. - intros; TrivialExists. Qed. @@ -308,13 +308,13 @@ Proof. + destruct (Int.ltu n a) eqn:L2. * assert (L3: Int.ltu (Int.sub a n) Int.iwordsize = true). { apply sub_shift_amount; auto using a32_range. - apply Int.ltu_inv in L2. omega. } + apply Int.ltu_inv in L2. lia. } econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto. simpl. rewrite L. rewrite Int.shr_shl, L2 by auto using a32_range. auto. * assert (L3: Int.ltu (Int.sub n a) Int.iwordsize = true). { apply sub_shift_amount; auto using a32_range. - unfold Int.ltu in L2. destruct zlt in L2; discriminate || omega. } + unfold Int.ltu in L2. destruct zlt in L2; discriminate || lia. } econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite mk_amount32_eq, L3, a32_range by auto. simpl. rewrite L. rewrite Int.shr_shl, L2 by auto using a32_range. auto. @@ -327,8 +327,8 @@ Proof. * InvBooleans. econstructor; split. EvalOp. rewrite mk_amount32_eq by auto. destruct v1; simpl; auto. rewrite ! L; simpl. set (s' := s - Int.unsigned n). - replace s with (s' + Int.unsigned n) by (unfold s'; omega). - rewrite Int.shr_sign_ext. auto. unfold s'; omega. unfold s'; omega. + replace s with (s' + Int.unsigned n) by (unfold s'; lia). + rewrite Int.shr_sign_ext. auto. unfold s'; lia. unfold s'; lia. * econstructor; split; [|eauto]. apply eval_shrimm_base; auto. EvalOp. + econstructor; eauto using eval_shrimm_base. - intros; TrivialExists. @@ -399,20 +399,20 @@ Proof. change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl. apply Val.lessdef_same. f_equal. transitivity (Int.repr (Z.shiftr (Int.signed i * Int.signed i0) 32)). - unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity. + unfold Int.mulhs; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity. apply Int.same_bits_eq; intros n N. change Int.zwordsize with 32 in *. - assert (N1: 0 <= n < 64) by omega. + assert (N1: 0 <= n < 64) by lia. rewrite Int64.bits_loword by auto. rewrite Int64.bits_shr' by auto. change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64. - rewrite zlt_true by omega. + rewrite zlt_true by lia. rewrite Int.testbit_repr by auto. - unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega). + unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia). transitivity (Z.testbit (Int.signed i * Int.signed i0) (n + 32)). - rewrite Z.shiftr_spec by omega. auto. + rewrite Z.shiftr_spec by lia. auto. apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. - change Int64.zwordsize with 64; omega. + change Int64.zwordsize with 64; lia. Qed. Theorem eval_mulhu: binary_constructor_sound mulhu Val.mulhu. @@ -425,20 +425,20 @@ Proof. change (Int.ltu (Int.repr 32) Int64.iwordsize') with true; simpl. apply Val.lessdef_same. f_equal. transitivity (Int.repr (Z.shiftr (Int.unsigned i * Int.unsigned i0) 32)). - unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by omega. reflexivity. + unfold Int.mulhu; f_equal. rewrite Zshiftr_div_two_p by lia. reflexivity. apply Int.same_bits_eq; intros n N. change Int.zwordsize with 32 in *. - assert (N1: 0 <= n < 64) by omega. + assert (N1: 0 <= n < 64) by lia. rewrite Int64.bits_loword by auto. rewrite Int64.bits_shru' by auto. change (Int.unsigned (Int.repr 32)) with 32. change Int64.zwordsize with 64. - rewrite zlt_true by omega. + rewrite zlt_true by lia. rewrite Int.testbit_repr by auto. - unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; omega). + unfold Int64.mul. rewrite Int64.testbit_repr by (change Int64.zwordsize with 64; lia). transitivity (Z.testbit (Int.unsigned i * Int.unsigned i0) (n + 32)). - rewrite Z.shiftr_spec by omega. auto. + rewrite Z.shiftr_spec by lia. auto. apply Int64.same_bits_eqm. apply Int64.eqm_mult; apply Int64.eqm_unsigned_repr. - change Int64.zwordsize with 64; omega. + change Int64.zwordsize with 64; lia. Qed. (** Integer conversions *) @@ -451,7 +451,7 @@ Proof. - TrivialExists. - destruct (zlt (Int.unsigned a0) sz). + econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite a32_range; simpl. - apply Val.lessdef_same. f_equal. rewrite Int.shl_zero_ext by omega. f_equal. omega. + apply Val.lessdef_same. f_equal. rewrite Int.shl_zero_ext by lia. f_equal. lia. + TrivialExists. - TrivialExists. Qed. @@ -464,29 +464,29 @@ Proof. - TrivialExists. - destruct (zlt (Int.unsigned a0) sz). + econstructor; split. EvalOp. destruct v1; simpl; auto. rewrite a32_range; simpl. - apply Val.lessdef_same. f_equal. rewrite Int.shl_sign_ext by omega. f_equal. omega. + apply Val.lessdef_same. f_equal. rewrite Int.shl_sign_ext by lia. f_equal. lia. + TrivialExists. - TrivialExists. Qed. Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). Proof. - apply eval_sign_ext; omega. + apply eval_sign_ext; lia. Qed. Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). Proof. - apply eval_zero_ext; omega. + apply eval_zero_ext; lia. Qed. Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). Proof. - apply eval_sign_ext; omega. + apply eval_sign_ext; lia. Qed. Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). Proof. - apply eval_zero_ext; omega. + apply eval_zero_ext; lia. Qed. (** Bitwise not, and, or, xor *) @@ -1029,7 +1029,13 @@ Theorem eval_addressing: Proof. intros until v. unfold addressing; case (addressing_match a); intros; InvEval. - econstructor; split. EvalOp. simpl; auto. -- econstructor; split. EvalOp. simpl; auto. +- destruct (symbol_is_relocatable id). + + exists (Genv.symbol_address ge id Ptrofs.zero :: nil); split. + constructor. EvalOp. constructor. + simpl. rewrite <- Genv.shift_symbol_address_64 by auto. + rewrite Ptrofs.of_int64_to_int64, Ptrofs.add_zero_l by auto. + auto. + + econstructor; split. EvalOp. simpl; auto. - econstructor; split. EvalOp. simpl. destruct v1; try discriminate. rewrite <- H; auto. - econstructor; split. EvalOp. simpl. congruence. diff --git a/aarch64/Stacklayout.v b/aarch64/Stacklayout.v index 86ba9f45..cdbc64d5 100644 --- a/aarch64/Stacklayout.v +++ b/aarch64/Stacklayout.v @@ -67,13 +67,13 @@ Local Opaque Z.add Z.mul sepconj range. set (ostkdata := align (ol + 4 * b.(bound_local)) 8). change (size_chunk Mptr) with 8. generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= 4 * b.(bound_outgoing)) by omega. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + 8 <= oretaddr) by (unfold oretaddr; omega). - assert (oretaddr + 8 <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + 8 <= oretaddr) by (unfold oretaddr; lia). + assert (oretaddr + 8 <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). - assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). - assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). (* Reorder as: outgoing back link @@ -86,11 +86,11 @@ Local Opaque Z.add Z.mul sepconj range. rewrite sep_swap45. (* Apply range_split and range_split2 repeatedly *) unfold fe_ofs_arg. - apply range_split_2. fold olink; omega. omega. - apply range_split. omega. - apply range_split. omega. - apply range_split_2. fold ol. omega. omega. - apply range_drop_right with ostkdata. omega. + apply range_split_2. fold olink; lia. lia. + apply range_split. lia. + apply range_split. lia. + apply range_split_2. fold ol. lia. lia. + apply range_drop_right with ostkdata. lia. eapply sep_drop2. eexact H. Qed. @@ -106,14 +106,14 @@ Proof. set (ol := align (size_callee_save_area b ocs) 8). set (ostkdata := align (ol + 4 * b.(bound_local)) 8). generalize b.(bound_local_pos) b.(bound_outgoing_pos) b.(bound_stack_data_pos); intros. - assert (0 <= 4 * b.(bound_outgoing)) by omega. - assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; omega). - assert (olink + 8 <= oretaddr) by (unfold oretaddr; omega). - assert (oretaddr + 8 <= ocs) by (unfold ocs; omega). + assert (0 <= 4 * b.(bound_outgoing)) by lia. + assert (4 * b.(bound_outgoing) <= olink) by (apply align_le; lia). + assert (olink + 8 <= oretaddr) by (unfold oretaddr; lia). + assert (oretaddr + 8 <= ocs) by (unfold ocs; lia). assert (ocs <= size_callee_save_area b ocs) by (apply size_callee_save_area_incr). - assert (size_callee_save_area b ocs <= ol) by (apply align_le; omega). - assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; omega). - split. omega. apply align_le. omega. + assert (size_callee_save_area b ocs <= ol) by (apply align_le; lia). + assert (ol + 4 * b.(bound_local) <= ostkdata) by (apply align_le; lia). + split. lia. apply align_le. lia. Qed. Lemma frame_env_aligned: @@ -133,8 +133,8 @@ Proof. set (ostkdata := align (ol + 4 * b.(bound_local)) 8). change (align_chunk Mptr) with 8. split. apply Z.divide_0_r. - split. apply align_divides; omega. - split. apply align_divides; omega. - split. apply align_divides; omega. - apply Z.divide_add_r. apply align_divides; omega. apply Z.divide_refl. + split. apply align_divides; lia. + split. apply align_divides; lia. + split. apply align_divides; lia. + apply Z.divide_add_r. apply align_divides; lia. apply Z.divide_refl. Qed. diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index 78b9eb2a..a9d47bdd 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -36,107 +36,135 @@ let is_immediate_float32 bits = let mant = Int32.logand bits 0x7F_FFFFl in exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant -(* Module containing the printing functions *) +(* Naming and printing registers *) + +let intsz oc (sz, n) = + match sz with X -> coqint64 oc n | W -> coqint oc n + +let xreg_name = function + | X0 -> "x0" | X1 -> "x1" | X2 -> "x2" | X3 -> "x3" + | X4 -> "x4" | X5 -> "x5" | X6 -> "x6" | X7 -> "x7" + | X8 -> "x8" | X9 -> "x9" | X10 -> "x10" | X11 -> "x11" + | X12 -> "x12" | X13 -> "x13" | X14 -> "x14" | X15 -> "x15" + | X16 -> "x16" | X17 -> "x17" | X18 -> "x18" | X19 -> "x19" + | X20 -> "x20" | X21 -> "x21" | X22 -> "x22" | X23 -> "x23" + | X24 -> "x24" | X25 -> "x25" | X26 -> "x26" | X27 -> "x27" + | X28 -> "x28" | X29 -> "x29" | X30 -> "x30" + +let wreg_name = function + | X0 -> "w0" | X1 -> "w1" | X2 -> "w2" | X3 -> "w3" + | X4 -> "w4" | X5 -> "w5" | X6 -> "w6" | X7 -> "w7" + | X8 -> "w8" | X9 -> "w9" | X10 -> "w10" | X11 -> "w11" + | X12 -> "w12" | X13 -> "w13" | X14 -> "w14" | X15 -> "w15" + | X16 -> "w16" | X17 -> "w17" | X18 -> "w18" | X19 -> "w19" + | X20 -> "w20" | X21 -> "w21" | X22 -> "w22" | X23 -> "w23" + | X24 -> "w24" | X25 -> "w25" | X26 -> "w26" | X27 -> "w27" + | X28 -> "w28" | X29 -> "w29" | X30 -> "w30" + +let xreg0_name = function RR0 r -> xreg_name r | XZR -> "xzr" +let wreg0_name = function RR0 r -> wreg_name r | XZR -> "wzr" + +let xregsp_name = function RR1 r -> xreg_name r | XSP -> "sp" +let wregsp_name = function RR1 r -> wreg_name r | XSP -> "wsp" + +let dreg_name = function +| D0 -> "d0" | D1 -> "d1" | D2 -> "d2" | D3 -> "d3" +| D4 -> "d4" | D5 -> "d5" | D6 -> "d6" | D7 -> "d7" +| D8 -> "d8" | D9 -> "d9" | D10 -> "d10" | D11 -> "d11" +| D12 -> "d12" | D13 -> "d13" | D14 -> "d14" | D15 -> "d15" +| D16 -> "d16" | D17 -> "d17" | D18 -> "d18" | D19 -> "d19" +| D20 -> "d20" | D21 -> "d21" | D22 -> "d22" | D23 -> "d23" +| D24 -> "d24" | D25 -> "d25" | D26 -> "d26" | D27 -> "d27" +| D28 -> "d28" | D29 -> "d29" | D30 -> "d30" | D31 -> "d31" + +let sreg_name = function +| D0 -> "s0" | D1 -> "s1" | D2 -> "s2" | D3 -> "s3" +| D4 -> "s4" | D5 -> "s5" | D6 -> "s6" | D7 -> "s7" +| D8 -> "s8" | D9 -> "s9" | D10 -> "s10" | D11 -> "s11" +| D12 -> "s12" | D13 -> "s13" | D14 -> "s14" | D15 -> "s15" +| D16 -> "s16" | D17 -> "s17" | D18 -> "s18" | D19 -> "s19" +| D20 -> "s20" | D21 -> "s21" | D22 -> "s22" | D23 -> "s23" +| D24 -> "s24" | D25 -> "s25" | D26 -> "s26" | D27 -> "s27" +| D28 -> "s28" | D29 -> "s29" | D30 -> "s30" | D31 -> "s31" + +let xreg oc r = output_string oc (xreg_name r) +let wreg oc r = output_string oc (wreg_name r) +let ireg oc (sz, r) = + output_string oc (match sz with X -> xreg_name r | W -> wreg_name r) + +let xreg0 oc r = output_string oc (xreg0_name r) +let wreg0 oc r = output_string oc (wreg0_name r) +let ireg0 oc (sz, r) = + output_string oc (match sz with X -> xreg0_name r | W -> wreg0_name r) + +let xregsp oc r = output_string oc (xregsp_name r) +let iregsp oc (sz, r) = + output_string oc (match sz with X -> xregsp_name r | W -> wregsp_name r) + +let dreg oc r = output_string oc (dreg_name r) +let sreg oc r = output_string oc (sreg_name r) +let freg oc (sz, r) = + output_string oc (match sz with D -> dreg_name r | S -> sreg_name r) + +let preg_asm oc ty = function + | IR r -> if ty = Tint then wreg oc r else xreg oc r + | FR r -> if ty = Tsingle then sreg oc r else dreg oc r + | _ -> assert false + +let preg_annot = function + | IR r -> xreg_name r + | FR r -> dreg_name r + | _ -> assert false + +(* Base-2 log of a Caml integer *) +let rec log2 n = + assert (n > 0); + if n = 1 then 0 else 1 + log2 (n lsr 1) + +(* System dependent printer functions *) + +module type SYSTEM = + sig + val comment: string + val raw_symbol: out_channel -> string -> unit + val symbol: out_channel -> P.t -> unit + val symbol_offset_high: out_channel -> P.t * Z.t -> unit + val symbol_offset_low: out_channel -> P.t * Z.t -> unit + val label: out_channel -> int -> unit + val label_high: out_channel -> int -> unit + val label_low: out_channel -> int -> unit + val load_symbol_address: out_channel -> ireg -> P.t -> unit + val name_of_section: section_name -> string + val print_fun_info: out_channel -> P.t -> unit + val print_var_info: out_channel -> P.t -> unit + val print_comm_decl: out_channel -> P.t -> Z.t -> int -> unit + val print_lcomm_decl: out_channel -> P.t -> Z.t -> int -> unit + end -module Target : TARGET = +module ELF_System : SYSTEM = struct - -(* Basic printing functions *) - let comment = "//" + let raw_symbol = output_string + let symbol = elf_symbol + let symbol_offset_high = elf_symbol_offset + let symbol_offset_low oc id_ofs = + fprintf oc "#:lo12:%a" elf_symbol_offset id_ofs - let symbol = elf_symbol - let symbol_offset = elf_symbol_offset - let label = elf_label + let label = elf_label + let label_high = elf_label + let label_low oc lbl = + fprintf oc "#:lo12:%a" elf_label lbl - let print_label oc lbl = label oc (transl_label lbl) - - let intsz oc (sz, n) = - match sz with X -> coqint64 oc n | W -> coqint oc n - - let xreg_name = function - | X0 -> "x0" | X1 -> "x1" | X2 -> "x2" | X3 -> "x3" - | X4 -> "x4" | X5 -> "x5" | X6 -> "x6" | X7 -> "x7" - | X8 -> "x8" | X9 -> "x9" | X10 -> "x10" | X11 -> "x11" - | X12 -> "x12" | X13 -> "x13" | X14 -> "x14" | X15 -> "x15" - | X16 -> "x16" | X17 -> "x17" | X18 -> "x18" | X19 -> "x19" - | X20 -> "x20" | X21 -> "x21" | X22 -> "x22" | X23 -> "x23" - | X24 -> "x24" | X25 -> "x25" | X26 -> "x26" | X27 -> "x27" - | X28 -> "x28" | X29 -> "x29" | X30 -> "x30" - - let wreg_name = function - | X0 -> "w0" | X1 -> "w1" | X2 -> "w2" | X3 -> "w3" - | X4 -> "w4" | X5 -> "w5" | X6 -> "w6" | X7 -> "w7" - | X8 -> "w8" | X9 -> "w9" | X10 -> "w10" | X11 -> "w11" - | X12 -> "w12" | X13 -> "w13" | X14 -> "w14" | X15 -> "w15" - | X16 -> "w16" | X17 -> "w17" | X18 -> "w18" | X19 -> "w19" - | X20 -> "w20" | X21 -> "w21" | X22 -> "w22" | X23 -> "w23" - | X24 -> "w24" | X25 -> "w25" | X26 -> "w26" | X27 -> "w27" - | X28 -> "w28" | X29 -> "w29" | X30 -> "w30" - - let xreg0_name = function RR0 r -> xreg_name r | XZR -> "xzr" - let wreg0_name = function RR0 r -> wreg_name r | XZR -> "wzr" - - let xregsp_name = function RR1 r -> xreg_name r | XSP -> "sp" - let wregsp_name = function RR1 r -> wreg_name r | XSP -> "wsp" - - let dreg_name = function - | D0 -> "d0" | D1 -> "d1" | D2 -> "d2" | D3 -> "d3" - | D4 -> "d4" | D5 -> "d5" | D6 -> "d6" | D7 -> "d7" - | D8 -> "d8" | D9 -> "d9" | D10 -> "d10" | D11 -> "d11" - | D12 -> "d12" | D13 -> "d13" | D14 -> "d14" | D15 -> "d15" - | D16 -> "d16" | D17 -> "d17" | D18 -> "d18" | D19 -> "d19" - | D20 -> "d20" | D21 -> "d21" | D22 -> "d22" | D23 -> "d23" - | D24 -> "d24" | D25 -> "d25" | D26 -> "d26" | D27 -> "d27" - | D28 -> "d28" | D29 -> "d29" | D30 -> "d30" | D31 -> "d31" - - let sreg_name = function - | D0 -> "s0" | D1 -> "s1" | D2 -> "s2" | D3 -> "s3" - | D4 -> "s4" | D5 -> "s5" | D6 -> "s6" | D7 -> "s7" - | D8 -> "s8" | D9 -> "s9" | D10 -> "s10" | D11 -> "s11" - | D12 -> "s12" | D13 -> "s13" | D14 -> "s14" | D15 -> "s15" - | D16 -> "s16" | D17 -> "s17" | D18 -> "s18" | D19 -> "s19" - | D20 -> "s20" | D21 -> "s21" | D22 -> "s22" | D23 -> "s23" - | D24 -> "s24" | D25 -> "s25" | D26 -> "s26" | D27 -> "s27" - | D28 -> "s28" | D29 -> "s29" | D30 -> "s30" | D31 -> "s31" - - let xreg oc r = output_string oc (xreg_name r) - let wreg oc r = output_string oc (wreg_name r) - let ireg oc (sz, r) = - output_string oc (match sz with X -> xreg_name r | W -> wreg_name r) - - let xreg0 oc r = output_string oc (xreg0_name r) - let wreg0 oc r = output_string oc (wreg0_name r) - let ireg0 oc (sz, r) = - output_string oc (match sz with X -> xreg0_name r | W -> wreg0_name r) - - let xregsp oc r = output_string oc (xregsp_name r) - let iregsp oc (sz, r) = - output_string oc (match sz with X -> xregsp_name r | W -> wregsp_name r) - - let dreg oc r = output_string oc (dreg_name r) - let sreg oc r = output_string oc (sreg_name r) - let freg oc (sz, r) = - output_string oc (match sz with D -> dreg_name r | S -> sreg_name r) - - let preg_asm oc ty = function - | IR r -> if ty = Tint then wreg oc r else xreg oc r - | FR r -> if ty = Tsingle then sreg oc r else dreg oc r - | _ -> assert false - - let preg_annot = function - | IR r -> xreg_name r - | FR r -> dreg_name r - | _ -> assert false - -(* Names of sections *) + let load_symbol_address oc rd id = + fprintf oc " adrp %a, :got:%a\n" xreg rd symbol id; + fprintf oc " ldr %a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id let name_of_section = function | Section_text -> ".text" | Section_data i | Section_small_data i -> - if i then ".data" else common_section () + variable_section ~sec:".data" ~bss:".bss" i | Section_const i | Section_small_const i -> - if i || (not !Clflags.option_fcommon) then ".section .rodata" else "COMM" + variable_section ~sec:".section .rodata" i | Section_string -> ".section .rodata" | Section_literal -> ".section .rodata" | Section_jumptable -> ".section .rodata" @@ -151,6 +179,94 @@ module Target : TARGET = s (if wr then "w" else "") (if ex then "x" else "") | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note" + let print_fun_info = elf_print_fun_info + let print_var_info = elf_print_var_info + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al + + let print_lcomm_decl oc name sz al = + fprintf oc " .local %a\n" symbol name; + print_comm_decl oc name sz al + + end + +module MacOS_System : SYSTEM = + struct + let comment = ";" + + let raw_symbol oc s = + fprintf oc "_%s" s + + let symbol oc symb = + raw_symbol oc (extern_atom symb) + + let symbol_offset_gen kind oc (id, ofs) = + fprintf oc "%a@%s" symbol id kind; + let ofs = camlint64_of_ptrofs ofs in + if ofs <> 0L then fprintf oc " + %Ld" ofs + + let symbol_offset_high = symbol_offset_gen "PAGE" + let symbol_offset_low = symbol_offset_gen "PAGEOFF" + + let label oc lbl = + fprintf oc "L%d" lbl + + let label_high oc lbl = + fprintf oc "%a@PAGE" label lbl + let label_low oc lbl = + fprintf oc "%a@PAGEOFF" label lbl + + let load_symbol_address oc rd id = + fprintf oc " adrp %a, %a@GOTPAGE\n" xreg rd symbol id; + fprintf oc " ldr %a, [%a, %a@GOTPAGEOFF]\n" xreg rd xreg rd symbol id + + let name_of_section = function + | Section_text -> ".text" + | Section_data i | Section_small_data i -> + variable_section ~sec:".data" i + | Section_const i | Section_small_const i -> + variable_section ~sec:".const" ~reloc:".const_data" i + | Section_string -> ".const" + | Section_literal -> ".const" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section \"%s\", %s, %s" + (if wr then "__DATA" else "__TEXT") s + (if ex then "regular, pure_instructions" else "regular") + | Section_debug_info _ -> ".section __DWARF,__debug_info,regular,debug" + | Section_debug_loc -> ".section __DWARF,__debug_loc,regular,debug" + | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug" + | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug" + | Section_debug_ranges -> ".section __DWARF,__debug_ranges,regular,debug" + | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" + | Section_ais_annotation -> assert false (* Not supported under MacOS *) + + let print_fun_info _ _ = () + let print_var_info _ _ = () + + let print_comm_decl oc name sz al = + fprintf oc " .comm %a, %s, %d\n" + symbol name (Z.to_string sz) (log2 al) + + let print_lcomm_decl oc name sz al = + fprintf oc " .lcomm %a, %s, %d\n" + symbol name (Z.to_string sz) (log2 al) + + end + +(* Module containing the printing functions *) + +module Target(System: SYSTEM): TARGET = + struct + include System + +(* Basic printing functions *) + + let print_label oc lbl = label oc (transl_label lbl) + +(* Names of sections *) + let section oc sec = fprintf oc " %s\n" (name_of_section sec) @@ -206,7 +322,7 @@ module Target : TARGET = | ADlsl(base, r, n) -> fprintf oc "[%a, %a, lsl #%a]" xregsp base xreg r coqint n | ADsxt(base, r, n) -> fprintf oc "[%a, %a, sxtw #%a]" xregsp base wreg r coqint n | ADuxt(base, r, n) -> fprintf oc "[%a, %a, uxtw #%a]" xregsp base wreg r coqint n - | ADadr(base, id, ofs) -> fprintf oc "[%a, #:lo12:%a]" xregsp base symbol_offset (id, ofs) + | ADadr(base, id, ofs) -> fprintf oc "[%a, %a]" xregsp base symbol_offset_low (id, ofs) | ADpostincr(base, n) -> fprintf oc "[%a], #%a" xregsp base coqint64 n (* Print a shifted operand *) @@ -217,15 +333,15 @@ module Target : TARGET = | SOasr n -> fprintf oc ", asr #%a" coqint n | SOror n -> fprintf oc ", ror #%a" coqint n -(* Print a sign- or zero-extended operand *) - let extendop oc = function - | EOsxtb n -> fprintf oc ", sxtb #%a" coqint n - | EOsxth n -> fprintf oc ", sxth #%a" coqint n - | EOsxtw n -> fprintf oc ", sxtw #%a" coqint n - | EOuxtb n -> fprintf oc ", uxtb #%a" coqint n - | EOuxth n -> fprintf oc ", uxth #%a" coqint n - | EOuxtw n -> fprintf oc ", uxtw #%a" coqint n - | EOuxtx n -> fprintf oc ", uxtx #%a" coqint n +(* Print a sign- or zero-extended register operand *) + let regextend oc = function + | (r, EOsxtb n) -> fprintf oc "%a, sxtb #%a" wreg r coqint n + | (r, EOsxth n) -> fprintf oc "%a, sxth #%a" wreg r coqint n + | (r, EOsxtw n) -> fprintf oc "%a, sxtw #%a" wreg r coqint n + | (r, EOuxtb n) -> fprintf oc "%a, uxtb #%a" wreg r coqint n + | (r, EOuxth n) -> fprintf oc "%a, uxth #%a" wreg r coqint n + | (r, EOuxtw n) -> fprintf oc "%a, uxtw #%a" wreg r coqint n + | (r, EOuxtx n) -> fprintf oc "%a, uxtx #%a" xreg r coqint n (* Printing of instructions *) let print_instruction oc = function @@ -312,9 +428,9 @@ module Target : TARGET = fprintf oc " movk %a, #%d, lsl #%d\n" ireg (sz, rd) (Z.to_int n) (Z.to_int pos) (* PC-relative addressing *) | Padrp(rd, id, ofs) -> - fprintf oc " adrp %a, %a\n" xreg rd symbol_offset (id, ofs) + fprintf oc " adrp %a, %a\n" xreg rd symbol_offset_high (id, ofs) | Paddadr(rd, r1, id, ofs) -> - fprintf oc " add %a, %a, #:lo12:%a\n" xreg rd xreg r1 symbol_offset (id, ofs) + fprintf oc " add %a, %a, %a\n" xreg rd xreg r1 symbol_offset_low (id, ofs) (* Bit-field operations *) | Psbfiz(sz, rd, r1, r, s) -> fprintf oc " sbfiz %a, %a, %a, %d\n" ireg (sz, rd) ireg (sz, r1) coqint r (Z.to_int s) @@ -335,13 +451,13 @@ module Target : TARGET = fprintf oc " cmn %a, %a%a\n" ireg0 (sz, r1) ireg (sz, r2) shiftop s (* Integer arithmetic, extending register *) | Paddext(rd, r1, r2, x) -> - fprintf oc " add %a, %a, %a%a\n" xregsp rd xregsp r1 wreg r2 extendop x + fprintf oc " add %a, %a, %a\n" xregsp rd xregsp r1 regextend (r2, x) | Psubext(rd, r1, r2, x) -> - fprintf oc " sub %a, %a, %a%a\n" xregsp rd xregsp r1 wreg r2 extendop x + fprintf oc " sub %a, %a, %a\n" xregsp rd xregsp r1 regextend (r2, x) | Pcmpext(r1, r2, x) -> - fprintf oc " cmp %a, %a%a\n" xreg r1 wreg r2 extendop x + fprintf oc " cmp %a, %a\n" xreg r1 regextend (r2, x) | Pcmnext(r1, r2, x) -> - fprintf oc " cmn %a, %a%a\n" xreg r1 wreg r2 extendop x + fprintf oc " cmn %a, %a\n" xreg r1 regextend (r2, x) (* Logical, shifted register *) | Pand(sz, rd, r1, r2, s) -> fprintf oc " and %a, %a, %a%a\n" ireg (sz, rd) ireg0 (sz, r1) ireg (sz, r2) shiftop s @@ -413,8 +529,8 @@ module Target : TARGET = fprintf oc " fmov %a, #%.7f\n" dreg rd (Int64.float_of_bits d) else begin let lbl = label_literal64 d in - fprintf oc " adrp x16, %a\n" label lbl; - fprintf oc " ldr %a, [x16, #:lo12:%a] %s %.18g\n" dreg rd label lbl comment (Int64.float_of_bits d) + fprintf oc " adrp x16, %a\n" label_high lbl; + fprintf oc " ldr %a, [x16, %a] %s %.18g\n" dreg rd label_low lbl comment (Int64.float_of_bits d) end | Pfmovimms(rd, f) -> let d = camlint_of_coqint (Floats.Float32.to_bits f) in @@ -422,8 +538,8 @@ module Target : TARGET = fprintf oc " fmov %a, #%.7f\n" sreg rd (Int32.float_of_bits d) else begin let lbl = label_literal32 d in - fprintf oc " adrp x16, %a\n" label lbl; - fprintf oc " ldr %a, [x16, #:lo12:%a] %s %.18g\n" sreg rd label lbl comment (Int32.float_of_bits d) + fprintf oc " adrp x16, %a\n" label_high lbl; + fprintf oc " ldr %a, [x16, %a] %s %.18g\n" sreg rd label_low lbl comment (Int32.float_of_bits d) end | Pfmovi(D, rd, r1) -> fprintf oc " fmov %a, %a\n" dreg rd xreg0 r1 @@ -490,8 +606,7 @@ module Target : TARGET = | Plabel lbl -> fprintf oc "%a:\n" print_label lbl | Ploadsymbol(rd, id) -> - fprintf oc " adrp %a, :got:%a\n" xreg rd symbol id; - fprintf oc " ldr %a, [%a, #:got_lo12:%a]\n" xreg rd xreg rd symbol id + load_symbol_address oc rd id | Pcvtsw2x(rd, r1) -> fprintf oc " sxtw %a, %a\n" xreg rd wreg r1 | Pcvtuw2x(rd, r1) -> @@ -554,19 +669,12 @@ module Target : TARGET = jumptables := [] end - let print_fun_info = elf_print_fun_info - let print_optional_fun_info _ = () - let print_var_info = elf_print_var_info - let print_comm_symb oc sz name align = - if C2C.atom_is_static name then - fprintf oc " .local %a\n" symbol name; - fprintf oc " .comm %a, %s, %d\n" - symbol name - (Z.to_string sz) - align + if C2C.atom_is_static name + then print_lcomm_decl oc name sz align + else print_comm_decl oc name sz align let print_instructions oc fn = current_function_sig := fn.fn_sig; @@ -587,7 +695,7 @@ module Target : TARGET = section oc Section_text; end - let default_falignment = 2 + let default_falignment = 4 let cfi_startproc oc = () let cfi_endproc oc = () @@ -595,4 +703,10 @@ module Target : TARGET = end let sel_target () = - (module Target:TARGET) + let module S = + (val (match Configuration.system with + | "linux" -> (module ELF_System : SYSTEM) + | "macos" -> (module MacOS_System : SYSTEM) + | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")) + : SYSTEM) in + (module Target(S) : TARGET) diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v index 5f26dc28..ae0006bc 100644 --- a/aarch64/extractionMachdep.v +++ b/aarch64/extractionMachdep.v @@ -6,22 +6,37 @@ (* *) (* Copyright Institut National de Recherche en Informatique et en *) (* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU General Public License as published by *) -(* the Free Software Foundation, either version 2 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. *) +(* 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. *) (* *) (* *********************************************************************) (* Additional extraction directives specific to the AArch64 port *) -Require Archi Asm. +Require Archi Asm Asmgen SelectOp. (* Archi *) -Extract Constant Archi.pic_code => "fun () -> false". (* for the time being *) +Extract Constant Archi.abi => + "match Configuration.abi with + | ""apple"" -> Apple + | _ -> AAPCS64". + +(* SelectOp *) + +Extract Constant SelectOp.symbol_is_relocatable => + "match Configuration.system with + | ""macos"" -> C2C.atom_is_extern + | _ -> (fun _ -> false)". (* Asm *) + Extract Constant Asm.symbol_low => "fun _ _ _ -> assert false". Extract Constant Asm.symbol_high => "fun _ _ _ -> assert false". + +(* Asmgen *) + Extract Constant Asmgen.symbol_is_aligned => "C2C.atom_is_aligned". |