diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index aebb631687b..21859b5e02d 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/pyk/src/pyk/kcfg/explore.py @@ -59,6 +59,19 @@ def _pretty_printer(self) -> PrettyPrinter: def pretty_print(self, kinner: KInner) -> str: return self._pretty_printer.print(kinner) + def _extract_rule_labels(self, _logs: tuple[LogEntry, ...]) -> list[str]: + _rule_lines = [] + for node_log in _logs: + if isinstance(node_log, LogRewrite) and isinstance(node_log.result, RewriteSuccess): + if node_log.result.rule_id in self.cterm_symbolic._definition.sentence_by_unique_id: + sent = self.cterm_symbolic._definition.sentence_by_unique_id[node_log.result.rule_id] + _rule_lines.append(f'{sent.label}:{sent.source}') + else: + if node_log.result.rule_id == 'UNKNOWN': + _LOGGER.warning(f'Unknown unique id attached to rule log entry: {node_log}') + _rule_lines.append(f'{node_log.result.rule_id}:UNKNOWN') + return _rule_lines + def implication_failure_reason(self, antecedent: CTerm, consequent: CTerm) -> tuple[bool, str]: def _is_cell_subst(csubst: KInner) -> bool: if type(csubst) is KApply and csubst.label.name == '_==K_': @@ -143,8 +156,9 @@ def step( _LOGGER.info(f'Found new node at depth {depth} {self.id}: {shorten_hashes((node.id, new_node.id))}') logs[new_node.id] = exec_res.logs out_edges = cfg.edges(source_id=node.id) + rule_logs = self._extract_rule_labels(exec_res.logs) if len(out_edges) == 0: - cfg.create_edge(node.id, new_node.id, depth=depth) + cfg.create_edge(node.id, new_node.id, depth=depth, rules=rule_logs) else: edge = out_edges[0] if depth > edge.depth: @@ -152,8 +166,8 @@ def step( f'Step depth {depth} greater than original edge depth {edge.depth} {self.id}: {shorten_hashes((edge.source.id, edge.target.id))}' ) cfg.remove_edge(edge.source.id, edge.target.id) - cfg.create_edge(edge.source.id, new_node.id, depth=depth) - cfg.create_edge(new_node.id, edge.target.id, depth=(edge.depth - depth)) + cfg.create_edge(edge.source.id, new_node.id, depth=depth, rules=rule_logs) + cfg.create_edge(new_node.id, edge.target.id, depth=(edge.depth - depth), rules=edge.rules[depth:]) return new_node.id def section_edge( @@ -175,7 +189,6 @@ def section_edge( new_nodes = [] curr_node_id = edge.source.id while new_depth < orig_depth: - _LOGGER.info(f'Taking {section_depth} steps from node {self.id}: {shorten_hashes(curr_node_id)}') curr_node_id = self.step(cfg, curr_node_id, logs, depth=section_depth) new_nodes.append(curr_node_id) new_depth += section_depth @@ -205,18 +218,6 @@ def extend_cterm( def log(message: str, *, warning: bool = False) -> None: _LOGGER.log(logging.WARNING if warning else logging.INFO, f'Extend result for {self.id}: {message}') - def extract_rule_labels(_logs: tuple[LogEntry, ...]) -> list[str]: - _rule_lines = [] - for node_log in _logs: - if isinstance(node_log, LogRewrite) and isinstance(node_log.result, RewriteSuccess): - if node_log.result.rule_id in self.cterm_symbolic._definition.sentence_by_unique_id: - sent = self.cterm_symbolic._definition.sentence_by_unique_id[node_log.result.rule_id] - _rule_lines.append(f'{sent.label}:{sent.source}') - else: - _LOGGER.warning(f'Unknown unique id attached to rule log entry: {node_log}') - _rule_lines.append('UNKNOWN') - return _rule_lines - custom_step_result = self.kcfg_semantics.custom_step(_cterm) if custom_step_result is not None: log(f'custom step node: {node_id}') @@ -238,7 +239,7 @@ def extract_rule_labels(_logs: tuple[LogEntry, ...]) -> list[str]: # Basic block if depth > 0: log(f'basic block at depth {depth}: {node_id}') - return Step(cterm, depth, next_node_logs, extract_rule_labels(next_node_logs)) + return Step(cterm, depth, next_node_logs, self._extract_rule_labels(next_node_logs)) # Stuck or vacuous if not next_states: @@ -255,7 +256,7 @@ def extract_rule_labels(_logs: tuple[LogEntry, ...]) -> list[str]: next_states[0].state, 1, next_node_logs, - extract_rule_labels(next_node_logs), + self._extract_rule_labels(next_node_logs), cut=True, ) @@ -283,4 +284,4 @@ def extract_rule_labels(_logs: tuple[LogEntry, ...]) -> list[str]: # NDBranch log(f'{len(next_states)} non-deterministic branches: {node_id}') next_cterms = [cterm for cterm, _ in next_states] - return NDBranch(next_cterms, next_node_logs, extract_rule_labels(next_node_logs)) + return NDBranch(next_cterms, next_node_logs, self._extract_rule_labels(next_node_logs)) diff --git a/pyk/src/pyk/kore/rpc.py b/pyk/src/pyk/kore/rpc.py index 7f986ab301e..4e309eec4d3 100644 --- a/pyk/src/pyk/kore/rpc.py +++ b/pyk/src/pyk/kore/rpc.py @@ -519,7 +519,7 @@ def extract_entry(pattern: Pattern) -> tuple[EVar, Pattern]: for conjunct in manip.conjuncts(pattern): key, value = extract_entry(conjunct) if key in res: - raise ValueError(f'Duplicate substitution entry key: {key.text}') + raise ValueError(f'Duplicate substitution entry key: {key.text} -> {[res[key].text, value.text]}') res[key] = value return res diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index c6cb2f1316c..73cb82d5a4f 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -70,6 +70,9 @@ class APRProofStep: module_name: str shortest_path_to_node: tuple[KCFG.Node, ...] prior_loops_cache: FrozenDict[int, tuple[int, ...]] = field(compare=False) + circularity: bool + nonzero_depth: bool + circularity_rule_id: str class APRProof(Proof[APRProofStep, APRProofResult], KCFGExploration): @@ -162,10 +165,7 @@ def get_steps(self) -> list[APRProofStep]: else: shortest_path.append(succ.source) - def nonzero_depth(proof: APRProof, node: KCFG.Node) -> bool: - return not proof.kcfg.zero_depth_between(proof.init, node.id) - - module_name = self.circularities_module_name if nonzero_depth(self, node) else self.dependencies_module_name + module_name = self.circularities_module_name if self.nonzero_depth(node) else self.dependencies_module_name steps.append( APRProofStep( @@ -176,6 +176,9 @@ def nonzero_depth(proof: APRProof, node: KCFG.Node) -> bool: target=self.kcfg.node(self.target), shortest_path_to_node=tuple(shortest_path), prior_loops_cache=FrozenDict(self.prior_loops_cache), + circularity=self.circularity, + nonzero_depth=self.nonzero_depth(node), + circularity_rule_id=f'{self.rule_id}-{self.init}-TO-{self.target}', ) ) return steps @@ -193,6 +196,13 @@ def commit(self, result: APRProofResult) -> None: else: raise ValueError(f'Incorrect result type, expected APRProofResult: {result}') + def nonzero_depth(self, node: KCFG.Node) -> bool: + return not self.kcfg.zero_depth_between(self.init, node.id) + + @property + def rule_id(self) -> str: + return f'APRPROOF-{self.id.upper()}' + @property def module_name(self) -> str: return self._make_module_name(self.id) @@ -384,18 +394,22 @@ def from_claim( ) def as_rules(self, priority: int = 20, direct_rule: bool = False) -> list[KRule]: - if (self.passed and direct_rule) or (self.admitted and not self.kcfg.predecessors(self.target)): + if ( + self.circularity + or (self.passed and direct_rule) + or (self.admitted and not self.kcfg.predecessors(self.target)) + ): return [self.as_rule(priority=priority)] _rules = [] for _edge in self.kcfg.edges(): - _rule = _edge.to_rule(f'APRPROOF-{self.id.upper()}-BASIC-BLOCK', priority=priority) + _rule = _edge.to_rule(self.rule_id, priority=priority) assert type(_rule) is KRule _rules.append(_rule) return _rules def as_rule(self, priority: int = 20) -> KRule: _edge = KCFG.Edge(self.kcfg.node(self.init), self.kcfg.node(self.target), depth=0, rules=()) - _rule = _edge.to_rule(f'APRPROOF-{self.id.upper()}-BASIC-BLOCK', priority=priority) + _rule = _edge.to_rule(self.rule_id, priority=priority) assert type(_rule) is KRule return _rule @@ -791,10 +805,20 @@ def step_proof(self, step: APRProofStep) -> list[APRProofResult]: if is_terminal: return terminal_result + # Ensure that we cut at applications of circularity, so that subsumption into target state will be checked + cut_rules = list(self.cut_point_rules) + if step.circularity and step.nonzero_depth: + cut_rules.append(step.circularity_rule_id) + + # Ensure that we record progress ASAP for circularities, so the circularity rule will be included for execution as soon as possible + execute_depth = self.execute_depth + if step.circularity and not step.nonzero_depth and (execute_depth is None or execute_depth > 1): + execute_depth = 1 + extend_result = self.kcfg_explore.extend_cterm( step.node.cterm, - execute_depth=self.execute_depth, - cut_point_rules=self.cut_point_rules, + execute_depth=execute_depth, + cut_point_rules=cut_rules, terminal_rules=self.terminal_rules, module_name=step.module_name, node_id=step.node.id, diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index cb49a3ffd9f..b087432a8ea 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -508,7 +508,7 @@ def custom_step(self, c: CTerm) -> KCFGExtendResult | None: 'sum-loop', None, None, - ['IMP.while'], # If we do not include `IMP.while` in this list, we get 4 branches instead of 2 + [], True, ProofStatus.PASSED, 2,