- Recognize __builtin_fabs as an operator, not just a builtin,

  enabling more aggressive optimizations.
- Less aggressive CSE for EF_builtin builtins, causes problems
  for __builtin_write{16,32}_reversed.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2363 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 11 insertions, 1 deletions

diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index a1860ec0..31643a92 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -28,7 +28,8 @@ Require Import Ctypes.
 Inductive unary_operation : Type :=
   | Onotbool : unary_operation          (**r boolean negation ([!] in C) *)
   | Onotint : unary_operation           (**r integer complement ([~] in C) *)
-  | Oneg : unary_operation.             (**r opposite (unary [-]) *)
+  | Oneg : unary_operation              (**r opposite (unary [-]) *)
+  | Oabsfloat : unary_operation.        (**r floating-point absolute value *)
 
 Inductive binary_operation : Type :=
   | Oadd : binary_operation             (**r addition (binary [+]) *)
@@ -451,6 +452,12 @@ Definition sem_notint (v: val) (ty: type): option val :=
   | notint_default => None
   end.
 
+Definition sem_absfloat (v: val) (ty: type): option val :=
+  match v with
+  | Vfloat f => Some (Vfloat (Float.abs f))
+  | _ => None
+  end.
+
 (** ** Binary operators *)
 
 (** For binary operations, the "usual binary conversions" consist in
@@ -844,6 +851,7 @@ Definition sem_unary_operation
   | Onotbool => sem_notbool v ty
   | Onotint => sem_notint v ty
   | Oneg => sem_neg v ty
+  | Oabsfloat => sem_absfloat v ty
   end.
 
 Definition sem_binary_operation
@@ -957,6 +965,8 @@ Proof.
   unfold sem_notint in *; destruct (classify_notint ty); inv H0; inv H; TrivialInject.
   (* neg *)
   unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject.
+  (* absfloat *)
+  unfold sem_absfloat in *; inv H0; inv H; TrivialInject.
 Qed.
 
 Definition optval_self_injects (ov: option val) : Prop :=