From 4e3d57e84a0ebf96723fc7a6deeb9fd27f56770a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 6 Aug 2019 13:34:23 +0200 Subject: x86: wrong expansion of __builtin_fmadd et al There was a misunderstanding on the asm syntax for 3-operand instructions such as vfmadd132: when the Intel manual reads vfmadd132 res, arg2, arg3 the corresponding GNU asm syntax is vfmadd132 arg3, arg2, res but not vfmadd132 arg2, arg3, res Closes: #188 --- x86/TargetPrinter.ml | 32 +++++++++++++++++++------------- 1 file changed, 19 insertions(+), 13 deletions(-) (limited to 'x86') diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index cd54e08b..6159437e 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -399,7 +399,13 @@ module Target(System: SYSTEM):TARGET = (* Printing of instructions *) -(* Reminder on AT&T syntax: op source, dest *) +(* Reminder on X86 assembly syntaxes: + AT&T syntax Intel syntax + (used by GNU as) (used in reference manuals) + dst <- op(src) op src, dst op dst, src + dst <- op(dst, src2) op src2, dst op dst, src2 + dst <- op(dst, src2, src3) op src3, src2, dst op dst, src2, src3 +*) let print_instruction oc = function (* Moves *) @@ -752,29 +758,29 @@ module Target(System: SYSTEM):TARGET = | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz) | Pfmadd132 (res,a1,a2) -> - fprintf oc " vfmadd132sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmadd132sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfmadd213 (res,a1,a2) -> - fprintf oc " vfmadd213sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmadd213sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfmadd231 (res,a1,a2) -> - fprintf oc " vfmadd231sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmadd231sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfmsub132 (res,a1,a2) -> - fprintf oc " vfmsub132sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmsub132sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfmsub213 (res,a1,a2) -> - fprintf oc " vfmsub213sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmsub213sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfmsub231 (res,a1,a2) -> - fprintf oc " vfmsub231sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfmsub231sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmadd132 (res,a1,a2) -> - fprintf oc " vfnmadd132sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmadd132sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmadd213 (res,a1,a2) -> - fprintf oc " vfnmadd213sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmadd213sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmadd231 (res,a1,a2) -> - fprintf oc " vfnmadd231sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmadd231sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmsub132 (res,a1,a2) -> - fprintf oc " vfnmsub132sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmsub132sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmsub213 (res,a1,a2) -> - fprintf oc " vfnmsub213sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmsub213sd %a, %a, %a\n" freg a2 freg a1 freg res | Pfnmsub231 (res,a1,a2) -> - fprintf oc " vfnmsub231sd %a, %a, %a\n" freg a1 freg a2 freg res + fprintf oc " vfnmsub231sd %a, %a, %a\n" freg a2 freg a1 freg res | Pmaxsd (res,a1) -> fprintf oc " maxsd %a, %a\n" freg a1 freg res | Pminsd (res,a1) -> -- cgit From 7d5db993033ce049776fa290ae1ebc6051dea0f3 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Sat, 17 Aug 2019 10:10:42 +0200 Subject: Fix compile for architectures other than AArch64 (#192) Some changes were not correctly propagated to all architectures. --- x86/SelectOpproof.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'x86') diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index a1bb0703..961f602c 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -381,9 +381,9 @@ Proof. - TrivialExists. simpl. rewrite Int.and_commut; auto. - TrivialExists. simpl. rewrite Val.and_assoc. rewrite Int.and_commut. auto. - rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. - rewrite Int.and_commut. auto. compute; auto. + rewrite Int.and_commut. auto. omega. - rewrite Val.zero_ext_and. TrivialExists. rewrite Val.and_assoc. - rewrite Int.and_commut. auto. compute; auto. + rewrite Int.and_commut. auto. omega. - TrivialExists. Qed. @@ -743,7 +743,7 @@ Proof. red; intros until x. unfold cast8unsigned. destruct (cast8unsigned_match a); intros; InvEval. TrivialExists. subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc. - rewrite Int.and_commut. apply eval_andimm; auto. compute; auto. + rewrite Int.and_commut. apply eval_andimm; auto. omega. TrivialExists. Qed. @@ -759,7 +759,7 @@ Proof. red; intros until x. unfold cast16unsigned. destruct (cast16unsigned_match a); intros; InvEval. TrivialExists. subst. rewrite Val.zero_ext_and. rewrite Val.and_assoc. - rewrite Int.and_commut. apply eval_andimm; auto. compute; auto. + rewrite Int.and_commut. apply eval_andimm; auto. omega. TrivialExists. Qed. -- cgit