rename new event to function_exit

bindings/python/ast.cpp

@@ -427,11 +427,11 @@ void bind_proof_trace(py::module_ &m) {
           &llvm_pattern_matching_failure_event::get_function_name);
 
   py::class_<
-      llvm_tail_call_info_event, std::shared_ptr<llvm_tail_call_info_event>>(
-      proof_trace, "llvm_tail_call_info_event", step_event)
+      llvm_function_exit_event, std::shared_ptr<llvm_function_exit_event>>(
+      proof_trace, "llvm_function_exit_event", step_event)
       .def_property_readonly(
-          "rule_ordinal", &llvm_tail_call_info_event::get_rule_ordinal)
-      .def_property_readonly("is_tail", &llvm_tail_call_info_event::is_tail);
+          "rule_ordinal", &llvm_function_exit_event::get_rule_ordinal)
+      .def_property_readonly("is_tail", &llvm_function_exit_event::is_tail);
 
   py::class_<llvm_function_event, std::shared_ptr<llvm_function_event>>(
       proof_trace, "llvm_function_event", step_event)

docs/proof-trace.md

@@ -38,7 +38,7 @@ event             ::= hook
                     | side_cond_exit
                     | config
                     | pattern_matching_failure
-                    | tail_call_info
+                    | function_exit
 
 arg               ::= kore_term
 
@@ -61,7 +61,7 @@ rule              ::= WORD(0x22) ordinal arity variable*
 side_cond_entry   ::= WORD(0xEE) ordinal arity variable*
 side_cond_exit    ::= WORD(0x33) ordinal boolean_result
 
-tail_call_info    ::= WORD(0x55) ordinal boolean_result
+function_exit     ::= WORD(0x55) ordinal boolean_result
 
 config            ::= WORD(0xFF) kore_term
 

include/kllvm/binary/ProofTraceParser.h

@@ -35,7 +35,7 @@ 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);
-constexpr uint64_t tail_call_info_sentinel = detail::word(0x55);
+constexpr uint64_t function_exit_sentinel = detail::word(0x55);
 
 class llvm_step_event : public std::enable_shared_from_this<llvm_step_event> {
 public:
@@ -173,20 +173,20 @@ class llvm_pattern_matching_failure_event : public llvm_step_event {
       const override;
 };
 
-class llvm_tail_call_info_event : public llvm_step_event {
+class llvm_function_exit_event : public llvm_step_event {
 private:
   uint64_t rule_ordinal_;
   bool is_tail_;
 
-  llvm_tail_call_info_event(uint64_t rule_ordinal, bool is_tail)
+  llvm_function_exit_event(uint64_t rule_ordinal, bool is_tail)
       : rule_ordinal_(rule_ordinal)
       , is_tail_(is_tail) { }
 
 public:
-  static sptr<llvm_tail_call_info_event>
+  static sptr<llvm_function_exit_event>
   create(uint64_t rule_ordinal, bool is_tail) {
-    return sptr<llvm_tail_call_info_event>(
-        new llvm_tail_call_info_event(rule_ordinal, is_tail));
+    return sptr<llvm_function_exit_event>(
+        new llvm_function_exit_event(rule_ordinal, is_tail));
   }
 
   [[nodiscard]] uint64_t get_rule_ordinal() const { return rule_ordinal_; }
@@ -623,9 +623,9 @@ class proof_trace_parser {
     return event;
   }
 
-  sptr<llvm_tail_call_info_event> static parse_tail_call_info(
+  sptr<llvm_function_exit_event> static parse_function_exit(
       proof_trace_buffer &buffer) {
-    if (!buffer.check_word(tail_call_info_sentinel)) {
+    if (!buffer.check_word(function_exit_sentinel)) {
       return nullptr;
     }
 
@@ -639,7 +639,7 @@ class proof_trace_parser {
       return nullptr;
     }
 
-    auto event = llvm_tail_call_info_event::create(ordinal, is_tail);
+    auto event = llvm_function_exit_event::create(ordinal, is_tail);
 
     return event;
   }
@@ -679,7 +679,7 @@ class proof_trace_parser {
     case pattern_matching_failure_sentinel:
       return parse_pattern_matching_failure(buffer);
 
-    case tail_call_info_sentinel: return parse_tail_call_info(buffer);
+    case function_exit_sentinel: return parse_function_exit(buffer);
 
     default: return nullptr;
     }

include/kllvm/codegen/ProofEvent.h

@@ -177,9 +177,9 @@ class proof_event {
       llvm::BasicBlock *insert_at_end);
 
   /*
-   * Emit a call to the `tail_call_info` API of the specified `proof_writer`.
+   * Emit a call to the `function_exit` API of the specified `proof_writer`.
    */
-  llvm::CallInst *emit_write_tail_call_info(
+  llvm::CallInst *emit_write_function_exit(
       llvm::Value *proof_writer, uint64_t ordinal, bool is_tail,
       llvm::BasicBlock *insert_at_end);
 
@@ -239,7 +239,7 @@ class proof_event {
   [[nodiscard]] llvm::BasicBlock *pattern_matching_failure(
       kore_composite_pattern const &pattern, llvm::BasicBlock *current_block);
 
-  [[nodiscard]] llvm::BasicBlock *tail_call_info(
+  [[nodiscard]] llvm::BasicBlock *function_exit(
       uint64_t ordinal, bool is_tail, llvm::Instruction *insert_before,
       llvm::BasicBlock *current_block);
 

include/runtime/header.h

@@ -231,7 +231,7 @@ void write_side_condition_event_post_to_proof_trace(
     void *proof_writer, uint64_t ordinal, bool side_cond_result);
 void write_pattern_matching_failure_to_proof_trace(
     void *proof_writer, char const *function_name);
-void write_tail_call_info_to_proof_trace(
+void write_function_exit_to_proof_trace(
     void *proof_writer, uint64_t ordinal, bool is_tail);
 void write_configuration_to_proof_trace(
     void *proof_writer, block *config, bool is_initial);

include/runtime/proof_trace_writer.h

@@ -33,7 +33,7 @@ class proof_trace_writer {
   side_condition_event_post(uint64_t ordinal, bool side_cond_result)
       = 0;
   virtual void pattern_matching_failure(char const *function_name) = 0;
-  virtual void tail_call_info(uint64_t ordinal, bool is_tail) = 0;
+  virtual void function_exit(uint64_t ordinal, bool is_tail) = 0;
   virtual void configuration(block *config, bool is_initial) = 0;
   virtual void start_new_chunk() = 0;
   virtual void end_of_trace() = 0;
@@ -164,8 +164,8 @@ class proof_trace_file_writer : public proof_trace_writer {
     write_null_terminated_string(function_name);
   }
 
-  void tail_call_info(uint64_t ordinal, bool is_tail) override {
-    write_uint64(kllvm::tail_call_info_sentinel);
+  void function_exit(uint64_t ordinal, bool is_tail) override {
+    write_uint64(kllvm::function_exit_sentinel);
     write_uint64(ordinal);
     write_bool(is_tail);
   }
@@ -234,11 +234,11 @@ class proof_trace_callback_writer : public proof_trace_writer {
         , result(result) { }
   };
 
-  struct tail_call_info_construction {
+  struct function_exit_construction {
     uint64_t ordinal;
     bool is_tail;
 
-    tail_call_info_construction(uint64_t ordinal, bool is_tail)
+    function_exit_construction(uint64_t ordinal, bool is_tail)
         : ordinal(ordinal)
         , is_tail(is_tail) { }
   };
@@ -300,7 +300,7 @@ class proof_trace_callback_writer : public proof_trace_writer {
   [[clang::optnone]] void pattern_matching_failure_callback(
       pattern_matching_failure_construction const &event) { }
   [[clang::optnone]] void
-  tail_call_info_callback(tail_call_info_construction const &event) { }
+  function_exit_callback(function_exit_construction const &event) { }
   [[clang::optnone]] void configuration_event_callback(
       kore_configuration_construction const &config, bool is_initial) { }
 
@@ -386,9 +386,9 @@ class proof_trace_callback_writer : public proof_trace_writer {
     pattern_matching_failure_callback(pm_failure);
   }
 
-  void tail_call_info(uint64_t ordinal, bool is_tail) override {
-    tail_call_info_construction tail_call_info(ordinal, is_tail);
-    tail_call_info_callback(tail_call_info);
+  void function_exit(uint64_t ordinal, bool is_tail) override {
+    function_exit_construction function_exit(ordinal, is_tail);
+    function_exit_callback(function_exit);
   }
 
   void configuration(block *config, bool is_initial) override {

lib/binary/ProofTraceParser.cpp

@@ -84,11 +84,11 @@ void llvm_pattern_matching_failure_event::print(
       "{}pattern matching failure: {}\n", indent, function_name_);
 }
 
-void llvm_tail_call_info_event::print(
+void llvm_function_exit_event::print(
     std::ostream &out, bool expand_terms, unsigned ind) const {
   std::string indent(ind * indent_size, ' ');
   out << fmt::format(
-      "{}tail_call_info: {} {}\n", indent, rule_ordinal_,
+      "{}function exit: {} {}\n", indent, rule_ordinal_,
       (is_tail_ ? "tail" : "notail"));
 }
 

lib/codegen/CreateTerm.cpp

@@ -1295,20 +1295,20 @@ bool make_function(
         if (is_apply_rule) {
           current_block
               = proof_event(definition, module)
-                    .tail_call_info(ordinal, true, call, current_block);
+                    .function_exit(ordinal, true, call, current_block);
         }
       } else {
         if (is_apply_rule) {
           current_block
               = proof_event(definition, module)
-                    .tail_call_info(ordinal, false, nullptr, current_block);
+                    .function_exit(ordinal, false, nullptr, current_block);
         }
       }
     } else {
       if (is_apply_rule) {
         current_block
             = proof_event(definition, module)
-                  .tail_call_info(ordinal, false, nullptr, current_block);
+                  .function_exit(ordinal, false, nullptr, current_block);
       }
     }
   }

lib/codegen/ProofEvent.cpp

@@ -304,7 +304,7 @@ llvm::CallInst *proof_event::emit_write_pattern_matching_failure(
   return b.CreateCall(func, {proof_writer, var_function_name});
 }
 
-llvm::CallInst *proof_event::emit_write_tail_call_info(
+llvm::CallInst *proof_event::emit_write_function_exit(
     llvm::Value *proof_writer, uint64_t ordinal, bool is_tail,
     llvm::BasicBlock *insert_at_end) {
   auto b = llvm::IRBuilder(insert_at_end);
@@ -318,7 +318,7 @@ llvm::CallInst *proof_event::emit_write_tail_call_info(
       = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i64_ty, i8_ty}, false);
 
   auto *func = get_or_insert_function(
-      module_, "write_tail_call_info_to_proof_trace", func_ty);
+      module_, "write_function_exit_to_proof_trace", func_ty);
 
   auto *var_ordinal = llvm::ConstantInt::get(i64_ty, ordinal);
   auto *var_is_tail = llvm::ConstantInt::get(i8_ty, is_tail);
@@ -745,7 +745,7 @@ llvm::BasicBlock *proof_event::pattern_matching_failure(
   return merge_block;
 }
 
-llvm::BasicBlock *proof_event::tail_call_info(
+llvm::BasicBlock *proof_event::function_exit(
     uint64_t ordinal, bool is_tail, llvm::Instruction *insert_before,
     llvm::BasicBlock *current_block) {
 
@@ -756,14 +756,14 @@ llvm::BasicBlock *proof_event::tail_call_info(
   std::tuple<llvm::BasicBlock *, llvm::BasicBlock *, llvm::Value *> prelude;
   if (is_tail) {
     assert(insert_before);
-    prelude = event_prelude("tail_call_info", insert_before);
+    prelude = event_prelude("function_exit", insert_before);
   } else {
-    prelude = event_prelude("tail_call_info", current_block);
+    prelude = event_prelude("function_exit", current_block);
   }
 
   auto [true_block, merge_block, proof_writer] = prelude;
 
-  emit_write_tail_call_info(proof_writer, ordinal, is_tail, true_block);
+  emit_write_function_exit(proof_writer, ordinal, is_tail, true_block);
 
   llvm::BranchInst::Create(merge_block, true_block);
 

runtime/util/ConfigurationSerializer.cpp

@@ -717,10 +717,10 @@ void write_pattern_matching_failure_to_proof_trace(
       ->pattern_matching_failure(function_name);
 }
 
-void write_tail_call_info_to_proof_trace(
+void write_function_exit_to_proof_trace(
     void *proof_writer, uint64_t ordinal, bool is_tail) {
   static_cast<proof_trace_writer *>(proof_writer)
-      ->tail_call_info(ordinal, is_tail);
+      ->function_exit(ordinal, is_tail);
 }
 
 void write_configuration_to_proof_trace(