Merge remote-tracking branch 'origin/main' into toolchain-2024-06-04-…

…manual

Cargo.toml

@@ -68,4 +68,5 @@ exclude = [
   "tests/script-based-pre",
   "tests/script-based-pre/build-cache-bin/target/new_dep",
   "tests/script-based-pre/build-cache-dirty/target/new_dep",
+  "tests/script-based-pre/verify_std_cmd/tmp_dir/target/kani_verify_std",
 ]

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -458,6 +458,45 @@ impl GotocHook for UntrackedDeref {
     }
 }
 
+struct InitContracts;
+
+/// CBMC contracts currently has a limitation where `free` has to be in scope.
+/// However, if there is no dynamic allocation in the harness, slicing removes `free` from the
+/// scope.
+///
+/// Thus, this function will basically translate into:
+/// ```c
+/// // This is a no-op.
+/// free(NULL);
+/// ```
+impl GotocHook for InitContracts {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance.def, "KaniInitContracts")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 0,);
+        let loc = gcx.codegen_span_stable(span);
+        Stmt::block(
+            vec![
+                BuiltinFn::Free
+                    .call(vec![Expr::pointer_constant(0, Type::void_pointer())], loc)
+                    .as_stmt(loc),
+                Stmt::goto(bb_label(target.unwrap()), loc),
+            ],
+            loc,
+        )
+    }
+}
+
 pub fn fn_hooks() -> GotocHooks {
     GotocHooks {
         hooks: vec![
@@ -472,6 +511,7 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
             Rc::new(UntrackedDeref),
+            Rc::new(InitContracts),
         ],
     }
 }

kani-compiler/src/kani_middle/intrinsics.rs

@@ -57,7 +57,12 @@ impl<'tcx> ModelIntrinsics<'tcx> {
         let arg_ty = args[0].node.ty(&self.local_decls, tcx);
         if arg_ty.is_simd() {
             // Get the stub definition.
-            let stub_id = tcx.get_diagnostic_item(Symbol::intern("KaniModelSimdBitmask")).unwrap();
+            let Some(stub_id) = tcx.get_diagnostic_item(Symbol::intern("KaniModelSimdBitmask"))
+            else {
+                // This should only happen when verifying the standard library.
+                // We don't need to warn here, since the backend will print unsupported constructs.
+                return;
+            };
             debug!(?func, ?stub_id, "replace_simd_bitmask");
 
             // Get SIMD information from the type.

kani-driver/src/args/mod.rs

@@ -6,6 +6,7 @@ pub mod assess_args;
 pub mod cargo;
 pub mod common;
 pub mod playback_args;
+pub mod std_args;
 
 pub use assess_args::*;
 
@@ -90,6 +91,8 @@ pub struct StandaloneArgs {
 pub enum StandaloneSubcommand {
     /// Execute concrete playback testcases of a local crate.
     Playback(Box<playback_args::KaniPlaybackArgs>),
+    /// Verify the rust standard library.
+    VerifyStd(Box<std_args::VerifyStdArgs>),
 }
 
 #[derive(Debug, clap::Parser)]
@@ -448,6 +451,13 @@ fn check_no_cargo_opt(is_set: bool, name: &str) -> Result<(), Error> {
 impl ValidateArgs for StandaloneArgs {
     fn validate(&self) -> Result<(), Error> {
         self.verify_opts.validate()?;
+
+        match &self.command {
+            Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?,
+            // TODO: Invoke PlaybackArgs::validate()
+            None | Some(StandaloneSubcommand::Playback(..)) => {}
+        };
+
         // Cargo target arguments.
         check_no_cargo_opt(self.verify_opts.target.bins, "--bins")?;
         check_no_cargo_opt(self.verify_opts.target.lib, "--lib")?;

kani-driver/src/args/std_args.rs

@@ -0,0 +1,77 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Implements the `verify-std` subcommand handling.
+
+use crate::args::{ValidateArgs, VerificationArgs};
+use clap::error::ErrorKind;
+use clap::{Error, Parser};
+use kani_metadata::UnstableFeature;
+use std::path::PathBuf;
+
+/// Verify a local version of the Rust standard library.
+///
+/// This is an **unstable option** and it the standard library version must be compatible with
+/// Kani's toolchain version.
+#[derive(Debug, Parser)]
+pub struct VerifyStdArgs {
+    /// The path to the folder containing the crates for the Rust standard library.
+    /// Note that this directory must be named `library` as used in the Rust toolchain and
+    /// repository.
+    pub std_path: PathBuf,
+
+    #[command(flatten)]
+    pub verify_opts: VerificationArgs,
+}
+
+impl ValidateArgs for VerifyStdArgs {
+    fn validate(&self) -> Result<(), Error> {
+        self.verify_opts.validate()?;
+
+        if !self
+            .verify_opts
+            .common_args
+            .unstable_features
+            .contains(UnstableFeature::UnstableOptions)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                "The `verify-std` subcommand is unstable and requires -Z unstable-options",
+            ));
+        }
+
+        if !self.std_path.exists() {
+            Err(Error::raw(
+                ErrorKind::InvalidValue,
+                format!(
+                    "Invalid argument: `<STD_PATH>` argument `{}` does not exist",
+                    self.std_path.display()
+                ),
+            ))
+        } else if !self.std_path.is_dir() {
+            Err(Error::raw(
+                ErrorKind::InvalidValue,
+                format!(
+                    "Invalid argument: `<STD_PATH>` argument `{}` is not a directory",
+                    self.std_path.display()
+                ),
+            ))
+        } else {
+            let full_path = self.std_path.canonicalize()?;
+            let dir = full_path.file_stem().unwrap();
+            if dir != "library" {
+                Err(Error::raw(
+                    ErrorKind::InvalidValue,
+                    format!(
+                        "Invalid argument: Expected `<STD_PATH>` to point to the `library` folder \
+                    containing the standard library crates.\n\
+                    Found `{}` folder instead",
+                        dir.to_string_lossy()
+                    ),
+                ))
+            } else {
+                Ok(())
+            }
+        }
+    }
+}

kani-driver/src/call_cargo.rs

@@ -2,20 +2,22 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::args::VerificationArgs;
-use crate::call_single_file::to_rustc_arg;
+use crate::call_single_file::{to_rustc_arg, LibConfig};
 use crate::project::Artifact;
-use crate::session::{setup_cargo_command, KaniSession};
+use crate::session::{lib_folder, lib_no_core_folder, setup_cargo_command, KaniSession};
 use crate::util;
 use anyhow::{bail, Context, Result};
 use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel};
-use cargo_metadata::{Message, Metadata, MetadataCommand, Package, Target};
+use cargo_metadata::{
+    Artifact as RustcArtifact, Message, Metadata, MetadataCommand, Package, Target,
+};
 use kani_metadata::{ArtifactType, CompilerArtifactStub};
 use std::ffi::{OsStr, OsString};
 use std::fmt::{self, Display};
 use std::fs::{self, File};
 use std::io::BufReader;
 use std::io::IsTerminal;
-use std::path::PathBuf;
+use std::path::{Path, PathBuf};
 use std::process::Command;
 use tracing::{debug, trace};
 
@@ -43,6 +45,49 @@ pub struct CargoOutputs {
 }
 
 impl KaniSession {
+    /// Create a new cargo library in the given path.
+    pub fn cargo_init_lib(&self, path: &Path) -> Result<()> {
+        let mut cmd = setup_cargo_command()?;
+        cmd.args(["init", "--lib", path.to_string_lossy().as_ref()]);
+        self.run_terminal(cmd)
+    }
+
+    pub fn cargo_build_std(&self, std_path: &Path, krate_path: &Path) -> Result<Vec<Artifact>> {
+        let lib_path = lib_no_core_folder().unwrap();
+        let mut rustc_args = self.kani_rustc_flags(LibConfig::new_no_core(lib_path));
+        rustc_args.push(to_rustc_arg(self.kani_compiler_flags()).into());
+        rustc_args.push(self.reachability_arg().into());
+        // Ignore global assembly, since `compiler_builtins` has some.
+        rustc_args.push(to_rustc_arg(vec!["--ignore-global-asm".to_string()]).into());
+
+        let mut cargo_args: Vec<OsString> = vec!["build".into()];
+        cargo_args.append(&mut cargo_config_args());
+
+        // Configuration needed to parse cargo compilation status.
+        cargo_args.push("--message-format".into());
+        cargo_args.push("json-diagnostic-rendered-ansi".into());
+        cargo_args.push("-Z".into());
+        cargo_args.push("build-std=panic_abort,core,std".into());
+
+        if self.args.common_args.verbose {
+            cargo_args.push("-v".into());
+        }
+
+        // Since we are verifying the standard library, we set the reachability to all crates.
+        let mut cmd = setup_cargo_command()?;
+        cmd.args(&cargo_args)
+            .current_dir(krate_path)
+            .env("RUSTC", &self.kani_compiler)
+            // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
+            // https://doc.rust-lang.org/cargo/reference/environment-variables.html
+            .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
+            .env("CARGO_TERM_PROGRESS_WHEN", "never")
+            .env("__CARGO_TESTS_ONLY_SRC_ROOT", std_path.as_os_str());
+
+        let build_artifacts = self.run_build(cmd)?;
+        Ok(build_artifacts.into_iter().filter_map(map_kani_artifact).collect())
+    }
+
     /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir`
     pub fn cargo_build(&self, keep_going: bool) -> Result<CargoOutputs> {
         let build_target = env!("TARGET"); // see build.rs
@@ -60,7 +105,8 @@ impl KaniSession {
             fs::remove_dir_all(&target_dir)?;
         }
 
-        let mut rustc_args = self.kani_rustc_flags();
+        let lib_path = lib_folder().unwrap();
+        let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
         rustc_args.push(to_rustc_arg(self.kani_compiler_flags()).into());
 
         let mut cargo_args: Vec<OsString> = vec!["rustc".into()];
@@ -120,7 +166,7 @@ impl KaniSession {
                     .env("CARGO_ENCODED_RUSTFLAGS", rustc_args.join(OsStr::new("\x1f")))
                     .env("CARGO_TERM_PROGRESS_WHEN", "never");
 
-                match self.run_cargo(cmd, verification_target.target()) {
+                match self.run_build_target(cmd, verification_target.target()) {
                     Err(err) => {
                         if keep_going {
                             let target_str = format!("{verification_target}");
@@ -179,9 +225,9 @@ impl KaniSession {
 
     /// Run cargo and collect any error found.
     /// We also collect the metadata file generated during compilation if any.
-    fn run_cargo(&self, cargo_cmd: Command, target: &Target) -> Result<Option<Artifact>> {
+    fn run_build(&self, cargo_cmd: Command) -> Result<Vec<RustcArtifact>> {
         let support_color = std::io::stdout().is_terminal();
-        let mut artifact = None;
+        let mut artifacts = vec![];
         if let Some(mut cargo_process) = self.run_piped(cargo_cmd)? {
             let reader = BufReader::new(cargo_process.stdout.take().unwrap());
             let mut error_count = 0;
@@ -211,33 +257,9 @@ impl KaniSession {
                         }
                     },
                     Message::CompilerArtifact(rustc_artifact) => {
-                        /// Compares two targets, and falls back to a weaker
-                        /// comparison where we avoid dashes in their names.
-                        fn same_target(t1: &Target, t2: &Target) -> bool {
-                            (t1 == t2)
-                                || (t1.name.replace('-', "_") == t2.name.replace('-', "_")
-                                    && t1.kind == t2.kind
-                                    && t1.src_path == t2.src_path
-                                    && t1.edition == t2.edition
-                                    && t1.doctest == t2.doctest
-                                    && t1.test == t2.test
-                                    && t1.doc == t2.doc)
-                        }
-                        // This used to be `rustc_artifact == *target`, but it
-                        // started to fail after the `cargo` change in
-                        // <https://github.com/rust-lang/cargo/pull/12783>
-                        //
-                        // We should revisit this check after a while to see if
-                        // it's not needed anymore or it can be restricted to
-                        // certain cases.
-                        // TODO: <https://github.com/model-checking/kani/issues/3111>
-                        if same_target(&rustc_artifact.target, target) {
-                            debug_assert!(
-                                artifact.is_none(),
-                                "expected only one artifact for `{target:?}`",
-                            );
-                            artifact = Some(rustc_artifact);
-                        }
+                        // Compares two targets, and falls back to a weaker
+                        // comparison where we avoid dashes in their names.
+                        artifacts.push(rustc_artifact)
                     }
                     Message::BuildScriptExecuted(_) | Message::BuildFinished(_) => {
                         // do nothing
@@ -263,11 +285,40 @@ impl KaniSession {
                 );
             }
         }
+        Ok(artifacts)
+    }
+
+    /// Run cargo and collect any error found.
+    /// We also collect the metadata file generated during compilation if any for the given target.
+    fn run_build_target(&self, cargo_cmd: Command, target: &Target) -> Result<Option<Artifact>> {
+        /// This used to be `rustc_artifact == *target`, but it
+        /// started to fail after the `cargo` change in
+        /// <https://github.com/rust-lang/cargo/pull/12783>
+        ///
+        /// We should revisit this check after a while to see if
+        /// it's not needed anymore or it can be restricted to
+        /// certain cases.
+        /// TODO: <https://github.com/model-checking/kani/issues/3111>
+        fn same_target(t1: &Target, t2: &Target) -> bool {
+            (t1 == t2)
+                || (t1.name.replace('-', "_") == t2.name.replace('-', "_")
+                    && t1.kind == t2.kind
+                    && t1.src_path == t2.src_path
+                    && t1.edition == t2.edition
+                    && t1.doctest == t2.doctest
+                    && t1.test == t2.test
+                    && t1.doc == t2.doc)
+        }
+
+        let artifacts = self.run_build(cargo_cmd)?;
+        debug!(?artifacts, "run_build_target");
+
         // We generate kani specific artifacts only for the build target. The build target is
         // always the last artifact generated in a build, and all the other artifacts are related
-        // to dependencies or build scripts. Hence, we need to invoke `map_kani_artifact` only
-        // for the last compiler artifact.
-        Ok(artifact.and_then(map_kani_artifact))
+        // to dependencies or build scripts.
+        Ok(artifacts.into_iter().rev().find_map(|artifact| {
+            if same_target(&artifact.target, target) { map_kani_artifact(artifact) } else { None }
+        }))
     }
 }