From 3fb4ee15ed74c55923fe702a130d77120a471ca3 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sun, 2 May 2010 07:40:56 +0000
Subject: Add "fabs" (floating-point absolute value) as a unary operator in
 Clight and C#minor.  Recognize __builtin_fabs and turn it into this operator.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1329 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/C2Clight.ml     | 12 +++++++++++-
 cfrontend/Csem.v          |  7 +++++++
 cfrontend/Cshmgen.v       |  4 ++++
 cfrontend/Cshmgenproof2.v | 13 +++++++++++++
 cfrontend/Csyntax.v       |  3 ++-
 cfrontend/PrintCsyntax.ml |  3 ++-
 6 files changed, 39 insertions(+), 3 deletions(-)

(limited to 'cfrontend')

diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml
index 6fc9b5ca..46242e0f 100644
--- a/cfrontend/C2Clight.ml
+++ b/cfrontend/C2Clight.ml
@@ -371,7 +371,14 @@ let volatile_write_fun ty =
 let convertTopExpr env e =
   match e.edesc with
   | C.EBinop(C.Oassign, lhs, {edesc = C.ECall(fn, args)}, _) ->
-      convertFuncall env (Some (convertExpr env lhs)) fn args
+      (* Recognize __builtin_fabs and turn it into Clight operator *)
+      begin match fn, args with
+      | {edesc = C.EVar {name = "__builtin_fabs"}}, [arg1] ->
+          Sassign(convertExpr env lhs, 
+                  Expr(Eunop(Ofabs, convertExpr env arg1), Tfloat F64))
+      | _ ->
+          convertFuncall env (Some (convertExpr env lhs)) fn args
+      end
   | C.EBinop(C.Oassign, lhs, rhs, _) ->
       if Cutil.is_composite_type env lhs.etyp then
         unsupported "assignment between structs or between unions";
@@ -808,6 +815,9 @@ let builtins_generic = {
     "__builtin_va_list", C.TPtr(C.TVoid [], [])
   ];
   functions = [
+    (* Floating-point absolute value *)
+    "__builtin_fabs",
+      (TFloat(FDouble, []), [TFloat(FDouble, [])], false);
     (* The volatile read/volatile write functions *)
     "__builtin_volatile_read_int8unsigned",
         (TInt(IUChar, []), [TPtr(TVoid [], [])], false);
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index bd26b0f9..6e35c2f0 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -117,6 +117,12 @@ Function sem_notbool (v: val) (ty: type) : option val :=
   | _ => None
   end.
 
+Function sem_fabs (v: val) : option val :=
+  match v with
+  | Vfloat f => Some (Vfloat (Float.abs f))
+  | _ => None
+  end.
+
 Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val :=
   match classify_add t1 t2 with 
   | add_case_ii =>                      (**r integer addition *)
@@ -320,6 +326,7 @@ Definition sem_unary_operation
   | Onotbool => sem_notbool v ty
   | Onotint => sem_notint v
   | Oneg => sem_neg v ty
+  | Ofabs => sem_fabs v
   end.
 
 Definition sem_binary_operation
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 548c8df8..cc81d0f4 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -120,6 +120,9 @@ Definition make_notbool (e: expr) (ty: type) :=
 Definition make_notint (e: expr) (ty: type) :=
   Eunop Onotint e.
 
+Definition make_fabs (e: expr) (ty: type) :=
+  Eunop Oabsf e.
+
 Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_add ty1 ty2 with
   | add_case_ii => OK (Ebinop Oadd e1 e2)
@@ -317,6 +320,7 @@ Definition transl_unop (op: Csyntax.unary_operation) (a: expr) (ta: type) : res
   | Csyntax.Onotbool => OK(make_notbool a ta)
   | Csyntax.Onotint => OK(make_notint a ta)
   | Csyntax.Oneg => make_neg a ta
+  | Csyntax.Ofabs => OK(make_fabs a ta)
   end.
 
 Definition transl_binop (op: Csyntax.binary_operation)
diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v
index 769aee7f..3f0f4b3e 100644
--- a/cfrontend/Cshmgenproof2.v
+++ b/cfrontend/Cshmgenproof2.v
@@ -142,6 +142,18 @@ Proof.
   inversion H2; eauto with cshm.
 Qed.
 
+Lemma make_fabs_correct:
+  forall a tya c va v e m,
+  sem_fabs va = Some v ->
+  make_fabs a tya = c ->  
+  eval_expr globenv e m a va ->
+  eval_expr globenv e m c v.
+Proof.
+  intros until m; intro SEM. unfold make_fabs. 
+  functional inversion SEM; intros. 
+  inversion H2; eauto with cshm.
+Qed.
+
 Definition binary_constructor_correct
     (make: expr -> type -> expr -> type -> res expr)
     (sem: val -> type -> val -> type -> option val): Prop :=
@@ -298,6 +310,7 @@ Proof.
   eapply make_notbool_correct; eauto. congruence.
   eapply make_notint_correct with (tya := tya); eauto. congruence.
   eapply make_neg_correct; eauto.
+  eapply make_fabs_correct with (tya := tya); eauto. congruence.
 Qed.
 
 Lemma transl_binop_correct:
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 48c326e1..c82aa9ea 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -108,7 +108,8 @@ with fieldlist : Type :=
 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 [-]) *)
+  | Ofabs : unary_operation.            (**r floating-point absolute value *)
 
 Inductive binary_operation : Type :=
   | Oadd : binary_operation             (**r addition (binary [+]) *)
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index ebeda7cc..d6788319 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -25,7 +25,7 @@ let name_unop = function
   | Onotbool -> "!"
   | Onotint  -> "~"
   | Oneg     -> "-"
-
+  | Ofabs    -> "__builtin_fabs"
 
 let name_binop = function
   | Oadd -> "+"
@@ -131,6 +131,7 @@ let parenthesis_level (Expr (e, ty)) =
   | Econst_int _ -> 0
   | Econst_float _ -> 0
   | Evar _ -> 0
+  | Eunop(Ofabs, _) -> -10 (* force parentheses around argument *)
   | Eunop(_, _) -> 30
   | Ederef _ -> 20
   | Eaddrof _ -> 30
-- 
cgit