Refactor k-rule-apply tool (#1110)

This PR is a preparatory refactoring that will enable me to fix a
problematic bug in the Kasmer project; I've factored out the changes
here because they include other related cleanups not directly relevant
to the bug I'm fixing in the subsequent PR.

Currently, the `k-rule-apply` tool is explicitly linked against the KORE
AST library in order for it to be able to parse a KORE definition and
search for an axiom with a particular label. This works fine, but on
changing the way that the LLVM backend is linked on macOS, this AST
linkage caused a subtle bug to manifest because of the way that
`k-rule-apply` uses `dlopen` to inspect a shared library compiled by the
backend.[^1]

The fix here is to remove the explicit dependency of this tool on the
AST + Parser libraries, and instead push all the required behaviour of
the tool into the C bindings so that it can be used fully with `dlopen`.

The changes in this PR are as follows:
- Reorganise the existing code in the `k-rule-apply` tool to be more
hygienic in its usage of header files etc.
- Push calls to the KORE parser library and references to the KORE AST
structures out in favour of C-linkage calls to the bindings module,
which is available and compiled into the same shared library as we're
already `dlopen`ing.
- Extract the one non-trivial usage of the AST library (mapping rule
labels to matching function names via their axiom) into the core C
bindings.
- Remove the dependency of this tool on the AST and Parser libraries,
finally enabling the downstream bugfix that motivated this change in the
first place.

[^1]: I have a full writeup of this on the way; in the context of this
PR the specifics aren't important.

Author: Baltoli

bindings/c/include/kllvm-c/kllvm-c.h

@@ -162,6 +162,18 @@ void kllvm_free_all_memory(void);
 
 bool kllvm_mutable_bytes_enabled(void);
 
+/* Definitions */
+
+/**
+ * Parse the given KORE definition, then if any of its axioms have a `label`
+ * attribute that matches the supplied label, return the name of the function
+ * symbol that attempts matching a pattern against that axiom (and will
+ * therefore populate the backend's global matching log).
+ *
+ * If no such axiom exists, return `nullptr`.
+ */
+char *kore_match_function_name(char const *defn_path, char const *label);
+
 #ifdef __cplusplus
 }
 #endif

bindings/c/lib.cpp

@@ -434,6 +434,17 @@ void kllvm_free_all_memory(void) {
 bool kllvm_mutable_bytes_enabled(void) {
   return hook_BYTES_mutableBytesEnabled();
 }
+
+/* Definitions */
+
+char *kore_match_function_name(char const *defn_path, char const *label) {
+  auto result = kllvm::bindings::get_match_function_name(defn_path, label);
+  if (!result) {
+    return nullptr;
+  }
+
+  return get_c_string(*result);
+}
 }
 
 namespace {

bindings/core/CMakeLists.txt

@@ -3,7 +3,7 @@ add_library(BindingsCore
 )
 
 target_link_libraries(BindingsCore
-  PUBLIC AST fmt::fmt-header-only
+  PUBLIC AST Parser fmt::fmt-header-only
 )
 
 install(

bindings/core/src/core.cpp

@@ -1,4 +1,5 @@
 #include <kllvm/bindings/core/core.h>
+#include <kllvm/parser/KOREParser.h>
 
 using namespace kllvm;
 
@@ -116,4 +117,25 @@ bool is_sort_k(std::shared_ptr<kore_sort> const &sort) {
   return false;
 }
 
+std::optional<std::string> get_match_function_name(
+    std::string const &definition_path, std::string const &label) {
+  // Parse the definition.kore to get the AST.
+  parser::kore_parser parser(definition_path);
+  auto kore_ast = parser.definition();
+  kore_ast->preprocess();
+
+  // Iterate through axioms and return the one with the give rulen label if exits.
+  for (auto *axiom : kore_ast.get()->get_axioms()) {
+    // Check if the current axiom has the attribute label.
+    if (axiom->attributes().contains(attribute_set::key::Label)) {
+      // Compare the axiom's label with the given rule label.
+      if (label == axiom->attributes().get_string(attribute_set::key::Label)) {
+        return "intern_match_" + std::to_string(axiom->get_ordinal());
+      }
+    }
+  }
+
+  return std::nullopt;
+}
+
 } // namespace kllvm::bindings

include/kllvm/ast/AST.h

@@ -1034,7 +1034,8 @@ class kore_definition {
   }
   kore_symbol *get_inj_symbol() { return inj_symbol_; }
 
-  std::vector<kore_composite_sort *> const &get_all_sorts() const {
+  [[nodiscard]] std::vector<kore_composite_sort *> const &
+  get_all_sorts() const {
     return all_sorts_;
   }
 };

include/kllvm/bindings/core/core.h

@@ -4,6 +4,7 @@
 #include <kllvm/ast/AST.h>
 
 #include <memory>
+#include <optional>
 
 // These headers need to be included last because they pollute a number of macro
 // definitions into the global namespace.
@@ -41,6 +42,13 @@ bool is_sort_k(std::shared_ptr<kllvm::kore_sort> const &sort);
 std::shared_ptr<kore_pattern>
 evaluate_function(std::shared_ptr<kore_composite_pattern> const &term);
 
+/**
+ * Get the name of the LLVM function that attempts matching on the rule with
+ * this label by parsing a KORE definition and examining its axioms.
+ */
+std::optional<std::string> get_match_function_name(
+    std::string const &definition_path, std::string const &label);
+
 } // namespace kllvm::bindings
 
 #endif

tools/k-rule-apply/CMakeLists.txt

@@ -1,9 +1,6 @@
 kllvm_add_tool(k-rule-apply
   main.cpp
-)
-
-target_link_libraries(k-rule-apply 
-  PUBLIC Parser AST gmp gmpxx
+  shims.cpp
 )
 
 install(

tools/k-rule-apply/auxiliar.h

@@ -1,4 +1,14 @@
-#include "auxiliar.h"
+#include "shims.h"
+
+#include <llvm/Support/CommandLine.h>
+
+#include <cstdlib>
+#include <dlfcn.h>
+#include <fstream>
+#include <iostream>
+#include <optional>
+
+#include "runtime/header.h"
 
 using namespace llvm;
 using namespace kllvm;
@@ -20,43 +30,10 @@ cl::opt<std::string> kore_pattern_filename(
 cl::opt<std::string> shared_lib_path(
     cl::Positional, cl::desc("<path_to_shared_lib>"), cl::cat(k_rule_cat));
 
-std::optional<std::string> get_match_function_name() {
-  auto definition = kompiled_dir + "/definition.kore";
-  // Parse the definition.kore to get the AST.
-  parser::kore_parser parser(definition);
-  auto kore_ast = parser.definition();
-  kore_ast->preprocess();
-
-  // Iterate through axioms and return the one with the give rulen label if exits.
-  for (auto *axiom : kore_ast.get()->get_axioms()) {
-    // Check if the current axiom has the attribute label.
-    if (axiom->attributes().contains(attribute_set::key::Label)) {
-      // Compare the axiom's label with the given rule label.
-      if (rule_label
-          == axiom->attributes().get_string(attribute_set::key::Label)) {
-        return "intern_match_" + std::to_string(axiom->get_ordinal());
-      }
-    }
-  }
-  std::cerr << rule_label << "\n";
-  return std::nullopt;
-}
-
 int main(int argc, char **argv) {
   cl::HideUnrelatedOptions({&k_rule_cat});
   cl::ParseCommandLineOptions(argc, argv);
 
-  // Parse the given KORE Pattern and get the block* to use as input for the
-  // match function.
-  parser::kore_parser parser(kore_pattern_filename.getValue());
-  auto initial_configuration = parser.pattern();
-
-  auto match_function_name = get_match_function_name();
-  if (!match_function_name.has_value()) {
-    std::cerr << "Rule with label " << rule_label << " does not exist.\n";
-    return EXIT_FAILURE;
-  }
-
   // Open the shared library that contains the llvm match functions.
   auto *handle = dlopen(shared_lib_path.c_str(), RTLD_LAZY);
 
@@ -66,30 +43,36 @@ int main(int argc, char **argv) {
     return EXIT_FAILURE;
   }
 
+  auto *match_function_name = get_match_function_name(
+      kompiled_dir + "/definition.kore", rule_label, handle);
+  if (!match_function_name) {
+    std::cerr << "Rule with label " << rule_label << " does not exist.\n";
+    return EXIT_FAILURE;
+  }
+
   // Get util function from the shared lib, cast it to its right type, and call
   // with its appropriate argument if any.
-  void *match_function_ptr = dlsym(handle, match_function_name->c_str());
-  if (match_function_ptr == nullptr) {
+  auto *match_function
+      = reinterpret_cast<void (*)(block *)>(dlsym(handle, match_function_name));
+  if (!match_function) {
     std::cerr << "Error: " << dlerror() << "\n";
     dlclose(handle);
     return EXIT_FAILURE;
   }
 
-  // NOLINTNEXTLINE(*-reinterpret-cast)
-  auto match_function = reinterpret_cast<void (*)(block *)>(match_function_ptr);
-
-  reset_match_reason(handle);
   init_static_objects(handle);
-  auto *b
-      = construct_initial_configuration(initial_configuration.get(), handle);
-  if (b == nullptr) {
+  reset_match_reason(handle);
+
+  auto *b = parse_initial_configuration(kore_pattern_filename, handle);
+  if (!b) {
     std::cerr << "Error: " << dlerror() << "\n";
     return EXIT_FAILURE;
   }
 
-  match_function((block *)b);
+  match_function(b);
+
   auto *log = getmatch_log(handle);
-  if (log == nullptr) {
+  if (!log) {
     std::cerr << "Error: " << dlerror() << "\n";
     return EXIT_FAILURE;
   }
@@ -101,7 +84,8 @@ int main(int argc, char **argv) {
   }
 
   print_match_result(
-      std::cout, (match_log *)log, log_size, kompiled_dir, handle);
+      std::cout, reinterpret_cast<match_log *>(log), log_size, kompiled_dir,
+      handle);
 
   dlclose(handle);
   return 0;