diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-10-27 17:03:26 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2021-10-28 17:16:18 +0200 |
commit | d194e47a7d494944385ff61c194693f8a67787cb (patch) | |
tree | f7e81e1152df6ff9bae7d01391a6c00c8ad9cbc6 /powerpc/Op.v | |
parent | a420914d237c96d0c5cd3a9055a0338c0d6805d4 (diff) | |
download | compcert-kvx-d194e47a7d494944385ff61c194693f8a67787cb.tar.gz compcert-kvx-d194e47a7d494944385ff61c194693f8a67787cb.zip |
PPC64: revised generation of rldic* instructions
In Op.v, the definitions of is_rldl_mask and is_rldr_mask mask were
swapped:
- rldl is for [00001111] masks that clear on the left,
hence start with 1s and finish with 0s;
- rldr is for [11110000] masks that clear on the right,
hence start with 0s and finish with 1s.
In Asmgen.v, the case for masks of the form [00011111100] that can
generate a rldic instruction was incorrectly detected.
Diffstat (limited to 'powerpc/Op.v')
-rw-r--r-- | powerpc/Op.v | 39 |
1 files changed, 24 insertions, 15 deletions
diff --git a/powerpc/Op.v b/powerpc/Op.v index a96a0439..b849efa0 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -1272,53 +1272,62 @@ Definition is_rlw_mask (x: int) : bool := is_mask_rec rlw_transition rlw_accepting Int.wordsize RLW_S0 (Int.unsigned x). (** For the 64-bit [rldicl] and [rldicr] instructions, the acceptable - masks are [1111100000] and [0000011111], that is, some ones in the - high bits and some zeroes in the low bits, or conversely. All ones - is OK, but not all zeroes. The corresponding automata are: -<< - 0 1 - / \ / \ - \ / \ / (accepting: [1]) - [0] --1--> [1] + masks are (in big endian): +- for [rldicl]: masks that clear the leftmost bits (most significant bits), + that is, [00000011111], that is, ones in the low bits followed by zeros + in the high bits; +- for [rldicr]: masks that clear the rightmost bits (least significant bits), + that is, [11110000000], that is, zeros in the low bits followed by ones + in the high bits. + All ones is OK, but not all zeroes. + The corresponding automata for [rldicl] is +<< 1 0 / \ / \ \ / \ / (accepting: [1], [2]) [0] --1--> [1] --0--> [2] >> + The automata for [rldicr] is +<< + 0 1 + / \ / \ + \ / \ / (accepting: [1]) + [0] --1--> [1] +>> *) -Inductive rll_state: Type := RLL_S0 | RLL_S1 | RLL_Sbad. +Inductive rll_state: Type := RLL_S0 | RLL_S1 | RLL_S2 | RLL_Sbad. Definition rll_transition (s: rll_state) (b: bool) : rll_state := match s, b with - | RLL_S0, false => RLL_S0 | RLL_S0, true => RLL_S1 + | RLL_S1, false => RLL_S2 | RLL_S1, true => RLL_S1 + | RLL_S2, false => RLL_S2 | _, _ => RLL_Sbad end. Definition rll_accepting (s: rll_state) : bool := match s with - | RLL_S1 => true + | RLL_S1 | RLL_S2 => true | _ => false end. -Inductive rlr_state: Type := RLR_S0 | RLR_S1 | RLR_S2 | RLR_Sbad. +Inductive rlr_state: Type := RLR_S0 | RLR_S1 | RLR_Sbad. Definition rlr_transition (s: rlr_state) (b: bool) : rlr_state := match s, b with + | RLR_S0, false => RLR_S0 | RLR_S0, true => RLR_S1 - | RLR_S1, false => RLR_S2 | RLR_S1, true => RLR_S1 - | RLR_S2, false => RLR_S2 | _, _ => RLR_Sbad end. Definition rlr_accepting (s: rlr_state) : bool := match s with - | RLR_S1 | RLR_S2 => true + | RLR_S1 => true | _ => false end. |