Global ASM is not supported

[danielsn]

Following LLVM, Rust allows global ASM in a module. This means that crates can have arbitrary code that we cannot analyze.

Likelihood

We know of crates that use this feature

Mitigation

We could fail any crate that uses this feature, but this would block any use of those crates, even if they did not use any of the risky features. Even worse, this would block all consumers of such crates, from even compiling, again even if they do not use any of the dangerous features.

Unlike for inline ASM in a function, where we can insert assert(0) as a mechanism to guarantee soundness, there is no obvious way to only fail code paths that use the injected ASM.

• Raise a warning if global asm appears
• Incorporate that warning into viewer

Path to soundness

• Support ASM in CBMC

Documentation

https://rust-lang.github.io/rfcs/1548-global-asm.html

[adpaco]

The "Raise a warning" item can be marked as done, right?

[zhassan-aws]

Capturing the current behavior as of c3d41b9: Kani produces a codegen warning, but does not cause verification to fail. For example, on the following test (adapted from the one here):

pub mod sally {
    std::arch::global_asm!(
        ".global foo",
        "foo:",
        "jmp baz",
    );

    #[no_mangle]
    pub unsafe extern "C" fn baz() {}
}

// the symbols `foo` and `bar` are global, no matter where
// `global_asm!` was used.
extern "C" {
    fn foo();
    fn bar();
}

pub mod harry {
    std::arch::global_asm!(
        ".global bar",
        "bar:",
        "jmp quux",
    );

    #[no_mangle]
    pub unsafe extern "C" fn quux() {}
}

#[kani::proof]
fn main() {
    assert!(1 + 1 == 2);
}

Kani produces two codegen warnings:

 WARN kani_compiler::codegen_cprover_gotoc::compiler_interface Crate global_asm contains global ASM, which is not handled by Kani
 WARN kani_compiler::codegen_cprover_gotoc::compiler_interface Crate global_asm contains global ASM, which is not handled by Kani
warning: 2 warnings emitted

but verification passes:

RESULTS:
Check 1: main.assertion.1
         - Status: SUCCESS
         - Description: "assertion failed: 1 + 1 == 2"
         - Location: global_asm.rs:32:5 in function main


SUMMARY: 
 ** 0 of 1 failed

VERIFICATION:- SUCCESSFUL