Merge remote-tracking branch 'origin/develop'

runtimeverification · Sep 30, 2024 · e829263 · e829263
2 parents b830daa + 315f1d4
commit e829263
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 8 deletions.
diff --git a/debug/kgdb.py b/debug/kgdb.py
@@ -671,6 +671,8 @@ def kllvm_lookup_function(val):
                 kind = t.tag
             else:
                 kind = t.name
+            if not kind:
+                return None
             if kind.startswith('immer::list'):
                 return termPrinter(val.address, "list", "SortList{}")
             elif kind.startswith('immer::set'):

diff --git a/include/runtime/collect.h b/include/runtime/collect.h
@@ -38,7 +38,7 @@ void migrate_rangemap(void *m);
 void migrate_set(void *s);
 void migrate_collection_node(void **node_ptr);
 void set_kore_memory_functions_for_gmp(void);
-void kore_collect(void **, uint8_t, layoutitem *);
+void kore_collect(void **, uint8_t, layoutitem *, bool force = false);
 }
 
 #ifdef GC_DBG

diff --git a/lib/codegen/Decision.cpp b/lib/codegen/Decision.cpp
@@ -1106,14 +1106,15 @@ std::pair<std::vector<llvm::Value *>, llvm::BasicBlock *> step_function_header(
       llvm::FunctionType::get(
           llvm::Type::getVoidTy(module->getContext()),
           {arr->getType(), llvm::Type::getInt8Ty(module->getContext()), ptr_ty,
-           ptr_ty},
+           ptr_ty, llvm::Type::getInt1Ty(module->getContext())},
           false));
   auto *call = llvm::CallInst::Create(
       kore_collect,
       {arr,
        llvm::ConstantInt::get(
            llvm::Type::getInt8Ty(module->getContext()), nroots),
-       llvm::ConstantExpr::getBitCast(layout, ptr_ty)},
+       llvm::ConstantExpr::getBitCast(layout, ptr_ty),
+       llvm::ConstantInt::getFalse(module->getContext())},
       "", collect);
   set_debug_loc(call);
   std::vector<llvm::Value *> phis;

diff --git a/runtime/alloc/arena.cpp b/runtime/alloc/arena.cpp
@@ -122,7 +122,7 @@ static void fresh_block(struct arena *arena) {
       BLOCK_SIZE - sizeof(memory_block_header));
 }
 
-bool gc_enabled;
+bool gc_enabled = true;
 
 __attribute__((noinline)) void *
 do_alloc_slow(size_t requested, struct arena *arena) {

diff --git a/runtime/collect/collect.cpp b/runtime/collect/collect.cpp
@@ -280,7 +280,11 @@ void init_static_objects(void) {
   set_kore_memory_functions_for_gmp();
 }
 
-void kore_collect(void **roots, uint8_t nroots, layoutitem *type_info) {
+void kore_collect(
+    void **roots, uint8_t nroots, layoutitem *type_info, bool force) {
+  if (!force && !gc_enabled) {
+    return;
+  }
   is_gc = true;
   time_for_collection = false;
   collect_old = should_collect_old_gen();
@@ -350,7 +354,7 @@ void kore_collect(void **roots, uint8_t nroots, layoutitem *type_info) {
 }
 
 void free_all_kore_mem() {
-  kore_collect(nullptr, 0, nullptr);
+  kore_collect(nullptr, 0, nullptr, true);
   kore_clear();
 }
 }
diff --git a/runtime/util/ConfigurationParser.cpp b/runtime/util/ConfigurationParser.cpp
@@ -98,6 +98,7 @@ struct construction {
 
 // NOLINTNEXTLINE(*-cognitive-complexity)
 extern "C" void *construct_initial_configuration(kore_pattern const *initial) {
+  bool enabled = gc_enabled;
   gc_enabled = false;
   std::vector<std::variant<kore_pattern const *, construction>> work_list{
       initial};
@@ -157,14 +158,15 @@ extern "C" void *construct_initial_configuration(kore_pattern const *initial) {
     }
   }
 
-  gc_enabled = true;
+  gc_enabled = enabled;
   return output[0];
 }
 
 // NOLINTBEGIN(*-cognitive-complexity)
 template <typename It>
 static void *
 deserialize_initial_configuration(It ptr, It end, binary_version version) {
+  bool enabled = gc_enabled;
   gc_enabled = false;
   using namespace kllvm::detail;
   auto begin = ptr;
@@ -256,7 +258,7 @@ deserialize_initial_configuration(It ptr, It end, binary_version version) {
     }
   }
 
-  gc_enabled = true;
+  gc_enabled = enabled;
   assert(output.size() == 1 && "Output stack left in invalid state");
   return output.front();
 }