diff options
| author |  Jason Gross <jgross@mit.edu> | 2019-01-15 15:53:34 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2019-01-16 16:51:11 -0500 |
| commit | 60bade02ccd577550bfcd5974d3c62a3d40e751a (patch) | |
| tree | 46a9e9ef505704bdff47f0c794c163ecd5d7fd76 /src/Rewriter.v | |
| parent | 538e541709d70caaa78104739cb965c6523d89a8 (diff) | |
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%
Diffstat (limited to 'src/Rewriter.v')
| -rw-r--r-- | src/Rewriter.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Rewriter.v b/src/Rewriter.v index 76071b866..8bbf13173 100644 --- a/src/Rewriter.v +++ b/src/Rewriter.v @@ -1790,6 +1790,8 @@ Module Compilers. := [make_rewrite (#(@pattern.ident.fst '1 '2) @ (??, ??)) (fun _ _ x y => x) ; make_rewrite (#(@pattern.ident.snd '1 '2) @ (??, ??)) (fun _ x _ y => y) + ; make_rewriteo (??') (fun r v => ##(lower r) when lower r =? upper r) + ; make_rewriteo (#?ℤ - (-'??')) (fun z rnv rv v => cst rv v when (z =? 0) && (ZRange.normalize rv <=? -ZRange.normalize rnv)%zrange) |