From cebb33217c03a9c907f08b5984e897ce24ed1a75 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 17 Oct 2023 19:35:31 -0500 Subject: [PATCH 1/7] Start refactor of Prover for work with multithreading --- src/pyk/proof/reachability.py | 77 +++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index f1a7e1b33..584bb6731 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -3,6 +3,7 @@ import graphlib import json import logging +from queue import Queue from dataclasses import dataclass from typing import TYPE_CHECKING @@ -12,6 +13,7 @@ from ..kast.manip import flatten_label, ml_pred_to_bool from ..kast.outer import KClaim from ..kcfg import KCFG +from ..kcfg.explore import ExtendResult from ..kcfg.exploration import KCFGExploration from ..prelude.kbool import BOOL, TRUE from ..prelude.ml import mlAnd, mlEquals, mlTop @@ -630,6 +632,9 @@ class APRProver(Prover): dependencies_module_name: str circularities_module_name: str counterexample_info: bool + + extensions: Queue + iterations: int _checked_for_terminal: set[int] _checked_for_subsumption: set[int] @@ -642,6 +647,8 @@ def __init__( ) -> None: super().__init__(kcfg_explore) self.proof = proof + self.extensions = Queue() + self.iterations = 0 self.main_module_name = self.kcfg_explore.kprint.definition.main_module_name self.counterexample_info = counterexample_info @@ -723,6 +730,76 @@ def advance_pending_node( module_name=module_name, ) + def get_node_extension( + self, + node: KCFG.node, + execute_depth: int | None = None, + cut_point_rules: Iterable[str] = (), + terminal_rules: Iterable[str] = (), + ) -> None: + module_name = self.circularities_module_name if self.nonzero_depth(node) else self.dependencies_module_name + self.kcfg_explore.check_extendable(kcfg_exploration, node) + self.extensions.put( + ( + self.kcfg_explore.extend_cterm( + node.cterm, + execute_depth=execute_depth, + cut_point_rules=cut_point_rules, + terminal_rules=terminal_rules, + module_name=module_name, + ), + node, + ) + ) + + def sync_extensions( + self, + fail_fast: bool = False, + max_iterations: int | None = None, + ) -> None: + self._check_all_terminals() + + while True: + try: + extend_result, node = self.extensions.get_nowait() + except Empty: + break + + if fail_fast and self.proof.failed: + _LOGGER.warning( + f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}' + ) + break #TODO mark proof as done + + if max_iterations is not None and max_iterations <= iterations: + _LOGGER.warning(f'Reached iteration bound {self.proof.id}: {max_iterations}') + break + iterations += 1 + curr_node = self.proof.pending[0] + + self.advance_pending_node( + node=curr_node, + execute_depth=execute_depth, + cut_point_rules=cut_point_rules, + terminal_rules=terminal_rules, + ) + + self._check_all_terminals() + + for node in self.proof.terminal: + if ( + not node.id in self._checked_for_subsumption + and self.proof.kcfg.is_leaf(node.id) + and not self.proof.is_target(node.id) + ): + self._checked_for_subsumption.add(node.id) + self._check_subsume(node) + + if self.proof.failed: + self.save_failure_info() + + self.proof.write_proof_data() + def advance_proof( self, max_iterations: int | None = None, From f44cb7313238dae03e24c9b734132a7691dd62a7 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 19 Oct 2023 21:07:56 -0500 Subject: [PATCH 2/7] Move use separate extending and syncing functions in advance_proof --- src/pyk/proof/reachability.py | 110 +++++++++++++++++++--------------- 1 file changed, 62 insertions(+), 48 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 584bb6731..6fe348b10 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -3,8 +3,8 @@ import graphlib import json import logging -from queue import Queue from dataclasses import dataclass +from queue import Empty, Queue from typing import TYPE_CHECKING from pyk.kore.rpc import LogEntry @@ -13,7 +13,6 @@ from ..kast.manip import flatten_label, ml_pred_to_bool from ..kast.outer import KClaim from ..kcfg import KCFG -from ..kcfg.explore import ExtendResult from ..kcfg.exploration import KCFGExploration from ..prelude.kbool import BOOL, TRUE from ..prelude.ml import mlAnd, mlEquals, mlTop @@ -632,9 +631,10 @@ class APRProver(Prover): dependencies_module_name: str circularities_module_name: str counterexample_info: bool - + extensions: Queue iterations: int + done: bool _checked_for_terminal: set[int] _checked_for_subsumption: set[int] @@ -649,6 +649,7 @@ def __init__( self.proof = proof self.extensions = Queue() self.iterations = 0 + self.done = False self.main_module_name = self.kcfg_explore.kprint.definition.main_module_name self.counterexample_info = counterexample_info @@ -732,13 +733,13 @@ def advance_pending_node( def get_node_extension( self, - node: KCFG.node, + node: KCFG.Node, execute_depth: int | None = None, cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), ) -> None: module_name = self.circularities_module_name if self.nonzero_depth(node) else self.dependencies_module_name - self.kcfg_explore.check_extendable(kcfg_exploration, node) + self.kcfg_explore.check_extendable(self.proof, node) self.extensions.put( ( self.kcfg_explore.extend_cterm( @@ -761,7 +762,7 @@ def sync_extensions( while True: try: - extend_result, node = self.extensions.get_nowait() + extend_result, curr_node = self.extensions.get_nowait() except Empty: break @@ -769,19 +770,20 @@ def sync_extensions( _LOGGER.warning( f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}' ) - break #TODO mark proof as done + self.done = True + break - if max_iterations is not None and max_iterations <= iterations: + if max_iterations is not None and max_iterations <= self.iterations: _LOGGER.warning(f'Reached iteration bound {self.proof.id}: {max_iterations}') + self.done = True break - iterations += 1 - curr_node = self.proof.pending[0] + self.iterations += 1 - self.advance_pending_node( + self.kcfg_explore.extend_kcfg( + extend_result=extend_result, + kcfg=self.proof.kcfg, node=curr_node, - execute_depth=execute_depth, - cut_point_rules=cut_point_rules, - terminal_rules=terminal_rules, + logs=self.proof.logs, ) self._check_all_terminals() @@ -808,46 +810,58 @@ def advance_proof( terminal_rules: Iterable[str] = (), fail_fast: bool = False, ) -> None: - iterations = 0 - - self._check_all_terminals() - - while self.proof.pending: - self.proof.write_proof_data() - if fail_fast and self.proof.failed: - _LOGGER.warning( - f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}' - ) - break - - if max_iterations is not None and max_iterations <= iterations: - _LOGGER.warning(f'Reached iteration bound {self.proof.id}: {max_iterations}') - break - iterations += 1 - curr_node = self.proof.pending[0] + while not self.done: + node = self.proof.pending[0] - self.advance_pending_node( - node=curr_node, + self.get_node_extension( + node=node, execute_depth=execute_depth, cut_point_rules=cut_point_rules, terminal_rules=terminal_rules, ) - self._check_all_terminals() - - for node in self.proof.terminal: - if ( - not node.id in self._checked_for_subsumption - and self.proof.kcfg.is_leaf(node.id) - and not self.proof.is_target(node.id) - ): - self._checked_for_subsumption.add(node.id) - self._check_subsume(node) - - if self.proof.failed: - self.save_failure_info() - - self.proof.write_proof_data() + self.sync_extensions(fail_fast=fail_fast, max_iterations=max_iterations) + + # iterations = 0 + # + # self._check_all_terminals() + # + # while self.proof.pending: + # self.proof.write_proof_data() + # if fail_fast and self.proof.failed: + # _LOGGER.warning( + # f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}' + # ) + # break + # + # if max_iterations is not None and max_iterations <= iterations: + # _LOGGER.warning(f'Reached iteration bound {self.proof.id}: {max_iterations}') + # break + # iterations += 1 + # curr_node = self.proof.pending[0] + # + # self.advance_pending_node( + # node=curr_node, + # execute_depth=execute_depth, + # cut_point_rules=cut_point_rules, + # terminal_rules=terminal_rules, + # ) + # + # self._check_all_terminals() + # + # for node in self.proof.terminal: + # if ( + # not node.id in self._checked_for_subsumption + # and self.proof.kcfg.is_leaf(node.id) + # and not self.proof.is_target(node.id) + # ): + # self._checked_for_subsumption.add(node.id) + # self._check_subsume(node) + # + # if self.proof.failed: + # self.save_failure_info() + # + # self.proof.write_proof_data() def refute_node(self, node: KCFG.Node) -> RefutationProof | None: _LOGGER.info(f'Attempting to refute node {node.id}') From e368c76d67556b7d63c856bdcd7c95f5291f23ad Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 19 Oct 2023 21:46:40 -0500 Subject: [PATCH 3/7] Fix to work with BMC proofs --- src/pyk/proof/reachability.py | 105 +++++++++++++++++++++++++--------- 1 file changed, 77 insertions(+), 28 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 6fe348b10..e595cbe06 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -28,6 +28,7 @@ from ..cterm import CTerm from ..kast.outer import KDefinition, KFlatModuleList from ..kcfg import KCFGExplore + from ..kcfg.explore import ExtendResult from ..kcfg.kcfg import NodeIdLike from ..ktool.kprint import KPrint @@ -753,6 +754,44 @@ def get_node_extension( ) ) + def sync_extension( + self, + extend_result: ExtendResult, + node: KCFG.Node, + fail_fast: bool, + max_iterations: int | None, + ) -> None: + if fail_fast and self.proof.failed: + _LOGGER.warning( + f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}' + ) + self.done = True + return + + if max_iterations is not None and max_iterations <= self.iterations: + _LOGGER.warning(f'Reached iteration bound {self.proof.id}: {max_iterations}') + self.done = True + return + self.iterations += 1 + + self.kcfg_explore.extend_kcfg( + extend_result=extend_result, + kcfg=self.proof.kcfg, + node=node, + logs=self.proof.logs, + ) + + self._check_all_terminals() + + for node in self.proof.terminal: + if ( + not node.id in self._checked_for_subsumption + and self.proof.kcfg.is_leaf(node.id) + and not self.proof.is_target(node.id) + ): + self._checked_for_subsumption.add(node.id) + self._check_subsume(node) + def sync_extensions( self, fail_fast: bool = False, @@ -766,37 +805,13 @@ def sync_extensions( except Empty: break - if fail_fast and self.proof.failed: - _LOGGER.warning( - f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}' - ) - self.done = True - break - - if max_iterations is not None and max_iterations <= self.iterations: - _LOGGER.warning(f'Reached iteration bound {self.proof.id}: {max_iterations}') - self.done = True - break - self.iterations += 1 - - self.kcfg_explore.extend_kcfg( + self.sync_extension( extend_result=extend_result, - kcfg=self.proof.kcfg, node=curr_node, - logs=self.proof.logs, + fail_fast=fail_fast, + max_iterations=max_iterations, ) - self._check_all_terminals() - - for node in self.proof.terminal: - if ( - not node.id in self._checked_for_subsumption - and self.proof.kcfg.is_leaf(node.id) - and not self.proof.is_target(node.id) - ): - self._checked_for_subsumption.add(node.id) - self._check_subsume(node) - if self.proof.failed: self.save_failure_info() @@ -810,7 +825,7 @@ def advance_proof( terminal_rules: Iterable[str] = (), fail_fast: bool = False, ) -> None: - while not self.done: + while not self.done and self.proof.pending: node = self.proof.pending[0] self.get_node_extension( @@ -1113,6 +1128,40 @@ def advance_pending_node( terminal_rules=terminal_rules, ) + def sync_extension( + self, + extend_result: ExtendResult, + node: KCFG.Node, + fail_fast: bool, + max_iterations: int | None, + ) -> None: + if node.id not in self._checked_nodes: + _LOGGER.info(f'Checking bmc depth for node {self.proof.id}: {node.id}') + self._checked_nodes.append(node.id) + _prior_loops = [ + succ.source.id + for succ in self.proof.shortest_path_to(node.id) + if self.kcfg_explore.kcfg_semantics.same_loop(succ.source.cterm, node.cterm) + ] + prior_loops: list[NodeIdLike] = [] + for _pl in _prior_loops: + if not ( + self.proof.kcfg.zero_depth_between(_pl, node.id) + or any(self.proof.kcfg.zero_depth_between(_pl, pl) for pl in prior_loops) + ): + prior_loops.append(_pl) + _LOGGER.info(f'Prior loop heads for node {self.proof.id}: {(node.id, prior_loops)}') + if len(prior_loops) > self.proof.bmc_depth: + self.proof.add_bounded(node.id) + return + + super().sync_extension( + extend_result=extend_result, + node=node, + fail_fast=fail_fast, + max_iterations=max_iterations, + ) + @dataclass(frozen=True) class APRBMCSummary(ProofSummary): From fafc748fddd51acdb4a5c0f5a384ceb0f4f93bbd Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 20 Oct 2023 18:02:24 -0500 Subject: [PATCH 4/7] Fix subsumption not being checked when no is_terminal is defined, fix proof being marked done prematurely --- src/pyk/proof/reachability.py | 41 ++++++++++++++++++++++++++--------- 1 file changed, 31 insertions(+), 10 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index e595cbe06..e53e63b9c 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -650,7 +650,6 @@ def __init__( self.proof = proof self.extensions = Queue() self.iterations = 0 - self.done = False self.main_module_name = self.kcfg_explore.kprint.definition.main_module_name self.counterexample_info = counterexample_info @@ -741,6 +740,11 @@ def get_node_extension( ) -> None: module_name = self.circularities_module_name if self.nonzero_depth(node) else self.dependencies_module_name self.kcfg_explore.check_extendable(self.proof, node) + + if self.proof.target not in self.proof._terminal: + if self._check_subsume(node): + return + self.extensions.put( ( self.kcfg_explore.extend_cterm( @@ -760,18 +764,21 @@ def sync_extension( node: KCFG.Node, fail_fast: bool, max_iterations: int | None, - ) -> None: + ) -> bool: + + print(f'sync_extension: node {node.id}') + if fail_fast and self.proof.failed: _LOGGER.warning( f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}' ) - self.done = True - return + print(f'fail_fast node={node.id}') + return True if max_iterations is not None and max_iterations <= self.iterations: _LOGGER.warning(f'Reached iteration bound {self.proof.id}: {max_iterations}') - self.done = True - return + print(f'max_iterations node={node.id}') + return True self.iterations += 1 self.kcfg_explore.extend_kcfg( @@ -784,6 +791,7 @@ def sync_extension( self._check_all_terminals() for node in self.proof.terminal: + print(f'node {node.id} is terminal') if ( not node.id in self._checked_for_subsumption and self.proof.kcfg.is_leaf(node.id) @@ -791,21 +799,24 @@ def sync_extension( ): self._checked_for_subsumption.add(node.id) self._check_subsume(node) + return False def sync_extensions( self, fail_fast: bool = False, max_iterations: int | None = None, - ) -> None: + ) -> bool: self._check_all_terminals() + done = False + while True: try: extend_result, curr_node = self.extensions.get_nowait() except Empty: break - self.sync_extension( + done = self.sync_extension( extend_result=extend_result, node=curr_node, fail_fast=fail_fast, @@ -817,6 +828,8 @@ def sync_extensions( self.proof.write_proof_data() + return done + def advance_proof( self, max_iterations: int | None = None, @@ -825,8 +838,15 @@ def advance_proof( terminal_rules: Iterable[str] = (), fail_fast: bool = False, ) -> None: - while not self.done and self.proof.pending: + + print(f'pending={self.proof.pending}') + + done = False + + while self.proof.pending and not done: + node = self.proof.pending[0] + print(f'node={node.id}') self.get_node_extension( node=node, @@ -835,7 +855,8 @@ def advance_proof( terminal_rules=terminal_rules, ) - self.sync_extensions(fail_fast=fail_fast, max_iterations=max_iterations) + done = self.sync_extensions(fail_fast=fail_fast, max_iterations=max_iterations) + # iterations = 0 # From 66c9777e06c4d7702be7f1bba699644fbf712623 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 20 Oct 2023 23:12:02 +0000 Subject: [PATCH 5/7] Set Version: 0.1.476 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 7608a133c..1a6661603 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.475 +0.1.476 diff --git a/pyproject.toml b/pyproject.toml index e8d71ff94..91aad9532 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.475" +version = "0.1.476" description = "" authors = [ "Runtime Verification, Inc. ", From 418540db3bfed9369acc8e9dd6ff67c3c36c69d9 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 20 Oct 2023 18:21:37 -0500 Subject: [PATCH 6/7] Fix formatting --- src/pyk/proof/reachability.py | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index e53e63b9c..50a1f35c1 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -765,7 +765,6 @@ def sync_extension( fail_fast: bool, max_iterations: int | None, ) -> bool: - print(f'sync_extension: node {node.id}') if fail_fast and self.proof.failed: @@ -838,13 +837,11 @@ def advance_proof( terminal_rules: Iterable[str] = (), fail_fast: bool = False, ) -> None: - print(f'pending={self.proof.pending}') done = False while self.proof.pending and not done: - node = self.proof.pending[0] print(f'node={node.id}') @@ -857,7 +854,6 @@ def advance_proof( done = self.sync_extensions(fail_fast=fail_fast, max_iterations=max_iterations) - # iterations = 0 # # self._check_all_terminals() @@ -1155,7 +1151,7 @@ def sync_extension( node: KCFG.Node, fail_fast: bool, max_iterations: int | None, - ) -> None: + ) -> bool: if node.id not in self._checked_nodes: _LOGGER.info(f'Checking bmc depth for node {self.proof.id}: {node.id}') self._checked_nodes.append(node.id) @@ -1174,9 +1170,9 @@ def sync_extension( _LOGGER.info(f'Prior loop heads for node {self.proof.id}: {(node.id, prior_loops)}') if len(prior_loops) > self.proof.bmc_depth: self.proof.add_bounded(node.id) - return + return False - super().sync_extension( + return super().sync_extension( extend_result=extend_result, node=node, fail_fast=fail_fast, From 2dcf7382ba89e1a70fdedcb9d008365030b0f3bb Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 23 Oct 2023 17:29:08 +0000 Subject: [PATCH 7/7] Set Version: 0.1.477 --- package/version | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/package/version b/package/version index 1a6661603..ed1bc7cef 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.476 +0.1.477 diff --git a/pyproject.toml b/pyproject.toml index 91aad9532..f4aff56ac 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.476" +version = "0.1.477" description = "" authors = [ "Runtime Verification, Inc. ",