some fixes to the vstd-importing special case options

 * always set the VSTD_KIND environment variable from the verus binary;
   this fixes --no-vstd from the command line
 * introduce --is-stdlib-outside-of-core

Author: tjhance

source/builtin_macros/src/lib.rs

@@ -169,6 +169,8 @@ enum VstdKind {
     Imported,
     /// Embed vstd and verus_builtin as modules, necessary for verifying the `core` library.
     IsCore,
+    /// For other crates in stdlib verification that import core
+    ImportedViaCore,
 }
 
 fn vstd_kind() -> VstdKind {
@@ -184,8 +186,10 @@ fn vstd_kind() -> VstdKind {
                     return VstdKind::Imported;
                 } else if &s == "IsCore" {
                     return VstdKind::IsCore;
+                } else if &s == "ImportsCore" {
+                    return VstdKind::ImportedViaCore;
                 } else {
-                    panic!("The environment variable VSTD_KIND was set but its value is invalid. Allowed values are 'IsVstd', 'NoVstd', 'Imported', and 'IsCore'");
+                    panic!("The environment variable VSTD_KIND was set but its value is invalid. Allowed values are 'IsVstd', 'NoVstd', 'Imported', 'IsCore', and 'ImportsCore'");
                 }
             }
             _ => { }
@@ -198,7 +202,8 @@ fn vstd_kind() -> VstdKind {
             return VstdKind::IsVstd;
         }
 
-        // TODO: consider using the environment variable for these instead
+        // For tests, which don't go through the verus binary, we infer the mode from
+        // these cfg options
         if cfg_verify_core() {
             return VstdKind::IsCore;
         }
@@ -239,7 +244,7 @@ pub(crate) fn cfg_verify_core() -> bool {
 }
 
 #[cfg(verus_keep_ghost)]
-pub(crate) fn cfg_no_vstd() -> bool {
+fn cfg_no_vstd() -> bool {
     static CFG_VERIFY_CORE: OnceLock<bool> = OnceLock::new();
     *CFG_VERIFY_CORE.get_or_init(|| {
         let ts: proc_macro::TokenStream = quote::quote! { ::core::cfg!(verus_no_vstd) }.into();
@@ -261,7 +266,7 @@ pub(crate) fn cfg_no_vstd() -> bool {
 
 // Because 'expand_expr' is unstable, we need a different impl when `not(verus_keep_ghost)`.
 #[cfg(not(verus_keep_ghost))]
-pub(crate) fn cfg_no_vstd() -> bool {
+fn cfg_no_vstd() -> bool {
     false
 }
 

source/builtin_macros/src/syntax.rs

@@ -5181,6 +5181,7 @@ impl ToTokens for Builtin {
             VstdKind::NoVstd => quote_spanned! { self.0 => ::verus_builtin },
             VstdKind::Imported => quote_spanned! { self.0 => ::vstd::prelude },
             VstdKind::IsCore => quote_spanned! { self.0 => crate::verus_builtin },
+            VstdKind::ImportedViaCore => quote_spanned! { self.0 => ::core::verus_builtin },
         };
         tokens.extend(toks);
     }
@@ -5197,6 +5198,7 @@ impl ToTokens for Vstd {
             VstdKind::NoVstd => quote_spanned! { self.0 => ::vstd },
             VstdKind::Imported => quote_spanned! { self.0 => ::vstd },
             VstdKind::IsCore => quote_spanned! { self.0 => crate::vstd },
+            VstdKind::ImportedViaCore => quote_spanned! { self.0 => ::core::vstd },
         };
         tokens.extend(toks);
     }

source/rust_verify/src/config.rs

@@ -68,6 +68,8 @@ pub enum Vstd {
     Imported,
     /// Embed vstd and verus_builtin as modules, necessary for verifying the `core` library.
     IsCore,
+    /// For other crates in stdlib verification that import core
+    ImportedViaCore,
 }
 
 #[derive(Debug)]
@@ -310,6 +312,7 @@ pub fn parse_args_with_imports(
     const OPT_NO_VSTD: &str = "no-vstd";
     const OPT_IS_VSTD: &str = "is-vstd";
     const OPT_IS_CORE: &str = "is-core";
+    const OPT_IS_STDLIB_OUTSIDE_OF_CORE: &str = "is-stdlib-outside-of-core";
     const OPT_EXPAND_ERRORS: &str = "expand-errors";
 
     const OPT_LOG_DIR: &str = "log-dir";
@@ -490,6 +493,11 @@ pub fn parse_args_with_imports(
         OPT_IS_CORE,
         "Indicates the crate being verified is core (requires a specialized setup)",
     );
+    opts.optflag(
+        "",
+        OPT_IS_STDLIB_OUTSIDE_OF_CORE,
+        "Indicates the crate being verified is the stdlib (requires a specialized setup)",
+    );
     opts.optflag(
         "",
         OPT_EXPAND_ERRORS,
@@ -601,13 +609,16 @@ pub fn parse_args_with_imports(
     let no_vstd = matches.opt_present(OPT_NO_VSTD);
     let is_vstd = matches.opt_present(OPT_IS_VSTD);
     let is_core = matches.opt_present(OPT_IS_CORE);
+    let is_stdlib_outside_of_core = matches.opt_present(OPT_IS_STDLIB_OUTSIDE_OF_CORE);
     if is_vstd && is_core {
         error("contradictory options --is-core and --is-vstd".to_string());
     }
     let vstd = if is_vstd {
         Vstd::IsVstd
     } else if is_core {
         Vstd::IsCore
+    } else if is_stdlib_outside_of_core {
+        Vstd::ImportedViaCore
     } else if no_vstd {
         Vstd::NoVstd
     } else {

source/rust_verify/src/driver.rs

@@ -123,7 +123,7 @@ pub(crate) fn run_with_erase_macro_compile(
 ) -> Result<(), ()> {
     let mut callbacks = CompilerCallbacksEraseMacro { do_compile: compile };
     rustc_args.extend(["--cfg", "verus_keep_ghost"].map(|s| s.to_string()));
-    if vstd == Vstd::IsCore {
+    if matches!(vstd, Vstd::IsCore | Vstd::ImportedViaCore) {
         rustc_args.extend(["--cfg", "verus_verify_core"].map(|s| s.to_string()));
     } else if vstd == Vstd::NoVstd {
         rustc_args.extend(["--cfg", "verus_no_vstd"].map(|s| s.to_string()));
@@ -212,7 +212,7 @@ pub fn run(
             let externs = VerusExterns {
                 verus_root: verusroot.clone(),
                 has_vstd: verifier.args.vstd == Vstd::Imported,
-                has_builtin: verifier.args.vstd != Vstd::IsCore,
+                has_builtin: !matches!(verifier.args.vstd, Vstd::IsCore | Vstd::ImportedViaCore),
             };
             rustc_args.extend(externs.to_args());
             if in_vargo && !std::env::var("VERUS_Z3_PATH").is_ok() {
@@ -230,7 +230,7 @@ pub fn run(
     let mut rustc_args_verify = rustc_args.clone();
     rustc_args_verify.extend(["--cfg", "verus_keep_ghost"].map(|s| s.to_string()));
     rustc_args_verify.extend(["--cfg", "verus_keep_ghost_body"].map(|s| s.to_string()));
-    if verifier.args.vstd == Vstd::IsCore {
+    if matches!(verifier.args.vstd, Vstd::IsCore | Vstd::ImportedViaCore) {
         rustc_args_verify.extend(["--cfg", "verus_verify_core"].map(|s| s.to_string()));
     }
     // Build VIR and run verification

source/rust_verify_test/tests/basic.rs

@@ -641,78 +641,3 @@ test_verify_one_file! {
         }
     } => Ok(())
 }
-
-test_verify_one_file_with_options! {
-    #[test] test_is_core ["--is-core", "no-auto-import-verus_builtin"] => code! {
-        #![allow(unused_parens)]
-        #![allow(unused_imports)]
-        #![allow(dead_code)]
-        #![allow(unused_attributes)]
-        #![allow(unused_variables)]
-
-        #![cfg_attr(verus_keep_ghost, feature(core_intrinsics))]
-        #![cfg_attr(verus_keep_ghost, feature(allocator_api))]
-        #![cfg_attr(verus_keep_ghost, feature(step_trait))]
-        #![cfg_attr(verus_keep_ghost, feature(ptr_metadata))]
-        #![cfg_attr(verus_keep_ghost, feature(strict_provenance_atomic_ptr))]
-        #![cfg_attr(verus_keep_ghost, feature(derive_clone_copy))]
-        #![cfg_attr(verus_keep_ghost, feature(freeze))]
-        #![cfg_attr(
-            verus_keep_ghost,
-            feature(fn_traits),
-        )]
-        #![cfg_attr(verus_keep_ghost, verifier::exec_allows_no_decreases_clause)]
-
-        #[verifier::external]
-        #[path="../../../../builtin/src/lib.rs"]
-        mod verus_builtin;
-
-        #[path="../../../../vstd/vstd.rs"]
-        mod vstd;
-
-        mod test {
-            use crate::vstd::set::*;
-            use crate::vstd::seq::*;
-            use crate::vstd::multiset::*;
-            use crate::vstd::prelude::*;
-
-            verus!{
-
-            proof fn test_seqs(a: Seq<int>, b: Seq<int>)
-                requires a == b,
-            {
-                crate::vstd::seq_lib::assert_seqs_equal!(a, b);
-                crate::vstd::seq_lib::assert_seqs_equal!(a == b);
-            }
-
-            proof fn test_sets(a: Set<int>, b: Set<int>)
-                requires a == b,
-            {
-                crate::vstd::set_lib::assert_sets_equal!(a, b);
-                crate::vstd::set_lib::assert_sets_equal!(a == b);
-            }
-
-            proof fn test_multisets(a: Multiset<int>, b: Multiset<int>)
-                requires a == b,
-            {
-                crate::vstd::multiset::assert_multisets_equal!(a, b);
-                crate::vstd::multiset::assert_multisets_equal!(a == b);
-            }
-
-            fn test_slice_index(x: &[u8]) -> u8
-                requires x@.len() > 0
-            {
-                x[0]
-            }
-
-            fn test_ptr_stuff(a: *mut u8, b: *mut [u8; 2]) {
-                let t = a as *mut u16;
-                let s = b as *mut [u8];
-            }
-
-            }
-        }
-
-        fn main() { }
-    } => Ok(())
-}

source/rust_verify_test/tests/verify_stdlib_special_setup.rs

@@ -0,0 +1,79 @@
+#![feature(rustc_private)]
+#[macro_use]
+mod common;
+use common::*;
+
+test_verify_one_file_with_options! {
+    #[test] test_is_core ["--is-core", "no-auto-import-verus_builtin"] => code! {
+        #![allow(unused_parens)]
+        #![allow(unused_imports)]
+        #![allow(dead_code)]
+        #![allow(unused_attributes)]
+        #![allow(unused_variables)]
+
+        #![cfg_attr(verus_keep_ghost, feature(core_intrinsics))]
+        #![cfg_attr(verus_keep_ghost, feature(allocator_api))]
+        #![cfg_attr(verus_keep_ghost, feature(step_trait))]
+        #![cfg_attr(verus_keep_ghost, feature(ptr_metadata))]
+        #![cfg_attr(verus_keep_ghost, feature(strict_provenance_atomic_ptr))]
+        #![cfg_attr(verus_keep_ghost, feature(derive_clone_copy))]
+        #![cfg_attr(verus_keep_ghost, feature(freeze))]
+        #![cfg_attr(
+            verus_keep_ghost,
+            feature(fn_traits),
+        )]
+        #![cfg_attr(verus_keep_ghost, verifier::exec_allows_no_decreases_clause)]
+
+        #[verifier::external]
+        #[path="../../../../builtin/src/lib.rs"]
+        mod verus_builtin;
+
+        #[path="../../../../vstd/vstd.rs"]
+        mod vstd;
+
+        mod test {
+            use crate::vstd::set::*;
+            use crate::vstd::seq::*;
+            use crate::vstd::multiset::*;
+            use crate::vstd::prelude::*;
+
+            verus!{
+
+            proof fn test_seqs(a: Seq<int>, b: Seq<int>)
+                requires a == b,
+            {
+                crate::vstd::seq_lib::assert_seqs_equal!(a, b);
+                crate::vstd::seq_lib::assert_seqs_equal!(a == b);
+            }
+
+            proof fn test_sets(a: Set<int>, b: Set<int>)
+                requires a == b,
+            {
+                crate::vstd::set_lib::assert_sets_equal!(a, b);
+                crate::vstd::set_lib::assert_sets_equal!(a == b);
+            }
+
+            proof fn test_multisets(a: Multiset<int>, b: Multiset<int>)
+                requires a == b,
+            {
+                crate::vstd::multiset::assert_multisets_equal!(a, b);
+                crate::vstd::multiset::assert_multisets_equal!(a == b);
+            }
+
+            fn test_slice_index(x: &[u8]) -> u8
+                requires x@.len() > 0
+            {
+                x[0]
+            }
+
+            fn test_ptr_stuff(a: *mut u8, b: *mut [u8; 2]) {
+                let t = a as *mut u16;
+                let s = b as *mut [u8];
+            }
+
+            }
+        }
+
+        fn main() { }
+    } => Ok(())
+}

source/verus/src/main.rs

@@ -183,6 +183,9 @@ fn run() -> Result<std::process::ExitStatus, String> {
 
     let mut cmd = Command::new("rustup");
 
+    let vstd_kind = get_vstd_kind(&args);
+    cmd.env("VSTD_KIND", vstd_kind);
+
     #[allow(unused_variables)]
     let z3_path = if let Some(z3_path) = std::env::var("VERUS_Z3_PATH").ok() {
         Some(std::path::PathBuf::from(z3_path))
@@ -481,3 +484,29 @@ fn run() -> Result<std::process::ExitStatus, String> {
         Ok(exit_status)
     }
 }
+
+fn get_vstd_kind(args: &Vec<String>) -> &'static str {
+    let arg_names = [
+        ("--no-vstd", "NoVstd"),
+        ("--is-vstd", "IsVstd"),
+        ("--is-core", "IsCore"),
+        ("--is-stdlib-outside-of-core", "ImportedViaCore"),
+    ];
+    let default = "Imported";
+
+    let mut found = None;
+    for (arg_name, kind_string) in arg_names.iter() {
+        if args.contains(&arg_name.to_string()) {
+            if found.is_none() {
+                found = Some((arg_name, kind_string));
+            } else {
+                eprintln!("contradictory arguments: {:} and {:}", found.unwrap().0, arg_name);
+                std::process::exit(255);
+            }
+        }
+    }
+    match found {
+        Some((_, kind)) => kind,
+        _ => default,
+    }
+}