Merge branch 'develop' into fix-side-condition-bug

bindings/python/ast.cpp

@@ -459,7 +459,7 @@ void bind_proof_trace(py::module_ &m) {
       .def_property_readonly("trace", &llvm_rewrite_trace::get_trace)
       .def_static(
           "parse",
-          [](py::bytes const &bytes, kore_header const &header) {
+          [](py::bytes const &bytes, std::shared_ptr<kore_header> &header) {
             proof_trace_parser parser(false, false, header);
             auto str = std::string(bytes);
             return parser.parse_proof_trace(str, false);
@@ -486,7 +486,8 @@ void bind_proof_trace(py::module_ &m) {
       .def("__repr__", print_repr_adapter<llvm_rewrite_trace_iterator>(true))
       .def_static(
           "from_file",
-          [](std::string const &filename, kore_header const &header) {
+          [](std::string const &filename,
+             std::shared_ptr<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)),

include/kllvm/binary/ProofTraceParser.h

@@ -328,7 +328,7 @@ class proof_trace_parser {
 private:
   bool verbose_;
   bool expand_terms_;
-  [[maybe_unused]] kore_header const &header_;
+  [[maybe_unused]] std::shared_ptr<kore_header> header_;
   [[maybe_unused]] std::optional<kore_definition> kore_definition_
       = std::nullopt;
 
@@ -342,7 +342,7 @@ class proof_trace_parser {
         || magic[3] != '2') {
       return nullptr;
     }
-    auto result = detail::read_v2(buffer, header_, pattern_len);
+    auto result = detail::read_v2(buffer, *header_, pattern_len);
     pattern_len += 4;
     return result;
   }
@@ -701,7 +701,7 @@ class proof_trace_parser {
 
 public:
   proof_trace_parser(
-      bool verbose, bool expand_terms, kore_header const &header,
+      bool verbose, bool expand_terms, std::shared_ptr<kore_header> header,
       std::optional<kore_definition> kore_definition = std::nullopt);
 
   std::optional<llvm_rewrite_trace> parse_proof_trace_from_file(
@@ -723,7 +723,8 @@ class llvm_rewrite_trace_iterator {
 
 public:
   llvm_rewrite_trace_iterator(
-      std::unique_ptr<proof_trace_buffer> buffer, kore_header const &header);
+      std::unique_ptr<proof_trace_buffer> buffer,
+      std::shared_ptr<kore_header> header);
   [[nodiscard]] uint32_t get_version() const { return version_; }
   std::optional<annotated_llvm_event> get_next_event();
   void print(

lib/binary/ProofTraceParser.cpp

@@ -130,9 +130,10 @@ void llvm_event::print(
 }
 
 llvm_rewrite_trace_iterator::llvm_rewrite_trace_iterator(
-    std::unique_ptr<proof_trace_buffer> buffer, kore_header const &header)
+    std::unique_ptr<proof_trace_buffer> buffer,
+    std::shared_ptr<kore_header> header)
     : buffer_(std::move(buffer))
-    , parser_(false, false, header) {
+    , parser_(false, false, std::move(header)) {
   if (!proof_trace_parser::parse_header(*buffer_, kind_, version_)) {
     throw std::runtime_error("invalid header");
   }
@@ -250,11 +251,11 @@ void llvm_rewrite_trace::print(
 }
 
 proof_trace_parser::proof_trace_parser(
-    bool verbose, bool expand_terms, kore_header const &header,
+    bool verbose, bool expand_terms, std::shared_ptr<kore_header> header,
     std::optional<kore_definition> kore_definition)
     : verbose_(verbose)
     , expand_terms_(expand_terms)
-    , header_(header)
+    , header_(std::move(header))
     , kore_definition_(std::move(kore_definition)) { }
 
 std::optional<llvm_rewrite_trace> proof_trace_parser::parse_proof_trace(

tools/kore-proof-trace/main.cpp

@@ -51,7 +51,7 @@ int main(int argc, char **argv) {
   cl::ParseCommandLineOptions(argc, argv);
 
   FILE *in = fopen(header_path.getValue().c_str(), "r");
-  kore_header header(in);
+  auto header = std::make_shared<kore_header>(in);
   fclose(in);
 
   if (use_streaming_parser) {