diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-09-14 16:24:30 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-09-14 16:24:30 +0000 |
| commit | 76ea1108be6f8b4ba9dc0118a13f685bcb62bc2b (patch) | |
| tree | 8b2dad961e6b368426573e8a217594b9bcb42752 /backend/Constpropproof.v | |
| parent | 9a0ff6bb768cb0a6e45c1c75727d1cd8199cb89e (diff) | |
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
Diffstat (limited to 'backend/Constpropproof.v')
| -rw-r--r-- | backend/Constpropproof.v | 12 |
1 files changed, 8 insertions, 4 deletions
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]]. |