HOTFIX invalidate cache when modifying known predicates #4103
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
The change in #3953 introduced additional arguments to evaluation functions which allow callers to supply some "known true" predicates for the simplification and evaluation. However, doing so means that the cache will get populated with associations that might only be true if this known truth does not change. The case in point was a predicate being cached as "true" because of an earlier evaluation, and then _removed_ from the path condition. This change removes returning the cache from any inteface functions that take known truth arguments, and runs internal computations that modify the predicates with a fresh empty cache.
This comment was marked as outdated.
This comment was marked as outdated.
…lugin dep The plugin has recently been changed, and appears to require `--no-write-lock-file` when building under a nix flake. In turn, the integration with llvm-kompile is now easier, a single library file needs to be linked into the LLVM interpreter.
…ache-when-modifying-known-predicates
|
...better performance now when we avoid re-simplifying the constraints each time we simplify the term
|
| Test | HOTFIX-invalidate-cache-when-modifying-known-predicates time | master-2a5be7830 time | (HOTFIX-invalidate-cache-when-modifying-known-predicates/master-2a5be7830) time |
|---|---|---|---|
| mcd-structured/pot-join-pass-rough-spec.k | 122.88 | 129.66 | 0.9477093937991671 |
| mcd/flopper-tick-pass-rough-spec.k | 130.97 | 125.66 | 1.0422568836543054 |
| mcd/vow-flog-fail-rough-spec.k | 94.32 | 90.36 | 1.043824701195219 |
| mcd/vow-fess-fail-rough-spec.k | 91.37 | 87.16 | 1.0483019733822856 |
| mcd/dstoken-approve-fail-rough-spec.k | 75.26 | 71.72 | 1.0493586168432796 |
| mcd-structured/vow-fess-fail-rough-spec.k | 90.69 | 86.24 | 1.051600185528757 |
| mcd/flopper-dent-guy-same-pass-rough-spec.k | 483.18 | 455.78 | 1.0601167229803854 |
| mcd/flopper-kick-pass-rough-spec.k | 114.75 | 107.94 | 1.0630906058921623 |
| mcd/end-pack-pass-rough-spec.k | 119.01 | 110.75 | 1.0745823927765237 |
| mcd/end-cash-pass-rough-spec.k | 160.47 | 149.07 | 1.0764741396659288 |
| mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k | 651.15 | 601.33 | 1.082849683202235 |
| mcd/flapper-yank-pass-rough-spec.k | 145.32 | 133.46 | 1.0888655777011838 |
| mcd/pot-join-pass-rough-spec.k | 173.23 | 157.78 | 1.0979211560400557 |
| mcd/cat-exhaustiveness-spec.k | 102.57 | 90.7 | 1.1308710033076075 |
| mcd-structured/cat-exhaustiveness-spec.k | 100.68 | 87.99 | 1.144220934197068 |
| TOTAL | 2655.85 | 2485.6 | 1.0684945284840683 |
kontrol tests
| Test | HOTFIX-invalidate-cache-when-modifying-known-predicates time | master-d3c36c17e time | (HOTFIX-invalidate-cache-when-modifying-known-predicates/master-d3c36c17e) time |
|---|---|---|---|
| ExpectRevertTest.testFail_expectRevert_empty() | 7.09 | 9.37 | 0.7566702241195304 |
| SymbolicStorageTest.testEmptyInitialStorage(uint256) | 9.53 | 11.79 | 0.8083121289228159 |
| StoreTest.testGasStoreColdVM() | 8.7 | 10.74 | 0.8100558659217876 |
| EmitContractTest.testExpectEmitLessTopics() | 9.37 | 11.18 | 0.8381037567084079 |
| BlockParamsTest.testRoll(uint256) | 7.93 | 9.44 | 0.840042372881356 |
| FeeTest.test_fee_setup() | 14.0 | 16.39 | 0.8541793776693105 |
| ExpectRevertTest.test_expectRevert_message() | 11.48 | 13.04 | 0.8803680981595093 |
| BlockParamsTest.testChainId(uint256) | 7.97 | 8.96 | 0.8895089285714285 |
| ChainIdTest.test_chainid_setup() | 13.73 | 15.15 | 0.9062706270627062 |
| AssertTest.prove_assert_true() | 7.14 | 7.58 | 0.941952506596306 |
| CopyStorageTest.testCopyStorage() | 22.28 | 23.38 | 0.9529512403763901 |
| ]) | 27.49 | 28.68 | 0.958507670850767 |
| test_foundry_show_with_hex_encoding | 3.11 | 3.24 | 0.9598765432098765 |
| AssumeTest.testFail_assume_true(uint256,uint256) | 20.51 | 21.34 | 0.9611059044048735 |
| test_foundry_refute_node | 7.09 | 6.84 | 1.036549707602339 |
| AssertTest.checkFail_assert_false() | 9.83 | 9.43 | 1.0424178154825028 |
| HevmTests.prove_revert | 7.5 | 7.16 | 1.047486033519553 |
| StoreTest.testStoreLoadNonExistent() | 7.84 | 7.48 | 1.0481283422459893 |
| AddrTest.test_notBuiltinAddress_concrete() | 7.35 | 6.92 | 1.0621387283236994 |
| AssumeTest.test_assume_staticCall(bool) | 8.9 | 8.29 | 1.0735826296743065 |
| ],uint256)) | 17.62 | 16.08 | 1.0957711442786071 |
| CounterTest.testIncrement() | 13.13 | 11.9 | 1.1033613445378152 |
| SymbolicStorageTest.testFail_SymbolicStorage(uint256) | 24.24 | 21.86 | 1.1088746569075938 |
| FreshBytesTest.test_symbolic_bytes_1 | 25.14 | 22.51 | 1.116836961350511 |
| BlockParamsTest.testBlockNumber() | 7.58 | 6.71 | 1.1296572280178838 |
| FreshBytesTest.test_symbolic_bytes_3 | 25.18 | 22.05 | 1.1419501133786847 |
| BlockParamsTest.testFee(uint256) | 9.15 | 8.01 | 1.1423220973782773 |
| ExpectRevertTest.test_expectRevert_bytes4() | 12.4 | 10.76 | 1.1524163568773236 |
| EmitContractTest.testExpectEmitCheckEmitter() | 10.79 | 9.2 | 1.1728260869565217 |
| StoreTest.testGasStoreWarmUp() | 11.55 | 9.82 | 1.1761710794297353 |
| BytesTypeTest.test_bytes4(bytes4) | 8.78 | 7.39 | 1.1880920162381596 |
| ExpectRevertTest.test_expectRevert_true() | 11.05 | 9.23 | 1.1971830985915493 |
| ExpectRevertTest.testFail_expectRevert_multipleReverts() | 12.48 | 10.34 | 1.206963249516441 |
| ConstructorTest.run_constructor() | 8.07 | 6.62 | 1.2190332326283988 |
| TOTAL | 416.0 | 408.88 | 1.017413422030914 |
tothtamas28
approved these changes
Apr 16, 2025
jberthold
deleted the
HOTFIX-invalidate-cache-when-modifying-known-predicates
branch
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
The change in #3953 introduced additional arguments to evaluation functions which allow callers to supply some "known true" predicates for the simplification and evaluation. However, doing so means that the cache will get populated with associations that might only be true if this known truth does not change.
The case in point was a predicate being cached as "true" because of an earlier evaluation, and then removed from the path condition (see added integration test).
This change
checkConstraintfunctions to fix the pattern constraintscheckConstraint, andFurthermore, to avoid a significant performance penalty, we
ensures), this constraint is evaluated before adding itWe are not using the SMT solver to detect a vacuous state at the start, though, could add that separately if desired. At the moment, the behaviour is largely the same as before (integration test expectations identical except for some evaluation in vacuous states).