Merge branch 'master' into maude

INSTALL.md

@@ -23,6 +23,7 @@ sudo apt install      \
   pkg-config          \
   python3             \
   python3-pip         \
+  xxd                 \
   zlib1g-dev
 python3 -m pip install pybind11 lit
 ```

bin/llvm-kompile

@@ -27,6 +27,9 @@ Options:
   --python-output-dir PATH  Output directory to place automatically-named Python
                             modules. Only meaningful in "python" or "pythonast"
                             mode.
+  --embed PATH NAME         Embed additional information into shared library
+                            bindings. This is a low-level interface designed to
+                            be called from kompile. Only meaningful in "c" mode.
 
 Any option not listed above will be passed through to clang; use '--' to
 separate additional positional arguments to clang from those for $0.
@@ -71,6 +74,8 @@ kompile_clang_flags=()
 clang_args=()
 python_cmd=python3
 python_output_dir=""
+embedded_files=()
+embedded_names=()
 use_opt=false
 
 export verbose=false
@@ -125,10 +130,19 @@ while [[ $# -gt 0 ]]; do
       python_output_dir="$2"
       shift; shift
       ;;
+    --embed)
+      embedded_files+=("$2")
+      embedded_names+=("$3")
+      shift; shift; shift
+      ;;
     --)
       reading_clang_args=true
       shift
       ;;
+    -o)
+      kompile_clang_flags+=("$1" "$2")
+      shift; shift;
+      ;;
     -*)
       kompile_clang_flags+=("$1")
       shift
@@ -156,9 +170,10 @@ fi
 
 mod="$(mktemp tmp.XXXXXXXXXX)"
 modopt_tmp="$(mktemp tmp.XXXXXXXXXX)"
+tmpdir="$(mktemp -d tmp.XXXXXXXXXX)"
 modopt="$modopt_tmp"
 if [ "$save_temps" = false ]; then
-  trap 'rm -rf "$mod" "$modopt_tmp"' INT TERM EXIT
+  trap 'rm -rf "$mod" "$modopt_tmp" "$tmpdir"' INT TERM EXIT
 fi
 
 definition="${positional_args[0]}"
@@ -174,7 +189,7 @@ case "$definition" in
     ;;
 esac
 
-if [ "$compile" = "default" ]; then
+if [[ "$compile" = "default" ]]; then
   dt_dir="${positional_args[1]}"
   main="${positional_args[2]}"
 
@@ -183,8 +198,6 @@ if [ "$compile" = "default" ]; then
       -g)
         codegen_flags+=("--debug")
         ;;
-      *)
-        ;;
     esac
   done
 
@@ -232,6 +245,17 @@ if [[ "${python_output_dir}" == "" ]]; then
 fi
 kompile_clang_flags+=("--python-output-dir" "${python_output_dir}")
 
+embed_length="${#embedded_files[@]}"
+for (( idx = 0; idx < embed_length; idx++ )); do
+  name="${embedded_names[$idx]}"
+  file="${embedded_files[$idx]}"
+
+  cp "$file" "$tmpdir/$name"
+  (cd "$tmpdir"; xxd -i "$name" > "$name.cpp")
+
+  kompile_clang_flags+=("$tmpdir/$name.cpp")
+done
+
 run "$(dirname "$0")"/llvm-kompile-clang          \
   "$modopt" "$main"                               \
   @LLVM_KOMPILE_LTO@ -fno-stack-protector         \

bin/llvm-kompile-clang

@@ -116,6 +116,8 @@ esac
 
 LIBDIR="$(dirname "$0")/../lib/kllvm/"
 INCDIR="$(dirname "$0")/../include/"
+BINDIR="$(dirname "$0")"
+
 if [ "$main" = "main" ]; then
   MAINFILES="$LIBDIR"/llvm/main/main.ll
 elif [ "$main" = "search" ]; then

bin/llvm-kompile-testing

@@ -12,4 +12,4 @@ definition=$(realpath "$1")
 mode="$2"
 shift; shift
 ( cd "@PROJECT_SOURCE_DIR@"/matching && mvn exec:java -Dexec.args="$definition qbaL $dt_dir 1" -q )
-llvm-kompile "$definition" "$dt_dir" "$mode" -- "$@" -g
+llvm-kompile "$definition" "$dt_dir" "$mode" "$@" -g

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

@@ -39,6 +39,8 @@ typedef struct block block;
 
 char *kore_pattern_dump(kore_pattern const *);
 
+char *kore_pattern_pretty_print(kore_pattern const *);
+
 void kore_pattern_serialize(kore_pattern const *, char **, size_t *);
 
 void kore_pattern_free(kore_pattern const *);

bindings/c/lib.cpp

@@ -1,18 +1,27 @@
-#include <iostream>
-#include <memory>
+#include <kllvm-c/kllvm-c.h>
 
 #include <kllvm/ast/AST.h>
 #include <kllvm/binary/serializer.h>
 #include <kllvm/parser/KOREParser.h>
+#include <kllvm/printer/printer.h>
 
-#include <kllvm-c/kllvm-c.h>
+#define FMT_HEADER_ONLY
+#include <fmt/format.h>
 
-#include <runtime/arena.h>
+#include <filesystem>
+#include <fstream>
+#include <iostream>
+#include <memory>
+#include <optional>
+#include <unistd.h>
 
-// This header needs to be included last because it pollutes a number of macro
+// 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 fs = std::filesystem;
+
 // Internal implementation details
 namespace {
 
@@ -24,6 +33,15 @@ kore_pattern *kore_string_pattern_new_internal(std::string const &);
 kore_pattern *
 kore_pattern_new_token_internal(kore_pattern const *, kore_sort const *);
 
+struct pretty_print_definition {
+  std::string syntax;
+  std::string macros;
+};
+
+std::optional<pretty_print_definition> get_print_data();
+
+/* std::string load_dynamic_string(void *dylib, std::string const &symbol); */
+
 } // namespace
 
 /*
@@ -40,6 +58,17 @@ void *constructInitialConfiguration(const kllvm::KOREPattern *);
 
 extern "C" {
 
+/*
+ * These symbols may not have been compiled into the library (if
+ * `--embed-kprint` was not passed), and so we need to give them a weak default
+ * definition. If the embed flag was passed, the value of these symbols will be
+ * given by the embedded data.
+ */
+int kore_definition_syntax_len __attribute__((weak)) = -1;
+char kore_definition_syntax __attribute__((weak)) = -1;
+int kore_definition_macros_len __attribute__((weak)) = -1;
+char kore_definition_macros __attribute__((weak)) = -1;
+
 /* Completed types */
 
 struct kore_pattern {
@@ -62,6 +91,52 @@ char *kore_pattern_dump(kore_pattern const *pat) {
   return get_c_string(os);
 }
 
+char *kore_pattern_pretty_print(kore_pattern const *pat) {
+  char temp_dir_name[] = "tmp.pretty_print.XXXXXX";
+  auto temp_path = [&temp_dir_name](auto const &file) {
+    return fmt::format("{}/{}", temp_dir_name, file);
+  };
+
+  if (!mkdtemp(temp_dir_name)) {
+    return nullptr;
+  }
+
+  auto maybe_print_data = get_print_data();
+  if (!maybe_print_data) {
+    return nullptr;
+  }
+
+  auto [syntax, macros] = *maybe_print_data;
+
+  // Clean up ostreams at block scope exit
+  {
+    auto syntax_out
+        = std::ofstream(temp_path("syntaxDefinition.kore"), std::ios::out);
+    syntax_out << syntax;
+
+    auto macros_out = std::ofstream(temp_path("macros.kore"), std::ios::out);
+    macros_out << macros;
+
+    auto pattern_out = std::ofstream(temp_path("pattern.kore"), std::ios::out);
+    pat->ptr_->print(pattern_out);
+  }
+
+  auto ss = std::stringstream{};
+  kllvm::printKORE(
+      ss, temp_dir_name, temp_path("pattern.kore"), false, false, true);
+
+  fs::remove_all(temp_dir_name);
+
+  auto pretty_str = ss.str();
+  auto data
+      = static_cast<char *>(malloc(sizeof(char) * (pretty_str.size() + 1)));
+
+  std::copy(pretty_str.begin(), pretty_str.end(), data);
+  data[pretty_str.size()] = '\0';
+
+  return data;
+}
+
 void kore_pattern_serialize(
     kore_pattern const *pat, char **data_out, size_t *size_out) {
   auto out = kllvm::serializer();
@@ -397,4 +472,15 @@ kore_pattern *kore_pattern_new_token_internal(
   return pat;
 }
 
+std::optional<pretty_print_definition> get_print_data() {
+  if (kore_definition_macros_len == -1 || kore_definition_macros == -1
+      || kore_definition_syntax_len == -1 || kore_definition_syntax == -1) {
+    return std::nullopt;
+  }
+
+  return pretty_print_definition{
+      std::string(&kore_definition_syntax, kore_definition_syntax_len),
+      std::string(&kore_definition_macros, kore_definition_macros_len)};
+}
+
 } // namespace

nix/llvm-backend.nix

@@ -1,5 +1,5 @@
 { lib, src, cmake, coreutils, flex, fmt, pkgconfig, llvm, libllvm, libcxxabi, stdenv, boost, gmp
-, jemalloc, libffi, libiconv, libyaml, mpfr, ncurses, python39,
+, jemalloc, libffi, libiconv, libyaml, mpfr, ncurses, python39, unixtools,
 # Runtime dependencies:
 host,
 # Options:
@@ -14,7 +14,7 @@ stdenv.mkDerivation {
   nativeBuildInputs = [ cmake flex llvm pkgconfig ];
   buildInputs = [ libyaml ];
   propagatedBuildInputs = [
-    boost coreutils fmt gmp jemalloc libffi mpfr ncurses python-env
+    boost coreutils fmt gmp jemalloc libffi mpfr ncurses python-env unixtools.xxd
   ] ++ lib.optional stdenv.isDarwin libiconv;
 
   dontStrip = true;

runtime/arithmetic/int.cpp

@@ -80,6 +80,13 @@ SortInt hook_INT_sub(SortInt a, SortInt b) {
   return move_int(result);
 }
 
+SortInt hook_INT_neg(SortInt a) {
+  mpz_t result;
+  mpz_init(result);
+  mpz_neg(result, a);
+  return move_int(result);
+}
+
 SortInt hook_INT_tdiv(SortInt a, SortInt b) {
   mpz_t result;
   if (mpz_sgn(b) == 0) {

test/c/Inputs/api.c

@@ -2,6 +2,7 @@
 
 #include <assert.h>
 #include <dlfcn.h>
+#include <stdio.h>
 #include <stdlib.h>
 
 // Uses a GNU extension (fully supported by clang) to make the cast from dlsym
@@ -15,12 +16,14 @@
 struct kllvm_c_api load_c_api(char const *path) {
   void *lib = dlopen(path, RTLD_NOW);
   if (!lib) {
+    fprintf(stderr, "%s", dlerror());
     abort();
   }
 
   struct kllvm_c_api api;
 
   API_FUNCTION(kore_pattern_dump);
+  API_FUNCTION(kore_pattern_pretty_print);
   API_FUNCTION(kore_pattern_serialize);
   API_FUNCTION(kore_pattern_free);
   API_FUNCTION(kore_pattern_parse);

test/c/Inputs/api.h

@@ -5,6 +5,7 @@
 
 struct kllvm_c_api {
   char *(*kore_pattern_dump)(kore_pattern const *);
+  char *(*kore_pattern_pretty_print)(kore_pattern const *);
   void (*kore_pattern_serialize)(kore_pattern const *, char **, size_t *);
   void (*kore_pattern_free)(kore_pattern const *);
   kore_pattern *(*kore_pattern_parse)(char const *);

test/c/Inputs/print.c

@@ -0,0 +1,29 @@
+#include "api.h"
+
+#include <stdio.h>
+#include <stdlib.h>
+
+int main(int argc, char **argv) {
+  if (argc <= 1) {
+    return 1;
+  }
+
+  struct kllvm_c_api api = load_c_api(argv[1]);
+
+  api.kllvm_init();
+
+  kore_sort *sort_int = api.kore_composite_sort_new("SortInt");
+
+  kore_pattern *foo = api.kore_composite_pattern_new("Lblfoo");
+  kore_pattern *val = api.kore_pattern_new_token("423", sort_int);
+  api.kore_sort_free(sort_int);
+
+  api.kore_composite_pattern_add_argument(foo, val);
+  api.kore_pattern_free(val);
+
+  char *printed = api.kore_pattern_pretty_print(foo);
+  printf("%s", printed);
+  free(printed);
+
+  api.kore_pattern_free(foo);
+}

test/c/Inputs/printing/macros.kore

@@ -0,0 +1 @@
+// macros