Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

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()) {