diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-04-09 13:26:16 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2014-04-09 13:26:16 +0000 |
commit | 336a1f906a9c617e68e9d43e244bf42e9bdbae64 (patch) | |
tree | 47c65aa1aa9c9eadbd98ec0e443ad0105bb0b268 /backend/SelectLong.vp | |
parent | 76f49ca6af4ffbc77c0ba7965d409c3de04011bd (diff) | |
download | compcert-336a1f906a9c617e68e9d43e244bf42e9bdbae64.tar.gz compcert-336a1f906a9c617e68e9d43e244bf42e9bdbae64.zip |
Constprop: use "not" for "xorimm(-1)"; optimize == 1 and != 0 comparisons over booleans.
Select*: more systematic constant propagation; don't CP shifts by amounts outside of [0..31].
Driver: timer for whole compilation.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2452 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/SelectLong.vp')
-rw-r--r-- | backend/SelectLong.vp | 38 |
1 files changed, 22 insertions, 16 deletions
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index 09f29afc..0c1cbb3a 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -27,10 +27,10 @@ Open Local Scope cminorsel_scope. the names of these functions. *) Record helper_functions : Type := mk_helper_functions { - i64_dtos: ident; (**r float -> signed long *) - i64_dtou: ident; (**r float -> unsigned long *) - i64_stod: ident; (**r signed long -> float *) - i64_utod: ident; (**r unsigned long -> float *) + i64_dtos: ident; (**r float64 -> signed long *) + i64_dtou: ident; (**r float64 -> unsigned long *) + i64_stod: ident; (**r signed long -> float64 *) + i64_utod: ident; (**r unsigned long -> float64 *) i64_stof: ident; (**r signed long -> float32 *) i64_utof: ident; (**r unsigned long -> float32 *) i64_neg: ident; (**r opposite *) @@ -304,13 +304,16 @@ Definition cmplu_gen (ch cl: comparison) (e1 e2: expr) := Definition cmplu (c: comparison) (e1 e2: expr) := match c with | Ceq => - if is_longconst_zero e2 - then cmpl_eq_zero e1 - else cmpl_eq_zero (xorl e1 e2) + cmpl_eq_zero (xorl e1 e2) +(* + (if is_longconst_zero e2 then e1 + else if is_longconst_zero e1 then e2 + else xorl e1 e2) *) | Cne => - if is_longconst_zero e2 - then cmpl_ne_zero e1 - else cmpl_ne_zero (xorl e1 e2) + cmpl_ne_zero (xorl e1 e2) +(* (if is_longconst_zero e2 then e1 + else if is_longconst_zero e1 then e2 + else xorl e1 e2) *) | Clt => cmplu_gen Clt Clt e1 e2 | Cle => @@ -330,13 +333,16 @@ Definition cmpl_gen (ch cl: comparison) (e1 e2: expr) := Definition cmpl (c: comparison) (e1 e2: expr) := match c with | Ceq => - if is_longconst_zero e2 - then cmpl_eq_zero e1 - else cmpl_eq_zero (xorl e1 e2) + cmpl_eq_zero (xorl e1 e2) +(* + (if is_longconst_zero e2 then e1 + else if is_longconst_zero e1 then e2 + else xorl e1 e2) *) | Cne => - if is_longconst_zero e2 - then cmpl_ne_zero e1 - else cmpl_ne_zero (xorl e1 e2) + cmpl_ne_zero (xorl e1 e2) +(* (if is_longconst_zero e2 then e1 + else if is_longconst_zero e1 then e2 + else xorl e1 e2) *) | Clt => if is_longconst_zero e2 then comp Clt (highlong e1) (Eop (Ointconst Int.zero) Enil) |