Error out for crates with global ASM (rust-lang#1112)

Author: zhassan-aws

kani-compiler/kani_queries/src/lib.rs

@@ -15,6 +15,9 @@ pub trait UserInput {
 
     fn set_output_pretty_json(&mut self, pretty_json: bool);
     fn get_output_pretty_json(&self) -> bool;
+
+    fn set_ignore_global_asm(&mut self, global_asm: bool);
+    fn get_ignore_global_asm(&self) -> bool;
 }
 
 #[derive(Debug, Default)]
@@ -23,6 +26,7 @@ pub struct QueryDb {
     emit_vtable_restrictions: AtomicBool,
     symbol_table_passes: Vec<String>,
     json_pretty_print: AtomicBool,
+    ignore_global_asm: AtomicBool,
 }
 
 impl UserInput for QueryDb {
@@ -57,4 +61,12 @@ impl UserInput for QueryDb {
     fn get_output_pretty_json(&self) -> bool {
         self.json_pretty_print.load(Ordering::Relaxed)
     }
+
+    fn set_ignore_global_asm(&mut self, global_asm: bool) {
+        self.ignore_global_asm.store(global_asm, Ordering::Relaxed);
+    }
+
+    fn get_ignore_global_asm(&self) -> bool {
+        self.ignore_global_asm.load(Ordering::Relaxed)
+    }
 }

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -84,10 +84,18 @@ impl CodegenBackend for GotocCodegenBackend {
                         );
                     }
                     MonoItem::GlobalAsm(_) => {
-                        warn!(
-                            "Crate {} contains global ASM, which is not handled by Kani",
-                            c.short_crate_name()
-                        );
+                        if !self.queries.get_ignore_global_asm() {
+                            let error_msg = format!(
+                                "Crate {} contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**).",
+                                c.short_crate_name()
+                            );
+                            tcx.sess.err(&error_msg);
+                        } else {
+                            warn!(
+                                "Ignoring global ASM in crate {}. Verification results may be impacted.",
+                                c.short_crate_name()
+                            );
+                        }
                     }
                 }
             }

kani-compiler/src/main.rs

@@ -92,6 +92,7 @@ fn main() -> Result<(), &'static str> {
     queries.set_emit_vtable_restrictions(matches.is_present(parser::RESTRICT_FN_PTRS));
     queries.set_check_assertion_reachability(matches.is_present(parser::ASSERTION_REACH_CHECKS));
     queries.set_output_pretty_json(matches.is_present(parser::PRETTY_OUTPUT_FILES));
+    queries.set_ignore_global_asm(matches.is_present(parser::IGNORE_GLOBAL_ASM));
 
     // Generate rustc args.
     let rustc_args = generate_rustc_args(&matches);

kani-compiler/src/parser.rs

@@ -28,12 +28,15 @@ pub const COLOR_OUTPUT: &'static str = "color-output";
 /// Option name used to dump function pointer restrictions.
 pub const RESTRICT_FN_PTRS: &'static str = "restrict-vtable-fn-ptrs";
 
-/// Option name used to enable assertion reachability checks
+/// Option name used to enable assertion reachability checks.
 pub const ASSERTION_REACH_CHECKS: &'static str = "assertion-reach-checks";
 
 /// Option name used to use json pretty-print for output files.
 pub const PRETTY_OUTPUT_FILES: &'static str = "pretty-json-files";
 
+/// Option used for suppressing global ASM error.
+pub const IGNORE_GLOBAL_ASM: &'static str = "ignore-global-asm";
+
 /// Option name used to override the sysroot.
 pub const SYSROOT: &'static str = "sysroot";
 
@@ -135,6 +138,11 @@ pub fn parser<'a, 'b>() -> App<'a, 'b> {
                 .long("--pretty-json-files")
                 .help("Output json files in a more human-readable format (with spaces)."),
         )
+        .arg(
+            Arg::with_name(IGNORE_GLOBAL_ASM)
+                .long("--ignore-global-asm")
+                .help("Suppress error due to the existence of global_asm in a crate"),
+        )
 }
 
 /// Retrieves the arguments from the command line and process hack to incorporate CARGO arguments.

kani-driver/src/args.rs

@@ -143,6 +143,11 @@ pub struct KaniArgs {
     /// Turn off assertion reachability checks
     #[structopt(long)]
     pub no_assertion_reach_checks: bool,
+
+    /// Do not error out for crates containing `global_asm!`.
+    /// This option may impact the soundness of the analysis and may cause false proofs and/or counterexamples
+    #[structopt(long, hidden_short_help(true), requires("enable-unstable"))]
+    pub ignore_global_asm: bool,
     /*
     The below is a "TODO list" of things not yet implemented from the kani_flags.py script.
 

kani-driver/src/call_single_file.rs

@@ -117,6 +117,9 @@ impl KaniSession {
         if self.args.assertion_reach_checks() {
             flags.push("--assertion-reach-checks".into());
         }
+        if self.args.ignore_global_asm {
+            flags.push("--ignore-global-asm".into());
+        }
 
         // Stratification point!
         // Above are arguments that should be parsed by kani-compiler

scripts/std-lib-regression.sh

@@ -44,7 +44,7 @@ cp ${KANI_DIR}/rust-toolchain.toml .
 
 echo "Starting cargo build with Kani"
 export RUSTC_LOG=error
-export KANIFLAGS="--goto-c"
+export KANIFLAGS="--goto-c --ignore-global-asm"
 export RUSTFLAGS="--kani-flags"
 export RUSTC="$KANI_DIR/target/debug/kani-compiler"
 $WRAPPER cargo build --verbose -Z build-std --lib --target $TARGET

tests/cargo-kani/asm/global/Cargo.toml

@@ -0,0 +1,15 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "global"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+crate_with_global_asm = { path = "crate_with_global_asm" }
+
+[package.metadata.kani]
+flags = { enable-unstable = true, ignore-global-asm = true }

tests/cargo-kani/asm/global/calls_crate_with_global_asm.expected

@@ -0,0 +1,2 @@
+Status: SUCCESS\
+Description: "assertion failed: x * y == 33"

tests/cargo-kani/asm/global/crate_with_global_asm/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "crate_with_global_asm"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

tests/cargo-kani/asm/global/crate_with_global_asm/src/lib.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// A crate with global ASM
+
+// defines a function `foo`
+std::arch::global_asm!(".global foo", "foo:", "nop",);
+
+pub static mut STATIC_VAR: u16 = 98;
+
+// exports the fn `foo`
+extern "C" {
+    pub fn foo();
+}
+
+// a function that does not involve any ASM
+pub fn eleven() -> i32 {
+    11
+}

tests/cargo-kani/asm/global/reads_static_var_in_crate_with_global_asm.expected

@@ -0,0 +1,2 @@
+Status: SUCCESS\
+Description: "assertion failed: x == 98"

tests/cargo-kani/asm/global/src/lib.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Call a function from crate with global ASM
+// Should pass with --ignore-global-asm
+#[kani::proof]
+fn calls_crate_with_global_asm() {
+    let x = 3;
+    let y = crate_with_global_asm::eleven();
+    assert_eq!(x * y, 33);
+}
+
+// Access a static variable from crate with global ASM
+// Should pass with --ignore-global-asm
+#[kani::proof]
+fn reads_static_var_in_crate_with_global_asm() {
+    let x = unsafe { crate_with_global_asm::STATIC_VAR };
+    assert_eq!(x, 98);
+}

tests/cargo-kani/asm/global_error/Cargo.toml

@@ -0,0 +1,12 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "global"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+crate_with_global_asm = { path = "crate_with_global_asm" }

tests/cargo-kani/asm/global_error/crate_with_global_asm/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "crate_with_global_asm"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]

tests/cargo-kani/asm/global_error/crate_with_global_asm/src/lib.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// A crate with global ASM
+
+// defines a function `foo`
+std::arch::global_asm!(".global foo", "foo:", "nop",);
+
+pub static mut STATIC_VAR: u16 = 98;
+
+// exports the fn `foo`
+extern "C" {
+    pub fn foo();
+}
+
+// a function that does not involve any ASM
+pub fn eleven() -> i32 {
+    11
+}

tests/cargo-kani/asm/global_error/doesnt_call_crate_with_global_asm.expected

@@ -0,0 +1,4 @@
+error: Crate crate_with_global_asm contains global ASM, which is not supported by Kani. Rerun with `--enable-unstable --ignore-global-asm` to suppress this error (**Verification results may be impacted**).
+Error: "Failed to compile crate."
+error: could not compile `crate_with_global_asm` due to previous error
+Error: cargo exited with status exit status: 101

tests/cargo-kani/asm/global_error/src/lib.rs

@@ -0,0 +1,11 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Kani should error out if run without --ignore-global-asm even if the crate
+// with global ASM is not called
+#[kani::proof]
+fn doesnt_call_crate_with_global_asm() {
+    let x = 3;
+    let y = 11;
+    assert_eq!(x * y, 33);
+}