__builtin_absfloat can be applied to integers too.

More precise classification of float results of arithmetic operations,
in preparation for future work on the C/Clight static type system.


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

3 files changed, 60 insertions, 22 deletions

diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index fec540b..7bda1b1 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -385,11 +385,11 @@ Proof.
   destruct (classify_bool t); auto; destruct v; auto; rewrite negb_involutive; auto.
 Qed.
 
-(** *** Opposite *)
+(** *** Opposite and absolute value *)
 
 Inductive classify_neg_cases : Type :=
   | neg_case_i(s: signedness)              (**r int *)
-  | neg_case_f                             (**r float *)
+  | neg_case_f(sz: floatsize)              (**r float *)
   | neg_case_l(s: signedness)              (**r long *)
   | neg_default.
 
@@ -397,7 +397,7 @@ Definition classify_neg (ty: type) : classify_neg_cases :=
   match ty with
   | Tint I32 Unsigned _ => neg_case_i Unsigned
   | Tint _ _ _ => neg_case_i Signed
-  | Tfloat _ _ => neg_case_f
+  | Tfloat sz _ => neg_case_f sz
   | Tlong si _ => neg_case_l si
   | _ => neg_default
   end.
@@ -409,7 +409,7 @@ Definition sem_neg (v: val) (ty: type) : option val :=
       | Vint n => Some (Vint (Int.neg n))
       | _ => None
       end
-  | neg_case_f =>
+  | neg_case_f sz =>
       match v with
       | Vfloat f => Some (Vfloat (Float.neg f))
       | _ => None
@@ -422,6 +422,26 @@ Definition sem_neg (v: val) (ty: type) : option val :=
   | neg_default => None
   end.
 
+Definition sem_absfloat (v: val) (ty: type) : option val :=
+  match classify_neg ty with
+  | neg_case_i sg =>
+      match v with
+      | Vint n => Some (Vfloat (Float.abs (cast_int_float sg F64 n)))
+      | _ => None
+      end
+  | neg_case_f sz =>
+      match v with
+      | Vfloat f => Some (Vfloat (Float.abs f))
+      | _ => None
+      end
+  | neg_case_l sg =>
+      match v with
+      | Vlong n => Some (Vfloat (Float.abs (cast_long_float sg F64 n)))
+      | _ => None
+      end
+  | neg_default => None
+  end.
+
 (** *** Bitwise complement *)
 
 Inductive classify_notint_cases : Type :=
@@ -452,12 +472,6 @@ 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
@@ -470,7 +484,7 @@ Definition sem_absfloat (v: val) (ty: type): option val :=
 Inductive binarith_cases: Type :=
   | bin_case_i (s: signedness)         (**r at int type *)
   | bin_case_l (s: signedness)         (**r at long int type *)
-  | bin_case_f                         (**r at float type *)
+  | bin_case_f (sz: floatsize)         (**r at float type *)
   | bin_default.                       (**r error *)
 
 Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases :=
@@ -482,16 +496,21 @@ Definition classify_binarith (ty1: type) (ty2: type) : binarith_cases :=
   | Tlong _ _, Tlong _ _ => bin_case_l Unsigned
   | Tlong sg _, Tint _ _ _ => bin_case_l sg
   | Tint _ _ _, Tlong sg _ => bin_case_l sg
-  | Tfloat _ _, (Tint _ _ _ | Tlong _ _ | Tfloat _ _) => bin_case_f
-  | (Tint _ _ _ | Tlong _ _), Tfloat _ _ => bin_case_f
+  | Tfloat F32 _, Tfloat F32 _ => bin_case_f F32
+  | Tfloat _ _, Tfloat _ _ => bin_case_f F64
+  | Tfloat sz _, (Tint _ _ _ | Tlong _ _) => bin_case_f sz
+  | (Tint _ _ _ | Tlong _ _), Tfloat sz _ => bin_case_f sz
   | _, _ => bin_default
   end.
 
+(** The type at which the computation is done.  Both arguments are
+  converted to this type before the actual computation.  *)
+
 Definition binarith_type (c: binarith_cases) : type :=
   match c with
   | bin_case_i sg => Tint I32 sg noattr
   | bin_case_l sg => Tlong sg noattr
-  | bin_case_f    => Tfloat F64 noattr
+  | bin_case_f sz => Tfloat F64 noattr
   | bin_default   => Tvoid
   end.
 
@@ -508,13 +527,13 @@ Definition sem_binarith
   match sem_cast v2 t2 t with
   | None => None
   | Some v2' =>
-  match classify_binarith t1 t2 with
+  match c with
   | bin_case_i sg =>
       match v1', v2' with
       | Vint n1, Vint n2 => sem_int sg n1 n2
       | _,  _ => None
       end
-  | bin_case_f =>
+  | bin_case_f sz =>
       match v1', v2' with
       | Vfloat n1, Vfloat n2 => sem_float n1 n2
       | _,  _ => None
@@ -966,7 +985,7 @@ Proof.
   (* neg *)
   unfold sem_neg in *; destruct (classify_neg ty); inv H0; inv H; TrivialInject.
   (* absfloat *)
-  unfold sem_absfloat in *; inv H0; inv H; TrivialInject.
+  unfold sem_absfloat in *; destruct (classify_neg ty); 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 1380695..c97e881 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -164,11 +164,19 @@ Definition make_notbool (e: expr) (ty: type) :=
 Definition make_neg (e: expr) (ty: type) :=
   match classify_neg ty with
   | neg_case_i _ => OK (Eunop Onegint e)
-  | neg_case_f => OK (Eunop Onegf e)
+  | neg_case_f _ => OK (Eunop Onegf e)
   | neg_case_l _ => OK (Eunop Onegl e)
   | _ => Error (msg "Cshmgen.make_neg")
   end.
 
+Definition make_absfloat (e: expr) (ty: type) :=
+  match classify_neg ty with
+  | neg_case_i sg => OK (Eunop Oabsf (make_floatofint e sg F64))
+  | neg_case_f _ => OK (Eunop Oabsf e)
+  | neg_case_l sg => OK (Eunop Oabsf (make_floatoflong e sg F64))
+  | _ => Error (msg "Cshmgen.make_absfloat")
+  end.
+
 Definition make_notint (e: expr) (ty: type) :=
   match classify_notint ty with
   | notint_case_i _ => OK (Eunop Onotint e)
@@ -187,7 +195,7 @@ Definition make_binarith (iop iopu fop lop lopu: binary_operation)
   match c with
   | bin_case_i Signed => OK (Ebinop iop e1' e2')
   | bin_case_i Unsigned => OK (Ebinop iopu e1' e2')
-  | bin_case_f => OK (Ebinop fop e1' e2')
+  | bin_case_f _ => OK (Ebinop fop e1' e2')
   | bin_case_l Signed => OK (Ebinop lop e1' e2')
   | bin_case_l Unsigned => OK (Ebinop lopu e1' e2')
   | bin_default => Error (msg "Cshmgen.make_binarith")
@@ -243,7 +251,7 @@ Definition make_binarith_int (iop iopu lop lopu: binary_operation)
   | bin_case_i Unsigned => OK (Ebinop iopu e1' e2')
   | bin_case_l Signed => OK (Ebinop lop e1' e2')
   | bin_case_l Unsigned => OK (Ebinop lopu e1' e2')
-  | bin_case_f | bin_default => Error (msg "Cshmgen.make_binarith_int")
+  | bin_case_f _ | bin_default => Error (msg "Cshmgen.make_binarith_int")
   end.
 
 Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
@@ -329,7 +337,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)
+  | Cop.Oabsfloat => make_absfloat a ta
   end.
 
 Definition transl_binop (op: Cop.binary_operation)
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index d6e881e..15c4e4c 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -348,6 +348,17 @@ Proof.
   destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
 Qed.
 
+Lemma make_absfloat_correct:
+  forall a tya c va v e le m,
+  sem_absfloat va tya = Some v ->
+  make_absfloat a tya = OK c ->  
+  eval_expr ge e le m a va ->
+  eval_expr ge e le m c v.
+Proof.
+  unfold sem_absfloat, make_absfloat; intros until m; intros SEM MAKE EV1;
+  destruct (classify_neg tya); inv MAKE; destruct va; inv SEM; eauto with cshm.
+Qed.
+
 Lemma make_notbool_correct:
   forall a tya c va v e le m,
   sem_notbool va tya = Some v ->
@@ -621,7 +632,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.
+  eapply make_absfloat_correct; eauto.
 Qed.
 
 Lemma transl_binop_correct: