Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

make all logging data types non-strict #3125

Merged
merged 1 commit into from
Jun 30, 2022
Merged

Conversation

jberthold
Copy link
Member

@jberthold jberthold commented Jun 29, 2022

Part of #3087

Scope:

Adds NoStrict and NoStrictData to all modules defining data types for logging (in Kore.Log.*), to avoid constructing log data needlessly.

Estimate:


Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

  • Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
  • Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
  • Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
  • Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.323583 0.000748
test/regression-evm/test-storagevar03.sh -0.471682 -0.000208
test/regression-evm/test-totalSupply.sh -0.211938 0.001564
test/regression-evm/test-sum-to-n.sh -0.249971 0.004808
test/regression-evm/test-lemmas.sh -0.099691 -0.215182
test/regression-evm/test-addu48u48.sh -0.178967 -0.007486
test/regression-wasm/test-wrc20.sh -0.098047 -0.077171
test/regression-wasm/test-loops.sh -0.102971 0.000386
test/regression-wasm/test-memory.sh -0.065087 0.000024
test/regression-wasm/test-simple-arithmetic.sh -0.022961 -0.000093
test/regression-wasm/test-locals.sh -0.002209 0.000096

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.323608 0.002255
test/regression-evm/test-storagevar03.sh -0.471684 -0.002592
test/regression-evm/test-totalSupply.sh -0.211938 0.001837
test/regression-evm/test-sum-to-n.sh -0.249959 0.004805
test/regression-evm/test-lemmas.sh -0.099653 -0.001225
test/regression-evm/test-addu48u48.sh -0.178970 -0.001471
test/regression-wasm/test-wrc20.sh -0.098050 -0.080243
test/regression-wasm/test-loops.sh -0.102976 0.000003
test/regression-wasm/test-memory.sh -0.065104 0.000024
test/regression-wasm/test-simple-arithmetic.sh -0.022992 -0.000020
test/regression-wasm/test-locals.sh -0.002190 -0.002953

@jberthold jberthold marked this pull request as ready for review June 29, 2022 05:50
@jberthold
Copy link
Member Author

Some timings from evm-semantics, looks like a good improvement:

Test lazy-logging time master-logging time (lazy-logging/master-logging) time
specs/benchmarks/ecrecover00-sigvalid-spec.k 235.83 408.79 0.5768976736221532
specs/benchmarks/ecrecover00-siginvalid-spec.k 183.9 318.51 0.5773759065649431
specs/benchmarks/encode-keccak00-spec.k 234.96 378.46 0.6208317919991545
specs/benchmarks/staticarray00-spec.k 121.86 193.15 0.6309086202433342
specs/benchmarks/staticloop00-a0lt10-spec.k 154.49 237.87 0.6494724008912431
specs/benchmarks/requires01-a0gt0-spec.k 88.53 135.79 0.6519625892922896
specs/benchmarks/encodepacked-keccak01-spec.k 121.73 186.16 0.6538998710786421
specs/benchmarks/overflow00-nooverflow-spec.k 88.8 133.78 0.6637763492300792
specs/benchmarks/storagevar02-nooverflow-spec.k 79.37 118.84 0.6678727701110737
specs/benchmarks/keccak00-spec.k 151.66 227.0 0.6681057268722467
specs/benchmarks/overflow00-overflow-spec.k 85.8 127.77 0.6715191359474055
specs/benchmarks/storagevar02-overflow-spec.k 76.66 113.23 0.6770290559039124
specs/benchmarks/bytes00-spec.k 148.15 218.57 0.6778148876790044
specs/benchmarks/requires01-a0le0-spec.k 66.74 97.83 0.6822038229581927
erc20/hkg/transferFrom-failure-2-spec.k 272.24 398.62 0.6829561988861572
specs/benchmarks/storagevar03-spec.k 54.27 79.03 0.6867012526888524
specs/benchmarks/storagevar00-spec.k 64.72 93.92 0.6890971039182282
erc20/hkg/transferFrom-success-2-spec.k 358.88 518.91 0.6916035536027443
erc20/hkg/transfer-failure-1-spec.k 206.49 297.31 0.6945275974571996
erc20/hkg/transfer-success-2-spec.k 145.68 209.1 0.696700143472023
specs/benchmarks/storagevar01-spec.k 73.44 105.08 0.6988960791777693
erc20/hkg/transfer-success-1-spec.k 251.09 357.07 0.7031954518721819
specs/mcd/cat-exhaustiveness-spec.k 104.64 146.51 0.7142174595590746
specs/mcd/cat-file-addr-pass-rough-spec.k 162.76 227.65 0.7149571710959806
erc20/hkg/transfer-failure-2-spec.k 117.12 163.73 0.7153240090392721
specs/mcd/vat-move-diff-rough-spec.k 530.21 734.35 0.722012664260911
specs/mcd/vow-flog-fail-rough-spec.k 255.68 340.44 0.7510280813065445
erc20/hkg/approve-spec.k 112.89 149.94 0.7529011604641856
erc20/hkg/allowance-spec.k 85.99 112.65 0.7633377718597425
specs/mcd/vow-fess-fail-rough-spec.k 283.89 370.35 0.766545159983799
specs/bihu/forwardToHotWallet-failure-2-spec.k 196.85 256.8 0.7665498442367601
specs/benchmarks/address00-spec.k 95.28 124.26 0.766779333655239
specs/bihu/forwardToHotWallet-failure-3-spec.k 216.34 280.44 0.7714306090429326
specs/bihu/forwardToHotWallet-failure-1-spec.k 145.19 186.28 0.7794180803092119
erc20/ds/transfer-failure-1-c-spec.k 269.93 345.56 0.7811378631786087
erc20/ds/transfer-failure-2-a-spec.k 358.22 454.24 0.7886139485734414
erc20/ds/transferFrom-failure-1-d-spec.k 330.17 418.54 0.7888612796865294
specs/mcd/dai-symbol-pass-spec.k 151.61 191.78 0.7905412451767652
erc20/hkg/balanceOf-spec.k 64.93 81.99 0.7919258446151971
erc20/ds/transferFrom-failure-2-c-spec.k 213.0 268.11 0.79445003916303
erc20/ds/transfer-failure-2-b-spec.k 182.89 229.3 0.797601395551679
erc20/ds/approve-success-spec.k 343.93 429.14 0.8014400894812882
specs/mcd/vat-subui-pass-rough-spec.k 261.03 324.77 0.8037380299904547
specs/bihu/forwardToHotWallet-failure-4-spec.k 345.31 429.55 0.8038877895472005
specs/mcd/vat-deny-diff-fail-rough-spec.k 304.76 378.83 0.8044769421640313
specs/mcd/vat-mului-pass-spec.k 198.36 245.38 0.8083788409813352
specs/examples/solidity-code-spec.md 105.57 130.45 0.8092755845151399
specs/mcd/vat-subui-pass-spec.k 265.13 327.22 0.8102499847197603
specs/mcd/flopper-cage-pass-spec.k 169.06 207.75 0.8137665463297232
erc20/ds/allowance-spec.k 191.57 234.88 0.8156079700272479
specs/mcd/dsvalue-read-pass-spec.k 191.55 232.44 0.8240836344863192
specs/mcd/flipper-ttl-pass-spec.k 116.03 140.3 0.8270135424091233
specs/mcd/vat-subui-fail-rough-spec.k 194.27 233.52 0.8319201781431997
erc20/ds/balanceOf-spec.k 127.22 152.0 0.8369736842105263
specs/mcd/flipper-tau-pass-spec.k 116.46 138.97 0.838022594804634
specs/mcd/vat-addui-fail-rough-spec.k 193.01 228.42 0.8449785482882409
specs/mcd/dsvalue-peek-pass-rough-spec.k 186.63 220.82 0.8451680101440087
erc20/ds/approve-failure-spec.k 81.81 94.95 0.861611374407583
erc20/hkg/totalSupply-spec.k 31.3 35.97 0.8701695857659161
specs/benchmarks/functional-spec.k 28.58 32.7 0.874006116207951
specs/mcd/dai-adduu-fail-rough-spec.k 61.21 70.02 0.8741788060554128
erc20/ds/totalSupply-spec.k 80.66 92.19 0.8749322052283328
specs/examples/sum-to-n-spec.k 19.09 21.79 0.8760899495181276
specs/mcd/flipper-addu48u48-fail-rough-spec.k 78.3 86.96 0.9004139834406624
specs/mcd/end-subuu-pass-spec.k 113.78 124.16 0.9163981958762887
specs/mcd/dsvalue-read-pass-summarize-spec.k 87.33 94.43 0.9248120300751879
specs/bihu/functional-spec.k 11.74 12.33 0.9521492295214923
specs/functional/lemmas-spec.k 20.17 21.14 0.9541154210028383
specs/mcd/dstoken-burn-self-fail-rough-spec.k 1328.16 1383.5 0.9600000000000001
specs/functional/infinite-gas-spec.k 18.34 17.53 1.0462065031374785
specs/functional/lemmas-no-smt-spec.k 14.46 12.55 1.152191235059761
0 25.17 18.23 1.3806911684037302
TOTAL 12452.869999999995 16210.599999999999 0.7681930341875067

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.323609 0.007853
test/regression-evm/test-storagevar03.sh -0.471681 -0.000934
test/regression-evm/test-totalSupply.sh -0.211936 0.003691
test/regression-evm/test-sum-to-n.sh -0.249981 0.006311
test/regression-evm/test-lemmas.sh -0.099681 -0.214139
test/regression-evm/test-addu48u48.sh -0.178968 -0.008910
test/regression-wasm/test-wrc20.sh -0.098058 -0.089192
test/regression-wasm/test-loops.sh -0.102978 0.000003
test/regression-wasm/test-memory.sh -0.065127 0.000131
test/regression-wasm/test-simple-arithmetic.sh -0.023055 -0.000313
test/regression-wasm/test-locals.sh -0.002207 0.000096

Copy link
Member

@goodlyrottenapple goodlyrottenapple left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM! Did a quick and dirty heap profiling on one or two kevm-bug proofs and there are definitely fewer calls to some functions in Kore.Log due to added laziness without any significant uptick in memory usage, which the github bot also seems to confirm

@github-actions
Copy link

name diff_allocated_bytes diff_max_live_bytes
test/regression-evm/test-dsvalue-peek-pass-rough.sh -0.323622 0.011404
test/regression-evm/test-storagevar03.sh -0.471687 -0.001005
test/regression-evm/test-totalSupply.sh -0.211938 0.000312
test/regression-evm/test-sum-to-n.sh -0.249990 0.004788
test/regression-evm/test-lemmas.sh -0.099693 -0.214070
test/regression-evm/test-addu48u48.sh -0.178973 -0.011961
test/regression-wasm/test-wrc20.sh -0.098056 -0.092651
test/regression-wasm/test-loops.sh -0.102943 0.000003
test/regression-wasm/test-memory.sh -0.065102 0.000024
test/regression-wasm/test-simple-arithmetic.sh -0.022991 -0.000021
test/regression-wasm/test-locals.sh -0.002209 0.000096

@rv-jenkins rv-jenkins merged commit c86e9d2 into master Jun 30, 2022
@rv-jenkins rv-jenkins deleted the jb/3087-lazier-logging branch June 30, 2022 01:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants