diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-07-31 12:44:18 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-07-31 12:44:18 +0000 |
commit | 4c8a550fae641115170e4fc9c1b1292834e0c6c0 (patch) | |
tree | 2363194510dce61b3a6e3280601654c0c8646f9a /backend | |
parent | 99294ec7c8054b92536d14883599ff3bfe7745ee (diff) | |
download | compcert-4c8a550fae641115170e4fc9c1b1292834e0c6c0.tar.gz compcert-4c8a550fae641115170e4fc9c1b1292834e0c6c0.zip |
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.v | 34 | ||||
-rw-r--r-- | backend/Selectionproof.v | 15 |
2 files changed, 29 insertions, 20 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: |