runtimeverification / llvm-backend

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

Add MapIter and SetIter sort categories #1080

Closed dwightguth closed 1 month ago

dwightguth commented 1 month ago

This is the first of a sequence of PRs designed to make progress towards generating stack maps so that we can trigger the GC during allocation rather than in between rewrite steps only. The first few PRs will be preliminaries that add small features that will be used by future PRs.

This PR adds a SetIter and MapIter sort category. These sort categories are needed because the stack may contain references to live sets and maps through these iterators that need to be relocated by the GC. However, no K terms will ever be created with these sort categories, so a lot of the code cases currently in the code deliberately do not handle these categories. Future PRs will add GC code to handle fixing up the pointer to a collection contained in these iterators.