evm: skip #addr if we know it wont be used

[ehildenb]

This is inspired by the data here: #1048 (comment)

I noticed that one of the really-high frequency rules was for #addr[_], and also noticed that this rule wasn't particularly fast (or slow). This rule only needs to be fired on a very small fraction of opcodes, so if we inline the condition about whether we should run this check or not using an #if_#then_#else_#fi, we can skip an entire rewrite rule per EVM opcode step in many cases!

I ran an initial test using tests/specs/benchmarks/storagevar00-spec.k, results are:

* 906ef670 - evm: skip #addr if we know it wont be used                                       - Everett Hildenbrandt (HEAD, upstream/addr-optimizations, addr-optimizations)
| testset: single-profile - Thu Jun 17 00:03:34 UTC 2021
| pre: rm -rf .build
| pre: git submodule update --init --recursive
| pre: make deps RELEASE=true
| 0  60.69s   761.92s  20.39s  2729392KB  make  build                                             -j8                            RELEASE=true
| 0  260.02s  462.54s  8.90s   3356184KB  make  tests/specs/benchmarks/storagevar00-spec.k.prove  TEST_SYMBOLIC_BACKEND=haskell
| 0  246.05s  285.20s  3.99s   1937556KB  make  tests/specs/benchmarks/storagevar00-spec.k.prove  TEST_SYMBOLIC_BACKEND=haskell
| 0  238.03s  277.13s  5.33s   1937300KB  make  tests/specs/benchmarks/storagevar00-spec.k.prove  TEST_SYMBOLIC_BACKEND=haskell
| 
* 64ae85bf - uppercase variables in tests/specs/mcd (#1051)                                   - 0xVerif (upstream/master)
| testset: single-profile - Wed Jun 16 23:49:53 UTC 2021
| pre: rm -rf .build
| pre: git submodule update --init --recursive
| pre: make deps RELEASE=true
| 0  311.92s  1046.14s  22.53s  2570444KB  make  build                                             -j8                            RELEASE=true
| 0  281.90s  471.91s   7.58s   2962644KB  make  tests/specs/benchmarks/storagevar00-spec.k.prove  TEST_SYMBOLIC_BACKEND=haskell
| 0  263.16s  301.48s   3.88s   1938472KB  make  tests/specs/benchmarks/storagevar00-spec.k.prove  TEST_SYMBOLIC_BACKEND=haskell
| 0  268.46s  309.28s   3.79s   1937592KB  make  tests/specs/benchmarks/storagevar00-spec.k.prove  TEST_SYMBOLIC_BACKEND=haskell

Three runs on master: 282s, 263s, 269s
Three runs on this PR: 260s, 246s, 238s - roughly 9% speedup consistently (somewhat consistent with the fact that we're skipping a little fewer than 1/10 steps).

I'll get data on the entirety of the test-suite before marking this as ready.

[ehildenb]

Data for all the tests (excluding tests with <3.5% difference in performance):

 Test                                            | f7cd5070-prove-haskell time | 64ae85bf-prove-haskell time | (f7cd5070-prove-haskell/64ae85bf-prove-haskell) time
-------------------------------------------------+-----------------------------+-----------------------------+------------------------------------------------------
 specs/benchmarks/storagevar01-spec.k            | 321.05                      | 342.13                      | 0.9383859936281531
 specs/benchmarks/encode-keccak00-spec.k         | 1229.21                     | 1307.52                     | 0.9401079906999511
 specs/benchmarks/overflow00-nooverflow-spec.k   | 356.79                      | 379.32                      | 0.9406042391648213
 specs/benchmarks/storagevar02-overflow-spec.k   | 348.02                      | 369.91                      | 0.9408234435403205
 specs/benchmarks/requires01-a0le0-spec.k        | 277.66                      | 294.77                      | 0.941954744376972
 specs/benchmarks/storagevar03-spec.k            | 213.25                      | 226.32                      | 0.9422499116295511
 specs/benchmarks/overflow00-overflow-spec.k     | 320.49                      | 339.8                       | 0.9431724543849324
 specs/benchmarks/storagevar00-spec.k            | 249.22                      | 264.12                      | 0.9435862486748448
 specs/benchmarks/storagevar02-nooverflow-spec.k | 376.49                      | 398.14                      | 0.9456221429647863
 specs/benchmarks/address00-spec.k               | 323.61                      | 341.99                      | 0.9462557384718852
 erc20/ds/totalSupply-spec.k                     | 973.65                      | 1021.62                     | 0.9530451635637517
 erc20/hkg/allowance-spec.k                      | 398.23                      | 417.3                       | 0.9543014617780973
 erc20/ds/approve-failure-spec.k                 | 957.06                      | 996.97                      | 0.9599687051766853
 specs/functional/lemmas-no-smt-spec.k           | 41.76                       | 43.42                       | 0.9617687701520036
 specs/functional/infinite-gas-spec.k            | 42.92                       | 44.57                       | 0.962979582678932
 specs/mcd/functional-spec.k                     | 65.38                       | 61.84                       | 1.0572445019404915
 TOTAL                                           | 6494.79                     | 6849.740000000001           | 0.9481805148808566

So we see ~5% speedup for a large amount of the tests, and in the total time. One test (a functional one, so it never executes the #addr rule) slows down by 5%.