From 4441785fb44b88bb6943ddbf639d872c8c903281 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 16 Jan 2019 00:24:19 -0500 Subject: Constant-propogate 0+x and x+0 after bounds After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m22.67s | Total | 21m28.24s || -0m05.56s | -0.43% -------------------------------------------------------------------------------------------- 4m09.95s | PushButtonSynthesis.vo | 4m14.76s || -0m04.81s | -1.88% 3m07.95s | p384_32.c | 3m11.17s || -0m03.21s | -1.68% 2m06.43s | Rewriter.vo | 2m06.15s || +0m00.28s | +0.22% 1m55.83s | RewriterWf2.vo | 1m56.15s || -0m00.32s | -0.27% 1m52.36s | RewriterRulesGood.vo | 1m52.34s || +0m00.01s | +0.01% 1m46.52s | RewriterRulesInterpGood.vo | 1m45.70s || +0m00.82s | +0.77% 0m46.56s | RewriterInterpProofs1.vo | 0m46.72s || -0m00.15s | -0.34% 0m45.04s | ExtractionHaskell/word_by_word_montgomery | 0m45.33s || -0m00.28s | -0.63% 0m39.17s | p521_32.c | 0m39.07s || +0m00.10s | +0.25% 0m32.40s | p521_64.c | 0m32.64s || -0m00.24s | -0.73% 0m31.13s | ExtractionHaskell/unsaturated_solinas | 0m30.88s || +0m00.25s | +0.80% 0m24.20s | ExtractionHaskell/saturated_solinas | 0m24.27s || -0m00.07s | -0.28% 0m23.72s | RewriterWf1.vo | 0m23.42s || +0m00.29s | +1.28% 0m17.52s | ExtractionOCaml/word_by_word_montgomery | 0m17.10s || +0m00.41s | +2.45% 0m13.39s | secp256k1_32.c | 0m13.29s || +0m00.10s | +0.75% 0m13.08s | p256_32.c | 0m13.26s || -0m00.17s | -1.35% 0m11.49s | p484_64.c | 0m11.18s || +0m00.31s | +2.77% 0m10.68s | ExtractionOCaml/unsaturated_solinas | 0m10.64s || +0m00.03s | +0.37% 0m10.11s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.10s || +0m00.00s | +0.09% 0m07.96s | ExtractionOCaml/saturated_solinas | 0m07.95s || +0m00.00s | +0.12% 0m06.81s | ExtractionOCaml/unsaturated_solinas.ml | 0m06.76s || +0m00.04s | +0.73% 0m06.30s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.26s || +0m00.04s | +0.63% 0m06.07s | p224_32.c | 0m05.94s || +0m00.12s | +2.18% 0m06.06s | BoundsPipeline.vo | 0m06.08s || -0m00.02s | -0.32% 0m05.46s | p384_64.c | 0m05.30s || +0m00.16s | +3.01% 0m05.28s | ExtractionOCaml/saturated_solinas.ml | 0m05.18s || +0m00.10s | +1.93% 0m04.97s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.99s || -0m00.02s | -0.40% 0m04.13s | ExtractionHaskell/saturated_solinas.hs | 0m04.10s || +0m00.03s | +0.73% 0m02.34s | curve25519_32.c | 0m02.21s || +0m00.12s | +5.88% 0m01.59s | curve25519_64.c | 0m01.47s || +0m00.12s | +8.16% 0m01.46s | CLI.vo | 0m01.48s || -0m00.02s | -1.35% 0m01.15s | secp256k1_64.c | 0m01.03s || +0m00.11s | +11.65% 0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88% 0m01.14s | StandaloneHaskellMain.vo | 0m01.09s || +0m00.04s | +4.58% 0m01.14s | StandaloneOCamlMain.vo | 0m01.12s || +0m00.01s | +1.78% 0m01.09s | p256_64.c | 0m00.98s || +0m00.11s | +11.22% 0m01.06s | p224_64.c | 0m01.00s || +0m00.06s | +6.00% --- p521_32.c | 326 +++++++++++++++++++++++++++++++------------------------------- 1 file changed, 161 insertions(+), 165 deletions(-) (limited to 'p521_32.c') diff --git a/p521_32.c b/p521_32.c index b044dc804..7d929b584 100644 --- a/p521_32.c +++ b/p521_32.c @@ -1201,100 +1201,98 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint32_t arg1[17]) { uint8_t x131 = (uint8_t)(x129 >> 8); uint8_t x132 = (uint8_t)(x129 & UINT8_C(0xff)); uint8_t x133 = (uint8_t)(x131 & UINT8_C(0xff)); - uint32_t x134 = (0x0 + x48); - uint32_t x135 = (x134 >> 8); - uint8_t x136 = (uint8_t)(x134 & UINT8_C(0xff)); - uint32_t x137 = (x135 >> 8); - uint8_t x138 = (uint8_t)(x135 & UINT8_C(0xff)); - uint8_t x139 = (uint8_t)(x137 >> 8); - uint8_t x140 = (uint8_t)(x137 & UINT8_C(0xff)); - uint64_t x141 = (x139 + x78); - uint32_t x142 = (uint32_t)(x141 >> 8); - uint8_t x143 = (uint8_t)(x141 & UINT8_C(0xff)); - uint32_t x144 = (x142 >> 8); - uint8_t x145 = (uint8_t)(x142 & UINT8_C(0xff)); - uint32_t x146 = (x144 >> 8); - uint8_t x147 = (uint8_t)(x144 & UINT8_C(0xff)); - uint8_t x148 = (uint8_t)(x146 >> 8); - uint8_t x149 = (uint8_t)(x146 & UINT8_C(0xff)); - uint64_t x150 = (x148 + x77); - uint32_t x151 = (uint32_t)(x150 >> 8); - uint8_t x152 = (uint8_t)(x150 & UINT8_C(0xff)); - uint32_t x153 = (x151 >> 8); - uint8_t x154 = (uint8_t)(x151 & UINT8_C(0xff)); - uint32_t x155 = (x153 >> 8); - uint8_t x156 = (uint8_t)(x153 & UINT8_C(0xff)); - uint8_t x157 = (uint8_t)(x155 >> 8); - uint8_t x158 = (uint8_t)(x155 & UINT8_C(0xff)); - uint64_t x159 = (x157 + x76); - uint32_t x160 = (uint32_t)(x159 >> 8); - uint8_t x161 = (uint8_t)(x159 & UINT8_C(0xff)); - uint32_t x162 = (x160 >> 8); - uint8_t x163 = (uint8_t)(x160 & UINT8_C(0xff)); - uint32_t x164 = (x162 >> 8); - uint8_t x165 = (uint8_t)(x162 & UINT8_C(0xff)); - uint8_t x166 = (uint8_t)(x164 >> 8); - uint8_t x167 = (uint8_t)(x164 & UINT8_C(0xff)); - uint64_t x168 = (x166 + x75); - uint32_t x169 = (uint32_t)(x168 >> 8); - uint8_t x170 = (uint8_t)(x168 & UINT8_C(0xff)); - uint32_t x171 = (x169 >> 8); - uint8_t x172 = (uint8_t)(x169 & UINT8_C(0xff)); - uint32_t x173 = (x171 >> 8); - uint8_t x174 = (uint8_t)(x171 & UINT8_C(0xff)); - uint8_t x175 = (uint8_t)(x173 >> 8); - uint8_t x176 = (uint8_t)(x173 & UINT8_C(0xff)); - uint32_t x177 = (x175 + x74); - uint32_t x178 = (x177 >> 8); - uint8_t x179 = (uint8_t)(x177 & UINT8_C(0xff)); - uint32_t x180 = (x178 >> 8); - uint8_t x181 = (uint8_t)(x178 & UINT8_C(0xff)); - uint8_t x182 = (uint8_t)(x180 >> 8); - uint8_t x183 = (uint8_t)(x180 & UINT8_C(0xff)); - uint8_t x184 = (uint8_t)(x182 & UINT8_C(0xff)); - uint32_t x185 = (0x0 + x60); - uint32_t x186 = (x185 >> 8); - uint8_t x187 = (uint8_t)(x185 & UINT8_C(0xff)); - uint32_t x188 = (x186 >> 8); + uint32_t x134 = (x48 >> 8); + uint8_t x135 = (uint8_t)(x48 & UINT8_C(0xff)); + uint32_t x136 = (x134 >> 8); + uint8_t x137 = (uint8_t)(x134 & UINT8_C(0xff)); + uint8_t x138 = (uint8_t)(x136 >> 8); + uint8_t x139 = (uint8_t)(x136 & UINT8_C(0xff)); + uint64_t x140 = (x138 + x78); + uint32_t x141 = (uint32_t)(x140 >> 8); + uint8_t x142 = (uint8_t)(x140 & UINT8_C(0xff)); + uint32_t x143 = (x141 >> 8); + uint8_t x144 = (uint8_t)(x141 & UINT8_C(0xff)); + uint32_t x145 = (x143 >> 8); + uint8_t x146 = (uint8_t)(x143 & UINT8_C(0xff)); + uint8_t x147 = (uint8_t)(x145 >> 8); + uint8_t x148 = (uint8_t)(x145 & UINT8_C(0xff)); + uint64_t x149 = (x147 + x77); + uint32_t x150 = (uint32_t)(x149 >> 8); + uint8_t x151 = (uint8_t)(x149 & UINT8_C(0xff)); + uint32_t x152 = (x150 >> 8); + uint8_t x153 = (uint8_t)(x150 & UINT8_C(0xff)); + uint32_t x154 = (x152 >> 8); + uint8_t x155 = (uint8_t)(x152 & UINT8_C(0xff)); + uint8_t x156 = (uint8_t)(x154 >> 8); + uint8_t x157 = (uint8_t)(x154 & UINT8_C(0xff)); + uint64_t x158 = (x156 + x76); + uint32_t x159 = (uint32_t)(x158 >> 8); + uint8_t x160 = (uint8_t)(x158 & UINT8_C(0xff)); + uint32_t x161 = (x159 >> 8); + uint8_t x162 = (uint8_t)(x159 & UINT8_C(0xff)); + uint32_t x163 = (x161 >> 8); + uint8_t x164 = (uint8_t)(x161 & UINT8_C(0xff)); + uint8_t x165 = (uint8_t)(x163 >> 8); + uint8_t x166 = (uint8_t)(x163 & UINT8_C(0xff)); + uint64_t x167 = (x165 + x75); + uint32_t x168 = (uint32_t)(x167 >> 8); + uint8_t x169 = (uint8_t)(x167 & UINT8_C(0xff)); + uint32_t x170 = (x168 >> 8); + uint8_t x171 = (uint8_t)(x168 & UINT8_C(0xff)); + uint32_t x172 = (x170 >> 8); + uint8_t x173 = (uint8_t)(x170 & UINT8_C(0xff)); + uint8_t x174 = (uint8_t)(x172 >> 8); + uint8_t x175 = (uint8_t)(x172 & UINT8_C(0xff)); + uint32_t x176 = (x174 + x74); + uint32_t x177 = (x176 >> 8); + uint8_t x178 = (uint8_t)(x176 & UINT8_C(0xff)); + uint32_t x179 = (x177 >> 8); + uint8_t x180 = (uint8_t)(x177 & UINT8_C(0xff)); + uint8_t x181 = (uint8_t)(x179 >> 8); + uint8_t x182 = (uint8_t)(x179 & UINT8_C(0xff)); + uint8_t x183 = (uint8_t)(x181 & UINT8_C(0xff)); + uint32_t x184 = (x60 >> 8); + uint8_t x185 = (uint8_t)(x60 & UINT8_C(0xff)); + uint32_t x186 = (x184 >> 8); + uint8_t x187 = (uint8_t)(x184 & UINT8_C(0xff)); + uint8_t x188 = (uint8_t)(x186 >> 8); uint8_t x189 = (uint8_t)(x186 & UINT8_C(0xff)); - uint8_t x190 = (uint8_t)(x188 >> 8); - uint8_t x191 = (uint8_t)(x188 & UINT8_C(0xff)); - uint64_t x192 = (x190 + x73); - uint32_t x193 = (uint32_t)(x192 >> 8); - uint8_t x194 = (uint8_t)(x192 & UINT8_C(0xff)); + uint64_t x190 = (x188 + x73); + uint32_t x191 = (uint32_t)(x190 >> 8); + uint8_t x192 = (uint8_t)(x190 & UINT8_C(0xff)); + uint32_t x193 = (x191 >> 8); + uint8_t x194 = (uint8_t)(x191 & UINT8_C(0xff)); uint32_t x195 = (x193 >> 8); uint8_t x196 = (uint8_t)(x193 & UINT8_C(0xff)); - uint32_t x197 = (x195 >> 8); + uint8_t x197 = (uint8_t)(x195 >> 8); uint8_t x198 = (uint8_t)(x195 & UINT8_C(0xff)); - uint8_t x199 = (uint8_t)(x197 >> 8); - uint8_t x200 = (uint8_t)(x197 & UINT8_C(0xff)); - uint64_t x201 = (x199 + x72); - uint32_t x202 = (uint32_t)(x201 >> 8); - uint8_t x203 = (uint8_t)(x201 & UINT8_C(0xff)); + uint64_t x199 = (x197 + x72); + uint32_t x200 = (uint32_t)(x199 >> 8); + uint8_t x201 = (uint8_t)(x199 & UINT8_C(0xff)); + uint32_t x202 = (x200 >> 8); + uint8_t x203 = (uint8_t)(x200 & UINT8_C(0xff)); uint32_t x204 = (x202 >> 8); uint8_t x205 = (uint8_t)(x202 & UINT8_C(0xff)); - uint32_t x206 = (x204 >> 8); + uint8_t x206 = (uint8_t)(x204 >> 8); uint8_t x207 = (uint8_t)(x204 & UINT8_C(0xff)); - uint8_t x208 = (uint8_t)(x206 >> 8); - uint8_t x209 = (uint8_t)(x206 & UINT8_C(0xff)); - uint64_t x210 = (x208 + x71); - uint32_t x211 = (uint32_t)(x210 >> 8); - uint8_t x212 = (uint8_t)(x210 & UINT8_C(0xff)); + uint64_t x208 = (x206 + x71); + uint32_t x209 = (uint32_t)(x208 >> 8); + uint8_t x210 = (uint8_t)(x208 & UINT8_C(0xff)); + uint32_t x211 = (x209 >> 8); + uint8_t x212 = (uint8_t)(x209 & UINT8_C(0xff)); uint32_t x213 = (x211 >> 8); uint8_t x214 = (uint8_t)(x211 & UINT8_C(0xff)); - uint32_t x215 = (x213 >> 8); + uint8_t x215 = (uint8_t)(x213 >> 8); uint8_t x216 = (uint8_t)(x213 & UINT8_C(0xff)); - uint8_t x217 = (uint8_t)(x215 >> 8); - uint8_t x218 = (uint8_t)(x215 & UINT8_C(0xff)); - uint64_t x219 = (x217 + x70); - uint32_t x220 = (uint32_t)(x219 >> 8); - uint8_t x221 = (uint8_t)(x219 & UINT8_C(0xff)); + uint64_t x217 = (x215 + x70); + uint32_t x218 = (uint32_t)(x217 >> 8); + uint8_t x219 = (uint8_t)(x217 & UINT8_C(0xff)); + uint32_t x220 = (x218 >> 8); + uint8_t x221 = (uint8_t)(x218 & UINT8_C(0xff)); uint32_t x222 = (x220 >> 8); uint8_t x223 = (uint8_t)(x220 & UINT8_C(0xff)); - uint32_t x224 = (x222 >> 8); + fiat_p521_uint1 x224 = (fiat_p521_uint1)(x222 >> 8); uint8_t x225 = (uint8_t)(x222 & UINT8_C(0xff)); - fiat_p521_uint1 x226 = (fiat_p521_uint1)(x224 >> 8); - uint8_t x227 = (uint8_t)(x224 & UINT8_C(0xff)); out1[0] = x85; out1[1] = x87; out1[2] = x89; @@ -1318,49 +1316,49 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint32_t arg1[17]) { out1[20] = x130; out1[21] = x132; out1[22] = x133; - out1[23] = x136; - out1[24] = x138; - out1[25] = x140; - out1[26] = x143; - out1[27] = x145; - out1[28] = x147; - out1[29] = x149; - out1[30] = x152; - out1[31] = x154; - out1[32] = x156; - out1[33] = x158; - out1[34] = x161; - out1[35] = x163; - out1[36] = x165; - out1[37] = x167; - out1[38] = x170; - out1[39] = x172; - out1[40] = x174; - out1[41] = x176; - out1[42] = x179; - out1[43] = x181; - out1[44] = x183; - out1[45] = x184; - out1[46] = x187; - out1[47] = x189; - out1[48] = x191; - out1[49] = x194; - out1[50] = x196; - out1[51] = x198; - out1[52] = x200; - out1[53] = x203; - out1[54] = x205; - out1[55] = x207; - out1[56] = x209; - out1[57] = x212; - out1[58] = x214; - out1[59] = x216; - out1[60] = x218; - out1[61] = x221; - out1[62] = x223; - out1[63] = x225; - out1[64] = x227; - out1[65] = x226; + out1[23] = x135; + out1[24] = x137; + out1[25] = x139; + out1[26] = x142; + out1[27] = x144; + out1[28] = x146; + out1[29] = x148; + out1[30] = x151; + out1[31] = x153; + out1[32] = x155; + out1[33] = x157; + out1[34] = x160; + out1[35] = x162; + out1[36] = x164; + out1[37] = x166; + out1[38] = x169; + out1[39] = x171; + out1[40] = x173; + out1[41] = x175; + out1[42] = x178; + out1[43] = x180; + out1[44] = x182; + out1[45] = x183; + out1[46] = x185; + out1[47] = x187; + out1[48] = x189; + out1[49] = x192; + out1[50] = x194; + out1[51] = x196; + out1[52] = x198; + out1[53] = x201; + out1[54] = x203; + out1[55] = x205; + out1[56] = x207; + out1[57] = x210; + out1[58] = x212; + out1[59] = x214; + out1[60] = x216; + out1[61] = x219; + out1[62] = x221; + out1[63] = x223; + out1[64] = x225; + out1[65] = x224; } /* @@ -1469,52 +1467,50 @@ static void fiat_p521_from_bytes(uint32_t out1[17], const uint8_t arg1[66]) { uint32_t x97 = (uint32_t)(x95 & UINT32_C(0x7fffffff)); uint32_t x98 = (x96 + x81); uint32_t x99 = (x98 & UINT32_C(0x3fffffff)); - uint32_t x100 = (0x0 + x80); - fiat_p521_uint1 x101 = (fiat_p521_uint1)(x100 >> 31); - uint32_t x102 = (x100 & UINT32_C(0x7fffffff)); - uint64_t x103 = (x101 + x79); - uint8_t x104 = (uint8_t)(x103 >> 31); - uint32_t x105 = (uint32_t)(x103 & UINT32_C(0x7fffffff)); - uint64_t x106 = (x104 + x78); - uint8_t x107 = (uint8_t)(x106 >> 30); - uint32_t x108 = (uint32_t)(x106 & UINT32_C(0x3fffffff)); - uint64_t x109 = (x107 + x77); - uint8_t x110 = (uint8_t)(x109 >> 31); - uint32_t x111 = (uint32_t)(x109 & UINT32_C(0x7fffffff)); - uint64_t x112 = (x110 + x76); - uint8_t x113 = (uint8_t)(x112 >> 31); - uint32_t x114 = (uint32_t)(x112 & UINT32_C(0x7fffffff)); - uint32_t x115 = (x113 + x75); - uint32_t x116 = (x115 & UINT32_C(0x3fffffff)); - uint32_t x117 = (0x0 + x74); - fiat_p521_uint1 x118 = (fiat_p521_uint1)(x117 >> 31); - uint32_t x119 = (x117 & UINT32_C(0x7fffffff)); - uint64_t x120 = (x118 + x73); - uint8_t x121 = (uint8_t)(x120 >> 31); - uint32_t x122 = (uint32_t)(x120 & UINT32_C(0x7fffffff)); - uint64_t x123 = (x121 + x72); - uint8_t x124 = (uint8_t)(x123 >> 30); - uint32_t x125 = (uint32_t)(x123 & UINT32_C(0x3fffffff)); - uint64_t x126 = (x124 + x71); - uint8_t x127 = (uint8_t)(x126 >> 31); - uint32_t x128 = (uint32_t)(x126 & UINT32_C(0x7fffffff)); - uint32_t x129 = (x127 + x70); + fiat_p521_uint1 x100 = (fiat_p521_uint1)(x80 >> 31); + uint32_t x101 = (x80 & UINT32_C(0x7fffffff)); + uint64_t x102 = (x100 + x79); + uint8_t x103 = (uint8_t)(x102 >> 31); + uint32_t x104 = (uint32_t)(x102 & UINT32_C(0x7fffffff)); + uint64_t x105 = (x103 + x78); + uint8_t x106 = (uint8_t)(x105 >> 30); + uint32_t x107 = (uint32_t)(x105 & UINT32_C(0x3fffffff)); + uint64_t x108 = (x106 + x77); + uint8_t x109 = (uint8_t)(x108 >> 31); + uint32_t x110 = (uint32_t)(x108 & UINT32_C(0x7fffffff)); + uint64_t x111 = (x109 + x76); + uint8_t x112 = (uint8_t)(x111 >> 31); + uint32_t x113 = (uint32_t)(x111 & UINT32_C(0x7fffffff)); + uint32_t x114 = (x112 + x75); + uint32_t x115 = (x114 & UINT32_C(0x3fffffff)); + fiat_p521_uint1 x116 = (fiat_p521_uint1)(x74 >> 31); + uint32_t x117 = (x74 & UINT32_C(0x7fffffff)); + uint64_t x118 = (x116 + x73); + uint8_t x119 = (uint8_t)(x118 >> 31); + uint32_t x120 = (uint32_t)(x118 & UINT32_C(0x7fffffff)); + uint64_t x121 = (x119 + x72); + uint8_t x122 = (uint8_t)(x121 >> 30); + uint32_t x123 = (uint32_t)(x121 & UINT32_C(0x3fffffff)); + uint64_t x124 = (x122 + x71); + uint8_t x125 = (uint8_t)(x124 >> 31); + uint32_t x126 = (uint32_t)(x124 & UINT32_C(0x7fffffff)); + uint32_t x127 = (x125 + x70); out1[0] = x69; out1[1] = x88; out1[2] = x91; out1[3] = x94; out1[4] = x97; out1[5] = x99; - out1[6] = x102; - out1[7] = x105; - out1[8] = x108; - out1[9] = x111; - out1[10] = x114; - out1[11] = x116; - out1[12] = x119; - out1[13] = x122; - out1[14] = x125; - out1[15] = x128; - out1[16] = x129; + out1[6] = x101; + out1[7] = x104; + out1[8] = x107; + out1[9] = x110; + out1[10] = x113; + out1[11] = x115; + out1[12] = x117; + out1[13] = x120; + out1[14] = x123; + out1[15] = x126; + out1[16] = x127; } -- cgit v1.2.3