From a68e113d362e3d28fb1fc45d7f40692fdffe2498 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 30 Jun 2012 14:18:35 +0000 Subject: More aggressive 'uncasting' before storing small integers git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1944 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 31 ++++++++++++++++--------------- 1 file changed, 16 insertions(+), 15 deletions(-) (limited to 'cfrontend/Cminorgen.v') 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 -- cgit