Translate LLVM modules lazily

[RyanGlScott]

Currently, crucible-llvm's translateModule function eagerly translates every function in an LLVM Module. For most applications, however, this is more work than is necessary, as verification will typically only use a subset of the definitions in the Module. For these sorts of applications, it would be more performant to defer the translation of each function until the simulator invokes the corresponding function for the first time.

To make things slightly more concrete, here is a sketch of how this could work:

1. When loading a Module, create a simple override for each function that invokes a special intrinsic. I'll tentatively propose the name "load_llvm_function" for this intrinsic. No actual translation happens at this point.
2. Simulation begins. When the simulator invokes a function for the first time, the load_llvm_function intrinsic translates the LLVM bitcode for that function, constructs an override from the resulting CFG, and replaces the current override for the function with the newly constructed one.
3. Finally, the simulator invokes the override containing the actual, translated function. Because the simulator now stores this new override, any subsequent invocations of the function will use that rather than having to go through load_llvm_function again.

The finer details of this plan still need to be pinned down, but I imagine that the evalStmt case for LLVM_LoadHandle will need to be changed. There is also a question of what to do with LLVM global variables—do these need to be translated lazily as well, or does it suffice to only give special treatment to functions?

This plan is very similar in spirit to GaloisInc/llvm-pretty-bc-parser#190, and indeed, implementing this plan will be necessary if we want to actually achieve the theoretical benefits of parsing LLVM bitcode on demand.

[robdockins]

PR #1006 implements a version of this using a different mechanism. It's not clear to me if we should close this bug now or not.

[RyanGlScott]

Ultimately, the mechanism above was just a sketch, and one that paraphrases an idea that you recalled to me in passing. The primary purpose of this issue was to track the idea of translating LLVM module lazily in some form or another, and I'd say that #1006 carries out that idea. Let's close this.