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

Explore the remainder branch when Booster is uncertain about rewrite rule conditions #3960

Draft
wants to merge 70 commits into
base: master
Choose a base branch
from
Draft

Explore the remainder branch when Booster is uncertain about rewrite rule conditions #3960

wants to merge 70 commits into from

Conversation

geo2a
Copy link
Collaborator

@geo2a geo2a commented Jun 24, 2024

Part of #3956

geo2a and others added 23 commits June 24, 2024 15:52
@geo2a
Add condition to Applied
09f8916
@geo2a
Allow assuming unclear requires clauses
254e877
@geo2a
Draft remainder predicate computation and check
1ee240d
@goodlyrottenapple
Reorganised doSteps function in performRewrite
b67a97f
Format with fourmolu
0d6092b
@goodlyrottenapple
further tweaks to performRewrite
a5e8318
@goodlyrottenapple
merge
770d65b
@goodlyrottenapple
implment isSat
3a47065
@goodlyrottenapple
actually return the branching condition as part of the rewritten patt…
c5dd30b 
…ern + fix unit tests
@goodlyrottenapple
fourmolu
07189d7
@goodlyrottenapple
Merge branch 'master' into georgy/booster-remainders
b0fd4e8
@goodlyrottenapple
merge master
5f5e2de
@goodlyrottenapple
misc
cee50e9
@geo2a
Log rule remainder predicates
e384a97
@geo2a
Continue with lower-priority rules if no rules applied group
e70bdca
@geo2a
Merge remote-tracking branch 'origin/master' into georgy/booster-rema…
ded261a 
…inders
@geo2a
Fix KEVM script by calling the new Makefile target
ac350fd
@geo2a
Merge remote-tracking branch 'origin/master' into georgy/booster-rema…
775218c 
…inders
@geo2a
Increment rewrite depth counter in the same way as before, add comments
cab49d7
@geo2a
Log uncovered remainder
b4d3a99
@geo2a
Increment depth counter when pruning branch in post-simpl
fafaf13
@geo2a
Add rule predicates
5e03d41
@geo2a
Apply substitution to the rule predicate
391b47c
@geo2a geo2a force-pushed the georgy/booster-remainders branch from 9d065d9 to 391b47c Compare July 7, 2024 14:33
@geo2a geo2a force-pushed the georgy/booster-remainders branch from 71ba327 to ad42fbd Compare July 7, 2024 14:55
geo2a added 12 commits July 12, 2024 08:43
@geo2a
Only emit proxy branch-eliminating rewrite trace when asked for
6d730a5
@geo2a
Update output of test-3934-smt: slight change in rule predicate
4e1524e
@geo2a
Merge remote-tracking branch 'origin/master' into georgy/booster-rema…
4d12b6a 
…inders
@geo2a
Do not ignore rule predicates in unit-tests, only rule subst
18ca384
@geo2a
Merge remote-tracking branch 'origin/master' into georgy/booster-rema…
6ef5cd3 
…inders
@geo2a
Merge remote-tracking branch 'origin/master' into georgy/booster-rema…
8d1c69e 
…inders
@geo2a
Merge remote-tracking branch 'origin/master' into georgy/booster-rema…
c072d46 
…inders
@geo2a
Merge remote-tracking branch 'origin/master' into georgy/booster-rema…
979606a 
…inders
@geo2a
Merge remote-tracking branch 'origin/master' into georgy/booster-rema…
9c82e4e 
…inders
@geo2a
Make default fallback reasons more explicit, fix comment
8c943d3
@geo2a
Refactor result printing messages
13b4b9e
@geo2a
Add a new handler for Booster Branching in Proxy.hs
3b179b2
@geo2a geo2a force-pushed the georgy/booster-remainders branch from ca12819 to 3b179b2 Compare July 24, 2024 08:35
geo2a and others added 5 commits July 26, 2024 11:59
@geo2a
Update kore-rpc-client to use tar-0.6.3 (#3996)
cbfa774 
With runtimeverification/k#4548, the bug reports
will be generated in GNU format of tar files instead of the default
POSIX.1-2001 pax format. This is necessary because:
- the filenames in the bug reports are often longer than the
format-portable restriction of 256 characters
- the Haskell [library](https://hackage.haskell.org/package/tar-0.6.3.0)
we use to work with tar does not support the pax format. However, it
does support the GNU format which also allows long names.

With this change, we get to process bug reports with long names.
@jberthold @geo2a
Fixes to simplification diff, request statistics, process-logs (#3992)
01c344c 
* Add some context lines to simplification diff 
* compute request statistics in seconds (and output in seconds in the
json format)
* Make `process-logs` fail immediately on parse errors, and process
lines incrementally (less heap)
@geo2a
TEMP comment-out Kore fallback
b7590bc
@geo2a
Merge remote-tracking branch 'origin/master' into georgy/booster-rema…
f52088d 
…inders
@geo2a
Merge remote-tracking branch 'origin/master' into georgy/booster-rema…
7bf75ea 
…inders
@geo2a
Copy link
Collaborator Author

geo2a commented Jul 30, 2024

KEVM performance at 7bf75ea:

| Test                                                                    | georgy-booster-remainders time | master-3b90f2b79 time | (georgy-booster-remainders/master-3b90f2b79) time
|-------------------------------------------------------------------------|--------------------------------|-----------------------|---------------------------------------------------
| mcd/flopper-dent-guy-same-pass-rough-spec.k                             | 923.28                         | 971.42                | 0.9504436803854152
| mcd/end-subuu-pass-spec.k                                               | 58.38                          | 61.04                 | 0.956422018348624
| mcd/flopper-dent-guy-diff-tic-not-0-pass-rough-spec.k                   | 1012.77                        | 1056.91               | 0.9582367467428635
| kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k | 57.41                          | 59.82                 | 0.95971247074557
| mcd/flopper-tick-pass-rough-spec.k                                      | 217.44                         | 225.81                | 0.9629334396173774
| erc20/hkg/transferFrom-success-2-spec.k                                 | 60.72                          | 58.62                 | 1.0358239508700102
| kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k    | 77.34                          | 74.53                 | 1.0377029384140615
| erc20/ds/transferFrom-failure-1-c-spec.k                                | 118.03                         | 113.72                | 1.0379001055223356
| kontrol/test-allowchangestest-testallow_fail-0-spec.k                   | 54.75                          | 52.66                 | 1.0396885681731864
| kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k     | 53.58                          | 51.44                 | 1.041601866251944
| erc20/hkg/transferFrom-failure-1-spec.k                                 | 94.08                          | 89.88                 | 1.046728971962617
| mcd/end-cash-pass-rough-spec.k                                          | 229.3                          | 218.66                | 1.0486600201225649
| erc20/ds/transferFrom-failure-1-b-spec.k                                | 151.48                         | 144.06                | 1.0515063168124392
| erc20/ds/transfer-failure-1-a-spec.k                                    | 75.35                          | 71.45                 | 1.0545836249125262
| benchmarks/ecrecoverloop00-sig1-invalid-spec.k                          | 118.31                         | 109.35                | 1.0819387288523092
| TOTAL                                                                   | 3302.22                        | 3359.3699999999994    | 0.9829878816563821

@geo2a geo2a mentioned this pull request Jul 30, 2024
Open
@geo2a geo2a force-pushed the georgy/booster-remainders branch from fcc8ed0 to a580cfc Compare August 6, 2024 15:29
@geo2a geo2a mentioned this pull request Aug 20, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

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