With a conservative analysis it's possible to make an underestimation on the names one can remove. This shouldn't be done on object files but at a level where program flow information is still preserved. A flow-independent analysis using a superset lattice over the callable names should do the trick for a first-order implementation that will look good enough compared to shipping 37mb for google authentication. Further you could make it flow-sensitive for a more accurate analysis with the caveat that the runtime will be significantly longer.

Control flow graphs are well-studied, critical parts of most compilers. The halting problem involves complexity of semantics in loops and jumps, but it’s possible to understand what loops may run just fine, without being able to decide exactly when a loop may exit.

In many cases Clang and GCC compiler can easily understand loops, and even reduce them to constant time.