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.

Sign up for GitHub

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

Jump to bottom

Invert --no-fallback-simplify and --no-post-exec-simplify (new default: no simplification) #4011

Closed
wants to merge 3 commits into from
Closed

Invert --no-fallback-simplify and --no-post-exec-simplify (new default: no simplification) #4011

wants to merge 3 commits into from

Conversation

jberthold
Copy link
Member

@jberthold jberthold commented Aug 1, 2024 •
edited
Loading

  • Introduces options --fallback-simplify and --post-exec-simplify to perform said simplifications (before fallbacks and after execute) in kore-rpc-booster
  • The default is changed to not simplify before fallbacks or after execution any more. To get the prior behaviour, both of the new options have to be given.
  • The old --no-fallback-simplify and --no-post-exec-simplify options are still accepted but not doing anything any more.

Needs discussion, see integration test changes

@jberthold
Invert --no-fallback-simplify and --no-post-exec-simplify (new de…
96d60f5 
…fault: no simplification)

* Introduces options `--fallback-simplify` and `--post-exec-simplify`
  to perform said simplifications (before fallbacks and after execute)
  in `kore-rpc-booster`
* The old `--no-fallback-simplify` and `--no-post-exec-simplify`
  options are still accepted but not doing anything any more.
@jberthold
Copy link
Member Author

jberthold commented Aug 1, 2024 •
edited
Loading

kontrol tests

Five tests failed on the branch:

FAILED src/tests/integration/test_foundry_prove.py::test_foundry_prove[AssumeTest.testFail_assume_true(uint256,uint256)]
FAILED src/tests/integration/test_foundry_prove.py::test_foundry_fail[AssumeTest.test_assume_false(uint256,uint256)]
FAILED src/tests/integration/test_foundry_prove.py::test_foundry_fail[AssumeTest.testFail_assume_false(uint256,uint256)]
FAILED src/tests/integration/test_foundry_prove.py::test_foundry_merge_nodes
FAILED src/tests/integration/test_foundry_prove.py::test_foundry_split_node

but 4 are comparing textual output and the fourth (test_foundry_merge_nodes) also failed on master.

Test HOTFIX-invert-proxy-simplify-options time master-e5a921f5a time (HOTFIX-invert-proxy-simplify-options/master-e5a921f5a) time
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_merge_loop_heads 41.84 131.37 0.3184897617416457
kontrol/src/tests/integration/test_foundry_prove.py::test_constructor_with_symbolic_args 25.98 76.62 0.33907595927956147
ImmutableVarsTest.test_run_deployment(uint256) 81.84 235.09 0.34812199583138376
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_refute_node 25.07 63.96 0.391963727329581
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_resume_proof 23.73 55.71 0.42595584275713516
AssertTest.testFail_expect_revert() 30.83 62.44 0.49375400384368995
HevmTests.prove_require_assert_true 14.85 29.99 0.49516505501833946
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_split_node 221.79 447.83 0.4952548958310073
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_remove_node 6.81 13.52 0.5036982248520709
SymbolicStorageTest.testFail_SymbolicStorage(uint256) 29.66 58.37 0.5081377419907487
BMCLoopsTest.test_countdown_concrete() 12.21 23.7 0.5151898734177216
StoreTest.testStoreLoadNonExistent() 13.38 24.21 0.5526641883519207
AssumeTest.testFail_assume_true(uint256,uint256) 21.04 38.0 0.5536842105263158
MockCallTestFoundry.testMockNested() 24.98 43.93 0.5686319144092875
SymbolicStorageTest.testFail_SymbolicStorage1(uint256) 34.74 59.31 0.5857359635811836
AssertTest.test_revert_branch(uint256,uint256) 35.94 60.78 0.5913129318854886
AssertTest.test_failing_branch(uint256) 37.05 62.46 0.5931796349663784
ArithmeticTest.test_max2(uint256,uint256) 18.87 31.45 0.6000000000000001
AccountParamsTest.testEtchConcrete() 22.88 37.69 0.6070575749535686
AssertTest.test_assert_true_branch(uint256) 22.68 36.89 0.6148007590132827
MockCallTestFoundry.testMockCalldata() 24.07 38.75 0.6211612903225806
MockCallTestFoundry.testMockGetters() 21.76 34.89 0.6236744052737174
MockFunctionTest.test_mock_function_concrete_args() 27.77 44.0 0.6311363636363636
HevmTests.proveFail_require_assert 18.51 29.3 0.631740614334471
MockFunctionTest.test_mock_function_all_args() 28.13 43.51 0.6465180418294645
ArithmeticTest.test_max1(uint256,uint256) 20.93 32.35 0.6469860896445131
SetUpDeployTest.test_extcodesize() 32.53 48.84 0.666052416052416
MockCallTestFoundry.testMockCallEmptyAccount() 24.24 36.2 0.6696132596685082
AssumeTest.test_assume_false(uint256,uint256) 32.8 48.95 0.6700715015321755
MockCallTestFoundry.testMockSelector() 19.18 28.45 0.6741652021089631
AssertTest.test_assert_true() 16.1 23.7 0.679324894514768
ExpectRevertTest.test_ExpectRevert_increasedDepth() 13.65 20.0 0.6825
CounterTest.testSetNumber(uint256) 15.07 22.03 0.6840671811166591
PlainPrankTest.test_startPrankWithOrigin_true() 13.1 19.14 0.6844305120167189
ExpectCallTest.testExpectStaticCall() 12.45 18.14 0.6863285556780595
AssertTest.checkFail_assert_false() 16.23 23.58 0.688295165394402
MockCallTest.testSelectorMockCall() 17.76 25.79 0.6886390073671966
PlainPrankTest.test_prank_zeroAddress_true() 14.41 20.89 0.6898037338439444
InitCodeTest.testFail_init() 31.83 45.51 0.6994067237969677
ExpectRevertTest.test_expectRevert_message() 13.6 19.37 0.7021166752710376
MockCallTestFoundry.testRevertMock() 18.31 25.99 0.7045017314351674
ExpectCallTest.testExpectRegularCall() 13.67 19.37 0.7057305110996386
AssumeTest.testFail_assume_false(uint256,uint256) 26.68 37.71 0.707504640678865
ExpectRevertTest.testFail_expectRevert_multipleReverts() 13.39 18.89 0.7088406564319746
AccountParamsTest.test_getNonce_unknownSymbolic(address) 21.73 30.48 0.7129265091863517
ExpectRevertTest.test_expectRevert_returnValue() 15.68 21.94 0.7146763901549681
CounterTest.testIncrement() 17.18 23.92 0.7182274247491638
InitCodeTest.test_init() 76.99 107.11 0.7187937634207824
ExpectRevertTest.test_expectRevert_true() 12.06 16.73 0.7208607292289301
HevmTests.proveFail_all_branches 27.26 37.45 0.7279038718291054
LoopsTest.test_sum_10() 14.18 19.45 0.7290488431876607
MockFunctionTest.test_mock_function() 35.65 48.88 0.7293371522094926
PlainPrankTest.test_prank_expectRevert() 13.65 18.71 0.7295563869588455
ExpectRevertTest.testFail_ExpectRevert_failAndSuccess() 14.42 19.72 0.731237322515213
ExpectRevertTest.testFail_expectRevert_false() 13.86 18.88 0.7341101694915254
SymbolicStorageTest.testEmptyInitialStorage(uint256) 13.83 18.62 0.742749731471536
AccountParamsTest.testFail_GetNonce_true() 15.08 20.22 0.7457962413452028
ExpectRevertTest.testFail_expectRevert_bytes4() 15.84 21.12 0.75
EmitContractTest.testExpectEmit() 12.99 17.23 0.7539175856065002
AssertTest.test_assert_false() 38.72 51.24 0.7556596409055425
AccountParamsTest.testNonceSymbolic(uint64) 19.3 25.45 0.7583497053045187
PlainPrankTest.test_startPrank_true() 14.07 18.5 0.7605405405405405
FreshBytesTest.test_symbolic_bytes_3 29.11 38.25 0.7610457516339869
EmitContractTest.testExpectEmitCheckEmitter() 12.52 16.37 0.7648136835675015
ExpectRevertTest.test_expectRevert_bytes4() 13.83 18.06 0.76578073089701
StoreTest.testGasStoreWarmUp() 13.81 17.96 0.7689309576837416
AllowChangesTest.testFailAllowChangesToStorage() 14.94 19.42 0.7693099897013387
EmitContractTest.testExpectEmitDoNotCheckData() 12.86 16.64 0.7728365384615384
StoreTest.testStoreLoad() 13.12 16.73 0.784219964136282
AllowChangesTest.testAllowSymbolic() 15.68 19.91 0.7875439477649422
AccountParamsTest.test_Nonce_ExistentAddress() 14.19 18.01 0.7878956135480287
StoreTest.testGasLoadWarmUp() 12.89 16.27 0.7922556853103873
BytesTypeTest.test_bytes4(bytes4) 12.88 16.25 0.7926153846153846
AccountParamsTest.test_Nonce_NonExistentAddress() 14.31 17.93 0.7981037367540436
EmitContractTest.testExpectEmitLessTopics() 12.69 15.89 0.7986154814348646
AllowChangesTest.testAllow() 27.71 34.61 0.8006356544351344
PlainPrankTest.test_startPrank_zeroAddress_true() 15.4 19.23 0.8008320332813312
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_auto_abstraction 25.18 31.39 0.8021662949984071
FreshBytesTest.test_symbolic_bytes_1 32.1 39.86 0.8053186151530357
PrankTestOrigin.test_origin_setup() 27.6 34.24 0.8060747663551402
BlockParamsTest.testChainId(uint256) 13.29 16.46 0.8074119076549209
PlainPrankTest.testFail_startPrank_internalCall() 13.43 16.59 0.8095238095238095
AssertTest.testFail_assert_true() 27.22 33.59 0.8103602262578147
AllowChangesTest.testFailAllowCallsToAddress() 16.01 19.64 0.8151731160896131
PrankTestMsgSender.test_msgsender_setup() 26.64 32.51 0.8194401722546909
StoreTest.testGasStoreColdVM() 12.11 14.67 0.825494205862304
FreshCheatcodes.test_address() 15.01 18.14 0.8274531422271223
StoreTest.testGasLoadColdVM() 13.39 16.06 0.8337484433374845
AssumeTest.test_multi_assume(address,address) 17.35 20.76 0.8357418111753372
FreshCheatcodes.test_freshSymbolicWord() 13.54 16.2 0.8358024691358025
Setup2Test.test_setup() 13.87 16.55 0.8380664652567975
StartPrankTestOrigin.test_startprank_origin_setup() 27.44 32.67 0.839914294459749
ExpectRevertTest.testFail_expectRevert_empty() 11.24 13.35 0.8419475655430712
AccountParamsTest.test_GetNonce_true() 13.59 16.07 0.8456751711263223
BlockParamsTest.testFee(uint256) 14.17 16.75 0.8459701492537314
StartPrankTestMsgSender.test_startprank_msgsender_setup() 26.11 30.58 0.8538260300850229
AssumeTest.test_assume_true(uint256,uint256) 14.39 16.8 0.856547619047619
],uint256)) 39.3 45.74 0.859204197638828
AssumeTest.test_assume_staticCall(bool) 14.61 16.96 0.861438679245283
FreshCheatcodes.test_bool() 17.39 20.17 0.8621715418939018
AccountParamsTest.testDealSymbolic(uint256) 17.74 20.57 0.8624210014584345
BlockParamsTest.testRoll(uint256) 13.65 15.8 0.8639240506329113
AddrTest.test_builtInAddresses() 11.45 13.09 0.8747135217723453
LoopsTest.sum_N(uint256) 129.0 147.04 0.8773122959738847
PlainPrankTest.test_stopPrank_notExistent() 11.15 12.66 0.8807266982622433
HevmTests.prove_require_assert_false 32.74 37.16 0.881054897739505
BytesTypeTest.test_bytes32(bytes32) 11.72 13.15 0.8912547528517111
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_show_with_hex_encoding 6.79 7.58 0.895778364116095
BlockParamsTest.testBlockNumber() 11.53 12.87 0.8958818958818959
Setup2Test.testFail_setup() 27.99 31.23 0.8962536023054755
LabelTest.testLabel() 11.59 12.86 0.901244167962675
GasTest.testSetGas() 11.83 13.09 0.9037433155080214
WarpTest.test_warp_setup() 25.0 27.61 0.9054690329590728
CoinBaseTest.test_coinbase_setup() 25.43 27.88 0.9121233859397417
AssertTest.prove_assert_true() 13.48 14.74 0.9145183175033922
FreshCheatcodes.test_int128() 12.05 13.17 0.914958238420653
MethodDisambiguateTest.test_method_call() 15.29 16.66 0.917767106842737
StructTypeTest.test_vars((uint8,uint32,bytes32)) 12.13 13.2 0.9189393939393941
FeeTest.test_fee_setup() 25.58 27.83 0.9191519942508085
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_xml_report 21.01 22.68 0.9263668430335098
AddrTest.test_notBuiltinAddress_symbolic(address) 15.9 17.08 0.930913348946136
ChainIdTest.test_chainid_setup() 25.79 27.65 0.9327305605786619
UintTypeTest.test_uint256(uint256) 15.47 16.56 0.9341787439613528
AddrTest.test_notBuiltinAddress_concrete() 12.13 12.96 0.9359567901234568
StoreTest.testLoadNonExistent() 11.79 12.43 0.9485116653258245
RollTest.test_roll_setup() 26.66 27.87 0.9565841406530319
BlockParamsTest.testCoinBase() 12.01 12.55 0.9569721115537848
BlockParamsTest.testWarp(uint256)-trace_options2 21.94 20.17 1.0877540902330194
AccountParamsTest.testDealConcrete()-trace_options0 20.54 18.72 1.0972222222222223
ConstructorTest.test_constructor() 63.9 55.2 1.1576086956521738
ERC20.sol 70.16 56.35 1.245075421472937
Storage.sol 73.11 56.56 1.2926096181046676
kontrol/src/tests/integration/test_foundry_prove.py::test_foundry_prove_skips_setup 131.6 100.59 1.3082811412665274
AddrTest.test_addr_true()-trace_options1 29.46 21.57 1.3657858136300418
ConstructorTest.testFail_constructor() 35.81 24.78 1.4451170298627927
ConstructorArgsTest.test_constructor_args() 84.72 56.66 1.4952347334980587
SetUpTest.testSetupData() 54.64 28.93 1.8886968544763223
Test HOTFIX-invert-proxy-simplify-options time master-e5a921f5a time (HOTFIX-invert-proxy-simplify-options/master-e5a921f5a) time
TOTAL 3458.53 4759.1 0.7267193376898992

jberthold
jberthold commented Aug 1, 2024
View reviewed changes
booster/test/rpc-integration/test-vacuous/response-vacuous-but-rewritten.json
Comment on lines -5 to 6
"reason": "vacuous",
"reason": "stuck",
"depth": 1,
Copy link
Member Author

@jberthold jberthold Aug 1, 2024 •
edited
Loading

Choose a reason for hiding this comment

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

This might be a deal-breaker for the PR:

  • without --post-exec-simplify, kore-rpc-booster does not recognise that the result is vacuous (the input state was already vacuous, having N ==Int 1 andBool N =/=Int 1 in the predicate).
  • Also, the split between predicates and substitutions is not happening in the same way as in kore-rpc / fallbacks (see other tests).

Copy link
Collaborator

Choose a reason for hiding this comment

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

I think we are unlikely to end-up in this situation in the first place, because Booster checks consistency of ensured conditions and would report if it makes the pattern #Bottom during rewriting, i.e. executing the state

Term:
    <generatedTop>(
        <k>(kseq("init", dotk())),
        <int>("0"),
        <generatedCounter>("0")
    )
Conditions:

results in a vacuous response after an attempt to apply the init rule:

"result": {"reason":"vacuous","depth":0, ...

and the logs would show:

[booster][execute][term e7bdd85][rewrite 29b5f78][detail] TEST.init
[booster][execute][term e7bdd85][rewrite 29b5f78][match][success] TEST.init
[booster][execute][term e7bdd85][rewrite 29b5f78][match][success][substitution] Substitution: Rule#Var_DotVar0:SortGeneratedCounterCell{} -> <generatedCounter>("0") , Rule#VarX:SortInt{} -> "0" , Rule#Var_Gen4:SortIntCell{} -> <int>("0") , Rule#Var_DotVar1:SortK{} -> dotk()
[booster][execute][term e7bdd85][rewrite 29b5f78][constraint][term d6e7b73][kore-term] _==Int_("0", "42")
[booster][execute][term e7bdd85][rewrite 29b5f78][constraint][term d6e7b73][hook INT.eq][success][term 9eb81e8][kore-term] "false"
[booster][execute][term e7bdd85][rewrite e7fa1c1][detail] TEST.JNIT-E
[booster][execute][term e7bdd85][rewrite e7fa1c1][match][failure] Values differ:"jnit" "init"
[booster][execute][term e7bdd85][rewrite 928fbc2][detail] TEST.JNIT-F
[booster][execute][term e7bdd85][rewrite 928fbc2][match][failure] Values differ:"jnit" "init"
[booster][execute][term e7bdd85][kore-term] <generatedTop>(<k>(kseq("init", dotk())), <int>("0"), <generatedCounter>("0"))
[booster][execute][term e7bdd85] Simplified to bottom after 0 steps.

We are fine in "execute" requests, because Booster would never produce state-vacuous-but-rewritten.execute anymore. It would have before, as we did not have the SMT solver to prune the contradictory ensured conditions.

I have a related comment about the "simplify" requests, but I'll post it in a separate comment.

jberthold
jberthold commented Aug 1, 2024
View reviewed changes
scripts/booster-integration-tests.sh
Comment on lines +62 to +65
"issue3764-vacuous-branch")
# must discover the vacuous branch during post-exec simplification
SERVER=$KORE_RPC_BOOSTER SERVER_OPTS="--post-exec-simplify" ./runDirectoryTest.sh test-$name $@
;;
Copy link
Member Author

Choose a reason for hiding this comment

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

This test was specifically addressing the problem that a vacuous branch was only recognised as such in the post-exec simplification (see issue #3764).

@jberthold jberthold marked this pull request as ready for review August 1, 2024 04:09
@geo2a
Copy link
Collaborator

geo2a commented Aug 1, 2024

Perhaps we need to consider changing the behaviour of the "simplify" endpoint in Booster, as it's different from what Kore does. When asked to simplify the state state-vacuous-but-rewritten.execute:

Term:
    <generatedTop>(
        <k>(kseq("b", dotk())),
        <int>(N:SortInt{}),
        <generatedCounter>("0")
    )
Conditions:
    _=/=Int_(N:SortInt{}, "0")
    _==Int_(N:SortInt{}, "0")

which is a pattern with contradictory constraints, booster-dev returns the pattern almost unchanged:

Term:
    <generatedTop>(
        <k>(kseq("b", dotk())),
        <int>(N:SortInt{}),
        <generatedCounter>("0")
    )
Conditions:
    _==Int_(N:SortInt{}, "0")
    notBool_(_==Int_(N:SortInt{}, "0"))

while kore-rpc-booster will return #Bottom (via Kore):

[request 1][proxy][timing] Performed SimplifyM in 0.45s (0.41s kore time)
[request 1][proxy][abort][detail] Kore simplification: Diff (< before - > after)
*** /tmp/extra-dir-51565986628734/diff_file1.txt	2024-08-01 08:37:36.610508904 +0200
--- /tmp/extra-dir-51565986628734/diff_file2.txt	2024-08-01 08:37:36.610508904 +0200
***************
*** 1,9 ****
- Term:
-     <generatedTop>(
-         <k>(kseq("b", dotk())),
-         <int>(N:SortInt{}),
-         <generatedCounter>("0")
-     )
  Conditions:
!     _==Int_(N:SortInt{}, "0")
!     notBool_(_==Int_(N:SortInt{}, "0"))
\ No newline at end of file
--- 1,4 ----
  Conditions:
! Ceil conditions:
! Substitutions:Unsupported parts:
! {"sort":{"args":[],"name":"SortGeneratedTopCell","tag":"SortApp"},"tag":"Bottom"}

that means that ApplyEquations.evaluatePattern --- the function behind the "simplify" endpoint in Booster, is unable to detect a contradiction in constraints. And this is indeed the case, since it evaluates every constraint assuming all the others, but never calls Z3 on them together as we do when rewriting.

Same happens if we isolate the constraints and ask the servers to simplify that:

request 1][proxy][timing] Performed SimplifyM in 0.49s (0.47s kore time)
[request 1][proxy][abort][detail] Kore simplification: Diff (< before - > after)
*** /tmp/extra-dir-51565986628735/diff_file1.txt	2024-08-01 08:40:47.352321295 +0200
--- /tmp/extra-dir-51565986628735/diff_file2.txt	2024-08-01 08:40:47.352321295 +0200
***************
*** 1,5 ****
  Conditions:
-     _==Int_(N:SortInt{}, "0")
-     notBool_(_==Int_(N:SortInt{}, "0"))
  Ceil conditions:
! Substitutions:
\ No newline at end of file
--- 1,4 ----
  Conditions:
  Ceil conditions:
! Substitutions:Unsupported parts:
! {"sort":{"args":[],"name":"SortGeneratedTopCell","tag":"SortApp"},"tag":"Bottom"}

and indeed, the "simplify" endpoint, when it receives predicates only, simplifies them in isolation and never checks their combined consistency.

I understand that this behaviour of the "simplify" endpoint in Booster is intentional, since, for most of its lifetime, Booster did not have an SMT solver and thus we've geared to towards simplifying constraints in isolation. Perhaps it's time to change that.

@geo2a
Copy link
Collaborator

geo2a commented Aug 1, 2024

We have agreed to make the bahaviour of the "simplify" endpoint on Booster consistent with Kore (see #4012). After that has been done, we can merge this change as well.

@geo2a geo2a mentioned this pull request Aug 7, 2024
Open
@jberthold
Copy link
Member Author

Superseded by #4020

@jberthold jberthold closed this Aug 9, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@goodlyrottenapple goodlyrottenapple Awaiting requested review from goodlyrottenapple

@geo2a geo2a Awaiting requested review from geo2a

Assignees

@geo2a geo2a

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@jberthold @geo2a