From e13dd0e143dea85eba9c9dcb79c32f04a152221e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 3 May 2020 09:43:14 +0200 Subject: Dual-license aarch64/{Archi.v,Cbuiltins.ml,extractionMachdep.v} The corresponding files in all other ports are dual-licensed (GPL + non-commercial), there is no reason it should be different for aarch64. --- aarch64/Archi.v | 3 +++ aarch64/CBuiltins.ml | 3 +++ aarch64/extractionMachdep.v | 3 +++ 3 files changed, 9 insertions(+) (limited to 'aarch64') diff --git a/aarch64/Archi.v b/aarch64/Archi.v index aef4ab77..24431cb2 100644 --- a/aarch64/Archi.v +++ b/aarch64/Archi.v @@ -6,6 +6,9 @@ (* *) (* 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. *) (* *) (* *********************************************************************) diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml index fdc1372d..dfd5b768 100644 --- a/aarch64/CBuiltins.ml +++ b/aarch64/CBuiltins.ml @@ -6,6 +6,9 @@ (* *) (* 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. *) (* *) (* *********************************************************************) diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v index e82056e2..5f26dc28 100644 --- a/aarch64/extractionMachdep.v +++ b/aarch64/extractionMachdep.v @@ -6,6 +6,9 @@ (* *) (* 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. *) (* *) (* *********************************************************************) -- cgit From 19aed83caebcae1103e0c4f6e200744492f17545 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 24 Apr 2020 15:17:37 +0200 Subject: Use Hashtbl.find_opt. Replace the pattern `try Some (Hashtbl.find ...) with Not_found -> None` by a call to the function Hashtbl.find_opt. --- aarch64/Machregsaux.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64') diff --git a/aarch64/Machregsaux.ml b/aarch64/Machregsaux.ml index d7f10b9b..39008965 100644 --- a/aarch64/Machregsaux.ml +++ b/aarch64/Machregsaux.ml @@ -27,7 +27,7 @@ let is_scratch_register s = let name_of_register r = - try Some (Hashtbl.find register_names r) with Not_found -> None + Hashtbl.find_opt register_names r let register_by_name s = Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s) -- cgit From faa1d7fbfd7c9d5aa333d9b353a6118e105c4428 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Sat, 25 Apr 2020 16:52:33 +0200 Subject: Remove the `can_reserve_register` function. The function is in fact just a call to the function`is_callee_save_register` from `Conventions1.v`. --- aarch64/Machregsaux.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Machregsaux.ml b/aarch64/Machregsaux.ml index 39008965..7d233041 100644 --- a/aarch64/Machregsaux.ml +++ b/aarch64/Machregsaux.ml @@ -31,5 +31,3 @@ let name_of_register r = let register_by_name s = Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s) - -let can_reserve_register r = Conventions1.is_callee_save r -- cgit From ad2ea9c2e701dd82c26e6cd3e8a777be9bdef2a2 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 29 Apr 2020 15:12:54 +0200 Subject: Move shared code in new file. The name_of_register and register_of_name function are shared between all architectures and can be moved in a common file. --- aarch64/Machregsaux.ml | 17 ----------------- 1 file changed, 17 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Machregsaux.ml b/aarch64/Machregsaux.ml index 7d233041..5f3c1a8d 100644 --- a/aarch64/Machregsaux.ml +++ b/aarch64/Machregsaux.ml @@ -12,22 +12,5 @@ (** Auxiliary functions on machine registers *) -open Camlcoq -open Machregs - -let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31 - -let _ = - List.iter - (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s)) - Machregs.register_names - let is_scratch_register s = s = "X16" || s = "x16" || s = "X30" || s = "x30" - - -let name_of_register r = - Hashtbl.find_opt register_names r - -let register_by_name s = - Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s) -- cgit From 465f6b4120bb38d2ef2871de4972df92ee935ed6 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 25 Jul 2020 10:37:05 +0200 Subject: No need to process __builtin_fabs in $ARCH/Asmexpand.ml __builtin_fabs has already been expanded in backend/Selection.v . --- aarch64/Asmexpand.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index 471ad501..dcb2d1aa 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -347,8 +347,6 @@ let expand_builtin_inline name args res = | ("__builtin_clsl" | "__builtin_clsll"), [BA(IR a1)], BR(IR res) -> emit (Pcls(X, res, a1)) (* Float arithmetic *) - | "__builtin_fabs", [BA(FR a1)], BR(FR res) -> - emit (Pfabs(D, res, a1)) | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> emit (Pfsqrt(D, res, a1)) | "__builtin_fmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> -- cgit From a56e0c65b08f0f7123630f3a1b415e67ef48c38e Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 25 Jul 2020 18:27:04 +0200 Subject: AArch64 implementation of __builtin_ctz* Using the "rbit" instruction (reverse bits). --- aarch64/Asm.v | 2 ++ aarch64/Asmexpand.ml | 8 +++++++- aarch64/TargetPrinter.ml | 2 ++ 3 files changed, 11 insertions(+), 1 deletion(-) (limited to 'aarch64') diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 47cd3051..79232783 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -237,6 +237,7 @@ Inductive instruction: Type := | Pclz (sz: isize) (rd r1: ireg) (**r count leading zero bits *) | Prev (sz: isize) (rd r1: ireg) (**r reverse bytes *) | Prev16 (sz: isize) (rd r1: ireg) (**r reverse bytes in each 16-bit word *) + | Prbit (sz: isize) (rd r1: ireg) (**r reverse bits *) (** Conditional data processing *) | Pcsel (rd: ireg) (r1 r2: ireg) (c: testcond) (**r int conditional move *) | Pcset (rd: ireg) (c: testcond) (**r set to 1/0 if cond is true/false *) @@ -1107,6 +1108,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pclz _ _ _ | Prev _ _ _ | Prev16 _ _ _ + | Prbit _ _ _ | Pfsqrt _ _ _ | Pfmadd _ _ _ _ _ | Pfmsub _ _ _ _ _ diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index dcb2d1aa..02c27053 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -337,7 +337,7 @@ let expand_builtin_inline name args res = | "__builtin_bswap16", [BA(IR a1)], BR(IR res) -> emit (Prev16(W, res, a1)); emit (Pandimm(W, res, RR0 res, Z.of_uint 0xFFFF)) - (* Count leading zeros and leading sign bits *) + (* Count leading zeros, leading sign bits, trailing zeros *) | "__builtin_clz", [BA(IR a1)], BR(IR res) -> emit (Pclz(W, res, a1)) | ("__builtin_clzl" | "__builtin_clzll"), [BA(IR a1)], BR(IR res) -> @@ -346,6 +346,12 @@ let expand_builtin_inline name args res = emit (Pcls(W, res, a1)) | ("__builtin_clsl" | "__builtin_clsll"), [BA(IR a1)], BR(IR res) -> emit (Pcls(X, res, a1)) + | "__builtin_ctz", [BA(IR a1)], BR(IR res) -> + emit (Prbit(W, res, a1)); + emit (Pclz(W, res, res)) + | ("__builtin_ctzl" | "__builtin_ctzll"), [BA(IR a1)], BR(IR res) -> + emit (Prbit(X, res, a1)); + emit (Pclz(X, res, res)) (* Float arithmetic *) | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> emit (Pfsqrt(D, res, a1)) diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index e54673dd..fec05cc6 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -375,6 +375,8 @@ module Target : TARGET = fprintf oc " rev %a, %a\n" ireg (sz, rd) ireg (sz, r1) | Prev16(sz, rd, r1) -> fprintf oc " rev16 %a, %a\n" ireg (sz, rd) ireg (sz, r1) + | Prbit(sz, rd, r1) -> + fprintf oc " rbit %a, %a\n" ireg (sz, rd) ireg (sz, r1) (* Conditional data processing *) | Pcsel(rd, r1, r2, c) -> fprintf oc " csel %a, %a, %a, %s\n" xreg rd xreg r1 xreg r2 (condition_name c) -- cgit From bc20d7c0d16d07790fb6eb608bf608237b0abbc3 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sat, 25 Jul 2020 17:47:25 +0200 Subject: Move declarations of __builtin_clz* and __builtin_ctz* to C2C.ml These functions are now available on all targets. --- aarch64/CBuiltins.ml | 8 -------- 1 file changed, 8 deletions(-) (limited to 'aarch64') diff --git a/aarch64/CBuiltins.ml b/aarch64/CBuiltins.ml index dfd5b768..e2a9c87a 100644 --- a/aarch64/CBuiltins.ml +++ b/aarch64/CBuiltins.ml @@ -32,14 +32,6 @@ let builtins = { "__builtin_fence", (TVoid [], [], false); (* Integer arithmetic *) - "__builtin_bswap64", - (TInt(IULongLong, []), [TInt(IULongLong, [])], false); - "__builtin_clz", - (TInt(IInt, []), [TInt(IUInt, [])], false); - "__builtin_clzl", - (TInt(IInt, []), [TInt(IULong, [])], false); - "__builtin_clzll", - (TInt(IInt, []), [TInt(IULongLong, [])], false); "__builtin_cls", (TInt(IInt, []), [TInt(IInt, [])], false); "__builtin_clsl", -- cgit From 77ce8ba291afa9f5629a160df440f9af6614f3ef Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 27 Jul 2020 09:54:00 +0200 Subject: Add __builtin_sqrt as synonymous for __builtin_fsqrt __builtin_sqrt (no "f") is the name used by GCC and Clang. --- aarch64/Asmexpand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'aarch64') diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index 02c27053..ea2ee703 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -353,7 +353,7 @@ let expand_builtin_inline name args res = emit (Prbit(X, res, a1)); emit (Pclz(X, res, res)) (* Float arithmetic *) - | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> + | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) -> emit (Pfsqrt(D, res, a1)) | "__builtin_fmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfmadd(D, res, a1, a2, a3)) -- cgit From ab0d9476db875a82cf293623d18552b62f239d5c Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Mon, 21 Sep 2020 14:15:57 +0200 Subject: Support the use of already-installed MenhirLib and Flocq libraries configure flags -use-external-Flocq and -use external-MenhirLib. --- aarch64/Archi.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Archi.v b/aarch64/Archi.v index 24431cb2..42500e70 100644 --- a/aarch64/Archi.v +++ b/aarch64/Archi.v @@ -15,9 +15,8 @@ (** Architecture-dependent parameters for AArch64 *) +From Flocq Require Import Binary Bits. Require Import ZArith List. -(*From Flocq*) -Require Import Binary Bits. Definition ptr64 := true. -- cgit From acaabc6c481cc70e5597ccb74052a7f6d330b0f1 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 29 Oct 2020 18:10:16 +0100 Subject: Added implementation for fmin/fmax for aarch64. The two built-in function map to the fmax and fmin instruction. Bug 30035 --- aarch64/Asm.v | 4 ++++ aarch64/Asmexpand.ml | 4 ++++ aarch64/TargetPrinter.ml | 4 ++++ 3 files changed, 12 insertions(+) (limited to 'aarch64') diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 79232783..5ac577b1 100644 --- a/aarch64/Asm.v +++ b/aarch64/Asm.v @@ -283,6 +283,8 @@ Inductive instruction: Type := | Pfmsub (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = r3 - r1 * r2] *) | Pfnmadd (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = - r3 - r1 * r2] *) | Pfnmsub (sz: fsize) (rd r1 r2 r3: freg) (**r [rd = - r3 + r1 * r2] *) + | Pfmax (sz: fsize) (rd r1 r2: freg) (**r maximum *) + | Pfmin (sz: fsize) (rd r1 r2: freg) (**r minimum *) (** Floating-point comparison *) | Pfcmp (sz: fsize) (r1 r2: freg) (**r compare [r1] and [r2] *) | Pfcmp0 (sz: fsize) (r1: freg) (**r compare [r1] and [+0.0] *) @@ -1114,6 +1116,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pfmsub _ _ _ _ _ | Pfnmadd _ _ _ _ _ | Pfnmsub _ _ _ _ _ + | Pfmax _ _ _ _ + | Pfmin _ _ _ _ | Pnop | Pcfi_adjust _ | Pcfi_rel_offset _ => diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml index ea2ee703..1ba754dd 100644 --- a/aarch64/Asmexpand.ml +++ b/aarch64/Asmexpand.ml @@ -363,6 +363,10 @@ let expand_builtin_inline name args res = emit (Pfnmadd(D, res, a1, a2, a3)) | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfnmsub(D, res, a1, a2, a3)) + | "__builtin_fmax", [BA (FR a1); BA (FR a2)], BR (FR res) -> + emit (Pfmax (D, res, a1, a2)) + | "__builtin_fmin", [BA (FR a1); BA (FR a2)], BR (FR res) -> + emit (Pfmin (D, res, a1, a2)) (* Vararg *) | "__builtin_va_start", [BA(IR a)], _ -> expand_builtin_va_start a diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml index fec05cc6..78b9eb2a 100644 --- a/aarch64/TargetPrinter.ml +++ b/aarch64/TargetPrinter.ml @@ -467,6 +467,10 @@ module Target : TARGET = fprintf oc " fnmadd %a, %a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2) freg (sz, r3) | Pfnmsub(sz, rd, r1, r2, r3) -> fprintf oc " fnmsub %a, %a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2) freg (sz, r3) + | Pfmax (sz, rd, r1, r2) -> + fprintf oc " fmax %a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2) + | Pfmin (sz, rd, r1, r2) -> + fprintf oc " fmin %a, %a, %a\n" freg (sz, rd) freg (sz, r1) freg (sz, r2) (* Floating-point comparison *) | Pfcmp(sz, r1, r2) -> fprintf oc " fcmp %a, %a\n" freg (sz, r1) freg (sz, r2) -- cgit From 0df99dc46209a9fe5026b83227ef73280f0dab70 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Dec 2020 16:46:42 +0100 Subject: AArch64 modeling of registers destroyed by pseudo-instructions Pfmovimms, Pfmovimmd destroy X16 Pbtbl preserves X17 Inlined built-in functions destroy X16 and X30 --- aarch64/Asm.v | 8 ++++---- aarch64/Asmgenproof.v | 11 +++++++---- 2 files changed, 11 insertions(+), 8 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Asm.v b/aarch64/Asm.v index 5ac577b1..346cb649 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', diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index eeff1956..b60623a6 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -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]]]]. -- cgit