From d6ff56c9221bf898bdb9ef315f00da3f90237dcc Mon Sep 17 00:00:00 2001
From: Roberto Rosmaninho <robertogomes@dcc.ufmg.br>
Date: Sat, 21 Sep 2024 21:05:26 -0300
Subject: [PATCH] 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:
https://github.com/runtimeverification/llvm-backend/pull/1148
- The K update LLVM Backend PR:
https://github.com/runtimeverification/k/pull/4639

---------

Co-authored-by: rv-jenkins <admin@runtimeverification.com>
---
 pyk/src/pyk/kllvm/hints/prooftrace.py         | 37 +++++++++++++++++++
 .../integration/kllvm/test_prooftrace.py      |  7 +++-
 2 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py
index 2cc98e6f0ed..fabe1d2f64d 100644
--- a/pyk/src/pyk/kllvm/hints/prooftrace.py
+++ b/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()
 
diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py
index 0883ca54471..62fa039a55d 100644
--- a/pyk/src/tests/integration/kllvm/test_prooftrace.py
+++ b/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 = """