From f2bbc3d7b6e4a9e2cb89aa9f1cffda5d7bf62c9d Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Mon, 3 Jun 2024 15:02:28 -0500 Subject: [PATCH] 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 --- bindings/python/ast.cpp | 26 ++++++++++++++++++++ include/kllvm/binary/ProofTraceParser.h | 4 ++-- include/kllvm/binary/deserializer.h | 6 ++--- lib/binary/ProofTraceParser.cpp | 18 +++++++------- test/python/test_proof_trace.py | 32 +++++++++++++++++++++++++ tools/kore-proof-trace/main.cpp | 4 ++-- 6 files changed, 74 insertions(+), 16 deletions(-) diff --git a/bindings/python/ast.cpp b/bindings/python/ast.cpp index a657512f9..e20c194e8 100644 --- a/bindings/python/ast.cpp +++ b/bindings/python/ast.cpp @@ -457,6 +457,32 @@ void bind_proof_trace(py::module_ &m) { py::class_>( proof_trace, "kore_header") .def(py::init(&kore_header::create), py::arg("path")); + + py::enum_(proof_trace, "LLVMEventType") + .value("PreTrace", llvm_event_type::PreTrace) + .value("InitialConfig", llvm_event_type::InitialConfig) + .value("Trace", llvm_event_type::Trace); + + py::class_(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>( + 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(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) { diff --git a/include/kllvm/binary/ProofTraceParser.h b/include/kllvm/binary/ProofTraceParser.h index 57139b6c3..2a6714708 100644 --- a/include/kllvm/binary/ProofTraceParser.h +++ b/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 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 buffer, kore_header const &header); [[nodiscard]] uint32_t get_version() const { return version_; } std::optional get_next_event(); void print(std::ostream &out, bool expand_terms, unsigned indent = 0U); diff --git a/include/kllvm/binary/deserializer.h b/include/kllvm/binary/deserializer.h index b47ba34a5..376495625 100644 --- a/include/kllvm/binary/deserializer.h +++ b/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); diff --git a/lib/binary/ProofTraceParser.cpp b/lib/binary/ProofTraceParser.cpp index 94af512d1..1c8869a75 100644 --- a/lib/binary/ProofTraceParser.cpp +++ b/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 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 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 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); diff --git a/test/python/test_proof_trace.py b/test/python/test_proof_trace.py index ce527e7e1..edd7ef875 100644 --- a/test/python/test_proof_trace.py +++ b/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() diff --git a/tools/kore-proof-trace/main.cpp b/tools/kore-proof-trace/main.cpp index 5e175d9e0..7af32d7c5 100644 --- a/tools/kore-proof-trace/main.cpp +++ b/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(std::move(file)), header); if (verbose_output) { it.print(std::cout, expand_terms_in_output); }