Reusing backend information to construct KCFGs more efficiently #4590
Conversation
PetarMax
force-pushed
the
petar/streamlining-branching
branch
from
687ccda to
079be45
Compare
|
I need some help with this PR, @ehildenb, @tothtamas28, @nwatson22, if you can. I've left comments throughout, please advise. |
PetarMax
changed the title
PetarMax
requested review from
tothtamas28,
nwatson22 and
ehildenb
and removed request for
tothtamas28
|
I will now run some engagement proofs using this and check for speedups. |
pyk/src/pyk/kcfg/kcfg.py
Outdated
| @@ -1306,7 +1321,8 @@ def read_node_data(cfg_dir: Path, node_id: int) -> KCFG.Node: | |||
| return KCFG.Node.from_dict(store.read_node_data(node_id)) | |||
|
|
|||
|
|
|||
| class KCFGExtendResult(ABC): ... | |||
| class KCFGExtendResult(ABC): | |||
| info: str = field(default='') | |||
There was a problem hiding this comment.
Consider
| info: str = field(default='') | |
| info: str |
and adding the info: str = field(default='') to each dataclass subclass.
Alternatively, do not make it an abstract attribute, since the value is not used for most subclasses.
There was a problem hiding this comment.
Would it be ok to just have it in the ones where it's needed? The compilation does not seem to complain.
There was a problem hiding this comment.
Yes, but then it shouldn't be present in the abstract class.
There was a problem hiding this comment.
Yes, I removed it from there.
pyk/src/pyk/proof/reachability.py
Outdated
| extend_result: KCFGExtendResult | ||
| """Holds the description of how an APRProof should be extended. | ||
|
|
||
| Fields: |
There was a problem hiding this comment.
| Fields: | |
| Attributes: |
pyk/src/pyk/proof/reachability.py
Outdated
| to_cache: Holds an indicator of whether or not the provided extension | ||
| should be cached instead of being applied. |
There was a problem hiding this comment.
What does it mean for an extension to be cached?
There was a problem hiding this comment.
extend_cterm can now return two extensions, the first of which is a Step, and the second of which is a cut-rule, branch, or NDBranch. When that happens, the first one is to be applied, and the second one is to be cached so that it can be automatically applied instead of recomputed when we explore from the node created by that first Step.
pyk/src/pyk/proof/reachability.py
Outdated
| assert len(result.extend_results) == 0 | ||
| assert result.use_cache in self._next_steps |
There was a problem hiding this comment.
To me, all these assertions indicate that APRProofExtendResult could be broken up into multiple subclasses with stronger typing guarantees.
There was a problem hiding this comment.
100%. I will think about this a bit.
There was a problem hiding this comment.
I've redesigned them now.
pyk/src/pyk/kcfg/semantics.py
Outdated
| @@ -12,15 +12,28 @@ class KCFGSemantics(ABC): | |||
| @abstractmethod | |||
| def is_terminal(self, c: CTerm) -> bool: ... | |||
|
|
|||
| """Checks whether or not a given CTerm is terminal.""" | |||
There was a problem hiding this comment.
| """Checks whether or not a given CTerm is terminal.""" | |
| """Check whether or not a given ``CTerm`` is terminal.""" |
| node_id=step.node.id, | ||
| ) | ||
| # If the step has already been cached, do not invoke the backend and only send a signal back to the proof to use the cache | ||
| if step.use_cache is not None: |
There was a problem hiding this comment.
What happens if the prover is terminated with cached results not yet applied? Is it still possible to continue extending the KCFG?
There was a problem hiding this comment.
Yes, it is, and cached results should be re-used if the proof has survived. If they are lost, there is no loss for the KCFG, since they are only a snapshot of guaranteed future extension results.
|
Yes, it has been extensively tested with Kontrol and engagement tests. |
Co-authored-by: Tamás Tóth <[email protected]>
Corrections
This PR leverages information provided by the backend as part of an
executerequest to construct more than one KCFG element: specifically, vacuous nodes, stuck nodes, edges resulting from cut-nodes, branches, and non-deterministic branches.In addition, it moves the associated printing to the KCFG class, allowing for more informative prints: for example, we can now print the target nodes of edges and branches, the absence of which (personally) was making debugging of large proofs slightly more difficult.
The PR also removes the
always_check_subsumptionflag, which was not used and was made obsolete by the subsumption logic instep_proof.