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

PyK: Misc enhancements to KCFG and anti-unification #4775

Conversation

nishantjr
Copy link
Collaborator

@nishantjr nishantjr commented Mar 19, 2025

  • KCFG: Shorten log message for easier readability

    This brings the more important parts of the messages into focus.

  • CTerm.anti_unify: Don't call ml_pred_to_bool unless necessary

    Since these values are only used if keep_values is set, we do not need to always
    compute them. In addition, it avoids exceptions when the predicate cannot be
    converted to a bool expression: e.g. when using #Ceil as a side condition

    This is only a work-around (it would
    still break for a #Ceil side condition, if keep_values=True), but lets us move forward without risking
    breaking other projects that rely on the original behaviour.

  • pyk:KCFGShow.to_module: Thread imports and defunc_with parameters through to KCFG.to_module

    This lets us use those options for printing the modules.

@nishantjr nishantjr force-pushed the misc-pyk-fixes branch 2 times, most recently from c0044cf to 5d98e4a Compare March 19, 2025 04:49
@nishantjr nishantjr changed the base branch from master to develop March 19, 2025 04:51
@nishantjr nishantjr requested a review from ehildenb March 19, 2025 16:37
@ehildenb
Copy link
Member

@nishantjr it looks ilke you updated the Haskell and LLVM submodules both in your PR, is that intentional? In general, you shouldn't do that, because it missed updating all of the things like nix flake, pyproject.toml, and dependency list files. Can you back those changes out?

@nishantjr
Copy link
Collaborator Author

@nishantjr it looks ilke you updated the Haskell and LLVM submodules both in your PR, is that intentional? In general, you shouldn't do that, because it missed updating all of the things like nix flake, pyproject.toml, and dependency list files. Can you back those changes out?

Ugh, accidentally committed after a rebase. Fixed.

@nishantjr nishantjr marked this pull request as ready for review March 20, 2025 03:56
@nishantjr
Copy link
Collaborator Author

@ehildenb I've pushed another change that exposes KCFG.to_module's imports parameter in KCFGShow.

We remove all text that is obvious
Since these values are only used if keep_values is set, we do not need to always
compute them. In addition, it avoids exceptions when the predicated cannot be
converted to a bool expression: e.g. when using #Ceil

I'm not sure why the terms need to be converted into Bool expressions (vs ML
predicates) in the first place. Thus, while this is only a work-around (it would
still break if keep_values=True), it lets us move forward without risking
breaking other projects that rely on the original behaviour.
@ehildenb
Copy link
Member

@nishantjr , looking at the CI failures, I think this test is the most telling one: TestKonvertCellMap.test_kast_to_kore[account-cell-map]. I guess this comes from the change in how you're handling cell-maps, maybe that change isn't needed? If it is needed, please add a test demonstrating why it's needed, so we can make sure that one is passing and current ones are passing.

@nishantjr nishantjr marked this pull request as draft March 20, 2025 14:27
@ehildenb
Copy link
Member

I re-triggered teh CI run, it was due to the haskell server becoming unavailable for some reason. Maybe changing the way that modules are built is causing some issues? But I figured it's worth re-triggering the run.

Can you update the PR description so we get a good commit message?

@nishantjr nishantjr changed the title Miscelanous pyk fixes PyK: Misc enhancements to KCFG and anti-unification Mar 20, 2025
@nishantjr
Copy link
Collaborator Author

Thanks Everett. How does it look now? I've backed out one of the commits; will add in the test for it next week.

@nishantjr nishantjr marked this pull request as ready for review March 20, 2025 15:15
Co-authored-by: Nishant Rodrigues <[email protected]>
@automergerpr-permission-manager automergerpr-permission-manager bot merged commit 45c0b09 into runtimeverification:develop Mar 20, 2025
18 checks passed
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.

2 participants