From 4c8a550fae641115170e4fc9c1b1292834e0c6c0 Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 31 Jul 2008 12:44:18 +0000 Subject: Flag to turn on/off the recognition of fused multiply-add and multiply-sub git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@706 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Selection.v | 34 +++++++++++++++++------------ backend/Selectionproof.v | 15 +++++++------ caml/Driver.ml | 19 ++++++---------- extraction/.depend | 56 +++++++++++++++++++++++++----------------------- extraction/Makefile | 1 + extraction/extraction.v | 3 +++ test/c/Makefile | 2 +- 7 files changed, 69 insertions(+), 61 deletions(-) diff --git a/backend/Selection.v b/backend/Selection.v index 6554e429..1de6ae3c 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -712,6 +712,8 @@ Definition shru (e1: expr) (e2: expr) := (** ** Floating-point arithmetic *) +Parameter use_fused_mul : unit -> bool. + (* Definition addf (e1: expr) (e2: expr) := match e1, e2 with @@ -749,14 +751,16 @@ Definition addf_match (e1: expr) (e2: expr) := end. Definition addf (e1: expr) (e2: expr) := - match addf_match e1 e2 with - | addf_case1 t1 t2 t3 => - Eop Omuladdf (t1:::t2:::t3:::Enil) - | addf_case2 t1 t2 t3 => - Elet t1 (Eop Omuladdf (lift t2:::lift t3:::Eletvar 0:::Enil)) - | addf_default e1 e2 => - Eop Oaddf (e1:::e2:::Enil) - end. + if use_fused_mul tt then + match addf_match e1 e2 with + | addf_case1 t1 t2 t3 => + Eop Omuladdf (t1:::t2:::t3:::Enil) + | addf_case2 t1 t2 t3 => + Eop Omuladdf (t2:::t3:::t1:::Enil) + | addf_default e1 e2 => + Eop Oaddf (e1:::e2:::Enil) + end + else Eop Oaddf (e1:::e2:::Enil). (* Definition subf (e1: expr) (e2: expr) := @@ -783,12 +787,14 @@ Definition subf_match (e1: expr) (e2: expr) := end. Definition subf (e1: expr) (e2: expr) := - match subf_match e1 e2 with - | subf_case1 t1 t2 t3 => - Eop Omulsubf (t1:::t2:::t3:::Enil) - | subf_default e1 e2 => - Eop Osubf (e1:::e2:::Enil) - end. + if use_fused_mul tt then + match subf_match e1 e2 with + | subf_case1 t1 t2 t3 => + Eop Omulsubf (t1:::t2:::t3:::Enil) + | subf_default e1 e2 => + Eop Osubf (e1:::e2:::Enil) + end + else Eop Osubf (e1:::e2:::Enil). (** ** Truncations and sign extensions *) diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index bd4dd233..784823b0 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -722,13 +722,13 @@ Theorem eval_addf: eval_expr ge sp e m le b (Vfloat y) -> eval_expr ge sp e m le (addf a b) (Vfloat (Float.add x y)). Proof. - intros until y; unfold addf; case (addf_match a b); intros; InvEval. + intros until y; unfold addf. + destruct (use_fused_mul tt). + case (addf_match a b); intros; InvEval. EvalOp. simpl. congruence. - econstructor. eauto. EvalOp. econstructor. eauto with evalexpr. - econstructor. eauto with evalexpr. econstructor. - econstructor. simpl. reflexivity. constructor. - simpl. subst y. rewrite Float.addf_commut. auto. + EvalOp. simpl. rewrite Float.addf_commut. congruence. EvalOp. + intros. EvalOp. Qed. Theorem eval_subf: @@ -737,9 +737,12 @@ Theorem eval_subf: eval_expr ge sp e m le b (Vfloat y) -> eval_expr ge sp e m le (subf a b) (Vfloat (Float.sub x y)). Proof. - intros until y; unfold subf; case (subf_match a b); intros. + intros until y; unfold subf. + destruct (use_fused_mul tt). + case (subf_match a b); intros. InvEval. EvalOp. simpl. congruence. EvalOp. + intros. EvalOp. Qed. Theorem eval_cast8signed: diff --git a/caml/Driver.ml b/caml/Driver.ml index 659422e9..dacc9dcb 100644 --- a/caml/Driver.ml +++ b/caml/Driver.ml @@ -11,6 +11,7 @@ (* *********************************************************************) open Printf +open Clflags (* Location of the standard library *) @@ -20,19 +21,6 @@ let stdlib_path = ref( with Not_found -> Configuration.stdlib_path) -(* Command-line flags *) - -let prepro_options = ref ([]: string list) -let linker_options = ref ([]: string list) -let exe_name = ref "a.out" -let option_flonglong = ref false -let option_dclight = ref false -let option_dasm = ref false -let option_E = ref false -let option_S = ref false -let option_c = ref false -let option_v = ref false - let command cmd = if !option_v then begin prerr_string "+ "; prerr_string cmd; prerr_endline "" @@ -273,6 +261,7 @@ Preprocessing options: -U Undefine preprocessor symbol Compilation options: -flonglong Treat 'long long' as 'long' and 'long double' as 'double' + -fmadd Use fused multiply-add and multiply-sub instructions -dclight Save generated Clight in .light.c -dasm Save generated assembly in .s Linking options: @@ -308,6 +297,10 @@ let rec parse_cmdline i = option_flonglong := true; parse_cmdline (i + 1) end else + if s = "-fmadd" then begin + option_fmadd := true; + parse_cmdline (i + 1) + end else if s = "-dclight" then begin option_dclight := true; parse_cmdline (i + 1) diff --git a/extraction/.depend b/extraction/.depend index 4f6abc22..ac888a52 100644 --- a/extraction/.depend +++ b/extraction/.depend @@ -33,13 +33,13 @@ Locations.cmx InterfGraph.cmx Datatypes.cmx Conventions.cmx \ ../caml/Camlcoq.cmx BinPos.cmx BinInt.cmx AST.cmx ../caml/Coloringaux.cmi ../caml/Driver.cmo: ../caml/PrintPPC.cmi ../caml/PrintCsyntax.cmo Main.cmi \ - Errors.cmi Csyntax.cmi ../caml/Configuration.cmo ../caml/Cil2Csyntax.cmo \ - ../caml/Camlcoq.cmo ../caml/CMtypecheck.cmi ../caml/CMparser.cmi \ - ../caml/CMlexer.cmi + Errors.cmi Csyntax.cmi ../caml/Configuration.cmo ../caml/Clflags.cmo \ + ../caml/Cil2Csyntax.cmo ../caml/Camlcoq.cmo ../caml/CMtypecheck.cmi \ + ../caml/CMparser.cmi ../caml/CMlexer.cmi ../caml/Driver.cmx: ../caml/PrintPPC.cmx ../caml/PrintCsyntax.cmx Main.cmx \ - Errors.cmx Csyntax.cmx ../caml/Configuration.cmx ../caml/Cil2Csyntax.cmx \ - ../caml/Camlcoq.cmx ../caml/CMtypecheck.cmx ../caml/CMparser.cmx \ - ../caml/CMlexer.cmx + Errors.cmx Csyntax.cmx ../caml/Configuration.cmx ../caml/Clflags.cmx \ + ../caml/Cil2Csyntax.cmx ../caml/Camlcoq.cmx ../caml/CMtypecheck.cmx \ + ../caml/CMparser.cmx ../caml/CMlexer.cmx ../caml/Floataux.cmo: Integers.cmi ../caml/Camlcoq.cmo ../caml/Floataux.cmx: Integers.cmx ../caml/Camlcoq.cmx ../caml/Linearizeaux.cmo: Maps.cmi Lattice.cmi LTL.cmi Datatypes.cmi \ @@ -87,8 +87,8 @@ Cminorgen.cmi: Zmax.cmi Specif.cmi OrderedType.cmi Ordered.cmi Mem.cmi \ Cminor.cmi: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ Globalenvs.cmi Floats.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi \ AST.cmi -CminorSel.cmi: Values.cmi Op.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi \ - CList.cmi BinInt.cmi AST.cmi +CminorSel.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi AST.cmi Coloring.cmi: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \ Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ CList.cmi BinInt.cmi AST.cmi @@ -137,8 +137,8 @@ Linearize.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Op.cmi Maps.cmi \ Lattice.cmi LTLin.cmi LTL.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \ CString.cmi CList.cmi CInt.cmi BinPos.cmi BinInt.cmi Ascii.cmi AST.cmi Linear.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ - Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ - AST.cmi + Globalenvs.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi CList.cmi \ + BinPos.cmi BinInt.cmi AST.cmi Locations.cmi: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ BinInt.cmi AST.cmi LTLin.cmi: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ @@ -176,7 +176,7 @@ Registers.cmi: Specif.cmi OrderedType.cmi Ordered.cmi Maps.cmi Datatypes.cmi \ Reload.cmi: Specif.cmi Parallelmove.cmi Op.cmi Locations.cmi Linear.cmi \ LTLin.cmi Datatypes.cmi Conventions.cmi CList.cmi AST.cmi RTLgen.cmi: Switch.cmi Specif.cmi Registers.cmi RTL.cmi Op.cmi Maps.cmi \ - Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CminorSel.cmi \ + Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi CminorSel.cmi Cminor.cmi \ CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi RTL.cmi: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \ Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi @@ -249,10 +249,12 @@ Cminor.cmo: Values.cmi Specif.cmi Mem.cmi Maps.cmi Integers.cmi \ Cminor.cmx: Values.cmx Specif.cmx Mem.cmx Maps.cmx Integers.cmx \ Globalenvs.cmx Floats.cmx Datatypes.cmx CList.cmx BinPos.cmx BinInt.cmx \ AST.cmx Cminor.cmi -CminorSel.cmo: Values.cmi Op.cmi Integers.cmi Globalenvs.cmi Datatypes.cmi \ - CList.cmi BinInt.cmi AST.cmi CminorSel.cmi -CminorSel.cmx: Values.cmx Op.cmx Integers.cmx Globalenvs.cmx Datatypes.cmx \ - CList.cmx BinInt.cmx AST.cmx CminorSel.cmi +CminorSel.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Integers.cmi \ + Globalenvs.cmi Datatypes.cmi Cminor.cmi CList.cmi BinInt.cmi AST.cmi \ + CminorSel.cmi +CminorSel.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Integers.cmx \ + Globalenvs.cmx Datatypes.cmx Cminor.cmx CList.cmx BinInt.cmx AST.cmx \ + CminorSel.cmi Coloring.cmo: Specif.cmi Registers.cmi RTLtyping.cmi RTL.cmi Op.cmi Maps.cmi \ Locations.cmi InterfGraph.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi \ ../caml/Coloringaux.cmi CList.cmi BinInt.cmi AST.cmi Coloring.cmi @@ -366,11 +368,11 @@ Linearize.cmx: Specif.cmx OrderedType.cmx Ordered.cmx Op.cmx Maps.cmx \ FSetAVL.cmx Errors.cmx Datatypes.cmx Coqlib.cmx CString.cmx CList.cmx \ BinPos.cmx BinInt.cmx Ascii.cmx AST.cmx Linearize.cmi Linear.cmo: Values.cmi Specif.cmi Op.cmi Mem.cmi Locations.cmi Integers.cmi \ - Globalenvs.cmi Datatypes.cmi Coqlib.cmi CList.cmi BinPos.cmi BinInt.cmi \ - AST.cmi Linear.cmi + Globalenvs.cmi Datatypes.cmi Coqlib.cmi Conventions.cmi CList.cmi \ + BinPos.cmi BinInt.cmi AST.cmi Linear.cmi Linear.cmx: Values.cmx Specif.cmx Op.cmx Mem.cmx Locations.cmx Integers.cmx \ - Globalenvs.cmx Datatypes.cmx Coqlib.cmx CList.cmx BinPos.cmx BinInt.cmx \ - AST.cmx Linear.cmi + Globalenvs.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx CList.cmx \ + BinPos.cmx BinInt.cmx AST.cmx Linear.cmi Locations.cmo: Values.cmi Specif.cmi Datatypes.cmi Coqlib.cmi BinPos.cmi \ BinInt.cmi AST.cmi Locations.cmi Locations.cmx: Values.cmx Specif.cmx Datatypes.cmx Coqlib.cmx BinPos.cmx \ @@ -453,12 +455,12 @@ Reload.cmx: Specif.cmx Parallelmove.cmx Op.cmx Locations.cmx Linear.cmx \ LTLin.cmx Datatypes.cmx Conventions.cmx CList.cmx AST.cmx Reload.cmi RTLgen.cmo: Switch.cmi Specif.cmi Registers.cmi ../caml/RTLgenaux.cmo RTL.cmi \ Op.cmi Maps.cmi Integers.cmi Errors.cmi Datatypes.cmi Coqlib.cmi \ - CminorSel.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi AST.cmi \ - RTLgen.cmi + CminorSel.cmi Cminor.cmi CString.cmi CList.cmi BinPos.cmi Ascii.cmi \ + AST.cmi RTLgen.cmi RTLgen.cmx: Switch.cmx Specif.cmx Registers.cmx ../caml/RTLgenaux.cmx RTL.cmx \ Op.cmx Maps.cmx Integers.cmx Errors.cmx Datatypes.cmx Coqlib.cmx \ - CminorSel.cmx CString.cmx CList.cmx BinPos.cmx Ascii.cmx AST.cmx \ - RTLgen.cmi + CminorSel.cmx Cminor.cmx CString.cmx CList.cmx BinPos.cmx Ascii.cmx \ + AST.cmx RTLgen.cmi RTL.cmo: Values.cmi Registers.cmi Op.cmi Mem.cmi Maps.cmi Integers.cmi \ Globalenvs.cmi Datatypes.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \ RTL.cmi @@ -472,11 +474,11 @@ RTLtyping.cmx: Specif.cmx Registers.cmx ../caml/RTLtypingaux.cmx RTL.cmx \ Op.cmx Maps.cmx Errors.cmx Datatypes.cmx Coqlib.cmx Conventions.cmx \ CString.cmx CList.cmx Ascii.cmx AST.cmx RTLtyping.cmi Selection.cmo: Specif.cmi Op.cmi Integers.cmi Datatypes.cmi Compare_dec.cmi \ - CminorSel.cmi Cminor.cmi CList.cmi BinPos.cmi BinInt.cmi AST.cmi \ - Selection.cmi + CminorSel.cmi Cminor.cmi ../caml/Clflags.cmo CList.cmi BinPos.cmi \ + BinInt.cmi AST.cmi Selection.cmi Selection.cmx: Specif.cmx Op.cmx Integers.cmx Datatypes.cmx Compare_dec.cmx \ - CminorSel.cmx Cminor.cmx CList.cmx BinPos.cmx BinInt.cmx AST.cmx \ - Selection.cmi + CminorSel.cmx Cminor.cmx ../caml/Clflags.cmx CList.cmx BinPos.cmx \ + BinInt.cmx AST.cmx Selection.cmi Setoid.cmo: Datatypes.cmi Setoid.cmi Setoid.cmx: Datatypes.cmx Setoid.cmi Specif.cmo: Datatypes.cmi Specif.cmi diff --git a/extraction/Makefile b/extraction/Makefile index 54933cc0..044f89f0 100644 --- a/extraction/Makefile +++ b/extraction/Makefile @@ -22,6 +22,7 @@ FILES=\ Coqlib.ml Maps.ml Ordered.ml Errors.ml AST.ml Iteration.ml Integers.ml \ ../caml/Camlcoq.ml ../caml/Floataux.ml Floats.ml Parmov.ml Values.ml \ Mem.ml Globalenvs.ml \ + ../caml/Clflags.ml \ Csyntax.ml Ctyping.ml Cminor.ml Csharpminor.ml Cshmgen.ml \ Cminorgen.ml \ Op.ml CminorSel.ml \ diff --git a/extraction/extraction.v b/extraction/extraction.v index abb792c0..69034bc1 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -50,6 +50,9 @@ Extract Constant Iteration.GenIter.iterate => in iter". +(* Selection *) +Extract Constant Selection.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". + (* RTLgen *) Extract Constant RTLgen.compile_switch => "RTLgenaux.compile_switch". Extract Constant RTLgen.more_likely => "RTLgenaux.more_likely". diff --git a/test/c/Makefile b/test/c/Makefile index c6cd9289..bff62114 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -1,7 +1,7 @@ include ../../Makefile.config CCOMP=../../ccomp -CCOMPFLAGS=-stdlib ../../runtime -dclight -dasm +CCOMPFLAGS=-stdlib ../../runtime -fmadd -dclight -dasm CFLAGS=-O1 -Wall -- cgit