Skip to content

Commit eff6e63

Browse files
tjhancetjhance
committed
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
1 parent 278d492 commit eff6e63

File tree

7 files changed

+133
-82
lines changed

7 files changed

+133
-82
lines changed

‎source/builtin_macros/src/lib.rs

Lines changed: 9 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,8 @@ enum VstdKind {
169169
Imported,
170170
/// Embed vstd and verus_builtin as modules, necessary for verifying the `core` library.
171171
IsCore,
172+
/// For other crates in stdlib verification that import core
173+
ImportedViaCore,
172174
}
173175

174176
fn vstd_kind() -> VstdKind {
@@ -184,8 +186,10 @@ fn vstd_kind() -> VstdKind {
184186
return VstdKind::Imported;
185187
} else if &s == "IsCore" {
186188
return VstdKind::IsCore;
189+
} else if &s == "ImportsCore" {
190+
return VstdKind::ImportedViaCore;
187191
} else {
188-
panic!("The environment variable VSTD_KIND was set but its value is invalid. Allowed values are 'IsVstd', 'NoVstd', 'Imported', and 'IsCore'");
192+
panic!("The environment variable VSTD_KIND was set but its value is invalid. Allowed values are 'IsVstd', 'NoVstd', 'Imported', 'IsCore', and 'ImportsCore'");
189193
}
190194
}
191195
_ => { }
@@ -198,7 +202,8 @@ fn vstd_kind() -> VstdKind {
198202
return VstdKind::IsVstd;
199203
}
200204

201-
// TODO: consider using the environment variable for these instead
205+
// For tests, which don't go through the verus binary, we infer the mode from
206+
// these cfg options
202207
if cfg_verify_core() {
203208
return VstdKind::IsCore;
204209
}
@@ -239,7 +244,7 @@ pub(crate) fn cfg_verify_core() -> bool {
239244
}
240245

241246
#[cfg(verus_keep_ghost)]
242-
pub(crate) fn cfg_no_vstd() -> bool {
247+
fn cfg_no_vstd() -> bool {
243248
static CFG_VERIFY_CORE: OnceLock<bool> = OnceLock::new();
244249
*CFG_VERIFY_CORE.get_or_init(|| {
245250
let ts: proc_macro::TokenStream = quote::quote! { ::core::cfg!(verus_no_vstd) }.into();
@@ -261,7 +266,7 @@ pub(crate) fn cfg_no_vstd() -> bool {
261266

262267
// Because 'expand_expr' is unstable, we need a different impl when `not(verus_keep_ghost)`.
263268
#[cfg(not(verus_keep_ghost))]
264-
pub(crate) fn cfg_no_vstd() -> bool {
269+
fn cfg_no_vstd() -> bool {
265270
false
266271
}
267272

‎source/builtin_macros/src/syntax.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5181,6 +5181,7 @@ impl ToTokens for Builtin {
51815181
VstdKind::NoVstd => quote_spanned! { self.0 => ::verus_builtin },
51825182
VstdKind::Imported => quote_spanned! { self.0 => ::vstd::prelude },
51835183
VstdKind::IsCore => quote_spanned! { self.0 => crate::verus_builtin },
5184+
VstdKind::ImportedViaCore => quote_spanned! { self.0 => ::core::verus_builtin },
51845185
};
51855186
tokens.extend(toks);
51865187
}
@@ -5197,6 +5198,7 @@ impl ToTokens for Vstd {
51975198
VstdKind::NoVstd => quote_spanned! { self.0 => ::vstd },
51985199
VstdKind::Imported => quote_spanned! { self.0 => ::vstd },
51995200
VstdKind::IsCore => quote_spanned! { self.0 => crate::vstd },
5201+
VstdKind::ImportedViaCore => quote_spanned! { self.0 => ::core::vstd },
52005202
};
52015203
tokens.extend(toks);
52025204
}

‎source/rust_verify/src/config.rs

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,8 @@ pub enum Vstd {
6868
Imported,
6969
/// Embed vstd and verus_builtin as modules, necessary for verifying the `core` library.
7070
IsCore,
71+
/// For other crates in stdlib verification that import core
72+
ImportedViaCore,
7173
}
7274

7375
#[derive(Debug)]
@@ -310,6 +312,7 @@ pub fn parse_args_with_imports(
310312
const OPT_NO_VSTD: &str = "no-vstd";
311313
const OPT_IS_VSTD: &str = "is-vstd";
312314
const OPT_IS_CORE: &str = "is-core";
315+
const OPT_IS_STDLIB_OUTSIDE_OF_CORE: &str = "is-stdlib-outside-of-core";
313316
const OPT_EXPAND_ERRORS: &str = "expand-errors";
314317

315318
const OPT_LOG_DIR: &str = "log-dir";
@@ -490,6 +493,11 @@ pub fn parse_args_with_imports(
490493
OPT_IS_CORE,
491494
"Indicates the crate being verified is core (requires a specialized setup)",
492495
);
496+
opts.optflag(
497+
"",
498+
OPT_IS_STDLIB_OUTSIDE_OF_CORE,
499+
"Indicates the crate being verified is the stdlib (requires a specialized setup)",
500+
);
493501
opts.optflag(
494502
"",
495503
OPT_EXPAND_ERRORS,
@@ -601,13 +609,16 @@ pub fn parse_args_with_imports(
601609
let no_vstd = matches.opt_present(OPT_NO_VSTD);
602610
let is_vstd = matches.opt_present(OPT_IS_VSTD);
603611
let is_core = matches.opt_present(OPT_IS_CORE);
612+
let is_stdlib_outside_of_core = matches.opt_present(OPT_IS_STDLIB_OUTSIDE_OF_CORE);
604613
if is_vstd && is_core {
605614
error("contradictory options --is-core and --is-vstd".to_string());
606615
}
607616
let vstd = if is_vstd {
608617
Vstd::IsVstd
609618
} else if is_core {
610619
Vstd::IsCore
620+
} else if is_stdlib_outside_of_core {
621+
Vstd::ImportedViaCore
611622
} else if no_vstd {
612623
Vstd::NoVstd
613624
} else {

‎source/rust_verify/src/driver.rs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -123,7 +123,7 @@ pub(crate) fn run_with_erase_macro_compile(
123123
) -> Result<(), ()> {
124124
let mut callbacks = CompilerCallbacksEraseMacro { do_compile: compile };
125125
rustc_args.extend(["--cfg", "verus_keep_ghost"].map(|s| s.to_string()));
126-
if vstd == Vstd::IsCore {
126+
if matches!(vstd, Vstd::IsCore | Vstd::ImportedViaCore) {
127127
rustc_args.extend(["--cfg", "verus_verify_core"].map(|s| s.to_string()));
128128
} else if vstd == Vstd::NoVstd {
129129
rustc_args.extend(["--cfg", "verus_no_vstd"].map(|s| s.to_string()));
@@ -212,7 +212,7 @@ pub fn run(
212212
let externs = VerusExterns {
213213
verus_root: verusroot.clone(),
214214
has_vstd: verifier.args.vstd == Vstd::Imported,
215-
has_builtin: verifier.args.vstd != Vstd::IsCore,
215+
has_builtin: !matches!(verifier.args.vstd, Vstd::IsCore | Vstd::ImportedViaCore),
216216
};
217217
rustc_args.extend(externs.to_args());
218218
if in_vargo && !std::env::var("VERUS_Z3_PATH").is_ok() {
@@ -230,7 +230,7 @@ pub fn run(
230230
let mut rustc_args_verify = rustc_args.clone();
231231
rustc_args_verify.extend(["--cfg", "verus_keep_ghost"].map(|s| s.to_string()));
232232
rustc_args_verify.extend(["--cfg", "verus_keep_ghost_body"].map(|s| s.to_string()));
233-
if verifier.args.vstd == Vstd::IsCore {
233+
if matches!(verifier.args.vstd, Vstd::IsCore | Vstd::ImportedViaCore) {
234234
rustc_args_verify.extend(["--cfg", "verus_verify_core"].map(|s| s.to_string()));
235235
}
236236
// Build VIR and run verification

‎source/rust_verify_test/tests/basic.rs

Lines changed: 0 additions & 75 deletions
Original file line numberDiff line numberDiff line change
@@ -641,78 +641,3 @@ test_verify_one_file! {
641641
}
642642
} => Ok(())
643643
}
644-
645-
test_verify_one_file_with_options! {
646-
#[test] test_is_core ["--is-core", "no-auto-import-verus_builtin"] => code! {
647-
#![allow(unused_parens)]
648-
#![allow(unused_imports)]
649-
#![allow(dead_code)]
650-
#![allow(unused_attributes)]
651-
#![allow(unused_variables)]
652-
653-
#![cfg_attr(verus_keep_ghost, feature(core_intrinsics))]
654-
#![cfg_attr(verus_keep_ghost, feature(allocator_api))]
655-
#![cfg_attr(verus_keep_ghost, feature(step_trait))]
656-
#![cfg_attr(verus_keep_ghost, feature(ptr_metadata))]
657-
#![cfg_attr(verus_keep_ghost, feature(strict_provenance_atomic_ptr))]
658-
#![cfg_attr(verus_keep_ghost, feature(derive_clone_copy))]
659-
#![cfg_attr(verus_keep_ghost, feature(freeze))]
660-
#![cfg_attr(
661-
verus_keep_ghost,
662-
feature(fn_traits),
663-
)]
664-
#![cfg_attr(verus_keep_ghost, verifier::exec_allows_no_decreases_clause)]
665-
666-
#[verifier::external]
667-
#[path="../../../../builtin/src/lib.rs"]
668-
mod verus_builtin;
669-
670-
#[path="../../../../vstd/vstd.rs"]
671-
mod vstd;
672-
673-
mod test {
674-
use crate::vstd::set::*;
675-
use crate::vstd::seq::*;
676-
use crate::vstd::multiset::*;
677-
use crate::vstd::prelude::*;
678-
679-
verus!{
680-
681-
proof fn test_seqs(a: Seq<int>, b: Seq<int>)
682-
requires a == b,
683-
{
684-
crate::vstd::seq_lib::assert_seqs_equal!(a, b);
685-
crate::vstd::seq_lib::assert_seqs_equal!(a == b);
686-
}
687-
688-
proof fn test_sets(a: Set<int>, b: Set<int>)
689-
requires a == b,
690-
{
691-
crate::vstd::set_lib::assert_sets_equal!(a, b);
692-
crate::vstd::set_lib::assert_sets_equal!(a == b);
693-
}
694-
695-
proof fn test_multisets(a: Multiset<int>, b: Multiset<int>)
696-
requires a == b,
697-
{
698-
crate::vstd::multiset::assert_multisets_equal!(a, b);
699-
crate::vstd::multiset::assert_multisets_equal!(a == b);
700-
}
701-
702-
fn test_slice_index(x: &[u8]) -> u8
703-
requires x@.len() > 0
704-
{
705-
x[0]
706-
}
707-
708-
fn test_ptr_stuff(a: *mut u8, b: *mut [u8; 2]) {
709-
let t = a as *mut u16;
710-
let s = b as *mut [u8];
711-
}
712-
713-
}
714-
}
715-
716-
fn main() { }
717-
} => Ok(())
718-
}

‎source/rust_verify_test/tests/verify_stdlib_special_setup.rs

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
#![feature(rustc_private)]
2+
#[macro_use]
3+
mod common;
4+
use common::*;
5+
6+
test_verify_one_file_with_options! {
7+
#[test] test_is_core ["--is-core", "no-auto-import-verus_builtin"] => code! {
8+
#![allow(unused_parens)]
9+
#![allow(unused_imports)]
10+
#![allow(dead_code)]
11+
#![allow(unused_attributes)]
12+
#![allow(unused_variables)]
13+
14+
#![cfg_attr(verus_keep_ghost, feature(core_intrinsics))]
15+
#![cfg_attr(verus_keep_ghost, feature(allocator_api))]
16+
#![cfg_attr(verus_keep_ghost, feature(step_trait))]
17+
#![cfg_attr(verus_keep_ghost, feature(ptr_metadata))]
18+
#![cfg_attr(verus_keep_ghost, feature(strict_provenance_atomic_ptr))]
19+
#![cfg_attr(verus_keep_ghost, feature(derive_clone_copy))]
20+
#![cfg_attr(verus_keep_ghost, feature(freeze))]
21+
#![cfg_attr(
22+
verus_keep_ghost,
23+
feature(fn_traits),
24+
)]
25+
#![cfg_attr(verus_keep_ghost, verifier::exec_allows_no_decreases_clause)]
26+
27+
#[verifier::external]
28+
#[path="../../../../builtin/src/lib.rs"]
29+
mod verus_builtin;
30+
31+
#[path="../../../../vstd/vstd.rs"]
32+
mod vstd;
33+
34+
mod test {
35+
use crate::vstd::set::*;
36+
use crate::vstd::seq::*;
37+
use crate::vstd::multiset::*;
38+
use crate::vstd::prelude::*;
39+
40+
verus!{
41+
42+
proof fn test_seqs(a: Seq<int>, b: Seq<int>)
43+
requires a == b,
44+
{
45+
crate::vstd::seq_lib::assert_seqs_equal!(a, b);
46+
crate::vstd::seq_lib::assert_seqs_equal!(a == b);
47+
}
48+
49+
proof fn test_sets(a: Set<int>, b: Set<int>)
50+
requires a == b,
51+
{
52+
crate::vstd::set_lib::assert_sets_equal!(a, b);
53+
crate::vstd::set_lib::assert_sets_equal!(a == b);
54+
}
55+
56+
proof fn test_multisets(a: Multiset<int>, b: Multiset<int>)
57+
requires a == b,
58+
{
59+
crate::vstd::multiset::assert_multisets_equal!(a, b);
60+
crate::vstd::multiset::assert_multisets_equal!(a == b);
61+
}
62+
63+
fn test_slice_index(x: &[u8]) -> u8
64+
requires x@.len() > 0
65+
{
66+
x[0]
67+
}
68+
69+
fn test_ptr_stuff(a: *mut u8, b: *mut [u8; 2]) {
70+
let t = a as *mut u16;
71+
let s = b as *mut [u8];
72+
}
73+
74+
}
75+
}
76+
77+
fn main() { }
78+
} => Ok(())
79+
}

‎source/verus/src/main.rs

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -183,6 +183,9 @@ fn run() -> Result<std::process::ExitStatus, String> {
183183

184184
let mut cmd = Command::new("rustup");
185185

186+
let vstd_kind = get_vstd_kind(&args);
187+
cmd.env("VSTD_KIND", vstd_kind);
188+
186189
#[allow(unused_variables)]
187190
let z3_path = if let Some(z3_path) = std::env::var("VERUS_Z3_PATH").ok() {
188191
Some(std::path::PathBuf::from(z3_path))
@@ -481,3 +484,29 @@ fn run() -> Result<std::process::ExitStatus, String> {
481484
Ok(exit_status)
482485
}
483486
}
487+
488+
fn get_vstd_kind(args: &Vec<String>) -> &'static str {
489+
let arg_names = [
490+
("--no-vstd", "NoVstd"),
491+
("--is-vstd", "IsVstd"),
492+
("--is-core", "IsCore"),
493+
("--is-stdlib-outside-of-core", "ImportedViaCore"),
494+
];
495+
let default = "Imported";
496+
497+
let mut found = None;
498+
for (arg_name, kind_string) in arg_names.iter() {
499+
if args.contains(&arg_name.to_string()) {
500+
if found.is_none() {
501+
found = Some((arg_name, kind_string));
502+
} else {
503+
eprintln!("contradictory arguments: {:} and {:}", found.unwrap().0, arg_name);
504+
std::process::exit(255);
505+
}
506+
}
507+
}
508+
match found {
509+
Some((_, kind)) => kind,
510+
_ => default,
511+
}
512+
}

0 commit comments

Comments
 (0)