Conditional compilation flag for GC strategy.

runtimeverification · Dec 6, 2024 · 01c324b · 01c324b
1 parent f23039a
commit 01c324b
Show file tree

Hide file tree

Showing 5 changed files with 23 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/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) {