From 76ea1108be6f8b4ba9dc0118a13f685bcb62bc2b Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Sep 2013 16:24:30 +0000 Subject: Floats.v, Nan.v: hard-wire the general shape of binop_pl, so that no axioms are necessary, only two parameters (default_pl and choose_binop_pl). SelectDiv: optimize FP division by a power of 2. ConstpropOp: optimize 2.0 * x and x * 2.0 into x + x. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2326 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Constpropproof.v | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 328f724..898c4df 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -517,10 +517,14 @@ Proof. exists (ev1 :: eargs''); split. simpl; constructor; auto. simpl. congruence. } - destruct ty; destruct (approx_reg app arg) as [] eqn:E2; inv H; auto; - exists eargs''; split; auto; simpl; f_equal; auto; - generalize (MATCH arg); rewrite E2; simpl; intros E3; - rewrite E3 in H5; inv H5; auto. + destruct ty; destruct (approx_reg app arg) as [] eqn:E2; inv H; auto. + * exists eargs''; split; auto; simpl; f_equal; auto. + generalize (MATCH arg); rewrite E2; simpl; intros E3; + rewrite E3 in H5; inv H5; auto. + * destruct (generate_float_constants tt); inv H1; auto. + exists eargs''; split; auto; simpl; f_equal; auto. + generalize (MATCH arg); rewrite E2; simpl; intros E3; + rewrite E3 in H5; inv H5; auto. + destruct (annot_strength_reduction app targs args) as [targs'' args''] eqn:E. inv H. exploit IHtargs; eauto. intros [eargs'' [A B]]. -- cgit v1.2.3