summaryrefslogtreecommitdiff
path: root/backend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-07-31 12:44:18 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2008-07-31 12:44:18 +0000
commit4c8a550fae641115170e4fc9c1b1292834e0c6c0 (patch)
tree2363194510dce61b3a6e3280601654c0c8646f9a /backend
parent99294ec7c8054b92536d14883599ff3bfe7745ee (diff)
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
Diffstat (limited to 'backend')
-rw-r--r--backend/Selection.v34
-rw-r--r--backend/Selectionproof.v15
2 files changed, 29 insertions, 20 deletions
diff --git a/backend/Selection.v b/backend/Selection.v
index 6554e42..1de6ae3 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 bd4dd23..784823b 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: