From c4c27ffadef4bad83ebabf2576e09d389115984b Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Mon, 3 Jun 2024 13:27:21 -0300 Subject: [PATCH] Adding inline documentation to `prooftrace.py` (#4407) This is a simple PR that documents the prooftrace bindings classes and methods using docstrings. It also adds `__init__.py` to `pyk.kllvm.hints` so it gets recognized by `Sphinx` and hopefully published in https://runtimeverification.github.io/pyk/index.html --- pyk/src/pyk/kllvm/hints/__init__.py | 0 pyk/src/pyk/kllvm/hints/prooftrace.py | 121 +++++++++++++++++++++++++- 2 files changed, 118 insertions(+), 3 deletions(-) create mode 100644 pyk/src/pyk/kllvm/hints/__init__.py diff --git a/pyk/src/pyk/kllvm/hints/__init__.py b/pyk/src/pyk/kllvm/hints/__init__.py new file mode 100644 index 00000000000..e69de29bb2d diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py index 00660f8187c..594eb8202ef 100644 --- a/pyk/src/pyk/kllvm/hints/prooftrace.py +++ b/pyk/src/pyk/kllvm/hints/prooftrace.py @@ -25,21 +25,43 @@ class LLVMStepEvent(ABC): - pass + """ + Abstract base class representing an LLVM step event. + """ class LLVMRewriteEvent(LLVMStepEvent): + """ + Represents LLVM rewrite event. + """ + @property @abstractmethod - def rule_ordinal(self) -> int: ... + 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.""" + ... @property @abstractmethod - def substitution(self) -> dict[str, Pattern]: ... + def substitution(self) -> dict[str, Pattern]: + """Returns the substitution dictionary used to perform the rewrite represented by this event.""" + ... @final class LLVMRuleEvent(LLVMRewriteEvent): + """ + Represents an LLVM rule event. + + 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: @@ -50,15 +72,29 @@ def __repr__(self) -> str: @property def rule_ordinal(self) -> int: + """Returns the axiom ordinal number of the rule event.""" return self._rule_event.rule_ordinal @property def substitution(self) -> dict[str, Pattern]: + """Returns the substitution dictionary used to perform the rewrite represented by this rule event.""" return {k: v[0] for k, v in self._rule_event.substitution.items()} @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. + + 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: @@ -69,15 +105,29 @@ def __repr__(self) -> str: @property def rule_ordinal(self) -> int: + """Returns the axiom ordinal number associated with the side condition event.""" return self._side_condition_event.rule_ordinal @property def substitution(self) -> dict[str, Pattern]: + """Returns the substitution dictionary used to perform the rewrite represented by this side condition event.""" return {k: v[0] for k, v in self._side_condition_event.substitution.items()} @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. + + 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: @@ -88,15 +138,29 @@ def __repr__(self) -> str: @property def rule_ordinal(self) -> int: + """Returns the axiom ordinal number associated with the side condition event.""" return self._side_condition_end_event.rule_ordinal @property def check_result(self) -> bool: + """Returns the boolean result of the evaluation of the side condition that corresponds to this event.""" return self._side_condition_end_event.check_result @final class LLVMFunctionEvent(LLVMStepEvent): + """ + Represents an LLVM function event in a proof trace. + + 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: @@ -107,19 +171,34 @@ def __repr__(self) -> str: @property def name(self) -> str: + """Returns the name of the LLVM function as a KORE Symbol Name.""" return self._function_event.name @property def relative_position(self) -> str: + """Returns the relative position of the LLVM function event in the proof trace. Ex.: (0:0:0:0)""" return self._function_event.relative_position @property def args(self) -> list[LLVMArgument]: + """Returns a list of LLVMArgument objects representing the arguments of the LLVM function.""" return [LLVMArgument(arg) for arg in self._function_event.args] @final class LLVMHookEvent(LLVMStepEvent): + """ + Represents a hook event in LLVM execution. + + 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: @@ -130,23 +209,39 @@ def __repr__(self) -> str: @property def name(self) -> str: + """Returns the attribute name of the hook event. Ex.: "INT.add" """ return self._hook_event.name @property def relative_position(self) -> str: + """Returns the relative position of the hook event in the proof trace. Ex.: (0:0:0:0)""" return self._hook_event.relative_position @property def args(self) -> list[LLVMArgument]: + """Returns a list of LLVMArgument objects representing the arguments of the hook event.""" return [LLVMArgument(arg) for arg in self._hook_event.args] @property def result(self) -> Pattern: + """Returns the result pattern of the hook event evaluation.""" return self._hook_event.result @final 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 def __init__(self, argument: Argument) -> None: @@ -157,6 +252,7 @@ def __repr__(self) -> str: @property def step_event(self) -> LLVMStepEvent: + """Returns the LLVMStepEvent associated with the argument if any.""" if isinstance(self._argument.step_event, llvm_rule_event): return LLVMRuleEvent(self._argument.step_event) elif isinstance(self._argument.step_event, llvm_side_condition_event): @@ -172,18 +268,37 @@ def step_event(self) -> LLVMStepEvent: @property def kore_pattern(self) -> Pattern: + """Returns the KORE Pattern associated with the argument if any.""" assert isinstance(self._argument.kore_pattern, Pattern) return self._argument.kore_pattern def is_kore_pattern(self) -> bool: + """Checks if the argument is a KORE Pattern.""" return self._argument.is_kore_pattern() def is_step_event(self) -> bool: + """Checks if the argument is a step event.""" return self._argument.is_step_event() @final class LLVMRewriteTrace: + """ + Represents an LLVM rewrite trace. + + 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: