Skip to content

Commit

Permalink
Make branch extraction more intelligent (runtimeverification/pyk#652)
Browse files Browse the repository at this point in the history
Closes #632.

Before introducing a branch, simplify each of the would-be new nodes and
see if they simplify to bottom
If there are more than 1 non-bottom node, add all these simplified nodes
to the CFG, creating a split/branch. If not, simply continue
straight-line execution.

This should reduce eliminate some infeasible branching by simplifying
earlier in the process.

Also should eliminate repeated branching encountered in
runtimeverification/evm-semantics#2065 when
creating new proofs from branches.

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
  • Loading branch information
3 people authored and Baltoli committed Apr 10, 2024
1 parent 38410ab commit 7753cac
Show file tree
Hide file tree
Showing 3 changed files with 15 additions and 10 deletions.
2 changes: 1 addition & 1 deletion pyk/package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.443
0.1.444
2 changes: 1 addition & 1 deletion pyk/pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "pyk"
version = "0.1.443"
version = "0.1.444"
description = ""
authors = [
"Runtime Verification, Inc. <[email protected]>",
Expand Down
21 changes: 13 additions & 8 deletions pyk/src/pyk/kcfg/explore.py
Original file line number Diff line number Diff line change
Expand Up @@ -377,14 +377,19 @@ def extend(
if self._check_abstract(node, kcfg):
return

if not kcfg.splits(target_id=node.id):
branches = self.kcfg_semantics.extract_branches(node.cterm)
if branches:
kcfg.split_on_constraints(node.id, branches)
_LOGGER.info(
f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}'
)
return
_branches = self.kcfg_semantics.extract_branches(node.cterm)
branches = []
for constraint in _branches:
kast = mlAnd(list(node.cterm.constraints) + [constraint])
kast, _ = self.kast_simplify(kast)
if not CTerm._is_bottom(kast):
branches.append(constraint)
if len(branches) > 1:
kcfg.split_on_constraints(node.id, branches)
_LOGGER.info(
f'Found {len(branches)} branches using heuristic for node {node.id}: {shorten_hashes(node.id)}: {[self.kprint.pretty_print(bc) for bc in branches]}'
)
return

_LOGGER.info(f'Extending KCFG from node {self.id}: {shorten_hashes(node.id)}')
_is_vacuous, depth, cterm, next_cterms, next_node_logs = self.cterm_execute(
Expand Down

0 comments on commit 7753cac

Please sign in to comment.