runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
34 stars 19 forks source link

Further cleanup GC code for map/list/set #1086

Closed dwightguth closed 1 month ago

dwightguth commented 1 month ago

This is a further cleanup of the code used to deal with map/list/set objects that are returned by functions and not immediately placed into a term. Previously, these objects lived on the alwaysgcspace and were promoted to the youngspace by placing them as a child of a special placeholder symbol if they survived to a collection cycle. However, this had the undesirable trait that it breaks the invariant originally imagined by the alwaysgcspace that it should not contain any allocations that might survive past the beginning of the next rewrite step.

Because of this, we were unable to separate the alwaysgcspace clear operation from the garbage collection cycle, something that is required for the sequence of GC refactorings I am in the progress of. To fix this, we simply change the way we allocate such map/list/set terms such that we allocate them directly to the youngspace as special placeholder symbols, rather than going through the intermediary of the alwaysgcspace. This resets the expectations that ultimately lead to the alwaysgcspace having the property that allocations might survive past the end of the current rewrite step, which allows us to make a further cleanup in the next PR which automatically resets and clears the space after every rewrite step.