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. --- powerpc/Machregsaux.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml index 664f71a0..711eb623 100644 --- a/powerpc/Machregsaux.ml +++ b/powerpc/Machregsaux.ml @@ -25,7 +25,7 @@ let _ = let is_scratch_register s = s = "R0" || s = "r0" 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`. --- powerpc/Machregsaux.ml | 4 ---- powerpc/Machregsaux.mli | 1 - 2 files changed, 5 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml index 711eb623..40c993fd 100644 --- a/powerpc/Machregsaux.ml +++ b/powerpc/Machregsaux.ml @@ -29,7 +29,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 = - List.mem r Conventions1.int_callee_save_regs - || List.mem r Conventions1.float_callee_save_regs diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli index 9404568d..884100bb 100644 --- a/powerpc/Machregsaux.mli +++ b/powerpc/Machregsaux.mli @@ -15,4 +15,3 @@ val name_of_register: Machregs.mreg -> string option val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool -val can_reserve_register: Machregs.mreg -> bool -- 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. --- powerpc/Machregsaux.ml | 16 ---------------- powerpc/Machregsaux.mli | 2 -- 2 files changed, 18 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml index 40c993fd..9d3a2243 100644 --- a/powerpc/Machregsaux.ml +++ b/powerpc/Machregsaux.ml @@ -12,20 +12,4 @@ (** 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 = "R0" || s = "r0" - -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) diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli index 884100bb..f3d52849 100644 --- a/powerpc/Machregsaux.mli +++ b/powerpc/Machregsaux.mli @@ -12,6 +12,4 @@ (** Auxiliary functions on machine registers *) -val name_of_register: Machregs.mreg -> string option -val register_by_name: string -> Machregs.mreg option val is_scratch_register: string -> bool -- cgit From c94405f67ca18be997974f88ff91c072d8a5c0cb Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 1 Jul 2020 14:13:25 +0200 Subject: Fix typo in name of builtin function. --- powerpc/Machregs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index e7c8758b..07622a0e 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -232,7 +232,7 @@ Definition mregs_for_builtin (ef: external_function): list (option mreg) * list | EF_builtin id sg => if string_dec id "__builtin_atomic_exchange" then ((Some R3)::(Some R4)::(Some R5)::nil,nil) else if string_dec id "__builtin_sync_fetch_and_add" then ((Some R4)::(Some R5)::nil,(Some R3)::nil) - else if string_dec id "___builtin_atomic_compare_exchange" then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil) + else if string_dec id "__builtin_atomic_compare_exchange" then ((Some R4)::(Some R5)::(Some R6)::nil, (Some R3):: nil) else (nil, nil) | _ => (nil, nil) end. -- cgit From bb9fa5550d6145344c4ed296ed980cb419e4cb27 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 1 Jul 2020 15:16:55 +0200 Subject: Added asserts for constraints of PowerPC builtins --- powerpc/Asmexpand.ml | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'powerpc') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index ce88778c..1854ec16 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -767,6 +767,8 @@ let expand_builtin_inline name args res = emit (Pori (GPR0, GPR0, Cint _0)) (* atomic operations *) | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ -> + (* Register constraints imposed by Machregs.v *) + assert(a1 = GPR3 && a2 = GPR4 && a3 = GPR5); emit (Plwz (GPR10,Cint _0,a2)); emit (Psync); let lbl = new_label() in @@ -786,6 +788,8 @@ let expand_builtin_inline name args res = emit (Pisync); emit (Pstw (GPR0,Cint _0, a2)) | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) -> + (* Register constraints imposed by Machregs.v *) + assert (a1 = GPR4 && a2 = GPR5 && res = GPR3); let lbl = new_label() in emit (Psync); emit (Plabel lbl); @@ -795,6 +799,8 @@ let expand_builtin_inline name args res = emit (Pbf (CRbit_2, lbl)); emit (Pisync); | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) -> + (* Register constraints imposed by Machregs.v *) + assert (dst = GPR4 && exp = GPR5 && des = GPR6 && res = GPR3); let lbls = new_label () and lblneq = new_label () and lblsucc = new_label () in -- 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 . --- powerpc/Asmexpand.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 1854ec16..9b7c3cc7 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -594,8 +594,6 @@ let expand_builtin_inline name args res = emit (Pfnmadd(res, a1, a2, a3)) | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfnmsub(res, a1, a2, a3)) - | "__builtin_fabs", [BA(FR a1)], BR(FR res) -> - emit (Pfabs(res, a1)) | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> emit (Pfsqrt(res, a1)) | "__builtin_frsqrte", [BA(FR a1)], BR(FR res) -> -- 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. --- powerpc/CBuiltins.ml | 12 ------------ 1 file changed, 12 deletions(-) (limited to 'powerpc') diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index e29a41f1..e0826877 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -28,18 +28,6 @@ let builtins = { (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); "__builtin_mulhwu", (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); - "__builtin_clz", - (TInt(IInt, []), [TInt(IUInt, [])], false); - "__builtin_clzl", - (TInt(IInt, []), [TInt(IULong, [])], false); - "__builtin_clzll", - (TInt(IInt, []), [TInt(IULongLong, [])], false); - "__builtin_ctz", - (TInt(IInt, []), [TInt(IUInt, [])], false); - "__builtin_ctzl", - (TInt(IInt, []), [TInt(IULong, [])], false); - "__builtin_ctzll", - (TInt(IInt, []), [TInt(IULongLong, [])], false); "__builtin_cmpb", (TInt (IUInt, []), [TInt(IUInt, []);TInt(IUInt, [])], false); (* Integer arithmetic in 32/64-bit hybrid mode *) -- 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. --- powerpc/Asmexpand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 9b7c3cc7..d8cbd94e 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -594,7 +594,7 @@ let expand_builtin_inline name args res = emit (Pfnmadd(res, a1, a2, a3)) | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) -> emit (Pfnmsub(res, a1, a2, a3)) - | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) -> + | ("__builtin_fsqrt" | "__builtin_sqrt"), [BA(FR a1)], BR(FR res) -> emit (Pfsqrt(res, a1)) | "__builtin_frsqrte", [BA(FR a1)], BR(FR res) -> emit (Pfrsqrte(res, a1)) -- 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. --- powerpc/Archi.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 10f38391..ae10c54c 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -16,9 +16,8 @@ (** Architecture-dependent parameters for PowerPC *) +From Flocq Require Import Binary Bits. Require Import ZArith List. -(*From Flocq*) -Require Import Binary Bits. Definition ptr64 := false. -- cgit From 4011a085abee25df19c6e7659f2168ef17c7c344 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 29 Oct 2020 18:16:17 +0100 Subject: Added missing printer for PowerPC 64 bit comparison. These comparisons are supported in the hybrid 64 bit mode. Bug 30035 --- powerpc/PrintOp.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'powerpc') diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml index 8d7f17ab..77791827 100644 --- a/powerpc/PrintOp.ml +++ b/powerpc/PrintOp.ml @@ -42,6 +42,14 @@ let print_condition reg pp = function fprintf pp "%a & 0x%lx == 0" reg r1 (camlint_of_coqint n) | (Cmasknotzero n, [r1]) -> fprintf pp "%a & 0x%lx != 0" reg r1 (camlint_of_coqint n) + | (Ccompl c, [r1;r2]) -> + fprintf pp "%a %sls %a" reg r1 (comparison_name c) reg r2 + | (Ccomplu c, [r1;r2]) -> + fprintf pp "%a %slu %a" reg r1 (comparison_name c) reg r2 + | (Ccomplimm(c, n), [r1]) -> + fprintf pp "%a %sls %Ld" reg r1 (comparison_name c) (camlint64_of_coqint n) + | (Ccompluimm(c, n), [r1]) -> + fprintf pp "%a %slu %Ld" reg r1 (comparison_name c) (camlint64_of_coqint n) | _ -> fprintf pp "" -- cgit From 0aeff47ea220a16fec90bcad05e4b79b838a69c9 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 29 Oct 2020 18:16:59 +0100 Subject: Added semantics for the PowerPC sel and mulh built-ins The semantics of the various selection functions are defined analogously to the ones from the type generic sel function. The semantics for the various high word multiplication functions is defined using the Integer functions. Bug 30035 --- powerpc/Builtins1.v | 48 ++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 44 insertions(+), 4 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Builtins1.v b/powerpc/Builtins1.v index 53c83d7e..9d7aadd9 100644 --- a/powerpc/Builtins1.v +++ b/powerpc/Builtins1.v @@ -19,15 +19,55 @@ Require Import String Coqlib. Require Import AST Integers Floats Values. Require Import Builtins0. -Inductive platform_builtin : Type := . +Inductive platform_builtin : Type := + | BI_isel + | BI_uisel + | BI_isel64 + | BI_uisel64 + | BI_bsel + | BI_mulhw + | BI_mulhwu + | BI_mulhd + | BI_mulhdu. Local Open Scope string_scope. Definition platform_builtin_table : list (string * platform_builtin) := - nil. + ("__builtin_isel", BI_isel) + :: ("__builtin_uisel", BI_uisel) + :: ("__builtin_isel64", BI_isel64) + :: ("__builtin_uisel64", BI_uisel64) + :: ("__builtin_bsel", BI_bsel) + :: ("__builtin_mulhw", BI_mulhw) + :: ("__builtin_mulhwu", BI_mulhwu) + :: ("__builtin_mulhd", BI_mulhd) + :: ("__builtin_mulhdu", BI_mulhdu) + :: nil. Definition platform_builtin_sig (b: platform_builtin) : signature := - match b with end. + match b with + | BI_isel | BI_uisel | BI_bsel => + mksignature (Tint :: Tint :: Tint :: nil) Tint cc_default + | BI_isel64 | BI_uisel64 => + mksignature (Tint :: Tlong :: Tlong :: nil) Tlong cc_default + | BI_mulhw | BI_mulhwu => + mksignature (Tint :: Tint :: nil) Tint cc_default + | BI_mulhd | BI_mulhdu => + mksignature (Tlong :: Tlong :: nil) Tlong cc_default + end. Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) := - match b with end. + match b with + | BI_isel | BI_uisel | BI_bsel => + mkbuiltin_n3t Tint Tint Tint Tint (fun c n1 n2 => if Int.eq c Int.zero then n2 else n1) + | BI_isel64 | BI_uisel64 => + mkbuiltin_n3t Tint Tlong Tlong Tlong (fun c n1 n2 => if Int.eq c Int.zero then n2 else n1) + | BI_mulhw => + mkbuiltin_n2t Tint Tint Tint Int.mulhs + | BI_mulhwu => + mkbuiltin_n2t Tint Tint Tint Int.mulhu + | BI_mulhd => + mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhs + | BI_mulhdu => + mkbuiltin_n2t Tlong Tlong Tlong Int64.mulhu + end. -- cgit From ef5477a47b49c405744319fbdef0a689b1bf03d4 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Dec 2020 10:30:51 +0100 Subject: Remove Pfcfi, Pfcfiu, Pfctiu pseudoinstructions Also remove the Ofloatofint, Ofloatofintu, and Ointuoffloat PowerPC operations. The pseudoinstructions were used to implement these operations, as follows: Pfcfi : Ofloatofint i.e. the conversion signed int32 -> float64 Pfcfiu : Ofloatofintu i.e. the conversion unsigned int32 -> float64 Pfctiu : Ointuoffloat i.e. the conversion float64 -> unsigned int32 These pseudoinstructions were expanded (in Asmexpand.ml) in terms of Pfcfid : signed int64 -> float64 Pfctidz : float64 -> signed int64 and int32/int64 conversions. This commit performs this expansion during instruction selection (SelectOp.vp): floatofint(n) becomes floatoflong(longofint(n)) floatofintu(n) becomes floatoflong(longuofint(n)) intuoffloat(n) becomes cast32unsigned(longoffloat(n)) Then there is no need for the 3 removed operations and the 3 removed pseudoinstructions. More importantly, the correctness of these expansions is now proved as part of instruction selection, using the corresponding results from Floats.v. --- powerpc/Asm.v | 9 --------- powerpc/AsmToJSON.ml | 3 --- powerpc/Asmexpand.ml | 26 -------------------------- powerpc/Asmgen.v | 9 --------- powerpc/Asmgenproof1.v | 12 ------------ powerpc/Machregs.v | 2 +- powerpc/NeedOp.v | 2 +- powerpc/Op.v | 18 +----------------- powerpc/SelectOp.vp | 8 +++++--- powerpc/SelectOpproof.v | 24 +++++++++++++++--------- powerpc/TargetPrinter.ml | 6 ------ powerpc/ValueAOp.v | 3 --- 12 files changed, 23 insertions(+), 99 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 4fb38ff8..6ec20d62 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -200,12 +200,9 @@ Inductive instruction : Type := | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) | Pfadds: freg -> freg -> freg -> instruction (**r float addition *) | Pfcmpu: freg -> freg -> instruction (**r float comparison *) - | Pfcfi: freg -> ireg -> instruction (**r signed-int-to-float conversion (pseudo, PPC64) *) | Pfcfl: freg -> ireg -> instruction (**r signed-long-to-float conversion (pseudo, PPC64) *) - | Pfcfiu: freg -> ireg -> instruction (**r unsigned-int-to-float conversion (pseudo, PPC64) *) | Pfcfid: freg -> freg -> instruction (**r signed-long-to-float conversion (PPC64) *) | Pfcti: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo) *) - | Pfctiu: ireg -> freg -> instruction (**r float-to-unsigned-int conversion, round towards 0 (pseudo, PPC64) *) | Pfctid: ireg -> freg -> instruction (**r float-to-signed-int conversion, round towards 0 (pseudo, PPC64) *) | Pfctidz: freg -> freg -> instruction (**r float-to-signed-long conversion, round towards 0 (PPC64) *) | Pfctiw: freg -> freg -> instruction (**r float-to-signed-int conversion, round by default *) @@ -825,16 +822,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out Next (nextinstr (rs#rd <- (Val.addfs rs#r1 rs#r2))) m | Pfcmpu r1 r2 => Next (nextinstr (compare_float rs rs#r1 rs#r2)) m - | Pfcfi rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofint rs#r1)))) m | Pfcfl rd r1 => Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatoflong rs#r1)))) m - | Pfcfiu rd r1 => - Next (nextinstr (rs#rd <- (Val.maketotal (Val.floatofintu rs#r1)))) m | Pfcti rd r1 => Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m - | Pfctiu rd r1 => - Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intuoffloat rs#r1)))) m | Pfctid rd r1 => Next (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.longoffloat rs#r1)))) m | Pfdiv rd r1 r2 => diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index f4d4285a..09cfc28d 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -198,12 +198,9 @@ let pp_instructions pp ic = | Pfadd (fr1,fr2,fr3) -> instruction pp "Pfadd" [Freg fr1; Freg fr2; Freg fr3] | Pfadds (fr1,fr2,fr3) -> instruction pp "Pfadds" [Freg fr1; Freg fr2; Freg fr3] | Pfcmpu (fr1,fr2) -> instruction pp "Pfcmpu" [Freg fr1; Freg fr2] - | Pfcfi (ir,fr) | Pfcfl (ir,fr) -> assert false (* Should not occur *) | Pfcfid (fr1,fr2) -> instruction pp "Pfcfid" [Freg fr1; Freg fr2] - | Pfcfiu _ (* Should not occur *) | Pfcti _ (* Should not occur *) - | Pfctiu _ (* Should not occur *) | Pfctid _ -> assert false (* Should not occur *) | Pfctidz (fr1,fr2) -> instruction pp "Pfctidz" [Freg fr1; Freg fr2] | Pfctiw (fr1,fr2) -> instruction pp "Pfctiw" [Freg fr1; Freg fr2] diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index d8cbd94e..cb6a659f 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -875,15 +875,6 @@ let expand_instruction instr = emit (Paddi(GPR1, GPR1, Cint(coqint_of_camlint sz))) else emit (Plwz(GPR1, Cint ofs, GPR1)) - | Pfcfi(r1, r2) -> - assert (Archi.ppc64); - emit (Pextsw(GPR0, r2)); - emit (Pstdu(GPR0, Cint _m8, GPR1)); - emit (Pcfi_adjust _8); - emit (Plfd(r1, Cint _0, GPR1)); - emit (Pfcfid(r1, r1)); - emit (Paddi(GPR1, GPR1, Cint _8)); - emit (Pcfi_adjust _m8) | Pfcfl(r1, r2) -> assert (Archi.ppc64); emit (Pstdu(r2, Cint _m8, GPR1)); @@ -892,15 +883,6 @@ let expand_instruction instr = emit (Pfcfid(r1, r1)); emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) - | Pfcfiu(r1, r2) -> - assert (Archi.ppc64); - emit (Prldicl(GPR0, r2, _0, _32)); - emit (Pstdu(GPR0, Cint _m8, GPR1)); - emit (Pcfi_adjust _8); - emit (Plfd(r1, Cint _0, GPR1)); - emit (Pfcfid(r1, r1)); - emit (Paddi(GPR1, GPR1, Cint _8)); - emit (Pcfi_adjust _m8) | Pfcti(r1, r2) -> emit (Pfctiwz(FPR13, r2)); emit (Pstfdu(FPR13, Cint _m8, GPR1)); @@ -908,14 +890,6 @@ let expand_instruction instr = emit (Plwz(r1, Cint _4, GPR1)); emit (Paddi(GPR1, GPR1, Cint _8)); emit (Pcfi_adjust _m8) - | Pfctiu(r1, r2) -> - assert (Archi.ppc64); - emit (Pfctidz(FPR13, r2)); - emit (Pstfdu(FPR13, Cint _m8, GPR1)); - emit (Pcfi_adjust _8); - emit (Plwz(r1, Cint _4, GPR1)); - emit (Paddi(GPR1, GPR1, Cint _8)); - emit (Pcfi_adjust _m8) | Pfctid(r1, r2) -> assert (Archi.ppc64); emit (Pfctidz(FPR13, r2)); diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index a686414a..1dca4ba4 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -611,15 +611,6 @@ Definition transl_op | Ointoffloat, a1 :: nil => do r1 <- freg_of a1; do r <- ireg_of res; OK (Pfcti r r1 :: k) - | Ointuoffloat, a1 :: nil => - do r1 <- freg_of a1; do r <- ireg_of res; - OK (Pfctiu r r1 :: k) - | Ofloatofint, a1 :: nil => - do r1 <- ireg_of a1; do r <- freg_of res; - OK (Pfcfi r r1 :: k) - | Ofloatofintu, a1 :: nil => - do r1 <- ireg_of a1; do r <- freg_of res; - OK (Pfcfiu r r1 :: k) | Ofloatofwords, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res; OK (Pfmake r r1 r2 :: k) diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 20cf9c1d..0442f7e8 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -1498,18 +1498,6 @@ Opaque Val.add. rewrite H1; auto. (* Ointoffloat *) - replace v with (Val.maketotal (Val.intoffloat (rs x))). - TranslOpSimpl. - rewrite H1; auto. - (* Ointuoffloat *) -- replace v with (Val.maketotal (Val.intuoffloat (rs x))). - TranslOpSimpl. - rewrite H1; auto. - (* Ofloatofint *) -- replace v with (Val.maketotal (Val.floatofint (rs x))). - TranslOpSimpl. - rewrite H1; auto. - (* Ofloatofintu *) -- replace v with (Val.maketotal (Val.floatofintu (rs x))). TranslOpSimpl. rewrite H1; auto. (* Ocmp *) diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 07622a0e..9967bbae 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -166,7 +166,7 @@ Definition destroyed_by_op (op: operation): list mreg := | Ofloatconst _ => R12 :: nil | Osingleconst _ => R12 :: nil | Olongconst _ => R12 :: nil - | Ointoffloat | Ointuoffloat => F13 :: nil + | Ointoffloat => F13 :: nil | Olongoffloat => F13 :: nil | Oaddlimm _ => R12 :: nil | Oandlimm _ => R12 :: nil diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index 5ea09bd8..74ee6b85 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -61,7 +61,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Onegfs | Oabsfs => op1 (default nv) | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) | Osingleoffloat | Ofloatofsingle => op1 (default nv) - | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv) + | Ointoffloat => op1 (default nv) | Ofloatofwords | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocmp c => needs_of_condition c diff --git a/powerpc/Op.v b/powerpc/Op.v index 0f082c1f..a96a0439 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -105,7 +105,7 @@ Inductive operation : Type := | Osubl: operation (**r [rd = r1 - r2] *) | Onegl: operation (**r [rd = - r1] *) | Omull: operation (**r [rd = r1 * r2] *) - | Omullhs: operation (**r [rd = high part of r1 * r2, signed] *) + | Omullhs: operation (**r [rd = high part of r1 * r2, signed] *) | Omullhu: operation (**r [rd = high part of r1 * r2, unsigned] *) | Odivl: operation (**r [rd = r1 / r2] (signed) *) | Odivlu: operation (**r [rd = r1 / r2] (unsigned) *) @@ -141,9 +141,6 @@ Inductive operation : Type := | Ofloatofsingle: operation (**r [rd] is [r1] extended to double-precision float *) (*c Conversions between int and float: *) | Ointoffloat: operation (**r [rd = signed_int_of_float(r1)] *) - | Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] (PPC64 only) *) - | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] (PPC64 only) *) - | Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] (PPC64 only *) | Ofloatofwords: operation (**r [rd = float_of_words(r1,r2)] *) (*c Manipulating 64-bit integers: *) | Omakelong: operation (**r [rd = r1 << 32 | r2] *) @@ -299,9 +296,6 @@ Definition eval_operation | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1) | Ofloatofsingle, v1::nil => Some(Val.floatofsingle v1) | Ointoffloat, v1::nil => Val.intoffloat v1 - | Ointuoffloat, v1::nil => Val.intuoffloat v1 - | Ofloatofint, v1::nil => Val.floatofint v1 - | Ofloatofintu, v1::nil => Val.floatofintu v1 | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2) | Omakelong, v1::v2::nil => Some(Val.longofwords v1 v2) | Olowlong, v1::nil => Some(Val.loword v1) @@ -449,9 +443,6 @@ Definition type_of_operation (op: operation) : list typ * typ := | Osingleoffloat => (Tfloat :: nil, Tsingle) | Ofloatofsingle => (Tsingle :: nil, Tfloat) | Ointoffloat => (Tfloat :: nil, Tint) - | Ointuoffloat => (Tfloat :: nil, Tint) - | Ofloatofint => (Tint :: nil, Tfloat) - | Ofloatofintu => (Tint :: nil, Tfloat) | Ofloatofwords => (Tint :: Tint :: nil, Tfloat) | Omakelong => (Tint :: Tint :: nil, Tlong) | Olowlong => (Tlong :: nil, Tint) @@ -570,9 +561,6 @@ Proof with (try exact I; try reflexivity). destruct v0... destruct v0... destruct v0; simpl in H0; inv H0. destruct (Float.to_int f); inv H2... - destruct v0; simpl in H0; inv H0. destruct (Float.to_intu f); inv H2... - destruct v0; simpl in H0; inv H0... - destruct v0; simpl in H0; inv H0... destruct v0; destruct v1... destruct v0; destruct v1... destruct v0... @@ -999,10 +987,6 @@ Proof. inv H4; simpl; auto. inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_int f0); simpl in H2; inv H2. exists (Vint i); auto. - inv H4; simpl in H1; inv H1. simpl. destruct (Float.to_intu f0); simpl in H2; inv H2. - exists (Vint i); auto. - inv H4; simpl in H1; inv H1; simpl. TrivialExists. - inv H4; simpl in H1; inv H1; simpl. TrivialExists. inv H4; inv H2; simpl; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index ba6612e8..cd9a65df 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -468,7 +468,7 @@ Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil). Definition intuoffloat (e: expr) := if Archi.ppc64 then - Eop Ointuoffloat (e ::: Enil) + Eop Olowlong (Eop Olongoffloat (e ::: Enil) ::: Enil) else Elet e (Elet (Eop (Ofloatconst (Float.of_intu Float.ox8000_0000)) Enil) @@ -482,7 +482,8 @@ Nondetfunction floatofintu (e: expr) := Eop (Ofloatconst (Float.of_intu n)) Enil | _ => if Archi.ppc64 then - Eop Ofloatofintu (e ::: Enil) else + Eop Ofloatoflong (Eop Ocast32unsigned (e ::: Enil) ::: Enil) + else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil) end. @@ -493,7 +494,8 @@ Nondetfunction floatofint (e: expr) := Eop (Ofloatconst (Float.of_int n)) Enil | _ => if Archi.ppc64 then - Eop Ofloatofint (e ::: Enil) else + Eop Ofloatoflong (Eop Ocast32signed (e ::: Enil) ::: Enil) + else subf (Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: addimm Float.ox8000_0000 e ::: Enil)) (Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil) diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index c3eda068..7b34ea89 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -851,8 +851,13 @@ Proof. destruct (Float.to_intu f) as [n|] eqn:?; simpl in H0; inv H0. exists (Vint n); split; auto. unfold intuoffloat. destruct Archi.ppc64. - econstructor. constructor; eauto. constructor. simpl; rewrite Heqo; auto. - set (im := Int.repr Int.half_modulus). +- apply Float.to_intu_to_long in Heqo. + econstructor. constructor. econstructor. econstructor; eauto. constructor. + simpl; rewrite Heqo; simpl; eauto. constructor. + simpl. unfold Int64.loword. rewrite Int64.unsigned_repr, Int.repr_unsigned. auto. + assert (Int.modulus < Int64.max_unsigned) by (compute; auto). + generalize (Int.unsigned_range n). omega. +- set (im := Int.repr Int.half_modulus). set (fm := Float.of_intu im). assert (eval_expr ge sp e m (Vfloat fm :: Vfloat f :: le) (Eletvar (S O)) (Vfloat f)). constructor. auto. @@ -889,11 +894,12 @@ Theorem eval_floatofint: Proof. intros until y. unfold floatofint. destruct (floatofint_match a); intros. InvEval. TrivialExists. - destruct Archi.ppc64. - TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. exists (Vfloat (Float.of_int i)); split; auto. - set (t1 := addimm Float.ox8000_0000 a). + destruct Archi.ppc64. +- rewrite Float.of_int_of_long. + EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto. +- set (t1 := addimm Float.ox8000_0000 a). set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: t1 ::: Enil)). set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Float.ox8000_0000)) Enil). exploit (eval_addimm Float.ox8000_0000 le a). eauto. fold t1. @@ -913,12 +919,12 @@ Theorem eval_floatofintu: Proof. intros until y. unfold floatofintu. destruct (floatofintu_match a); intros. InvEval. TrivialExists. - destruct Archi.ppc64. - TrivialExists. rename e0 into a. destruct x; simpl in H0; inv H0. exists (Vfloat (Float.of_intu i)); split; auto. - unfold floatofintu. - set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)). + destruct Archi.ppc64. +- rewrite Float.of_intu_of_long. + EvalOp. constructor. EvalOp. simpl; eauto. constructor. auto. +- set (t2 := Eop Ofloatofwords (Eop (Ointconst Float.ox4330_0000) Enil ::: a ::: Enil)). set (t3 := Eop (Ofloatconst (Float.from_words Float.ox4330_0000 Int.zero)) Enil). exploit (eval_subf le t2). unfold t2. EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 0f608d25..43d2447d 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -553,22 +553,16 @@ module Target (System : SYSTEM):TARGET = fprintf oc " fadds %a, %a, %a\n" freg r1 freg r2 freg r3 | Pfcmpu(r1, r2) -> fprintf oc " fcmpu %a, %a, %a\n" creg 0 freg r1 freg r2 - | Pfcfi(r1, r2) -> - assert false | Pfcfl(r1, r2) -> assert false | Pfcfid(r1, r2) -> fprintf oc " fcfid %a, %a\n" freg r1 freg r2 - | Pfcfiu(r1, r2) -> - assert false | Pfcti(r1, r2) -> assert false | Pfctid(r1, r2) -> assert false | Pfctidz(r1, r2) -> fprintf oc " fctidz %a, %a\n" freg r1 freg r2 - | Pfctiu(r1, r2) -> - assert false | Pfctiw(r1, r2) -> fprintf oc " fctiw %a, %a\n" freg r1 freg r2 | Pfctiwz(r1, r2) -> diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index a270d857..c81f1a6c 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -133,9 +133,6 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Osingleoffloat, v1::nil => singleoffloat v1 | Ofloatofsingle, v1::nil => floatofsingle v1 | Ointoffloat, v1::nil => intoffloat v1 - | Ointuoffloat, v1::nil => intuoffloat v1 - | Ofloatofint, v1::nil => floatofint v1 - | Ofloatofintu, v1::nil => floatofintu v1 | Ofloatofwords, v1::v2::nil => floatofwords v1 v2 | Omakelong, v1::v2::nil => longofwords v1 v2 | Olowlong, v1::nil => loword v1 -- cgit From 5e3898945c063801d4a93f44182d160ccfe4badc Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 6 Dec 2020 16:47:19 +0100 Subject: PowerPC modeling of registers destroyed by pseudo-instructions Inlined built-in functions destroy GPR0 --- powerpc/Asm.v | 2 +- powerpc/Asmgenproof.v | 8 +++++--- 2 files changed, 6 insertions(+), 4 deletions(-) (limited to 'powerpc') diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 6ec20d62..d9901960 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -1195,7 +1195,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 GPR0 :: 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/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index d653633c..a1ae5855 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -781,16 +781,18 @@ Opaque loadind. 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. simpl. rewrite undef_regs_other_2. + rewrite Pregmap.gso by auto with asmgen. rewrite <- H1. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. rewrite preg_notin_charact. intros. auto with asmgen. auto with asmgen. apply agree_nextinstr. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. + eapply agree_undef_regs; eauto. + intros. simpl. rewrite undef_regs_other_2; auto. apply Pregmap.gso. auto with asmgen. congruence. intros. Simpl. rewrite set_res_other by auto. - rewrite undef_regs_other_2; auto with asmgen. + simpl. rewrite undef_regs_other_2; auto with asmgen. - (* Mgoto *) assert (f0 = f) by congruence. subst f0. -- cgit