From 60bade02ccd577550bfcd5974d3c62a3d40e751a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 15 Jan 2019 15:53:34 -0500 Subject: Add a rewrite rule to collapse constant casts If, e.g., we know from bounds analysis that the result of an operation fits in the range r[0~>0], we now just replace it with the literal constant. Fixes #493 After | File Name | Before || Change | % Change -------------------------------------------------------------------------------------------- 21m22.14s | Total | 21m22.79s || -0m00.65s | -0.05% -------------------------------------------------------------------------------------------- 4m09.97s | PushButtonSynthesis.vo | 4m10.56s || -0m00.59s | -0.23% 3m09.12s | p384_32.c | 3m08.91s || +0m00.21s | +0.11% 2m05.94s | Rewriter.vo | 2m06.30s || -0m00.35s | -0.28% 1m56.58s | RewriterWf2.vo | 1m56.09s || +0m00.48s | +0.42% 1m52.39s | RewriterRulesGood.vo | 1m52.04s || +0m00.35s | +0.31% 1m46.01s | RewriterRulesInterpGood.vo | 1m45.79s || +0m00.21s | +0.20% 0m46.44s | RewriterInterpProofs1.vo | 0m46.47s || -0m00.03s | -0.06% 0m44.96s | ExtractionHaskell/word_by_word_montgomery | 0m45.59s || -0m00.63s | -1.38% 0m39.18s | p521_32.c | 0m39.33s || -0m00.14s | -0.38% 0m32.41s | p521_64.c | 0m32.54s || -0m00.13s | -0.39% 0m30.87s | ExtractionHaskell/unsaturated_solinas | 0m30.67s || +0m00.19s | +0.65% 0m24.32s | ExtractionHaskell/saturated_solinas | 0m24.44s || -0m00.12s | -0.49% 0m23.59s | RewriterWf1.vo | 0m24.10s || -0m00.51s | -2.11% 0m17.01s | ExtractionOCaml/word_by_word_montgomery | 0m17.14s || -0m00.12s | -0.75% 0m13.48s | secp256k1_32.c | 0m13.30s || +0m00.17s | +1.35% 0m13.11s | p256_32.c | 0m13.37s || -0m00.25s | -1.94% 0m11.34s | p484_64.c | 0m11.34s || +0m00.00s | +0.00% 0m10.78s | ExtractionOCaml/unsaturated_solinas | 0m10.79s || -0m00.00s | -0.09% 0m10.27s | ExtractionOCaml/word_by_word_montgomery.ml | 0m10.06s || +0m00.20s | +2.08% 0m08.11s | ExtractionOCaml/saturated_solinas | 0m07.92s || +0m00.18s | +2.39% 0m06.92s | ExtractionOCaml/unsaturated_solinas.ml | 0m07.02s || -0m00.09s | -1.42% 0m06.18s | ExtractionHaskell/word_by_word_montgomery.hs | 0m06.28s || -0m00.10s | -1.59% 0m06.13s | BoundsPipeline.vo | 0m05.98s || +0m00.14s | +2.50% 0m05.90s | p224_32.c | 0m05.92s || -0m00.01s | -0.33% 0m05.29s | p384_64.c | 0m05.33s || -0m00.04s | -0.75% 0m05.17s | ExtractionOCaml/saturated_solinas.ml | 0m05.20s || -0m00.03s | -0.57% 0m04.91s | ExtractionHaskell/unsaturated_solinas.hs | 0m04.93s || -0m00.01s | -0.40% 0m04.06s | ExtractionHaskell/saturated_solinas.hs | 0m04.00s || +0m00.05s | +1.49% 0m02.21s | curve25519_32.c | 0m02.22s || -0m00.01s | -0.45% 0m01.52s | curve25519_64.c | 0m01.50s || +0m00.02s | +1.33% 0m01.38s | CLI.vo | 0m01.42s || -0m00.04s | -2.81% 0m01.14s | RewriterProofs.vo | 0m01.13s || +0m00.01s | +0.88% 0m01.14s | StandaloneOCamlMain.vo | 0m00.96s || +0m00.17s | +18.74% 0m01.12s | StandaloneHaskellMain.vo | 0m01.03s || +0m00.09s | +8.73% 0m01.12s | secp256k1_64.c | 0m01.00s || +0m00.12s | +12.00% 0m01.05s | p256_64.c | 0m00.98s || +0m00.07s | +7.14% 0m01.03s | p224_64.c | 0m01.15s || -0m00.11s | -10.43% --- p521_64.c | 254 +++++++++++++++++++++++++++++++------------------------------- 1 file changed, 125 insertions(+), 129 deletions(-) (limited to 'p521_64.c') diff --git a/p521_64.c b/p521_64.c index f81fa7967..08ba9e1b7 100644 --- a/p521_64.c +++ b/p521_64.c @@ -646,73 +646,73 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) { uint8_t x100 = (uint8_t)(x97 & UINT8_C(0xff)); uint8_t x101 = (uint8_t)(x99 >> 8); uint8_t x102 = (uint8_t)(x99 & UINT8_C(0xff)); - fiat_p521_uint1 x103 = (fiat_p521_uint1)(x101 >> 8); - uint8_t x104 = (uint8_t)(x101 & UINT8_C(0xff)); - uint64_t x105 = (x103 + x28); - uint64_t x106 = (x105 >> 8); - uint8_t x107 = (uint8_t)(x105 & UINT8_C(0xff)); - uint64_t x108 = (x106 >> 8); - uint8_t x109 = (uint8_t)(x106 & UINT8_C(0xff)); - uint64_t x110 = (x108 >> 8); - uint8_t x111 = (uint8_t)(x108 & UINT8_C(0xff)); - uint64_t x112 = (x110 >> 8); - uint8_t x113 = (uint8_t)(x110 & UINT8_C(0xff)); - uint64_t x114 = (x112 >> 8); - uint8_t x115 = (uint8_t)(x112 & UINT8_C(0xff)); - uint64_t x116 = (x114 >> 8); - uint8_t x117 = (uint8_t)(x114 & UINT8_C(0xff)); - uint8_t x118 = (uint8_t)(x116 >> 8); - uint8_t x119 = (uint8_t)(x116 & UINT8_C(0xff)); - uint64_t x120 = (x118 + x40); - uint64_t x121 = (x120 >> 8); - uint8_t x122 = (uint8_t)(x120 & UINT8_C(0xff)); - uint64_t x123 = (x121 >> 8); - uint8_t x124 = (uint8_t)(x121 & UINT8_C(0xff)); - uint64_t x125 = (x123 >> 8); - uint8_t x126 = (uint8_t)(x123 & UINT8_C(0xff)); - uint64_t x127 = (x125 >> 8); - uint8_t x128 = (uint8_t)(x125 & UINT8_C(0xff)); - uint64_t x129 = (x127 >> 8); - uint8_t x130 = (uint8_t)(x127 & UINT8_C(0xff)); - uint64_t x131 = (x129 >> 8); - uint8_t x132 = (uint8_t)(x129 & UINT8_C(0xff)); - uint8_t x133 = (uint8_t)(x131 >> 8); - uint8_t x134 = (uint8_t)(x131 & UINT8_C(0xff)); - uint64_t x135 = (x133 + x39); - uint64_t x136 = (x135 >> 8); - uint8_t x137 = (uint8_t)(x135 & UINT8_C(0xff)); - uint64_t x138 = (x136 >> 8); - uint8_t x139 = (uint8_t)(x136 & UINT8_C(0xff)); - uint64_t x140 = (x138 >> 8); - uint8_t x141 = (uint8_t)(x138 & UINT8_C(0xff)); - uint64_t x142 = (x140 >> 8); - uint8_t x143 = (uint8_t)(x140 & UINT8_C(0xff)); - uint64_t x144 = (x142 >> 8); - uint8_t x145 = (uint8_t)(x142 & UINT8_C(0xff)); - uint64_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 + x38); - uint64_t x151 = (x150 >> 8); - uint8_t x152 = (uint8_t)(x150 & UINT8_C(0xff)); - uint64_t x153 = (x151 >> 8); - uint8_t x154 = (uint8_t)(x151 & UINT8_C(0xff)); - uint64_t x155 = (x153 >> 8); - uint8_t x156 = (uint8_t)(x153 & UINT8_C(0xff)); - uint64_t x157 = (x155 >> 8); - uint8_t x158 = (uint8_t)(x155 & UINT8_C(0xff)); - uint64_t x159 = (x157 >> 8); - uint8_t x160 = (uint8_t)(x157 & UINT8_C(0xff)); - uint64_t x161 = (x159 >> 8); - uint8_t x162 = (uint8_t)(x159 & UINT8_C(0xff)); - uint8_t x163 = (uint8_t)(x161 >> 8); - uint8_t x164 = (uint8_t)(x161 & UINT8_C(0xff)); - fiat_p521_uint1 x165 = (fiat_p521_uint1)(x163 >> 8); - uint8_t x166 = (uint8_t)(x163 & UINT8_C(0xff)); - uint64_t x167 = (x165 + x36); - uint64_t x168 = (x167 >> 8); - uint8_t x169 = (uint8_t)(x167 & UINT8_C(0xff)); + uint8_t x103 = (uint8_t)(x101 & UINT8_C(0xff)); + uint64_t x104 = (0x0 + x28); + uint64_t x105 = (x104 >> 8); + uint8_t x106 = (uint8_t)(x104 & UINT8_C(0xff)); + uint64_t x107 = (x105 >> 8); + uint8_t x108 = (uint8_t)(x105 & UINT8_C(0xff)); + uint64_t x109 = (x107 >> 8); + uint8_t x110 = (uint8_t)(x107 & UINT8_C(0xff)); + uint64_t x111 = (x109 >> 8); + uint8_t x112 = (uint8_t)(x109 & UINT8_C(0xff)); + uint64_t x113 = (x111 >> 8); + uint8_t x114 = (uint8_t)(x111 & UINT8_C(0xff)); + uint64_t x115 = (x113 >> 8); + uint8_t x116 = (uint8_t)(x113 & UINT8_C(0xff)); + uint8_t x117 = (uint8_t)(x115 >> 8); + uint8_t x118 = (uint8_t)(x115 & UINT8_C(0xff)); + uint64_t x119 = (x117 + x40); + uint64_t x120 = (x119 >> 8); + uint8_t x121 = (uint8_t)(x119 & UINT8_C(0xff)); + uint64_t x122 = (x120 >> 8); + uint8_t x123 = (uint8_t)(x120 & UINT8_C(0xff)); + uint64_t x124 = (x122 >> 8); + uint8_t x125 = (uint8_t)(x122 & UINT8_C(0xff)); + uint64_t x126 = (x124 >> 8); + uint8_t x127 = (uint8_t)(x124 & UINT8_C(0xff)); + uint64_t x128 = (x126 >> 8); + uint8_t x129 = (uint8_t)(x126 & UINT8_C(0xff)); + uint64_t x130 = (x128 >> 8); + uint8_t x131 = (uint8_t)(x128 & UINT8_C(0xff)); + uint8_t x132 = (uint8_t)(x130 >> 8); + uint8_t x133 = (uint8_t)(x130 & UINT8_C(0xff)); + uint64_t x134 = (x132 + x39); + uint64_t x135 = (x134 >> 8); + uint8_t x136 = (uint8_t)(x134 & UINT8_C(0xff)); + uint64_t x137 = (x135 >> 8); + uint8_t x138 = (uint8_t)(x135 & UINT8_C(0xff)); + uint64_t x139 = (x137 >> 8); + uint8_t x140 = (uint8_t)(x137 & UINT8_C(0xff)); + uint64_t x141 = (x139 >> 8); + uint8_t x142 = (uint8_t)(x139 & UINT8_C(0xff)); + uint64_t x143 = (x141 >> 8); + uint8_t x144 = (uint8_t)(x141 & UINT8_C(0xff)); + uint64_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 + x38); + uint64_t x150 = (x149 >> 8); + uint8_t x151 = (uint8_t)(x149 & UINT8_C(0xff)); + uint64_t x152 = (x150 >> 8); + uint8_t x153 = (uint8_t)(x150 & UINT8_C(0xff)); + uint64_t x154 = (x152 >> 8); + uint8_t x155 = (uint8_t)(x152 & UINT8_C(0xff)); + uint64_t x156 = (x154 >> 8); + uint8_t x157 = (uint8_t)(x154 & UINT8_C(0xff)); + uint64_t x158 = (x156 >> 8); + uint8_t x159 = (uint8_t)(x156 & UINT8_C(0xff)); + uint64_t x160 = (x158 >> 8); + uint8_t x161 = (uint8_t)(x158 & UINT8_C(0xff)); + uint8_t x162 = (uint8_t)(x160 >> 8); + uint8_t x163 = (uint8_t)(x160 & UINT8_C(0xff)); + uint8_t x164 = (uint8_t)(x162 & UINT8_C(0xff)); + uint64_t x165 = (0x0 + x36); + uint64_t x166 = (x165 >> 8); + uint8_t x167 = (uint8_t)(x165 & UINT8_C(0xff)); + uint64_t x168 = (x166 >> 8); + uint8_t x169 = (uint8_t)(x166 & UINT8_C(0xff)); uint64_t x170 = (x168 >> 8); uint8_t x171 = (uint8_t)(x168 & UINT8_C(0xff)); uint64_t x172 = (x170 >> 8); @@ -721,10 +721,8 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) { uint8_t x175 = (uint8_t)(x172 & UINT8_C(0xff)); uint64_t x176 = (x174 >> 8); uint8_t x177 = (uint8_t)(x174 & UINT8_C(0xff)); - uint64_t x178 = (x176 >> 8); + fiat_p521_uint1 x178 = (fiat_p521_uint1)(x176 >> 8); uint8_t x179 = (uint8_t)(x176 & UINT8_C(0xff)); - fiat_p521_uint1 x180 = (fiat_p521_uint1)(x178 >> 8); - uint8_t x181 = (uint8_t)(x178 & UINT8_C(0xff)); out1[0] = x45; out1[1] = x47; out1[2] = x49; @@ -753,44 +751,44 @@ static void fiat_p521_to_bytes(uint8_t out1[66], const uint64_t arg1[9]) { out1[25] = x98; out1[26] = x100; out1[27] = x102; - out1[28] = x104; - out1[29] = x107; - out1[30] = x109; - out1[31] = x111; - out1[32] = x113; - out1[33] = x115; - out1[34] = x117; - out1[35] = x119; - out1[36] = x122; - out1[37] = x124; - out1[38] = x126; - out1[39] = x128; - out1[40] = x130; - out1[41] = x132; - out1[42] = x134; - out1[43] = x137; - out1[44] = x139; - out1[45] = x141; - out1[46] = x143; - out1[47] = x145; - out1[48] = x147; - out1[49] = x149; - out1[50] = x152; - out1[51] = x154; - out1[52] = x156; - out1[53] = x158; - out1[54] = x160; - out1[55] = x162; - out1[56] = x164; - out1[57] = x166; - out1[58] = x169; - out1[59] = x171; - out1[60] = x173; - out1[61] = x175; - out1[62] = x177; - out1[63] = x179; - out1[64] = x181; - out1[65] = x180; + out1[28] = x103; + out1[29] = x106; + out1[30] = x108; + out1[31] = x110; + out1[32] = x112; + out1[33] = x114; + out1[34] = x116; + out1[35] = x118; + out1[36] = x121; + out1[37] = x123; + out1[38] = x125; + out1[39] = x127; + out1[40] = x129; + out1[41] = x131; + out1[42] = x133; + out1[43] = x136; + out1[44] = x138; + out1[45] = x140; + out1[46] = x142; + out1[47] = x144; + out1[48] = x146; + out1[49] = x148; + out1[50] = x151; + out1[51] = x153; + out1[52] = x155; + out1[53] = x157; + out1[54] = x159; + out1[55] = x161; + out1[56] = x163; + out1[57] = x164; + out1[58] = x167; + out1[59] = x169; + out1[60] = x171; + out1[61] = x173; + out1[62] = x175; + out1[63] = x177; + out1[64] = x179; + out1[65] = x178; } /* @@ -884,29 +882,27 @@ static void fiat_p521_from_bytes(uint64_t out1[9], const uint8_t arg1[66]) { uint8_t x82 = (uint8_t)(x81 >> 58); uint64_t x83 = (x81 & UINT64_C(0x3ffffffffffffff)); uint64_t x84 = (x82 + x75); - fiat_p521_uint1 x85 = (fiat_p521_uint1)(x84 >> 58); - uint64_t x86 = (x84 & UINT64_C(0x3ffffffffffffff)); - uint64_t x87 = (x85 + x74); - uint8_t x88 = (uint8_t)(x87 >> 58); - uint64_t x89 = (x87 & UINT64_C(0x3ffffffffffffff)); - uint64_t x90 = (x88 + x73); - uint8_t x91 = (uint8_t)(x90 >> 58); - uint64_t x92 = (x90 & UINT64_C(0x3ffffffffffffff)); - uint64_t x93 = (x91 + x72); - uint8_t x94 = (uint8_t)(x93 >> 58); - uint64_t x95 = (x93 & UINT64_C(0x3ffffffffffffff)); - uint64_t x96 = (x94 + x71); - fiat_p521_uint1 x97 = (fiat_p521_uint1)(x96 >> 58); - uint64_t x98 = (x96 & UINT64_C(0x3ffffffffffffff)); - uint64_t x99 = (x97 + x70); + uint64_t x85 = (x84 & UINT64_C(0x3ffffffffffffff)); + uint64_t x86 = (0x0 + x74); + uint8_t x87 = (uint8_t)(x86 >> 58); + uint64_t x88 = (x86 & UINT64_C(0x3ffffffffffffff)); + uint64_t x89 = (x87 + x73); + uint8_t x90 = (uint8_t)(x89 >> 58); + uint64_t x91 = (x89 & UINT64_C(0x3ffffffffffffff)); + uint64_t x92 = (x90 + x72); + uint8_t x93 = (uint8_t)(x92 >> 58); + uint64_t x94 = (x92 & UINT64_C(0x3ffffffffffffff)); + uint64_t x95 = (x93 + x71); + uint64_t x96 = (x95 & UINT64_C(0x3ffffffffffffff)); + uint64_t x97 = (0x0 + x70); out1[0] = x69; out1[1] = x80; out1[2] = x83; - out1[3] = x86; - out1[4] = x89; - out1[5] = x92; - out1[6] = x95; - out1[7] = x98; - out1[8] = x99; + out1[3] = x85; + out1[4] = x88; + out1[5] = x91; + out1[6] = x94; + out1[7] = x96; + out1[8] = x97; } -- cgit v1.2.3