runtimeverification / llvm-backend

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

merge allocations in same basic block up to a size bound #1125

Closed dwightguth closed 3 months ago

dwightguth commented 3 months ago

Previously, when we were allocating a large term, we would issue a number of repeated calls to kore_alloc. This is inefficient because it has to check whether there is enough space and execute a branch instruction on each allocation. It is more efficient if we do one, larger call to kore_alloc for all the memory that we need.

In order to efficiently implement this, we modify the way we generate calls to kore_alloc in the code generator so that it will place the allocation function at the beginning of the basic block and then, if further allocations are required in the same basic block, it will modify the call to the allocation function so it requests a larger amount of memory. This only happens up to a certain bound, in order to prevent memory from being wasted due to requesting particularly large chunks of memory. In practice, this leads to most apply_rule functions only calling kore_alloc once.