In a nutshell it would build a dependency graph first using simplified algorithm that only looked at imports. Then it would pick a function, eval types statement by statement (I think that's what you call symbolic execution), and if any named value as result would expand the list of possible types it could have, all the functions that use that value (global var, passed as argument, etc) would be queued for reevaluation. Until either the set of possible types for all values is steady or some reevaluation limit is reached.