diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-07 09:22:56 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-03-07 09:22:56 +0000 |
| commit | fdcaf6fabd3d594e40a2b7a31341202e9a93f5cb (patch) | |
| tree | 807d8c24c96db39b596a7e75d746d70ba196e01f /powerpc/SelectOp.vp | |
| parent | 2f37eb9bd85b6638cce1c2e75c71cdc642acf80a (diff) | |
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
Diffstat (limited to 'powerpc/SelectOp.vp')
| -rw-r--r-- | powerpc/SelectOp.vp | 20 |
1 files changed, 2 insertions, 18 deletions
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 943c400..d7944b6 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). |