Skip to content

Commit

Permalink
Refactoring to KCFG printer for CSubst (#4630)
Browse files Browse the repository at this point in the history 
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.
  • Loading branch information
@ehildenb
ehildenb authored Sep 6, 2024
1 parent 859b1ce commit 82f8de0
Show file tree
Hide file tree
Showing 7 changed files with 145 additions and 101 deletions.
22 changes: 16 additions & 6 deletions pyk/regression-new/kprove-haskell/sum-spec.k.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,7 +31,9 @@ Subproofs: 0
│ #And { true #Equals N:Int >=Int 0 }
┃
┃ (branch)
┣━━┓ constraint: N:Int >Int 0
┣━━┓ subst: .Subst
┃ ┃ constraint:
┃ ┃ N:Int >Int 0
┃ │
┃ ├─ 3
┃ │ <generatedTop>
Expand Down Expand Up @@ -92,8 +94,11 @@ Subproofs: 0
┃ │ #And { true #Equals N:Int >=Int 0 }
┃ │ #And { true #Equals N:Int +Int -1 >=Int 0 }
┃ │
┃ ┊ constraint: OMITTED CONSTRAINT
┃ ┊ subst: OMITTED SUBST
┃ ┊ constraint:
┃ ┊ S:Int +Int C:Int +Int N:Int +Int -1 *Int C:Int +Int 1 +Int N:Int +Int -2 *Int N:Int +Int -1 /Int 2 ==K S:Int +Int N:Int *Int C:Int +Int N:Int +Int -1 *Int N:Int /Int 2
┃ ┊ subst:
┃ ┊ ?_COUNTER_CELL_af8c44a5 <- COUNTER_CELL_af8c44a5:Int
┃ ┊ ?_GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_5e3e01ba:Int
┃ └─ 2 (leaf, target)
┃ <generatedTop>
┃ <k>
Expand All @@ -112,7 +117,9 @@ Subproofs: 0
┃ #And { true #Equals N:Int >=Int 0 }
┃ #And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 }
┃
┗━━┓ constraint: N:Int ==Int 0
┗━━┓ subst: .Subst
┃ constraint:
┃ N:Int ==Int 0
│
├─ 4
│ <generatedTop>
Expand Down Expand Up @@ -151,8 +158,11 @@ Subproofs: 0
│ </generatedTop>
│ #And { N:Int #Equals 0 }
│
┊ constraint: OMITTED CONSTRAINT
┊ subst: OMITTED SUBST
┊ constraint:
┊ S:Int ==Int S:Int +Int N:Int *Int COUNTER_CELL_af8c44a5:Int +Int N:Int +Int -1 *Int N:Int /Int 2
┊ subst:
┊ C <- COUNTER_CELL_af8c44a5:Int
┊ GENERATEDCOUNTER_CELL_5e3e01ba <- GENERATEDCOUNTER_CELL_949ec677:Int
└─ 2 (leaf, target)
<generatedTop>
<k>
Expand Down
3 changes: 2 additions & 1 deletion pyk/regression-new/kprove-haskell/test-spec.k.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,8 @@ Subproofs: 0
│ </generatedTop>
│
┊ constraint: true
┊ subst: GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int
┊ subst:
┊ GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int
└─ 2 (leaf, target)
<generatedTop>
<k>
Expand Down
2 changes: 1 addition & 1 deletion pyk/src/pyk/__main__.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -282,7 +282,7 @@ def explore_context() -> Iterator[KCFGExplore]:
if options.show_kcfg and type(proof) is APRProof:
node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False)
show = APRProofShow(kprove, node_printer=node_printer)
print('\n'.join(show.show(proof)))
print('\n'.join(show.show(proof, minimize=False)))
sys.exit(len([p.id for p in proofs if not p.passed]))


Expand Down
34 changes: 17 additions & 17 deletions pyk/src/pyk/kast/manip.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -215,39 +215,39 @@ def extract_rhs(term: KInner) -> KInner:


def extract_subst(term: KInner) -> tuple[Subst, KInner]:
_subst = {}
subst = {}
rem_conjuncts: list[KInner] = []

def _extract_subst(_term1: KInner, _term2: KInner) -> tuple[str, KInner] | None:
def _extract_subst(term: KInner, term2: KInner) -> tuple[str, KInner] | None:
if (
(type(_term1) is KVariable and _term1.name not in _subst)
and not (type(_term2) is KVariable and _term2.name in _subst)
and _term1.name not in free_vars(_term2)
(isinstance(term, KVariable) and term.name not in subst)
and not (isinstance(term2, KVariable) and term2.name in subst)
and term.name not in free_vars(term2)
):
return (_term1.name, _term2)
return (term.name, term2)
if (
(type(_term2) is KVariable and _term2.name not in _subst)
and not (type(_term1) is KVariable and _term1.name in _subst)
and _term2.name not in free_vars(_term1)
(isinstance(term2, KVariable) and term2.name not in subst)
and not (isinstance(term, KVariable) and term.name in subst)
and term2.name not in free_vars(term)
):
return (_term2.name, _term1)
if _term1 == TRUE and type(_term2) is KApply and _term2.label.name in {'_==K_', '_==Int_'}:
return _extract_subst(_term2.args[0], _term2.args[1])
if _term2 == TRUE and type(_term1) is KApply and _term1.label.name in {'_==K_', '_==Int_'}:
return _extract_subst(_term1.args[0], _term1.args[1])
return (term2.name, term)
if term == TRUE and isinstance(term2, KApply) and term2.label.name in {'_==K_', '_==Int_'}:
return _extract_subst(term2.args[0], term2.args[1])
if term2 == TRUE and isinstance(term, KApply) and term.label.name in {'_==K_', '_==Int_'}:
return _extract_subst(term.args[0], term.args[1])
return None

for conjunct in flatten_label('#And', term):
if type(conjunct) is KApply and conjunct.label.name == '#Equals':
if isinstance(conjunct, KApply) and conjunct.label.name == '#Equals':
if _conjunct_subst := _extract_subst(conjunct.args[0], conjunct.args[1]):
name, value = _conjunct_subst
_subst[name] = value
subst[name] = value
else:
rem_conjuncts.append(conjunct)
else:
rem_conjuncts.append(conjunct)

return Subst(_subst), mlAnd(rem_conjuncts)
return Subst(subst), mlAnd(rem_conjuncts)


def count_vars(term: KInner) -> Counter[str]:
Expand Down
71 changes: 33 additions & 38 deletions pyk/src/pyk/kcfg/show.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,7 @@
from pathlib import Path
from typing import Final

from ..cterm import CSubst
from ..kast import KInner
from ..kast.outer import KFlatModule, KSentence
from ..ktool.kprint import KPrint
Expand Down Expand Up @@ -126,6 +127,34 @@ def pretty_segments(self, kcfg: KCFG, minimize: bool = True) -> Iterable[tuple[s
processed_nodes: list[KCFG.Node] = []
ret_lines: list[tuple[str, list[str]]] = []

def _multi_line_print(
label: str, lines: list[str], default: str = 'None', indent: int = 4, max_width: int | None = None
) -> list[str]:
ret_lines = []
if len(lines) == 0:
ret_lines.append(f'{label}: {default}')
else:
ret_lines.append(f'{label}:')
ret_lines.extend([f'{indent * " "}{line}' for line in lines])
if max_width is not None:
ret_lines = [
ret_line if len(ret_line) <= max_width else ret_line[0:max_width] + '...' for ret_line in ret_lines
]
return ret_lines

def _print_csubst(
csubst: CSubst, subst_first: bool = False, indent: int = 4, max_width: int | None = None
) -> list[str]:
_constraint_strs = [
self.kprint.pretty_print(ml_pred_to_bool(constraint, unsafe=True)) for constraint in csubst.constraints
]
constraint_strs = _multi_line_print('constraint', _constraint_strs, 'true', max_width=max_width)
_subst_strs = [f'{k} <- {self.kprint.pretty_print(v)}' for k, v in csubst.subst.minimize().items()]
subst_strs = _multi_line_print('subst', _subst_strs, '.Subst', max_width=max_width)
if subst_first:
return subst_strs + constraint_strs
return constraint_strs + subst_strs

def _print_node(node: KCFG.Node) -> list[str]:
return self.node_short_info(kcfg, node)

Expand All @@ -143,46 +172,12 @@ def _print_merged_edge(merged_edge: KCFG.MergedEdge) -> list[str]:
return [res] if len(res) < 78 else ['(merged edge)']

def _print_cover(cover: KCFG.Cover) -> Iterable[str]:
subst_strs = [f'{k} <- {self.kprint.pretty_print(v)}' for k, v in cover.csubst.subst.items()]
subst_str = ''
if len(subst_strs) == 0:
subst_str = '.Subst'
if len(subst_strs) == 1:
subst_str = subst_strs[0]
if len(subst_strs) > 1 and minimize:
subst_str = 'OMITTED SUBST'
if len(subst_strs) > 1 and not minimize:
subst_str = '{\n ' + '\n '.join(subst_strs) + '\n}'
constraint_str = self.kprint.pretty_print(ml_pred_to_bool(cover.csubst.constraint, unsafe=True))
if len(constraint_str) > 78:
constraint_str = 'OMITTED CONSTRAINT'
return [
f'constraint: {constraint_str}',
f'subst: {subst_str}',
]
max_width = None if not minimize else 78
return _print_csubst(cover.csubst, subst_first=False, indent=4, max_width=max_width)

def _print_split_edge(split: KCFG.Split, target_id: int) -> list[str]:
csubst = split.splits[target_id]
ret_split_lines: list[str] = []
substs = csubst.subst.minimize().items()
constraints = [ml_pred_to_bool(c, unsafe=True) for c in csubst.constraints]
if len(constraints) == 1:
first_line, *rest_lines = self.kprint.pretty_print(constraints[0]).split('\n')
ret_split_lines.append(f'constraint: {first_line}')
ret_split_lines.extend(f' {line}' for line in rest_lines)
elif len(constraints) > 1:
ret_split_lines.append('constraints:')
for constraint in constraints:
first_line, *rest_lines = self.kprint.pretty_print(constraint).split('\n')
ret_split_lines.append(f' {first_line}')
ret_split_lines.extend(f' {line}' for line in rest_lines)
if len(substs) == 1:
vname, term = list(substs)[0]
ret_split_lines.append(f'subst: {vname} <- {self.kprint.pretty_print(term)}')
elif len(substs) > 1:
ret_split_lines.append('substs:')
ret_split_lines.extend(f' {vname} <- {self.kprint.pretty_print(term)}' for vname, term in substs)
return ret_split_lines
max_width = None if not minimize else 78
return _print_csubst(split.splits[target_id], subst_first=True, indent=4, max_width=max_width)

def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: list[KCFG.Node]) -> None:
processed = curr_node in processed_nodes
Expand Down
24 changes: 16 additions & 8 deletions pyk/src/tests/unit/kcfg/test_minimize.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -340,56 +340,64 @@ def x_lt(n: int) -> KApply:
'┌─ 1 (root, split)\n'
'┃\n'
'┃ (branch)\n'
'┣━━┓ constraints:\n'
'┣━━┓ subst: .Subst\n'
'┃ ┃ constraint:\n'
'┃ ┃ _>=Int_ ( X , 0 )\n'
'┃ ┃ _>=Int_ ( X , 32 )\n'
'┃ ┃ _>=Int_ ( X , 64 )\n'
'┃ │\n'
'┃ └─ 8 (leaf)\n'
'┃\n'
'┣━━┓ constraints:\n'
'┣━━┓ subst: .Subst\n'
'┃ ┃ constraint:\n'
'┃ ┃ _>=Int_ ( X , 0 )\n'
'┃ ┃ _>=Int_ ( X , 32 )\n'
'┃ ┃ _<Int_ ( X , 64 )\n'
'┃ │\n'
'┃ └─ 9 (leaf)\n'
'┃\n'
'┣━━┓ constraints:\n'
'┣━━┓ subst: .Subst\n'
'┃ ┃ constraint:\n'
'┃ ┃ _>=Int_ ( X , 0 )\n'
'┃ ┃ _<Int_ ( X , 32 )\n'
'┃ ┃ _>=Int_ ( X , 16 )\n'
'┃ │\n'
'┃ └─ 10 (leaf)\n'
'┃\n'
'┣━━┓ constraints:\n'
'┣━━┓ subst: .Subst\n'
'┃ ┃ constraint:\n'
'┃ ┃ _>=Int_ ( X , 0 )\n'
'┃ ┃ _<Int_ ( X , 32 )\n'
'┃ ┃ _<Int_ ( X , 16 )\n'
'┃ │\n'
'┃ └─ 11 (leaf)\n'
'┃\n'
'┣━━┓ constraints:\n'
'┣━━┓ subst: .Subst\n'
'┃ ┃ constraint:\n'
'┃ ┃ _<Int_ ( X , 0 )\n'
'┃ ┃ _>=Int_ ( X , -32 )\n'
'┃ ┃ _>=Int_ ( X , -16 )\n'
'┃ │\n'
'┃ └─ 12 (leaf)\n'
'┃\n'
'┣━━┓ constraints:\n'
'┣━━┓ subst: .Subst\n'
'┃ ┃ constraint:\n'
'┃ ┃ _<Int_ ( X , 0 )\n'
'┃ ┃ _>=Int_ ( X , -32 )\n'
'┃ ┃ _<Int_ ( X , -16 )\n'
'┃ │\n'
'┃ └─ 13 (leaf)\n'
'┃\n'
'┣━━┓ constraints:\n'
'┣━━┓ subst: .Subst\n'
'┃ ┃ constraint:\n'
'┃ ┃ _<Int_ ( X , 0 )\n'
'┃ ┃ _<Int_ ( X , -32 )\n'
'┃ ┃ _>=Int_ ( X , -64 )\n'
'┃ │\n'
'┃ └─ 14 (leaf)\n'
'┃\n'
'┗━━┓ constraints:\n'
'┗━━┓ subst: .Subst\n'
' ┃ constraint:\n'
' ┃ _<Int_ ( X , 0 )\n'
' ┃ _<Int_ ( X , -32 )\n'
' ┃ _<Int_ ( X , -64 )\n'
Expand Down
Loading

0 comments on commit 82f8de0

Please sign in to comment.