Add python bindings for proof hint streaming parser (#1075)

Previously we did not have any python bindings for the streaming parser
I created.

This PR adds the relevant pybind code as well as adding a python unit
test for that code. A slight change is made to the ownership semantics
of proof_trace_buffer and its derived classes in order to allow the
python bindings to work as expected.

---------

Co-authored-by: rv-jenkins <[email protected]>

bindings/python/ast.cpp

@@ -457,6 +457,32 @@ void bind_proof_trace(py::module_ &m) {
   py::class_<kore_header, std::shared_ptr<kore_header>>(
       proof_trace, "kore_header")
       .def(py::init(&kore_header::create), py::arg("path"));
+
+  py::enum_<llvm_event_type>(proof_trace, "LLVMEventType")
+      .value("PreTrace", llvm_event_type::PreTrace)
+      .value("InitialConfig", llvm_event_type::InitialConfig)
+      .value("Trace", llvm_event_type::Trace);
+
+  py::class_<annotated_llvm_event>(proof_trace, "annotated_llvm_event")
+      .def_readonly("type", &annotated_llvm_event::type)
+      .def_readonly("event", &annotated_llvm_event::event);
+
+  py::class_<
+      llvm_rewrite_trace_iterator,
+      std::shared_ptr<llvm_rewrite_trace_iterator>>(
+      proof_trace, "llvm_rewrite_trace_iterator")
+      .def_static(
+          "from_file",
+          [](std::string const &filename, kore_header const &header) {
+            std::ifstream file(filename, std::ios_base::binary);
+            return llvm_rewrite_trace_iterator(
+                std::make_unique<proof_trace_file_buffer>(std::move(file)),
+                header);
+          },
+          py::arg("filename"), py::arg("header"))
+      .def_property_readonly(
+          "version", &llvm_rewrite_trace_iterator::get_version)
+      .def("get_next_event", &llvm_rewrite_trace_iterator::get_next_event);
 }
 
 PYBIND11_MODULE(_kllvm, m) {

include/kllvm/binary/ProofTraceParser.h

@@ -660,13 +660,13 @@ class proof_trace_parser {
 class llvm_rewrite_trace_iterator {
 private:
   uint32_t version_{};
-  proof_trace_buffer &buffer_;
+  std::unique_ptr<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);
+      std::unique_ptr<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);

include/kllvm/binary/deserializer.h

@@ -146,11 +146,11 @@ class proof_trace_memory_buffer : public proof_trace_buffer {
 
 class proof_trace_file_buffer : public proof_trace_buffer {
 private:
-  std::ifstream &file_;
+  std::ifstream file_;
 
 public:
-  proof_trace_file_buffer(std::ifstream &file)
-      : file_(file) { }
+  proof_trace_file_buffer(std::ifstream file)
+      : file_(std::move(file)) { }
 
   bool read(void *ptr, size_t len) override {
     file_.read((char *)ptr, len);

lib/binary/ProofTraceParser.cpp

@@ -116,30 +116,30 @@ void llvm_event::print(
 }
 
 llvm_rewrite_trace_iterator::llvm_rewrite_trace_iterator(
-    proof_trace_buffer &buffer, kore_header const &header)
-    : buffer_(buffer)
+    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_, version_)) {
     throw std::runtime_error("invalid header");
   }
 }
 
 std::optional<annotated_llvm_event>
 llvm_rewrite_trace_iterator::get_next_event() {
-  if (buffer_.eof()) {
+  if (buffer_->eof()) {
     return std::nullopt;
   }
   switch (type_) {
   case llvm_event_type::PreTrace: {
-    if (buffer_.has_word() && buffer_.peek_word() != config_sentinel) {
+    if (buffer_->has_word() && buffer_->peek_word() != config_sentinel) {
       llvm_event event;
-      if (!parser_.parse_event(buffer_, 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);
+    auto config = parser_.parse_config(*buffer_, pattern_len);
     if (!config) {
       throw std::runtime_error("could not parse config event");
     }
@@ -150,7 +150,7 @@ llvm_rewrite_trace_iterator::get_next_event() {
   }
   case llvm_event_type::Trace: {
     llvm_event event;
-    if (!parser_.parse_event(buffer_, event)) {
+    if (!parser_.parse_event(*buffer_, event)) {
       throw std::runtime_error("could not parse trace event");
     }
     return {{type_, event}};
@@ -207,7 +207,7 @@ proof_trace_parser::parse_proof_trace(std::string const &data) {
 std::optional<llvm_rewrite_trace>
 proof_trace_parser::parse_proof_trace_from_file(std::string const &filename) {
   std::ifstream file(filename, std::ios_base::binary);
-  proof_trace_file_buffer buffer(file);
+  proof_trace_file_buffer buffer(std::move(file));
   llvm_rewrite_trace trace;
   bool result = parse_trace(buffer, trace);
 

test/python/test_proof_trace.py

@@ -68,6 +68,38 @@ def test_file(self):
            # check that the third event is a configuration
            self.assertTrue(trace.trace[2].is_kore_pattern())
 
+        it = kllvm.prooftrace.llvm_rewrite_trace_iterator.from_file(binary_proof_trace, header)
+
+        while True:
+            event0 = it.get_next_event()
+            if event0.type != kllvm.prooftrace.LLVMEventType.PreTrace:
+                break
+
+        self.assertEqual(event0.type, kllvm.prooftrace.LLVMEventType.InitialConfig)
+        self.assertTrue(event0.event.is_kore_pattern())
+
+        event1 = it.get_next_event()
+        self.assertEqual(event1.type, kllvm.prooftrace.LLVMEventType.Trace)
+        self.assertTrue(event1.event.is_step_event())
+        rule_ordinal = event1.event.step_event.rule_ordinal
+        axiom = repr(definition.get_axiom_by_ordinal(rule_ordinal))
+        axiom_expected = self.get_pattern_from_ordinal(definition_text, rule_ordinal)
+        self.assertEqual(axiom, axiom_expected)
+
+        event2 = it.get_next_event()
+        self.assertEqual(event2.type, kllvm.prooftrace.LLVMEventType.Trace)
+        self.assertTrue(event2.event.is_step_event())
+        rule_ordinal = event2.event.step_event.rule_ordinal
+        axiom = repr(definition.get_axiom_by_ordinal(rule_ordinal))
+        axiom_expected = self.get_pattern_from_ordinal(definition_text, rule_ordinal)
+        self.assertEqual(axiom, axiom_expected)
+
+        event3 = it.get_next_event()
+        self.assertEqual(event3.type, kllvm.prooftrace.LLVMEventType.Trace)
+        self.assertTrue(event3.event.is_kore_pattern())
+
+        self.assertEqual(it.get_next_event(), None)
+
 
 if __name__ == "__main__":
     unittest.main()

tools/kore-proof-trace/main.cpp

@@ -42,8 +42,8 @@ int main(int argc, char **argv) {
 
   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);
+    llvm_rewrite_trace_iterator it(
+        std::make_unique<proof_trace_file_buffer>(std::move(file)), header);
     if (verbose_output) {
       it.print(std::cout, expand_terms_in_output);
     }