Feature request: Handling no_std/std extraction

[RaitoBezarius]

Code snippet:

Taking example from rust-lang/rfcs#2505, ignoring the unsafe part, which is not relevant to this issue.

#![no_std]

extern crate libm;

use core::ptr;

use libm::F32Ext;

#[no_mangle]
pub unsafe fn foo() {
    // volatile memory accesses to prevent the compiler from optimizing away everything
    let x: f32 = ptr::read_volatile(0x2000_0000 as *const _);
    let y = x.sqrt();
    ptr::write_volatile(0x2000_1000 as *mut _, y);
}

Without libm, a call to sqrt is not possible, but some libraries are offered in no_std / std variants, it may make sense to extract certain code with letting the user decide which level of std is available?

Current Charon output:

Not relevant as it fails earlier in the Rust compilation.

Extra context:

While no_std may be simpler, if certain functions are unavailable such as sqrt, ceil, ln, they need to be reimplemented via libm or LLVM intrinsics (which can translate to hardware optimized instructions or re-implement the function inline, see the RFC above), whether they are part of the extraction output should probably be a user choice.

std can be simpler also because it makes use of less unsafe or reuse more of the standard library which can already be verified and can be a simpler model of the code.

Desired behavior: A knob to control -Z build-std or similar during Charon extraction? (--rustc-flag could be enough but I'm not exactly sure.)

[Nadrieril]

I'm not sure what you'd like charon to do differently here, isn't that just an issue of setting up cargo/rustc properly? You can indeed pass cargo and rustc flags to charon with --rustc-arg and --cargo-arg.

[RaitoBezarius]

This is the bit I'm uncertain about, is there a way to tell rustc to extern crate std; to a certain crate?
Another way to see this issue is to add a --features flag but maybe you're right and we should just use --cargo-arg features=std in those cases.

[Nadrieril]

--cargo-arg does work for features. If you want to add the extern crate std;, you can pass --rustc-arg=--extern=std I think. Or you can add it in your source under a feature gate

[RaitoBezarius]

Thanks, I think this is all I needed. We can close this.