From 39bc6e4f98dabf672798893df990576542ac1675 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 29 Mar 2014 08:30:03 +0000 Subject: __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 --- cfrontend/Cop.v | 53 ++++++++++++++++++++++++++++++++---------------- cfrontend/Cshmgen.v | 16 +++++++++++---- cfrontend/Cshmgenproof.v | 13 +++++++++++- 3 files changed, 60 insertions(+), 22 deletions(-) (limited to 'cfrontend') 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: -- cgit v1.2.3