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.

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

MergedEdge class for merging node functionality #4603

Merged
merged 9 commits into from
Aug 27, 2024

Conversation

Stevengre
Copy link
Contributor

@Stevengre Stevengre commented Aug 22, 2024

Here is the alternative implementation for this PR.

  • commit 1: introduce the new class MergedEdge
  • commit 2: add to_rule function to MergedEdge for CSE
  • commit 3: add corresponding functions like Edge for MergedEdge
  • commit 4: modify Edge.to_rule related functions for CSE
  • commit 5: modify KCFGShow for MergedEdge
  • commit 6: modify KCFGViewer for MergedEdge

pyk/src/pyk/kcfg/kcfg.py Outdated Show resolved Hide resolved
@Stevengre
Copy link
Contributor Author

Compared to #4600, the impact of this implementation is smaller, but it still has some effects. Specifically, for KCFG.minimize, the lift_edge_edge and lift_split_edge functions won’t work with the MergedEdge, which will prevent obtaining a summary for a function that uses a summary. However, this approach still seems simpler than #4600. I’ll start a separate PR to refactor the existing KCFG.minimize.

@Stevengre Stevengre self-assigned this Aug 22, 2024
Copy link
Contributor

@tothtamas28 tothtamas28 left a comment

Choose a reason for hiding this comment

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

Please add some unit tests for a KCFG containing MergedEdge instances.

pyk/src/pyk/kcfg/kcfg.py Show resolved Hide resolved
pyk/src/pyk/proof/reachability.py Outdated Show resolved Hide resolved
pyk/src/pyk/kcfg/kcfg.py Outdated Show resolved Hide resolved
@Stevengre
Copy link
Contributor Author

Please add some unit tests for a KCFG containing MergedEdge instances.

This commit adds these unit tests, but leaves the unit test for minimization for another PR.

Copy link
Contributor

@tothtamas28 tothtamas28 left a comment

Choose a reason for hiding this comment

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

LGTM. Please test on evm-semantics before merging.

@Stevengre
Copy link
Contributor Author

  • make cov-unit passed for evm-semantics
  • make cov-unit passed for kontrol

@tothtamas28
Copy link
Contributor

  • make cov-unit passed for evm-semantics
  • make cov-unit passed for kontrol

Please also run integration tests for evm-semantics.

@Stevengre
Copy link
Contributor Author

After spending a long time configuring, I still couldn’t get the evm-semantics integration tests to run. So I decided to submit it as a PR and use the existing CI for testing.

@Stevengre
Copy link
Contributor Author

This PR encountered the same error as the previous PR, and it also failed the Nix tests.

Therefore, I believe the introduction of the merged edge doesn’t affect evm-semantics. It might be some other updates in the pyk repository that are impacting evm-semantics, but I’m not entirely sure.

@rv-jenkins rv-jenkins merged commit 98f057e into develop Aug 27, 2024
17 checks passed
@rv-jenkins rv-jenkins deleted the merged-edge-structure branch August 27, 2024 13:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants