diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Constprop.v | 4 | ||||
-rw-r--r-- | backend/Constpropproof.v | 12 | ||||
-rw-r--r-- | backend/SelectDiv.vp | 18 | ||||
-rw-r--r-- | backend/SelectDivproof.v | 18 |
4 files changed, 46 insertions, 6 deletions
diff --git a/backend/Constprop.v b/backend/Constprop.v index 24573a59..e5ea64d8 100644 --- a/backend/Constprop.v +++ b/backend/Constprop.v @@ -322,7 +322,9 @@ Function annot_strength_reduction let (targs'', args'') := annot_strength_reduction app targs' args' in match ty, approx_reg app arg with | Tint, I n => (AA_int n :: targs'', args'') - | Tfloat, F n => (AA_float n :: targs'', args'') + | Tfloat, F n => if generate_float_constants tt + then (AA_float n :: targs'', args'') + else (AA_arg ty :: targs'', arg :: args'') | _, _ => (AA_arg ty :: targs'', arg :: args'') end | targ :: targs', _ => diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 328f724f..898c4dff 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]]. diff --git a/backend/SelectDiv.vp b/backend/SelectDiv.vp index e60a97dc..1d9168c2 100644 --- a/backend/SelectDiv.vp +++ b/backend/SelectDiv.vp @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Instruction selection for integer division and modulus *) +(** Instruction selection for division and modulus *) Require Import Coqlib. Require Import AST. @@ -154,3 +154,19 @@ Nondetfunction mods (e1: expr) (e2: expr) := | _ => mods_base e1 e2 end. +(** Floating-point division by a constant can also be turned into a FP + multiplication by the inverse constant, but only for powers of 2. *) + +Definition divfimm (e: expr) (n: float) := + match Float.exact_inverse n with + | Some n' => Eop Omulf (e ::: Eop (Ofloatconst n') Enil ::: Enil) + | None => Eop Odivf (e ::: Eop (Ofloatconst n) Enil ::: Enil) + end. + +Nondetfunction divf (e1: expr) (e2: expr) := + match e2 with + | Eop (Ofloatconst n2) Enil => divfimm e1 n2 + | _ => Eop Odivf (e1 ::: e2 ::: Enil) + end. + + diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v index 4d8f96ac..0719a5ed 100644 --- a/backend/SelectDivproof.v +++ b/backend/SelectDivproof.v @@ -544,4 +544,22 @@ Proof. - eapply eval_mods_base; eauto. Qed. +(** * Floating-point division *) + +Theorem eval_divf: + forall le a b x y, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + exists v, eval_expr ge sp e m le (divf a b) v /\ Val.lessdef (Val.divf x y) v. +Proof. + intros until y. unfold divf. destruct (divf_match b); intros. +- unfold divfimm. destruct (Float.exact_inverse n2) as [n2' | ] eqn:EINV. + + inv H0. inv H4. simpl in H6. inv H6. econstructor; split. + EvalOp. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. + simpl; eauto. + destruct x; simpl; auto. erewrite Float.div_mul_inverse; eauto. + + TrivialExists. +- TrivialExists. +Qed. + End CMCONSTRS. |