cryspen / hacl-packages / 5808703668

5808703668

Pull #418

github

web-flow 
Merge 4abdd0203 into 1575f26e8
Pull Request #418: Add support for Hacl_AES_128_GCM_NI and Hacl_AES_128_GCM_M32

7433 of 7433 new or added lines in 12 files covered. (100.0%)

31975 of 62256 relevant lines covered (51.36%)

1238863.46 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

95.1
/src/Hacl_Gf128_CT64.c
1 
/* MIT License
2 
 *
3 
 * Copyright (c) 2016-2022 INRIA, CMU and Microsoft Corporation
4 
 * Copyright (c) 2022-2023 HACL* Contributors
5 
 *
6 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
7 
 * of this software and associated documentation files (the "Software"), to deal
8 
 * in the Software without restriction, including without limitation the rights
9 
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10 
 * copies of the Software, and to permit persons to whom the Software is
11 
 * furnished to do so, subject to the following conditions:
12 
 *
13 
 * The above copyright notice and this permission notice shall be included in all
14 
 * copies or substantial portions of the Software.
15 
 *
16 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21 
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
22 
 * SOFTWARE.
23 
 */
24 









25












26



#include "Hacl_Gf128_CT64.h"










27












28



static inline void fmul0(uint64_t *x, uint64_t *y)











29



{




45,446✔






30



  uint64_t uu____0 = y[0U];




45,446✔






31



  uint64_t




45,446✔






32



  x10 =




45,446✔






33



    (uu____0 & (uint64_t)0x5555555555555555U)




45,446✔






34



    << (uint32_t)(uint8_t)1U




45,446✔






35



    | (uu____0 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




45,446✔






36



  uint64_t




45,446✔






37



  x20 =




45,446✔






38



    (x10 & (uint64_t)0x3333333333333333U)




45,446✔






39



    << (uint32_t)(uint8_t)2U




45,446✔






40



    | (x10 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




45,446✔






41



  uint64_t




45,446✔






42



  x30 =




45,446✔






43



    (x20 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




45,446✔






44



    << (uint32_t)(uint8_t)4U




45,446✔






45



    | (x20 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




45,446✔






46



  uint64_t




45,446✔






47



  x4 =




45,446✔






48



    (x30 & (uint64_t)0x00FF00FF00FF00FFU)




45,446✔






49



    << (uint32_t)(uint8_t)8U




45,446✔






50



    | (x30 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




45,446✔






51



  uint64_t




45,446✔






52



  x5 =




45,446✔






53



    (x4 & (uint64_t)0x0000FFFF0000FFFFU)




45,446✔






54



    << (uint32_t)(uint8_t)16U




45,446✔






55



    | (x4 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




45,446✔






56



  uint64_t yr1 = x5 << (uint32_t)32U | x5 >> (uint32_t)32U;




45,446✔






57



  uint64_t uu____1 = y[1U];




45,446✔






58



  uint64_t




45,446✔






59



  x11 =




45,446✔






60



    (uu____1 & (uint64_t)0x5555555555555555U)




45,446✔






61



    << (uint32_t)(uint8_t)1U




45,446✔






62



    | (uu____1 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




45,446✔






63



  uint64_t




45,446✔






64



  x21 =




45,446✔






65



    (x11 & (uint64_t)0x3333333333333333U)




45,446✔






66



    << (uint32_t)(uint8_t)2U




45,446✔






67



    | (x11 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




45,446✔






68



  uint64_t




45,446✔






69



  x31 =




45,446✔






70



    (x21 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




45,446✔






71



    << (uint32_t)(uint8_t)4U




45,446✔






72



    | (x21 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




45,446✔






73



  uint64_t




45,446✔






74



  x40 =




45,446✔






75



    (x31 & (uint64_t)0x00FF00FF00FF00FFU)




45,446✔






76



    << (uint32_t)(uint8_t)8U




45,446✔






77



    | (x31 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




45,446✔






78



  uint64_t




45,446✔






79



  x50 =




45,446✔






80



    (x40 & (uint64_t)0x0000FFFF0000FFFFU)




45,446✔






81



    << (uint32_t)(uint8_t)16U




45,446✔






82



    | (x40 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




45,446✔






83



  uint64_t yr2 = x50 << (uint32_t)32U | x50 >> (uint32_t)32U;




45,446✔






84



  uint64_t uu____2 = x[0U];




45,446✔






85



  uint64_t uu____3 = x[1U];




45,446✔






86



  uint64_t uu____4 = y[0U];




45,446✔






87



  uint64_t uu____5 = y[1U];




45,446✔






88



  uint64_t uu____6 = y[0U] ^ y[1U];




45,446✔






89



  uint64_t




45,446✔






90



  x12 =




45,446✔






91



    (uu____2 & (uint64_t)0x5555555555555555U)




45,446✔






92



    << (uint32_t)(uint8_t)1U




45,446✔






93



    | (uu____2 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




45,446✔






94



  uint64_t




45,446✔






95



  x22 =




45,446✔






96



    (x12 & (uint64_t)0x3333333333333333U)




45,446✔






97



    << (uint32_t)(uint8_t)2U




45,446✔






98



    | (x12 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




45,446✔






99



  uint64_t




45,446✔






100



  x32 =




45,446✔






101



    (x22 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




45,446✔






102



    << (uint32_t)(uint8_t)4U




45,446✔






103



    | (x22 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




45,446✔






104



  uint64_t




45,446✔






105



  x41 =




45,446✔






106



    (x32 & (uint64_t)0x00FF00FF00FF00FFU)




45,446✔






107



    << (uint32_t)(uint8_t)8U




45,446✔






108



    | (x32 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




45,446✔






109



  uint64_t




45,446✔






110



  x51 =




45,446✔






111



    (x41 & (uint64_t)0x0000FFFF0000FFFFU)




45,446✔






112



    << (uint32_t)(uint8_t)16U




45,446✔






113



    | (x41 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




45,446✔






114



  uint64_t y1r = x51 << (uint32_t)32U | x51 >> (uint32_t)32U;




45,446✔






115



  uint64_t




45,446✔






116



  x13 =




45,446✔






117



    (uu____3 & (uint64_t)0x5555555555555555U)




45,446✔






118



    << (uint32_t)(uint8_t)1U




45,446✔






119



    | (uu____3 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




45,446✔






120



  uint64_t




45,446✔






121



  x23 =




45,446✔






122



    (x13 & (uint64_t)0x3333333333333333U)




45,446✔






123



    << (uint32_t)(uint8_t)2U




45,446✔






124



    | (x13 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




45,446✔






125



  uint64_t




45,446✔






126



  x33 =




45,446✔






127



    (x23 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




45,446✔






128



    << (uint32_t)(uint8_t)4U




45,446✔






129



    | (x23 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




45,446✔






130



  uint64_t




45,446✔






131



  x42 =




45,446✔






132



    (x33 & (uint64_t)0x00FF00FF00FF00FFU)




45,446✔






133



    << (uint32_t)(uint8_t)8U




45,446✔






134



    | (x33 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




45,446✔






135



  uint64_t




45,446✔






136



  x52 =




45,446✔






137



    (x42 & (uint64_t)0x0000FFFF0000FFFFU)




45,446✔






138



    << (uint32_t)(uint8_t)16U




45,446✔






139



    | (x42 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




45,446✔






140



  uint64_t y2r = x52 << (uint32_t)32U | x52 >> (uint32_t)32U;




45,446✔






141



  uint64_t y3 = uu____2 ^ uu____3;




45,446✔






142



  uint64_t y3r = y1r ^ y2r;




45,446✔






143



  uint64_t x00 = uu____2 & (uint64_t)0x1111111111111111U;




45,446✔






144



  uint64_t x14 = uu____2 & (uint64_t)0x2222222222222222U;




45,446✔






145



  uint64_t x24 = uu____2 & (uint64_t)0x4444444444444444U;




45,446✔






146



  uint64_t x34 = uu____2 & (uint64_t)0x8888888888888888U;




45,446✔






147



  uint64_t y00 = uu____4 & (uint64_t)0x1111111111111111U;




45,446✔






148



  uint64_t y10 = uu____4 & (uint64_t)0x2222222222222222U;




45,446✔






149



  uint64_t y20 = uu____4 & (uint64_t)0x4444444444444444U;




45,446✔






150



  uint64_t y310 = uu____4 & (uint64_t)0x8888888888888888U;




45,446✔






151



  uint64_t z0 = x00 * y00 ^ (x14 * y310 ^ (x24 * y20 ^ x34 * y10));




45,446✔






152



  uint64_t z10 = x00 * y10 ^ (x14 * y00 ^ (x24 * y310 ^ x34 * y20));




45,446✔






153



  uint64_t z20 = x00 * y20 ^ (x14 * y10 ^ (x24 * y00 ^ x34 * y310));




45,446✔






154



  uint64_t z30 = x00 * y310 ^ (x14 * y20 ^ (x24 * y10 ^ x34 * y00));




45,446✔






155



  uint64_t




45,446✔






156



  z00 =




45,446✔






157



    (((z0 & (uint64_t)0x1111111111111111U) | (z10 & (uint64_t)0x2222222222222222U))




45,446✔






158



    | (z20 & (uint64_t)0x4444444444444444U))




45,446✔






159



    | (z30 & (uint64_t)0x8888888888888888U);




45,446✔






160



  uint64_t x01 = uu____3 & (uint64_t)0x1111111111111111U;




45,446✔






161



  uint64_t x15 = uu____3 & (uint64_t)0x2222222222222222U;




45,446✔






162



  uint64_t x25 = uu____3 & (uint64_t)0x4444444444444444U;




45,446✔






163



  uint64_t x35 = uu____3 & (uint64_t)0x8888888888888888U;




45,446✔






164



  uint64_t y01 = uu____5 & (uint64_t)0x1111111111111111U;




45,446✔






165



  uint64_t y11 = uu____5 & (uint64_t)0x2222222222222222U;




45,446✔






166



  uint64_t y21 = uu____5 & (uint64_t)0x4444444444444444U;




45,446✔






167



  uint64_t y311 = uu____5 & (uint64_t)0x8888888888888888U;




45,446✔






168



  uint64_t z010 = x01 * y01 ^ (x15 * y311 ^ (x25 * y21 ^ x35 * y11));




45,446✔






169



  uint64_t z12 = x01 * y11 ^ (x15 * y01 ^ (x25 * y311 ^ x35 * y21));




45,446✔






170



  uint64_t z22 = x01 * y21 ^ (x15 * y11 ^ (x25 * y01 ^ x35 * y311));




45,446✔






171



  uint64_t z31 = x01 * y311 ^ (x15 * y21 ^ (x25 * y11 ^ x35 * y01));




45,446✔






172



  uint64_t




45,446✔






173



  z13 =




45,446✔






174



    (((z010 & (uint64_t)0x1111111111111111U) | (z12 & (uint64_t)0x2222222222222222U))




45,446✔






175



    | (z22 & (uint64_t)0x4444444444444444U))




45,446✔






176



    | (z31 & (uint64_t)0x8888888888888888U);




45,446✔






177



  uint64_t x02 = y3 & (uint64_t)0x1111111111111111U;




45,446✔






178



  uint64_t x16 = y3 & (uint64_t)0x2222222222222222U;




45,446✔






179



  uint64_t x26 = y3 & (uint64_t)0x4444444444444444U;




45,446✔






180



  uint64_t x36 = y3 & (uint64_t)0x8888888888888888U;




45,446✔






181



  uint64_t y02 = uu____6 & (uint64_t)0x1111111111111111U;




45,446✔






182



  uint64_t y12 = uu____6 & (uint64_t)0x2222222222222222U;




45,446✔






183



  uint64_t y22 = uu____6 & (uint64_t)0x4444444444444444U;




45,446✔






184



  uint64_t y312 = uu____6 & (uint64_t)0x8888888888888888U;




45,446✔






185



  uint64_t z011 = x02 * y02 ^ (x16 * y312 ^ (x26 * y22 ^ x36 * y12));




45,446✔






186



  uint64_t z110 = x02 * y12 ^ (x16 * y02 ^ (x26 * y312 ^ x36 * y22));




45,446✔






187



  uint64_t z23 = x02 * y22 ^ (x16 * y12 ^ (x26 * y02 ^ x36 * y312));




45,446✔






188



  uint64_t z32 = x02 * y312 ^ (x16 * y22 ^ (x26 * y12 ^ x36 * y02));




45,446✔






189



  uint64_t




45,446✔






190



  z24 =




45,446✔






191



    (((z011 & (uint64_t)0x1111111111111111U) | (z110 & (uint64_t)0x2222222222222222U))




45,446✔






192



    | (z23 & (uint64_t)0x4444444444444444U))




45,446✔






193



    | (z32 & (uint64_t)0x8888888888888888U);




45,446✔






194



  uint64_t x03 = y1r & (uint64_t)0x1111111111111111U;




45,446✔






195



  uint64_t x17 = y1r & (uint64_t)0x2222222222222222U;




45,446✔






196



  uint64_t x27 = y1r & (uint64_t)0x4444444444444444U;




45,446✔






197



  uint64_t x37 = y1r & (uint64_t)0x8888888888888888U;




45,446✔






198



  uint64_t y03 = yr1 & (uint64_t)0x1111111111111111U;




45,446✔






199



  uint64_t y13 = yr1 & (uint64_t)0x2222222222222222U;




45,446✔






200



  uint64_t y23 = yr1 & (uint64_t)0x4444444444444444U;




45,446✔






201



  uint64_t y313 = yr1 & (uint64_t)0x8888888888888888U;




45,446✔






202



  uint64_t z012 = x03 * y03 ^ (x17 * y313 ^ (x27 * y23 ^ x37 * y13));




45,446✔






203



  uint64_t z111 = x03 * y13 ^ (x17 * y03 ^ (x27 * y313 ^ x37 * y23));




45,446✔






204



  uint64_t z210 = x03 * y23 ^ (x17 * y13 ^ (x27 * y03 ^ x37 * y313));




45,446✔






205



  uint64_t z33 = x03 * y313 ^ (x17 * y23 ^ (x27 * y13 ^ x37 * y03));




45,446✔






206



  uint64_t




45,446✔






207



  z0h =




45,446✔






208



    (((z012 & (uint64_t)0x1111111111111111U) | (z111 & (uint64_t)0x2222222222222222U))




45,446✔






209



    | (z210 & (uint64_t)0x4444444444444444U))




45,446✔






210



    | (z33 & (uint64_t)0x8888888888888888U);




45,446✔






211



  uint64_t x04 = y2r & (uint64_t)0x1111111111111111U;




45,446✔






212



  uint64_t x18 = y2r & (uint64_t)0x2222222222222222U;




45,446✔






213



  uint64_t x28 = y2r & (uint64_t)0x4444444444444444U;




45,446✔






214



  uint64_t x38 = y2r & (uint64_t)0x8888888888888888U;




45,446✔






215



  uint64_t y04 = yr2 & (uint64_t)0x1111111111111111U;




45,446✔






216



  uint64_t y14 = yr2 & (uint64_t)0x2222222222222222U;




45,446✔






217



  uint64_t y24 = yr2 & (uint64_t)0x4444444444444444U;




45,446✔






218



  uint64_t y314 = yr2 & (uint64_t)0x8888888888888888U;




45,446✔






219



  uint64_t z013 = x04 * y04 ^ (x18 * y314 ^ (x28 * y24 ^ x38 * y14));




45,446✔






220



  uint64_t z112 = x04 * y14 ^ (x18 * y04 ^ (x28 * y314 ^ x38 * y24));




45,446✔






221



  uint64_t z211 = x04 * y24 ^ (x18 * y14 ^ (x28 * y04 ^ x38 * y314));




45,446✔






222



  uint64_t z34 = x04 * y314 ^ (x18 * y24 ^ (x28 * y14 ^ x38 * y04));




45,446✔






223



  uint64_t




45,446✔






224



  z1h =




45,446✔






225



    (((z013 & (uint64_t)0x1111111111111111U) | (z112 & (uint64_t)0x2222222222222222U))




45,446✔






226



    | (z211 & (uint64_t)0x4444444444444444U))




45,446✔






227



    | (z34 & (uint64_t)0x8888888888888888U);




45,446✔






228



  uint64_t x0 = y3r & (uint64_t)0x1111111111111111U;




45,446✔






229



  uint64_t x19 = y3r & (uint64_t)0x2222222222222222U;




45,446✔






230



  uint64_t x29 = y3r & (uint64_t)0x4444444444444444U;




45,446✔






231



  uint64_t x3 = y3r & (uint64_t)0x8888888888888888U;




45,446✔






232



  uint64_t y0 = (yr1 ^ yr2) & (uint64_t)0x1111111111111111U;




45,446✔






233



  uint64_t y1 = (yr1 ^ yr2) & (uint64_t)0x2222222222222222U;




45,446✔






234



  uint64_t y2 = (yr1 ^ yr2) & (uint64_t)0x4444444444444444U;




45,446✔






235



  uint64_t y31 = (yr1 ^ yr2) & (uint64_t)0x8888888888888888U;




45,446✔






236



  uint64_t z01 = x0 * y0 ^ (x19 * y31 ^ (x29 * y2 ^ x3 * y1));




45,446✔






237



  uint64_t z11 = x0 * y1 ^ (x19 * y0 ^ (x29 * y31 ^ x3 * y2));




45,446✔






238



  uint64_t z212 = x0 * y2 ^ (x19 * y1 ^ (x29 * y0 ^ x3 * y31));




45,446✔






239



  uint64_t z35 = x0 * y31 ^ (x19 * y2 ^ (x29 * y1 ^ x3 * y0));




45,446✔






240



  uint64_t




45,446✔






241



  z2h =




45,446✔






242



    (((z01 & (uint64_t)0x1111111111111111U) | (z11 & (uint64_t)0x2222222222222222U))




45,446✔






243



    | (z212 & (uint64_t)0x4444444444444444U))




45,446✔






244



    | (z35 & (uint64_t)0x8888888888888888U);




45,446✔






245



  uint64_t z21 = z24 ^ (z00 ^ z13);




45,446✔






246



  uint64_t z2h1 = z2h ^ (z0h ^ z1h);




45,446✔






247



  uint64_t




45,446✔






248



  x110 =




45,446✔






249



    (z0h & (uint64_t)0x5555555555555555U)




45,446✔






250



    << (uint32_t)(uint8_t)1U




45,446✔






251



    | (z0h >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




45,446✔






252



  uint64_t




45,446✔






253



  x210 =




45,446✔






254



    (x110 & (uint64_t)0x3333333333333333U)




45,446✔






255



    << (uint32_t)(uint8_t)2U




45,446✔






256



    | (x110 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




45,446✔






257



  uint64_t




45,446✔






258



  x39 =




45,446✔






259



    (x210 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




45,446✔






260



    << (uint32_t)(uint8_t)4U




45,446✔






261



    | (x210 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




45,446✔






262



  uint64_t




45,446✔






263



  x43 =




45,446✔






264



    (x39 & (uint64_t)0x00FF00FF00FF00FFU)




45,446✔






265



    << (uint32_t)(uint8_t)8U




45,446✔






266



    | (x39 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




45,446✔






267



  uint64_t




45,446✔






268



  x53 =




45,446✔






269



    (x43 & (uint64_t)0x0000FFFF0000FFFFU)




45,446✔






270



    << (uint32_t)(uint8_t)16U




45,446✔






271



    | (x43 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




45,446✔






272



  uint64_t z0h1 = (x53 << (uint32_t)32U | x53 >> (uint32_t)32U) >> (uint32_t)1U;




45,446✔






273



  uint64_t




45,446✔






274



  x111 =




45,446✔






275



    (z1h & (uint64_t)0x5555555555555555U)




45,446✔






276



    << (uint32_t)(uint8_t)1U




45,446✔






277



    | (z1h >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




45,446✔






278



  uint64_t




45,446✔






279



  x211 =




45,446✔






280



    (x111 & (uint64_t)0x3333333333333333U)




45,446✔






281



    << (uint32_t)(uint8_t)2U




45,446✔






282



    | (x111 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




45,446✔






283



  uint64_t




45,446✔






284



  x310 =




45,446✔






285



    (x211 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




45,446✔






286



    << (uint32_t)(uint8_t)4U




45,446✔






287



    | (x211 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




45,446✔






288



  uint64_t




45,446✔






289



  x44 =




45,446✔






290



    (x310 & (uint64_t)0x00FF00FF00FF00FFU)




45,446✔






291



    << (uint32_t)(uint8_t)8U




45,446✔






292



    | (x310 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




45,446✔






293



  uint64_t




45,446✔






294



  x54 =




45,446✔






295



    (x44 & (uint64_t)0x0000FFFF0000FFFFU)




45,446✔






296



    << (uint32_t)(uint8_t)16U




45,446✔






297



    | (x44 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




45,446✔






298



  uint64_t z1h1 = (x54 << (uint32_t)32U | x54 >> (uint32_t)32U) >> (uint32_t)1U;




45,446✔






299



  uint64_t




45,446✔






300



  x1 =




45,446✔






301



    (z2h1 & (uint64_t)0x5555555555555555U)




45,446✔






302



    << (uint32_t)(uint8_t)1U




45,446✔






303



    | (z2h1 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




45,446✔






304



  uint64_t




45,446✔






305



  x212 =




45,446✔






306



    (x1 & (uint64_t)0x3333333333333333U)




45,446✔






307



    << (uint32_t)(uint8_t)2U




45,446✔






308



    | (x1 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




45,446✔






309



  uint64_t




45,446✔






310



  x311 =




45,446✔






311



    (x212 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




45,446✔






312



    << (uint32_t)(uint8_t)4U




45,446✔






313



    | (x212 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




45,446✔






314



  uint64_t




45,446✔






315



  x45 =




45,446✔






316



    (x311 & (uint64_t)0x00FF00FF00FF00FFU)




45,446✔






317



    << (uint32_t)(uint8_t)8U




45,446✔






318



    | (x311 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




45,446✔






319



  uint64_t




45,446✔






320



  x55 =




45,446✔






321



    (x45 & (uint64_t)0x0000FFFF0000FFFFU)




45,446✔






322



    << (uint32_t)(uint8_t)16U




45,446✔






323



    | (x45 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




45,446✔






324



  uint64_t z2h2 = (x55 << (uint32_t)32U | x55 >> (uint32_t)32U) >> (uint32_t)1U;




45,446✔






325



  uint64_t z1 = z00;




45,446✔






326



  uint64_t z2 = z0h1 ^ z21;




45,446✔






327



  uint64_t z3 = z13 ^ z2h2;




45,446✔






328



  uint64_t z4 = z1h1;




45,446✔






329



  uint64_t v3 = z4 << (uint32_t)1U | z3 >> (uint32_t)63U;




45,446✔






330



  uint64_t v2 = z3 << (uint32_t)1U | z2 >> (uint32_t)63U;




45,446✔






331



  uint64_t v1 = z2 << (uint32_t)1U | z1 >> (uint32_t)63U;




45,446✔






332



  uint64_t v0 = z1 << (uint32_t)1U;




45,446✔






333



  uint64_t v21 = v2 ^ (v0 ^ (v0 >> (uint32_t)1U ^ (v0 >> (uint32_t)2U ^ v0 >> (uint32_t)7U)));




45,446✔






334



  uint64_t v11 = v1 ^ (v0 << (uint32_t)63U ^ (v0 << (uint32_t)62U ^ v0 << (uint32_t)57U));




45,446✔






335



  uint64_t




45,446✔






336



  v31 = v3 ^ (v11 ^ (v11 >> (uint32_t)1U ^ (v11 >> (uint32_t)2U ^ v11 >> (uint32_t)7U)));




45,446✔






337



  uint64_t v22 = v21 ^ (v11 << (uint32_t)63U ^ (v11 << (uint32_t)62U ^ v11 << (uint32_t)57U));




45,446✔






338



  uint64_t x112 = v22;




45,446✔






339



  uint64_t x2 = v31;




45,446✔






340



  x[0U] = x112;




45,446✔






341



  x[1U] = x2;




45,446✔






342



}




45,446✔





343












344



static inline void load_precompute_r(uint64_t *pre, uint8_t *key)











345



{




6,014✔






346



  uint64_t *h1_0 = pre + (uint32_t)6U;




6,014✔






347



  uint64_t *h2_0 = pre + (uint32_t)4U;




6,014✔






348



  uint64_t *h3_0 = pre + (uint32_t)2U;




6,014✔






349



  uint64_t *h4_0 = pre;




6,014✔






350



  uint64_t u = load64_be(key);




6,014✔






351



  h1_0[1U] = u;




6,014✔






352



  uint64_t u0 = load64_be(key + (uint32_t)8U);




6,014✔






353



  h1_0[0U] = u0;




6,014✔






354



  h2_0[0U] = h1_0[0U];




6,014✔






355



  h2_0[1U] = h1_0[1U];




6,014✔






356



  h3_0[0U] = h1_0[0U];




6,014✔






357



  h3_0[1U] = h1_0[1U];




6,014✔






358



  h4_0[0U] = h1_0[0U];




6,014✔






359



  h4_0[1U] = h1_0[1U];




6,014✔






360



  fmul0(h2_0, h1_0);




6,014✔






361



  fmul0(h3_0, h2_0);




6,014✔






362



  fmul0(h4_0, h3_0);




6,014✔






363



  uint64_t uu____0 = h1_0[0U];




6,014✔






364



  uint64_t




6,014✔






365



  x =




6,014✔






366



    (uu____0 & (uint64_t)0x5555555555555555U)




6,014✔






367



    << (uint32_t)(uint8_t)1U




6,014✔






368



    | (uu____0 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




6,014✔






369



  uint64_t




6,014✔






370



  x1 =




6,014✔






371



    (x & (uint64_t)0x3333333333333333U)




6,014✔






372



    << (uint32_t)(uint8_t)2U




6,014✔






373



    | (x >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




6,014✔






374



  uint64_t




6,014✔






375



  x2 =




6,014✔






376



    (x1 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




6,014✔






377



    << (uint32_t)(uint8_t)4U




6,014✔






378



    | (x1 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




6,014✔






379



  uint64_t




6,014✔






380



  x3 =




6,014✔






381



    (x2 & (uint64_t)0x00FF00FF00FF00FFU)




6,014✔






382



    << (uint32_t)(uint8_t)8U




6,014✔






383



    | (x2 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




6,014✔






384



  uint64_t




6,014✔






385



  x4 =




6,014✔






386



    (x3 & (uint64_t)0x0000FFFF0000FFFFU)




6,014✔






387



    << (uint32_t)(uint8_t)16U




6,014✔






388



    | (x3 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




6,014✔






389



  pre[14U] = x4 << (uint32_t)32U | x4 >> (uint32_t)32U;




6,014✔






390



  uint64_t uu____1 = h1_0[1U];




6,014✔






391



  uint64_t




6,014✔






392



  x0 =




6,014✔






393



    (uu____1 & (uint64_t)0x5555555555555555U)




6,014✔






394



    << (uint32_t)(uint8_t)1U




6,014✔






395



    | (uu____1 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




6,014✔






396



  uint64_t




6,014✔






397



  x10 =




6,014✔






398



    (x0 & (uint64_t)0x3333333333333333U)




6,014✔






399



    << (uint32_t)(uint8_t)2U




6,014✔






400



    | (x0 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




6,014✔






401



  uint64_t




6,014✔






402



  x20 =




6,014✔






403



    (x10 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




6,014✔






404



    << (uint32_t)(uint8_t)4U




6,014✔






405



    | (x10 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




6,014✔






406



  uint64_t




6,014✔






407



  x30 =




6,014✔






408



    (x20 & (uint64_t)0x00FF00FF00FF00FFU)




6,014✔






409



    << (uint32_t)(uint8_t)8U




6,014✔






410



    | (x20 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




6,014✔






411



  uint64_t




6,014✔






412



  x40 =




6,014✔






413



    (x30 & (uint64_t)0x0000FFFF0000FFFFU)




6,014✔






414



    << (uint32_t)(uint8_t)16U




6,014✔






415



    | (x30 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




6,014✔






416



  pre[15U] = x40 << (uint32_t)32U | x40 >> (uint32_t)32U;




6,014✔






417



  uint64_t uu____2 = h2_0[0U];




6,014✔






418



  uint64_t




6,014✔






419



  x5 =




6,014✔






420



    (uu____2 & (uint64_t)0x5555555555555555U)




6,014✔






421



    << (uint32_t)(uint8_t)1U




6,014✔






422



    | (uu____2 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




6,014✔






423



  uint64_t




6,014✔






424



  x11 =




6,014✔






425



    (x5 & (uint64_t)0x3333333333333333U)




6,014✔






426



    << (uint32_t)(uint8_t)2U




6,014✔






427



    | (x5 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




6,014✔






428



  uint64_t




6,014✔






429



  x21 =




6,014✔






430



    (x11 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




6,014✔






431



    << (uint32_t)(uint8_t)4U




6,014✔






432



    | (x11 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




6,014✔






433



  uint64_t




6,014✔






434



  x31 =




6,014✔






435



    (x21 & (uint64_t)0x00FF00FF00FF00FFU)




6,014✔






436



    << (uint32_t)(uint8_t)8U




6,014✔






437



    | (x21 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




6,014✔






438



  uint64_t




6,014✔






439



  x41 =




6,014✔






440



    (x31 & (uint64_t)0x0000FFFF0000FFFFU)




6,014✔






441



    << (uint32_t)(uint8_t)16U




6,014✔






442



    | (x31 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




6,014✔






443



  pre[12U] = x41 << (uint32_t)32U | x41 >> (uint32_t)32U;




6,014✔






444



  uint64_t uu____3 = h2_0[1U];




6,014✔






445



  uint64_t




6,014✔






446



  x6 =




6,014✔






447



    (uu____3 & (uint64_t)0x5555555555555555U)




6,014✔






448



    << (uint32_t)(uint8_t)1U




6,014✔






449



    | (uu____3 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




6,014✔






450



  uint64_t




6,014✔






451



  x12 =




6,014✔






452



    (x6 & (uint64_t)0x3333333333333333U)




6,014✔






453



    << (uint32_t)(uint8_t)2U




6,014✔






454



    | (x6 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




6,014✔






455



  uint64_t




6,014✔






456



  x22 =




6,014✔






457



    (x12 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




6,014✔






458



    << (uint32_t)(uint8_t)4U




6,014✔






459



    | (x12 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




6,014✔






460



  uint64_t




6,014✔






461



  x32 =




6,014✔






462



    (x22 & (uint64_t)0x00FF00FF00FF00FFU)




6,014✔






463



    << (uint32_t)(uint8_t)8U




6,014✔






464



    | (x22 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




6,014✔






465



  uint64_t




6,014✔






466



  x42 =




6,014✔






467



    (x32 & (uint64_t)0x0000FFFF0000FFFFU)




6,014✔






468



    << (uint32_t)(uint8_t)16U




6,014✔






469



    | (x32 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




6,014✔






470



  pre[13U] = x42 << (uint32_t)32U | x42 >> (uint32_t)32U;




6,014✔






471



  uint64_t uu____4 = h3_0[0U];




6,014✔






472



  uint64_t




6,014✔






473



  x7 =




6,014✔






474



    (uu____4 & (uint64_t)0x5555555555555555U)




6,014✔






475



    << (uint32_t)(uint8_t)1U




6,014✔






476



    | (uu____4 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




6,014✔






477



  uint64_t




6,014✔






478



  x13 =




6,014✔






479



    (x7 & (uint64_t)0x3333333333333333U)




6,014✔






480



    << (uint32_t)(uint8_t)2U




6,014✔






481



    | (x7 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




6,014✔






482



  uint64_t




6,014✔






483



  x23 =




6,014✔






484



    (x13 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




6,014✔






485



    << (uint32_t)(uint8_t)4U




6,014✔






486



    | (x13 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




6,014✔






487



  uint64_t




6,014✔






488



  x33 =




6,014✔






489



    (x23 & (uint64_t)0x00FF00FF00FF00FFU)




6,014✔






490



    << (uint32_t)(uint8_t)8U




6,014✔






491



    | (x23 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




6,014✔






492



  uint64_t




6,014✔






493



  x43 =




6,014✔






494



    (x33 & (uint64_t)0x0000FFFF0000FFFFU)




6,014✔






495



    << (uint32_t)(uint8_t)16U




6,014✔






496



    | (x33 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




6,014✔






497



  pre[10U] = x43 << (uint32_t)32U | x43 >> (uint32_t)32U;




6,014✔






498



  uint64_t uu____5 = h3_0[1U];




6,014✔






499



  uint64_t




6,014✔






500



  x8 =




6,014✔






501



    (uu____5 & (uint64_t)0x5555555555555555U)




6,014✔






502



    << (uint32_t)(uint8_t)1U




6,014✔






503



    | (uu____5 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




6,014✔






504



  uint64_t




6,014✔






505



  x14 =




6,014✔






506



    (x8 & (uint64_t)0x3333333333333333U)




6,014✔






507



    << (uint32_t)(uint8_t)2U




6,014✔






508



    | (x8 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




6,014✔






509



  uint64_t




6,014✔






510



  x24 =




6,014✔






511



    (x14 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




6,014✔






512



    << (uint32_t)(uint8_t)4U




6,014✔






513



    | (x14 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




6,014✔






514



  uint64_t




6,014✔






515



  x34 =




6,014✔






516



    (x24 & (uint64_t)0x00FF00FF00FF00FFU)




6,014✔






517



    << (uint32_t)(uint8_t)8U




6,014✔






518



    | (x24 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




6,014✔






519



  uint64_t




6,014✔






520



  x44 =




6,014✔






521



    (x34 & (uint64_t)0x0000FFFF0000FFFFU)




6,014✔






522



    << (uint32_t)(uint8_t)16U




6,014✔






523



    | (x34 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




6,014✔






524



  pre[11U] = x44 << (uint32_t)32U | x44 >> (uint32_t)32U;




6,014✔






525



  uint64_t uu____6 = h4_0[0U];




6,014✔






526



  uint64_t




6,014✔






527



  x9 =




6,014✔






528



    (uu____6 & (uint64_t)0x5555555555555555U)




6,014✔






529



    << (uint32_t)(uint8_t)1U




6,014✔






530



    | (uu____6 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




6,014✔






531



  uint64_t




6,014✔






532



  x15 =




6,014✔






533



    (x9 & (uint64_t)0x3333333333333333U)




6,014✔






534



    << (uint32_t)(uint8_t)2U




6,014✔






535



    | (x9 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




6,014✔






536



  uint64_t




6,014✔






537



  x25 =




6,014✔






538



    (x15 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




6,014✔






539



    << (uint32_t)(uint8_t)4U




6,014✔






540



    | (x15 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




6,014✔






541



  uint64_t




6,014✔






542



  x35 =




6,014✔






543



    (x25 & (uint64_t)0x00FF00FF00FF00FFU)




6,014✔






544



    << (uint32_t)(uint8_t)8U




6,014✔






545



    | (x25 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




6,014✔






546



  uint64_t




6,014✔






547



  x45 =




6,014✔






548



    (x35 & (uint64_t)0x0000FFFF0000FFFFU)




6,014✔






549



    << (uint32_t)(uint8_t)16U




6,014✔






550



    | (x35 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




6,014✔






551



  pre[8U] = x45 << (uint32_t)32U | x45 >> (uint32_t)32U;




6,014✔






552



  uint64_t uu____7 = h4_0[1U];




6,014✔






553



  uint64_t




6,014✔






554



  x16 =




6,014✔






555



    (uu____7 & (uint64_t)0x5555555555555555U)




6,014✔






556



    << (uint32_t)(uint8_t)1U




6,014✔






557



    | (uu____7 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




6,014✔






558



  uint64_t




6,014✔






559



  x17 =




6,014✔






560



    (x16 & (uint64_t)0x3333333333333333U)




6,014✔






561



    << (uint32_t)(uint8_t)2U




6,014✔






562



    | (x16 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




6,014✔






563



  uint64_t




6,014✔






564



  x26 =




6,014✔






565



    (x17 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




6,014✔






566



    << (uint32_t)(uint8_t)4U




6,014✔






567



    | (x17 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




6,014✔






568



  uint64_t




6,014✔






569



  x36 =




6,014✔






570



    (x26 & (uint64_t)0x00FF00FF00FF00FFU)




6,014✔






571



    << (uint32_t)(uint8_t)8U




6,014✔






572



    | (x26 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




6,014✔






573



  uint64_t




6,014✔






574



  x46 =




6,014✔






575



    (x36 & (uint64_t)0x0000FFFF0000FFFFU)




6,014✔






576



    << (uint32_t)(uint8_t)16U




6,014✔






577



    | (x36 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




6,014✔






578



  pre[9U] = x46 << (uint32_t)32U | x46 >> (uint32_t)32U;




6,014✔






579



}




6,014✔





580












581



static inline void normalize4(uint64_t *acc, uint64_t *x, uint64_t *pre)











582



{




3,472✔






583



  uint64_t *x1 = x;




3,472✔






584



  uint64_t *x2 = x + (uint32_t)2U;




3,472✔






585



  uint64_t *x3 = x + (uint32_t)4U;




3,472✔






586



  uint64_t *x4 = x + (uint32_t)6U;




3,472✔






587



  uint64_t *y1 = pre;




3,472✔






588



  uint64_t *y2 = pre + (uint32_t)2U;




3,472✔






589



  uint64_t *y3 = pre + (uint32_t)4U;




3,472✔






590



  uint64_t *y4 = pre + (uint32_t)6U;




3,472✔






591



  uint64_t *yr1 = pre + (uint32_t)8U;




3,472✔






592



  uint64_t *yr2 = pre + (uint32_t)10U;




3,472✔






593



  uint64_t *yr3 = pre + (uint32_t)12U;




3,472✔






594



  uint64_t *yr4 = pre + (uint32_t)14U;




3,472✔






595



  uint64_t uu____0 = x1[0U];




3,472✔






596



  uint64_t uu____1 = x1[1U];




3,472✔






597



  uint64_t uu____2 = y1[0U];




3,472✔






598



  uint64_t uu____3 = y1[1U];




3,472✔






599



  uint64_t uu____4 = y1[0U] ^ y1[1U];




3,472✔






600



  uint64_t uu____5 = yr1[0U];




3,472✔






601



  uint64_t uu____6 = yr1[1U];




3,472✔






602



  uint64_t uu____7 = yr1[0U] ^ yr1[1U];




3,472✔






603



  uint64_t




3,472✔






604



  x50 =




3,472✔






605



    (uu____0 & (uint64_t)0x5555555555555555U)




3,472✔






606



    << (uint32_t)(uint8_t)1U




3,472✔






607



    | (uu____0 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






608



  uint64_t




3,472✔






609



  x6 =




3,472✔






610



    (x50 & (uint64_t)0x3333333333333333U)




3,472✔






611



    << (uint32_t)(uint8_t)2U




3,472✔






612



    | (x50 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






613



  uint64_t




3,472✔






614



  x7 =




3,472✔






615



    (x6 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






616



    << (uint32_t)(uint8_t)4U




3,472✔






617



    | (x6 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






618



  uint64_t




3,472✔






619



  x8 =




3,472✔






620



    (x7 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






621



    << (uint32_t)(uint8_t)8U




3,472✔






622



    | (x7 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






623



  uint64_t




3,472✔






624



  x9 =




3,472✔






625



    (x8 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






626



    << (uint32_t)(uint8_t)16U




3,472✔






627



    | (x8 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






628



  uint64_t y1r = x9 << (uint32_t)32U | x9 >> (uint32_t)32U;




3,472✔






629



  uint64_t




3,472✔






630



  x51 =




3,472✔






631



    (uu____1 & (uint64_t)0x5555555555555555U)




3,472✔






632



    << (uint32_t)(uint8_t)1U




3,472✔






633



    | (uu____1 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






634



  uint64_t




3,472✔






635



  x60 =




3,472✔






636



    (x51 & (uint64_t)0x3333333333333333U)




3,472✔






637



    << (uint32_t)(uint8_t)2U




3,472✔






638



    | (x51 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






639



  uint64_t




3,472✔






640



  x70 =




3,472✔






641



    (x60 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






642



    << (uint32_t)(uint8_t)4U




3,472✔






643



    | (x60 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






644



  uint64_t




3,472✔






645



  x80 =




3,472✔






646



    (x70 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






647



    << (uint32_t)(uint8_t)8U




3,472✔






648



    | (x70 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






649



  uint64_t




3,472✔






650



  x90 =




3,472✔






651



    (x80 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






652



    << (uint32_t)(uint8_t)16U




3,472✔






653



    | (x80 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






654



  uint64_t y2r = x90 << (uint32_t)32U | x90 >> (uint32_t)32U;




3,472✔






655



  uint64_t y310 = uu____0 ^ uu____1;




3,472✔






656



  uint64_t y3r0 = y1r ^ y2r;




3,472✔






657



  uint64_t x00 = uu____0 & (uint64_t)0x1111111111111111U;




3,472✔






658



  uint64_t x110 = uu____0 & (uint64_t)0x2222222222222222U;




3,472✔






659



  uint64_t x210 = uu____0 & (uint64_t)0x4444444444444444U;




3,472✔






660



  uint64_t x310 = uu____0 & (uint64_t)0x8888888888888888U;




3,472✔






661



  uint64_t y00 = uu____2 & (uint64_t)0x1111111111111111U;




3,472✔






662



  uint64_t y110 = uu____2 & (uint64_t)0x2222222222222222U;




3,472✔






663



  uint64_t y210 = uu____2 & (uint64_t)0x4444444444444444U;




3,472✔






664



  uint64_t y320 = uu____2 & (uint64_t)0x8888888888888888U;




3,472✔






665



  uint64_t z00 = x00 * y00 ^ (x110 * y320 ^ (x210 * y210 ^ x310 * y110));




3,472✔






666



  uint64_t z10 = x00 * y110 ^ (x110 * y00 ^ (x210 * y320 ^ x310 * y210));




3,472✔






667



  uint64_t z20 = x00 * y210 ^ (x110 * y110 ^ (x210 * y00 ^ x310 * y320));




3,472✔






668



  uint64_t z30 = x00 * y320 ^ (x110 * y210 ^ (x210 * y110 ^ x310 * y00));




3,472✔






669



  uint64_t




3,472✔






670



  z02 =




3,472✔






671



    (((z00 & (uint64_t)0x1111111111111111U) | (z10 & (uint64_t)0x2222222222222222U))




3,472✔






672



    | (z20 & (uint64_t)0x4444444444444444U))




3,472✔






673



    | (z30 & (uint64_t)0x8888888888888888U);




3,472✔






674



  uint64_t x01 = uu____1 & (uint64_t)0x1111111111111111U;




3,472✔






675



  uint64_t x111 = uu____1 & (uint64_t)0x2222222222222222U;




3,472✔






676



  uint64_t x211 = uu____1 & (uint64_t)0x4444444444444444U;




3,472✔






677



  uint64_t x311 = uu____1 & (uint64_t)0x8888888888888888U;




3,472✔






678



  uint64_t y01 = uu____3 & (uint64_t)0x1111111111111111U;




3,472✔






679



  uint64_t y111 = uu____3 & (uint64_t)0x2222222222222222U;




3,472✔






680



  uint64_t y211 = uu____3 & (uint64_t)0x4444444444444444U;




3,472✔






681



  uint64_t y321 = uu____3 & (uint64_t)0x8888888888888888U;




3,472✔






682



  uint64_t z010 = x01 * y01 ^ (x111 * y321 ^ (x211 * y211 ^ x311 * y111));




3,472✔






683



  uint64_t z14 = x01 * y111 ^ (x111 * y01 ^ (x211 * y321 ^ x311 * y211));




3,472✔






684



  uint64_t z24 = x01 * y211 ^ (x111 * y111 ^ (x211 * y01 ^ x311 * y321));




3,472✔






685



  uint64_t z33 = x01 * y321 ^ (x111 * y211 ^ (x211 * y111 ^ x311 * y01));




3,472✔






686



  uint64_t




3,472✔






687



  z15 =




3,472✔






688



    (((z010 & (uint64_t)0x1111111111111111U) | (z14 & (uint64_t)0x2222222222222222U))




3,472✔






689



    | (z24 & (uint64_t)0x4444444444444444U))




3,472✔






690



    | (z33 & (uint64_t)0x8888888888888888U);




3,472✔






691



  uint64_t x02 = y310 & (uint64_t)0x1111111111111111U;




3,472✔






692



  uint64_t x112 = y310 & (uint64_t)0x2222222222222222U;




3,472✔






693



  uint64_t x212 = y310 & (uint64_t)0x4444444444444444U;




3,472✔






694



  uint64_t x312 = y310 & (uint64_t)0x8888888888888888U;




3,472✔






695



  uint64_t y02 = uu____4 & (uint64_t)0x1111111111111111U;




3,472✔






696



  uint64_t y112 = uu____4 & (uint64_t)0x2222222222222222U;




3,472✔






697



  uint64_t y212 = uu____4 & (uint64_t)0x4444444444444444U;




3,472✔






698



  uint64_t y322 = uu____4 & (uint64_t)0x8888888888888888U;




3,472✔






699



  uint64_t z011 = x02 * y02 ^ (x112 * y322 ^ (x212 * y212 ^ x312 * y112));




3,472✔






700



  uint64_t z110 = x02 * y112 ^ (x112 * y02 ^ (x212 * y322 ^ x312 * y212));




3,472✔






701



  uint64_t z25 = x02 * y212 ^ (x112 * y112 ^ (x212 * y02 ^ x312 * y322));




3,472✔






702



  uint64_t z34 = x02 * y322 ^ (x112 * y212 ^ (x212 * y112 ^ x312 * y02));




3,472✔






703



  uint64_t




3,472✔






704



  z26 =




3,472✔






705



    (((z011 & (uint64_t)0x1111111111111111U) | (z110 & (uint64_t)0x2222222222222222U))




3,472✔






706



    | (z25 & (uint64_t)0x4444444444444444U))




3,472✔






707



    | (z34 & (uint64_t)0x8888888888888888U);




3,472✔






708



  uint64_t x03 = y1r & (uint64_t)0x1111111111111111U;




3,472✔






709



  uint64_t x113 = y1r & (uint64_t)0x2222222222222222U;




3,472✔






710



  uint64_t x213 = y1r & (uint64_t)0x4444444444444444U;




3,472✔






711



  uint64_t x313 = y1r & (uint64_t)0x8888888888888888U;




3,472✔






712



  uint64_t y03 = uu____5 & (uint64_t)0x1111111111111111U;




3,472✔






713



  uint64_t y113 = uu____5 & (uint64_t)0x2222222222222222U;




3,472✔






714



  uint64_t y213 = uu____5 & (uint64_t)0x4444444444444444U;




3,472✔






715



  uint64_t y323 = uu____5 & (uint64_t)0x8888888888888888U;




3,472✔






716



  uint64_t z012 = x03 * y03 ^ (x113 * y323 ^ (x213 * y213 ^ x313 * y113));




3,472✔






717



  uint64_t z111 = x03 * y113 ^ (x113 * y03 ^ (x213 * y323 ^ x313 * y213));




3,472✔






718



  uint64_t z210 = x03 * y213 ^ (x113 * y113 ^ (x213 * y03 ^ x313 * y323));




3,472✔






719



  uint64_t z35 = x03 * y323 ^ (x113 * y213 ^ (x213 * y113 ^ x313 * y03));




3,472✔






720



  uint64_t




3,472✔






721



  z0h =




3,472✔






722



    (((z012 & (uint64_t)0x1111111111111111U) | (z111 & (uint64_t)0x2222222222222222U))




3,472✔






723



    | (z210 & (uint64_t)0x4444444444444444U))




3,472✔






724



    | (z35 & (uint64_t)0x8888888888888888U);




3,472✔






725



  uint64_t x04 = y2r & (uint64_t)0x1111111111111111U;




3,472✔






726



  uint64_t x114 = y2r & (uint64_t)0x2222222222222222U;




3,472✔






727



  uint64_t x214 = y2r & (uint64_t)0x4444444444444444U;




3,472✔






728



  uint64_t x314 = y2r & (uint64_t)0x8888888888888888U;




3,472✔






729



  uint64_t y04 = uu____6 & (uint64_t)0x1111111111111111U;




3,472✔






730



  uint64_t y114 = uu____6 & (uint64_t)0x2222222222222222U;




3,472✔






731



  uint64_t y214 = uu____6 & (uint64_t)0x4444444444444444U;




3,472✔






732



  uint64_t y324 = uu____6 & (uint64_t)0x8888888888888888U;




3,472✔






733



  uint64_t z013 = x04 * y04 ^ (x114 * y324 ^ (x214 * y214 ^ x314 * y114));




3,472✔






734



  uint64_t z112 = x04 * y114 ^ (x114 * y04 ^ (x214 * y324 ^ x314 * y214));




3,472✔






735



  uint64_t z211 = x04 * y214 ^ (x114 * y114 ^ (x214 * y04 ^ x314 * y324));




3,472✔






736



  uint64_t z36 = x04 * y324 ^ (x114 * y214 ^ (x214 * y114 ^ x314 * y04));




3,472✔






737



  uint64_t




3,472✔






738



  z1h =




3,472✔






739



    (((z013 & (uint64_t)0x1111111111111111U) | (z112 & (uint64_t)0x2222222222222222U))




3,472✔






740



    | (z211 & (uint64_t)0x4444444444444444U))




3,472✔






741



    | (z36 & (uint64_t)0x8888888888888888U);




3,472✔






742



  uint64_t x05 = y3r0 & (uint64_t)0x1111111111111111U;




3,472✔






743



  uint64_t x115 = y3r0 & (uint64_t)0x2222222222222222U;




3,472✔






744



  uint64_t x215 = y3r0 & (uint64_t)0x4444444444444444U;




3,472✔






745



  uint64_t x315 = y3r0 & (uint64_t)0x8888888888888888U;




3,472✔






746



  uint64_t y05 = uu____7 & (uint64_t)0x1111111111111111U;




3,472✔






747



  uint64_t y115 = uu____7 & (uint64_t)0x2222222222222222U;




3,472✔






748



  uint64_t y215 = uu____7 & (uint64_t)0x4444444444444444U;




3,472✔






749



  uint64_t y325 = uu____7 & (uint64_t)0x8888888888888888U;




3,472✔






750



  uint64_t z014 = x05 * y05 ^ (x115 * y325 ^ (x215 * y215 ^ x315 * y115));




3,472✔






751



  uint64_t z113 = x05 * y115 ^ (x115 * y05 ^ (x215 * y325 ^ x315 * y215));




3,472✔






752



  uint64_t z212 = x05 * y215 ^ (x115 * y115 ^ (x215 * y05 ^ x315 * y325));




3,472✔






753



  uint64_t z37 = x05 * y325 ^ (x115 * y215 ^ (x215 * y115 ^ x315 * y05));




3,472✔






754



  uint64_t




3,472✔






755



  z2h =




3,472✔






756



    (((z014 & (uint64_t)0x1111111111111111U) | (z113 & (uint64_t)0x2222222222222222U))




3,472✔






757



    | (z212 & (uint64_t)0x4444444444444444U))




3,472✔






758



    | (z37 & (uint64_t)0x8888888888888888U);




3,472✔






759



  uint64_t z213 = z26 ^ (z02 ^ z15);




3,472✔






760



  uint64_t z2h10 = z2h ^ (z0h ^ z1h);




3,472✔






761



  uint64_t




3,472✔






762



  x52 =




3,472✔






763



    (z0h & (uint64_t)0x5555555555555555U)




3,472✔






764



    << (uint32_t)(uint8_t)1U




3,472✔






765



    | (z0h >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






766



  uint64_t




3,472✔






767



  x61 =




3,472✔






768



    (x52 & (uint64_t)0x3333333333333333U)




3,472✔






769



    << (uint32_t)(uint8_t)2U




3,472✔






770



    | (x52 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






771



  uint64_t




3,472✔






772



  x71 =




3,472✔






773



    (x61 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






774



    << (uint32_t)(uint8_t)4U




3,472✔






775



    | (x61 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






776



  uint64_t




3,472✔






777



  x81 =




3,472✔






778



    (x71 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






779



    << (uint32_t)(uint8_t)8U




3,472✔






780



    | (x71 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






781



  uint64_t




3,472✔






782



  x91 =




3,472✔






783



    (x81 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






784



    << (uint32_t)(uint8_t)16U




3,472✔






785



    | (x81 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






786



  uint64_t z0h1 = (x91 << (uint32_t)32U | x91 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






787



  uint64_t




3,472✔






788



  x53 =




3,472✔






789



    (z1h & (uint64_t)0x5555555555555555U)




3,472✔






790



    << (uint32_t)(uint8_t)1U




3,472✔






791



    | (z1h >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






792



  uint64_t




3,472✔






793



  x62 =




3,472✔






794



    (x53 & (uint64_t)0x3333333333333333U)




3,472✔






795



    << (uint32_t)(uint8_t)2U




3,472✔






796



    | (x53 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






797



  uint64_t




3,472✔






798



  x72 =




3,472✔






799



    (x62 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






800



    << (uint32_t)(uint8_t)4U




3,472✔






801



    | (x62 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






802



  uint64_t




3,472✔






803



  x82 =




3,472✔






804



    (x72 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






805



    << (uint32_t)(uint8_t)8U




3,472✔






806



    | (x72 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






807



  uint64_t




3,472✔






808



  x92 =




3,472✔






809



    (x82 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






810



    << (uint32_t)(uint8_t)16U




3,472✔






811



    | (x82 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






812



  uint64_t z1h1 = (x92 << (uint32_t)32U | x92 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






813



  uint64_t




3,472✔






814



  x54 =




3,472✔






815



    (z2h10 & (uint64_t)0x5555555555555555U)




3,472✔






816



    << (uint32_t)(uint8_t)1U




3,472✔






817



    | (z2h10 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






818



  uint64_t




3,472✔






819



  x63 =




3,472✔






820



    (x54 & (uint64_t)0x3333333333333333U)




3,472✔






821



    << (uint32_t)(uint8_t)2U




3,472✔






822



    | (x54 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






823



  uint64_t




3,472✔






824



  x73 =




3,472✔






825



    (x63 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






826



    << (uint32_t)(uint8_t)4U




3,472✔






827



    | (x63 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






828



  uint64_t




3,472✔






829



  x83 =




3,472✔






830



    (x73 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






831



    << (uint32_t)(uint8_t)8U




3,472✔






832



    | (x73 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






833



  uint64_t




3,472✔






834



  x93 =




3,472✔






835



    (x83 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






836



    << (uint32_t)(uint8_t)16U




3,472✔






837



    | (x83 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






838



  uint64_t z2h2 = (x93 << (uint32_t)32U | x93 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






839



  uint64_t z1_1 = z02;




3,472✔






840



  uint64_t z1_2 = z0h1 ^ z213;




3,472✔






841



  uint64_t z1_3 = z15 ^ z2h2;




3,472✔






842



  uint64_t z1_4 = z1h1;




3,472✔






843



  uint64_t uu____8 = x2[0U];




3,472✔






844



  uint64_t uu____9 = x2[1U];




3,472✔






845



  uint64_t uu____10 = y2[0U];




3,472✔






846



  uint64_t uu____11 = y2[1U];




3,472✔






847



  uint64_t uu____12 = y2[0U] ^ y2[1U];




3,472✔






848



  uint64_t uu____13 = yr2[0U];




3,472✔






849



  uint64_t uu____14 = yr2[1U];




3,472✔






850



  uint64_t uu____15 = yr2[0U] ^ yr2[1U];




3,472✔






851



  uint64_t




3,472✔






852



  x55 =




3,472✔






853



    (uu____8 & (uint64_t)0x5555555555555555U)




3,472✔






854



    << (uint32_t)(uint8_t)1U




3,472✔






855



    | (uu____8 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






856



  uint64_t




3,472✔






857



  x64 =




3,472✔






858



    (x55 & (uint64_t)0x3333333333333333U)




3,472✔






859



    << (uint32_t)(uint8_t)2U




3,472✔






860



    | (x55 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






861



  uint64_t




3,472✔






862



  x74 =




3,472✔






863



    (x64 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






864



    << (uint32_t)(uint8_t)4U




3,472✔






865



    | (x64 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






866



  uint64_t




3,472✔






867



  x84 =




3,472✔






868



    (x74 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






869



    << (uint32_t)(uint8_t)8U




3,472✔






870



    | (x74 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






871



  uint64_t




3,472✔






872



  x94 =




3,472✔






873



    (x84 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






874



    << (uint32_t)(uint8_t)16U




3,472✔






875



    | (x84 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






876



  uint64_t y1r0 = x94 << (uint32_t)32U | x94 >> (uint32_t)32U;




3,472✔






877



  uint64_t




3,472✔






878



  x56 =




3,472✔






879



    (uu____9 & (uint64_t)0x5555555555555555U)




3,472✔






880



    << (uint32_t)(uint8_t)1U




3,472✔






881



    | (uu____9 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






882



  uint64_t




3,472✔






883



  x65 =




3,472✔






884



    (x56 & (uint64_t)0x3333333333333333U)




3,472✔






885



    << (uint32_t)(uint8_t)2U




3,472✔






886



    | (x56 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






887



  uint64_t




3,472✔






888



  x75 =




3,472✔






889



    (x65 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






890



    << (uint32_t)(uint8_t)4U




3,472✔






891



    | (x65 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






892



  uint64_t




3,472✔






893



  x85 =




3,472✔






894



    (x75 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






895



    << (uint32_t)(uint8_t)8U




3,472✔






896



    | (x75 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






897



  uint64_t




3,472✔






898



  x95 =




3,472✔






899



    (x85 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






900



    << (uint32_t)(uint8_t)16U




3,472✔






901



    | (x85 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






902



  uint64_t y2r0 = x95 << (uint32_t)32U | x95 >> (uint32_t)32U;




3,472✔






903



  uint64_t y311 = uu____8 ^ uu____9;




3,472✔






904



  uint64_t y3r1 = y1r0 ^ y2r0;




3,472✔






905



  uint64_t x06 = uu____8 & (uint64_t)0x1111111111111111U;




3,472✔






906



  uint64_t x116 = uu____8 & (uint64_t)0x2222222222222222U;




3,472✔






907



  uint64_t x216 = uu____8 & (uint64_t)0x4444444444444444U;




3,472✔






908



  uint64_t x316 = uu____8 & (uint64_t)0x8888888888888888U;




3,472✔






909



  uint64_t y06 = uu____10 & (uint64_t)0x1111111111111111U;




3,472✔






910



  uint64_t y116 = uu____10 & (uint64_t)0x2222222222222222U;




3,472✔






911



  uint64_t y216 = uu____10 & (uint64_t)0x4444444444444444U;




3,472✔






912



  uint64_t y326 = uu____10 & (uint64_t)0x8888888888888888U;




3,472✔






913



  uint64_t z03 = x06 * y06 ^ (x116 * y326 ^ (x216 * y216 ^ x316 * y116));




3,472✔






914



  uint64_t z16 = x06 * y116 ^ (x116 * y06 ^ (x216 * y326 ^ x316 * y216));




3,472✔






915



  uint64_t z27 = x06 * y216 ^ (x116 * y116 ^ (x216 * y06 ^ x316 * y326));




3,472✔






916



  uint64_t z38 = x06 * y326 ^ (x116 * y216 ^ (x216 * y116 ^ x316 * y06));




3,472✔






917



  uint64_t




3,472✔






918



  z04 =




3,472✔






919



    (((z03 & (uint64_t)0x1111111111111111U) | (z16 & (uint64_t)0x2222222222222222U))




3,472✔






920



    | (z27 & (uint64_t)0x4444444444444444U))




3,472✔






921



    | (z38 & (uint64_t)0x8888888888888888U);




3,472✔






922



  uint64_t x07 = uu____9 & (uint64_t)0x1111111111111111U;




3,472✔






923



  uint64_t x117 = uu____9 & (uint64_t)0x2222222222222222U;




3,472✔






924



  uint64_t x217 = uu____9 & (uint64_t)0x4444444444444444U;




3,472✔






925



  uint64_t x317 = uu____9 & (uint64_t)0x8888888888888888U;




3,472✔






926



  uint64_t y07 = uu____11 & (uint64_t)0x1111111111111111U;




3,472✔






927



  uint64_t y117 = uu____11 & (uint64_t)0x2222222222222222U;




3,472✔






928



  uint64_t y217 = uu____11 & (uint64_t)0x4444444444444444U;




3,472✔






929



  uint64_t y327 = uu____11 & (uint64_t)0x8888888888888888U;




3,472✔






930



  uint64_t z015 = x07 * y07 ^ (x117 * y327 ^ (x217 * y217 ^ x317 * y117));




3,472✔






931



  uint64_t z17 = x07 * y117 ^ (x117 * y07 ^ (x217 * y327 ^ x317 * y217));




3,472✔






932



  uint64_t z28 = x07 * y217 ^ (x117 * y117 ^ (x217 * y07 ^ x317 * y327));




3,472✔






933



  uint64_t z39 = x07 * y327 ^ (x117 * y217 ^ (x217 * y117 ^ x317 * y07));




3,472✔






934



  uint64_t




3,472✔






935



  z18 =




3,472✔






936



    (((z015 & (uint64_t)0x1111111111111111U) | (z17 & (uint64_t)0x2222222222222222U))




3,472✔






937



    | (z28 & (uint64_t)0x4444444444444444U))




3,472✔






938



    | (z39 & (uint64_t)0x8888888888888888U);




3,472✔






939



  uint64_t x08 = y311 & (uint64_t)0x1111111111111111U;




3,472✔






940



  uint64_t x118 = y311 & (uint64_t)0x2222222222222222U;




3,472✔






941



  uint64_t x218 = y311 & (uint64_t)0x4444444444444444U;




3,472✔






942



  uint64_t x318 = y311 & (uint64_t)0x8888888888888888U;




3,472✔






943



  uint64_t y08 = uu____12 & (uint64_t)0x1111111111111111U;




3,472✔






944



  uint64_t y118 = uu____12 & (uint64_t)0x2222222222222222U;




3,472✔






945



  uint64_t y218 = uu____12 & (uint64_t)0x4444444444444444U;




3,472✔






946



  uint64_t y328 = uu____12 & (uint64_t)0x8888888888888888U;




3,472✔






947



  uint64_t z016 = x08 * y08 ^ (x118 * y328 ^ (x218 * y218 ^ x318 * y118));




3,472✔






948



  uint64_t z114 = x08 * y118 ^ (x118 * y08 ^ (x218 * y328 ^ x318 * y218));




3,472✔






949



  uint64_t z29 = x08 * y218 ^ (x118 * y118 ^ (x218 * y08 ^ x318 * y328));




3,472✔






950



  uint64_t z310 = x08 * y328 ^ (x118 * y218 ^ (x218 * y118 ^ x318 * y08));




3,472✔






951



  uint64_t




3,472✔






952



  z214 =




3,472✔






953



    (((z016 & (uint64_t)0x1111111111111111U) | (z114 & (uint64_t)0x2222222222222222U))




3,472✔






954



    | (z29 & (uint64_t)0x4444444444444444U))




3,472✔






955



    | (z310 & (uint64_t)0x8888888888888888U);




3,472✔






956



  uint64_t x09 = y1r0 & (uint64_t)0x1111111111111111U;




3,472✔






957



  uint64_t x119 = y1r0 & (uint64_t)0x2222222222222222U;




3,472✔






958



  uint64_t x219 = y1r0 & (uint64_t)0x4444444444444444U;




3,472✔






959



  uint64_t x319 = y1r0 & (uint64_t)0x8888888888888888U;




3,472✔






960



  uint64_t y09 = uu____13 & (uint64_t)0x1111111111111111U;




3,472✔






961



  uint64_t y119 = uu____13 & (uint64_t)0x2222222222222222U;




3,472✔






962



  uint64_t y219 = uu____13 & (uint64_t)0x4444444444444444U;




3,472✔






963



  uint64_t y329 = uu____13 & (uint64_t)0x8888888888888888U;




3,472✔






964



  uint64_t z017 = x09 * y09 ^ (x119 * y329 ^ (x219 * y219 ^ x319 * y119));




3,472✔






965



  uint64_t z115 = x09 * y119 ^ (x119 * y09 ^ (x219 * y329 ^ x319 * y219));




3,472✔






966



  uint64_t z215 = x09 * y219 ^ (x119 * y119 ^ (x219 * y09 ^ x319 * y329));




3,472✔






967



  uint64_t z311 = x09 * y329 ^ (x119 * y219 ^ (x219 * y119 ^ x319 * y09));




3,472✔






968



  uint64_t




3,472✔






969



  z0h0 =




3,472✔






970



    (((z017 & (uint64_t)0x1111111111111111U) | (z115 & (uint64_t)0x2222222222222222U))




3,472✔






971



    | (z215 & (uint64_t)0x4444444444444444U))




3,472✔






972



    | (z311 & (uint64_t)0x8888888888888888U);




3,472✔






973



  uint64_t x010 = y2r0 & (uint64_t)0x1111111111111111U;




3,472✔






974



  uint64_t x1110 = y2r0 & (uint64_t)0x2222222222222222U;




3,472✔






975



  uint64_t x2110 = y2r0 & (uint64_t)0x4444444444444444U;




3,472✔






976



  uint64_t x3110 = y2r0 & (uint64_t)0x8888888888888888U;




3,472✔






977



  uint64_t y010 = uu____14 & (uint64_t)0x1111111111111111U;




3,472✔






978



  uint64_t y1110 = uu____14 & (uint64_t)0x2222222222222222U;




3,472✔






979



  uint64_t y2110 = uu____14 & (uint64_t)0x4444444444444444U;




3,472✔






980



  uint64_t y3210 = uu____14 & (uint64_t)0x8888888888888888U;




3,472✔






981



  uint64_t z018 = x010 * y010 ^ (x1110 * y3210 ^ (x2110 * y2110 ^ x3110 * y1110));




3,472✔






982



  uint64_t z116 = x010 * y1110 ^ (x1110 * y010 ^ (x2110 * y3210 ^ x3110 * y2110));




3,472✔






983



  uint64_t z216 = x010 * y2110 ^ (x1110 * y1110 ^ (x2110 * y010 ^ x3110 * y3210));




3,472✔






984



  uint64_t z312 = x010 * y3210 ^ (x1110 * y2110 ^ (x2110 * y1110 ^ x3110 * y010));




3,472✔






985



  uint64_t




3,472✔






986



  z1h0 =




3,472✔






987



    (((z018 & (uint64_t)0x1111111111111111U) | (z116 & (uint64_t)0x2222222222222222U))




3,472✔






988



    | (z216 & (uint64_t)0x4444444444444444U))




3,472✔






989



    | (z312 & (uint64_t)0x8888888888888888U);




3,472✔






990



  uint64_t x011 = y3r1 & (uint64_t)0x1111111111111111U;




3,472✔






991



  uint64_t x1111 = y3r1 & (uint64_t)0x2222222222222222U;




3,472✔






992



  uint64_t x2111 = y3r1 & (uint64_t)0x4444444444444444U;




3,472✔






993



  uint64_t x3111 = y3r1 & (uint64_t)0x8888888888888888U;




3,472✔






994



  uint64_t y011 = uu____15 & (uint64_t)0x1111111111111111U;




3,472✔






995



  uint64_t y1111 = uu____15 & (uint64_t)0x2222222222222222U;




3,472✔






996



  uint64_t y2111 = uu____15 & (uint64_t)0x4444444444444444U;




3,472✔






997



  uint64_t y3211 = uu____15 & (uint64_t)0x8888888888888888U;




3,472✔






998



  uint64_t z019 = x011 * y011 ^ (x1111 * y3211 ^ (x2111 * y2111 ^ x3111 * y1111));




3,472✔






999



  uint64_t z117 = x011 * y1111 ^ (x1111 * y011 ^ (x2111 * y3211 ^ x3111 * y2111));




3,472✔






1000



  uint64_t z217 = x011 * y2111 ^ (x1111 * y1111 ^ (x2111 * y011 ^ x3111 * y3211));




3,472✔






1001



  uint64_t z313 = x011 * y3211 ^ (x1111 * y2111 ^ (x2111 * y1111 ^ x3111 * y011));




3,472✔






1002



  uint64_t




3,472✔






1003



  z2h0 =




3,472✔






1004



    (((z019 & (uint64_t)0x1111111111111111U) | (z117 & (uint64_t)0x2222222222222222U))




3,472✔






1005



    | (z217 & (uint64_t)0x4444444444444444U))




3,472✔






1006



    | (z313 & (uint64_t)0x8888888888888888U);




3,472✔






1007



  uint64_t z218 = z214 ^ (z04 ^ z18);




3,472✔






1008



  uint64_t z2h11 = z2h0 ^ (z0h0 ^ z1h0);




3,472✔






1009



  uint64_t




3,472✔






1010



  x57 =




3,472✔






1011



    (z0h0 & (uint64_t)0x5555555555555555U)




3,472✔






1012



    << (uint32_t)(uint8_t)1U




3,472✔






1013



    | (z0h0 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1014



  uint64_t




3,472✔






1015



  x66 =




3,472✔






1016



    (x57 & (uint64_t)0x3333333333333333U)




3,472✔






1017



    << (uint32_t)(uint8_t)2U




3,472✔






1018



    | (x57 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1019



  uint64_t




3,472✔






1020



  x76 =




3,472✔






1021



    (x66 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1022



    << (uint32_t)(uint8_t)4U




3,472✔






1023



    | (x66 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1024



  uint64_t




3,472✔






1025



  x86 =




3,472✔






1026



    (x76 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1027



    << (uint32_t)(uint8_t)8U




3,472✔






1028



    | (x76 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1029



  uint64_t




3,472✔






1030



  x96 =




3,472✔






1031



    (x86 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1032



    << (uint32_t)(uint8_t)16U




3,472✔






1033



    | (x86 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1034



  uint64_t z0h10 = (x96 << (uint32_t)32U | x96 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






1035



  uint64_t




3,472✔






1036



  x58 =




3,472✔






1037



    (z1h0 & (uint64_t)0x5555555555555555U)




3,472✔






1038



    << (uint32_t)(uint8_t)1U




3,472✔






1039



    | (z1h0 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1040



  uint64_t




3,472✔






1041



  x67 =




3,472✔






1042



    (x58 & (uint64_t)0x3333333333333333U)




3,472✔






1043



    << (uint32_t)(uint8_t)2U




3,472✔






1044



    | (x58 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1045



  uint64_t




3,472✔






1046



  x77 =




3,472✔






1047



    (x67 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1048



    << (uint32_t)(uint8_t)4U




3,472✔






1049



    | (x67 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1050



  uint64_t




3,472✔






1051



  x87 =




3,472✔






1052



    (x77 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1053



    << (uint32_t)(uint8_t)8U




3,472✔






1054



    | (x77 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1055



  uint64_t




3,472✔






1056



  x97 =




3,472✔






1057



    (x87 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1058



    << (uint32_t)(uint8_t)16U




3,472✔






1059



    | (x87 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1060



  uint64_t z1h10 = (x97 << (uint32_t)32U | x97 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






1061



  uint64_t




3,472✔






1062



  x59 =




3,472✔






1063



    (z2h11 & (uint64_t)0x5555555555555555U)




3,472✔






1064



    << (uint32_t)(uint8_t)1U




3,472✔






1065



    | (z2h11 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1066



  uint64_t




3,472✔






1067



  x68 =




3,472✔






1068



    (x59 & (uint64_t)0x3333333333333333U)




3,472✔






1069



    << (uint32_t)(uint8_t)2U




3,472✔






1070



    | (x59 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1071



  uint64_t




3,472✔






1072



  x78 =




3,472✔






1073



    (x68 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1074



    << (uint32_t)(uint8_t)4U




3,472✔






1075



    | (x68 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1076



  uint64_t




3,472✔






1077



  x88 =




3,472✔






1078



    (x78 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1079



    << (uint32_t)(uint8_t)8U




3,472✔






1080



    | (x78 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1081



  uint64_t




3,472✔






1082



  x98 =




3,472✔






1083



    (x88 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1084



    << (uint32_t)(uint8_t)16U




3,472✔






1085



    | (x88 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1086



  uint64_t z2h20 = (x98 << (uint32_t)32U | x98 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






1087



  uint64_t z2_1 = z04;




3,472✔






1088



  uint64_t z2_2 = z0h10 ^ z218;




3,472✔






1089



  uint64_t z2_3 = z18 ^ z2h20;




3,472✔






1090



  uint64_t z2_4 = z1h10;




3,472✔






1091



  uint64_t z1 = z1_1 ^ z2_1;




3,472✔






1092



  uint64_t z2 = z1_2 ^ z2_2;




3,472✔






1093



  uint64_t z3 = z1_3 ^ z2_3;




3,472✔






1094



  uint64_t z4 = z1_4 ^ z2_4;




3,472✔






1095



  uint64_t uu____16 = x3[0U];




3,472✔






1096



  uint64_t uu____17 = x3[1U];




3,472✔






1097



  uint64_t uu____18 = y3[0U];




3,472✔






1098



  uint64_t uu____19 = y3[1U];




3,472✔






1099



  uint64_t uu____20 = y3[0U] ^ y3[1U];




3,472✔






1100



  uint64_t uu____21 = yr3[0U];




3,472✔






1101



  uint64_t uu____22 = yr3[1U];




3,472✔






1102



  uint64_t uu____23 = yr3[0U] ^ yr3[1U];




3,472✔






1103



  uint64_t




3,472✔






1104



  x510 =




3,472✔






1105



    (uu____16 & (uint64_t)0x5555555555555555U)




3,472✔






1106



    << (uint32_t)(uint8_t)1U




3,472✔






1107



    | (uu____16 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1108



  uint64_t




3,472✔






1109



  x69 =




3,472✔






1110



    (x510 & (uint64_t)0x3333333333333333U)




3,472✔






1111



    << (uint32_t)(uint8_t)2U




3,472✔






1112



    | (x510 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1113



  uint64_t




3,472✔






1114



  x79 =




3,472✔






1115



    (x69 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1116



    << (uint32_t)(uint8_t)4U




3,472✔






1117



    | (x69 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1118



  uint64_t




3,472✔






1119



  x89 =




3,472✔






1120



    (x79 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1121



    << (uint32_t)(uint8_t)8U




3,472✔






1122



    | (x79 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1123



  uint64_t




3,472✔






1124



  x99 =




3,472✔






1125



    (x89 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1126



    << (uint32_t)(uint8_t)16U




3,472✔






1127



    | (x89 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1128



  uint64_t y1r1 = x99 << (uint32_t)32U | x99 >> (uint32_t)32U;




3,472✔






1129



  uint64_t




3,472✔






1130



  x511 =




3,472✔






1131



    (uu____17 & (uint64_t)0x5555555555555555U)




3,472✔






1132



    << (uint32_t)(uint8_t)1U




3,472✔






1133



    | (uu____17 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1134



  uint64_t




3,472✔






1135



  x610 =




3,472✔






1136



    (x511 & (uint64_t)0x3333333333333333U)




3,472✔






1137



    << (uint32_t)(uint8_t)2U




3,472✔






1138



    | (x511 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1139



  uint64_t




3,472✔






1140



  x710 =




3,472✔






1141



    (x610 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1142



    << (uint32_t)(uint8_t)4U




3,472✔






1143



    | (x610 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1144



  uint64_t




3,472✔






1145



  x810 =




3,472✔






1146



    (x710 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1147



    << (uint32_t)(uint8_t)8U




3,472✔






1148



    | (x710 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1149



  uint64_t




3,472✔






1150



  x910 =




3,472✔






1151



    (x810 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1152



    << (uint32_t)(uint8_t)16U




3,472✔






1153



    | (x810 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1154



  uint64_t y2r1 = x910 << (uint32_t)32U | x910 >> (uint32_t)32U;




3,472✔






1155



  uint64_t y312 = uu____16 ^ uu____17;




3,472✔






1156



  uint64_t y3r2 = y1r1 ^ y2r1;




3,472✔






1157



  uint64_t x012 = uu____16 & (uint64_t)0x1111111111111111U;




3,472✔






1158



  uint64_t x1112 = uu____16 & (uint64_t)0x2222222222222222U;




3,472✔






1159



  uint64_t x2112 = uu____16 & (uint64_t)0x4444444444444444U;




3,472✔






1160



  uint64_t x3112 = uu____16 & (uint64_t)0x8888888888888888U;




3,472✔






1161



  uint64_t y012 = uu____18 & (uint64_t)0x1111111111111111U;




3,472✔






1162



  uint64_t y1112 = uu____18 & (uint64_t)0x2222222222222222U;




3,472✔






1163



  uint64_t y2112 = uu____18 & (uint64_t)0x4444444444444444U;




3,472✔






1164



  uint64_t y3212 = uu____18 & (uint64_t)0x8888888888888888U;




3,472✔






1165



  uint64_t z05 = x012 * y012 ^ (x1112 * y3212 ^ (x2112 * y2112 ^ x3112 * y1112));




3,472✔






1166



  uint64_t z118 = x012 * y1112 ^ (x1112 * y012 ^ (x2112 * y3212 ^ x3112 * y2112));




3,472✔






1167



  uint64_t z219 = x012 * y2112 ^ (x1112 * y1112 ^ (x2112 * y012 ^ x3112 * y3212));




3,472✔






1168



  uint64_t z314 = x012 * y3212 ^ (x1112 * y2112 ^ (x2112 * y1112 ^ x3112 * y012));




3,472✔






1169



  uint64_t




3,472✔






1170



  z06 =




3,472✔






1171



    (((z05 & (uint64_t)0x1111111111111111U) | (z118 & (uint64_t)0x2222222222222222U))




3,472✔






1172



    | (z219 & (uint64_t)0x4444444444444444U))




3,472✔






1173



    | (z314 & (uint64_t)0x8888888888888888U);




3,472✔






1174



  uint64_t x013 = uu____17 & (uint64_t)0x1111111111111111U;




3,472✔






1175



  uint64_t x1113 = uu____17 & (uint64_t)0x2222222222222222U;




3,472✔






1176



  uint64_t x2113 = uu____17 & (uint64_t)0x4444444444444444U;




3,472✔






1177



  uint64_t x3113 = uu____17 & (uint64_t)0x8888888888888888U;




3,472✔






1178



  uint64_t y013 = uu____19 & (uint64_t)0x1111111111111111U;




3,472✔






1179



  uint64_t y1113 = uu____19 & (uint64_t)0x2222222222222222U;




3,472✔






1180



  uint64_t y2113 = uu____19 & (uint64_t)0x4444444444444444U;




3,472✔






1181



  uint64_t y3213 = uu____19 & (uint64_t)0x8888888888888888U;




3,472✔






1182



  uint64_t z0110 = x013 * y013 ^ (x1113 * y3213 ^ (x2113 * y2113 ^ x3113 * y1113));




3,472✔






1183



  uint64_t z119 = x013 * y1113 ^ (x1113 * y013 ^ (x2113 * y3213 ^ x3113 * y2113));




3,472✔






1184



  uint64_t z2110 = x013 * y2113 ^ (x1113 * y1113 ^ (x2113 * y013 ^ x3113 * y3213));




3,472✔






1185



  uint64_t z315 = x013 * y3213 ^ (x1113 * y2113 ^ (x2113 * y1113 ^ x3113 * y013));




3,472✔






1186



  uint64_t




3,472✔






1187



  z1110 =




3,472✔






1188



    (((z0110 & (uint64_t)0x1111111111111111U) | (z119 & (uint64_t)0x2222222222222222U))




3,472✔






1189



    | (z2110 & (uint64_t)0x4444444444444444U))




3,472✔






1190



    | (z315 & (uint64_t)0x8888888888888888U);




3,472✔






1191



  uint64_t x014 = y312 & (uint64_t)0x1111111111111111U;




3,472✔






1192



  uint64_t x1114 = y312 & (uint64_t)0x2222222222222222U;




3,472✔






1193



  uint64_t x2114 = y312 & (uint64_t)0x4444444444444444U;




3,472✔






1194



  uint64_t x3114 = y312 & (uint64_t)0x8888888888888888U;




3,472✔






1195



  uint64_t y014 = uu____20 & (uint64_t)0x1111111111111111U;




3,472✔






1196



  uint64_t y1114 = uu____20 & (uint64_t)0x2222222222222222U;




3,472✔






1197



  uint64_t y2114 = uu____20 & (uint64_t)0x4444444444444444U;




3,472✔






1198



  uint64_t y3214 = uu____20 & (uint64_t)0x8888888888888888U;




3,472✔






1199



  uint64_t z0111 = x014 * y014 ^ (x1114 * y3214 ^ (x2114 * y2114 ^ x3114 * y1114));




3,472✔






1200



  uint64_t z120 = x014 * y1114 ^ (x1114 * y014 ^ (x2114 * y3214 ^ x3114 * y2114));




3,472✔






1201



  uint64_t z2111 = x014 * y2114 ^ (x1114 * y1114 ^ (x2114 * y014 ^ x3114 * y3214));




3,472✔






1202



  uint64_t z316 = x014 * y3214 ^ (x1114 * y2114 ^ (x2114 * y1114 ^ x3114 * y014));




3,472✔






1203



  uint64_t




3,472✔






1204



  z2112 =




3,472✔






1205



    (((z0111 & (uint64_t)0x1111111111111111U) | (z120 & (uint64_t)0x2222222222222222U))




3,472✔






1206



    | (z2111 & (uint64_t)0x4444444444444444U))




3,472✔






1207



    | (z316 & (uint64_t)0x8888888888888888U);




3,472✔






1208



  uint64_t x015 = y1r1 & (uint64_t)0x1111111111111111U;




3,472✔






1209



  uint64_t x1115 = y1r1 & (uint64_t)0x2222222222222222U;




3,472✔






1210



  uint64_t x2115 = y1r1 & (uint64_t)0x4444444444444444U;




3,472✔






1211



  uint64_t x3115 = y1r1 & (uint64_t)0x8888888888888888U;




3,472✔






1212



  uint64_t y015 = uu____21 & (uint64_t)0x1111111111111111U;




3,472✔






1213



  uint64_t y1115 = uu____21 & (uint64_t)0x2222222222222222U;




3,472✔






1214



  uint64_t y2115 = uu____21 & (uint64_t)0x4444444444444444U;




3,472✔






1215



  uint64_t y3215 = uu____21 & (uint64_t)0x8888888888888888U;




3,472✔






1216



  uint64_t z0112 = x015 * y015 ^ (x1115 * y3215 ^ (x2115 * y2115 ^ x3115 * y1115));




3,472✔






1217



  uint64_t z121 = x015 * y1115 ^ (x1115 * y015 ^ (x2115 * y3215 ^ x3115 * y2115));




3,472✔






1218



  uint64_t z220 = x015 * y2115 ^ (x1115 * y1115 ^ (x2115 * y015 ^ x3115 * y3215));




3,472✔






1219



  uint64_t z317 = x015 * y3215 ^ (x1115 * y2115 ^ (x2115 * y1115 ^ x3115 * y015));




3,472✔






1220



  uint64_t




3,472✔






1221



  z0h2 =




3,472✔






1222



    (((z0112 & (uint64_t)0x1111111111111111U) | (z121 & (uint64_t)0x2222222222222222U))




3,472✔






1223



    | (z220 & (uint64_t)0x4444444444444444U))




3,472✔






1224



    | (z317 & (uint64_t)0x8888888888888888U);




3,472✔






1225



  uint64_t x016 = y2r1 & (uint64_t)0x1111111111111111U;




3,472✔






1226



  uint64_t x1116 = y2r1 & (uint64_t)0x2222222222222222U;




3,472✔






1227



  uint64_t x2116 = y2r1 & (uint64_t)0x4444444444444444U;




3,472✔






1228



  uint64_t x3116 = y2r1 & (uint64_t)0x8888888888888888U;




3,472✔






1229



  uint64_t y016 = uu____22 & (uint64_t)0x1111111111111111U;




3,472✔






1230



  uint64_t y1116 = uu____22 & (uint64_t)0x2222222222222222U;




3,472✔






1231



  uint64_t y2116 = uu____22 & (uint64_t)0x4444444444444444U;




3,472✔






1232



  uint64_t y3216 = uu____22 & (uint64_t)0x8888888888888888U;




3,472✔






1233



  uint64_t z0113 = x016 * y016 ^ (x1116 * y3216 ^ (x2116 * y2116 ^ x3116 * y1116));




3,472✔






1234



  uint64_t z122 = x016 * y1116 ^ (x1116 * y016 ^ (x2116 * y3216 ^ x3116 * y2116));




3,472✔






1235



  uint64_t z221 = x016 * y2116 ^ (x1116 * y1116 ^ (x2116 * y016 ^ x3116 * y3216));




3,472✔






1236



  uint64_t z318 = x016 * y3216 ^ (x1116 * y2116 ^ (x2116 * y1116 ^ x3116 * y016));




3,472✔






1237



  uint64_t




3,472✔






1238



  z1h2 =




3,472✔






1239



    (((z0113 & (uint64_t)0x1111111111111111U) | (z122 & (uint64_t)0x2222222222222222U))




3,472✔






1240



    | (z221 & (uint64_t)0x4444444444444444U))




3,472✔






1241



    | (z318 & (uint64_t)0x8888888888888888U);




3,472✔






1242



  uint64_t x017 = y3r2 & (uint64_t)0x1111111111111111U;




3,472✔






1243



  uint64_t x1117 = y3r2 & (uint64_t)0x2222222222222222U;




3,472✔






1244



  uint64_t x2117 = y3r2 & (uint64_t)0x4444444444444444U;




3,472✔






1245



  uint64_t x3117 = y3r2 & (uint64_t)0x8888888888888888U;




3,472✔






1246



  uint64_t y017 = uu____23 & (uint64_t)0x1111111111111111U;




3,472✔






1247



  uint64_t y1117 = uu____23 & (uint64_t)0x2222222222222222U;




3,472✔






1248



  uint64_t y2117 = uu____23 & (uint64_t)0x4444444444444444U;




3,472✔






1249



  uint64_t y3217 = uu____23 & (uint64_t)0x8888888888888888U;




3,472✔






1250



  uint64_t z0114 = x017 * y017 ^ (x1117 * y3217 ^ (x2117 * y2117 ^ x3117 * y1117));




3,472✔






1251



  uint64_t z123 = x017 * y1117 ^ (x1117 * y017 ^ (x2117 * y3217 ^ x3117 * y2117));




3,472✔






1252



  uint64_t z222 = x017 * y2117 ^ (x1117 * y1117 ^ (x2117 * y017 ^ x3117 * y3217));




3,472✔






1253



  uint64_t z319 = x017 * y3217 ^ (x1117 * y2117 ^ (x2117 * y1117 ^ x3117 * y017));




3,472✔






1254



  uint64_t




3,472✔






1255



  z2h3 =




3,472✔






1256



    (((z0114 & (uint64_t)0x1111111111111111U) | (z123 & (uint64_t)0x2222222222222222U))




3,472✔






1257



    | (z222 & (uint64_t)0x4444444444444444U))




3,472✔






1258



    | (z319 & (uint64_t)0x8888888888888888U);




3,472✔






1259



  uint64_t z223 = z2112 ^ (z06 ^ z1110);




3,472✔






1260



  uint64_t z2h12 = z2h3 ^ (z0h2 ^ z1h2);




3,472✔






1261



  uint64_t




3,472✔






1262



  x512 =




3,472✔






1263



    (z0h2 & (uint64_t)0x5555555555555555U)




3,472✔






1264



    << (uint32_t)(uint8_t)1U




3,472✔






1265



    | (z0h2 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1266



  uint64_t




3,472✔






1267



  x611 =




3,472✔






1268



    (x512 & (uint64_t)0x3333333333333333U)




3,472✔






1269



    << (uint32_t)(uint8_t)2U




3,472✔






1270



    | (x512 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1271



  uint64_t




3,472✔






1272



  x711 =




3,472✔






1273



    (x611 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1274



    << (uint32_t)(uint8_t)4U




3,472✔






1275



    | (x611 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1276



  uint64_t




3,472✔






1277



  x811 =




3,472✔






1278



    (x711 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1279



    << (uint32_t)(uint8_t)8U




3,472✔






1280



    | (x711 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1281



  uint64_t




3,472✔






1282



  x911 =




3,472✔






1283



    (x811 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1284



    << (uint32_t)(uint8_t)16U




3,472✔






1285



    | (x811 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1286



  uint64_t z0h11 = (x911 << (uint32_t)32U | x911 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






1287



  uint64_t




3,472✔






1288



  x513 =




3,472✔






1289



    (z1h2 & (uint64_t)0x5555555555555555U)




3,472✔






1290



    << (uint32_t)(uint8_t)1U




3,472✔






1291



    | (z1h2 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1292



  uint64_t




3,472✔






1293



  x612 =




3,472✔






1294



    (x513 & (uint64_t)0x3333333333333333U)




3,472✔






1295



    << (uint32_t)(uint8_t)2U




3,472✔






1296



    | (x513 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1297



  uint64_t




3,472✔






1298



  x712 =




3,472✔






1299



    (x612 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1300



    << (uint32_t)(uint8_t)4U




3,472✔






1301



    | (x612 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1302



  uint64_t




3,472✔






1303



  x812 =




3,472✔






1304



    (x712 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1305



    << (uint32_t)(uint8_t)8U




3,472✔






1306



    | (x712 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1307



  uint64_t




3,472✔






1308



  x912 =




3,472✔






1309



    (x812 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1310



    << (uint32_t)(uint8_t)16U




3,472✔






1311



    | (x812 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1312



  uint64_t z1h11 = (x912 << (uint32_t)32U | x912 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






1313



  uint64_t




3,472✔






1314



  x514 =




3,472✔






1315



    (z2h12 & (uint64_t)0x5555555555555555U)




3,472✔






1316



    << (uint32_t)(uint8_t)1U




3,472✔






1317



    | (z2h12 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1318



  uint64_t




3,472✔






1319



  x613 =




3,472✔






1320



    (x514 & (uint64_t)0x3333333333333333U)




3,472✔






1321



    << (uint32_t)(uint8_t)2U




3,472✔






1322



    | (x514 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1323



  uint64_t




3,472✔






1324



  x713 =




3,472✔






1325



    (x613 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1326



    << (uint32_t)(uint8_t)4U




3,472✔






1327



    | (x613 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1328



  uint64_t




3,472✔






1329



  x813 =




3,472✔






1330



    (x713 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1331



    << (uint32_t)(uint8_t)8U




3,472✔






1332



    | (x713 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1333



  uint64_t




3,472✔






1334



  x913 =




3,472✔






1335



    (x813 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1336



    << (uint32_t)(uint8_t)16U




3,472✔






1337



    | (x813 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1338



  uint64_t z2h21 = (x913 << (uint32_t)32U | x913 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






1339



  uint64_t z3_1 = z06;




3,472✔






1340



  uint64_t z3_2 = z0h11 ^ z223;




3,472✔






1341



  uint64_t z3_3 = z1110 ^ z2h21;




3,472✔






1342



  uint64_t z3_4 = z1h11;




3,472✔






1343



  uint64_t z11 = z1 ^ z3_1;




3,472✔






1344



  uint64_t z21 = z2 ^ z3_2;




3,472✔






1345



  uint64_t z31 = z3 ^ z3_3;




3,472✔






1346



  uint64_t z41 = z4 ^ z3_4;




3,472✔






1347



  uint64_t uu____24 = x4[0U];




3,472✔






1348



  uint64_t uu____25 = x4[1U];




3,472✔






1349



  uint64_t uu____26 = y4[0U];




3,472✔






1350



  uint64_t uu____27 = y4[1U];




3,472✔






1351



  uint64_t uu____28 = y4[0U] ^ y4[1U];




3,472✔






1352



  uint64_t uu____29 = yr4[0U];




3,472✔






1353



  uint64_t uu____30 = yr4[1U];




3,472✔






1354



  uint64_t uu____31 = yr4[0U] ^ yr4[1U];




3,472✔






1355



  uint64_t




3,472✔






1356



  x515 =




3,472✔






1357



    (uu____24 & (uint64_t)0x5555555555555555U)




3,472✔






1358



    << (uint32_t)(uint8_t)1U




3,472✔






1359



    | (uu____24 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1360



  uint64_t




3,472✔






1361



  x614 =




3,472✔






1362



    (x515 & (uint64_t)0x3333333333333333U)




3,472✔






1363



    << (uint32_t)(uint8_t)2U




3,472✔






1364



    | (x515 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1365



  uint64_t




3,472✔






1366



  x714 =




3,472✔






1367



    (x614 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1368



    << (uint32_t)(uint8_t)4U




3,472✔






1369



    | (x614 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1370



  uint64_t




3,472✔






1371



  x814 =




3,472✔






1372



    (x714 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1373



    << (uint32_t)(uint8_t)8U




3,472✔






1374



    | (x714 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1375



  uint64_t




3,472✔






1376



  x914 =




3,472✔






1377



    (x814 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1378



    << (uint32_t)(uint8_t)16U




3,472✔






1379



    | (x814 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1380



  uint64_t y1r2 = x914 << (uint32_t)32U | x914 >> (uint32_t)32U;




3,472✔






1381



  uint64_t




3,472✔






1382



  x516 =




3,472✔






1383



    (uu____25 & (uint64_t)0x5555555555555555U)




3,472✔






1384



    << (uint32_t)(uint8_t)1U




3,472✔






1385



    | (uu____25 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1386



  uint64_t




3,472✔






1387



  x615 =




3,472✔






1388



    (x516 & (uint64_t)0x3333333333333333U)




3,472✔






1389



    << (uint32_t)(uint8_t)2U




3,472✔






1390



    | (x516 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1391



  uint64_t




3,472✔






1392



  x715 =




3,472✔






1393



    (x615 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1394



    << (uint32_t)(uint8_t)4U




3,472✔






1395



    | (x615 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1396



  uint64_t




3,472✔






1397



  x815 =




3,472✔






1398



    (x715 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1399



    << (uint32_t)(uint8_t)8U




3,472✔






1400



    | (x715 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1401



  uint64_t




3,472✔






1402



  x915 =




3,472✔






1403



    (x815 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1404



    << (uint32_t)(uint8_t)16U




3,472✔






1405



    | (x815 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1406



  uint64_t y2r2 = x915 << (uint32_t)32U | x915 >> (uint32_t)32U;




3,472✔






1407



  uint64_t y31 = uu____24 ^ uu____25;




3,472✔






1408



  uint64_t y3r = y1r2 ^ y2r2;




3,472✔






1409



  uint64_t x018 = uu____24 & (uint64_t)0x1111111111111111U;




3,472✔






1410



  uint64_t x1118 = uu____24 & (uint64_t)0x2222222222222222U;




3,472✔






1411



  uint64_t x2118 = uu____24 & (uint64_t)0x4444444444444444U;




3,472✔






1412



  uint64_t x3118 = uu____24 & (uint64_t)0x8888888888888888U;




3,472✔






1413



  uint64_t y018 = uu____26 & (uint64_t)0x1111111111111111U;




3,472✔






1414



  uint64_t y1118 = uu____26 & (uint64_t)0x2222222222222222U;




3,472✔






1415



  uint64_t y2118 = uu____26 & (uint64_t)0x4444444444444444U;




3,472✔






1416



  uint64_t y3218 = uu____26 & (uint64_t)0x8888888888888888U;




3,472✔






1417



  uint64_t z0 = x018 * y018 ^ (x1118 * y3218 ^ (x2118 * y2118 ^ x3118 * y1118));




3,472✔






1418



  uint64_t z124 = x018 * y1118 ^ (x1118 * y018 ^ (x2118 * y3218 ^ x3118 * y2118));




3,472✔






1419



  uint64_t z224 = x018 * y2118 ^ (x1118 * y1118 ^ (x2118 * y018 ^ x3118 * y3218));




3,472✔






1420



  uint64_t z320 = x018 * y3218 ^ (x1118 * y2118 ^ (x2118 * y1118 ^ x3118 * y018));




3,472✔






1421



  uint64_t




3,472✔






1422



  z07 =




3,472✔






1423



    (((z0 & (uint64_t)0x1111111111111111U) | (z124 & (uint64_t)0x2222222222222222U))




3,472✔






1424



    | (z224 & (uint64_t)0x4444444444444444U))




3,472✔






1425



    | (z320 & (uint64_t)0x8888888888888888U);




3,472✔






1426



  uint64_t x019 = uu____25 & (uint64_t)0x1111111111111111U;




3,472✔






1427



  uint64_t x1119 = uu____25 & (uint64_t)0x2222222222222222U;




3,472✔






1428



  uint64_t x2119 = uu____25 & (uint64_t)0x4444444444444444U;




3,472✔






1429



  uint64_t x3119 = uu____25 & (uint64_t)0x8888888888888888U;




3,472✔






1430



  uint64_t y019 = uu____27 & (uint64_t)0x1111111111111111U;




3,472✔






1431



  uint64_t y1119 = uu____27 & (uint64_t)0x2222222222222222U;




3,472✔






1432



  uint64_t y2119 = uu____27 & (uint64_t)0x4444444444444444U;




3,472✔






1433



  uint64_t y3219 = uu____27 & (uint64_t)0x8888888888888888U;




3,472✔






1434



  uint64_t z0115 = x019 * y019 ^ (x1119 * y3219 ^ (x2119 * y2119 ^ x3119 * y1119));




3,472✔






1435



  uint64_t z125 = x019 * y1119 ^ (x1119 * y019 ^ (x2119 * y3219 ^ x3119 * y2119));




3,472✔






1436



  uint64_t z225 = x019 * y2119 ^ (x1119 * y1119 ^ (x2119 * y019 ^ x3119 * y3219));




3,472✔






1437



  uint64_t z321 = x019 * y3219 ^ (x1119 * y2119 ^ (x2119 * y1119 ^ x3119 * y019));




3,472✔






1438



  uint64_t




3,472✔






1439



  z126 =




3,472✔






1440



    (((z0115 & (uint64_t)0x1111111111111111U) | (z125 & (uint64_t)0x2222222222222222U))




3,472✔






1441



    | (z225 & (uint64_t)0x4444444444444444U))




3,472✔






1442



    | (z321 & (uint64_t)0x8888888888888888U);




3,472✔






1443



  uint64_t x020 = y31 & (uint64_t)0x1111111111111111U;




3,472✔






1444



  uint64_t x1120 = y31 & (uint64_t)0x2222222222222222U;




3,472✔






1445



  uint64_t x2120 = y31 & (uint64_t)0x4444444444444444U;




3,472✔






1446



  uint64_t x3120 = y31 & (uint64_t)0x8888888888888888U;




3,472✔






1447



  uint64_t y020 = uu____28 & (uint64_t)0x1111111111111111U;




3,472✔






1448



  uint64_t y1120 = uu____28 & (uint64_t)0x2222222222222222U;




3,472✔






1449



  uint64_t y2120 = uu____28 & (uint64_t)0x4444444444444444U;




3,472✔






1450



  uint64_t y3220 = uu____28 & (uint64_t)0x8888888888888888U;




3,472✔






1451



  uint64_t z0116 = x020 * y020 ^ (x1120 * y3220 ^ (x2120 * y2120 ^ x3120 * y1120));




3,472✔






1452



  uint64_t z130 = x020 * y1120 ^ (x1120 * y020 ^ (x2120 * y3220 ^ x3120 * y2120));




3,472✔






1453



  uint64_t z226 = x020 * y2120 ^ (x1120 * y1120 ^ (x2120 * y020 ^ x3120 * y3220));




3,472✔






1454



  uint64_t z322 = x020 * y3220 ^ (x1120 * y2120 ^ (x2120 * y1120 ^ x3120 * y020));




3,472✔






1455



  uint64_t




3,472✔






1456



  z227 =




3,472✔






1457



    (((z0116 & (uint64_t)0x1111111111111111U) | (z130 & (uint64_t)0x2222222222222222U))




3,472✔






1458



    | (z226 & (uint64_t)0x4444444444444444U))




3,472✔






1459



    | (z322 & (uint64_t)0x8888888888888888U);




3,472✔






1460



  uint64_t x021 = y1r2 & (uint64_t)0x1111111111111111U;




3,472✔






1461



  uint64_t x1121 = y1r2 & (uint64_t)0x2222222222222222U;




3,472✔






1462



  uint64_t x2121 = y1r2 & (uint64_t)0x4444444444444444U;




3,472✔






1463



  uint64_t x3121 = y1r2 & (uint64_t)0x8888888888888888U;




3,472✔






1464



  uint64_t y021 = uu____29 & (uint64_t)0x1111111111111111U;




3,472✔






1465



  uint64_t y1121 = uu____29 & (uint64_t)0x2222222222222222U;




3,472✔






1466



  uint64_t y2121 = uu____29 & (uint64_t)0x4444444444444444U;




3,472✔






1467



  uint64_t y3221 = uu____29 & (uint64_t)0x8888888888888888U;




3,472✔






1468



  uint64_t z0117 = x021 * y021 ^ (x1121 * y3221 ^ (x2121 * y2121 ^ x3121 * y1121));




3,472✔






1469



  uint64_t z131 = x021 * y1121 ^ (x1121 * y021 ^ (x2121 * y3221 ^ x3121 * y2121));




3,472✔






1470



  uint64_t z230 = x021 * y2121 ^ (x1121 * y1121 ^ (x2121 * y021 ^ x3121 * y3221));




3,472✔






1471



  uint64_t z323 = x021 * y3221 ^ (x1121 * y2121 ^ (x2121 * y1121 ^ x3121 * y021));




3,472✔






1472



  uint64_t




3,472✔






1473



  z0h3 =




3,472✔






1474



    (((z0117 & (uint64_t)0x1111111111111111U) | (z131 & (uint64_t)0x2222222222222222U))




3,472✔






1475



    | (z230 & (uint64_t)0x4444444444444444U))




3,472✔






1476



    | (z323 & (uint64_t)0x8888888888888888U);




3,472✔






1477



  uint64_t x022 = y2r2 & (uint64_t)0x1111111111111111U;




3,472✔






1478



  uint64_t x1122 = y2r2 & (uint64_t)0x2222222222222222U;




3,472✔






1479



  uint64_t x2122 = y2r2 & (uint64_t)0x4444444444444444U;




3,472✔






1480



  uint64_t x3122 = y2r2 & (uint64_t)0x8888888888888888U;




3,472✔






1481



  uint64_t y022 = uu____30 & (uint64_t)0x1111111111111111U;




3,472✔






1482



  uint64_t y1122 = uu____30 & (uint64_t)0x2222222222222222U;




3,472✔






1483



  uint64_t y2122 = uu____30 & (uint64_t)0x4444444444444444U;




3,472✔






1484



  uint64_t y3222 = uu____30 & (uint64_t)0x8888888888888888U;




3,472✔






1485



  uint64_t z0118 = x022 * y022 ^ (x1122 * y3222 ^ (x2122 * y2122 ^ x3122 * y1122));




3,472✔






1486



  uint64_t z132 = x022 * y1122 ^ (x1122 * y022 ^ (x2122 * y3222 ^ x3122 * y2122));




3,472✔






1487



  uint64_t z231 = x022 * y2122 ^ (x1122 * y1122 ^ (x2122 * y022 ^ x3122 * y3222));




3,472✔






1488



  uint64_t z324 = x022 * y3222 ^ (x1122 * y2122 ^ (x2122 * y1122 ^ x3122 * y022));




3,472✔






1489



  uint64_t




3,472✔






1490



  z1h3 =




3,472✔






1491



    (((z0118 & (uint64_t)0x1111111111111111U) | (z132 & (uint64_t)0x2222222222222222U))




3,472✔






1492



    | (z231 & (uint64_t)0x4444444444444444U))




3,472✔






1493



    | (z324 & (uint64_t)0x8888888888888888U);




3,472✔






1494



  uint64_t x0 = y3r & (uint64_t)0x1111111111111111U;




3,472✔






1495



  uint64_t x11 = y3r & (uint64_t)0x2222222222222222U;




3,472✔






1496



  uint64_t x21 = y3r & (uint64_t)0x4444444444444444U;




3,472✔






1497



  uint64_t x31 = y3r & (uint64_t)0x8888888888888888U;




3,472✔






1498



  uint64_t y0 = uu____31 & (uint64_t)0x1111111111111111U;




3,472✔






1499



  uint64_t y11 = uu____31 & (uint64_t)0x2222222222222222U;




3,472✔






1500



  uint64_t y21 = uu____31 & (uint64_t)0x4444444444444444U;




3,472✔






1501



  uint64_t y32 = uu____31 & (uint64_t)0x8888888888888888U;




3,472✔






1502



  uint64_t z01 = x0 * y0 ^ (x11 * y32 ^ (x21 * y21 ^ x31 * y11));




3,472✔






1503



  uint64_t z13 = x0 * y11 ^ (x11 * y0 ^ (x21 * y32 ^ x31 * y21));




3,472✔






1504



  uint64_t z232 = x0 * y21 ^ (x11 * y11 ^ (x21 * y0 ^ x31 * y32));




3,472✔






1505



  uint64_t z325 = x0 * y32 ^ (x11 * y21 ^ (x21 * y11 ^ x31 * y0));




3,472✔






1506



  uint64_t




3,472✔






1507



  z2h4 =




3,472✔






1508



    (((z01 & (uint64_t)0x1111111111111111U) | (z13 & (uint64_t)0x2222222222222222U))




3,472✔






1509



    | (z232 & (uint64_t)0x4444444444444444U))




3,472✔






1510



    | (z325 & (uint64_t)0x8888888888888888U);




3,472✔






1511



  uint64_t z23 = z227 ^ (z07 ^ z126);




3,472✔






1512



  uint64_t z2h1 = z2h4 ^ (z0h3 ^ z1h3);




3,472✔






1513



  uint64_t




3,472✔






1514



  x517 =




3,472✔






1515



    (z0h3 & (uint64_t)0x5555555555555555U)




3,472✔






1516



    << (uint32_t)(uint8_t)1U




3,472✔






1517



    | (z0h3 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1518



  uint64_t




3,472✔






1519



  x616 =




3,472✔






1520



    (x517 & (uint64_t)0x3333333333333333U)




3,472✔






1521



    << (uint32_t)(uint8_t)2U




3,472✔






1522



    | (x517 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1523



  uint64_t




3,472✔






1524



  x716 =




3,472✔






1525



    (x616 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1526



    << (uint32_t)(uint8_t)4U




3,472✔






1527



    | (x616 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1528



  uint64_t




3,472✔






1529



  x816 =




3,472✔






1530



    (x716 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1531



    << (uint32_t)(uint8_t)8U




3,472✔






1532



    | (x716 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1533



  uint64_t




3,472✔






1534



  x916 =




3,472✔






1535



    (x816 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1536



    << (uint32_t)(uint8_t)16U




3,472✔






1537



    | (x816 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1538



  uint64_t z0h12 = (x916 << (uint32_t)32U | x916 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






1539



  uint64_t




3,472✔






1540



  x518 =




3,472✔






1541



    (z1h3 & (uint64_t)0x5555555555555555U)




3,472✔






1542



    << (uint32_t)(uint8_t)1U




3,472✔






1543



    | (z1h3 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1544



  uint64_t




3,472✔






1545



  x617 =




3,472✔






1546



    (x518 & (uint64_t)0x3333333333333333U)




3,472✔






1547



    << (uint32_t)(uint8_t)2U




3,472✔






1548



    | (x518 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1549



  uint64_t




3,472✔






1550



  x717 =




3,472✔






1551



    (x617 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1552



    << (uint32_t)(uint8_t)4U




3,472✔






1553



    | (x617 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1554



  uint64_t




3,472✔






1555



  x817 =




3,472✔






1556



    (x717 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1557



    << (uint32_t)(uint8_t)8U




3,472✔






1558



    | (x717 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1559



  uint64_t




3,472✔






1560



  x917 =




3,472✔






1561



    (x817 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1562



    << (uint32_t)(uint8_t)16U




3,472✔






1563



    | (x817 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1564



  uint64_t z1h12 = (x917 << (uint32_t)32U | x917 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






1565



  uint64_t




3,472✔






1566



  x5 =




3,472✔






1567



    (z2h1 & (uint64_t)0x5555555555555555U)




3,472✔






1568



    << (uint32_t)(uint8_t)1U




3,472✔






1569



    | (z2h1 >> (uint32_t)(uint8_t)1U & (uint64_t)0x5555555555555555U);




3,472✔






1570



  uint64_t




3,472✔






1571



  x618 =




3,472✔






1572



    (x5 & (uint64_t)0x3333333333333333U)




3,472✔






1573



    << (uint32_t)(uint8_t)2U




3,472✔






1574



    | (x5 >> (uint32_t)(uint8_t)2U & (uint64_t)0x3333333333333333U);




3,472✔






1575



  uint64_t




3,472✔






1576



  x718 =




3,472✔






1577



    (x618 & (uint64_t)0x0F0F0F0F0F0F0F0FU)




3,472✔






1578



    << (uint32_t)(uint8_t)4U




3,472✔






1579



    | (x618 >> (uint32_t)(uint8_t)4U & (uint64_t)0x0F0F0F0F0F0F0F0FU);




3,472✔






1580



  uint64_t




3,472✔






1581



  x818 =




3,472✔






1582



    (x718 & (uint64_t)0x00FF00FF00FF00FFU)




3,472✔






1583



    << (uint32_t)(uint8_t)8U




3,472✔






1584



    | (x718 >> (uint32_t)(uint8_t)8U & (uint64_t)0x00FF00FF00FF00FFU);




3,472✔






1585



  uint64_t




3,472✔






1586



  x918 =




3,472✔






1587



    (x818 & (uint64_t)0x0000FFFF0000FFFFU)




3,472✔






1588



    << (uint32_t)(uint8_t)16U




3,472✔






1589



    | (x818 >> (uint32_t)(uint8_t)16U & (uint64_t)0x0000FFFF0000FFFFU);




3,472✔






1590



  uint64_t z2h22 = (x918 << (uint32_t)32U | x918 >> (uint32_t)32U) >> (uint32_t)1U;




3,472✔






1591



  uint64_t z4_1 = z07;




3,472✔






1592



  uint64_t z4_2 = z0h12 ^ z23;




3,472✔






1593



  uint64_t z4_3 = z126 ^ z2h22;




3,472✔






1594



  uint64_t z4_4 = z1h12;




3,472✔






1595



  uint64_t z12 = z11 ^ z4_1;




3,472✔






1596



  uint64_t z22 = z21 ^ z4_2;




3,472✔






1597



  uint64_t z32 = z31 ^ z4_3;




3,472✔






1598



  uint64_t z42 = z41 ^ z4_4;




3,472✔






1599



  uint64_t v3 = z42 << (uint32_t)1U | z32 >> (uint32_t)63U;




3,472✔






1600



  uint64_t v20 = z32 << (uint32_t)1U | z22 >> (uint32_t)63U;




3,472✔






1601



  uint64_t v1 = z22 << (uint32_t)1U | z12 >> (uint32_t)63U;




3,472✔






1602



  uint64_t v0 = z12 << (uint32_t)1U;




3,472✔






1603



  uint64_t v21 = v20 ^ (v0 ^ (v0 >> (uint32_t)1U ^ (v0 >> (uint32_t)2U ^ v0 >> (uint32_t)7U)));




3,472✔






1604



  uint64_t v11 = v1 ^ (v0 << (uint32_t)63U ^ (v0 << (uint32_t)62U ^ v0 << (uint32_t)57U));




3,472✔






1605



  uint64_t




3,472✔






1606



  v31 = v3 ^ (v11 ^ (v11 >> (uint32_t)1U ^ (v11 >> (uint32_t)2U ^ v11 >> (uint32_t)7U)));




3,472✔






1607



  uint64_t v22 = v21 ^ (v11 << (uint32_t)63U ^ (v11 << (uint32_t)62U ^ v11 << (uint32_t)57U));




3,472✔






1608



  uint64_t v10 = v22;




3,472✔






1609



  uint64_t v2 = v31;




3,472✔






1610



  acc[0U] = v10;




3,472✔






1611



  acc[1U] = v2;




3,472✔






1612



}




3,472✔





1613












1614



void Hacl_Gf128_CT64_gcm_init(uint64_t *ctx, uint8_t *key)











1615



{




6,014✔






1616



  uint64_t *acc = ctx;




6,014✔






1617



  uint64_t *pre = ctx + (uint32_t)2U;




6,014✔






1618



  acc[0U] = (uint64_t)0U;




6,014✔






1619



  acc[1U] = (uint64_t)0U;




6,014✔






1620



  load_precompute_r(pre, key);




6,014✔






1621



}




6,014✔





1622












1623



void Hacl_Gf128_CT64_gcm_update_blocks(uint64_t *ctx, uint32_t len, uint8_t *text)











1624



{




36,084✔






1625



  uint64_t *acc = ctx;




36,084✔






1626



  uint64_t *pre = ctx + (uint32_t)2U;




36,084✔






1627



  uint32_t len0 = len / (uint32_t)64U * (uint32_t)64U;




36,084✔






1628



  uint8_t *t0 = text;




36,084✔






1629



  if (len0 > (uint32_t)0U)




36,084✔






1630



  {




1,488✔






1631



    uint64_t f[8U] = { 0U };




1,488✔






1632



    uint64_t *b4 = f;




1,488✔






1633



    uint32_t nb = len0 / (uint32_t)64U;




1,488✔






1634



    for (uint32_t i = (uint32_t)0U; i < nb; i++)




4,960✔






1635



    {




3,472✔






1636



      uint8_t *tb = t0 + i * (uint32_t)64U;




3,472✔






1637



      uint64_t *x0 = b4;




3,472✔






1638



      uint8_t *y0 = tb;




3,472✔






1639



      uint64_t *x1 = b4 + (uint32_t)2U;




3,472✔






1640



      uint8_t *y1 = tb + (uint32_t)16U;




3,472✔






1641



      uint64_t *x2 = b4 + (uint32_t)4U;




3,472✔






1642



      uint8_t *y2 = tb + (uint32_t)32U;




3,472✔






1643



      uint64_t *x3 = b4 + (uint32_t)6U;




3,472✔






1644



      uint8_t *y3 = tb + (uint32_t)48U;




3,472✔






1645



      uint64_t u = load64_be(y0);




3,472✔






1646



      x0[1U] = u;




3,472✔






1647



      uint64_t u0 = load64_be(y0 + (uint32_t)8U);




3,472✔






1648



      x0[0U] = u0;




3,472✔






1649



      uint64_t u1 = load64_be(y1);




3,472✔






1650



      x1[1U] = u1;




3,472✔






1651



      uint64_t u2 = load64_be(y1 + (uint32_t)8U);




3,472✔






1652



      x1[0U] = u2;




3,472✔






1653



      uint64_t u3 = load64_be(y2);




3,472✔






1654



      x2[1U] = u3;




3,472✔






1655



      uint64_t u4 = load64_be(y2 + (uint32_t)8U);




3,472✔






1656



      x2[0U] = u4;




3,472✔






1657



      uint64_t u5 = load64_be(y3);




3,472✔






1658



      x3[1U] = u5;




3,472✔






1659



      uint64_t u6 = load64_be(y3 + (uint32_t)8U);




3,472✔






1660



      x3[0U] = u6;




3,472✔






1661



      uint64_t *uu____0 = b4;




3,472✔






1662



      uu____0[0U] = uu____0[0U] ^ acc[0U];




3,472✔






1663



      uu____0[1U] = uu____0[1U] ^ acc[1U];




3,472✔






1664



      normalize4(acc, b4, pre);




3,472✔






1665



    }




3,472✔






1666



  }




1,488✔






1667



  uint32_t len1 = len - len0;




36,084✔






1668



  uint8_t *t1 = text + len0;




36,084✔






1669



  uint64_t *r1 = pre + (uint32_t)6U;




36,084✔






1670



  uint32_t nb = len1 / (uint32_t)16U;




36,084✔






1671



  uint32_t rem = len1 % (uint32_t)16U;




36,084✔






1672



  for (uint32_t i = (uint32_t)0U; i < nb; i++)




58,776✔






1673



  {




22,692✔






1674



    uint8_t *tb = t1 + i * (uint32_t)16U;




22,692✔






1675



    uint64_t elem[2U] = { 0U };




22,692✔






1676



    uint64_t u = load64_be(tb);




22,692✔






1677



    elem[1U] = u;




22,692✔






1678



    uint64_t u0 = load64_be(tb + (uint32_t)8U);




22,692✔






1679



    elem[0U] = u0;




22,692✔






1680



    acc[0U] = acc[0U] ^ elem[0U];




22,692✔






1681



    acc[1U] = acc[1U] ^ elem[1U];




22,692✔






1682



    fmul0(acc, r1);




22,692✔






1683



  }




22,692✔






1684



  if (rem > (uint32_t)0U)




36,084✔






1685



  {




4,712✔






1686



    uint8_t *last = t1 + nb * (uint32_t)16U;




4,712✔






1687



    uint64_t elem[2U] = { 0U };




4,712✔






1688



    uint8_t b[16U] = { 0U };




4,712✔






1689



    memcpy(b, last, rem * sizeof (uint8_t));




4,712✔






1690



    uint64_t u = load64_be(b);




4,712✔






1691



    elem[1U] = u;




4,712✔






1692



    uint64_t u0 = load64_be(b + (uint32_t)8U);




4,712✔






1693



    elem[0U] = u0;




4,712✔






1694



    acc[0U] = acc[0U] ^ elem[0U];




4,712✔






1695



    acc[1U] = acc[1U] ^ elem[1U];




4,712✔






1696



    fmul0(acc, r1);




4,712✔






1697



    return;




4,712✔






1698



  }




4,712✔






1699



}




36,084✔





1700












1701



void










1702



(*Hacl_Gf128_CT64_gcm_update_blocks_padded)(uint64_t *x0, uint32_t x1, uint8_t *x2) =










1703



  Hacl_Gf128_CT64_gcm_update_blocks;










1704












1705



void Hacl_Gf128_CT64_gcm_emit(uint8_t *tag, uint64_t *ctx)











1706



{




12,028✔






1707



  uint64_t *acc = ctx;




12,028✔






1708



  uint64_t r0 = acc[1U];




12,028✔






1709



  uint64_t r1 = acc[0U];




12,028✔






1710



  store64_be(tag, r0);




12,028✔






1711



  store64_be(tag + (uint32_t)8U, r1);




12,028✔






1712



}




12,028✔





1713












1714



void Hacl_Gf128_CT64_ghash(uint8_t *tag, uint32_t len, uint8_t *text, uint8_t *key)











1715



{




×








1716



  uint64_t ctx[18U] = { 0U };




×








1717



  uint64_t *acc = ctx;




×








1718



  uint64_t *pre0 = ctx + (uint32_t)2U;




×








1719



  acc[0U] = (uint64_t)0U;




×








1720



  acc[1U] = (uint64_t)0U;




×








1721



  load_precompute_r(pre0, key);




×








1722



  uint64_t *acc0 = ctx;




×








1723



  uint64_t *pre = ctx + (uint32_t)2U;




×








1724



  uint32_t len0 = len / (uint32_t)64U * (uint32_t)64U;




×








1725



  uint8_t *t0 = text;




×








1726



  if (len0 > (uint32_t)0U)




×








1727



  {




×








1728



    uint64_t f[8U] = { 0U };




×








1729



    uint64_t *b4 = f;




×








1730



    uint32_t nb = len0 / (uint32_t)64U;




×








1731



    for (uint32_t i = (uint32_t)0U; i < nb; i++)




×








1732



    {




×








1733



      uint8_t *tb = t0 + i * (uint32_t)64U;




×








1734



      uint64_t *x0 = b4;




×








1735



      uint8_t *y0 = tb;




×








1736



      uint64_t *x1 = b4 + (uint32_t)2U;




×








1737



      uint8_t *y1 = tb + (uint32_t)16U;




×








1738



      uint64_t *x2 = b4 + (uint32_t)4U;




×








1739



      uint8_t *y2 = tb + (uint32_t)32U;




×








1740



      uint64_t *x3 = b4 + (uint32_t)6U;




×








1741



      uint8_t *y3 = tb + (uint32_t)48U;




×








1742



      uint64_t u = load64_be(y0);




×








1743



      x0[1U] = u;




×








1744



      uint64_t u0 = load64_be(y0 + (uint32_t)8U);




×








1745



      x0[0U] = u0;




×








1746



      uint64_t u1 = load64_be(y1);




×








1747



      x1[1U] = u1;




×








1748



      uint64_t u2 = load64_be(y1 + (uint32_t)8U);




×








1749



      x1[0U] = u2;




×








1750



      uint64_t u3 = load64_be(y2);




×








1751



      x2[1U] = u3;




×








1752



      uint64_t u4 = load64_be(y2 + (uint32_t)8U);




×








1753



      x2[0U] = u4;




×








1754



      uint64_t u5 = load64_be(y3);




×








1755



      x3[1U] = u5;




×








1756



      uint64_t u6 = load64_be(y3 + (uint32_t)8U);




×








1757



      x3[0U] = u6;




×








1758



      uint64_t *uu____0 = b4;




×








1759



      uu____0[0U] = uu____0[0U] ^ acc0[0U];




×








1760



      uu____0[1U] = uu____0[1U] ^ acc0[1U];




×








1761



      normalize4(acc0, b4, pre);




×








1762



    }




×








1763



  }




×








1764



  uint32_t len1 = len - len0;




×








1765



  uint8_t *t1 = text + len0;




×








1766



  uint64_t *r10 = pre + (uint32_t)6U;




×








1767



  uint32_t nb = len1 / (uint32_t)16U;




×








1768



  uint32_t rem = len1 % (uint32_t)16U;




×








1769



  for (uint32_t i = (uint32_t)0U; i < nb; i++)




×








1770



  {




×








1771



    uint8_t *tb = t1 + i * (uint32_t)16U;




×








1772



    uint64_t elem[2U] = { 0U };




×








1773



    uint64_t u = load64_be(tb);




×








1774



    elem[1U] = u;




×








1775



    uint64_t u0 = load64_be(tb + (uint32_t)8U);




×








1776



    elem[0U] = u0;




×








1777



    acc0[0U] = acc0[0U] ^ elem[0U];




×








1778



    acc0[1U] = acc0[1U] ^ elem[1U];




×








1779



    fmul0(acc0, r10);




×








1780



  }




×








1781



  if (rem > (uint32_t)0U)




×








1782



  {




×








1783



    uint8_t *last = t1 + nb * (uint32_t)16U;




×








1784



    uint64_t elem[2U] = { 0U };




×








1785



    uint8_t b[16U] = { 0U };




×








1786



    memcpy(b, last, rem * sizeof (uint8_t));




×








1787



    uint64_t u = load64_be(b);




×








1788



    elem[1U] = u;




×








1789



    uint64_t u0 = load64_be(b + (uint32_t)8U);




×








1790



    elem[0U] = u0;




×








1791



    acc0[0U] = acc0[0U] ^ elem[0U];




×








1792



    acc0[1U] = acc0[1U] ^ elem[1U];




×








1793



    fmul0(acc0, r10);




×








1794



  }




×








1795



  uint64_t *acc1 = ctx;




×








1796



  uint64_t r0 = acc1[1U];




×








1797



  uint64_t r1 = acc1[0U];




×








1798



  store64_be(tag, r0);




×








1799



  store64_be(tag + (uint32_t)8U, r1);




×








1800



}




×







1801


























    

  • 

    •