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

Closed
wants to merge 73 commits into from
Closed

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

wants to merge 73 commits into from

Commits on Jun 24, 2024

  1. Add condition to Applied

    @geo2a
    geo2a committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    09f8916 View commit details
    Browse the repository at this point in the history

  2. Allow assuming unclear requires clauses

    @geo2a
    geo2a committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    254e877 View commit details
    Browse the repository at this point in the history

  3. Draft remainder predicate computation and check

    @geo2a
    geo2a committed Jun 24, 2024
    Configuration menu
    Copy the full SHA
    1ee240d View commit details
    Browse the repository at this point in the history

Commits on Jun 26, 2024

  1. Reorganised doSteps function in performRewrite

    @goodlyrottenapple
    goodlyrottenapple committed Jun 26, 2024
    Configuration menu
    Copy the full SHA
    b67a97f View commit details
    Browse the repository at this point in the history

  2. Format with fourmolu

    github-actions committed Jun 26, 2024
    Configuration menu
    Copy the full SHA
    0d6092b View commit details
    Browse the repository at this point in the history

Commits on Jun 27, 2024

  1. further tweaks to performRewrite

    @goodlyrottenapple
    goodlyrottenapple committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    a5e8318 View commit details
    Browse the repository at this point in the history

  2. merge

    @goodlyrottenapple
    goodlyrottenapple committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    770d65b View commit details
    Browse the repository at this point in the history

  3. implment isSat

    @goodlyrottenapple
    goodlyrottenapple committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    3a47065 View commit details
    Browse the repository at this point in the history

  4. actually return the branching condition as part of the rewritten patt… 

    …ern + fix unit tests
    @goodlyrottenapple
    goodlyrottenapple committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    c5dd30b View commit details
    Browse the repository at this point in the history

  5. fourmolu

    @goodlyrottenapple
    goodlyrottenapple committed Jun 27, 2024
    Configuration menu
    Copy the full SHA
    07189d7 View commit details
    Browse the repository at this point in the history

  6. Merge branch 'master' into georgy/booster-remainders

    @goodlyrottenapple
    goodlyrottenapple authored Jun 27, 2024
    Configuration menu
    Copy the full SHA
    b0fd4e8 View commit details
    Browse the repository at this point in the history

Commits on Jun 28, 2024

  1. merge master

    @goodlyrottenapple
    goodlyrottenapple committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    5f5e2de View commit details
    Browse the repository at this point in the history

  2. misc

    @goodlyrottenapple
    goodlyrottenapple committed Jun 28, 2024
    Configuration menu
    Copy the full SHA
    cee50e9 View commit details
    Browse the repository at this point in the history

Commits on Jul 1, 2024

  1. Log rule remainder predicates

    @geo2a
    geo2a committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    e384a97 View commit details
    Browse the repository at this point in the history

  2. Continue with lower-priority rules if no rules applied group

    @geo2a
    geo2a committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    e70bdca View commit details
    Browse the repository at this point in the history

  3. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    ded261a View commit details
    Browse the repository at this point in the history

  4. Fix KEVM script by calling the new Makefile target

    @geo2a
    geo2a committed Jul 1, 2024
    Configuration menu
    Copy the full SHA
    ac350fd View commit details
    Browse the repository at this point in the history

Commits on Jul 2, 2024

  1. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 2, 2024
    Configuration menu
    Copy the full SHA
    775218c View commit details
    Browse the repository at this point in the history

  2. Increment rewrite depth counter in the same way as before, add comments

    @geo2a
    geo2a committed Jul 2, 2024
    Configuration menu
    Copy the full SHA
    cab49d7 View commit details
    Browse the repository at this point in the history

  3. Log uncovered remainder

    @geo2a
    geo2a committed Jul 2, 2024
    Configuration menu
    Copy the full SHA
    b4d3a99 View commit details
    Browse the repository at this point in the history

Commits on Jul 7, 2024

  1. Increment depth counter when pruning branch in post-simpl

    @geo2a
    geo2a committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    fafaf13 View commit details
    Browse the repository at this point in the history

  2. Add rule predicates

    @geo2a
    geo2a committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    5e03d41 View commit details
    Browse the repository at this point in the history

  3. Apply substitution to the rule predicate

    @geo2a
    geo2a committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    391b47c View commit details
    Browse the repository at this point in the history

  4. Return rule substitution

    @geo2a
    geo2a committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    ad42fbd View commit details
    Browse the repository at this point in the history

  5. Make rule predicate construction more explicit

    @geo2a
    geo2a committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    7ee244d View commit details
    Browse the repository at this point in the history

  6. Do not return rule substitution for now

    @geo2a
    geo2a committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    6b7bb6a View commit details
    Browse the repository at this point in the history

  7. Use termSort when externalising rule predicate

    @geo2a
    geo2a committed Jul 7, 2024
    Configuration menu
    Copy the full SHA
    bf200c3 View commit details
    Browse the repository at this point in the history

Commits on Jul 8, 2024

  1. Ignore rule predicate and substitution in unit tests

    @geo2a
    geo2a committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    d6e2043 View commit details
    Browse the repository at this point in the history

  2. Log rule priorities when processing groups

    @geo2a
    geo2a committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    f65cd34 View commit details
    Browse the repository at this point in the history

  3. Remove directory name assumption in kore-rpc-client

    @geo2a
    geo2a committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    2ae3693 View commit details
    Browse the repository at this point in the history

  4. Return False when the remainder is trivial

    @geo2a
    geo2a committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    119476a View commit details
    Browse the repository at this point in the history

  5. Check remainder for literal false when there's not SMT solver

    @geo2a
    geo2a committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    221083e View commit details
    Browse the repository at this point in the history

  6. Add test-remainder-predicates integration test

    @geo2a
    geo2a committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    00898f4 View commit details
    Browse the repository at this point in the history

  7. Oops, remove awkward print

    @geo2a
    geo2a committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    df0047f View commit details
    Browse the repository at this point in the history

  8. Add comment

    @geo2a
    geo2a committed Jul 8, 2024
    Configuration menu
    Copy the full SHA
    555728d View commit details
    Browse the repository at this point in the history

Commits on Jul 9, 2024

  1. Bring back the abort message on unclear rewrite rule match

    @geo2a
    geo2a committed Jul 9, 2024
    Configuration menu
    Copy the full SHA
    2d0b0fd View commit details
    Browse the repository at this point in the history

Commits on Jul 10, 2024

  1. Refactor match remainder into a function to deduplicate code

    @geo2a
    geo2a committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    554d701 View commit details
    Browse the repository at this point in the history

  2. Factor-out mkRulePredicate

    @geo2a
    geo2a committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    d8e712f View commit details
    Browse the repository at this point in the history

  3. Ignore rule substitution when comparing branching responses

    @geo2a
    geo2a committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    b709fb8 View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    c3a88f2 View commit details
    Browse the repository at this point in the history

  5. Do not send trivial remainders to SMT

    @geo2a
    geo2a committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    55c9dcf View commit details
    Browse the repository at this point in the history

  6. Remove trivial rule predicates from tests

    @geo2a
    geo2a committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    e5f674c View commit details
    Browse the repository at this point in the history

  7. Rework test-use-path-condition-in-equations

    @geo2a
    geo2a committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    f227ad7 View commit details
    Browse the repository at this point in the history

  8. Update test-non-linear-int-requires

    @geo2a
    geo2a committed Jul 10, 2024
    Configuration menu
    Copy the full SHA
    3a2b13f View commit details
    Browse the repository at this point in the history

Commits on Jul 12, 2024

  1. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    c5edee4 View commit details
    Browse the repository at this point in the history

  2. Only emit proxy branch-eliminating rewrite trace when asked for

    @geo2a
    geo2a committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    6d730a5 View commit details
    Browse the repository at this point in the history

  3. Update output of test-3934-smt: slight change in rule predicate

    @geo2a
    geo2a committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    4e1524e View commit details
    Browse the repository at this point in the history

  4. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    4d12b6a View commit details
    Browse the repository at this point in the history

  5. Do not ignore rule predicates in unit-tests, only rule subst

    @geo2a
    geo2a committed Jul 12, 2024
    Configuration menu
    Copy the full SHA
    18ca384 View commit details
    Browse the repository at this point in the history

Commits on Jul 15, 2024

  1. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 15, 2024
    Configuration menu
    Copy the full SHA
    6ef5cd3 View commit details
    Browse the repository at this point in the history

Commits on Jul 16, 2024

  1. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 16, 2024
    Configuration menu
    Copy the full SHA
    8d1c69e View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2024

  1. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    c072d46 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2024

  1. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    979606a View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2024

  1. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    9c82e4e View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2024

  1. Make default fallback reasons more explicit, fix comment

    @geo2a
    geo2a committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    8c943d3 View commit details
    Browse the repository at this point in the history

  2. Refactor result printing messages

    @geo2a
    geo2a committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    13b4b9e View commit details
    Browse the repository at this point in the history

  3. Add a new handler for Booster Branching in Proxy.hs

    @geo2a
    geo2a committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    3b179b2 View commit details
    Browse the repository at this point in the history

Commits on Jul 26, 2024

  1. Update kore-rpc-client to use tar-0.6.3 (#3996) 

    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.
    @geo2a
    geo2a committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    cbfa774 View commit details
    Browse the repository at this point in the history

  2. Fixes to simplification diff, request statistics, process-logs (#3992) 

    * 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)
    @jberthold @geo2a
    jberthold authored and geo2a committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    01c344c View commit details
    Browse the repository at this point in the history

  3. TEMP comment-out Kore fallback

    @geo2a
    geo2a committed Jul 26, 2024
    Configuration menu
    Copy the full SHA
    b7590bc View commit details
    Browse the repository at this point in the history

Commits on Jul 29, 2024

  1. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    f52088d View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Jul 29, 2024
    Configuration menu
    Copy the full SHA
    7bf75ea View commit details
    Browse the repository at this point in the history

Commits on Jul 30, 2024

  1. Allow matching functions when rewriting

    @geo2a
    geo2a committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    7bdf0a7 View commit details
    Browse the repository at this point in the history

  2. Allow matching empty sets

    @geo2a
    geo2a committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    bf05ef2 View commit details
    Browse the repository at this point in the history

  3. Add dummy unit test for set matching

    @geo2a
    geo2a committed Jul 30, 2024
    Configuration menu
    Copy the full SHA
    70817d4 View commit details
    Browse the repository at this point in the history

Commits on Aug 6, 2024

  1. Merge remote-tracking branch 'origin/master' into georgy/booster-rema… 

    …inders
    @geo2a
    geo2a committed Aug 6, 2024
    Configuration menu
    Copy the full SHA
    a580cfc View commit details
    Browse the repository at this point in the history

  2. Make unit-tests typecheck

    @geo2a
    geo2a committed Aug 6, 2024
    Configuration menu
    Copy the full SHA
    4f955f2 View commit details
    Browse the repository at this point in the history

Commits on Aug 7, 2024

  1. Revert "Allow matching functions when rewriting" 

    This reverts commit 7bdf0a7.
    @geo2a
    geo2a committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    342ddd9 View commit details
    Browse the repository at this point in the history

  2. Eliminate redundant pattern matches

    @geo2a
    geo2a committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    3d56118 View commit details
    Browse the repository at this point in the history

  3. hlint

    @geo2a
    geo2a committed Aug 7, 2024
    Configuration menu
    Copy the full SHA
    188075d View commit details
    Browse the repository at this point in the history

Commits on Sep 23, 2024

  1. Factor-out checkRequires

    @geo2a
    geo2a committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    1c48bc3 View commit details
    Browse the repository at this point in the history

  2. Factor-out checkEnsures

    @geo2a
    geo2a committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    1ad0dd0 View commit details
    Browse the repository at this point in the history

  3. Refactor applyEquation

    @geo2a
    geo2a committed Sep 23, 2024
    Configuration menu
    Copy the full SHA
    e675f3c View commit details
    Browse the repository at this point in the history