Skip to content
This repository was archived by the owner on Oct 9, 2025. It is now read-only.

Abort when Kore's simplifier throws DecidePredicateUnknown #392

Merged
merged 12 commits into from
Dec 8, 2023
Merged

Abort when Kore's simplifier throws DecidePredicateUnknown #392

merged 12 commits into from
Dec 8, 2023

Conversation

@geo2a
Copy link
Contributor

@geo2a geo2a commented Nov 28, 2023 •
edited
Loading

Fixes #373

This PR makes kore-rpc-booster return "execute" responses with "reason": "aborted" in cases when Kore's simplifier fails due to DecidePredicateUnknown in the post-exec simplification in Proxy.hs.

Scenario before

"execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> JsonRpcError`

returning JsonRpcError resulted in loosing information gained by executing in booster for X steps + in kore for up to 1 step.
Scenario now

"execute" request -> booster execute (X steps) > kore execute (0-1steps) -> kore simplify -> DecidePredicateUnknown -> ExecuteResult {reason=Aborted, unknownPredicate = <predicate>}`

this this change, we return the reached state (may be branching) and do not lose information anymore. Additionaly, we return the unknown predicate, so that pyk can decide what to do with these.

PR to pyk that takes advantage of this feature by intrroducing Undecided nodes to KCFG: runtimeverification/pyk#744

@geo2a geo2a changed the title Branch on when Kore's cosntarint solver emits ErrorDecidePredicateUnknown Branch when Kore's cosntarint solver emits ErrorDecidePredicateUnknown Nov 28, 2023
@geo2a geo2a changed the title Branch when Kore's cosntarint solver emits ErrorDecidePredicateUnknown Branch when Kore's constraint solver emits ErrorDecidePredicateUnknown Nov 28, 2023
@geo2a geo2a mentioned this pull request Nov 28, 2023
Closed
@geo2a geo2a changed the title Branch when Kore's constraint solver emits ErrorDecidePredicateUnknown Abort when Kore's simplifier throws DecidePredicateUnknown Nov 30, 2023
@geo2a geo2a mentioned this pull request Nov 30, 2023
Open
2 tasks
@geo2a
Copy link
Contributor Author

geo2a commented Dec 8, 2023

KEVM Performace

I would not expect a regression, but seems like there is one in some cases? Also improvement in some other cases. I was running with one worker, but some other stuff has been going on that machine...

Test georgy-branch-on-unknown time master-7fa6410 time (georgy-branch-on-unknown/master-7fa6410) time
mcd/vat-move-diff-rough-spec.k 154.77 244.2 0.6337837837837839
mcd/flopper-file-pass-rough-spec.k 341.62 418.02 0.8172336251853979
mcd/vat-mului-pass-spec.k 99.42 113.0 0.8798230088495576
erc20/ds/transferFrom-failure-1-d-spec.k 79.05 84.69 0.9334041799504074
erc20/ds/transferFrom-failure-1-a-spec.k 105.57 110.12 0.9586814384308027
mcd/flipper-bids-pass-rough-spec.k 155.06 160.8 0.9643034825870647
benchmarks/structarg00-spec.k 56.46 54.44 1.0371050698016164
erc20/ds/transfer-success-1-spec.k 87.75 84.39 1.0398151439744046
mcd/dsvalue-read-pass-summarize-spec.k 67.89 65.21 1.0410979911056588
erc20/ds/transfer-failure-1-a-spec.k 90.92 87.24 1.0421824850985788
erc20/ds/transfer-failure-2-a-spec.k 86.64 83.06 1.043101372501806
mcd/dsvalue-peek-pass-rough-spec.k 73.62 70.31 1.0470772294126014
mcd/vat-muluu-pass-spec.k 105.13 100.4 1.0471115537848605
mcd/flopper-cage-pass-spec.k 76.84 73.38 1.0471518124829655
erc20/ds/transfer-failure-1-c-spec.k 66.97 63.92 1.0477158948685856
erc20/hkg/transfer-failure-2-spec.k 71.38 67.88 1.0515615792575133
mcd/flipper-ttl-pass-spec.k 74.11 70.36 1.0532973280272881
erc20/ds/approve-success-spec.k 73.61 69.83 1.054131462122297
erc20/hkg/transfer-failure-1-spec.k 73.73 69.84 1.0556987399770905
bihu/forwardToHotWallet-success-1-spec.k 76.62 72.44 1.0577029265599118
erc20/ds/transfer-success-2-spec.k 83.47 78.91 1.0577873526802688
mcd/end-subuu-pass-spec.k 70.09 66.25 1.0579622641509434
bihu/forwardToHotWallet-success-2-spec.k 76.96 72.6 1.0600550964187327
mcd/flipper-tau-pass-spec.k 74.13 69.91 1.0603633242740667
erc20/hkg/approve-spec.k 59.88 56.45 1.0607617360496013
bihu/forwardToHotWallet-failure-2-spec.k 87.88 82.73 1.0622506950320318
benchmarks/ecrecover00-sigvalid-spec.k 133.94 126.0 1.063015873015873
benchmarks/storagevar01-spec.k 58.46 54.96 1.0636826783114992
mcd/flipper-addu48u48-fail-rough-spec.k 65.1 61.13 1.0649435628987403
erc20/ds/approve-failure-spec.k 62.24 58.44 1.0650239561943875
mcd/dai-symbol-pass-spec.k 67.48 63.31 1.0658663718211974
examples/solidity-code-spec.md 221.79 207.44 1.0691766293868106
benchmarks/storagevar00-spec.k 54.31 50.77 1.0697262162694505
benchmarks/storagevar02-overflow-spec.k 61.36 57.34 1.070108126961981
erc20/hkg/transfer-success-1-spec.k 67.03 62.6 1.0707667731629393
erc20/hkg/balanceOf-spec.k 56.36 52.57 1.0720943503899563
erc20/hkg/allowance-spec.k 60.27 56.2 1.0724199288256229
erc20/ds/totalSupply-spec.k 55.57 51.79 1.0729870631396023
examples/erc20-spec.md 263.31 245.38 1.0730703398810009
erc20/hkg/transferFrom-success-2-spec.k 77.99 72.67 1.0732076510251822
mcd/dai-adduu-fail-rough-spec.k 61.61 57.39 1.073531974211535
erc20/hkg/transfer-success-2-spec.k 64.87 60.41 1.0738288362853834
erc20/ds/transfer-failure-2-b-spec.k 64.13 59.71 1.074024451515659
erc20/hkg/totalSupply-spec.k 51.56 47.95 1.0752867570385818
benchmarks/ecrecover00-siginvalid-spec.k 121.63 112.91 1.0772296519351696
erc20/ds/balanceOf-spec.k 59.96 55.61 1.0782233411256967
examples/storage-spec.md 228.64 209.0 1.0939712918660287
erc20/ds/allowance-spec.k 132.47 119.34 1.1100217864923747
functional/evm-int-simplifications-spec.k 144.68 129.15 1.1202477739063106
bihu/functional-spec.k 131.21 114.42 1.1467400804055237
erc20/ds/transferFrom-failure-1-b-spec.k 210.92 170.99 1.233522428212176
erc20/ds/transferFrom-failure-1-c-spec.k 168.84 130.62 1.292604501607717
mcd/cat-file-addr-pass-rough-spec.k 93.9 68.17 1.3774387560510488
mcd/cat-exhaustiveness-spec.k 278.67 199.77 1.394954197326926
bihu/forwardToHotWallet-failure-1-spec.k 195.2 126.37 1.5446704122813957
benchmarks/storagevar02-nooverflow-spec.k 103.26 57.87 1.7843442198030068
benchmarks/storagevar03-spec.k 112.35 52.82 2.1270352139341155
TOTAL 5998.680000000001 5583.479999999999 1.0743622257086982

@geo2a
Copy link
Contributor Author

geo2a commented Dec 8, 2023

Same sort of noisy result for Kontrol:

| AddrTest.test_notBuiltinAddress_concrete()                             | 25.27                         | 42.42               | 0.5957095709570956
| AssumeTest.testFail_assume_false(uint256,uint256)                      | 48.97                         | 69.42               | 0.7054163065399021
| AccountParamsTest.test_Nonce_NonExistentAddress()                      | 65.43                         | 83.42               | 0.7843442819467754
| src/tests/integration/test_foundry_prove.py::test_foundry_resume_proof | 89.09                         | 112.82              | 0.7896649530225138
| PlainPrankTest.test_prank_zeroAddress_true()                           | 189.94                        | 231.17              | 0.8216464074058053
| AccountParamsTest.test_getNonce_unknownSymbolic(address)               | 119.61                        | 141.19              | 0.8471563141865571
| ERC20.sol                                                              | 73.92                         | 86.24               | 0.8571428571428572
| AssertTest.test_revert_branch(uint256,uint256)                         | 79.29                         | 92.42               | 0.8579311837264662
| Setup2Test.testFail_setup()                                            | 133.33                        | 155.13              | 0.8594727003158642
| PlainPrankTest.test_startPrank_zeroAddress_true()                      | 177.84                        | 203.72              | 0.872962890241508
| AllowChangesTest.testAllow()                                           | 176.81                        | 201.1               | 0.8792143212332173
| PlainPrankTest.test_startPrankWithOrigin_true()                        | 169.71                        | 191.42              | 0.8865844739316687
| InitCodeTest.test_init()                                               | 202.42                        | 226.75              | 0.8927012127894156
| AccountParamsTest.test_Nonce_ExistentAddress()                         | 59.12                         | 66.21               | 0.8929164778734331
| AssumeTest.test_assume_false(uint256,uint256)                          | 83.29                         | 92.79               | 0.8976182778316629
| AllowChangesTest.testFailAllowCallsToAddress()                         | 191.21                        | 211.19              | 0.9053932477863535
| AddrTest.test_builtInAddresses()                                       | 25.87                         | 28.31               | 0.9138113740727659
| InitCodeTest.testFail_init()                                           | 147.86                        | 160.0               | 0.9241250000000001
| Setup2Test.test_setup()                                                | 59.35                         | 62.02               | 0.9569493711705901
| AddrTest.test_notBuiltinAddress_symbolic(address)                      | 67.68                         | 70.63               | 0.95823304544811
| AssertTest.testFail_assert_true()                                      | 40.87                         | 42.53               | 0.9609687279567364
| StoreTest.testGasLoadColdVM()                                          | 45.17                         | 46.93               | 0.9624973364585553
| StructTypeTest.test_vars((uint8,uint32,bytes32))                       | 40.98                         | 39.34               | 1.0416878495170308
| BlockParamsTest.testFee(uint256)                                       | 43.93                         | 41.94               | 1.047448736289938
| LabelTest.testLabel()                                                  | 38.6                          | 34.89               | 1.1063341931785613
| LoopsTest.sum_N(uint256)                                               | 141.66                        | 124.14              | 1.141130981150314
| AssertTest.test_assert_false()                                         | 81.01                         | 61.32               | 1.321102413568167
| AccountParamsTest.testDealSymbolic(uint256)                            | 73.68                         | 52.66               | 1.3991644511963541
| TOTAL                                                                  | 2691.9099999999994            | 2972.12             | 0.9057204958077061

@geo2a geo2a marked this pull request as ready for review December 8, 2023 10:54
goodlyrottenapple
goodlyrottenapple reviewed Dec 8, 2023
View reviewed changes
goodlyrottenapple
goodlyrottenapple approved these changes Dec 8, 2023
View reviewed changes
Copy link
Contributor

@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. Left a small code change suggestion

@geo2a geo2a added the automerge label Dec 8, 2023
@rv-jenkins rv-jenkins merged commit 9469f18 into main Dec 8, 2023
@rv-jenkins rv-jenkins deleted the georgy/branch-on-unknown branch December 8, 2023 13:42
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

@jberthold jberthold Awaiting requested review from jberthold

@tothtamas28 tothtamas28 Awaiting requested review from tothtamas28

1 more reviewer

@goodlyrottenapple goodlyrottenapple goodlyrottenapple approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

automerge

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

"execute" endpoint returns SMT error instead of Branching result

4 participants

@geo2a @goodlyrottenapple @rv-jenkins