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

15 files changed, 27 insertions, 67 deletions

diff --git a/Changelog b/Changelog
index 87220ca..2b2e701 100644
--- a/Changelog
+++ b/Changelog
@@ -10,6 +10,8 @@ Improvements in confidence:
   parameters, and other instances of using composites as r-values, with
   the exception of returning composites by value from a function.
   (The latter remains emulated, using the -fstruct-return option.)
+- PowerPC: removed the -fmadd option, not semantically-preserving
+  in the strict sense.
 
 Language features:
 - Support for _Bool type from ISO C99.
@@ -34,6 +36,7 @@ Performance improvements:
 Other improvements:
 - PowerPC/EABI: uninitialized global variables now go in common (bss) section.
 - PowerPC: work around limited excursion of conditional branch instructions.
+- PowerPC: added __builtin_fnmadd() and __builtin_fnmsub().
 - Reference interpreter: better printing of pointer values and locations.
 - Added command-line options -Wp,<opt> -Wa,<opt> -Wl,<opt> to pass
   specific options to the preprocessor, assembler, or linker, respectively.
diff --git a/cfrontend/CPragmas.ml b/cfrontend/CPragmas.ml
index 6fa6d5c..4b4c0f1 100644
--- a/cfrontend/CPragmas.ml
+++ b/cfrontend/CPragmas.ml
@@ -21,13 +21,19 @@ open Cparser
 
 (* #pragma section *)
 
+let sda_supported =
+  match Configuration.arch, Configuration.system with
+  | "powerpc", "linux" -> true
+  | "powerpc", "diab"  -> true
+  | _, _ -> false
+
 let process_section_pragma classname istring ustring addrmode accmode =
   Sections.define_section classname
     ?iname: (if istring = "" then None else Some istring)
     ?uname: (if ustring = "" then None else Some ustring)
     ?writable: (if accmode = "" then None else Some(String.contains accmode 'W'))
     ?executable: (if accmode = "" then None else Some(String.contains accmode 'X'))
-    ?near: (if addrmode = "" then None else Some(addrmode = "near-data"))
+    ?near: (if addrmode = "" then None else Some(sda_supported && addrmode = "near-data"))
     ()
 
 (* #pragma use_section *)
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 2eb4147..8feac7a 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -22,7 +22,6 @@ let option_fstruct_return = ref false
 let option_fbitfields = ref false
 let option_fvararg_calls = ref true
 let option_fpacked_structs = ref false
-let option_fmadd = ref false
 let option_fsse = ref true
 let option_dparse = ref false
 let option_dcmedium = ref false
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 443dbac..1ca915c 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -343,7 +343,6 @@ Language support options (use -fno-<opt> to turn off -f<opt>) :
   -fall          Activate all language support options above
   -fnone         Turn off all language support options above
 Code generation options: (use -fno-<opt> to turn off -f<opt>) :
-  -fmadd         (PowerPC) Use fused multiply-add and multiply-sub instructions [off]
   -fsse          (IA32) Use SSE2 instructions for some integer operations [on]
   -fsmall-data <n>  Set maximal size <n> for allocation in small data area
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
@@ -446,7 +445,6 @@ let cmdline_actions =
   @ f_opt "struct-return" option_fstruct_return
   @ f_opt "bitfields" option_fbitfields
   @ f_opt "vararg-calls" option_fvararg_calls
-  @ f_opt "madd" option_fmadd
   @ f_opt "packed-structs" option_fpacked_structs
   @ f_opt "sse" option_fsse
 
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 2d71ca9..ea5e416 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -162,10 +162,8 @@ Inductive instruction : Type :=
   | Pfcmpu: freg -> freg -> instruction                       (**r float comparison *)
   | Pfcti: ireg -> freg -> instruction                        (**r float-to-signed-int conversion *)
   | Pfdiv: freg -> freg -> freg -> instruction                (**r float division *)
-  | Pfmadd: freg -> freg -> freg -> freg -> instruction       (**r float multiply-add *)
   | Pfmake: freg -> ireg -> ireg -> instruction               (**r build a float from 2 ints *)
   | Pfmr: freg -> freg -> instruction                         (**r float move *)
-  | Pfmsub: freg -> freg -> freg -> freg -> instruction       (**r float multiply-sub *)
   | Pfmul: freg -> freg -> freg -> instruction                (**r float multiply *)
   | Pfneg: freg -> freg -> instruction                        (**r float negation *)
   | Pfrsp: freg -> freg -> instruction                        (**r float round to single precision *)
@@ -632,14 +630,10 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
       OK (nextinstr (rs#FPR13 <- Vundef #rd <- (Val.maketotal (Val.intoffloat rs#r1)))) m
   | Pfdiv rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.divf rs#r1 rs#r2))) m
-  | Pfmadd rd r1 r2 r3 =>
-      OK (nextinstr (rs#rd <- (Val.addf (Val.mulf rs#r1 rs#r2) rs#r3))) m
   | Pfmake rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.floatofwords rs#r1 rs#r2))) m
   | Pfmr rd r1 =>
       OK (nextinstr (rs#rd <- (rs#r1))) m
-  | Pfmsub rd r1 r2 r3 =>
-      OK (nextinstr (rs#rd <- (Val.subf (Val.mulf rs#r1 rs#r2) rs#r3))) m
   | Pfmul rd r1 r2 =>
       OK (nextinstr (rs#rd <- (Val.mulf rs#r1 rs#r2))) m
   | Pfneg rd r1 =>
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index b166d34..f9e4b2c 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -394,10 +394,6 @@ Definition transl_op
       Pfmul (freg_of r) (freg_of a1) (freg_of a2) :: k
   | Odivf, a1 :: a2 :: nil =>
       Pfdiv (freg_of r) (freg_of a1) (freg_of a2) :: k
-  | Omuladdf, a1 :: a2 :: a3 :: nil =>
-      Pfmadd (freg_of r) (freg_of a1) (freg_of a2) (freg_of a3) :: k
-  | Omulsubf, a1 :: a2 :: a3 :: nil =>
-      Pfmsub (freg_of r) (freg_of a1) (freg_of a2) (freg_of a3) :: k
   | Osingleoffloat, a1 :: nil =>
       Pfrsp (freg_of r) (freg_of a1) :: k
   | Ointoffloat, a1 :: nil =>
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 076288e..50b9be1 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -39,6 +39,14 @@ let builtins = {
       (TFloat(FDouble, []), 
        [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
        false);
+    "__builtin_fnmadd",
+      (TFloat(FDouble, []), 
+       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
+       false);
+    "__builtin_fnmsub",
+      (TFloat(FDouble, []), 
+       [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])],
+       false);
     "__builtin_fsqrt",
       (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
     "__builtin_frsqrte",
diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp
index cb958d4..3298671 100644
--- a/powerpc/ConstpropOp.vp
+++ b/powerpc/ConstpropOp.vp
@@ -117,8 +117,6 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
   | Osubf, F n1 :: F n2 :: nil => F(Float.sub n1 n2)
   | Omulf, F n1 :: F n2 :: nil => F(Float.mul n1 n2)
   | Odivf, F n1 :: F n2 :: nil => F(Float.div n1 n2)
-  | Omuladdf, F n1 :: F n2 :: F n3 :: nil => F(Float.add (Float.mul n1 n2) n3)
-  | Omulsubf, F n1 :: F n2 :: F n3 :: nil => F(Float.sub (Float.mul n1 n2) n3)
   | Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
   | Ointoffloat, F n1 :: nil => eval_static_intoffloat n1
   | Ofloatofwords, I n1 :: I n2 :: nil => F(Float.from_words n1 n2)
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 64e47e3..76c426b 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -94,8 +94,6 @@ Inductive operation : Type :=
   | Osubf: operation                    (**r [rd = r1 - r2] *)
   | Omulf: operation                    (**r [rd = r1 * r2] *)
   | Odivf: operation                    (**r [rd = r1 / r2] *)
-  | Omuladdf: operation                 (**r [rd = r1 * r2 + r3] *)
-  | Omulsubf: operation                 (**r [rd = r1 * r2 - r3] *)
   | Osingleoffloat: operation           (**r [rd] is [r1] truncated to single-precision float *)
 (*c Conversions between int and float: *)
   | Ointoffloat: operation              (**r [rd = signed_int_of_float(r1)] *)
@@ -203,8 +201,6 @@ Definition eval_operation
   | Osubf, v1::v2::nil => Some(Val.subf v1 v2)
   | Omulf, v1::v2::nil => Some(Val.mulf v1 v2)
   | Odivf, v1::v2::nil => Some(Val.divf v1 v2)
-  | Omuladdf, v1::v2::v3::nil => Some(Val.addf (Val.mulf v1 v2) v3)
-  | Omulsubf, v1::v2::v3::nil => Some(Val.subf (Val.mulf v1 v2) v3)
   | Osingleoffloat, v1::nil => Some(Val.singleoffloat v1)
   | Ointoffloat, v1::nil => Val.intoffloat v1
   | Ofloatofwords, v1::v2::nil => Some(Val.floatofwords v1 v2)
@@ -292,8 +288,6 @@ Definition type_of_operation (op: operation) : list typ * typ :=
   | Osubf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Omulf => (Tfloat :: Tfloat :: nil, Tfloat)
   | Odivf => (Tfloat :: Tfloat :: nil, Tfloat)
-  | Omuladdf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat)
-  | Omulsubf => (Tfloat :: Tfloat :: Tfloat :: nil, Tfloat)
   | Osingleoffloat => (Tfloat :: nil, Tfloat)
   | Ointoffloat => (Tfloat :: nil, Tint)
   | Ofloatofwords => (Tint :: Tint :: nil, Tfloat)
@@ -366,8 +360,6 @@ Proof with (try exact I).
   destruct v0; destruct v1...
   destruct v0; destruct v1...
   destruct v0; destruct v1...
-  destruct v0; destruct v1; destruct v2...
-  destruct v0; destruct v1; destruct v2...
   destruct v0...
   destruct v0; simpl in H0; inv H0. destruct (Float.intoffloat f); inv H2...
   destruct v0; destruct v1...
@@ -796,8 +788,6 @@ Proof.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
   inv H4; inv H2; simpl; auto.
-  inv H4; simpl; auto; inv H2; simpl; auto; inv H3; simpl; auto.
-  inv H4; simpl; auto; inv H2; simpl; auto; inv H3; simpl; auto.
   inv H4; simpl; auto.
   inv H4; simpl in H1; inv H1. simpl. destruct (Float.intoffloat f0); simpl in H2; inv H2.
   exists (Vint i); auto.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 8323d56..3492de4 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -476,6 +476,10 @@ let print_builtin_inline oc name args res =
       fprintf oc "	fmadd	%a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3
   | "__builtin_fmsub", [FR a1; FR a2; FR a3], FR res ->
       fprintf oc "	fmsub	%a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3
+  | "__builtin_fnmadd", [FR a1; FR a2; FR a3], FR res ->
+      fprintf oc "	fnmadd	%a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3
+  | "__builtin_fnmsub", [FR a1; FR a2; FR a3], FR res ->
+      fprintf oc "	fnmsub	%a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3
   | "__builtin_fabs", [FR a1], FR res ->
       fprintf oc "	fabs	%a, %a\n" freg res freg a1
   | "__builtin_fsqrt", [FR a1], FR res ->
@@ -636,8 +640,6 @@ let print_instruction oc tbl pc = function
       fprintf oc "%s end pseudoinstr fcti\n" comment
   | Pfdiv(r1, r2, r3) ->
       fprintf oc "	fdiv	%a, %a, %a\n" freg r1 freg r2 freg r3
-  | Pfmadd(r1, r2, r3, r4) ->
-      fprintf oc "	fmadd	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
   | Pfmake(rd, r1, r2) ->
       fprintf oc "%s begin pseudoinstr %a = fmake(%a, %a)\n"
               comment freg rd ireg r1 ireg r2;
@@ -648,8 +650,6 @@ let print_instruction oc tbl pc = function
       fprintf oc "%s end pseudoinstr fmake\n" comment
   | Pfmr(r1, r2) ->
       fprintf oc "	fmr	%a, %a\n" freg r1 freg r2
-  | Pfmsub(r1, r2, r3, r4) ->
-      fprintf oc "	fmsub	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
   | Pfmul(r1, r2, r3) ->
       fprintf oc "	fmul	%a, %a, %a\n" freg r1 freg r2 freg r3
   | Pfneg(r1, r2) ->
diff --git a/powerpc/PrintOp.ml b/powerpc/PrintOp.ml
index 13eb4ae..5bc4658 100644
--- a/powerpc/PrintOp.ml
+++ b/powerpc/PrintOp.ml
@@ -93,8 +93,6 @@ let print_operation reg pp = function
   | Osubf, [r1;r2] -> fprintf pp "%a -f %a" reg r1 reg r2
   | Omulf, [r1;r2] -> fprintf pp "%a *f %a" reg r1 reg r2
   | Odivf, [r1;r2] -> fprintf pp "%a /f %a" reg r1 reg r2
-  | Omuladdf, [r1;r2;r3] -> fprintf pp "%a *f %a +f %a" reg r1 reg r2 reg r3
-  | Omulsubf, [r1;r2;r3] -> fprintf pp "%a *f %a -f %a" reg r1 reg r2 reg r3
   | Osingleoffloat, [r1] -> fprintf pp "singleoffloat(%a)" reg r1
   | Ointoffloat, [r1] -> fprintf pp "intoffloat(%a)" reg r1
   | Ofloatofwords, [r1;r2] -> fprintf pp "floatofwords(%a,%a)" reg r1 reg r2
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).
 
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index 1d35d9f..27a0fd0 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -631,23 +631,12 @@ Qed.
 
 Theorem eval_addf: binary_constructor_sound addf Val.addf.
 Proof.
-  red; intros until y; unfold addf.
-  destruct (use_fused_mul tt); simpl.
-  case (addf_match a b); intros; InvEval.
-  TrivialExists. simpl. congruence.
-  TrivialExists. simpl. rewrite Val.addf_commut. congruence.
-  intros. TrivialExists.
-  intros. TrivialExists.
+  red; intros; TrivialExists.
 Qed.
  
 Theorem eval_subf: binary_constructor_sound subf Val.subf.
 Proof.
-  red; intros until y; unfold subf.
-  destruct (use_fused_mul tt); simpl.
-  case (subf_match a); intros; InvEval.
-  TrivialExists. simpl. congruence.
-  TrivialExists.
-  intros. TrivialExists.
+  red; intros; TrivialExists.
 Qed.
 
 Theorem eval_mulf: binary_constructor_sound mulf Val.mulf.
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
index cb4c3c2..bc0184e 100644
--- a/powerpc/extractionMachdep.v
+++ b/powerpc/extractionMachdep.v
@@ -12,9 +12,6 @@
 
 (* Additional extraction directives specific to the PowerPC port *)
 
-(* Selection *)
-Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)".
-
 (* Asm *)
 Extract Constant Asm.low_half => "fun _ -> assert false".
 Extract Constant Asm.high_half => "fun _ -> assert false".
diff --git a/test/c/Makefile b/test/c/Makefile
index 9c57a3f..2b9f4b7 100644
--- a/test/c/Makefile
+++ b/test/c/Makefile
@@ -1,7 +1,7 @@
 include ../../Makefile.config
 
 CCOMP=../../ccomp
-CCOMPFLAGS=-stdlib ../../runtime -fmadd -dc -dclight -dasm
+CCOMPFLAGS=-stdlib ../../runtime -dc -dclight -dasm
 
 CFLAGS=-O1 -Wall