From 018e8ffad241d9b714567ac8509f5a93151e906e Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Fri, 2 Feb 2024 15:37:12 -0500 Subject: [PATCH 1/3] don't compile Regex in frequently called function get_rust_item --- source/Cargo.lock | 5 +++-- source/rust_verify/Cargo.toml | 1 + source/rust_verify/src/verus_items.rs | 6 ++++-- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/source/Cargo.lock b/source/Cargo.lock index 57aa718474..64a3cd624c 100644 --- a/source/Cargo.lock +++ b/source/Cargo.lock @@ -1033,9 +1033,9 @@ checksum = "830b246a0e5f20af87141b25c173cd1b609bd7779a4617d6ec582abaf90870f3" [[package]] name = "once_cell" -version = "1.18.0" +version = "1.19.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" +checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" [[package]] name = "papergrid" @@ -1445,6 +1445,7 @@ dependencies = [ "internals_interface", "num-bigint 0.4.4", "num-format", + "once_cell", "regex", "rust_verify_test_macros", "serde", diff --git a/source/rust_verify/Cargo.toml b/source/rust_verify/Cargo.toml index fa10ebc3f3..579af27a8a 100644 --- a/source/rust_verify/Cargo.toml +++ b/source/rust_verify/Cargo.toml @@ -19,6 +19,7 @@ regex = "1" internals_interface = { path = "../tools/internals_interface" } indicatif = "0.17.7" console = { version = "0.15", default-features = false, features = ["ansi-parsing"] } +once_cell = { version = "1.19.0" } [target.'cfg(windows)'.dependencies] win32job = "1" diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs index a68aef3758..5d16a51566 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs @@ -1,4 +1,5 @@ use air::ast::Ident; +use once_cell::sync::Lazy; use regex::Regex; use rustc_middle::ty::{TyCtxt, TyKind}; use rustc_span::def_id::DefId; @@ -631,8 +632,9 @@ pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option = + Lazy::new(|| Regex::new(r"^([A-Za-z0-9_]+)::(MIN|MAX|BITS)").unwrap()); + if let Some(captures) = NUM_RE.captures(rust_path) { let ty_name = captures.get(1).expect("invalid int intrinsic regex"); let const_name = captures.get(2).expect("invalid int intrinsic regex"); use RustIntType::*; From 961963b97d95541b26fb9d1028d748a07a0f8c44 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Mon, 5 Feb 2024 09:14:43 -0500 Subject: [PATCH 2/3] remove dep --- source/Cargo.lock | 5 ++--- source/rust_verify/Cargo.toml | 1 - 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/source/Cargo.lock b/source/Cargo.lock index 64a3cd624c..57aa718474 100644 --- a/source/Cargo.lock +++ b/source/Cargo.lock @@ -1033,9 +1033,9 @@ checksum = "830b246a0e5f20af87141b25c173cd1b609bd7779a4617d6ec582abaf90870f3" [[package]] name = "once_cell" -version = "1.19.0" +version = "1.18.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" +checksum = "dd8b5dd2ae5ed71462c540258bedcb51965123ad7e7ccf4b9a8cafaa4a63576d" [[package]] name = "papergrid" @@ -1445,7 +1445,6 @@ dependencies = [ "internals_interface", "num-bigint 0.4.4", "num-format", - "once_cell", "regex", "rust_verify_test_macros", "serde", diff --git a/source/rust_verify/Cargo.toml b/source/rust_verify/Cargo.toml index 579af27a8a..fa10ebc3f3 100644 --- a/source/rust_verify/Cargo.toml +++ b/source/rust_verify/Cargo.toml @@ -19,7 +19,6 @@ regex = "1" internals_interface = { path = "../tools/internals_interface" } indicatif = "0.17.7" console = { version = "0.15", default-features = false, features = ["ansi-parsing"] } -once_cell = { version = "1.19.0" } [target.'cfg(windows)'.dependencies] win32job = "1" From 3a046a6f1e935b9891b145252551653dc7227908 Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Mon, 5 Feb 2024 09:19:40 -0500 Subject: [PATCH 3/3] use std::sync::OnceLock instead --- source/rust_verify/src/verus_items.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs index 5d16a51566..6956e4925a 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs @@ -1,5 +1,4 @@ use air::ast::Ident; -use once_cell::sync::Lazy; use regex::Regex; use rustc_middle::ty::{TyCtxt, TyKind}; use rustc_span::def_id::DefId; @@ -632,9 +631,10 @@ pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option = - Lazy::new(|| Regex::new(r"^([A-Za-z0-9_]+)::(MIN|MAX|BITS)").unwrap()); - if let Some(captures) = NUM_RE.captures(rust_path) { + static NUM_RE: std::sync::OnceLock = std::sync::OnceLock::new(); + let num_re = + NUM_RE.get_or_init(|| Regex::new(r"^([A-Za-z0-9_]+)::(MIN|MAX|BITS)").unwrap()); + if let Some(captures) = num_re.captures(rust_path) { let ty_name = captures.get(1).expect("invalid int intrinsic regex"); let const_name = captures.get(2).expect("invalid int intrinsic regex"); use RustIntType::*;