I didn't really phrase this particularly well: I meant that you cannot determine this stuff at compile time because it is inherently a runtime analysis. Of course the compiler could emit the Miri interpreter into a binary if people chose to put the pieces togehter that way.