New GC strategy. (#1175)

This PR adds a new GCStrategy, that treats any pointer with address space other than 0 as a pointer to managed memory. We extent class GCStrategy in llvm/IR/GCStrategy.h, and register the new GCStrategy.
runtimeverification · Dec 9, 2024 · 8de42ea · 8de42ea
1 parent dd25f06
commit 8de42ea
Show file tree

Hide file tree

Showing 11 changed files with 126 additions and 0 deletions.
diff --git a/bin/llvm-kompile b/bin/llvm-kompile
@@ -42,6 +42,7 @@ Options:
                                     (immutable) that are enabled by default.
   --hidden-visibility               Set the visibility of all global symbols in generated code to
                                     "hidden"
+  --use-gcstrategy                  Use GC strategy defined for the LLVM backend.
   --profile-matching                Instrument interpeter to emit a profile of time spent in
                                     top-level rule matching on stderr.
   --verify-ir                       Verify result of IR generation.
@@ -197,6 +198,11 @@ while [[ $# -gt 0 ]]; do
       kompile_clang_flags+=("--hidden-visibility")
       shift
       ;;
+    --use-gcstrategy)
+      codegen_flags+=("--use-gcstrategy")
+      kompile_clang_flags+=("--use-gcstrategy")
+      shift
+      ;;
     --profile-matching)
       codegen_flags+=("--profile-matching")
       codegen_verify_flags+=("--profile-matching")

diff --git a/bin/llvm-kompile-clang b/bin/llvm-kompile-clang
@@ -15,6 +15,7 @@ flags=()
 llc_flags=()
 llc_opt_flags="-O0"
 visibility_hidden=false
+use_gcstrategy=false
 link=true
 export verbose=false
 export profile=false
@@ -101,6 +102,10 @@ while [[ $# -gt 0 ]]; do
       visibility_hidden=true
       shift
       ;;
+    --use-gcstrategy)
+      use_gcstrategy=true
+      shift
+      ;;
     *)
       ;;
   esac
@@ -188,6 +193,9 @@ if [ "$main" != "python_ast" ]; then
         run @OPT@ "$modopt" -load-pass-plugin "$passes" -set-visibility-hidden -o "$modhidden"
         modopt="$modhidden"
       fi
+      if $use_gcstrategy; then
+        llc_flags+=("-load="$passes"")
+      fi
       run @LLC@ \
         "$modopt" -mtriple=@BACKEND_TARGET_TRIPLE@ \
         -filetype=obj "$llc_opt_flags" "${llc_flags[@]}" -o "$modasm"

diff --git a/include/kllvm/codegen/GCStrategy.h b/include/kllvm/codegen/GCStrategy.h
@@ -0,0 +1,37 @@
+//===- Extend GCStrategy of llvm/CodeGen/GCStrategy.h ---------------------===//
+//
+// We extend the base GCStrategy as follows:
+// - use gc.safepoints instead of (default) gc.roots.
+// - specify that the RewriteStatepointsForGC pass should rewrite the calls of
+//   this function.
+// - pointers with address space != 0 are pointing to GC-managed memory.
+//===----------------------------------------------------------------------===//
+
+// NOLINTBEGIN
+
+#ifndef LLVM_BACKEND_GC_STRATEGY_H
+#define LLVM_BACKEND_GC_STRATEGY_H
+
+#include "llvm/IR/GCStrategy.h"
+#include "llvm/IR/Type.h"
+
+namespace kllvm {
+
+/// The GCStrategy for the LLVM Backend
+class LLVMBackendGCStrategy : public llvm::GCStrategy {
+public:
+  LLVMBackendGCStrategy();
+
+  // Override
+#if LLVM_VERSION_MAJOR == 15
+  llvm::Optional<bool> isGCManagedPointer(llvm::Type const *Ty) const override;
+#else
+  std::optional<bool> isGCManagedPointer(llvm::Type const *Ty) const override;
+#endif
+};
+
+} // namespace kllvm
+
+#endif // LLVM_BACKEND_GC_STRATEGY_H
+
+// NOLINTEND
diff --git a/include/kllvm/codegen/Options.h b/include/kllvm/codegen/Options.h
@@ -10,6 +10,7 @@ extern llvm::cl::opt<bool> no_optimize;
 extern llvm::cl::opt<bool> emit_object;
 extern llvm::cl::opt<bool> binary_ir;
 extern llvm::cl::opt<bool> force_binary;
+extern llvm::cl::opt<bool> use_gcstrategy;
 extern llvm::cl::opt<bool> proof_hint_instrumentation;
 extern llvm::cl::opt<bool> proof_hint_instrumentation_slow;
 extern llvm::cl::opt<bool> keep_frame_pointer;

diff --git a/lib/codegen/CreateTerm.cpp b/lib/codegen/CreateTerm.cpp
@@ -1,6 +1,7 @@
 #include "kllvm/codegen/CreateTerm.h"
 #include "kllvm/codegen/CreateStaticTerm.h"
 #include "kllvm/codegen/Debug.h"
+#include "kllvm/codegen/Options.h"
 #include "kllvm/codegen/ProofEvent.h"
 #include "kllvm/codegen/Util.h"
 
@@ -1224,6 +1225,9 @@ bool make_function(
       = llvm::FunctionType::get(return_type, param_types, false);
   llvm::Function *apply_rule = get_or_insert_function(module, name, func_type);
   apply_rule->setLinkage(llvm::GlobalValue::InternalLinkage);
+  if (use_gcstrategy) {
+    apply_rule->setGC("gcs-llvm-backend");
+  }
   init_debug_axiom(axiom->attributes());
   std::string debug_name = name;
   if (axiom->attributes().contains(attribute_set::key::Label)) {

diff --git a/lib/codegen/Options.cpp b/lib/codegen/Options.cpp
@@ -48,6 +48,10 @@ cl::opt<bool> force_binary(
     "f", cl::desc("Force binary bitcode output to stdout"), cl::Hidden,
     cl::cat(codegen_lib_cat));
 
+cl::opt<bool> use_gcstrategy(
+    "use-gcstrategy", cl::desc("Use GC strategy defined for the LLVM backend."),
+    cl::Hidden, cl::init(false), cl::cat(codegen_lib_cat));
+
 namespace kllvm {
 
 void validate_codegen_args(bool is_tty) {

diff --git a/lib/passes/CMakeLists.txt b/lib/passes/CMakeLists.txt
@@ -2,13 +2,15 @@ add_library(KLLVMPassInternal
   SetVisibilityHidden.cpp
   RemoveDeadKFunctions.cpp
   MustTailDeadArgElimination.cpp
+  GCStrategy.cpp
   PluginInfo.cpp
 )
 
 add_library(KLLVMPass MODULE
   SetVisibilityHidden.cpp
   RemoveDeadKFunctions.cpp
   MustTailDeadArgElimination.cpp
+  GCStrategy.cpp
   PluginInfo.cpp
 )
 

diff --git a/lib/passes/GCStrategy.cpp b/lib/passes/GCStrategy.cpp
@@ -0,0 +1,52 @@
+//===- Extend GCStrategy of llvm/CodeGen/GCStrategy.h ---------------------===//
+//
+// We extend the base GCStrategy as follows:
+// - use gc.safepoints instead of (default) gc.roots.
+// - specify that the RewriteStatepointsForGC pass should rewrite the calls of
+//   this function.
+// - pointers with address space != 0 are pointing to GC-managed memory.
+//===----------------------------------------------------------------------===//
+
+// NOLINTBEGIN
+
+#include "kllvm/codegen/GCStrategy.h"
+
+#include "llvm/CodeGen/GCMetadata.h"
+#include "llvm/IR/DerivedTypes.h"
+#include "llvm/Support/Compiler.h"
+
+using namespace llvm;
+using namespace kllvm;
+
+LLVMBackendGCStrategy::LLVMBackendGCStrategy() {
+  UseStatepoints = true; // Use gc.statepoints
+#if LLVM_VERSION_MAJOR != 15
+  UseRS4GC = true; // Rewrite the calls of a function that has this GCStrategy
+#endif
+}
+
+// Override
+#if LLVM_VERSION_MAJOR == 15
+llvm::Optional<bool>
+LLVMBackendGCStrategy::isGCManagedPointer(Type const *Ty) const {
+#else
+std::optional<bool>
+LLVMBackendGCStrategy::isGCManagedPointer(Type const *Ty) const {
+#endif
+  // Return false for any non-pointer type
+  if (!Ty->isPointerTy()) {
+    return false;
+  }
+  // Any pointer with address space != 0 is to managed memory.
+  PointerType const *PTy = dyn_cast<PointerType>(Ty);
+  if (PTy->getAddressSpace()) {
+    return true;
+  }
+  return false;
+}
+
+// Add LLVMBackendGCStrategy to the global GCRegistry
+static GCRegistry::Add<LLVMBackendGCStrategy>
+    X("gcs-llvm-backend", "GC Strategy for the LLVM Backend");
+
+// NOLINTEND
diff --git a/test/defn/imp.kore b/test/defn/imp.kore
@@ -1,6 +1,8 @@
 // RUN: %interpreter
 // RUN: %check-grep
 // RUN: %check-statistics
+// RUN: %gcs-interpreter
+// RUN: %check-grep
 // RUN: %proof-interpreter
 // RUN: %check-proof-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/defn/k-files/imp.md)")]

diff --git a/test/lit.cfg.py b/test/lit.cfg.py
@@ -98,6 +98,13 @@ def exclude_x86_and_llvm18(s):
             exit 1
         fi
     ''')),
+    ('%gcs-interpreter', one_line('''
+        output=$(%kompile %s main --use-gcstrategy -o %t.interpreter 2>&1)
+        if [[ -n "$output" ]]; then
+            echo "llvm-kompile error or warning: $output"
+            exit 1
+        fi
+    ''')),
     ('%proof-interpreter', one_line('''
         output=$(%kompile %s main --proof-hint-instrumentation -o %t.interpreter 2>&1)
         if [[ -n "$output" ]]; then

diff --git a/tools/llvm-kompile-codegen/main.cpp b/tools/llvm-kompile-codegen/main.cpp
@@ -1,3 +1,4 @@
+#include "kllvm/codegen/GCStrategy.h"
 #include <kllvm/ast/AST.h>
 #include <kllvm/codegen/ApplyPasses.h>
 #include <kllvm/codegen/CreateTerm.h>
@@ -147,6 +148,8 @@ void emit_metadata(llvm::Module &mod) {
 
 // NOLINTNEXTLINE(*-cognitive-complexity)
 int main(int argc, char **argv) {
+  // NOLINTNEXTLINE(*-identifier-naming)
+  LLVMBackendGCStrategy _gcs; // Unused. This is needed to ensure linking.
   initialize_llvm();
 
   cl::HideUnrelatedOptions({&codegen_tool_cat, &codegen_lib_cat});