This repository has been archived by the owner on Apr 25, 2024. It is now read-only.
Refactoring the branching mechanism #1072
Closed
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
PetarMax
commented
Apr 9, 2024
PetarMax
commented
Apr 9, 2024
Comment on lines
+123
to
+129
| next_states = tuple( | ||
| ( | ||
| CTerm.from_kast(self.kore_to_kast(ns.kore)), | ||
| self.kore_to_kast(ns.rule_predicate) if ns.rule_predicate is not None else None, | ||
| ) | ||
| for ns in resp_next_states | ||
| ) |
There was a problem hiding this comment.
Propagating the branching constraints along with the CTerms, perhaps there is a better way of doing this?
There was a problem hiding this comment.
CTermExecute could be abstract with concrete subclasses for branching vs non-branching steps.
PetarMax
commented
Apr 9, 2024
Comment on lines
+225
to
+235
| # _branches = self.kcfg_semantics.extract_branches(_cterm) | ||
| # branches = [] | ||
| # for constraint in _branches: | ||
| # kast = mlAnd(list(_cterm.constraints) + [constraint]) | ||
| # kast, _ = self.cterm_symbolic.kast_simplify(kast) | ||
| # if not CTerm._is_bottom(kast): | ||
| # branches.append(constraint) | ||
| # if len(branches) > 1: | ||
| # constraint_strs = [self.pretty_print(bc) for bc in branches] | ||
| # log(f'{len(branches)} branches using heuristics: {node_id} -> {constraint_strs}') | ||
| # return Branch(branches, heuristic=True) |
There was a problem hiding this comment.
This does not seem to be necessary anymore.
There was a problem hiding this comment.
Let's remove the comments, we can bring that code back at any time from the version history.
PetarMax
commented
Apr 9, 2024
| constraint_strs = [self.pretty_print(bc) for bc in branches] | ||
| log(f'{len(branches)} branches using heuristics: {node_id} -> {constraint_strs}') | ||
| assert len(next_cterms_with_branch_constraints) > 1 | ||
| if all(branch_constraint for _, branch_constraint in next_cterms_with_branch_constraints): |
There was a problem hiding this comment.
This could be too strong, but feels safe at the moment.
|
As a first example, I have that the KCFG of the CSE execution of which is not great, and in which simultaneous applications of multiple specifications of the underlying functions cause non-deterministic branching, to this where there are no non-deterministic branches and all branching conditions are present. |
|
In a recent proof, also, the two branchings below were characterised as non-deterministic, but their constraints are now fully captured: |
tothtamas28
reviewed
Apr 10, 2024
Comment on lines
+123
to
+129
| next_states = tuple( | ||
| ( | ||
| CTerm.from_kast(self.kore_to_kast(ns.kore)), | ||
| self.kore_to_kast(ns.rule_predicate) if ns.rule_predicate is not None else None, | ||
| ) | ||
| for ns in resp_next_states | ||
| ) |
There was a problem hiding this comment.
CTermExecute could be abstract with concrete subclasses for branching vs non-branching steps.
Comment on lines
+225
to
+235
| # _branches = self.kcfg_semantics.extract_branches(_cterm) | ||
| # branches = [] | ||
| # for constraint in _branches: | ||
| # kast = mlAnd(list(_cterm.constraints) + [constraint]) | ||
| # kast, _ = self.cterm_symbolic.kast_simplify(kast) | ||
| # if not CTerm._is_bottom(kast): | ||
| # branches.append(constraint) | ||
| # if len(branches) > 1: | ||
| # constraint_strs = [self.pretty_print(bc) for bc in branches] | ||
| # log(f'{len(branches)} branches using heuristics: {node_id} -> {constraint_strs}') | ||
| # return Branch(branches, heuristic=True) |
There was a problem hiding this comment.
Let's remove the comments, we can bring that code back at any time from the version history.
rv-jenkins
pushed a commit
to runtimeverification/k
that referenced
this pull request
Apr 24, 2024
Transfer of: runtimeverification/pyk#1072 This PR that uses branching information from the backend (for which support was enabled by runtimeverification/pyk#942) to simplify the branching mechanism, potentially making the `extract_branches` obsolete and only creating `NDBranches` in the presence of true non-determinism. I've done a preliminary testing in Kontrol, more info in comments below. --------- Co-authored-by: Petar Maksimovic <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
Sign up for free
to subscribe to this conversation on GitHub.
Already have an account?
Sign in.
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.
This is a very draft PR that uses branching information from the backend (for which support was enabled by #942) to simplify the branching mechanism, potentially making the
extract_branchesobsolete and only creatingNDBranchesin the presence of true non-determinism.I've done a preliminary testing in Kontrol, more info in comments below.