Feature request: Stdlib and foreign function bodies?

[giltho]

Hello,

Not quite sure about that one, we've found a few issues, PRs, and mentions to Kani, but the question is: what's the path towards being able to get ULLBC for the entirety of the code (including stdlib, which I know Kani handles in a different way).

We don't necessarily need anything pruned as a first approach, happy with charon loading absolutely everything if that's tractable.

Cheers!

[Nadrieril]

In principle that's not hard, I can iterate over all the loaded crates. That would be a natural extension of https://github.com/AeneasVerif/charon/issues/336. What's your usecase?

[giltho]

In principle, something similar to Kani really. One of the analyses we want to try and implement would require exhaustive access to the code one would be executing. Also, out of curiosity, I can see Kani now vendors Charon. What's the usage there? Should we do something similar?

[Nadrieril]

In principle, something similar to Kani really.

I don't actually know what Kani does here, doesn't Kani use monomorphized code?

One of the analyses we want to try and implement would require exhaustive access to the code one would be executing.

Ah, that's different! If you just want to have all the code that could be reached from your crate, you can pass --include '*' to charon today.

Also, out of curiosity, I can see Kani now vendors Charon. What's the usage there?

They don't quite vendor charon, they're using charon as a dependency so that they can emit LLBC. I believe they wanted to reuse charon's control-flow reconstruction pass and experiment with the aeneas backend.

Should we do something similar?

How are you using charon today?

[N1ark]

Hi! I'm the person working on the project involving Charon :) The issue right now is that, e.g. when wanting to analyse a simple hello world, the (U)LLBC uses the function std::io::stdio::_print<0>(core::fmt::Arguments<0>), which is opaque.

The command I'm using right now is charon --mir_optimized --rustc-arg=--extern=std --extract-opaque-bodies --no-cargo --input %s --dest-file %s; tried adding --include '*', but of course print remains opaque. From what I understand, Kani re-compiles the std crate (source) -- would adding this to Charon, possibly as a flag, be an option?

[giltho]

Also, re this

I don't actually know what Kani does here, doesn't Kani use monomorphized code?

Yes, and we have two projects, one of them might require monomorphized code (at least as a start, and then we can maybe get polymorphism in).

[Nadrieril]

I see, thanks for the Kani link. Compared to Kani at the time this was written, we already do the reachability analysis, but we have the same issue of only being able to translate function bodies that have been compiled by charon, i.e. everything except the standard library.

Today we don't yet translate all function bodies in non-std dependent crates even with --extract-opaque-bodies because we don't pass -Zalways-encode-mir to dependencies, but that's on my todo list and not hard.

On the other hand, being able to retreive the MIR for std functions would require us to ship our own MIR sysroot like Kani. This is not in our medium-term plans at the moment.

[Nadrieril]

Actually before thinking of shipping that ourselves, you may be able to get what you want by rebuilding the stdlib yourselves with -Zalways-encode-mir (like Miri and Kani do) and see if something like charon --extract-opaque-bodies --rustc-arg="--sysroot=/path/to/custom-built-sysroot/" can be made to work.

[N1ark]

Oh this seems promising, thank you very much! I have other things I need to get working before getting to this, but I'll definitely keep this in mind for later on, thank you very much :)

[Nadrieril]

I managed to reuse miri to get a usable full-MIR std!

Here's what I tried:

• rustup component add miri;
• cargo miri setup -v --print-sysroot builds a std with -Zalways-encode-mir;
• pass this path to charon --extract-opaque-bodies --rustc-arg=--sysroot=<miri sysroot>.

This works! Well except that I get tons of errors because we don't yet handle later MIRs (#543), but the basic idea works: I get access to the bodies of stdlib functions. Hence once #543 is done you might get what you want.

[N1ark]

Oh that's so great to hear! Thanks a ton, I'm busy with other things but Ill try this out soon, looks super promising and would solve some problems, thank you : )

[giltho]

This can be closed right?

[Nadrieril]

I'd like Charon to do this automatically eventually

[Nadrieril]

Closing in favor of https://github.com/AeneasVerif/charon/issues/865 which contains instructions.