Add option to extract opaque bodies

[Nadrieril]

With --extract-opaque-bodies, we now also extract foreign globals, methods, trait provided methods, and ADT definitions. This is limited by two things:

• not all function bodies have a MIR in the crate data (only inlineable and generic functions do);
• when function have MIR available it's only optimized MIR, which we don't support as well.

This PR includes a few tests that fail because of other problems. Two of them are hax limitations that I'm ignoring until we're back on hax master. I opened issues for the other two: #123, #120.

The PR also includes many improvements to the ui tests that I needed along the way.

Fixes #114

[sonmarcho]

The fact that we can't always retrieve the bodies of the external functions makes the effects of this PR quite limited, unfortunately. I wonder how the Kani people do, as I thought Kani looked into the bodies of the external definitions (@zhassan-aws could you comment on that?).
This being said, all the improvements you added to the UI tests are good and most welcome.

[Nadrieril]

We could pass -Zalways-encode-mir (or -Zcross-crate-inline-threshold=yes?) to dependencies, I think this ensures we get the MIR for everything (while we're at it, -Zno-codegen avoids generating code we don't need).

This doesn't work for std though; for that, this proposal might be the solution, as it proposes shipping a std with full MIR: rust-lang/compiler-team#738. Or we could ship our own MIR-only sysroot.

[zhassan-aws]

The fact that we can't always retrieve the bodies of the external functions makes the effects of this PR quite limited, unfortunately. I wonder how the Kani people do, as I thought Kani looked into the bodies of the external definitions (@zhassan-aws could you comment on that?).

In Kani, we run the kani-compiler on each of the dependent crates to generate the MIR only. Then, when compiling the target user crate, the kani-compiler has access to the MIR of all the dependent crates. This also applies to std, but it's handled in a special way.

See this RFC and one of the PRs that implements it for more information.

Feel free to reach out for further information.

[Nadrieril]

Thank you for these links!

[sonmarcho]

This is useful documentation, thanks!

[sonmarcho]

Looks good: it indeed makes sense to do check once and for all in translate_body whether we should extract the body or not.