search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
208 stars 41 forks source link

keep cache and constraint store after recursion, revert state on exceptions #3929

Closed jberthold closed 3 months ago

jberthold commented 3 months ago

Previously we were discarding any simplifications cached during recursive simplification. This is overly cautious - while the change flag and the term stack (for iteration count and loop detection) should be restored, the cache remains valid (we may only gain new path conditions, and only in rare cases where equations have an ensures clause), and continues to be useful when the same or a similar recursive evaluation is needed.

This change sped up a particular request extracted from an mx-backend proof from 5 minutes to 5 seconds.

jberthold commented 3 months ago

KEVM performance run (PYTEST_PARALLEL=1, but with moderate additional load)

Test HOTFIX-persist-cache-during-recursive-evaluation time master-3b01114ca time (HOTFIX-persist-cache-during-recursive-evaluation/master-3b01114ca) time
mcd/end-pack-pass-rough-spec.k 88.17 106.43 0.8284318331297567
erc20/hkg/transferFrom-success-1-spec.k 37.06 44.55 0.8318742985409653
mcd/flapper-yank-pass-rough-spec.k 110.49 132.65 0.8329438371654729
erc20/hkg/transferFrom-success-2-spec.k 36.36 42.94 0.8467629250116442
mcd/flopper-kick-pass-rough-spec.k 81.22 95.76 0.8481620718462823
erc20/ds/transfer-success-1-spec.k 39.87 46.73 0.8531992296169484
erc20/hkg/approve-spec.k 31.44 36.48 0.861842105263158
erc20/ds/transferFrom-success-1-spec.k 46.88 54.22 0.864625599409812
erc20/ds/transfer-success-2-spec.k 39.31 45.29 0.867962022521528
mcd/flopper-file-pass-rough-spec.k 237.34 272.94 0.8695684033120833
mcd/flipper-bids-pass-rough-spec.k 47.03 54.03 0.8704423468443457
mcd/flopper-dent-guy-same-pass-rough-spec.k 377.16 433.1 0.8708381436157931
erc20/ds/transferFrom-success-2-spec.k 45.14 51.34 0.8792364627970393
mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k 520.02 589.44 0.8822271986970683
kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k 43.67 48.85 0.8939611054247697
mcd/pot-join-pass-rough-spec.k 116.47 130.15 0.894890510948905
mcd/flopper-tick-pass-rough-spec.k 113.98 126.76 0.8991795519091196
kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k 32.93 36.54 0.9012041598248495
mcd/dsvalue-peek-pass-rough-spec.k 38.11 42.02 0.9069490718705377
mcd/cat-file-addr-pass-rough-spec.k 37.36 41.07 0.9096664231799366
erc20/ds/approve-success-spec.k 38.21 41.94 0.9110634239389604
mcd/flipper-ttl-pass-spec.k 35.52 38.98 0.9112365315546436
mcd/cat-exhaustiveness-spec.k 70.36 77.14 0.9121078558465128
kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k 33.47 36.67 0.9127352058903735
kontrol/test-storetest-testaccesses-0-spec.k 32.96 36.07 0.9137787635153868
mcd/dsvalue-read-pass-spec.k 38.93 42.57 0.9144937749588912
mcd/flopper-cage-pass-spec.k 36.68 40.1 0.914713216957606
kontrol/test-owneruponlytest-testincrementasowner-0-spec.k 46.7 51.0 0.915686274509804
erc20/ds/transferFrom-failure-1-b-spec.k 68.86 75.12 0.9166666666666666
kontrol/test-allowchangestest-testallow-0-spec.k 32.9 35.88 0.9169453734671125
kontrol/test-storetest-teststoreload-0-spec.k 33.19 36.18 0.9173576561636263
kontrol/test-expectcalltest-testexpectregularcall-0-spec.k 32.96 35.92 0.9175946547884187
kontrol/test-countertest-testincrement-0-spec.k 57.87 62.93 0.9195931987923088
mcd/vat-move-diff-rough-spec.k 59.36 64.55 0.9195972114639814
kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k 32.83 35.68 0.9201233183856502
kontrol/test-emitcontracttest-testexpectemit-0-spec.k 33.13 35.99 0.9205334815226452
mcd/flipper-tau-pass-spec.k 35.9 38.94 0.9219311761684643
kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k 32.86 35.63 0.9222565253999437
mcd/dstoken-approve-fail-rough-spec.k 54.73 59.28 0.9232456140350876
benchmarks/ecrecoverloop00-sig1-invalid-spec.k 58.67 63.48 0.9242281033396346
kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k 33.67 36.43 0.924238265166072
kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k 37.42 40.48 0.9244071146245061
mcd/end-subuu-pass-spec.k 38.31 41.41 0.9251388553489497
benchmarks/ecrecoverloop00-sig0-invalid-spec.k 36.92 39.85 0.926474278544542
kontrol/test-allowchangestest-testallow_fail-0-spec.k 32.98 35.59 0.9266647934813148
mcd/dai-adduu-fail-rough-spec.k 34.38 37.1 0.9266846361185984
erc20/hkg/transfer-success-1-spec.k 33.9 36.58 0.9267359212684527
kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k 45.21 48.75 0.9273846153846154
kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k 31.72 34.2 0.9274853801169589
kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k 33.42 36.03 0.9275603663613655
mcd/flipper-addu48u48-fail-rough-spec.k 36.06 38.83 0.9286634045840846
mcd/dai-symbol-pass-spec.k 35.05 37.71 0.9294616812516573
kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k 33.58 36.09 0.9304516486561373
mcd/vat-flux-diff-pass-rough-spec.k 60.86 65.32 0.9317207593386406
kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k 32.82 35.21 0.9321215563760296
kontrol/test-arithmetictest-test_wmul_weakly_increasing_positive-uint256-uint256-0-spec.k 46.03 49.24 0.9348090982940699
kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k 44.61 47.63 0.9365945832458534
kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k 33.01 35.16 0.9388509670079637
mcd/vat-slip-pass-rough-spec.k 50.96 53.84 0.9465081723625557
erc20/ds/transfer-failure-1-b-spec.k 54.01 57.0 0.9475438596491228
erc20/hkg/allowance-spec.k 31.09 32.74 0.9496029321930359
benchmarks/ecrecoverloop00-sigs-valid-spec.k 44.21 46.2 0.9569264069264068
benchmarks/ecrecoverloop02-sig0-invalid-spec.k 132.42 138.22 0.9580379105773403
erc20/hkg/transfer-success-2-spec.k 33.65 35.02 0.9608794974300399
benchmarks/ecrecover00-siginvalid-spec.k 34.49 35.86 0.9617958728388177
erc20/ds/transferFrom-failure-1-c-spec.k 55.05 57.04 0.9651122019635343
benchmarks/ecrecoverloop02-sig1-invalid-spec.k 234.61 242.88 0.9659502635046114
mcd/dsvalue-read-pass-summarize-spec.k 43.74 40.12 1.0902293120638087
TOTAL 4380.28 4845.87 0.9039202454873946
jberthold commented 3 months ago

kontrol performance test

(Had to hack the script as the test_foundry_kompile generated module had the import statements in a different order)

Test HOTFIX-persist-cache-during-recursive-evaluation time master-7bbc744b4 time (HOTFIX-persist-cache-during-recursive-evaluation/master-7bbc744b4) time
PlainPrankTest.test_stopPrank_notExistent() 10.91 14.18 0.7693935119887165
AssumeTest.test_multi_assume(address,address) 22.33 28.66 0.7791346824842986
AccountParamsTest.test_getNonce_unknownSymbolic(address) 27.76 33.14 0.8376584188292094
ExpectRevertTest.testFail_expectRevert_empty() 10.79 12.88 0.8377329192546583
ExpectCallTest.testExpectStaticCall() 15.51 17.95 0.8640668523676881
FreshBytesTest.test_symbolic_bytes_3 59.86 69.25 0.8644043321299639
FreshBytesTest.test_symbolic_bytes_length 32.49 37.21 0.8731523783929052
ConstructorTest.run_constructor() 10.35 11.84 0.8741554054054054
BytesTypeTest.test_bytes32(bytes32) 10.58 12.09 0.8751033912324235
AccountParamsTest.testEtchConcrete() 32.7 37.26 0.8776167471819647
FreshBytesTest.test_symbolic_bytes_1 85.2 96.23 0.885378780006235
SymbolicStorageTest.testFail_SymbolicStorage(uint256) 36.55 40.41 0.9044790893343232
SymbolicStorageTest.testFail_SymbolicStorage1(uint256) 39.29 43.42 0.9048825426070934
AssumeTest.testFail_assume_true(uint256,uint256) 32.77 36.05 0.9090152565880723
CounterTest.testSetNumber(uint256) 18.69 20.47 0.9130434782608696
ExpectRevertTest.test_expectRevert_message() 16.08 17.42 0.9230769230769229
ExpectRevertTest.test_expectRevert_returnValue() 20.46 22.15 0.9237020316027089
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_resume_proof 34.79 37.58 0.925758382118148
AssumeTest.test_assume_false(uint256,uint256) 41.89 44.98 0.9313028012449979
LoopsTest.test_sum_10() 16.77 17.99 0.9321845469705392
PlainPrankTest.test_startPrankWithOrigin_true() 16.06 17.2 0.9337209302325581
MockCallTestFoundry.testMockNested() 36.79 39.35 0.9349428208386277
PlainPrankTest.test_prank_zeroAddress_true() 17.32 18.49 0.9367225527312062
BlockParamsTest.testRoll(uint256) 13.62 14.49 0.9399585921325051
AssumeTest.test_assume_true(uint256,uint256) 14.98 15.93 0.9403640929064658
SymbolicStorageTest.testEmptyInitialStorage(uint256) 12.62 13.42 0.9403874813710879
MockCallTestFoundry.testMockCalldata() 34.62 36.8 0.9407608695652174
],uint256)) 132.11 140.37 0.9411555175607325
AccountParamsTest.testFail_GetNonce_true() 17.38 18.46 0.9414951245937161
]) 31.27 33.2 0.941867469879518
MockCallTestFoundry.testMockSelector() 24.27 25.76 0.9421583850931676
ArithmeticTest.test_max1(uint256,uint256) 28.13 29.82 0.9433266264252179
ExpectRevertTest.test_expectRevert_true() 13.87 14.62 0.9487004103967168
EmitContractTest.testExpectEmitLessTopics() 13.76 14.48 0.9502762430939226
ExpectRevertTest.testFail_expectRevert_bytes4() 18.23 19.15 0.951958224543081
Setup2Test.testFail_setup() 26.15 27.45 0.9526411657559198
ExpectCallTest.testExpectRegularCall() 15.34 16.06 0.9551681195516812
AccountParamsTest.testDealSymbolic(uint256) 16.25 17.01 0.9553203997648442
PlainPrankTest.test_startPrank_zeroAddress_true() 16.33 17.08 0.9560889929742389
FreshCheatcodes.test_int128() 13.88 14.51 0.9565816678152999
PlainPrankTest.test_startPrank_true() 16.14 16.87 0.956727919383521
PlainPrankTest.test_prank_expectRevert() 17.93 18.69 0.9593365436062065
StoreTest.testStoreLoadNonExistent() 11.09 11.55 0.9601731601731601
StoreTest.testStoreLoad() 13.63 14.19 0.9605355884425653
MockCallTest.testSelectorMockCall() 22.07 22.97 0.9608184588593819
EmitContractTest.testExpectEmit() 13.77 14.33 0.9609211444521981
ExpectRevertTest.testFail_expectRevert_multipleReverts() 15.28 15.88 0.9622166246851385
ExpectRevertTest.testFail_expectRevert_false() 16.49 17.12 0.9632009345794391
LoopsTest.sum_N(uint256) 127.05 131.78 0.9641068447412353
BlockParamsTest.testWarp(uint256)-trace_options2 16.22 16.82 0.9643281807372175
StoreTest.testLoadNonExistent() 10.81 11.19 0.9660411081322611
AssertTest.test_assert_false() 30.63 29.25 1.047179487179487
ExpectRevertTest.test_expectRevert_bytes4() 17.66 16.68 1.0587529976019185
BytesTypeTest.test_bytes4(bytes4) 14.63 13.5 1.0837037037037038
ExpectRevertTest.testFail_ExpectRevert_failAndSuccess() 18.38 16.72 1.0992822966507176
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_refute_node 10.8 9.54 1.1320754716981134
StructTypeTest.test_vars((uint8,uint32,bytes32)) 18.96 16.71 1.1346499102333931
FreshCheatcodes.test_freshSymbolicWord() 16.16 13.94 1.1592539454806314
AddrTest.test_notBuiltinAddress_symbolic(address) 21.91 18.51 1.183684494867639
FreshCheatcodes.test_address() 21.44 17.45 1.22865329512894
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_xml_report 23.66 17.44 1.3566513761467889
TOTAL 1563.46 1655.94 0.9441525659142244