Skip to content
This repository was archived by the owner on Apr 25, 2024. It is now read-only.

Commit fde07ec

Browse files
nwatson22rv-auditor
nwatson22
and
rv-auditor
authored
Make anti-unification more sort-aware (#598)
- Changed `anti_unify` and `anti_unify_with_constraints` to require a `KDefinition` which they use to grab the tightest sort for the terms they are abstracting - Since these actions are now associated with a specific K definition, moved them into `KDefinition` as methods. - Adds `KDefinition.least_common_supersort` which returns the most specific sort that will cover two terms (as long as one sort is a subsort of the other). - Uses this function in `KDefinition.sort` to determine the sort of a `KRewrite`. - Rewrote the tests for `anti_unify` and `anti_unify_with_constraints` to use `KDefinition` and test that the abstracted variables are now more tightly typed based on the original terms. This is an attempt to fix an issue in runtimeverification/evm-semantics#1934 where the looser sort bound is preventing simplification after the merging (anti-unification) of two nodes. --------- Co-authored-by: devops <[email protected]>
1 parent 3dbb978 commit fde07ec

File tree

8 files changed

+307
-158
lines changed

8 files changed

+307
-158
lines changed

‎package/version‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
0.1.415
1+
0.1.416

‎pyproject.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
44

55
[tool.poetry]
66
name = "pyk"
7-
version = "0.1.415"
7+
version = "0.1.416"
88
description = ""
99
authors = [
1010
"Runtime Verification, Inc. <[email protected]>",

‎src/pyk/cterm.py‎

Lines changed: 60 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,10 @@
55
from itertools import chain
66
from typing import TYPE_CHECKING
77

8-
from .kast.inner import KApply, KInner, KRewrite, KVariable, Subst
8+
from .kast.inner import KApply, KInner, KRewrite, KToken, KVariable, Subst, bottom_up
99
from .kast.kast import KAtt
1010
from .kast.manip import (
11+
abstract_term_safely,
1112
apply_existential_substitutions,
1213
count_vars,
1314
flatten_label,
@@ -22,13 +23,16 @@
2223
)
2324
from .kast.outer import KClaim, KRule
2425
from .prelude.k import GENERATED_TOP_CELL
25-
from .prelude.ml import is_top, mlAnd, mlImplies, mlTop
26+
from .prelude.kbool import orBool
27+
from .prelude.ml import is_top, mlAnd, mlEqualsTrue, mlImplies, mlTop
2628
from .utils import unique
2729

2830
if TYPE_CHECKING:
2931
from collections.abc import Iterable, Iterator
3032
from typing import Any
3133

34+
from .kast.outer import KDefinition
35+
3236

3337
@dataclass(frozen=True, order=True)
3438
class CTerm:
@@ -56,7 +60,7 @@ def from_dict(dct: dict[str, Any]) -> CTerm:
5660
@staticmethod
5761
def _check_config(config: KInner) -> None:
5862
if not isinstance(config, KApply) or not config.is_cell:
59-
raise ValueError('Expected cell label, found: {config.label.name}')
63+
raise ValueError(f'Expected cell label, found: {config}')
6064

6165
@staticmethod
6266
def _normalize_constraints(constraints: Iterable[KInner]) -> tuple[KInner, ...]:
@@ -138,6 +142,59 @@ def _ml_impl(antecedents: Iterable[KInner], consequents: Iterable[KInner]) -> KI
138142
def add_constraint(self, new_constraint: KInner) -> CTerm:
139143
return CTerm(self.config, [new_constraint] + list(self.constraints))
140144

145+
def anti_unify(
146+
self, other: CTerm, keep_values: bool = False, kdef: KDefinition | None = None
147+
) -> tuple[CTerm, CSubst, CSubst]:
148+
def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner:
149+
if KToken('true', 'Bool') in [subst1.pred, subst2.pred]:
150+
return mlTop()
151+
return mlEqualsTrue(orBool([subst1.pred, subst2.pred]))
152+
153+
new_config, self_subst, other_subst = anti_unify(self.config, other.config, kdef=kdef)
154+
common_constraints = [constraint for constraint in self.constraints if constraint in other.constraints]
155+
156+
new_cterm = CTerm(
157+
config=new_config, constraints=([disjunction_from_substs(self_subst, other_subst)] if keep_values else [])
158+
)
159+
160+
new_constraints = []
161+
fvs = free_vars(new_cterm.kast)
162+
len_fvs = 0
163+
while len_fvs < len(fvs):
164+
len_fvs = len(fvs)
165+
for constraint in common_constraints:
166+
if constraint not in new_constraints:
167+
constraint_fvs = free_vars(constraint)
168+
if any(fv in fvs for fv in constraint_fvs):
169+
new_constraints.append(constraint)
170+
fvs.extend(constraint_fvs)
171+
172+
for constraint in new_constraints:
173+
new_cterm = new_cterm.add_constraint(constraint)
174+
self_csubst = new_cterm.match_with_constraint(self)
175+
other_csubst = new_cterm.match_with_constraint(other)
176+
if self_csubst is None or other_csubst is None:
177+
raise ValueError(
178+
f'Anti-unification failed to produce a more general state: {(new_cterm, (self, self_csubst), (other, other_csubst))}'
179+
)
180+
return (new_cterm, self_csubst, other_csubst)
181+
182+
183+
def anti_unify(state1: KInner, state2: KInner, kdef: KDefinition | None = None) -> tuple[KInner, Subst, Subst]:
184+
def _rewrites_to_abstractions(_kast: KInner) -> KInner:
185+
if type(_kast) is KRewrite:
186+
sort = kdef.sort(_kast) if kdef else None
187+
return abstract_term_safely(_kast, sort=sort)
188+
return _kast
189+
190+
minimized_rewrite = push_down_rewrites(KRewrite(state1, state2))
191+
abstracted_state = bottom_up(_rewrites_to_abstractions, minimized_rewrite)
192+
subst1 = abstracted_state.match(state1)
193+
subst2 = abstracted_state.match(state2)
194+
if subst1 is None or subst2 is None:
195+
raise ValueError('Anti-unification failed to produce a more general state!')
196+
return (abstracted_state, subst1, subst2)
197+
141198

142199
@dataclass(frozen=True, order=True)
143200
class CSubst:

‎src/pyk/kast/manip.py‎

Lines changed: 1 addition & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@
66

77
from ..prelude.k import DOTS, GENERATED_TOP_CELL
88
from ..prelude.kbool import FALSE, TRUE, andBool, impliesBool, notBool, orBool
9-
from ..prelude.ml import mlAnd, mlEqualsTrue, mlImplies, mlOr, mlTop
9+
from ..prelude.ml import mlAnd, mlEqualsTrue, mlOr
1010
from ..utils import find_common_items, hash_str
1111
from .inner import KApply, KRewrite, KSequence, KToken, KVariable, Subst, bottom_up, top_down, var_occurrences
1212
from .kast import EMPTY_ATT, KAtt, WithKAtt
@@ -582,58 +582,6 @@ def _abstract(k: KInner) -> KVariable:
582582
return new_var
583583

584584

585-
def anti_unify(state1: KInner, state2: KInner) -> tuple[KInner, Subst, Subst]:
586-
def _rewrites_to_abstractions(_kast: KInner) -> KInner:
587-
if type(_kast) is KRewrite:
588-
return abstract_term_safely(_kast)
589-
return _kast
590-
591-
minimized_rewrite = push_down_rewrites(KRewrite(state1, state2))
592-
abstracted_state = bottom_up(_rewrites_to_abstractions, minimized_rewrite)
593-
subst1 = abstracted_state.match(state1)
594-
subst2 = abstracted_state.match(state2)
595-
if subst1 is None or subst2 is None:
596-
raise ValueError('Anti-unification failed to produce a more general state!')
597-
return (abstracted_state, subst1, subst2)
598-
599-
600-
def anti_unify_with_constraints(
601-
constrained_term_1: KInner,
602-
constrained_term_2: KInner,
603-
implications: bool = False,
604-
constraint_disjunct: bool = False,
605-
abstracted_disjunct: bool = False,
606-
) -> KInner:
607-
def disjunction_from_substs(subst1: Subst, subst2: Subst) -> KInner:
608-
if KToken('true', 'Bool') in [subst1.pred, subst2.pred]:
609-
return mlTop()
610-
return mlEqualsTrue(orBool([subst1.pred, subst2.pred]))
611-
612-
state1, constraint1 = split_config_and_constraints(constrained_term_1)
613-
state2, constraint2 = split_config_and_constraints(constrained_term_2)
614-
constraints1 = flatten_label('#And', constraint1)
615-
constraints2 = flatten_label('#And', constraint2)
616-
state, subst1, subst2 = anti_unify(state1, state2)
617-
618-
constraints = [c for c in constraints1 if c in constraints2]
619-
constraint1 = mlAnd([c for c in constraints1 if c not in constraints])
620-
constraint2 = mlAnd([c for c in constraints2 if c not in constraints])
621-
implication1 = mlImplies(constraint1, subst1.ml_pred)
622-
implication2 = mlImplies(constraint2, subst2.ml_pred)
623-
624-
if abstracted_disjunct:
625-
constraints.append(disjunction_from_substs(subst1, subst2))
626-
627-
if implications:
628-
constraints.append(implication1)
629-
constraints.append(implication2)
630-
631-
if constraint_disjunct:
632-
constraints.append(mlOr([constraint1, constraint2]))
633-
634-
return mlAnd([state] + constraints)
635-
636-
637585
def apply_existential_substitutions(constrained_term: KInner) -> KInner:
638586
state, constraint = split_config_and_constraints(constrained_term)
639587
constraints = flatten_label('#And', constraint)

‎src/pyk/kast/outer.py‎

Lines changed: 18 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1101,8 +1101,11 @@ def sort(self, kast: KInner) -> KSort | None:
11011101
case KToken(_, sort) | KVariable(_, sort):
11021102
return sort
11031103
case KRewrite(lhs, rhs):
1104-
sort = self.sort(lhs)
1105-
return sort if sort == self.sort(rhs) else None
1104+
lhs_sort = self.sort(lhs)
1105+
rhs_sort = self.sort(rhs)
1106+
if lhs_sort and rhs_sort:
1107+
return self.least_common_supersort(lhs_sort, rhs_sort)
1108+
return None
11061109
case KSequence(_):
11071110
return KSort('K')
11081111
case KApply(label, _):
@@ -1128,13 +1131,26 @@ def sort_strict(self, kast: KInner) -> KSort:
11281131
raise ValueError(f'Could not determine sort of term: {kast}')
11291132
return sort
11301133

1134+
def least_common_supersort(self, sort1: KSort, sort2: KSort) -> KSort | None:
1135+
if sort1 == sort2:
1136+
return sort1
1137+
if sort1 in self.subsorts(sort2):
1138+
return sort2
1139+
if sort2 in self.subsorts(sort1):
1140+
return sort1
1141+
# Computing least common supersort is not currently supported if sort1 is not a subsort of sort2 or
1142+
# vice versa. In that case there may be more than one LCS.
1143+
return None
1144+
11311145
def greatest_common_subsort(self, sort1: KSort, sort2: KSort) -> KSort | None:
11321146
if sort1 == sort2:
11331147
return sort1
11341148
if sort1 in self.subsorts(sort2):
11351149
return sort1
11361150
if sort2 in self.subsorts(sort1):
11371151
return sort2
1152+
# Computing greatest common subsort is not currently supported if sort1 is not a subsort of sort2 or
1153+
# vice versa. In that case there may be more than one GCS.
11381154
return None
11391155

11401156
# Sorts like Int cannot be injected directly into sort K so they are embedded in a KSequence.

‎src/tests/integration/kcfg/test_imp.py‎

Lines changed: 136 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,10 @@
88

99
from pyk.cterm import CSubst, CTerm
1010
from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
11-
from pyk.kast.manip import minimize_term
11+
from pyk.kast.manip import get_cell, minimize_term
1212
from pyk.kcfg.semantics import KCFGSemantics
1313
from pyk.kcfg.show import KCFGShow
14-
from pyk.prelude.kbool import BOOL, notBool
14+
from pyk.prelude.kbool import BOOL, notBool, orBool
1515
from pyk.prelude.kint import intToken
1616
from pyk.prelude.ml import mlAnd, mlBottom, mlEqualsFalse, mlEqualsTrue, mlTop
1717
from pyk.proof import APRBMCProof, APRBMCProver, APRProof, APRProver, ProofStatus
@@ -1147,3 +1147,137 @@ def test_fail_fast(
11471147
assert len(proof.pending) == 1
11481148
assert len(proof.terminal) == 1
11491149
assert len(proof.failing) == 1
1150+
1151+
def test_anti_unify_forget_values(
1152+
self,
1153+
kcfg_explore: KCFGExplore,
1154+
kprint: KPrint,
1155+
) -> None:
1156+
cterm1 = self.config(
1157+
kprint=kprint,
1158+
k='int $n ; { }',
1159+
state='N |-> X:Int',
1160+
constraint=mlAnd(
1161+
[
1162+
mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])),
1163+
mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1164+
mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
1165+
mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
1166+
]
1167+
),
1168+
)
1169+
cterm2 = self.config(
1170+
kprint=kprint,
1171+
k='int $n ; { }',
1172+
state='N |-> Y:Int',
1173+
constraint=mlAnd(
1174+
[
1175+
mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])),
1176+
mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1177+
mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
1178+
mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
1179+
]
1180+
),
1181+
)
1182+
1183+
anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=False, kdef=kprint.definition)
1184+
1185+
k_cell = get_cell(anti_unifier.kast, 'STATE_CELL')
1186+
assert type(k_cell) is KApply
1187+
assert k_cell.label.name == '_|->_'
1188+
assert type(k_cell.args[1]) is KVariable
1189+
abstracted_var: KVariable = k_cell.args[1]
1190+
1191+
expected_anti_unifier = self.config(
1192+
kprint=kprint,
1193+
k='int $n ; { }',
1194+
state=f'N |-> {abstracted_var.name}:Int',
1195+
constraint=mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1196+
)
1197+
1198+
assert anti_unifier.kast == expected_anti_unifier.kast
1199+
1200+
def test_anti_unify_keep_values(
1201+
self,
1202+
kcfg_explore: KCFGExplore,
1203+
kprint: KPrint,
1204+
) -> None:
1205+
cterm1 = self.config(
1206+
kprint=kprint,
1207+
k='int $n ; { }',
1208+
state='N |-> X:Int',
1209+
constraint=mlAnd(
1210+
[
1211+
mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])),
1212+
mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1213+
mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
1214+
mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
1215+
]
1216+
),
1217+
)
1218+
cterm2 = self.config(
1219+
kprint=kprint,
1220+
k='int $n ; { }',
1221+
state='N |-> Y:Int',
1222+
constraint=mlAnd(
1223+
[
1224+
mlEqualsTrue(KApply('_>Int_', [KVariable('K', 'Int'), KToken('1', 'Int')])),
1225+
mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1226+
mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
1227+
mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
1228+
]
1229+
),
1230+
)
1231+
1232+
anti_unifier, subst1, subst2 = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprint.definition)
1233+
1234+
k_cell = get_cell(anti_unifier.kast, 'STATE_CELL')
1235+
assert type(k_cell) is KApply
1236+
assert k_cell.label.name == '_|->_'
1237+
assert type(k_cell.args[1]) is KVariable
1238+
abstracted_var: KVariable = k_cell.args[1]
1239+
1240+
expected_anti_unifier = self.config(
1241+
kprint=kprint,
1242+
k='int $n ; { }',
1243+
state=f'N |-> {abstracted_var.name}:Int',
1244+
constraint=mlAnd(
1245+
[
1246+
mlEqualsTrue(KApply('_>Int_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1247+
mlEqualsTrue(KApply('_>Int_', [KVariable('X', 'Int'), KToken('1', 'Int')])),
1248+
mlEqualsTrue(KApply('_>Int_', [KVariable('Y', 'Int'), KToken('1', 'Int')])),
1249+
mlEqualsTrue(
1250+
orBool(
1251+
[
1252+
KApply('_==K_', [KVariable(name=abstracted_var.name), KVariable('X', 'Int')]),
1253+
KApply('_==K_', [KVariable(name=abstracted_var.name), KVariable('Y', 'Int')]),
1254+
]
1255+
)
1256+
),
1257+
]
1258+
),
1259+
)
1260+
1261+
assert anti_unifier.kast == expected_anti_unifier.kast
1262+
1263+
def test_anti_unify_subst_true(
1264+
self,
1265+
kcfg_explore: KCFGExplore,
1266+
kprint: KPrint,
1267+
) -> None:
1268+
cterm1 = self.config(
1269+
kprint=kprint,
1270+
k='int $n ; { }',
1271+
state='N |-> 0',
1272+
constraint=mlEqualsTrue(KApply('_==K_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1273+
)
1274+
cterm2 = self.config(
1275+
kprint=kprint,
1276+
k='int $n ; { }',
1277+
state='N |-> 0',
1278+
constraint=mlEqualsTrue(KApply('_==K_', [KVariable('N', 'Int'), KToken('1', 'Int')])),
1279+
)
1280+
1281+
anti_unifier, _, _ = cterm1.anti_unify(cterm2, keep_values=True, kdef=kprint.definition)
1282+
1283+
assert anti_unifier.kast == cterm1.kast

0 commit comments

Comments
 (0)