From fdcaf6fabd3d594e40a2b7a31341202e9a93f5cb Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 7 Mar 2012 09:22:56 +0000 Subject: PowerPC: remove the fmadd and fmsub operators/Asm instructions (definitely not semantics-preserving; hard to justify). CPragmas: make sure SDAs are not recognized on MacOSX. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1836 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/SelectOp.vp | 20 ++------------------ 1 file changed, 2 insertions(+), 18 deletions(-) (limited to 'powerpc/SelectOp.vp') diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 943c4006..d7944b6b 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -370,24 +370,8 @@ Nondetfunction shru (e1: expr) (e2: expr) := Definition negf (e: expr) := Eop Onegf (e ::: Enil). Definition absf (e: expr) := Eop Oabsf (e ::: Enil). - -Parameter use_fused_mul : unit -> bool. - -Nondetfunction addf (e1: expr) (e2: expr) := - if negb(use_fused_mul tt) then Eop Oaddf (e1:::e2:::Enil) else - match e1, e2 with - | Eop Omulf (t1:::t2:::Enil), t3 => Eop Omuladdf (t1:::t2:::t3:::Enil) - | t1, Eop Omulf (t2:::t3:::Enil) => Eop Omuladdf (t2:::t3:::t1:::Enil) - | _, _ => Eop Oaddf (e1:::e2:::Enil) - end. - -Nondetfunction subf (e1: expr) (e2: expr) := - if negb(use_fused_mul tt) then Eop Osubf (e1:::e2:::Enil) else - match e1 with - | Eop Omulf (t1:::t2:::Enil) => Eop Omulsubf (t1:::t2:::e2:::Enil) - | _ => Eop Osubf (e1:::e2:::Enil) - end. - +Definition addf (e1 e2: expr) := Eop Oaddf (e1 ::: e2 ::: Enil). +Definition subf (e1 e2: expr) := Eop Osubf (e1 ::: e2 ::: Enil). Definition mulf (e1 e2: expr) := Eop Omulf (e1 ::: e2 ::: Enil). Definition divf (e1 e2: expr) := Eop Odivf (e1 ::: e2 ::: Enil). -- cgit