diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-11-06 13:51:31 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-11-06 13:51:31 +0000 |
commit | f8202f62ed65d15738e0868005c856168a302696 (patch) | |
tree | d9a16b650e62be1c15830eb41f9339485e948bd8 /cfrontend/Cop.v | |
parent | f9c799143067c3197dc925f7fd916206d075a25d (diff) | |
download | compcert-f8202f62ed65d15738e0868005c856168a302696.tar.gz compcert-f8202f62ed65d15738e0868005c856168a302696.zip |
- 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
Diffstat (limited to 'cfrontend/Cop.v')
-rw-r--r-- | cfrontend/Cop.v | 12 |
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 := |