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% --- curve25519_32.c | 148 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 73 insertions(+), 75 deletions(-) (limited to 'curve25519_32.c') diff --git a/curve25519_32.c b/curve25519_32.c index 5366ec40c..508141786 100644 --- a/curve25519_32.c +++ b/curve25519_32.c @@ -748,43 +748,42 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) { uint8_t x81 = (uint8_t)(x78 & UINT8_C(0xff)); uint8_t x82 = (uint8_t)(x80 >> 8); uint8_t x83 = (uint8_t)(x80 & UINT8_C(0xff)); - fiat_25519_uint1 x84 = (fiat_25519_uint1)(x82 >> 8); - uint8_t x85 = (uint8_t)(x82 & UINT8_C(0xff)); - uint32_t x86 = (x84 + x32); - uint32_t x87 = (x86 >> 8); - uint8_t x88 = (uint8_t)(x86 & UINT8_C(0xff)); - uint32_t x89 = (x87 >> 8); - uint8_t x90 = (uint8_t)(x87 & UINT8_C(0xff)); - fiat_25519_uint1 x91 = (fiat_25519_uint1)(x89 >> 8); - uint8_t x92 = (uint8_t)(x89 & UINT8_C(0xff)); - uint32_t x93 = (x91 + x45); - uint32_t x94 = (x93 >> 8); - uint8_t x95 = (uint8_t)(x93 & UINT8_C(0xff)); - uint32_t x96 = (x94 >> 8); - uint8_t x97 = (uint8_t)(x94 & UINT8_C(0xff)); - uint8_t x98 = (uint8_t)(x96 >> 8); - uint8_t x99 = (uint8_t)(x96 & UINT8_C(0xff)); - uint32_t x100 = (x98 + x44); - uint32_t x101 = (x100 >> 8); - uint8_t x102 = (uint8_t)(x100 & UINT8_C(0xff)); - uint32_t x103 = (x101 >> 8); - uint8_t x104 = (uint8_t)(x101 & UINT8_C(0xff)); - uint8_t x105 = (uint8_t)(x103 >> 8); - uint8_t x106 = (uint8_t)(x103 & UINT8_C(0xff)); - uint32_t x107 = (x105 + x43); - uint32_t x108 = (x107 >> 8); - uint8_t x109 = (uint8_t)(x107 & UINT8_C(0xff)); - uint32_t x110 = (x108 >> 8); - uint8_t x111 = (uint8_t)(x108 & UINT8_C(0xff)); - uint8_t x112 = (uint8_t)(x110 >> 8); - uint8_t x113 = (uint8_t)(x110 & UINT8_C(0xff)); - uint32_t x114 = (x112 + x42); - uint32_t x115 = (x114 >> 8); - uint8_t x116 = (uint8_t)(x114 & UINT8_C(0xff)); - uint32_t x117 = (x115 >> 8); - uint8_t x118 = (uint8_t)(x115 & UINT8_C(0xff)); - uint8_t x119 = (uint8_t)(x117 >> 8); - uint8_t x120 = (uint8_t)(x117 & UINT8_C(0xff)); + uint8_t x84 = (uint8_t)(x82 & UINT8_C(0xff)); + uint32_t x85 = (0x0 + x32); + uint32_t x86 = (x85 >> 8); + uint8_t x87 = (uint8_t)(x85 & UINT8_C(0xff)); + uint32_t x88 = (x86 >> 8); + uint8_t x89 = (uint8_t)(x86 & UINT8_C(0xff)); + fiat_25519_uint1 x90 = (fiat_25519_uint1)(x88 >> 8); + uint8_t x91 = (uint8_t)(x88 & UINT8_C(0xff)); + uint32_t x92 = (x90 + x45); + uint32_t x93 = (x92 >> 8); + uint8_t x94 = (uint8_t)(x92 & UINT8_C(0xff)); + uint32_t x95 = (x93 >> 8); + uint8_t x96 = (uint8_t)(x93 & UINT8_C(0xff)); + uint8_t x97 = (uint8_t)(x95 >> 8); + uint8_t x98 = (uint8_t)(x95 & UINT8_C(0xff)); + uint32_t x99 = (x97 + x44); + uint32_t x100 = (x99 >> 8); + uint8_t x101 = (uint8_t)(x99 & UINT8_C(0xff)); + uint32_t x102 = (x100 >> 8); + uint8_t x103 = (uint8_t)(x100 & UINT8_C(0xff)); + uint8_t x104 = (uint8_t)(x102 >> 8); + uint8_t x105 = (uint8_t)(x102 & UINT8_C(0xff)); + uint32_t x106 = (x104 + x43); + uint32_t x107 = (x106 >> 8); + uint8_t x108 = (uint8_t)(x106 & UINT8_C(0xff)); + uint32_t x109 = (x107 >> 8); + uint8_t x110 = (uint8_t)(x107 & UINT8_C(0xff)); + uint8_t x111 = (uint8_t)(x109 >> 8); + uint8_t x112 = (uint8_t)(x109 & UINT8_C(0xff)); + uint32_t x113 = (x111 + x42); + uint32_t x114 = (x113 >> 8); + uint8_t x115 = (uint8_t)(x113 & UINT8_C(0xff)); + uint32_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)); out1[0] = x51; out1[1] = x53; out1[2] = x55; @@ -800,23 +799,23 @@ static void fiat_25519_to_bytes(uint8_t out1[32], const uint32_t arg1[10]) { out1[12] = x79; out1[13] = x81; out1[14] = x83; - out1[15] = x85; - out1[16] = x88; - out1[17] = x90; - out1[18] = x92; - out1[19] = x95; - out1[20] = x97; - out1[21] = x99; - out1[22] = x102; - out1[23] = x104; - out1[24] = x106; - out1[25] = x109; - out1[26] = x111; - out1[27] = x113; - out1[28] = x116; - out1[29] = x118; - out1[30] = x120; - out1[31] = x119; + out1[15] = x84; + out1[16] = x87; + out1[17] = x89; + out1[18] = x91; + out1[19] = x94; + out1[20] = x96; + out1[21] = x98; + out1[22] = x101; + out1[23] = x103; + out1[24] = x105; + out1[25] = x108; + out1[26] = x110; + out1[27] = x112; + out1[28] = x115; + out1[29] = x117; + out1[30] = x119; + out1[31] = x118; } /* @@ -880,30 +879,29 @@ static void fiat_25519_from_bytes(uint32_t out1[10], const uint8_t arg1[32]) { uint8_t x52 = (uint8_t)(x51 >> 25); uint32_t x53 = (x51 & UINT32_C(0x1ffffff)); uint32_t x54 = (x52 + x41); - fiat_25519_uint1 x55 = (fiat_25519_uint1)(x54 >> 26); - uint32_t x56 = (x54 & UINT32_C(0x3ffffff)); - uint32_t x57 = (x55 + x40); - uint8_t x58 = (uint8_t)(x57 >> 25); - uint32_t x59 = (x57 & UINT32_C(0x1ffffff)); - uint32_t x60 = (x58 + x39); - uint8_t x61 = (uint8_t)(x60 >> 26); - uint32_t x62 = (x60 & UINT32_C(0x3ffffff)); - uint32_t x63 = (x61 + x38); - uint8_t x64 = (uint8_t)(x63 >> 25); - uint32_t x65 = (x63 & UINT32_C(0x1ffffff)); - uint32_t x66 = (x64 + x37); - uint8_t x67 = (uint8_t)(x66 >> 26); - uint32_t x68 = (x66 & UINT32_C(0x3ffffff)); - uint32_t x69 = (x67 + x36); + uint32_t x55 = (x54 & UINT32_C(0x3ffffff)); + uint32_t x56 = (0x0 + x40); + uint8_t x57 = (uint8_t)(x56 >> 25); + uint32_t x58 = (x56 & UINT32_C(0x1ffffff)); + uint32_t x59 = (x57 + x39); + uint8_t x60 = (uint8_t)(x59 >> 26); + uint32_t x61 = (x59 & UINT32_C(0x3ffffff)); + uint32_t x62 = (x60 + x38); + uint8_t x63 = (uint8_t)(x62 >> 25); + uint32_t x64 = (x62 & UINT32_C(0x1ffffff)); + uint32_t x65 = (x63 + x37); + uint8_t x66 = (uint8_t)(x65 >> 26); + uint32_t x67 = (x65 & UINT32_C(0x3ffffff)); + uint32_t x68 = (x66 + x36); out1[0] = x35; out1[1] = x47; out1[2] = x50; out1[3] = x53; - out1[4] = x56; - out1[5] = x59; - out1[6] = x62; - out1[7] = x65; - out1[8] = x68; - out1[9] = x69; + out1[4] = x55; + out1[5] = x58; + out1[6] = x61; + out1[7] = x64; + out1[8] = x67; + out1[9] = x68; } -- cgit v1.2.3