Add term simplification to Python bindings (#897)

This PR exposes the concrete term simplification routines already used
by the booster to the Python bindings so that they can be called from
Pyk. Specifically, it adds two free functions to the `runtime` module:
```python
simplify_pattern(Pattern, Sort) -> Pattern
simplify_bool_pattern(Pattern) -> bool
```

These are exposed as free functions because they depend on the runtime
library and so can't be automatically bound to the `Pattern` class as
methods; I suggest Pyk probably wants to monkey-patch them into its
`Pattern` class along with some kind of dynamic check for whether the
`runtime` module has been loaded or not.

Previously, the C and Python bindings didn't share a great deal of code;
the simplification routine is the first bit of non-trivial behaviour
that they need to share. I have therefore started a reorganisation of
the bindings code to extract as much functionality to a common library,
which has the additional benefit of reducing the amount of memory-leak
prone handling of C wrapper structures. To keep the diff in this PR
reasonable I have not completed this migration, but this is future work
that I will complete in a future PR.

A summary of the changes in this PR is as follows:
* Build a common bindings library that the C and Python bindings link
against.
* Extract the minimal set of features from the existing C bindings that
the Python bindings require to perform term simplification, and port the
C bindings over to calling the extracted common features.
* Add a test case to the Python bindings test suite that performs a few
small simplifications of sort `Int` and `Bool`; these are really just
smoke tests and Pyk should test the feature more thoroughly.

Author: Baltoli

bin/llvm-kompile-clang

@@ -236,6 +236,7 @@ if $link; then
     "$LIBDIR"/libcollections.a \
     "$LIBDIR"/libParser.a \
     "$LIBDIR"/libAST.a \
+    "$LIBDIR"/libBindingsCore.a \
     "$LIBDIR"/libBinaryKore.a \
     "$LIBDIR"/libKOREPrinter.a \
     "$LIBDIR"/liballoc.a \

bindings/CMakeLists.txt

@@ -1,2 +1,3 @@
 add_subdirectory(c)
+add_subdirectory(core)
 add_subdirectory(python)

bindings/c/CMakeLists.txt

@@ -7,6 +7,7 @@ target_include_directories(kllvm-c-static PUBLIC
 
 target_link_libraries(kllvm-c-static PUBLIC
   AST
+  BindingsCore
   util
   collect
 )

bindings/c/lib.cpp

@@ -2,10 +2,10 @@
 
 #include <kllvm/ast/AST.h>
 #include <kllvm/binary/serializer.h>
+#include <kllvm/bindings/core/core.h>
 #include <kllvm/parser/KOREParser.h>
 #include <kllvm/printer/printer.h>
 
-#define FMT_HEADER_ONLY
 #include <fmt/format.h>
 
 #include <filesystem>
@@ -53,7 +53,6 @@ extern "C" {
 block *take_steps(int64_t, block *);
 void initStaticObjects(void);
 void freeAllKoreMem(void);
-void *constructInitialConfiguration(const kllvm::KOREPattern *);
 }
 
 extern "C" {
@@ -186,14 +185,8 @@ kore_pattern *kore_pattern_new_token_with_len(
 
 kore_pattern *kore_pattern_new_injection(
     kore_pattern const *term, kore_sort const *from, kore_sort const *to) {
-  auto inj_sym = kore_symbol_new("inj");
-  kore_symbol_add_formal_argument(inj_sym, from);
-  kore_symbol_add_formal_argument(inj_sym, to);
-
-  auto inj = kore_composite_pattern_from_symbol(inj_sym);
-  kore_composite_pattern_add_argument(inj, term);
-
-  kore_symbol_free(inj_sym);
+  auto inj = new kore_pattern;
+  inj->ptr_ = kllvm::bindings::make_injection(term->ptr_, from->ptr_, to->ptr_);
   return inj;
 }
 
@@ -243,7 +236,7 @@ kore_pattern *kore_pattern_desugar_associative(kore_pattern const *pat) {
 }
 
 block *kore_pattern_construct(kore_pattern const *pat) {
-  return static_cast<block *>(constructInitialConfiguration(pat->ptr_.get()));
+  return kllvm::bindings::construct_term(pat->ptr_);
 }
 
 char *kore_block_dump(block *term) {
@@ -258,53 +251,24 @@ char *kore_block_dump(block *term) {
 }
 
 kore_pattern *kore_pattern_from_block(block *term) {
-  auto ast = termToKorePattern(term);
-
   auto pat = new kore_pattern;
-  pat->ptr_ = ast;
+  pat->ptr_ = kllvm::bindings::term_to_pattern(term);
   return pat;
 }
 
 bool kore_block_get_bool(block *term) {
-  assert((((uintptr_t)term) & 1) == 0);
-  return *(bool *)term->children;
+  return kllvm::bindings::get_bool(term);
 }
 
 bool kore_simplify_bool(kore_pattern const *pattern) {
-  auto bool_sort = kore_composite_sort_new("SortBool");
-  auto kitem_sort = kore_composite_sort_new("SortKItem");
-
-  auto inj = kore_pattern_new_injection(pattern, bool_sort, kitem_sort);
-  auto ret = kore_block_get_bool(kore_pattern_construct(inj));
-
-  kore_sort_free(bool_sort);
-  kore_sort_free(kitem_sort);
-  kore_pattern_free(inj);
-
-  return ret;
+  return kllvm::bindings::simplify_to_bool(pattern->ptr_);
 }
 
 void kore_simplify(
     kore_pattern const *pattern, kore_sort const *sort, char **data_out,
     size_t *size_out) {
-  auto kitem_sort = kore_composite_sort_new("SortKItem");
-  auto kitem_sort_str = kore_sort_dump(kitem_sort);
-
-  auto block = [&] {
-    if (kore_sort_is_kitem(sort) || kore_sort_is_k(sort)) {
-      return kore_pattern_construct(pattern);
-    } else {
-      auto inj = kore_pattern_new_injection(pattern, sort, kitem_sort);
-      auto ret = kore_pattern_construct(inj);
-      kore_pattern_free(inj);
-      return ret;
-    }
-  }();
-
-  serializeConfiguration(block, kitem_sort_str, data_out, size_out, true);
-
-  kore_sort_free(kitem_sort);
-  free(kitem_sort_str);
+  auto block = kllvm::bindings::simplify_to_term(pattern->ptr_, sort->ptr_);
+  serializeConfiguration(block, "SortKItem{}", data_out, size_out, true);
 }
 
 void kore_simplify_binary(
@@ -370,21 +334,11 @@ bool kore_sort_is_concrete(kore_sort const *sort) {
 }
 
 bool kore_sort_is_kitem(kore_sort const *sort) {
-  if (auto composite
-      = dynamic_cast<kllvm::KORECompositeSort *>(sort->ptr_.get())) {
-    return composite->getName() == "SortKItem";
-  }
-
-  return false;
+  return kllvm::bindings::is_sort_kitem(sort->ptr_);
 }
 
 bool kore_sort_is_k(kore_sort const *sort) {
-  if (auto composite
-      = dynamic_cast<kllvm::KORECompositeSort *>(sort->ptr_.get())) {
-    return composite->getName() == "SortK";
-  }
-
-  return false;
+  return kllvm::bindings::is_sort_k(sort->ptr_);
 }
 
 /* KORECompositeSort */

bindings/core/CMakeLists.txt

@@ -0,0 +1,12 @@
+add_library(BindingsCore
+  src/core.cpp
+)
+
+target_link_libraries(BindingsCore
+  PUBLIC AST fmt::fmt-header-only
+)
+
+install(
+  TARGETS BindingsCore
+  ARCHIVE DESTINATION lib/kllvm
+)

bindings/core/src/core.cpp

@@ -0,0 +1,83 @@
+#include <kllvm/bindings/core/core.h>
+
+using namespace kllvm;
+
+/*
+ * These declarations are internal to the backend and aren't exposed explicitly
+ * through any header files, so we pull them in manually here.
+ */
+extern "C" {
+void *constructInitialConfiguration(const KOREPattern *);
+}
+
+namespace kllvm::bindings {
+
+std::shared_ptr<KOREPattern> make_injection(
+    std::shared_ptr<KOREPattern> term, std::shared_ptr<KORESort> from,
+    std::shared_ptr<KORESort> to) {
+  auto inj_sym = KORESymbol::Create("inj");
+
+  inj_sym->addFormalArgument(from);
+  inj_sym->addFormalArgument(to);
+
+  auto inj = KORECompositePattern::Create(std::move(inj_sym));
+  inj->addArgument(term);
+
+  return inj;
+}
+
+block *construct_term(std::shared_ptr<KOREPattern> const &pattern) {
+  return static_cast<block *>(constructInitialConfiguration(pattern.get()));
+}
+
+std::shared_ptr<KOREPattern> term_to_pattern(block *term) {
+  return termToKorePattern(term);
+}
+
+bool get_bool(block *term) {
+  assert((((uintptr_t)term) & 1) == 0);
+  return *(bool *)term->children;
+}
+
+bool simplify_to_bool(std::shared_ptr<KOREPattern> pattern) {
+  auto bool_sort = KORECompositeSort::Create("SortBool");
+  auto kitem_sort = KORECompositeSort::Create("SortKItem");
+
+  auto inj = make_injection(pattern, bool_sort, kitem_sort);
+  return get_bool(construct_term(inj));
+}
+
+block *simplify_to_term(
+    std::shared_ptr<KOREPattern> pattern, std::shared_ptr<KORESort> sort) {
+  auto kitem_sort = KORECompositeSort::Create("SortKItem");
+
+  if (is_sort_kitem(sort) || is_sort_k(sort)) {
+    return construct_term(pattern);
+  } else {
+    auto inj = make_injection(pattern, sort, kitem_sort);
+    return construct_term(inj);
+  }
+}
+
+std::shared_ptr<KOREPattern>
+simplify(std::shared_ptr<KOREPattern> pattern, std::shared_ptr<KORESort> sort) {
+  return term_to_pattern(simplify_to_term(pattern, sort));
+}
+
+bool is_sort_kitem(std::shared_ptr<KORESort> const &sort) {
+  if (auto composite = std::dynamic_pointer_cast<KORECompositeSort>(sort)) {
+    return composite->getName() == "SortKItem";
+  }
+
+  return false;
+}
+
+bool is_sort_k(std::shared_ptr<KORESort> const &sort) {
+  if (auto composite = std::dynamic_pointer_cast<KORECompositeSort>(sort)) {
+    return composite->getName() == "SortK";
+  }
+
+  return false;
+}
+
+} // namespace kllvm::bindings

bindings/python/CMakeLists.txt

@@ -25,6 +25,7 @@ target_link_libraries(_kllvm PUBLIC
 target_link_libraries(kllvm-python-static PUBLIC
   AST
   util
+  BindingsCore
 )
 
 install(FILES $<TARGET_FILE:kllvm-python-static>

bindings/python/runtime.cpp

@@ -1,4 +1,5 @@
 #include <kllvm/ast/AST.h>
+#include <kllvm/bindings/core/core.h>
 
 #include <pybind11/pybind11.h>
 
@@ -46,6 +47,15 @@ void *constructInitialConfiguration(const KOREPattern *initial);
 void bind_runtime(py::module_ &m) {
   auto runtime = m.def_submodule("runtime", "K LLVM backend runtime");
 
+  // This simplification should really be a member function on the Python
+  // Pattern class, but it depends on the runtime library and so needs to be
+  // bound as a free function in the kllvm.runtime module.
+  m.def(
+      "simplify_pattern",
+      [](std::shared_ptr<KOREPattern> pattern, std::shared_ptr<KORESort> sort) {
+        return bindings::simplify(pattern, sort);
+      });
+
   // This class can't be used directly from Python; the mutability semantics
   // that we get from the Pybind wrappers make it really easy to break things.
   // We therefore have to wrap it up in some external Python code; see

include/kllvm/bindings/core/core.h

@@ -0,0 +1,40 @@
+#ifndef BINDINGS_CORE_H
+#define BINDINGS_CORE_H
+
+#include <kllvm/ast/AST.h>
+
+#include <memory>
+
+// These headers need to be included last because they pollute a number of macro
+// definitions into the global namespace.
+#include <runtime/arena.h>
+#include <runtime/header.h>
+
+namespace kllvm::bindings {
+
+std::shared_ptr<kllvm::KOREPattern> make_injection(
+    std::shared_ptr<kllvm::KOREPattern> term,
+    std::shared_ptr<kllvm::KORESort> from, std::shared_ptr<kllvm::KORESort> to);
+
+block *construct_term(std::shared_ptr<kllvm::KOREPattern> const &pattern);
+
+std::shared_ptr<kllvm::KOREPattern> term_to_pattern(block *term);
+
+bool get_bool(block *term);
+
+bool simplify_to_bool(std::shared_ptr<kllvm::KOREPattern> pattern);
+
+block *simplify_to_term(
+    std::shared_ptr<kllvm::KOREPattern> pattern,
+    std::shared_ptr<kllvm::KORESort> sort);
+
+std::shared_ptr<kllvm::KOREPattern> simplify(
+    std::shared_ptr<kllvm::KOREPattern> pattern,
+    std::shared_ptr<kllvm::KORESort> sort);
+
+bool is_sort_kitem(std::shared_ptr<kllvm::KORESort> const &sort);
+bool is_sort_k(std::shared_ptr<kllvm::KORESort> const &sort);
+
+} // namespace kllvm::bindings
+
+#endif

runtime/util/ConfigurationPrinter.cpp

@@ -301,14 +301,6 @@ void printSortedConfigurationToFile(
   printConfigurationInternal(&w, subject, sort, false, &state);
 }
 
-std::shared_ptr<kllvm::KOREPattern> termToKorePattern(block *subject) {
-  auto *kore_str = printConfigurationToString(subject);
-  auto kore = std::string(kore_str->data, len(kore_str));
-
-  auto parser = kllvm::parser::KOREParser::from_string(kore);
-  return parser->pattern();
-}
-
 extern "C" void printMatchResult(
     std::ostream &os, MatchLog *matchLog, size_t logSize,
     const std::string &definitionPath) {

runtime/util/ConfigurationSerializer.cpp

@@ -1,4 +1,5 @@
 #include <kllvm/ast/AST.h>
+#include <kllvm/binary/deserializer.h>
 #include <kllvm/binary/serializer.h>
 #include <kllvm/parser/KOREParser.h>
 
@@ -450,3 +451,11 @@ void serializeRawTermToFile(
   fwrite(data, 1, size, file);
   fclose(file);
 }
+
+std::shared_ptr<kllvm::KOREPattern> termToKorePattern(block *subject) {
+  char *data_out;
+  size_t size_out;
+
+  serializeConfiguration(subject, "SortKItem{}", &data_out, &size_out, true);
+  return deserialize_pattern(data_out, data_out + size_out);
+}