Implement serialization/deserialization of new algorithm

bindings/python/ast.cpp

@@ -439,12 +439,16 @@ void bind_proof_trace(py::module_ &m) {
       .def_property_readonly("trace", &llvm_rewrite_trace::get_trace)
       .def_static(
           "parse",
-          [](py::bytes const &bytes) {
-            proof_trace_parser parser(false, false);
+          [](py::bytes const &bytes, kore_header const &header) {
+            proof_trace_parser parser(false, false, header);
             auto str = std::string(bytes);
             return parser.parse_proof_trace(str);
           },
-          py::arg("bytes"));
+          py::arg("bytes"), py::arg("header"));
+
+  py::class_<kore_header, std::shared_ptr<kore_header>>(
+      proof_trace, "kore_header")
+      .def(py::init(&kore_header::create), py::arg("path"));
 }
 
 PYBIND11_MODULE(_kllvm, m) {

include/kllvm/binary/ProofTraceParser.h

@@ -265,6 +265,7 @@ class proof_trace_parser {
 private:
   bool verbose_;
   bool expand_terms_;
+  [[maybe_unused]] kore_header const &header_;
 
   // Caller needs to check that there are at least 8 bytes remaining in the
   // stream before peeking
@@ -337,30 +338,19 @@ class proof_trace_parser {
 
   template <typename It>
   sptr<kore_pattern> parse_kore_term(It &ptr, It end, uint64_t &pattern_len) {
-    if (std::distance(ptr, end) < 11U) {
+    if (std::distance(ptr, end) < 9U) {
       return nullptr;
     }
+    It old_ptr = ptr;
     if (detail::read<char>(ptr, end) != '\x7F'
         || detail::read<char>(ptr, end) != 'K'
-        || detail::read<char>(ptr, end) != 'O'
         || detail::read<char>(ptr, end) != 'R'
-        || detail::read<char>(ptr, end) != 'E') {
+        || detail::read<char>(ptr, end) != '2') {
       return nullptr;
     }
-    auto version = detail::read_version(ptr, end);
-
-    if (!read_uint64(ptr, end, pattern_len)) {
-      return nullptr;
-    }
-
-    if (std::distance(ptr, end) < pattern_len) {
-      return nullptr;
-    }
-    if (pattern_len > 0 && std::distance(ptr, end) > pattern_len) {
-      end = std::next(ptr, pattern_len);
-    }
-
-    return detail::read(ptr, end, version);
+    auto result = detail::read_v2(ptr, end, header_);
+    pattern_len = ptr - old_ptr;
+    return result;
   }
 
   template <typename It>
@@ -736,7 +726,8 @@ class proof_trace_parser {
   }
 
 public:
-  proof_trace_parser(bool verbose, bool expand_terms);
+  proof_trace_parser(
+      bool verbose, bool expand_terms, kore_header const &header);
 
   std::optional<llvm_rewrite_trace>
   parse_proof_trace_from_file(std::string const &filename);

include/kllvm/binary/deserializer.h

@@ -6,13 +6,36 @@
 #include <kllvm/binary/version.h>
 
 #include <cstddef>
+#include <cstdio>
 #include <cstring>
 #include <vector>
 
 #include <iostream>
 
 namespace kllvm {
 
+class kore_header {
+private:
+  std::vector<uint8_t> arities_;
+  std::vector<ptr<kore_symbol>> symbols_;
+
+public:
+  kore_header(FILE *in);
+  static std::unique_ptr<kore_header> create(std::string const &path) {
+    FILE *f = fopen(path.c_str(), "rb");
+    auto *result = new kore_header(f);
+    fclose(f);
+    return std::unique_ptr<kore_header>(result);
+  }
+
+  [[nodiscard]] uint8_t get_arity(uint32_t offset) const {
+    return arities_[offset];
+  };
+  [[nodiscard]] kore_symbol *get_symbol(uint32_t offset) const {
+    return symbols_[offset].get();
+  };
+};
+
 namespace detail {
 
 template <typename It>
@@ -249,6 +272,35 @@ sptr<kore_pattern> read(It &ptr, It end, binary_version version) {
   return term_stack[0];
 }
 
+template <typename It>
+sptr<kore_pattern> read_v2(It &ptr, It end, kore_header const &header) {
+  switch (peek(ptr)) {
+  case 0: {
+    ++ptr;
+    auto len = detail::read<uint64_t>(ptr, end);
+    auto str = std::string((char *)&*ptr, (char *)(&*ptr + len));
+    ptr += len + 1;
+    return kore_string_pattern::create(str);
+  }
+  case 1: {
+    ++ptr;
+    auto offset = detail::read<uint32_t>(ptr, end);
+    auto arity = header.get_arity(offset);
+    // TODO: we need to check if this PR is an `inj` symbol and adjust the
+    // second sort parameter of the symbol to be equal to the sort of the
+    // current pattern.
+    auto symbol = header.get_symbol(offset);
+    auto new_pattern = kore_composite_pattern::create(symbol);
+    for (auto i = 0; i < arity; ++i) {
+      auto child = read_v2(ptr, end, header);
+      new_pattern->add_argument(child);
+    }
+    return new_pattern;
+  }
+  default: throw std::runtime_error("Bad term " + std::to_string(*ptr));
+  }
+}
+
 } // namespace detail
 
 std::string file_contents(std::string const &fn, int max_bytes = -1);

include/kllvm/codegen/ProofEvent.h

@@ -52,15 +52,6 @@ class proof_event {
       kore_composite_sort &sort, llvm::Value *output_file, llvm::Value *term,
       llvm::BasicBlock *insert_at_end);
 
-  /*
-   * Emit a call that will serialize `config` to the specified `outputFile` as
-   * binary KORE. This function does not require a sort, but the configuration
-   * passed must be a top-level configuration.
-   */
-  llvm::CallInst *emit_serialize_configuration(
-      llvm::Value *output_file, llvm::Value *config,
-      llvm::BasicBlock *insert_at_end);
-
   /*
    * Emit a call that will serialize `value` to the specified `outputFile`.
    */

include/runtime/header.h

@@ -331,13 +331,16 @@ void serialize_configurations(
 void serialize_configuration(
     block *subject, char const *sort, char **data_out, size_t *size_out,
     bool emit_size, bool use_intern);
+void serialize_configuration_v2(FILE *file, block *subject, uint32_t sort);
 void serialize_configuration_to_file(
     FILE *file, block *subject, bool emit_size, bool use_intern);
+void serialize_configuration_to_file_v2(FILE *file, block *subject);
 void write_uint64_to_file(FILE *file, uint64_t i);
 void write_bool_to_file(FILE *file, bool b);
 void serialize_term_to_file(
     FILE *file, void *subject, char const *sort, bool use_intern,
     bool k_item_inj = false);
+void serialize_term_to_file_v2(FILE *file, void *subject, uint64_t, bool);
 void serialize_raw_term_to_file(
     FILE *file, void *subject, char const *sort, bool use_intern);
 void print_variable_to_file(FILE *file, char const *varname);
@@ -360,6 +363,7 @@ bool hook_STRING_eq(SortString, SortString);
 char const *get_symbol_name_for_tag(uint32_t tag);
 char const *get_return_sort_for_tag(uint32_t tag);
 char const **get_argument_sorts_for_tag(uint32_t tag);
+uint32_t *get_argument_sorts_for_tag_v2(uint32_t tag);
 char const *top_sort(void);
 
 bool symbol_is_instantiation(uint32_t tag);
@@ -382,6 +386,19 @@ using visitor = struct {
       writer *, rangemap *, char const *, char const *, char const *, void *);
 };
 
+using serialize_visitor = struct {
+  void (*visit_config)(writer *, block *, uint32_t, bool);
+  void (*visit_map)(writer *, map *, uint32_t, uint32_t, uint32_t);
+  void (*visit_list)(writer *, list *, uint32_t, uint32_t, uint32_t);
+  void (*visit_set)(writer *, set *, uint32_t, uint32_t, uint32_t);
+  void (*visit_int)(writer *, mpz_t, uint32_t);
+  void (*visit_float)(writer *, floating *, uint32_t);
+  void (*visit_bool)(writer *, bool, uint32_t);
+  void (*visit_string_buffer)(writer *, stringbuffer *, uint32_t);
+  void (*visit_m_int)(writer *, size_t *, size_t, uint32_t);
+  void (*visit_range_map)(writer *, rangemap *, uint32_t, uint32_t, uint32_t);
+};
+
 void print_map(
     writer *, map *, char const *, char const *, char const *, void *);
 void print_range_map(
@@ -392,6 +409,8 @@ void print_list(
     writer *, list *, char const *, char const *, char const *, void *);
 void visit_children(
     block *subject, writer *file, visitor *printer, void *state);
+void visit_children_for_serialize(
+    block *subject, writer *file, serialize_visitor *printer);
 
 stringbuffer *hook_BUFFER_empty(void);
 stringbuffer *hook_BUFFER_concat(stringbuffer *buf, string *s);
@@ -442,4 +461,16 @@ void sfprintf(writer *file, char const *fmt, Args &&...args) {
   }
 }
 
+template <typename... Args>
+void sfwrite(void const *ptr, size_t size, size_t nmemb, writer *file) {
+  if (file->file) {
+    fwrite(ptr, size, nmemb, file->file);
+  } else {
+    std::string output;
+    output.resize(size * nmemb);
+    memcpy(output.data(), ptr, size * nmemb);
+    hook_BUFFER_concat_raw(file->buffer, output.data(), output.size());
+  }
+}
+
 #endif // RUNTIME_HEADER_H

lib/ast/definition.cpp

@@ -76,12 +76,19 @@ std::string get_raw_symbol_name(sort_category cat) {
 
 void kore_definition::insert_reserved_symbols() {
   auto mod = kore_module::create("K-RAW-TERM");
+  // syntax KItem ::= rawTerm(KItem)
   auto decl = kore_symbol_declaration::create("rawTerm", true);
+  // syntax KItem ::= rawKTerm(K)
+  auto k_decl = kore_symbol_declaration::create("rawKTerm", true);
   auto kitem = kore_composite_sort::create("SortKItem");
+  auto k = kore_composite_sort::create("SortK");
 
   decl->get_symbol()->add_sort(kitem);
   decl->get_symbol()->add_argument(kitem);
+  k_decl->get_symbol()->add_sort(kitem);
+  k_decl->get_symbol()->add_argument(k);
   mod->add_declaration(std::move(decl));
+  mod->add_declaration(std::move(k_decl));
 
   for (auto const &cat : hooked_sorts_) {
     switch (cat.first.cat) {

lib/binary/ProofTraceParser.cpp

@@ -125,9 +125,11 @@ void llvm_rewrite_trace::print(
   }
 }
 
-proof_trace_parser::proof_trace_parser(bool verbose, bool expand_terms)
+proof_trace_parser::proof_trace_parser(
+    bool verbose, bool expand_terms, kore_header const &header)
     : verbose_(verbose)
-    , expand_terms_(expand_terms) { }
+    , expand_terms_(expand_terms)
+    , header_(header) { }
 
 std::optional<llvm_rewrite_trace>
 proof_trace_parser::parse_proof_trace(std::string const &data) {

lib/binary/deserializer.cpp

@@ -37,4 +37,85 @@ sptr<kore_pattern> deserialize_pattern(std::string const &filename) {
   return deserialize_pattern(data.begin(), data.end());
 }
 
+// NOLINTNEXTLINE(*-cognitive-complexity)
+kore_header::kore_header(FILE *in) {
+  // NOLINTNEXTLINE(misc-redundant-expression)
+  if (fgetc(in) != 0x7f || fgetc(in) != 'K' || fgetc(in) != 'R'
+      || fgetc(in) != '2') {
+    throw std::runtime_error("invalid magic");
+  }
+  std::array<uint32_t, 4> num_entries{};
+  if (fread(num_entries.data(), sizeof(uint32_t), 4, in) != 4) {
+    throw std::runtime_error("invalid table header");
+  }
+  uint32_t version = num_entries[0];
+  uint32_t nstrings = num_entries[1];
+  uint32_t nsorts = num_entries[2];
+  uint32_t nsymbols = num_entries[3];
+
+  if (version != 1) {
+    throw std::runtime_error("invalid binary version");
+  }
+
+  std::vector<std::string> strings;
+  strings.reserve(nstrings);
+
+  for (uint32_t i = 0; i < nstrings; ++i) {
+    uint32_t len = 0;
+    if (fread(&len, sizeof(uint32_t), 1, in) != 1) {
+      throw std::runtime_error("invalid string table length");
+    }
+    std::string str;
+    str.resize(len);
+    if (fread(str.data(), 1, len, in) != len) {
+      throw std::runtime_error("invalid string table entry");
+    }
+    fgetc(in);
+    strings.push_back(str);
+  }
+
+  std::vector<sptr<kore_sort>> sorts;
+  sorts.reserve(nsorts);
+
+  for (uint32_t i = 0; i < nsorts; ++i) {
+    uint32_t offset = 0;
+    if (fread(&offset, sizeof(uint32_t), 1, in) != 1) {
+      throw std::runtime_error("invalid string table offset in sort table");
+    }
+    uint8_t nparams = fgetc(in);
+    auto sort = kore_composite_sort::create(strings[offset]);
+    for (uint8_t j = 0; j < nparams; j++) {
+      uint32_t param_offset = 0;
+      if (fread(&param_offset, sizeof(uint32_t), 1, in) != 1
+          || param_offset >= i) {
+        throw std::runtime_error("invalid sort table offset in sort table");
+      }
+      sort->add_argument(sorts[param_offset]);
+    }
+    sorts.push_back(sort);
+  }
+
+  arities_.reserve(nsymbols);
+  symbols_.reserve(nsymbols);
+
+  for (uint32_t i = 0; i < nsymbols; ++i) {
+    uint32_t offset = 0;
+    if (fread(&offset, sizeof(uint32_t), 1, in) != 1) {
+      throw std::runtime_error("invalid string table offset in symbol table");
+    }
+    uint8_t nparams = fgetc(in);
+    uint8_t arity = fgetc(in);
+    auto symbol = kore_symbol::create(strings[offset]);
+    for (uint8_t j = 0; j < nparams; j++) {
+      uint32_t param_offset = 0;
+      if (fread(&param_offset, sizeof(uint32_t), 1, in) != 1) {
+        throw std::runtime_error("invalid sort table offset in symbol table");
+      }
+      symbol->add_formal_argument(sorts[param_offset]);
+    }
+    symbols_.push_back(std::move(symbol));
+    arities_.push_back(arity);
+  }
+}
+
 } // namespace kllvm