Improvements/refactors to substitution extraction routine #4631
Conversation
This file contains 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
tothtamas28
approved these changes
Sep 6, 2024
ehildenb
added a commit
that referenced
this pull request
Sep 6, 2024
ehildenb
added a commit
that referenced
this pull request
Sep 6, 2024
rv-jenkins
pushed a commit
that referenced
this pull request
Sep 6, 2024
In the KCFG printer, we have two separate places where `CSubst` are printed out, for `Split` and for `Cover`. There was lots of very-similar code between the two of them, and also some incorrect logic abotu minimization. This PR: - Factors out helpers that make this printing logic easier. - Makes sure that we take into account minimization properly. - Standardizes how the printing for `CSubst` works. - Updates expected test output. - Includes some formatting/style reviews from #4631 that were skipped because of automerger.
rv-jenkins
pushed a commit
that referenced
this pull request
Sep 9, 2024
~Blocked on: #4631 ~Blocked on: #4630 ~Blocked on: #4633 While reviewing and going over #4621 with @Stevengre , it became somewhat clear that how we handle turning substitions into ML predicates is a bit dirty. This attempts to clean this up a bit. Where potentially breaking changes to API are introduced here, I've checked if it affects the following repos when I mention "downstream" below: `evm-semantics kontrol wasm-semantics riscv-semantics mir-semantics`. In particular: - The function `CTerm.anti_unify` has a simplification where it reuses a function from `kast.manip` instead of reimplementing it. - The functions `CSubst.from_pred` and `CSubst.pred` are added, as replacements for `Subst.ml_pred`. This is because `Subst.ml_pred` doesn't have a good way to produce correctly sorted predicates, because it's in module `kast.inner`. - `Subst.ml_pred` is removed, and tests are updated to use the new `CSubst` variant. None of the downstream repositories use `Subst.ml_pred` directly. - The new `CSubst.pred` correctly sorts the generated `#Equals` clauses, defaulting to `K` sort or if a `KDefinition` is supplied using it to do sort inference. It also provides options for controlling whether we include the substitution or the constraints in the generated predicate. - A test is added for a `CSubst.pred` case which caused a bug in the integration tests dealing with identity substitutions. - The `CTermSymbolic.implies` function is updated to reuse `CSubst.from_pred` instead of reimplementing it. - On the case of duplicate entries, the first is kept and the latter are made as predicates.
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.
Pulled out of: #4625
This PR improves the substitution extraction machinery in
kast.manip, and adds tests. This isn't used anywhere at the moment, but #4625 will start using it heavily.extract_substsis simplified.