From f8202f62ed65d15738e0868005c856168a302696 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 6 Nov 2013 13:51:31 +0000
Subject: - 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
---
 cfrontend/C2C.ml          |  3 +++
 cfrontend/Cop.v           | 12 +++++++++++-
 cfrontend/Cshmgen.v       |  1 +
 cfrontend/Cshmgenproof.v  |  1 +
 cfrontend/PrintClight.ml  |  2 ++
 cfrontend/PrintCsyntax.ml |  3 +++
 6 files changed, 21 insertions(+), 1 deletion(-)

(limited to 'cfrontend')

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 285797d..8083535 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -576,6 +576,9 @@ let rec convertExpr env e =
  | C.ECall({edesc = C.EVar {name = "__builtin_memcpy_aligned"}}, args) ->
       make_builtin_memcpy (convertExprList env args)
 
+  | C.ECall({edesc = C.EVar {name = "__builtin_fabs"}}, [arg]) ->
+      Eunop(Oabsfloat, convertExpr env arg, ty)
+
   | C.ECall(fn, args) ->
       if not (supported_return_type env e.etyp) then
         unsupported ("function returning a result of type " ^ string_of_type e.etyp);
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index a1860ec..31643a9 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 :=
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index fd34985..f37e8c7 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -329,6 +329,7 @@ Definition transl_unop (op: Cop.unary_operation) (a: expr) (ta: type) : res expr
   | Cop.Onotbool => make_notbool a ta
   | Cop.Onotint => make_notint a ta
   | Cop.Oneg => make_neg a ta
+  | Cop.Oabsfloat => OK (Eunop Oabsf a)
   end.
 
 Definition transl_binop (op: Cop.binary_operation)
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 1eb5830..851e3f2 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -598,6 +598,7 @@ Proof.
   eapply make_notbool_correct; eauto. 
   eapply make_notint_correct; eauto. 
   eapply make_neg_correct; eauto.
+  inv H. unfold sem_absfloat in H0. destruct va; inv H0. eauto with cshm.
 Qed.
 
 Lemma transl_binop_correct:
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index a8b2b98..8f0bfbf 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -82,6 +82,8 @@ let rec expr p (prec, e) =
       fprintf p "%F" (camlfloat_of_coqfloat f)
   | Econst_long(n, _) ->
       fprintf p "%LdLL" (camlint64_of_coqint n)
+  | Eunop(Oabsfloat, a1, _) ->
+      fprintf p "__builtin_fabs(%a)" expr (2, a1)
   | Eunop(op, a1, _) ->
       fprintf p "%s%a" (name_unop op) expr (prec', a1)
   | Eaddrof(a1, _) ->
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index ec82869..0bed647 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -30,6 +30,7 @@ let name_unop = function
   | Onotbool -> "!"
   | Onotint  -> "~"
   | Oneg     -> "-"
+  | Oabsfloat -> "__builtin_fabs"
 
 let name_binop = function
   | Oadd -> "+"
@@ -215,6 +216,8 @@ let rec expr p (prec, e) =
       fprintf p "sizeof(%s)" (name_type ty)
   | Ealignof(ty, _) ->
       fprintf p "__alignof__(%s)" (name_type ty)
+  | Eunop(Oabsfloat, a1, _) ->
+      fprintf p "__builtin_fabs(%a)" expr (2, a1)
   | Eunop(op, a1, _) ->
       fprintf p "%s%a" (name_unop op) expr (prec', a1)
   | Eaddrof(a1, _) ->
-- 
cgit v1.2.3