From 6fd119b36c55473d42c31c33f85ca54207086aa0 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 26 Feb 2024 16:57:02 -0700 Subject: [PATCH] Split out CTerm manipulation functionalities of KCFGExplore (#915) `KCFGExplore` class has grown quite a bit, and broadly contains two types of things: (i) wrappers around the `KoreClient` for the `CTerm` class, and (ii) functionalities for manipulating KCFGs using said wrappers. This PR pulls the first category out into a new submodule of the `cterm` submodule. - Module `cterm/symbolic.py` is added, with class `CTermSymbolic`, which wraps a `KoreClient` and lifts its functionalities to from Kore to `CTerm` level. - The class `CTermSymbolic` doesn't need access to a `KPrint`, instead just a `KDefinition` and a `KompiledKore`. - The class `CTermSymbolic` implements two new methods `CTermSymbolic.kast_to_kore(KInner) -> Pattern` and `CTermSymbolic.kore_to_kast(Pattern) -> KInner` as wrappers around the methods in `konvert` which have the definitions applied, and uses them in the various methods instead. In particular, that means we do _not_ have fallback to `kast` binary for these methods (instead crashes), but these codepaths are very well tested now. - The methods from `KCFGExplore.cterm_*` are moved to the `CTermSymbolic` class, with the prefix `cterm_` dropped. - The `KCFGExplore` is updated to use this class instead of a `KoreClient` directly, and various `*Prover` classes are updated as well. - Updates to the testing harness are made: - A new fixture `CTermSymbolic` is added, for when only that is needed. - The directory `src/tests/integration/kcfg` is moved to `src/tests/integration/cterm`, and lowered to `CTermSymbolic` instead of `KCFGExplore`. --------- Co-authored-by: devops --- docs/conf.py | 4 +- package/version | 2 +- pyproject.toml | 2 +- src/pyk/cterm/__init__.py | 1 + src/pyk/cterm/symbolic.py | 191 ++++++++++++++++++ src/pyk/kcfg/explore.py | 176 ++-------------- src/pyk/proof/implies.py | 6 +- src/pyk/proof/reachability.py | 10 +- src/pyk/testing/__init__.py | 1 + src/pyk/testing/_kompiler.py | 24 ++- .../integration/{kcfg => cterm}/__init__.py | 0 .../test_multiple_definitions.py | 24 ++- .../{kcfg => cterm}/test_simple.py | 28 +-- src/tests/integration/proof/test_cell_map.py | 6 +- src/tests/integration/proof/test_imp.py | 8 +- src/tests/integration/proof/test_mini_kevm.py | 2 +- 16 files changed, 280 insertions(+), 205 deletions(-) create mode 100644 src/pyk/cterm/symbolic.py rename src/tests/integration/{kcfg => cterm}/__init__.py (100%) rename src/tests/integration/{kcfg => cterm}/test_multiple_definitions.py (61%) rename src/tests/integration/{kcfg => cterm}/test_simple.py (77%) diff --git a/docs/conf.py b/docs/conf.py index cb1b74f20..4f780f8e4 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.652' -release = '0.1.652' +version = '0.1.653' +release = '0.1.653' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index 6f983f2ac..4e0b49191 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.652 +0.1.653 diff --git a/pyproject.toml b/pyproject.toml index 250a351ee..d2e3857ac 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.652" +version = "0.1.653" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/cterm/__init__.py b/src/pyk/cterm/__init__.py index 9993912f6..9615f699e 100644 --- a/src/pyk/cterm/__init__.py +++ b/src/pyk/cterm/__init__.py @@ -1 +1,2 @@ from .cterm import CSubst, CTerm, build_claim, build_rule +from .symbolic import CTermSymbolic diff --git a/src/pyk/cterm/symbolic.py b/src/pyk/cterm/symbolic.py new file mode 100644 index 000000000..8e104e315 --- /dev/null +++ b/src/pyk/cterm/symbolic.py @@ -0,0 +1,191 @@ +from __future__ import annotations + +import logging +from typing import TYPE_CHECKING, NamedTuple + +from ..cterm import CSubst, CTerm +from ..kast.inner import KApply, KLabel, KVariable, Subst +from ..kast.manip import flatten_label, free_vars +from ..konvert import kast_to_kore, kore_to_kast +from ..kore.rpc import AbortedResult, SatResult, StopReason, UnknownResult, UnsatResult +from ..prelude.k import GENERATED_TOP_CELL +from ..prelude.ml import is_top, mlEquals, mlTop + +if TYPE_CHECKING: + from collections.abc import Iterable + from typing import Final + + from ..kast import KInner + from ..kast.outer import KDefinition + from ..kore.kompiled import KompiledKore + from ..kore.rpc import KoreClient, LogEntry + from ..kore.syntax import Pattern + + +_LOGGER: Final = logging.getLogger(__name__) + + +class CTermExecute(NamedTuple): + state: CTerm + next_states: tuple[CTerm, ...] + depth: int + vacuous: bool + logs: tuple[LogEntry, ...] + + +class CTermSymbolic: + _kore_client: KoreClient + _definition: KDefinition + _kompiled_kore: KompiledKore + _trace_rewrites: bool + + def __init__( + self, + kore_client: KoreClient, + definition: KDefinition, + kompiled_kore: KompiledKore, + *, + trace_rewrites: bool = False, + ): + self._kore_client = kore_client + self._definition = definition + self._kompiled_kore = kompiled_kore + self._trace_rewrites = trace_rewrites + + def kast_to_kore(self, kinner: KInner) -> Pattern: + return kast_to_kore(self._definition, self._kompiled_kore, kinner, sort=GENERATED_TOP_CELL) + + def kore_to_kast(self, pattern: Pattern) -> KInner: + return kore_to_kast(self._definition, pattern) + + def execute( + self, + cterm: CTerm, + depth: int | None = None, + cut_point_rules: Iterable[str] | None = None, + terminal_rules: Iterable[str] | None = None, + module_name: str | None = None, + ) -> CTermExecute: + _LOGGER.debug(f'Executing: {cterm}') + kore = self.kast_to_kore(cterm.kast) + response = self._kore_client.execute( + kore, + max_depth=depth, + cut_point_rules=cut_point_rules, + terminal_rules=terminal_rules, + module_name=module_name, + log_successful_rewrites=True, + log_failed_rewrites=self._trace_rewrites, + log_successful_simplifications=self._trace_rewrites, + log_failed_simplifications=self._trace_rewrites, + ) + + if isinstance(response, AbortedResult): + unknown_predicate = response.unknown_predicate.text if response.unknown_predicate else None + raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}') + + state = CTerm.from_kast(self.kore_to_kast(response.state.kore)) + resp_next_states = response.next_states or () + next_states = tuple(CTerm.from_kast(self.kore_to_kast(ns.kore)) for ns in resp_next_states) + + assert all(not cterm.is_bottom for cterm in next_states) + assert len(next_states) != 1 or response.reason is StopReason.CUT_POINT_RULE + + return CTermExecute( + state=state, + next_states=next_states, + depth=response.depth, + vacuous=response.reason is StopReason.VACUOUS, + logs=response.logs, + ) + + def simplify(self, cterm: CTerm) -> tuple[CTerm, tuple[LogEntry, ...]]: + _LOGGER.debug(f'Simplifying: {cterm}') + kore = self.kast_to_kore(cterm.kast) + kore_simplified, logs = self._kore_client.simplify(kore) + kast_simplified = self.kore_to_kast(kore_simplified) + return CTerm.from_kast(kast_simplified), logs + + def kast_simplify(self, kast: KInner) -> tuple[KInner, tuple[LogEntry, ...]]: + _LOGGER.debug(f'Simplifying: {kast}') + kore = self.kast_to_kore(kast) + kore_simplified, logs = self._kore_client.simplify(kore) + kast_simplified = self.kore_to_kast(kore_simplified) + return kast_simplified, logs + + def get_model(self, cterm: CTerm, module_name: str | None = None) -> Subst | None: + _LOGGER.info(f'Getting model: {cterm}') + kore = self.kast_to_kore(cterm.kast) + result = self._kore_client.get_model(kore, module_name=module_name) + if type(result) is UnknownResult: + _LOGGER.debug('Result is Unknown') + return None + elif type(result) is UnsatResult: + _LOGGER.debug('Result is UNSAT') + return None + elif type(result) is SatResult: + _LOGGER.debug('Result is SAT') + if not result.model: + return Subst({}) + model_subst = self.kore_to_kast(result.model) + try: + return Subst.from_pred(model_subst) + except ValueError as err: + raise AssertionError(f'Received a non-substitution from get-model endpoint: {model_subst}') from err + + else: + raise AssertionError('Received an invalid response from get-model endpoint') + + def implies( + self, + antecedent: CTerm, + consequent: CTerm, + bind_universally: bool = False, + ) -> CSubst | None: + _LOGGER.debug(f'Checking implication: {antecedent} #Implies {consequent}') + _consequent = consequent.kast + fv_antecedent = free_vars(antecedent.kast) + unbound_consequent = [v for v in free_vars(_consequent) if v not in fv_antecedent] + if len(unbound_consequent) > 0: + bind_text, bind_label = ('existentially', '#Exists') + if bind_universally: + bind_text, bind_label = ('universally', '#Forall') + _LOGGER.debug(f'Binding variables in consequent {bind_text}: {unbound_consequent}') + for uc in unbound_consequent: + _consequent = KApply(KLabel(bind_label, [GENERATED_TOP_CELL]), [KVariable(uc), _consequent]) + antecedent_kore = self.kast_to_kore(antecedent.kast) + consequent_kore = self.kast_to_kore(_consequent) + result = self._kore_client.implies(antecedent_kore, consequent_kore) + if not result.satisfiable: + if result.substitution is not None: + _LOGGER.debug(f'Received a non-empty substitution for unsatisfiable implication: {result.substitution}') + if result.predicate is not None: + _LOGGER.debug(f'Received a non-empty predicate for unsatisfiable implication: {result.predicate}') + return None + if result.substitution is None: + raise ValueError('Received empty substutition for satisfiable implication.') + if result.predicate is None: + raise ValueError('Received empty predicate for satisfiable implication.') + ml_subst = self.kore_to_kast(result.substitution) + ml_pred = self.kore_to_kast(result.predicate) if result.predicate is not None else mlTop() + ml_preds = flatten_label('#And', ml_pred) + if is_top(ml_subst): + return CSubst(subst=Subst({}), constraints=ml_preds) + subst_pattern = mlEquals(KVariable('###VAR'), KVariable('###TERM')) + _subst: dict[str, KInner] = {} + for subst_pred in flatten_label('#And', ml_subst): + m = subst_pattern.match(subst_pred) + if m is not None and type(m['###VAR']) is KVariable: + _subst[m['###VAR'].name] = m['###TERM'] + else: + raise AssertionError(f'Received a non-substitution from implies endpoint: {subst_pred}') + return CSubst(subst=Subst(_subst), constraints=ml_preds) + + def assume_defined(self, cterm: CTerm) -> CTerm: + _LOGGER.debug(f'Computing definedness condition for: {cterm}') + kast = KApply(KLabel('#Ceil', [GENERATED_TOP_CELL, GENERATED_TOP_CELL]), [cterm.config]) + kore = self.kast_to_kore(kast) + kore_simplified, _logs = self._kore_client.simplify(kore) + kast_simplified = self.kore_to_kast(kore_simplified) + _LOGGER.debug(f'Definedness condition computed: {kast_simplified}') + return cterm.add_constraint(kast_simplified) diff --git a/src/pyk/kcfg/explore.py b/src/pyk/kcfg/explore.py index 31a5ad751..ddaeea24f 100644 --- a/src/pyk/kcfg/explore.py +++ b/src/pyk/kcfg/explore.py @@ -1,27 +1,25 @@ from __future__ import annotations import logging -from typing import TYPE_CHECKING, NamedTuple +from typing import TYPE_CHECKING -from ..cterm import CSubst, CTerm -from ..kast.inner import KApply, KLabel, KRewrite, KVariable, Subst +from ..cterm import CTerm +from ..kast.inner import KApply, KRewrite, KVariable, Subst from ..kast.manip import ( abstract_term_safely, bottom_up, extract_lhs, extract_rhs, flatten_label, - free_vars, minimize_term, ml_pred_to_bool, push_down_rewrites, ) -from ..kore.rpc import AbortedResult, RewriteSuccess, SatResult, StopReason, UnknownResult, UnsatResult +from ..kore.rpc import RewriteSuccess from ..prelude import k -from ..prelude.k import GENERATED_TOP_CELL from ..prelude.kbool import notBool from ..prelude.kint import leInt, ltInt -from ..prelude.ml import is_top, mlAnd, mlEquals, mlEqualsFalse, mlEqualsTrue, mlImplies, mlNot, mlTop +from ..prelude.ml import mlAnd, mlEqualsFalse, mlEqualsTrue, mlImplies, mlNot, mlTop from ..utils import shorten_hashes, single from .kcfg import KCFG, Abstract, Branch, NDBranch, Step, Stuck, Vacuous from .semantics import DefaultSemantics @@ -30,9 +28,10 @@ from collections.abc import Iterable from typing import Final + from ..cterm import CTermSymbolic from ..kast import KInner from ..kcfg.exploration import KCFGExploration - from ..kore.rpc import KoreClient, LogEntry + from ..kore.rpc import LogEntry from ..ktool.kprint import KPrint from .kcfg import KCFGExtendResult, NodeIdLike from .semantics import KCFGSemantics @@ -41,159 +40,25 @@ _LOGGER: Final = logging.getLogger(__name__) -class CTermExecute(NamedTuple): - state: CTerm - next_states: tuple[CTerm, ...] - depth: int - vacuous: bool - logs: tuple[LogEntry, ...] - - class KCFGExplore: kprint: KPrint - _kore_client: KoreClient + cterm_symbolic: CTermSymbolic kcfg_semantics: KCFGSemantics id: str - _trace_rewrites: bool def __init__( self, kprint: KPrint, - kore_client: KoreClient, + cterm_symbolic: CTermSymbolic, *, kcfg_semantics: KCFGSemantics | None = None, id: str | None = None, - trace_rewrites: bool = False, ): self.kprint = kprint - self._kore_client = kore_client + self.cterm_symbolic = cterm_symbolic self.kcfg_semantics = kcfg_semantics if kcfg_semantics is not None else DefaultSemantics() self.id = id if id is not None else 'NO ID' - self._trace_rewrites = trace_rewrites - - def cterm_execute( - self, - cterm: CTerm, - depth: int | None = None, - cut_point_rules: Iterable[str] | None = None, - terminal_rules: Iterable[str] | None = None, - module_name: str | None = None, - ) -> CTermExecute: - _LOGGER.debug(f'Executing: {cterm}') - kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL) - response = self._kore_client.execute( - kore, - max_depth=depth, - cut_point_rules=cut_point_rules, - terminal_rules=terminal_rules, - module_name=module_name, - log_successful_rewrites=True, - log_failed_rewrites=self._trace_rewrites, - log_successful_simplifications=self._trace_rewrites, - log_failed_simplifications=self._trace_rewrites, - ) - - if isinstance(response, AbortedResult): - unknown_predicate = response.unknown_predicate.text if response.unknown_predicate else None - raise ValueError(f'Backend responded with aborted state. Unknown predicate: {unknown_predicate}') - - state = CTerm.from_kast(self.kprint.kore_to_kast(response.state.kore)) - resp_next_states = response.next_states or () - next_states = tuple(CTerm.from_kast(self.kprint.kore_to_kast(ns.kore)) for ns in resp_next_states) - - assert all(not cterm.is_bottom for cterm in next_states) - assert len(next_states) != 1 or response.reason is StopReason.CUT_POINT_RULE - - return CTermExecute( - state=state, - next_states=next_states, - depth=response.depth, - vacuous=response.reason is StopReason.VACUOUS, - logs=response.logs, - ) - - def cterm_simplify(self, cterm: CTerm) -> tuple[CTerm, tuple[LogEntry, ...]]: - _LOGGER.debug(f'Simplifying: {cterm}') - kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL) - kore_simplified, logs = self._kore_client.simplify(kore) - kast_simplified = self.kprint.kore_to_kast(kore_simplified) - return CTerm.from_kast(kast_simplified), logs - - def kast_simplify(self, kast: KInner) -> tuple[KInner, tuple[LogEntry, ...]]: - _LOGGER.debug(f'Simplifying: {kast}') - kore = self.kprint.kast_to_kore(kast, GENERATED_TOP_CELL) - kore_simplified, logs = self._kore_client.simplify(kore) - kast_simplified = self.kprint.kore_to_kast(kore_simplified) - return kast_simplified, logs - - def cterm_get_model(self, cterm: CTerm, module_name: str | None = None) -> Subst | None: - _LOGGER.info(f'Getting model: {cterm}') - kore = self.kprint.kast_to_kore(cterm.kast, GENERATED_TOP_CELL) - result = self._kore_client.get_model(kore, module_name=module_name) - if type(result) is UnknownResult: - _LOGGER.debug('Result is Unknown') - return None - elif type(result) is UnsatResult: - _LOGGER.debug('Result is UNSAT') - return None - elif type(result) is SatResult: - _LOGGER.debug('Result is SAT') - if not result.model: - return Subst({}) - model_subst = self.kprint.kore_to_kast(result.model) - try: - return Subst.from_pred(model_subst) - except ValueError as err: - raise AssertionError(f'Received a non-substitution from get-model endpoint: {model_subst}') from err - - else: - raise AssertionError('Received an invalid response from get-model endpoint') - - def cterm_implies( - self, - antecedent: CTerm, - consequent: CTerm, - bind_universally: bool = False, - ) -> CSubst | None: - _LOGGER.debug(f'Checking implication: {antecedent} #Implies {consequent}') - _consequent = consequent.kast - fv_antecedent = free_vars(antecedent.kast) - unbound_consequent = [v for v in free_vars(_consequent) if v not in fv_antecedent] - if len(unbound_consequent) > 0: - bind_text, bind_label = ('existentially', '#Exists') - if bind_universally: - bind_text, bind_label = ('universally', '#Forall') - _LOGGER.debug(f'Binding variables in consequent {bind_text}: {unbound_consequent}') - for uc in unbound_consequent: - _consequent = KApply(KLabel(bind_label, [GENERATED_TOP_CELL]), [KVariable(uc), _consequent]) - antecedent_kore = self.kprint.kast_to_kore(antecedent.kast, GENERATED_TOP_CELL) - consequent_kore = self.kprint.kast_to_kore(_consequent, GENERATED_TOP_CELL) - result = self._kore_client.implies(antecedent_kore, consequent_kore) - if not result.satisfiable: - if result.substitution is not None: - _LOGGER.debug(f'Received a non-empty substitution for unsatisfiable implication: {result.substitution}') - if result.predicate is not None: - _LOGGER.debug(f'Received a non-empty predicate for unsatisfiable implication: {result.predicate}') - return None - if result.substitution is None: - raise ValueError('Received empty substutition for satisfiable implication.') - if result.predicate is None: - raise ValueError('Received empty predicate for satisfiable implication.') - ml_subst = self.kprint.kore_to_kast(result.substitution) - ml_pred = self.kprint.kore_to_kast(result.predicate) if result.predicate is not None else mlTop() - ml_preds = flatten_label('#And', ml_pred) - if is_top(ml_subst): - return CSubst(subst=Subst({}), constraints=ml_preds) - subst_pattern = mlEquals(KVariable('###VAR'), KVariable('###TERM')) - _subst: dict[str, KInner] = {} - for subst_pred in flatten_label('#And', ml_subst): - m = subst_pattern.match(subst_pred) - if m is not None and type(m['###VAR']) is KVariable: - _subst[m['###VAR'].name] = m['###TERM'] - else: - raise AssertionError(f'Received a non-substitution from implies endpoint: {subst_pred}') - return CSubst(subst=Subst(_subst), constraints=ml_preds) def implication_failure_reason(self, antecedent: CTerm, consequent: CTerm) -> tuple[bool, str]: def no_cell_rewrite_to_dots(term: KInner) -> KInner: @@ -233,7 +98,9 @@ def _replace_rewrites_with_implies(_kast: KInner) -> KInner: return bottom_up(_replace_rewrites_with_implies, kast) - config_match = self.cterm_implies(CTerm.from_kast(antecedent.config), CTerm.from_kast(consequent.config)) + config_match = self.cterm_symbolic.implies( + CTerm.from_kast(antecedent.config), CTerm.from_kast(consequent.config) + ) if config_match is None: failing_cells = [] curr_cell_match = Subst({}) @@ -273,19 +140,10 @@ def _replace_rewrites_with_implies(_kast: KInner) -> KInner: return (False, f'Implication check failed, the following is the remaining implication:\n{fail_str}') return (True, '') - def cterm_assume_defined(self, cterm: CTerm) -> CTerm: - _LOGGER.debug(f'Computing definedness condition for: {cterm}') - kast = KApply(KLabel('#Ceil', [GENERATED_TOP_CELL, GENERATED_TOP_CELL]), [cterm.config]) - kore = self.kprint.kast_to_kore(kast, GENERATED_TOP_CELL) - kore_simplified, _logs = self._kore_client.simplify(kore) - kast_simplified = self.kprint.kore_to_kast(kore_simplified) - _LOGGER.debug(f'Definedness condition computed: {kast_simplified}') - return cterm.add_constraint(kast_simplified) - def simplify(self, cfg: KCFG, logs: dict[int, tuple[LogEntry, ...]]) -> None: for node in cfg.nodes: _LOGGER.info(f'Simplifying node {self.id}: {shorten_hashes(node.id)}') - new_term, next_node_logs = self.cterm_simplify(node.cterm) + new_term, next_node_logs = self.cterm_symbolic.simplify(node.cterm) if new_term != node.cterm: cfg.replace_node(node.id, new_term) if node.id in logs: @@ -308,7 +166,7 @@ def step( if len(successors) != 0 and type(successors[0]) is KCFG.Split: raise ValueError(f'Cannot take step from split node {self.id}: {shorten_hashes(node.id)}') _LOGGER.info(f'Taking {depth} steps from node {self.id}: {shorten_hashes(node.id)}') - exec_res = self.cterm_execute(node.cterm, depth=depth, module_name=module_name) + exec_res = self.cterm_symbolic.execute(node.cterm, depth=depth, module_name=module_name) if exec_res.depth != depth: raise ValueError(f'Unable to take {depth} steps from node, got {exec_res.depth} steps {self.id}: {node.id}') if len(exec_res.next_states) > 0: @@ -400,7 +258,7 @@ def extract_rule_labels(_logs: tuple[LogEntry, ...]) -> list[str]: branches = [] for constraint in _branches: kast = mlAnd(list(_cterm.constraints) + [constraint]) - kast, _ = self.kast_simplify(kast) + kast, _ = self.cterm_symbolic.kast_simplify(kast) if not CTerm._is_bottom(kast): branches.append(constraint) if len(branches) > 1: @@ -408,7 +266,7 @@ def extract_rule_labels(_logs: tuple[LogEntry, ...]) -> list[str]: log(f'{len(branches)} branches using heuristics: {node_id} -> {constraint_strs}') return Branch(branches, heuristic=True) - cterm, next_cterms, depth, vacuous, next_node_logs = self.cterm_execute( + cterm, next_cterms, depth, vacuous, next_node_logs = self.cterm_symbolic.execute( _cterm, depth=execute_depth, cut_point_rules=cut_point_rules, diff --git a/src/pyk/proof/implies.py b/src/pyk/proof/implies.py index 9e27b9840..b9c8e08d6 100644 --- a/src/pyk/proof/implies.py +++ b/src/pyk/proof/implies.py @@ -389,8 +389,8 @@ def step_proof(self) -> None: # to prove the equality, we check the implication of the form `constraints #Implies LHS #Equals RHS`, i.e. # "LHS equals RHS under these constraints" - antecedent_simplified_kast, _ = self.kcfg_explore.kast_simplify(self.proof.antecedent) - consequent_simplified_kast, _ = self.kcfg_explore.kast_simplify(self.proof.consequent) + antecedent_simplified_kast, _ = self.kcfg_explore.cterm_symbolic.kast_simplify(self.proof.antecedent) + consequent_simplified_kast, _ = self.kcfg_explore.cterm_symbolic.kast_simplify(self.proof.consequent) self.proof.simplified_antecedent = antecedent_simplified_kast self.proof.simplified_consequent = consequent_simplified_kast _LOGGER.info(f'Simplified antecedent: {self.kcfg_explore.kprint.pretty_print(antecedent_simplified_kast)}') @@ -407,7 +407,7 @@ def step_proof(self) -> None: else: # TODO: we should not be forced to include the dummy configuration in the antecedent and consequent dummy_config = self.kcfg_explore.kprint.definition.empty_config(sort=GENERATED_TOP_CELL) - result = self.kcfg_explore.cterm_implies( + result = self.kcfg_explore.cterm_symbolic.implies( antecedent=CTerm(config=dummy_config, constraints=[self.proof.simplified_antecedent]), consequent=CTerm(config=dummy_config, constraints=[self.proof.simplified_consequent]), bind_universally=self.proof.bind_universally, diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index 1bd8f4112..b9fbe4a36 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -578,7 +578,7 @@ def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike _kore_module = kflatmodule_to_kore( self.kcfg_explore.kprint.definition, self.kcfg_explore.kprint.kompiled_kore, _module ) - self.kcfg_explore._kore_client.add_module(_kore_module, name_as_id=True) + self.kcfg_explore.cterm_symbolic._kore_client.add_module(_kore_module, name_as_id=True) super().__init__(kcfg_explore) self.proof = proof @@ -648,7 +648,7 @@ def _check_subsume(self, node: KCFG.Node) -> bool: f'Skipping full subsumption check because of fast may subsume check {self.proof.id}: {node.id}' ) return False - csubst = self.kcfg_explore.cterm_implies(node.cterm, self.proof.kcfg.node(self.proof.target).cterm) + csubst = self.kcfg_explore.cterm_symbolic.implies(node.cterm, self.proof.kcfg.node(self.proof.target).cterm) if csubst is not None: self.proof.kcfg.create_cover(node.id, self.proof.target, csubst=csubst) _LOGGER.info(f'Subsumed into target node {self.proof.id}: {shorten_hashes((node.id, self.proof.target))}') @@ -804,14 +804,14 @@ def from_proof(proof: APRProof, kcfg_explore: KCFGExplore, counterexample_info: failure_reasons = {} models = {} for node in proof.failing: - node_cterm, _ = kcfg_explore.cterm_simplify(node.cterm) - target_cterm, _ = kcfg_explore.cterm_simplify(target.cterm) + node_cterm, _ = kcfg_explore.cterm_symbolic.simplify(node.cterm) + target_cterm, _ = kcfg_explore.cterm_symbolic.simplify(target.cterm) _, reason = kcfg_explore.implication_failure_reason(node_cterm, target_cterm) path_condition = kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id)) failure_reasons[node.id] = reason path_conditions[node.id] = path_condition if counterexample_info: - model_subst = kcfg_explore.cterm_get_model(node.cterm) + model_subst = kcfg_explore.cterm_symbolic.get_model(node.cterm) if type(model_subst) is Subst: model: list[tuple[str, str]] = [] for var, term in model_subst.to_dict().items(): diff --git a/src/pyk/testing/__init__.py b/src/pyk/testing/__init__.py index d3021b7d0..f220df839 100644 --- a/src/pyk/testing/__init__.py +++ b/src/pyk/testing/__init__.py @@ -1,4 +1,5 @@ from ._kompiler import ( + CTermSymbolicTest, KCFGExploreTest, KompiledTest, Kompiler, diff --git a/src/pyk/testing/_kompiler.py b/src/pyk/testing/_kompiler.py index 8eb95a394..66088c172 100644 --- a/src/pyk/testing/_kompiler.py +++ b/src/pyk/testing/_kompiler.py @@ -7,10 +7,12 @@ import pytest +from ..cterm import CTermSymbolic from ..kast.outer import read_kast_definition from ..kcfg import KCFGExplore from ..kllvm.compiler import compile_runtime from ..kllvm.importer import import_runtime +from ..kore.kompiled import KompiledKore from ..kore.pool import KoreServerPool from ..kore.rpc import BoosterServer, KoreClient, KoreServer from ..ktool import TypeInferenceMode @@ -70,6 +72,10 @@ def definition_dir(self, kompile: Kompiler) -> Path: def definition(self, definition_dir: Path) -> KDefinition: return read_kast_definition(definition_dir / 'compiled.json') + @pytest.fixture(scope='class') + def kompiled_kore(self, definition_dir: Path) -> KompiledKore: + return KompiledKore.load(definition_dir) + @pytest.fixture(scope='class') def definition_info(self, definition_dir: Path) -> DefinitionInfo: return DefinitionInfo(definition_dir) @@ -226,7 +232,19 @@ def kore_client(self, _kore_server: KoreServer, bug_report: BugReport) -> Iterat yield client -class KCFGExploreTest(KoreClientTest, KPrintTest): +class CTermSymbolicTest(KoreClientTest): + @pytest.fixture + def cterm_symbolic( + self, + kore_client: KoreClient, + definition: KDefinition, + kompiled_kore: KompiledKore, + bug_report: BugReport | None, + ) -> CTermSymbolic: + return CTermSymbolic(kore_client, definition, kompiled_kore) + + +class KCFGExploreTest(CTermSymbolicTest, KPrintTest): @abstractmethod def semantics(self, definition: KDefinition) -> KCFGSemantics: ... @@ -234,12 +252,12 @@ def semantics(self, definition: KDefinition) -> KCFGSemantics: @pytest.fixture def kcfg_explore( self, - kore_client: KoreClient, + cterm_symbolic: CTermSymbolic, kprint: KProve, bug_report: BugReport | None, ) -> Iterator[KCFGExplore]: semantics = self.semantics(kprint.definition) - yield KCFGExplore(kprint, kore_client, kcfg_semantics=semantics) + yield KCFGExplore(kprint, cterm_symbolic, kcfg_semantics=semantics) class KoreServerPoolTest(KompiledTest, ABC): diff --git a/src/tests/integration/kcfg/__init__.py b/src/tests/integration/cterm/__init__.py similarity index 100% rename from src/tests/integration/kcfg/__init__.py rename to src/tests/integration/cterm/__init__.py diff --git a/src/tests/integration/kcfg/test_multiple_definitions.py b/src/tests/integration/cterm/test_multiple_definitions.py similarity index 61% rename from src/tests/integration/kcfg/test_multiple_definitions.py rename to src/tests/integration/cterm/test_multiple_definitions.py index e2de82cf1..85866ee4d 100644 --- a/src/tests/integration/kcfg/test_multiple_definitions.py +++ b/src/tests/integration/cterm/test_multiple_definitions.py @@ -7,20 +7,21 @@ from pyk.cterm import CTerm from pyk.kast.inner import KApply, KSequence, KVariable from pyk.prelude.ml import mlTop -from pyk.testing import KCFGExploreTest +from pyk.testing import CTermSymbolicTest, KPrintTest from ..utils import K_FILES if TYPE_CHECKING: from collections.abc import Iterable - from pyk.kcfg import KCFGExplore + from pyk.cterm import CTermSymbolic + from pyk.ktool.kprint import KPrint EXECUTE_TEST_DATA: Iterable[tuple[str]] = (('branch',),) -class TestMultipleDefinitionsProof(KCFGExploreTest): +class TestMultipleDefinitionsProof(CTermSymbolicTest, KPrintTest): KOMPILE_MAIN_FILE = K_FILES / 'multiple-definitions.k' @staticmethod @@ -41,13 +42,14 @@ def config() -> CTerm: ) def test_execute( self, - kcfg_explore: KCFGExplore, + kprint: KPrint, + cterm_symbolic: CTermSymbolic, test_id: str, ) -> None: - exec_res = kcfg_explore.cterm_execute(self.config(), depth=1) + exec_res = cterm_symbolic.execute(self.config(), depth=1) split_next_terms = exec_res.next_states - split_k = kcfg_explore.kprint.pretty_print(exec_res.state.cell('K_CELL')) - split_next_k = [kcfg_explore.kprint.pretty_print(exec_res.state.cell('K_CELL')) for _ in split_next_terms] + split_k = kprint.pretty_print(exec_res.state.cell('K_CELL')) + split_next_k = [kprint.pretty_print(exec_res.state.cell('K_CELL')) for _ in split_next_terms] assert exec_res.depth == 0 assert len(split_next_terms) == 2 @@ -57,10 +59,10 @@ def test_execute( 'a ( X:KItem )', ] == split_next_k - step_1_res = kcfg_explore.cterm_execute(split_next_terms[0], depth=1) - step_1_k = kcfg_explore.kprint.pretty_print(step_1_res.state.cell('K_CELL')) + step_1_res = cterm_symbolic.execute(split_next_terms[0], depth=1) + step_1_k = kprint.pretty_print(step_1_res.state.cell('K_CELL')) assert 'c' == step_1_k - step_2_res = kcfg_explore.cterm_execute(split_next_terms[1], depth=1) - step_2_k = kcfg_explore.kprint.pretty_print(step_2_res.state.cell('K_CELL')) + step_2_res = cterm_symbolic.execute(split_next_terms[1], depth=1) + step_2_k = kprint.pretty_print(step_2_res.state.cell('K_CELL')) assert 'c' == step_2_k diff --git a/src/tests/integration/kcfg/test_simple.py b/src/tests/integration/cterm/test_simple.py similarity index 77% rename from src/tests/integration/kcfg/test_simple.py rename to src/tests/integration/cterm/test_simple.py index df185a5de..ddb350407 100644 --- a/src/tests/integration/kcfg/test_simple.py +++ b/src/tests/integration/cterm/test_simple.py @@ -8,7 +8,7 @@ from pyk.kast.inner import KApply, KSequence, KToken, KVariable from pyk.kast.manip import get_cell from pyk.prelude.ml import mlEqualsTrue, mlTop -from pyk.testing import KCFGExploreTest +from pyk.testing import CTermSymbolicTest, KPrintTest from ..utils import K_FILES @@ -16,7 +16,7 @@ from collections.abc import Iterable from typing import Final, Union - from pyk.kcfg import KCFGExplore + from pyk.cterm import CTermSymbolic from pyk.ktool.kprint import KPrint STATE = Union[tuple[str, str], tuple[str, str, str]] @@ -37,7 +37,7 @@ SIMPLIFY_TEST_DATA: Final = (('bytes-return', ('mybytes', '.Map'), (r'b"\x00\x90\xa0\n\xa1\xf1a"', '.Map')),) -class TestSimpleProof(KCFGExploreTest): +class TestSimpleProof(CTermSymbolicTest, KPrintTest): KOMPILE_MAIN_FILE = K_FILES / 'simple-proofs.k' @staticmethod @@ -66,7 +66,8 @@ def config(kprint: KPrint, k: str, state: str, constraint: str | None = None) -> ) def test_execute( self, - kcfg_explore: KCFGExplore, + cterm_symbolic: CTermSymbolic, + kprint: KPrint, test_id: str, depth: int, pre: tuple[str, str], @@ -78,14 +79,14 @@ def test_execute( expected_k, expected_state, *_ = expected_post # When - exec_res = kcfg_explore.cterm_execute(self.config(kcfg_explore.kprint, *pre), depth=depth) - actual_k = kcfg_explore.kprint.pretty_print(exec_res.state.cell('K_CELL')) - actual_state = kcfg_explore.kprint.pretty_print(exec_res.state.cell('STATE_CELL')) + exec_res = cterm_symbolic.execute(self.config(kprint, *pre), depth=depth) + actual_k = kprint.pretty_print(exec_res.state.cell('K_CELL')) + actual_state = kprint.pretty_print(exec_res.state.cell('STATE_CELL')) actual_depth = exec_res.depth actual_next_states = [ ( - kcfg_explore.kprint.pretty_print(s.cell('K_CELL')), - kcfg_explore.kprint.pretty_print(s.cell('STATE_CELL')), + kprint.pretty_print(s.cell('K_CELL')), + kprint.pretty_print(s.cell('STATE_CELL')), ) for s in exec_res.next_states ] @@ -103,7 +104,8 @@ def test_execute( ) def test_simplify( self, - kcfg_explore: KCFGExplore, + cterm_symbolic: CTermSymbolic, + kprint: KPrint, test_id: str, pre: tuple[str, str], expected_post: tuple[str, str], @@ -113,9 +115,9 @@ def test_simplify( expected_k, expected_state, *_ = expected_post # When - actual_post, _logs = kcfg_explore.cterm_simplify(self.config(kcfg_explore.kprint, *pre)) - actual_k = kcfg_explore.kprint.pretty_print(get_cell(actual_post.kast, 'K_CELL')) - actual_state = kcfg_explore.kprint.pretty_print(get_cell(actual_post.kast, 'STATE_CELL')) + actual_post, _logs = cterm_symbolic.simplify(self.config(kprint, *pre)) + actual_k = kprint.pretty_print(get_cell(actual_post.kast, 'K_CELL')) + actual_state = kprint.pretty_print(get_cell(actual_post.kast, 'STATE_CELL')) # Then assert actual_k == expected_k diff --git a/src/tests/integration/proof/test_cell_map.py b/src/tests/integration/proof/test_cell_map.py index 92df353a7..c66326d1c 100644 --- a/src/tests/integration/proof/test_cell_map.py +++ b/src/tests/integration/proof/test_cell_map.py @@ -104,7 +104,9 @@ def test_execute( expected_k, _, _ = expected_post # When - exec_res = kcfg_explore.cterm_execute(self.config(kcfg_explore.kprint, k, aacounts, accounts), depth=depth) + exec_res = kcfg_explore.cterm_symbolic.execute( + self.config(kcfg_explore.kprint, k, aacounts, accounts), depth=depth + ) actual_k = kcfg_explore.kprint.pretty_print(exec_res.state.cell('K_CELL')) actual_depth = exec_res.depth @@ -134,7 +136,7 @@ def test_all_path_reachability_prove( proof = APRProof.from_claim(kprove.definition, claim, logs={}) init = proof.kcfg.node(proof.init) - new_init_term = kcfg_explore.cterm_assume_defined(init.cterm) + new_init_term = kcfg_explore.cterm_symbolic.assume_defined(init.cterm) proof.kcfg.replace_node(init.id, new_init_term) prover = APRProver(proof, kcfg_explore=kcfg_explore, execute_depth=max_depth) prover.advance_proof(max_iterations=max_iterations) diff --git a/src/tests/integration/proof/test_imp.py b/src/tests/integration/proof/test_imp.py index ced4e1be7..d2597b460 100644 --- a/src/tests/integration/proof/test_imp.py +++ b/src/tests/integration/proof/test_imp.py @@ -781,7 +781,7 @@ def test_execute( expected_k, expected_state = expected_post # When - exec_res = kcfg_explore.cterm_execute(self.config(kcfg_explore.kprint, k, state), depth=depth) + exec_res = kcfg_explore.cterm_symbolic.execute(self.config(kcfg_explore.kprint, k, state), depth=depth) actual_k = kcfg_explore.kprint.pretty_print(exec_res.state.cell('K_CELL')) actual_state = kcfg_explore.kprint.pretty_print(exec_res.state.cell('STATE_CELL')) actual_depth = exec_res.depth @@ -816,7 +816,7 @@ def test_get_model( cterm_term = self.config(kcfg_explore.kprint, *cterm) # When - actual = kcfg_explore.cterm_get_model(cterm_term) + actual = kcfg_explore.cterm_symbolic.get_model(cterm_term) # Then assert actual == expected @@ -842,7 +842,7 @@ def test_implies( consequent_term = self.config(kcfg_explore.kprint, *consequent) # When - actual = kcfg_explore.cterm_implies(antecedent_term, consequent_term) + actual = kcfg_explore.cterm_symbolic.implies(antecedent_term, consequent_term) # Then assert actual == expected @@ -861,7 +861,7 @@ def test_assume_defined( expected = config.add_constraint(constraint) # When - actual = kcfg_explore.cterm_assume_defined(config) + actual = kcfg_explore.cterm_symbolic.assume_defined(config) # Then assert actual == expected diff --git a/src/tests/integration/proof/test_mini_kevm.py b/src/tests/integration/proof/test_mini_kevm.py index 2bc81e71a..c1c39ec85 100644 --- a/src/tests/integration/proof/test_mini_kevm.py +++ b/src/tests/integration/proof/test_mini_kevm.py @@ -86,7 +86,7 @@ def test_all_path_reachability_prove( proof_dir=proof_dir, ) - new_init_cterm = kcfg_explore.cterm_assume_defined(proof.kcfg.node(proof.init).cterm) + new_init_cterm = kcfg_explore.cterm_symbolic.assume_defined(proof.kcfg.node(proof.init).cterm) proof.kcfg.replace_node(proof.init, new_init_cterm) kcfg_explore.simplify(proof.kcfg, {})