Introducing new llvm_pattern_matching_failure_event to Proof Events (#1134)

Fixes: Pi-Squared-Inc/pi2#1722
This PR introduces a new function event called
`llvm_pattern_matching_failure_event`, which is identified by the
`pattern_matching_failure_sentinel`. This new event flags to the user
that an attempt to apply a rule failed in pattern matching its
constructor; therefore, no further simplification can be done at this
point.

Author: Robertorosmaninho

docs/proof-trace.md

@@ -34,6 +34,7 @@ constexpr uint64_t hook_result_sentinel = detail::word(0xBB);
 constexpr uint64_t rule_event_sentinel = detail::word(0x22);
 constexpr uint64_t side_condition_event_sentinel = detail::word(0xEE);
 constexpr uint64_t side_condition_end_sentinel = detail::word(0x33);
+constexpr uint64_t pattern_matching_failure_sentinel = detail::word(0x44);
 
 class llvm_step_event : public std::enable_shared_from_this<llvm_step_event> {
 public:
@@ -149,6 +150,28 @@ class llvm_side_condition_end_event : public llvm_step_event {
       const override;
 };
 
+class llvm_pattern_matching_failure_event : public llvm_step_event {
+private:
+  std::string function_name_;
+
+  llvm_pattern_matching_failure_event(std::string function_name)
+      : function_name_(std::move(function_name)) { }
+
+public:
+  static sptr<llvm_pattern_matching_failure_event>
+  create(std::string function_name) {
+    return sptr<llvm_pattern_matching_failure_event>(
+        new llvm_pattern_matching_failure_event(std::move(function_name)));
+  }
+
+  [[nodiscard]] std::string const &get_function_name() const {
+    return function_name_;
+  }
+
+  void print(std::ostream &out, bool expand_terms, unsigned indent = 0U)
+      const override;
+};
+
 class llvm_event;
 
 class llvm_function_event : public llvm_step_event {
@@ -296,7 +319,7 @@ class llvm_rewrite_trace {
 
 class proof_trace_parser {
 public:
-  static constexpr uint32_t expected_version = 11U;
+  static constexpr uint32_t expected_version = 12U;
 
 private:
   bool verbose_;
@@ -545,6 +568,22 @@ class proof_trace_parser {
     return event;
   }
 
+  sptr<llvm_pattern_matching_failure_event> static parse_pattern_matching_failure(
+      proof_trace_buffer &buffer) {
+    if (!buffer.check_word(pattern_matching_failure_sentinel)) {
+      return nullptr;
+    }
+
+    std::string function_name;
+    if (!buffer.read_string(function_name)) {
+      return nullptr;
+    }
+
+    auto event = llvm_pattern_matching_failure_event::create(function_name);
+
+    return event;
+  }
+
   bool parse_argument(proof_trace_buffer &buffer, llvm_event &event) {
     if (!buffer.eof() && buffer.peek() == '\x7F') {
       uint64_t pattern_len = 0;
@@ -608,6 +647,16 @@ class proof_trace_parser {
       return true;
     }
 
+    case pattern_matching_failure_sentinel: {
+      auto pattern_matching_failure_event
+          = parse_pattern_matching_failure(buffer);
+      if (!pattern_matching_failure_event) {
+        return false;
+      }
+      event.set_step_event(pattern_matching_failure_event);
+      return true;
+    }
+
     default: return false;
     }
   }
@@ -629,6 +678,9 @@ class proof_trace_parser {
 
     case side_condition_end_sentinel: return parse_side_condition_end(buffer);
 
+    case pattern_matching_failure_sentinel:
+      return parse_pattern_matching_failure(buffer);
+
     default: return nullptr;
     }
   }

include/kllvm/binary/ProofTraceParser.h

@@ -129,6 +129,9 @@ class proof_event {
       kore_axiom_declaration const &axiom, llvm::Value *check_result,
       llvm::BasicBlock *current_block);
 
+  [[nodiscard]] llvm::BasicBlock *pattern_matching_failure(
+      kore_composite_pattern const &pattern, llvm::BasicBlock *current_block);
+
   proof_event(kore_definition *definition, llvm::Module *module)
       : definition_(definition)
       , module_(module)

include/kllvm/codegen/ProofEvent.h

@@ -77,6 +77,13 @@ void llvm_side_condition_end_event::print(
       (result_ ? "true" : "false"));
 }
 
+void llvm_pattern_matching_failure_event::print(
+    std::ostream &out, bool expand_terms, unsigned ind) const {
+  std::string indent(ind * indent_size, ' ');
+  out << fmt::format(
+      "{}pattern matching failure: {}\n", indent, function_name_);
+}
+
 void llvm_function_event::print(
     std::ostream &out, bool expand_terms, unsigned ind) const {
   std::string indent(ind * indent_size, ' ');

lib/binary/ProofTraceParser.cpp

@@ -922,6 +922,8 @@ void add_owise(
     auto var = kore_variable_pattern::create(name, symbol->get_arguments()[i]);
     pat->add_argument(std::move(var));
   }
+  proof_event p(d, module);
+  stuck = p.pattern_matching_failure(*pat, stuck);
   create_term creator = create_term(final_subst, d, stuck, module, true);
   llvm::Value *retval = creator(pat.get()).first;
 

lib/codegen/Decision.cpp

@@ -381,4 +381,24 @@ llvm::BasicBlock *proof_event::side_condition_event_post(
   return merge_block;
 }
 
+llvm::BasicBlock *proof_event::pattern_matching_failure(
+    kore_composite_pattern const &pattern, llvm::BasicBlock *current_block) {
+
+  if (!proof_hint_instrumentation) {
+    return current_block;
+  }
+
+  auto [true_block, merge_block, proof_writer]
+      = event_prelude("pattern_matching_failure", current_block);
+
+  std::string function_name = ast_to_string(*pattern.get_constructor());
+
+  emit_write_uint64(proof_writer, detail::word(0x44), true_block);
+  emit_write_string(proof_writer, function_name, true_block);
+
+  llvm::BranchInst::Create(merge_block, true_block);
+
+  return merge_block;
+}
+
 } // namespace kllvm

lib/codegen/ProofEvent.cpp

@@ -35,7 +35,7 @@ block *construct_raw_term(void *subject, char const *sort, bool raw_value) {
 }
 
 void print_proof_hint_header(kllvm::proof_trace_writer *writer) {
-  uint32_t version = 11;
+  uint32_t version = 12;
   writer->write_string("HINT");
   writer->write_uint32(version);
 }

runtime/util/util.cpp

@@ -1,4 +1,4 @@
-version: 11
+version: 12
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]

test/output/add-rewrite/input.proof.debug.out.diff

@@ -1,4 +1,4 @@
-version: 11
+version: 12
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]

test/output/add-rewrite/input.proof.out.diff

@@ -1,4 +1,4 @@
-version: 11
+version: 12
 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
   function: Lbl'UndsPipe'-'-GT-Unds'{} ()
   arg: kore[\dv{SortKConfigVar{}}("$PGM")]