diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-30 14:18:35 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2012-06-30 14:18:35 +0000 |
commit | a68e113d362e3d28fb1fc45d7f40692fdffe2498 (patch) | |
tree | 85a8c175702b1c1b92ed76de6a5187d9175ad3a1 /cfrontend/Cminorgen.v | |
parent | 7492cf1e20f39dab6f721b10332c1f4fcfb7c42f (diff) | |
download | compcert-a68e113d362e3d28fb1fc45d7f40692fdffe2498.tar.gz compcert-a68e113d362e3d28fb1fc45d7f40692fdffe2498.zip |
More aggressive 'uncasting' before storing small integers
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1944 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cfrontend/Cminorgen.v')
-rw-r--r-- | cfrontend/Cminorgen.v | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index a849a9ad..20e7bdb4 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -77,28 +77,29 @@ Definition compilenv := PMap.t var_info. with that implicitly performed by the memory store. [store_arg] detects this case and strips away the redundant cast. *) -Function uncast_int8 (e: expr) : expr := - match e with - | Eunop (Ocast8unsigned|Ocast8signed|Ocast16unsigned|Ocast16signed) e1 => - uncast_int8 e1 - | Ebinop Oand e1 (Econst (Ointconst n)) => - if Int.eq (Int.and n (Int.repr 255)) (Int.repr 255) - then uncast_int8 e1 - else e - | _ => e - end. - -Function uncast_int16 (e: expr) : expr := +Function uncast_int (m: int) (e: expr) {struct e} : expr := match e with + | Eunop (Ocast8unsigned|Ocast8signed) e1 => + if Int.eq (Int.and (Int.repr 255) m) m then uncast_int m e1 else e | Eunop (Ocast16unsigned|Ocast16signed) e1 => - uncast_int16 e1 + if Int.eq (Int.and (Int.repr 65535) m) m then uncast_int m e1 else e | Ebinop Oand e1 (Econst (Ointconst n)) => - if Int.eq (Int.and n (Int.repr 65535)) (Int.repr 65535) - then uncast_int16 e1 + if Int.eq (Int.and n m) m then uncast_int m e1 else e + | Ebinop Oshru e1 (Econst (Ointconst n)) => + if Int.eq (Int.shru (Int.shl m n) n) m + then Ebinop Oshru (uncast_int (Int.shl m n) e1) (Econst (Ointconst n)) + else e + | Ebinop Oshr e1 (Econst (Ointconst n)) => + if Int.eq (Int.shru (Int.shl m n) n) m + then Ebinop Oshr (uncast_int (Int.shl m n) e1) (Econst (Ointconst n)) else e | _ => e end. +Definition uncast_int8 (e: expr) : expr := uncast_int (Int.repr 255) e. + +Definition uncast_int16 (e: expr) : expr := uncast_int (Int.repr 65535) e. + Function uncast_float32 (e: expr) : expr := match e with | Eunop Osingleoffloat e1 => uncast_float32 e1 |