From 6088913e1d25bf9d08f0e4e5ad9d8e3ede655398 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 12 Jun 2024 07:42:09 -0600 Subject: [PATCH 1/3] Allow specifying that an APRProof generated lemmas should be direct (#4427) Currently, when we are generating lemmas from subproofs to be included in superproofs, we include each basic block of execution of the subproof directly as a rule for execution during the superproof. This means that we mirror the branching structure of the subproof directly, and aren't able to reduce the branching factor. However, when writing proofs that involve loop invariants or branching as `KClaim`, the user often provides the _exact_ final state that matters, even if it's reached in multiple different ways on different branches. For example, in the MCD proof suite, the `Vat.frob` proof: https://github.com/runtimeverification/evm-semantics/blob/20a292412797498f9eb70486aef19cd2f99cd9f2/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k#L7 End up reusing several of the `Vat.` arithmetic proofs, like `Vat.muluu` several times: https://github.com/runtimeverification/evm-semantics/blob/20a292412797498f9eb70486aef19cd2f99cd9f2/tests/specs/mcd/vat-frob-diff-zero-dart-pass-rough-spec.k#L288 If this subproof is included directly as its basic blocks as learned lemmas, then we arrive to a situation where we aren't actually reducing the branching factor in the superproof, even though the `Vat.muluu` specification already describes exactly the behavior that happens on all 3 branches of that proofs. This PR introduces an `direct_subproof_rules: bool = True` field to the `APRProver` class, so the user can specify whether they want this behavior or not. - A few logging messages are added to `APRProver.advance_proof` to help with debugging proofs that fail early. - The lemma generation process is handled more directly in `APRProof.as_rules`, instead of in `APRProve.init_proof`, which now can just call `APRProof.as_rules` directly without any extra processing of the results or deciding how to turn it into lemmas. - The field `direct_subproof_rules` is added to the `APRProver` class. - When building lemmas in `APRProver.init_proof`, we use the field `direct_subproof_rules` to determine how to build lemmas from subproofs. - The `APRProof.as_rules` changes its behavior on whether `direct_rule` is set or not. If `direct_subproof_rules` is set and the proof is passing, instead of building the lemmas as the basic blocks in the KCFG, we build it directly from the initial node to the target node of the KCFG. This improves the performance of the KEVM MCD Vat Proof suite dramatically in [this PR](https://github.com/runtimeverification/evm-semantics/pull/2467): ``` spec | original time | new time VAT-ADDUI-FAIL-ROUGH-SPEC.Vat.addui.fail.rough | 38.32540s | 38.8101s VAT-ARITHMETIC-SPEC.Vat.adduu.pass | 21.32606s | 20.8181s VAT-ARITHMETIC-SPEC.Vat.mului.pass | 72.18441s | 71.2940s VAT-ARITHMETIC-SPEC.Vat.muluu.pass | 84.01074s | 68.8481s VAT-ARITHMETIC-SPEC.Vat.subui.pass | 104.4093s | 105.154s VAT-ARITHMETIC-SPEC.Vat.subuu.pass | 20.32957s | 21.4818s VAT-DAI-PASS-SPEC.Vat.dai.pass | 10.81132s | 10.5747s VAT-DENY-DIFF-FAIL-ROUGH-SPEC.Vat.deny-diff.fail.rough | 58.88762s | 55.3194s VAT-FLUX-DIFF-PASS-ROUGH-SPEC.Vat.flux-diff.pass.rough | 45.90303s | 45.7166s VAT-FLUX-DIFF-PASS-SPEC.Vat.flux-diff.pass | 46.53391s | 44.7944s VAT-FOLD-PASS-ROUGH-SPEC.Vat.fold.pass.rough | 380.6935s | 107.786s VAT-FORK-DIFF-PASS-ROUGH-SPEC.Vat.fork-diff.pass.rough | 10961.03s | 466.333s VAT-FROB-DIFF-ZERO-DART-PASS-ROUGH-SPEC.Vat.frob-diff-zero-dart.pass.rough | 4382.788s | 992.793s VAT-HEAL-PASS-SPEC.Vat.heal.pass | 34.03113s | 28.5053s VAT-MOVE-DIFF-ROUGH-SPEC.Vat.move-diff.pass.rough | 38.68574s | 40.4618s VAT-SIN-PASS-SPEC.Vat.sin.pass | 10.80752s | 10.5180s VAT-SUBUI-FAIL-ROUGH-SPEC.Vat.subui.fail.rough | 35.38427s | 36.0153s ``` --- pyk/src/pyk/proof/proof.py | 6 ++++-- pyk/src/pyk/proof/reachability.py | 23 ++++++++++++++--------- 2 files changed, 18 insertions(+), 11 deletions(-) diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index f8600ed09ec..0736da51a6e 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -484,10 +484,12 @@ def advance_proof(self, proof: P, max_iterations: int | None = None, fail_fast: still available steps """ iterations = 0 + _LOGGER.info(f'Initializing proof: {proof.id}') self.init_proof(proof) while True: - steps = proof.get_steps() - if len(list(steps)) == 0: + steps = list(proof.get_steps()) + _LOGGER.info(f'Found {len(steps)} next steps for proof: {proof.id}') + if len(steps) == 0: break for step in steps: if fail_fast and proof.failed: diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index a9dfd583c13..d9c0872623c 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -27,7 +27,7 @@ from pathlib import Path from typing import Any, Final, TypeVar - from ..kast.outer import KClaim, KDefinition, KFlatModuleList, KRuleLike + from ..kast.outer import KClaim, KDefinition, KFlatModuleList from ..kcfg import KCFGExplore from ..kcfg.explore import KCFGExtendResult from ..kcfg.kcfg import CSubst, NodeIdLike @@ -383,7 +383,9 @@ def from_claim( **kwargs, ) - def as_rules(self, priority: int = 20) -> list[KRule]: + 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)): + 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) @@ -680,6 +682,7 @@ class APRProver(Prover[APRProof, APRProofStep, APRProofResult]): counterexample_info: bool always_check_subsumption: bool fast_check_subsumption: bool + direct_subproof_rules: bool kcfg_explore: KCFGExplore def __init__( @@ -691,6 +694,7 @@ def __init__( counterexample_info: bool = False, always_check_subsumption: bool = True, fast_check_subsumption: bool = False, + direct_subproof_rules: bool = False, ) -> None: self.kcfg_explore = kcfg_explore @@ -701,12 +705,13 @@ def __init__( self.counterexample_info = counterexample_info self.always_check_subsumption = always_check_subsumption self.fast_check_subsumption = fast_check_subsumption + self.direct_subproof_rules = direct_subproof_rules def close(self) -> None: self.kcfg_explore.cterm_symbolic._kore_client.close() def init_proof(self, proof: APRProof) -> None: - def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike]) -> None: + def _inject_module(module_name: str, import_name: str, sentences: list[KRule]) -> None: _module = KFlatModule(module_name, sentences, [KImport(import_name)]) _kore_module = kflatmodule_to_kore(self.kcfg_explore.cterm_symbolic._definition, _module) self.kcfg_explore.cterm_symbolic._kore_client.add_module(_kore_module, name_as_id=True) @@ -716,12 +721,12 @@ def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike if proof.proof_dir is not None else [] ) - - dependencies_as_rules: list[KRuleLike] = [] - for apr_subproof in [pf for pf in subproofs if isinstance(pf, APRProof)]: - dependencies_as_rules.extend(apr_subproof.as_rules(priority=20)) - if apr_subproof.admitted and len(apr_subproof.kcfg.predecessors(apr_subproof.target)) == 0: - dependencies_as_rules.append(apr_subproof.as_rule(priority=20)) + dependencies_as_rules = [ + rule + for subproof in subproofs + if isinstance(subproof, APRProof) + for rule in subproof.as_rules(priority=20, direct_rule=self.direct_subproof_rules) + ] circularity_rule = proof.as_rule(priority=20) _inject_module(proof.dependencies_module_name, self.main_module_name, dependencies_as_rules) From c1ef5ac07ac06542699eb1bb339931fc739544c1 Mon Sep 17 00:00:00 2001 From: Bruce Collie Date: Wed, 12 Jun 2024 16:02:22 +0100 Subject: [PATCH 2/3] Allow a longer time for Pyk documentation builds (#4440) Now that we're building a Docker environment for this job, it can hit its time limit of 10 minutes easily: https://github.com/runtimeverification/k/actions/runs/9481407834/job/26125129742 --- .github/workflows/release.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index d6b36a1ffc8..028cf56bfda 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -424,7 +424,7 @@ jobs: name: 'Build Pyk Documentation' needs: ubuntu-jammy runs-on: [self-hosted, linux, normal] - timeout-minutes: 10 + timeout-minutes: 30 steps: - name: 'Check out code' uses: actions/checkout@v4 From 500067879253a62fa2796aff760165cdf5ecbb3d Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 12 Jun 2024 13:02:50 -0300 Subject: [PATCH 3/3] Adding new PyK wrappers to LLVM Python Bindings (#4426) This PR exposes the new infrastructure created by the LLVm Backend to parse the Hints file. We introduce the wrappers to make the streaming parser possible to use as a list of events and access it through an integrator. Or not loading all the events at the same time but accessing them one per time through the `next()` function. Depends on: https://github.com/runtimeverification/llvm-backend/pull/1090 --------- Co-authored-by: rv-jenkins --- pyk/docs/conf.py | 5 + pyk/src/pyk/kllvm/hints/prooftrace.py | 310 +++++++++++++++--- pyk/src/pyk/testing/_kompiler.py | 20 +- .../integration/kllvm/test_prooftrace.py | 103 +++++- 4 files changed, 373 insertions(+), 65 deletions(-) diff --git a/pyk/docs/conf.py b/pyk/docs/conf.py index be5e565f0ba..f1503a10cb0 100644 --- a/pyk/docs/conf.py +++ b/pyk/docs/conf.py @@ -17,6 +17,7 @@ extensions = [ 'sphinx.ext.autodoc', + 'sphinx.ext.napoleon', 'sphinx.ext.viewcode', ] templates_path = ['_templates'] @@ -26,6 +27,10 @@ autodoc_inherit_docstrings = False viewcode_line_numbers = True +napoleon_google_docstring = True +napoleon_include_init_with_doc = True +napoleon_include_special_with_doc = True + # -- Options for HTML output ------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#options-for-html-output diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py index 594eb8202ef..d0a02aabf5b 100644 --- a/pyk/src/pyk/kllvm/hints/prooftrace.py +++ b/pyk/src/pyk/kllvm/hints/prooftrace.py @@ -15,12 +15,18 @@ llvm_side_condition_end_event, llvm_side_condition_event, llvm_step_event, + annotated_llvm_event, + llvm_rewrite_trace_iterator, + EventType, ) from ..ast import Pattern # isort: on if TYPE_CHECKING: + from collections.abc import Generator + from pathlib import Path + from _kllvm.prooftrace import Argument @@ -38,7 +44,10 @@ class LLVMRewriteEvent(LLVMStepEvent): @property @abstractmethod def rule_ordinal(self) -> int: - """Returns the axiom ordinal number of the rewrite rule. The rule ordinal represents the `nth` axiom in the kore definition.""" + """Return the axiom ordinal number of the rewrite rule. + + The rule ordinal represents the `nth` axiom in the kore definition. + """ ... @property @@ -55,19 +64,24 @@ class LLVMRuleEvent(LLVMRewriteEvent): Attributes: _rule_event (llvm_rule_event): The underlying LLVM rule event. - - Methods: - __init__(self, rule_event: llvm_rule_event) -> None: Initializes a new instance of the LLVMRuleEvent class. - - __repr__(self) -> str: Returns a string representation of the LLVMRuleEvent object using the AST printing method. """ _rule_event: llvm_rule_event def __init__(self, rule_event: llvm_rule_event) -> None: + """ + Initializes a new instance of the LLVMRuleEvent class. + + Args: + rule_event (llvm_rule_event): The LLVM rule event object. + """ self._rule_event = rule_event def __repr__(self) -> str: + """ + Returns: + A string representation of the LLVMRuleEvent object using the AST printing method. + """ return self._rule_event.__repr__() @property @@ -84,23 +98,30 @@ def substitution(self) -> dict[str, Pattern]: @final class LLVMSideConditionEventEnter(LLVMRewriteEvent): """ - Represents an event that enters a side condition in LLVM rewriting. This event is used to check the side condition of a rule. Mostly used in ensures/requires clauses. + Represents an event that enters a side condition in LLVM rewriting. + + This event is used to check the side condition of a rule. Mostly used in ensures/requires clauses. Attributes: _side_condition_event (llvm_side_condition_event): The underlying side condition event. - - Methods: - __init__(self, side_condition_event: llvm_side_condition_event) -> None: Initializes a new instance of the LLVMSideConditionEventEnter class. - - __repr__(self) -> str: Returns a string representation of the LLVMSideConditionEventEnter object using the AST printing method. """ _side_condition_event: llvm_side_condition_event def __init__(self, side_condition_event: llvm_side_condition_event) -> None: + """ + Initializes a new instance of the LLVMSideConditionEventEnter class. + + Args: + side_condition_event (llvm_side_condition_event): The LLVM side condition event object. + """ self._side_condition_event = side_condition_event def __repr__(self) -> str: + """ + Returns: + A string representation of the LLVMSideConditionEventEnter object using the AST printing method. + """ return self._side_condition_event.__repr__() @property @@ -117,23 +138,30 @@ def substitution(self) -> dict[str, Pattern]: @final class LLVMSideConditionEventExit(LLVMStepEvent): """ - Represents an LLVM side condition event indicating the exit of a side condition. This event contains the result of the side condition evaluation. + Represents an LLVM side condition event indicating the exit of a side condition. + + This event contains the result of the side condition evaluation. Attributes: _side_condition_end_event (llvm_side_condition_end_event): The underlying side condition end event. - - Methods: - __init__(side_condition_end_event: llvm_side_condition_end_event) -> None: Initializes the LLVMSideConditionEventExit instance. - - __repr__(self) -> str: Returns a string representation of the LLVMSideConditionEventExit instance using the AST printing method. """ _side_condition_end_event: llvm_side_condition_end_event def __init__(self, side_condition_end_event: llvm_side_condition_end_event) -> None: + """ + Initializes a new instance of the LLVMSideConditionEventExit class. + + Args: + side_condition_end_event (llvm_side_condition_end_event): The LLVM side condition end event object. + """ self._side_condition_end_event = side_condition_end_event def __repr__(self) -> str: + """ + Returns: + A string representation of the LLVMSideConditionEventExit object using the AST printing method. + """ return self._side_condition_end_event.__repr__() @property @@ -154,19 +182,24 @@ class LLVMFunctionEvent(LLVMStepEvent): Attributes: _function_event (llvm_function_event): The underlying LLVM function event object. - - Methods: - __init__(self, function_event: llvm_function_event) -> None: Initializes a new instance of the LLVMFunctionEvent class. - - __repr__(self) -> str: Returns a string representation of the LLVMFunctionEvent object using the AST printing method. """ _function_event: llvm_function_event def __init__(self, function_event: llvm_function_event) -> None: + """ + Initializes a new instance of the LLVMFunctionEvent class. + + Args: + function_event (llvm_function_event): The LLVM function event object. + """ self._function_event = function_event def __repr__(self) -> str: + """ + Returns: + A string representation of the LLVMFunctionEvent object using the AST printing method. + """ return self._function_event.__repr__() @property @@ -192,19 +225,24 @@ class LLVMHookEvent(LLVMStepEvent): Attributes: _hook_event (llvm_hook_event): The underlying hook event object. - - Methods: - __init__(hook_event: llvm_hook_event): Initializes a new instance of the LLVMHookEvent class. - - __repr__() -> str: Returns a string representation of the LLVMHookEvent object using the AST printing method. """ _hook_event: llvm_hook_event def __init__(self, hook_event: llvm_hook_event) -> None: + """ + Initializes a new instance of the LLVMHookEvent class. + + Args: + hook_event (llvm_hook_event): The LLVM hook event object. + """ self._hook_event = hook_event def __repr__(self) -> str: + """ + Returns: + A string representation of the LLVMHookEvent object using the AST printing method. + """ return self._hook_event.__repr__() @property @@ -234,20 +272,26 @@ class LLVMArgument: Represents an LLVM argument. Attributes: - _argument (Argument): The underlying Argument object. An argument is a wrapper object containing either a step event or a KORE pattern. - - Methods: - __init__(self, argument: Argument) -> None: Initializes the LLVMArgument object. - - __repr__(self) -> str: Returns a string representation of the LLVMArgument object using the AST printing method. + _argument (Argument): The underlying Argument object. An argument is a wrapper object containing either a step + event or a KORE pattern. """ _argument: Argument def __init__(self, argument: Argument) -> None: + """ + Initializes the LLVMArgument object. + + Args: + argument (Argument): The Argument object. + """ self._argument = argument def __repr__(self) -> str: + """ + Returns: + Returns a string representation of the LLVMArgument object using the AST printing method. + """ return self._argument.__repr__() @property @@ -288,41 +332,217 @@ class LLVMRewriteTrace: Attributes: _rewrite_trace (llvm_rewrite_trace): The underlying LLVM rewrite trace object. - - Methods: - __init__(self, rewrite_trace: llvm_rewrite_trace) -> None: Initializes a new instance of the LLVMRewriteTrace class. - __repr__(self) -> str: Returns a string representation of the LLVMRewriteTrace object using the AST printing method. - version(self) -> int: Returns the version of the HINTS formart. - pre_trace(self) -> list[LLVMArgument]: Returns the pre-trace events as a list of LLVMArgument objects. - initial_config(self) -> LLVMArgument: Returns the initial configuration as an LLVMArgument object. - trace(self) -> list[LLVMArgument]: Returns the trace events as a list of LLVMArgument objects. - parse(trace: bytes, header: kore_header) -> LLVMRewriteTrace: Parses the given proof hints byte string using the given kore_header object to create an LLVMRewriteTrace object. """ _rewrite_trace: llvm_rewrite_trace def __init__(self, rewrite_trace: llvm_rewrite_trace) -> None: + """ + Initializes a new instance of the LLVMRewriteTrace class. + + Args: + rewrite_trace (llvm_rewrite_trace): The LLVM rewrite trace object. + """ self._rewrite_trace = rewrite_trace def __repr__(self) -> str: + """ + Returns: + A string representation of the LLVMRewriteTrace object using the AST printing method. + """ return self._rewrite_trace.__repr__() @property def version(self) -> int: + """Returns the version of the binary hints format used by this trace.""" return self._rewrite_trace.version @property def pre_trace(self) -> list[LLVMArgument]: + """Returns a list of events that occurred before the initial configuration was constructed.""" return [LLVMArgument(event) for event in self._rewrite_trace.pre_trace] @property def initial_config(self) -> LLVMArgument: + """Returns the initial configuration as an LLVMArgument object.""" return LLVMArgument(self._rewrite_trace.initial_config) @property def trace(self) -> list[LLVMArgument]: + """Returns a list of events that occurred after the initial configurarion was constructed until the end of the + proof trace when the final configuration is reached.""" return [LLVMArgument(event) for event in self._rewrite_trace.trace] @staticmethod - def parse(trace: bytes, header: kore_header) -> LLVMRewriteTrace: - return LLVMRewriteTrace(llvm_rewrite_trace.parse(trace, header)) + def parse(trace: bytes, header: KoreHeader) -> LLVMRewriteTrace: + """Parses the given proof hints byte string using the given kore_header object to create an LLVMRewriteTrace + object.""" + return LLVMRewriteTrace(llvm_rewrite_trace.parse(trace, header._kore_header)) + + +class KoreHeader: + """ + Represents the Kore header, a file that contains the version of the Binary KORE used to serialize/deserialize the + Proof Trace and all the aditional information needed make this process faster the Proof Trace. + + Attributes: + _kore_header (kore_header): The underlying KORE Header object. + """ + + _kore_header: kore_header + + def __init__(self, kore_header: kore_header) -> None: + """ + Initializes a new instance of the KoreHeader class. + + Args: + kore_header (kore_header): The KORE Header object. + """ + self._kore_header = kore_header + + @staticmethod + def create(header_path: Path) -> KoreHeader: + """Creates a new KoreHeader object from the given header file path.""" + return KoreHeader(kore_header(str(header_path))) + + +class LLVMEventType: + """ + Represents an LLVM event type. This works as a wrapper around the EventType enum. + + It also provides properties to check the type of the event. + + Attributes: + _event_type (EventType): The underlying EventType object. + """ + + _event_type: EventType + + def __init__(self, event_type: EventType) -> None: + """ + Initializes a new instance of the LLVMEventType class. + + Args: + event_type (EventType): The EventType object. + """ + self._event_type = event_type + + @property + def is_pre_trace(self) -> bool: + """Checks if the event type is a pre-trace event.""" + return self._event_type == EventType.PreTrace + + @property + def is_initial_config(self) -> bool: + """Checks if the event type is an initial configuration event.""" + return self._event_type == EventType.InitialConfig + + @property + def is_trace(self) -> bool: + """Checks if the event type is a trace event.""" + return self._event_type == EventType.Trace + + +class LLVMEventAnnotated: + """ + Represents an annotated LLVM event. + + This class is used to wrap an llvm_event and its corresponding event type. + This class is used to iterate over the LLVM rewrite trace events. + + Attributes: + _annotated_llvm_event (annotated_llvm_event): The underlying annotated LLVM event object. + """ + + _annotated_llvm_event: annotated_llvm_event + + def __init__(self, annotated_llvm_event: annotated_llvm_event) -> None: + """Initializes a new instance of the LLVMEventAnnotated class. + + Args: + annotated_llvm_event (annotated_llvm_event): The annotated LLVM event object. + """ + self._annotated_llvm_event = annotated_llvm_event + + @property + def type(self) -> LLVMEventType: + """Returns the LLVM event type.""" + return LLVMEventType(self._annotated_llvm_event.type) + + @property + def event(self) -> LLVMArgument: + """Returns the LLVM event as an LLVMArgument object.""" + return LLVMArgument(self._annotated_llvm_event.event) + + +class LLVMRewriteTraceIterator: + """ + Represents an LLVM rewrite trace iterator. + + This class is used to iterate over the LLVM rewrite trace events in the stream parser. + + Attributes: + _rewrite_trace_iterator (llvm_rewrite_trace_iterator): The underlying LLVM rewrite trace iterator object. + """ + + _rewrite_trace_iterator: llvm_rewrite_trace_iterator + + def __init__(self, rewrite_trace_iterator: llvm_rewrite_trace_iterator) -> None: + """ + Initializes a new instance of the LLVMRewriteTraceIterator class. + + Args: + rewrite_trace_iterator (llvm_rewrite_trace_iterator): The LLVM rewrite trace iterator object. + """ + self._rewrite_trace_iterator = rewrite_trace_iterator + + def __repr__(self) -> str: + """ + Returns: + A string representation of the LLVMRewriteTraceIterator object using the AST printing method. + """ + return self._rewrite_trace_iterator.__repr__() + + def __iter__(self) -> Generator[LLVMEventAnnotated, None, None]: + """Yields LLVMEventAnnotated options. + + This method is an iterator that yields LLVMEventAnnotated options. + It iterates over the events in the trace and returns the next event as an LLVMEventAnnotated object. + + Yields: + LLVMEventAnnotated: The next LLVMEventAnnotated option. + + Raises: + None + """ + while True: + next_event = self._rewrite_trace_iterator.get_next_event() + if next_event is None: + return + else: + yield LLVMEventAnnotated(next_event) + + def __next__(self) -> LLVMEventAnnotated: + """Yields the next LLVMEventAnnotated object from the iterator. + + Returns: + LLVMEventAnnotated: The next LLVMEventAnnotated object. + + Raises: + StopIteration: If there are no more events in the iterator. + """ + next_event = self._rewrite_trace_iterator.get_next_event() + if next_event is not None: + return LLVMEventAnnotated(next_event) + else: + raise StopIteration + + @property + def version(self) -> int: + """Returns the version of the HINTS format.""" + return self._rewrite_trace_iterator.version + + @staticmethod + def from_file(trace_path: Path, header: KoreHeader) -> LLVMRewriteTraceIterator: + """Creates a new LLVMRewriteTraceIterator object from the given trace and header file paths.""" + return LLVMRewriteTraceIterator(llvm_rewrite_trace_iterator.from_file(str(trace_path), header._kore_header)) diff --git a/pyk/src/pyk/testing/_kompiler.py b/pyk/src/pyk/testing/_kompiler.py index 013e25fdd9c..af7f4ed26ab 100644 --- a/pyk/src/pyk/testing/_kompiler.py +++ b/pyk/src/pyk/testing/_kompiler.py @@ -33,7 +33,7 @@ from ..kast.outer import KDefinition from ..kcfg.semantics import KCFGSemantics - from ..kllvm.hints.prooftrace import kore_header + from ..kllvm.hints.prooftrace import KoreHeader from ..kllvm.runtime import Runtime from ..ktool.kprint import SymbolTable from ..utils import BugReport @@ -371,15 +371,16 @@ def hints(self, definition_dir: Path, kompile: Kompiler) -> bytes: return hints_file.read_bytes() @pytest.fixture(scope='class') - def header(self, definition_dir: Path) -> kore_header: + def header(self, definition_dir: Path) -> KoreHeader: process = subprocess.run(['kore-rich-header', str(definition_dir / 'definition.kore')], stdout=subprocess.PIPE) hdr = process.stdout - path = str(definition_dir / 'header.bin') - with open(path, 'wb') as f: + header_file_name = definition_dir.name + '.header' + path = definition_dir / header_file_name + with path.open('wb') as f: f.write(hdr) - from ..kllvm.hints.prooftrace import kore_header + from ..kllvm.hints.prooftrace import KoreHeader - return kore_header(path) + return KoreHeader.create(path) @pytest.fixture(scope='class') def definition_file(self, definition_dir: Path) -> str: @@ -387,3 +388,10 @@ def definition_file(self, definition_dir: Path) -> str: assert definition_path.is_file() with open(definition_path) as f: return f.read() + + @pytest.fixture(scope='class') + def hints_file(self, definition_dir: Path, kompile: Kompiler) -> Path: + input_kore_file = kompile._cache_definition(self.HINTS_INPUT_KORE) + hints_file_name = definition_dir.name.replace('.k', '.hints') + hints_file = generate_hints(definition_dir, input_kore_file, None, hints_file_name) + return hints_file diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py index 5f65c01690f..003860c9e30 100644 --- a/pyk/src/tests/integration/kllvm/test_prooftrace.py +++ b/pyk/src/tests/integration/kllvm/test_prooftrace.py @@ -1,5 +1,7 @@ from __future__ import annotations +from typing import TYPE_CHECKING + import pyk.kllvm.hints.prooftrace as prooftrace from pyk.kllvm.convert import llvm_to_pattern from pyk.kllvm.parser import parse_definition @@ -15,6 +17,9 @@ from pyk.kore.syntax import App from pyk.testing import ProofTraceTest +if TYPE_CHECKING: + from pathlib import Path + def get_pattern_from_ordinal(definition_text: list[str], ordinal: int) -> str: axiom_ordinal = 'ordinal{}("' + str(ordinal) + '")' @@ -48,7 +53,13 @@ class TestProofTrace(ProofTraceTest): ) ).text - def test_proof_trace(self, hints: bytes, header: prooftrace.kore_header, definition_file: str) -> None: + def get_pattern_from_ordinal(self, definition_text: list[str], ordinal: int) -> str: + axiom_ordinal = 'ordinal{}("' + str(ordinal) + '")' + line = next((i + 1 for i, l in enumerate(definition_text) if axiom_ordinal in l), None) + assert line is not None + return definition_text[line - 1].strip() + + def test_proof_trace(self, hints: bytes, header: prooftrace.KoreHeader, definition_file: str) -> None: definition = parse_definition(definition_file) assert definition is not None @@ -83,6 +94,72 @@ def test_proof_trace(self, hints: bytes, header: prooftrace.kore_header, definit # check that the third event is a configuration assert pt.trace[2].is_kore_pattern() + def test_streaming_parser_iter(self, header: prooftrace.KoreHeader, hints_file: Path) -> None: + # read the hints file and get the iterator for the proof trace + it = prooftrace.LLVMRewriteTraceIterator.from_file(hints_file, header) + assert it.version == 11 + + # Test that the __iter__ is working + list_of_events = list(it) + + # Test length of the list + assert len(list_of_events) == 13 + + # Test the type of the events + for event in list_of_events: + if event.type.is_pre_trace: + continue + elif event.type.is_initial_config: + assert event.event.is_kore_pattern() + elif event.type.is_trace: + if event.event.is_step_event(): + assert isinstance(event.event.step_event, prooftrace.LLVMRewriteEvent) + else: + assert event.event.is_kore_pattern() + + def test_streaming_parser_next(self, header: prooftrace.KoreHeader, hints_file: Path, definition_file: str) -> None: + definition = parse_definition(definition_file) + assert definition is not None + + definition.preprocess() + definition_text = repr(definition).split('\n') + + # read the hints file and get the iterator for the proof trace + it = prooftrace.LLVMRewriteTraceIterator.from_file(hints_file, header) + assert it.version == 11 + + # skip pre-trace events + while True: + event0 = next(it) + if event0 is None or not event0.type.is_pre_trace: + break + + # check that the first event is the initial configuration + assert event0.type.is_initial_config + assert event0.event.is_kore_pattern() + + # check that the first event is the rewrite a() => b() + event1 = next(it) + assert event1.event.is_step_event() + assert isinstance(event1.event.step_event, prooftrace.LLVMRewriteEvent) + axiom_ordinal = event1.event.step_event.rule_ordinal + axiom = repr(definition.get_axiom_by_ordinal(axiom_ordinal)) + axiom_expected = self.get_pattern_from_ordinal(definition_text, axiom_ordinal) + assert axiom == axiom_expected + + # check that the second event is the rewrite b() => c() + event2 = next(it) + assert event2.event.is_step_event() + assert isinstance(event2.event.step_event, prooftrace.LLVMRewriteEvent) + axiom_ordinal = event2.event.step_event.rule_ordinal + axiom = repr(definition.get_axiom_by_ordinal(axiom_ordinal)) + axiom_expected = self.get_pattern_from_ordinal(definition_text, axiom_ordinal) + assert axiom == axiom_expected + + event3 = next(it) + assert event3.type.is_trace + assert event3.event.is_kore_pattern() + class TestSingleRewrite(ProofTraceTest): KOMPILE_DEFINITION = """ @@ -101,7 +178,7 @@ class TestSingleRewrite(ProofTraceTest): HINTS_INPUT_KORE = """LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortFoo{}, SortKItem{}}(LblFooA'LParRParUnds'SINGLE-REWRITE-SYNTAX'Unds'Foo{}()))))""" def test_parse_proof_hint_single_rewrite( - self, hints: bytes, header: prooftrace.kore_header, definition_file: str + self, hints: bytes, header: prooftrace.KoreHeader, definition_file: str ) -> None: definition = parse_definition(definition_file) assert definition is not None @@ -171,7 +248,7 @@ class TestTreeReverse(ProofTraceTest): """ def test_parse_proof_hint_reverse_no_ints( - self, hints: bytes, header: prooftrace.kore_header, definition_file: str + self, hints: bytes, header: prooftrace.KoreHeader, definition_file: str ) -> None: definition = parse_definition(definition_file) assert definition is not None @@ -296,7 +373,7 @@ class TestNonRecFunction(ProofTraceTest): """ def test_parse_proof_hint_non_rec_function( - self, hints: bytes, header: prooftrace.kore_header, definition_file: str + self, hints: bytes, header: prooftrace.KoreHeader, definition_file: str ) -> None: definition = parse_definition(definition_file) assert definition is not None @@ -375,7 +452,7 @@ class TestDV(ProofTraceTest): LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortFoo{}, SortKItem{}}(Lblsucc'LParUndsRParUnds'DV'Unds'Foo'Unds'Foo{}(Lblfoo'LParUndsRParUnds'DV'Unds'Foo'Unds'Int{}(\\dv{SortInt{}}("5"))))))) """ - def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.kore_header, definition_file: str) -> None: + def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.KoreHeader, definition_file: str) -> None: definition = parse_definition(definition_file) assert definition is not None @@ -460,9 +537,7 @@ class TestConcurrentCounters(ProofTraceTest): LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortState{}, SortKItem{}}(Lblstate'LParUndsCommUndsRParUnds'CONCURRENT-COUNTERS-SYNTAX'Unds'State'Unds'Int'Unds'Int{}(\\dv{SortInt{}}("4"),\\dv{SortInt{}}("0")))))) """ - def test_parse_concurrent_counters( - self, hints: bytes, header: prooftrace.kore_header, definition_file: str - ) -> None: + def test_parse_concurrent_counters(self, hints: bytes, header: prooftrace.KoreHeader, definition_file: str) -> None: # main purpose of the test is to check the sequence of events in the trace with # successful and failed side condition checks definition = parse_definition(definition_file) @@ -630,7 +705,7 @@ class Test0Decrement(ProofTraceTest): LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortNat{}, SortKItem{}}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())))) """ - def test_parse_proof_hint_0_decrement(self, hints: bytes, header: prooftrace.kore_header) -> None: + def test_parse_proof_hint_0_decrement(self, hints: bytes, header: prooftrace.KoreHeader) -> None: pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None @@ -659,7 +734,7 @@ class Test1Decrement(ProofTraceTest): LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortNat{}, SortKItem{}}(Lbls'LParUndsRParUnds'DECREMENT-SYNTAX'Unds'Nat'Unds'Nat{}(Lbl1'Unds'DECREMENT-SYNTAX'Unds'Nat{}()))))) """ - def test_parse_proof_hint_1_decrement(self, hints: bytes, header: prooftrace.kore_header) -> None: + def test_parse_proof_hint_1_decrement(self, hints: bytes, header: prooftrace.KoreHeader) -> None: pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None @@ -688,7 +763,7 @@ class Test2Decrement(ProofTraceTest): LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortNat{}, SortKItem{}}(Lbls'LParUndsRParUnds'DECREMENT-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'DECREMENT-SYNTAX'Unds'Nat'Unds'Nat{}(Lbl2'Unds'DECREMENT-SYNTAX'Unds'Nat{}())))))) """ - def test_parse_proof_hint_2_decrement(self, hints: bytes, header: prooftrace.kore_header) -> None: + def test_parse_proof_hint_2_decrement(self, hints: bytes, header: prooftrace.KoreHeader) -> None: pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None @@ -727,7 +802,7 @@ class TestPeano(ProofTraceTest): """ - def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.kore_header) -> None: + def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeader) -> None: pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None @@ -831,7 +906,7 @@ class TestIMP5(ProofTraceTest): LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortPgm{}, SortKItem{}}(inj{SortBlock{}, SortPgm{}}(Lbl'LBraRBraUnds'IMP5-SYNTAX'Unds'Block{}()))))) """ - def test_parse_proof_hint_imp5(self, hints: bytes, header: prooftrace.kore_header) -> None: + def test_parse_proof_hint_imp5(self, hints: bytes, header: prooftrace.KoreHeader) -> None: pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None @@ -863,7 +938,7 @@ class TestBuiltInHookEvents(ProofTraceTest): """ def test_parse_proof_hint_builtin_hook_events( - self, hints: bytes, header: prooftrace.kore_header, definition_file: str + self, hints: bytes, header: prooftrace.KoreHeader, definition_file: str ) -> None: definition = parse_definition(definition_file) assert definition is not None