Introducing the LLVMPatternMatchingFailureEvent class in ProofTrace…

… module (#4643)

This PR exposes a new LLVM Proof Hint event by creating its own Pyk
representation class, which the Pi2 MPG Team can use to parse the new
Hints version!

- This PR depends on the LLVM Backend PR:
runtimeverification/llvm-backend#1148
- The K update LLVM Backend PR:
#4639

---------

Co-authored-by: rv-jenkins <[email protected]>

pyk/src/pyk/kllvm/hints/prooftrace.py

@@ -15,6 +15,7 @@
     llvm_side_condition_end_event,
     llvm_side_condition_event,
     llvm_step_event,
+    llvm_pattern_matching_failure_event,
     annotated_llvm_event,
     llvm_rewrite_trace_iterator,
     EventType,
@@ -168,6 +169,40 @@ def check_result(self) -> bool:
         return self._side_condition_end_event.check_result
 
 
+@final
+class LLVMPatternMatchingFailureEvent(LLVMStepEvent):
+    """Represents an LLVM pattern matching failure event.
+
+    This event is used to indicate that the pattern matching failed during the rewriting process.
+
+    Attributes:
+        _pattern_matching_failure_event (llvm_pattern_matching_failure_event): The underlying pattern matching failure event.
+    """
+
+    _pattern_matching_failure_event: llvm_pattern_matching_failure_event
+
+    def __init__(self, pattern_matching_failure_event: llvm_pattern_matching_failure_event) -> None:
+        """Initialize a new instance of the LLVMPatternMatchingFailureEvent class.
+
+        Args:
+            pattern_matching_failure_event (llvm_pattern_matching_failure_event): The LLVM pattern matching failure event object.
+        """
+        self._pattern_matching_failure_event = pattern_matching_failure_event
+
+    def __repr__(self) -> str:
+        """Return a string representation of the object.
+
+        Returns:
+            A string representation of the LLVMPatternMatchingFailureEvent object using the AST printing method.
+        """
+        return self._pattern_matching_failure_event.__repr__()
+
+    @property
+    def function_name(self) -> str:
+        """Return the name of the function that failed to match the pattern."""
+        return self._pattern_matching_failure_event.function_name
+
+
 @final
 class LLVMFunctionEvent(LLVMStepEvent):
     """Represent an LLVM function event in a proof trace.
@@ -297,6 +332,8 @@ def step_event(self) -> LLVMStepEvent:
             return LLVMFunctionEvent(self._argument.step_event)
         elif isinstance(self._argument.step_event, llvm_hook_event):
             return LLVMHookEvent(self._argument.step_event)
+        elif isinstance(self._argument.step_event, llvm_pattern_matching_failure_event):
+            return LLVMPatternMatchingFailureEvent(self._argument.step_event)
         else:
             raise AssertionError()
 

pyk/src/tests/integration/kllvm/test_prooftrace.py

@@ -808,9 +808,14 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade
         # 12 initialization events
         assert len(pt.pre_trace) == 12
 
-        # 404 post-initial-configuration events
+        # 776 post-initial-configuration events
         assert len(pt.trace) == 776
 
+        # Assert that we have a pattern matching failure as the 135th event
+        assert pt.trace[135].is_step_event() and isinstance(
+            pt.trace[135].step_event, prooftrace.LLVMPatternMatchingFailureEvent
+        )
+
 
 class TestIMP5(ProofTraceTest):
     KOMPILE_DEFINITION = """