Adjust the sort of mlEquals
#4633
Merged
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
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.
Currently
mlEqualshasGeneratedTopCellas the default argument sort, which is pretty specific/limited. Instead, we setKas the default argument sort (supersort of all sorts), and then go to all the sites that use it and specify the argument sort more carefully.This doesn't affect any downstream repos, none of them use
mlEqualsdirectly.