From 378ac3925503e6efd24cc34796e85d95c031e72d Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 13 Sep 2015 11:44:32 +0200 Subject: Use PowerPC 64 bits instructions (when available) for int<->FP conversions. Also: implement __builtin_isel on non-EREF platforms with a branch-free instruction sequence. Also: extend ./configure so that it recognizes "ppc64-" and "e5500-" platforms in addition to "ppc-". --- powerpc/NeedOp.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc/NeedOp.v') diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index e1307492..71c16ab9 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -56,7 +56,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval := | Onegfs | Oabsfs => op1 (default nv) | Oaddfs | Osubfs | Omulfs | Odivfs => op2 (default nv) | Osingleoffloat | Ofloatofsingle => op1 (default nv) - | Ointoffloat => op1 (default nv) + | Ointoffloat | Ointuoffloat | Ofloatofint | Ofloatofintu => op1 (default nv) | Ofloatofwords | Omakelong => op2 (default nv) | Olowlong | Ohighlong => op1 (default nv) | Ocmp c => needs_of_condition c -- cgit From f5bb397acd12292f6b41438778f2df7391d6f2fe Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:26:56 +0200 Subject: bug 17392: remove trailing whitespace in source files --- powerpc/NeedOp.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'powerpc/NeedOp.v') diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index 71c16ab9..4d8c32bd 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -101,7 +101,7 @@ Proof. intros. destruct cond; simpl in H; try (eapply default_needs_of_condition_sound; eauto; fail); simpl in *; FuncInv; InvAgree. -- eapply maskzero_sound; eauto. +- eapply maskzero_sound; eauto. - destruct (Val.maskzero_bool v i) as [b'|] eqn:MZ; try discriminate. erewrite maskzero_sound; eauto. Qed. @@ -117,7 +117,7 @@ Lemma needs_of_operation_sound: Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); simpl in *; FuncInv; InvAgree; TrivialExists. -- apply sign_ext_sound; auto. compute; auto. +- apply sign_ext_sound; auto. compute; auto. - apply sign_ext_sound; auto. compute; auto. - apply add_sound; auto. - apply add_sound; auto with na. @@ -137,8 +137,8 @@ Proof. - apply and_sound; auto. apply notint_sound; rewrite bitwise_idem; auto. - apply or_sound; auto. apply notint_sound; rewrite bitwise_idem; auto. - apply shrimm_sound; auto. -- apply rolm_sound; auto. -- destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. +- apply rolm_sound; auto. +- destruct (eval_condition c args m) as [b|] eqn:EC; simpl in H2. erewrite needs_of_condition_sound by eauto. subst v; simpl. auto with na. subst v; auto with na. @@ -154,7 +154,7 @@ Proof. intros. destruct op; simpl in *; try discriminate; inv H1; FuncInv; subst. - apply sign_ext_redundant_sound; auto. omega. - apply sign_ext_redundant_sound; auto. omega. -- apply andimm_redundant_sound; auto. +- apply andimm_redundant_sound; auto. - apply orimm_redundant_sound; auto. - apply rolm_redundant_sound; auto. Qed. -- cgit