Split proof hint trace into multiple files (#1147)

This PR adds support for generating multiple hint trace files containing
parts of the total trace. To this end, we add an optional
`--proof-chunk-size N` flag to the `interpreter` binary. When the flag
is passed and `N` is greater than `0`, then the trace is separated into
multiple files as follows:
- an `<output filename>.pre_trace` file with the pre-trace events and
the initial configuration.
- a number of `<output filename>.<idx>` files that each contain `N`
top-level rewrite rule events along with their corresponding side
condition events and simplification events. If the `interpreter` binary
has been generated with the slow option, then each of these files also
contains configuration events after each rewrite event. Note that the
last file may contain less than `N` events.

By default `N` equals to `0` and in this case, the trace is generated
exactly as before.

This PR also adds support to the `kore_proof_trace` tool to be able to
parse partial trace files. To achieve this, we introduce two more
special headers (one for the pre-trace file and one for the chunk files)
that allow the parser to recognize what kind of file it should expect.

bin/llvm-kompile-testing

@@ -41,4 +41,4 @@ while [ $# -gt 0 ]; do
   shift
 done
 
-llvm-kompile "$definition" "$dt_dir" "$mode" "${llvm_kompile_flags[@]}" "${clang_flags[@]}" -g --verify-ir
+llvm-kompile "$definition" "$dt_dir" "$mode" "${llvm_kompile_flags[@]}" --verify-ir "${clang_flags[@]}" -g

config/llvm_header.inc

@@ -193,7 +193,7 @@ define i1 @string_equal(ptr %str1, ptr %str2, i64 %len1, i64 %len2) {
 
 declare tailcc ptr @k_step(ptr)
 declare tailcc void @step_all(ptr)
-declare void @write_configuration_to_proof_trace(ptr, ptr)
+declare void @write_configuration_to_proof_trace(ptr, ptr, i1)
 
 @proof_output = external global i1
 @proof_writer = external global ptr
@@ -231,7 +231,7 @@ define ptr @take_steps(i64 %depth, ptr %subject) {
   br i1 %proof_output, label %if, label %merge
 if:
   %proof_writer = load ptr, ptr @proof_writer
-  call void @write_configuration_to_proof_trace(ptr %proof_writer, ptr %subject)
+  call void @write_configuration_to_proof_trace(ptr %proof_writer, ptr %subject, i1 true)
   br label %merge
 merge:
   store i64 %depth, ptr @depth

include/kllvm/binary/ProofTraceParser.h

@@ -323,6 +323,8 @@ class proof_trace_parser {
 public:
   static constexpr uint32_t expected_version = 13U;
 
+  enum class trace_kind { Hint, PreTrace, Chunk };
+
 private:
   bool verbose_;
   bool expand_terms_;
@@ -345,13 +347,24 @@ class proof_trace_parser {
     return result;
   }
 
-  static bool parse_header(proof_trace_buffer &buffer, uint32_t &version) {
+  static bool parse_header(
+      proof_trace_buffer &buffer, trace_kind &kind, uint32_t &version) {
     std::array<char, 4> magic{};
     if (!buffer.read(magic.data(), sizeof(magic))) {
       return false;
     }
-    if (magic[0] != 'H' || magic[1] != 'I' || magic[2] != 'N'
-        || magic[3] != 'T') {
+    if (magic[0] == 'H' && magic[1] == 'I' && magic[2] == 'N'
+        && magic[3] == 'T') {
+      kind = trace_kind::Hint;
+    } else if (
+        magic[0] == 'P' && magic[1] == 'T' && magic[2] == 'R'
+        && magic[3] == 'C') {
+      kind = trace_kind::PreTrace;
+    } else if (
+        magic[0] == 'C' && magic[1] == 'H' && magic[2] == 'N'
+        && magic[3] == 'K') {
+      kind = trace_kind::Chunk;
+    } else {
       return false;
     }
 
@@ -650,27 +663,30 @@ class proof_trace_parser {
 
   bool parse_trace(proof_trace_buffer &buffer, llvm_rewrite_trace &trace) {
     uint32_t version = 0;
-    if (!parse_header(buffer, version)) {
+    trace_kind kind = trace_kind::Hint;
+    if (!parse_header(buffer, kind, version)) {
       return false;
     }
     trace.set_version(version);
 
-    while (buffer.has_word() && buffer.peek_word() != config_sentinel) {
-      llvm_event event;
-      if (!parse_event(buffer, event)) {
-        return false;
+    if (kind == trace_kind::Hint || kind == trace_kind::PreTrace) {
+      while (buffer.has_word() && buffer.peek_word() != config_sentinel) {
+        llvm_event event;
+        if (!parse_event(buffer, event)) {
+          return false;
+        }
+        trace.add_pre_trace_event(event);
       }
-      trace.add_pre_trace_event(event);
-    }
 
-    uint64_t pattern_len = 0;
-    auto config = parse_config(buffer, pattern_len);
-    if (!config) {
-      return false;
+      uint64_t pattern_len = 0;
+      auto config = parse_config(buffer, pattern_len);
+      if (!config) {
+        return false;
+      }
+      llvm_event config_event;
+      config_event.setkore_pattern(config, pattern_len);
+      trace.set_initial_config(config_event);
     }
-    llvm_event config_event;
-    config_event.setkore_pattern(config, pattern_len);
-    trace.set_initial_config(config_event);
 
     while (!buffer.eof()) {
       llvm_event event;
@@ -699,6 +715,7 @@ class proof_trace_parser {
 class llvm_rewrite_trace_iterator {
 private:
   uint32_t version_{};
+  proof_trace_parser::trace_kind kind_{};
   std::unique_ptr<proof_trace_buffer> buffer_;
   llvm_event_type type_ = llvm_event_type::PreTrace;
   proof_trace_parser parser_;

include/kllvm/codegen/ProofEvent.h

@@ -43,6 +43,16 @@ class proof_event {
   std::tuple<llvm::BasicBlock *, llvm::BasicBlock *, llvm::Value *>
   event_prelude(std::string const &label, llvm::BasicBlock *insert_at_end);
 
+  /*
+   * Set up a check of whether a new proof hint chunk should be started. The
+   * condition for that is
+   *   proof_chunk_size != 0 and steps % proof_chunk_size = 0
+   * Returns a block intended for adding code that starts a new chunk. If the
+   * condition is false, we branch to the given merge_block.
+   */
+  llvm::BasicBlock *check_for_emit_new_chunk(
+      llvm::BasicBlock *insert_at_end, llvm::BasicBlock *merge_block);
+
   /*
    * Emit an instruction that has no effect and will be removed by optimization
    * passes.
@@ -60,6 +70,19 @@ class proof_event {
    */
   llvm::LoadInst *emit_get_proof_trace_writer(llvm::BasicBlock *insert_at_end);
 
+  /*
+   * Emit instructions to get the current value of the steps global variable,
+   * which counts the number of rewrite steps taken.
+   */
+  llvm::LoadInst *emit_get_steps(llvm::BasicBlock *insert_at_end);
+
+  /*
+   * Emit instructions to get the current value of the proof_chunk_size global
+   * variable, which dictates how many rewrite steps should be included per
+   * chunk of the hint trace.
+   */
+  llvm::LoadInst *emit_get_proof_chunk_size(llvm::BasicBlock *insert_at_end);
+
   /*
    * Get the block header value for the given `sort_name`.
    */
@@ -136,12 +159,18 @@ class proof_event {
       llvm::BasicBlock *insert_at_end);
 
   /*
-   * Emit a call to the `patteern_matching_failure` API of the specified `proof_writer`.
+   * Emit a call to the `pattern_matching_failure` API of the specified `proof_writer`.
    */
   llvm::CallInst *emit_write_pattern_matching_failure(
       llvm::Value *proof_writer, std::string const &function_name,
       llvm::BasicBlock *insert_at_end);
 
+  /*
+   * Emit a call to the `start_new_chunk` API of the specified `proof_writer`.
+   */
+  llvm::CallInst *emit_start_new_chunk(
+      llvm::Value *proof_writer, llvm::BasicBlock *insert_at_end);
+
 public:
   [[nodiscard]] llvm::BasicBlock *hook_event_pre(
       std::string const &name, kore_composite_pattern *pattern,

include/runtime/header.h

@@ -374,7 +374,9 @@ 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_configuration_to_proof_trace(void *proof_writer, block *config);
+void write_configuration_to_proof_trace(
+    void *proof_writer, block *config, bool is_initial);
+void start_new_chunk_in_proof_trace(void *proof_writer);
 
 // The following functions have to be generated at kompile time
 // and linked with the interpreter.

include/runtime/proof_trace_writer.h

@@ -33,12 +33,21 @@ 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 configuration(block *config) = 0;
+  virtual void configuration(block *config, bool is_initial) = 0;
+  virtual void start_new_chunk() = 0;
   virtual void end_of_trace() = 0;
 };
 
+extern "C" {
+extern FILE *output_file;
+}
+
 class proof_trace_file_writer : public proof_trace_writer {
 private:
+  char const *filename_base_;
+  size_t chunk_size_;
+  size_t file_number_;
+  uint32_t version_;
   FILE *file_;
 
   void write_bytes(void const *ptr, size_t len) { fwrite(ptr, len, 1, file_); }
@@ -62,12 +71,29 @@ class proof_trace_file_writer : public proof_trace_writer {
   void write_uint64(uint64_t i) { write_bytes(&i, sizeof(uint64_t)); }
 
 public:
-  proof_trace_file_writer(FILE *file)
-      : file_(file) { }
+  proof_trace_file_writer(char const *filename_base, size_t chunk_size)
+      : filename_base_(filename_base)
+      , chunk_size_(chunk_size)
+      , file_number_(0)
+      , version_(0) {
+    if (chunk_size_ > 0) {
+      std::string filename = std::string(filename_base_) + ".pre_trace";
+      file_ = std::fopen(filename.c_str(), "w");
+    } else {
+      file_ = std::fopen(filename_base_, "w");
+    }
+    output_file = file_;
+  }
 
   void proof_trace_header(uint32_t version) override {
-    write_string("HINT");
-    write_uint32(version);
+    if (chunk_size_ == 0) {
+      write_string("HINT");
+      write_uint32(version);
+    } else {
+      write_string("PTRC");
+      write_uint32(version);
+      version_ = version;
+    }
   }
 
   void hook_event_pre(
@@ -137,9 +163,24 @@ class proof_trace_file_writer : public proof_trace_writer {
     write_null_terminated_string(function_name);
   }
 
-  void configuration(block *config) override {
+  void configuration(block *config, bool is_initial) override {
     write_uint64(kllvm::config_sentinel);
     serialize_configuration_to_proof_trace(file_, config, 0);
+
+    if (chunk_size_ > 0 && is_initial) {
+      start_new_chunk();
+    }
+  }
+
+  void start_new_chunk() override {
+    std::fclose(file_);
+    std::string filename
+        = std::string(filename_base_) + "." + std::to_string(file_number_);
+    file_number_++;
+    file_ = std::fopen(filename.c_str(), "w");
+    output_file = file_;
+    write_string("CHNK");
+    write_uint32(version_);
   }
 
   void end_of_trace() override { }
@@ -242,9 +283,8 @@ class proof_trace_callback_writer : public proof_trace_writer {
       side_condition_result_construction const &event) { }
   [[clang::optnone]] void pattern_matching_failure_callback(
       pattern_matching_failure_construction const &event) { }
-  [[clang::optnone]] void
-  configuration_event_callback(kore_configuration_construction const &config) {
-  }
+  [[clang::optnone]] void configuration_event_callback(
+      kore_configuration_construction const &config, bool is_initial) { }
 
 public:
   proof_trace_callback_writer() { }
@@ -328,11 +368,13 @@ class proof_trace_callback_writer : public proof_trace_writer {
     pattern_matching_failure_callback(pm_failure);
   }
 
-  void configuration(block *config) override {
+  void configuration(block *config, bool is_initial) override {
     kore_configuration_construction configuration(config);
-    configuration_event_callback(configuration);
+    configuration_event_callback(configuration, is_initial);
   }
 
+  void start_new_chunk() override { }
+
   void end_of_trace() override { }
 };
 

lib/binary/ProofTraceParser.cpp

@@ -115,7 +115,7 @@ void llvm_event::print(
     std::ostream &out, bool expand_terms, bool is_arg, unsigned ind) const {
   if (is_step_event_) {
     step_event_->print(out, expand_terms, ind);
-  } else {
+  } else if (kore_pattern_) {
     std::string indent(ind * indent_size, ' ');
     if (expand_terms) {
       out << fmt::format("{}{}: kore[", indent, is_arg ? "arg" : "config");
@@ -133,9 +133,13 @@ llvm_rewrite_trace_iterator::llvm_rewrite_trace_iterator(
     std::unique_ptr<proof_trace_buffer> buffer, kore_header const &header)
     : buffer_(std::move(buffer))
     , parser_(false, false, header) {
-  if (!proof_trace_parser::parse_header(*buffer_, version_)) {
+  if (!proof_trace_parser::parse_header(*buffer_, kind_, version_)) {
     throw std::runtime_error("invalid header");
   }
+  if (kind_ != proof_trace_parser::trace_kind::Hint) {
+    throw std::runtime_error("invalid hint file: streaming parser does not "
+                             "work with partial traces");
+  }
 }
 
 std::optional<annotated_llvm_event>