From e99d18c442c40a14e6eaea722cbc7ef0ca6dd26a Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 21 Aug 2010 10:21:11 +0000 Subject: Integers: cleaned up bitwise operations, redefined shr, zero_ext and sign_ext as bitwise operations rather than arithmetic ones. CastOptimproof: fixed for ARM port. Other files: adapted to changes in Integers. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1472 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/SelectOp.v | 80 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 77 insertions(+), 3 deletions(-) (limited to 'powerpc/SelectOp.v') diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v index fe30b96a..e6a281b2 100644 --- a/powerpc/SelectOp.v +++ b/powerpc/SelectOp.v @@ -371,6 +371,80 @@ Definition sub (e1: expr) (e2: expr) := (** ** Rotates and immediate shifts *) +(** Recognition of integers that are acceptable as immediate operands + to the [rlwim] PowerPC instruction. These integers are of the form + [000011110000] or [111100001111], that is, a run of one bits + surrounded by zero bits, or conversely. We recognize these integers by + running the following automaton on the bits. The accepting states are + 2, 3, 4, 5, and 6. +<< + 0 1 0 + / \ / \ / \ + \ / \ / \ / + -0--> [1] --1--> [2] --0--> [3] + / + [0] + \ + -1--> [4] --0--> [5] --1--> [6] + / \ / \ / \ + \ / \ / \ / + 1 0 1 +>> +*) + +Inductive rlw_state: Type := + | RLW_S0 : rlw_state + | RLW_S1 : rlw_state + | RLW_S2 : rlw_state + | RLW_S3 : rlw_state + | RLW_S4 : rlw_state + | RLW_S5 : rlw_state + | RLW_S6 : rlw_state + | RLW_Sbad : rlw_state. + +Definition rlw_transition (s: rlw_state) (b: bool) : rlw_state := + match s, b with + | RLW_S0, false => RLW_S1 + | RLW_S0, true => RLW_S4 + | RLW_S1, false => RLW_S1 + | RLW_S1, true => RLW_S2 + | RLW_S2, false => RLW_S3 + | RLW_S2, true => RLW_S2 + | RLW_S3, false => RLW_S3 + | RLW_S3, true => RLW_Sbad + | RLW_S4, false => RLW_S5 + | RLW_S4, true => RLW_S4 + | RLW_S5, false => RLW_S5 + | RLW_S5, true => RLW_S6 + | RLW_S6, false => RLW_Sbad + | RLW_S6, true => RLW_S6 + | RLW_Sbad, _ => RLW_Sbad + end. + +Definition rlw_accepting (s: rlw_state) : bool := + match s with + | RLW_S0 => false + | RLW_S1 => false + | RLW_S2 => true + | RLW_S3 => true + | RLW_S4 => true + | RLW_S5 => true + | RLW_S6 => true + | RLW_Sbad => false + end. + +Fixpoint is_rlw_mask_rec (n: nat) (s: rlw_state) (x: Z) {struct n} : bool := + match n with + | O => + rlw_accepting s + | S m => + let (b, y) := Int.Z_bin_decomp x in + is_rlw_mask_rec m (rlw_transition s b) y + end. + +Definition is_rlw_mask (x: int) : bool := + is_rlw_mask_rec Int.wordsize RLW_S0 (Int.unsigned x). + (* Definition rolm (e1: expr) := match e1 with @@ -414,7 +488,7 @@ Definition rolm (e1: expr) (amount2 mask2: int) := | rolm_case2 amount1 mask1 t1 => let amount := Int.modu (Int.add amount1 amount2) Int.iwordsize in let mask := Int.and (Int.rol mask1 amount2) mask2 in - if Int.is_rlw_mask mask + if is_rlw_mask mask then Eop (Orolm amount mask) (t1:::Enil) else Eop (Orolm amount2 mask2) (e1:::Enil) | rolm_default e1 => @@ -548,7 +622,7 @@ Definition mul (e1: expr) (e2: expr) := (** ** Bitwise and, or, xor *) Definition andimm (n1: int) (e2: expr) := - if Int.is_rlw_mask n1 + if is_rlw_mask n1 then rolm e2 Int.zero n1 else Eop (Oandimm n1) (e2:::Enil). @@ -591,7 +665,7 @@ Definition or (e1: expr) (e2: expr) := match or_match e1 e2 with | or_case1 amount1 mask1 t1 amount2 mask2 t2 => if Int.eq amount1 amount2 - && Int.is_rlw_mask (Int.or mask1 mask2) + && is_rlw_mask (Int.or mask1 mask2) && same_expr_pure t1 t2 then Eop (Orolm amount1 (Int.or mask1 mask2)) (t1:::Enil) else Eop Oor (e1:::e2:::Enil) -- cgit