Skip to content

Commit

Permalink
pass make check
Browse files Browse the repository at this point in the history
  • Loading branch information
@Stevengre
Stevengre committed Jul 17, 2024
1 parent d031c7e commit 7ba6b7c
Show file tree
Hide file tree
Showing 2 changed files with 124 additions and 62 deletions.
85 changes: 48 additions & 37 deletions pyk/src/pyk/kcfg/kcfg.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -252,10 +252,11 @@ def to_dict(self) -> dict[str, Any]:

@staticmethod
def from_dict(dct: dict[str, Any], nodes: Mapping[int, KCFG.Node]) -> KCFG.Edge:
return KCFG.Edge(nodes[dct['source']], nodes[dct['target']], tuple(
(info['depth'], tuple(info['rules']), CSubst.from_dict(info['csubst']))
for info in dct['info']
))
return KCFG.Edge(
nodes[dct['source']],
nodes[dct['target']],
tuple((info['depth'], tuple(info['rules']), CSubst.from_dict(info['csubst'])) for info in dct['info']),
)

def to_rule(self, label: str, claim: bool = False, priority: int | None = None) -> KRuleLike:
def is_ceil_condition(kast: KInner) -> bool:
Expand Down Expand Up @@ -380,7 +381,9 @@ def replace_target(self, node: KCFG.Node) -> KCFG.Split:
return KCFG.Split(self.source, tuple(new_targets))

def discard_targets(self, nodes: tuple[NodeIdLike, ...]) -> KCFG.Split:
new_targets = [(target_node, csubst) for target_node, csubst in self._targets if target_node.id not in nodes]
new_targets = [
(target_node, csubst) for target_node, csubst in self._targets if target_node.id not in nodes
]
return KCFG.Split(self.source, tuple(new_targets))

def add_target(self, target: KCFG.Node, csubst: CSubst) -> KCFG.Split:
Expand Down Expand Up @@ -421,8 +424,10 @@ def with_single_target(self, target: KCFG.Node) -> KCFG.NDBranch:

@property
def edges(self) -> tuple[KCFG.Edge, ...]:
return tuple(KCFG.Edge(self.source, target, ((1, (str(rule),), CSubst()),))
for target, rule in zip(self.targets, self.rules, strict=True))
return tuple(
KCFG.Edge(self.source, target, ((1, (str(rule),), CSubst()),))
for target, rule in zip(self.targets, self.rules, strict=True)
)

def replace_source(self, node: KCFG.Node) -> KCFG.NDBranch:
assert node.id == self.source.id
Expand Down Expand Up @@ -737,13 +742,12 @@ def remove_node(self, node_id: NodeIdLike) -> None:
self.remove_alias(alias)

def remove_node_safely(
self,
node_id: NodeIdLike,
predecessors: dict[str, tuple[NodeIdLike, ...]] | None = None,
successors: dict[str, tuple[NodeIdLike, ...]] | None = None,
self,
node_id: NodeIdLike,
predecessors: dict[str, tuple[NodeIdLike, ...]] | None = None,
successors: dict[str, tuple[NodeIdLike, ...]] | None = None,
) -> None:
"""
successor_type: Edge, Cover, Split, NDBranch
"""successor_type: Edge, Cover, Split, NDBranch.
:param node_id: node to be removed safely
:param predecessors: {successor_type: (source_id, ...)};
Expand Down Expand Up @@ -938,13 +942,14 @@ def contains_edge(self, edge: Edge) -> bool:
return edge == other
return False

def create_edge(self,
source_id: NodeIdLike,
target_id: NodeIdLike,
depth: int | Iterable[int],
rules: Iterable[str] | Iterable[Iterable[str]] = (),
csubst: Iterable[CSubst] | None = None,
) -> Edge:
def create_edge(
self,
source_id: NodeIdLike,
target_id: NodeIdLike,
depth: int | Iterable[int],
rules: Iterable[str] | Iterable[Iterable[str]] = (),
csubst: Iterable[CSubst] | None = None,
) -> Edge:
if isinstance(depth, int):
depth = [depth]
for d in depth:
Expand Down Expand Up @@ -1264,8 +1269,8 @@ def minimize(self) -> None:
repeat = self.lift_splits() or repeat

def merge_nodes(self, semantics: KCFGSemantics) -> None:
"""
Merge targets of Split for cutting down the number of branches, using heuristics KCFGSemantics.is_mergeable.
"""Merge targets of Split for cutting down the number of branches, using heuristics KCFGSemantics.is_mergeable.
This should be used after minimize().
Side Effect: The KCFG is rewritten by the following rewrite pattern,
Expand Down Expand Up @@ -1310,9 +1315,10 @@ def merge_nodes(self, semantics: KCFGSemantics) -> None:
# todo: Also, we can merge `A_i -|Edge|-> B_i -|Cover|-> C` into `merged(A_i) -|Edge|-> C -|Split|-> B_i`
# if `C` is user-provided postcondition, then `-|Split|-> B_i` is not needed.

def _create_split_then_merged(split_source: NodeIdLike, nodes_to_merge: tuple[NodeIdLike, ...]) -> tuple[NodeIdLike, CSubst]:
"""
nodes_to_merge: A_x, A_y, ..., A_z
def _create_split_then_merged(
split_source: NodeIdLike, nodes_to_merge: tuple[NodeIdLike, ...]
) -> tuple[NodeIdLike, CSubst]:
"""nodes_to_merge: A_x, A_y, ..., A_z.
return the `A_x or A_y or ... or A_z` node and subts for |Split|-> A_x or A_y or ... or A_z
"""
Expand All @@ -1338,11 +1344,12 @@ def _create_split_then_merged(split_source: NodeIdLike, nodes_to_merge: tuple[No
merged_node = self.create_node(merged_cterm)
return merged_node.id, csubst

def _create_merged_then_split(nodes_to_merge_a: tuple[NodeIdLike, ...], nodes_to_merge_b: tuple[NodeIdLike, ...]) -> tuple[NodeIdLike, tuple[CSubst, ...], tuple[tuple[int, tuple[str, ...], CSubst], ...]]:
"""
nodes_to_merge: B_x, B_y, ..., B_z
def _create_merged_then_split(
nodes_to_merge_a: tuple[NodeIdLike, ...], nodes_to_merge_b: tuple[NodeIdLike, ...]
) -> tuple[NodeIdLike, tuple[CSubst, ...], tuple[tuple[int, tuple[str, ...], CSubst], ...]]:
"""nodes_to_merge: B_x, B_y, ..., B_z.
return:
Return:
1. the `B_x or B_y or ... or B_z` node
2. the subts for |Split|-> B_x, B_y, ..., B_z
3. the edges' info for A -|Edge|-> merged(B_i) -|Split|-> B_i
Expand All @@ -1356,6 +1363,7 @@ def _add_constraints(cs: CSubst, ct: CTerm) -> CSubst:
for constraint in ct.constraints:
cs = cs.add_constraint(constraint)
return cs

csubst0 = _add_constraints(csubst0, cterms_to_merge[0])
csubst1 = _add_constraints(csubst1, cterms_to_merge[1])
csubsts = [csubst0, csubst1]
Expand Down Expand Up @@ -1390,7 +1398,7 @@ def _merge_nodes(s: KCFGSemantics) -> bool:
mergeable_pairs: list[tuple[NodeIdLike, NodeIdLike]] = []
for idx, edge in enumerate(edges):
if idx + 1 < len(edges):
for e in edges[idx + 1:]:
for e in edges[idx + 1 :]:
if s.is_mergeable(edge.target.cterm, e.target.cterm):
mergeable_pairs.append((edge.source.id, e.source.id))
if len(mergeable_pairs) == 0:
Expand All @@ -1408,10 +1416,9 @@ def _merge_nodes(s: KCFGSemantics) -> bool:
a: NodeIdLike = splits_to_merge[index].source.id
mergeable_b_i_s_group: list[list[NodeIdLike]] = []
merged_a_groups: list[tuple[NodeIdLike, CSubst]] = []
merged_b_groups: list[tuple[
NodeIdLike,
tuple[CSubst, ...],
tuple[tuple[int, tuple[str, ...], CSubst], ...]]] = []
merged_b_groups: list[
tuple[NodeIdLike, tuple[CSubst, ...], tuple[tuple[int, tuple[str, ...], CSubst], ...]]
] = []
for mergeable_a_i_s in mergeable_a_i_s_group:
edges = [single(self.edges(source_id=a_i)) for a_i in mergeable_a_i_s]
# extract B_x, B_y, ..., B_z
Expand All @@ -1430,7 +1437,9 @@ def _merge_nodes(s: KCFGSemantics) -> bool:
# then A -|Edge|-> B_x or B_y or ... or B_z
# else A -|Split|-> A_x or A_y or ... or A_z -|Edge|-> B_x or B_y or ... or B_z
if len(merged_a_groups) == 1 and merged_a_groups[0][0] == a:
depth, rules, csubst = zip(*[(info[0], info[1], info[2]) for info in merged_b_groups[0][2]], strict=True)
depth, rules, csubst = zip(
*[(info[0], info[1], info[2]) for info in merged_b_groups[0][2]], strict=True
)
self.create_edge(a, merged_b_groups[0][0], depth, rules, csubst)
else:
splits = self.splits(source_id=a)
Expand All @@ -1440,10 +1449,12 @@ def _merge_nodes(s: KCFGSemantics) -> bool:
split = single(splits)
for merged_a, merged_b in zip(merged_a_groups, merged_b_groups, strict=True):
split = split.add_target(self.node(merged_a[0]), merged_a[1])
depth, rules, csubst = zip(*[(info[0], info[1], info[2]) for info in merged_b[2]],strict=True)
depth, rules, csubst = zip(*[(info[0], info[1], info[2]) for info in merged_b[2]], strict=True)
self.create_edge(merged_a[0], merged_b[0], depth, rules, csubst)
a = self._resolve(a)
self._splits[a] = split # todo: is there anything wrong if I don't change the _deleted and _created?
self._splits[a] = (
split # todo: is there anything wrong if I don't change the _deleted and _created?
)
# B_x or B_y or ... or B_z -|Split|-> B_x, B_y, ..., B_z
for merged_b, mergeable_b_i_s in zip(merged_b_groups, mergeable_b_i_s_group, strict=True):
self.create_split(merged_b[0], zip(mergeable_b_i_s, merged_b[1], strict=True))
Expand Down
101 changes: 76 additions & 25 deletions pyk/src/tests/unit/kcfg/test_merge_nodes.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,12 +21,24 @@ def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool:
return True


x_lt_5_ge_3 = mlAnd([mlEqualsTrue(geInt(KVariable('X'), intToken(3))), mlEqualsTrue(ltInt(KVariable('X'), intToken(5)))])
x_ge_3_lt_5 = mlAnd([mlEqualsTrue(ltInt(KVariable('X'), intToken(5))), mlEqualsTrue(geInt(KVariable('X'), intToken(3)))])
x_lt_3_ge_0 = mlAnd([mlEqualsTrue(geInt(KVariable('X'), intToken(0))), mlEqualsTrue(ltInt(KVariable('X'), intToken(3)))])
x_ge_0_lt_3 = mlAnd([mlEqualsTrue(ltInt(KVariable('X'), intToken(3))), mlEqualsTrue(geInt(KVariable('X'), intToken(0)))])
x_lt_5_ge_4 = mlAnd([mlEqualsTrue(geInt(KVariable('X'), intToken(4))), mlEqualsTrue(ltInt(KVariable('X'), intToken(5)))])
x_lt_4_ge_3 = mlAnd([mlEqualsTrue(geInt(KVariable('X'), intToken(3))), mlEqualsTrue(ltInt(KVariable('X'), intToken(4)))])
x_lt_5_ge_3 = mlAnd(
[mlEqualsTrue(geInt(KVariable('X'), intToken(3))), mlEqualsTrue(ltInt(KVariable('X'), intToken(5)))]
)
x_ge_3_lt_5 = mlAnd(
[mlEqualsTrue(ltInt(KVariable('X'), intToken(5))), mlEqualsTrue(geInt(KVariable('X'), intToken(3)))]
)
x_lt_3_ge_0 = mlAnd(
[mlEqualsTrue(geInt(KVariable('X'), intToken(0))), mlEqualsTrue(ltInt(KVariable('X'), intToken(3)))]
)
x_ge_0_lt_3 = mlAnd(
[mlEqualsTrue(ltInt(KVariable('X'), intToken(3))), mlEqualsTrue(geInt(KVariable('X'), intToken(0)))]
)
x_lt_5_ge_4 = mlAnd(
[mlEqualsTrue(geInt(KVariable('X'), intToken(4))), mlEqualsTrue(ltInt(KVariable('X'), intToken(5)))]
)
x_lt_4_ge_3 = mlAnd(
[mlEqualsTrue(geInt(KVariable('X'), intToken(3))), mlEqualsTrue(ltInt(KVariable('X'), intToken(4)))]
)

x_lt_0 = mlEqualsTrue(ltInt(KVariable('X'), intToken(0)))
x_ge_0 = mlEqualsTrue(geInt(KVariable('X'), intToken(0)))
Expand Down Expand Up @@ -64,15 +76,18 @@ def _lt5(ct: CTerm) -> bool:

def edge_dicts(*edges: Iterable) -> list[dict[str, Any]]:
def _make_edge_dict(i: int, j: int, info: tuple[tuple[int, tuple[str, ...], CSubst], ...] = ()) -> dict[str, Any]:
return {'source': i, 'target': j, 'info': [
{
'depth': depth,
'rules': list(rules),
'csubst': csubst.to_dict(),
}
for depth, rules, csubst in info
]
return {
'source': i,
'target': j,
'info': [
{
'depth': depth,
'rules': list(rules),
'csubst': csubst.to_dict(),
}
for depth, rules, csubst in info
],
}

return [_make_edge_dict(*edge) for edge in edges]

Expand All @@ -95,7 +110,14 @@ def merge_node_test_kcfg() -> KCFG:
'nodes': node_dicts(9, config=x_config()),
'edges': edge_dicts(
(2, 6, ((5, ('r1',), TOP_CSUBST),)),
(3, 7, ((10, ('r2', 'r3'), x_subst().add_constraint(x_lt_5_ge_4)), (15, ('r4',), x_subst().add_constraint(x_lt_4_ge_3)))),
(
3,
7,
(
(10, ('r2', 'r3'), x_subst().add_constraint(x_lt_5_ge_4)),
(15, ('r4',), x_subst().add_constraint(x_lt_4_ge_3)),
),
),
(4, 8, ((20, ('r5',), TOP_CSUBST),)),
(5, 9, ((25, ('r6',), TOP_CSUBST),)),
),
Expand All @@ -122,11 +144,25 @@ def merge_node_test_kcfg_simple_expected() -> KCFG:
'next': 11,
'nodes': node_dicts(10, config=x_config()),
'edges': edge_dicts(
(1, 10, ((5, ('r1',), x_subst().add_constraint(x_ge_5)),
(10, ('r2', 'r3'), x_subst().add_constraint(x_lt_5_ge_4).add_constraint(x_ge_3)), # add_constraint(x_ge_3) is meaningless, should be delte, if & works will for CSubst
(15, ('r4',), x_subst().add_constraint(x_lt_4_ge_3).add_constraint(x_lt_5)), # add_constraint(x_lt_5) is meaningless, should be delte, if & works will for CSubst
(20, ('r5',), x_subst().add_constraint(x_ge_0_lt_3)),
(25, ('r6',), x_subst().add_constraint(x_lt_0)))),
(
1,
10,
(
(5, ('r1',), x_subst().add_constraint(x_ge_5)),
(
10,
('r2', 'r3'),
x_subst().add_constraint(x_lt_5_ge_4).add_constraint(x_ge_3),
), # add_constraint(x_ge_3) is meaningless, should be delte, if & works will for CSubst
(
15,
('r4',),
x_subst().add_constraint(x_lt_4_ge_3).add_constraint(x_lt_5),
), # add_constraint(x_lt_5) is meaningless, should be delte, if & works will for CSubst
(20, ('r5',), x_subst().add_constraint(x_ge_0_lt_3)),
(25, ('r6',), x_subst().add_constraint(x_lt_0)),
),
),
),
'splits': split_dicts((10, [(6, x_ge_5), (7, x_ge_3_lt_5), (8, x_ge_0_lt_3), (9, x_lt_0)]), csubst=x_subst()),
}
Expand Down Expand Up @@ -156,17 +192,33 @@ def merge_node_test_kcfg_complex_expected(cfg: KCFG) -> None:
edge = single(cfg.edges(source_id=split_node_id))
if constraints == mlOr([mlOr([x_ge_3_lt_5, x_ge_0_lt_3]), x_ge_5]):
assert (5, ('r1',), x_subst().add_constraint(x_ge_5)) in edge.info
assert (10, ('r2', 'r3'), x_subst().add_constraint(x_ge_4).add_constraint(x_lt_5).add_constraint(x_ge_3)) in edge.info
assert (15, ('r4',), x_subst().add_constraint(x_ge_3).add_constraint(x_lt_4).add_constraint(x_lt_5)) in edge.info
assert (
10,
('r2', 'r3'),
x_subst().add_constraint(x_ge_4).add_constraint(x_lt_5).add_constraint(x_ge_3),
) in edge.info
assert (
15,
('r4',),
x_subst().add_constraint(x_ge_3).add_constraint(x_lt_4).add_constraint(x_lt_5),
) in edge.info
assert (20, ('r5',), x_subst().add_constraint(x_lt_3).add_constraint(x_ge_0)) in edge.info
end_split = single(cfg.splits(source_id=edge.target.id)).splits
assert end_split[6] == x_subst().add_constraint(x_ge_5)
assert end_split[7] == x_subst().add_constraint(x_lt_5).add_constraint(x_ge_3)
assert end_split[8] == x_subst().add_constraint(x_lt_3).add_constraint(x_ge_0)
elif constraints == mlOr([mlOr([x_ge_3_lt_5, x_ge_0_lt_3]), x_lt_0]):
# constraints == x_lt_5
assert (10, ('r2', 'r3'), x_subst().add_constraint(x_ge_4).add_constraint(x_lt_5).add_constraint(x_ge_3)) in edge.info
assert (15, ('r4',), x_subst().add_constraint(x_ge_3).add_constraint(x_lt_4).add_constraint(x_lt_5)) in edge.info
assert (
10,
('r2', 'r3'),
x_subst().add_constraint(x_ge_4).add_constraint(x_lt_5).add_constraint(x_ge_3),
) in edge.info
assert (
15,
('r4',),
x_subst().add_constraint(x_ge_3).add_constraint(x_lt_4).add_constraint(x_lt_5),
) in edge.info
assert (20, ('r5',), x_subst().add_constraint(x_lt_3).add_constraint(x_ge_0)) in edge.info
assert (25, ('r6',), x_subst().add_constraint(x_lt_0)) in edge.info
end_split = single(cfg.splits(source_id=edge.target.id)).splits
Expand All @@ -188,4 +240,3 @@ def test_merge_node() -> None:
original_cfg = merge_node_test_kcfg()
original_cfg.merge_nodes(complex_semantics)
merge_node_test_kcfg_complex_expected(original_cfg)

0 comments on commit 7ba6b7c

Please sign in to comment.