diff --git a/backend/Selection.v b/backend/Selection.v
index 6554e429aaaeb785ec550c867fbd82ef84042bad..1de6ae3c0b47f90c8b57e90ed97d3d2017e8c57d 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 bd4dd2337641168d6e71349df98958c6065fc966..784823b0df14cc885ea4f1697563862a1df36a06 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 659422e98f0f0b023c71f7db42821c10b310cc93..dacc9dcb4daa30b8beb57d6397438fac47d7f7c6 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<symb> 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 <file>.light.c
-dasm Save generated assembly in <file>.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 4f6abc225de3cd9a3294361c49298cb100d35f59..ac888a527fdb1f0adce1e199e16fc8b4f0469434 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 54933cc0a329227f006516c38b1dea92faaf842b..044f89f04e98794edf3ce076a43b01d9ab37583b 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 abb792c011f5cb6ea69ce7805c7733e087fb3c1f..69034bc1087a7a50357eb5bdb8f19c38f719404d 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 c6cd928908b1b7cb3d82c22c345cdfc3028b9ff4..bff62114063bee381fd49ec1be8bb672983f73a8 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