Write streaming event parser for proof hints (#1069)

This is a pretty straightforward diff. We can reuse the code for parsing
events and the proof trace header, so we just need to create an entry
point to the streaming parser that invokes the relevant parsing logic
and returns events one at a time, and then write code to test it. We
test it by modifying lit tests that test the proof hints so that they
test both parsers. This means we get the advantage of the entire
coverage set of tests that we imported from the math proof repo.

Author: Dwight Guth

include/kllvm/binary/ProofTraceParser.h

@@ -234,6 +234,13 @@ class llvm_event {
       unsigned indent = 0U) const;
 };
 
+enum class llvm_event_type { PreTrace, InitialConfig, Trace };
+
+struct annotated_llvm_event {
+  llvm_event_type type{};
+  llvm_event event;
+};
+
 class llvm_rewrite_trace {
 private:
   uint32_t version_{};
@@ -651,6 +658,23 @@ class proof_trace_parser {
   std::optional<llvm_rewrite_trace>
   parse_proof_trace_from_file(std::string const &filename);
   std::optional<llvm_rewrite_trace> parse_proof_trace(std::string const &data);
+
+  friend class llvm_rewrite_trace_iterator;
+};
+
+class llvm_rewrite_trace_iterator {
+private:
+  uint32_t version_{};
+  proof_trace_buffer &buffer_;
+  llvm_event_type type_ = llvm_event_type::PreTrace;
+  proof_trace_parser parser_;
+
+public:
+  llvm_rewrite_trace_iterator(
+      proof_trace_buffer &buffer, kore_header const &header);
+  [[nodiscard]] uint32_t get_version() const { return version_; }
+  std::optional<annotated_llvm_event> get_next_event();
+  void print(std::ostream &out, bool expand_terms, unsigned indent = 0U);
 };
 
 } // namespace kllvm

lib/binary/ProofTraceParser.cpp

@@ -115,6 +115,59 @@ void llvm_event::print(
   }
 }
 
+llvm_rewrite_trace_iterator::llvm_rewrite_trace_iterator(
+    proof_trace_buffer &buffer, kore_header const &header)
+    : buffer_(buffer)
+    , parser_(false, false, header) {
+  if (!proof_trace_parser::parse_header(buffer_, version_)) {
+    throw std::runtime_error("invalid header");
+  }
+}
+
+std::optional<annotated_llvm_event>
+llvm_rewrite_trace_iterator::get_next_event() {
+  if (buffer_.eof()) {
+    return std::nullopt;
+  }
+  switch (type_) {
+  case llvm_event_type::PreTrace: {
+    if (buffer_.has_word() && buffer_.peek_word() != config_sentinel) {
+      llvm_event event;
+      if (!parser_.parse_event(buffer_, event)) {
+        throw std::runtime_error("could not parse pre-trace event");
+      }
+      return {{type_, event}};
+    }
+    uint64_t pattern_len = 0;
+    auto config = parser_.parse_config(buffer_, pattern_len);
+    if (!config) {
+      throw std::runtime_error("could not parse config event");
+    }
+    llvm_event config_event;
+    config_event.setkore_pattern(config, pattern_len);
+    type_ = llvm_event_type::Trace;
+    return {{llvm_event_type::InitialConfig, config_event}};
+  }
+  case llvm_event_type::Trace: {
+    llvm_event event;
+    if (!parser_.parse_event(buffer_, event)) {
+      throw std::runtime_error("could not parse trace event");
+    }
+    return {{type_, event}};
+  }
+  default: throw std::runtime_error("should be unreachable");
+  }
+}
+
+void llvm_rewrite_trace_iterator::print(
+    std::ostream &out, bool expand_terms, unsigned ind) {
+  std::string indent(ind * indent_size, ' ');
+  out << fmt::format("{}version: {}\n", indent, version_);
+  while (auto event = get_next_event()) {
+    event.value().event.print(out, expand_terms, false, ind);
+  }
+}
+
 void llvm_rewrite_trace::print(
     std::ostream &out, bool expand_terms, unsigned ind) const {
   std::string indent(ind * indent_size, ' ');

test/lit.cfg.py

@@ -160,6 +160,12 @@ def one_line(s):
             echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms"
             exit 1
         fi
+        %kore-proof-trace --streaming-parser --verbose --expand-terms %t.header.bin %t.out.bin | diff - %test-proof-diff-out -q
+        result="$?"
+        if [ "$result" -ne 0 ]; then
+            echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms and streaming parser"
+            exit 1
+        fi
     ''')),
 
     ('%check-dir-proof-out', one_line('''
@@ -175,6 +181,12 @@ def one_line(s):
                 echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms"
                 exit 1
             fi
+            %kore-proof-trace --streaming-parser --verbose --expand-terms %t.header.bin $hint | diff - $out
+            result="$?"
+            if [ "$result" -ne 0 ]; then
+                echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms and streaming parser"
+                exit 1
+            fi
         done
     ''')),
 

tools/kore-proof-trace/main.cpp

@@ -27,6 +27,11 @@ cl::opt<bool> expand_terms_in_output(
     "expand-terms", llvm::cl::desc("Expand KORE terms in the verbose output"),
     llvm::cl::cat(kore_proof_trace_cat));
 
+cl::opt<bool> use_streaming_parser(
+    "streaming-parser",
+    llvm::cl::desc("Use streaming event parser to parse trace"),
+    llvm::cl::cat(kore_proof_trace_cat));
+
 int main(int argc, char **argv) {
   cl::HideUnrelatedOptions({&kore_proof_trace_cat});
   cl::ParseCommandLineOptions(argc, argv);
@@ -35,6 +40,16 @@ int main(int argc, char **argv) {
   kore_header header(in);
   fclose(in);
 
+  if (use_streaming_parser) {
+    std::ifstream file(input_filename, std::ios_base::binary);
+    proof_trace_file_buffer buffer(file);
+    llvm_rewrite_trace_iterator it(buffer, header);
+    if (verbose_output) {
+      it.print(std::cout, expand_terms_in_output);
+    }
+    return 0;
+  }
+
   proof_trace_parser parser(verbose_output, expand_terms_in_output, header);
   auto trace = parser.parse_proof_trace_from_file(input_filename);
   if (trace.has_value()) {