diff --git a/.gitignore b/.gitignore index df077f1120..ea6f50c445 100644 --- a/.gitignore +++ b/.gitignore @@ -54,4 +54,5 @@ output/ *.bpl.log .sparse -crates/sui-prover/tests/sources/* \ No newline at end of file +crates/sui-prover/tests/sources/* +settings.local.json diff --git a/Cargo.lock b/Cargo.lock index 02491a120d..8950658010 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -897,7 +897,7 @@ dependencies = [ [[package]] name = "enum-compat-util" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "serde_yaml", ] @@ -1827,7 +1827,7 @@ dependencies = [ [[package]] name = "jsonrpc" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "serde", "serde_json", @@ -2097,17 +2097,17 @@ dependencies = [ [[package]] name = "move-abstract-interpreter" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" [[package]] name = "move-abstract-stack" version = "0.0.1" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" [[package]] name = "move-binary-format" version = "0.0.3" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "enum-compat-util", @@ -2123,12 +2123,12 @@ dependencies = [ [[package]] name = "move-borrow-graph" version = "0.0.1" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" [[package]] name = "move-bytecode-source-map" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "bcs", @@ -2144,7 +2144,7 @@ dependencies = [ [[package]] name = "move-bytecode-utils" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "indexmap 2.13.0", @@ -2157,7 +2157,7 @@ dependencies = [ [[package]] name = "move-bytecode-verifier" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "move-abstract-interpreter", "move-abstract-stack", @@ -2174,7 +2174,7 @@ dependencies = [ [[package]] name = "move-bytecode-verifier-meter" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "move-binary-format", "move-core-types", @@ -2184,7 +2184,7 @@ dependencies = [ [[package]] name = "move-command-line-common" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "bcs", @@ -2204,7 +2204,7 @@ dependencies = [ [[package]] name = "move-compiler" version = "0.0.1" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "bcs", @@ -2239,7 +2239,7 @@ dependencies = [ [[package]] name = "move-core-types" version = "0.0.4" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "bcs", @@ -2263,7 +2263,7 @@ dependencies = [ [[package]] name = "move-coverage" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "bcs", @@ -2288,7 +2288,7 @@ dependencies = [ [[package]] name = "move-disassembler" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "bcs", @@ -2309,7 +2309,7 @@ dependencies = [ [[package]] name = "move-docgen" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "clap", @@ -2331,7 +2331,7 @@ dependencies = [ [[package]] name = "move-ir-to-bytecode" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "codespan-reporting", @@ -2349,7 +2349,7 @@ dependencies = [ [[package]] name = "move-ir-to-bytecode-syntax" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "hex", @@ -2362,7 +2362,7 @@ dependencies = [ [[package]] name = "move-ir-types" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "hex", "move-command-line-common", @@ -2391,7 +2391,6 @@ dependencies = [ "move-ir-types", "move-symbol-pool", "num", - "once_cell", "regex", "serde", ] @@ -2399,7 +2398,7 @@ dependencies = [ [[package]] name = "move-model" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "codespan", @@ -2423,7 +2422,7 @@ dependencies = [ [[package]] name = "move-model-2" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "bcs", @@ -2447,7 +2446,7 @@ dependencies = [ [[package]] name = "move-package" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "clap", @@ -2483,7 +2482,7 @@ dependencies = [ [[package]] name = "move-package-alt" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "append-only-vec", @@ -2526,7 +2525,7 @@ dependencies = [ [[package]] name = "move-package-alt-compilation" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "clap", @@ -2554,7 +2553,7 @@ dependencies = [ [[package]] name = "move-proc-macros" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "enum-compat-util", "quote", @@ -2583,7 +2582,6 @@ dependencies = [ "move-stackless-bytecode", "nix 0.29.0", "num", - "once_cell", "pretty", "rand 0.8.5", "regex", @@ -2600,7 +2598,7 @@ dependencies = [ [[package]] name = "move-regex-borrow-graph" version = "0.0.1" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "indexmap 2.13.0", "insta", @@ -2636,7 +2634,6 @@ dependencies = [ "move-stdlib", "move-symbol-pool", "num", - "once_cell", "paste", "petgraph", "regex", @@ -2646,7 +2643,7 @@ dependencies = [ [[package]] name = "move-stdlib" version = "0.1.1" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "hex", @@ -2666,7 +2663,7 @@ dependencies = [ [[package]] name = "move-symbol-pool" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "phf", "serde", @@ -2675,7 +2672,7 @@ dependencies = [ [[package]] name = "move-trace-format" version = "0.0.1" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "move-binary-format", "move-core-types", @@ -2687,7 +2684,7 @@ dependencies = [ [[package]] name = "move-vm-config" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "move-binary-format", ] @@ -2695,7 +2692,7 @@ dependencies = [ [[package]] name = "move-vm-profiler" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "move-trace-format", "move-vm-config", @@ -2707,7 +2704,7 @@ dependencies = [ [[package]] name = "move-vm-runtime" version = "0.1.0" -source = "git+https://github.com/asymptotic-code/sui?branch=next#c9181db4d7ca8dd12f93107f32a88fde290ae77f" +source = "git+https://github.com/asymptotic-code/sui?branch=next#321cf9102594b6ad3338b77735e1b55af92ab0ee" dependencies = [ "anyhow", "bcs", diff --git a/Cargo.toml b/Cargo.toml index 42b63b2256..42573c8831 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -42,7 +42,6 @@ colored = "2.0.0" tracing = "0.1.37" bimap = "0.6.2" serde = { version = "1.0.144", features = ["derive", "rc"] } -once_cell = "1.18.0" toml = { version = "0.7.4", features = ["preserve_order"] } async-trait = "0.1.61" itertools = "0.13.0" diff --git a/crates/move-model/CLAUDE.md b/crates/move-model/CLAUDE.md index 3682d55b8a..ba9fc3d85a 100644 --- a/crates/move-model/CLAUDE.md +++ b/crates/move-model/CLAUDE.md @@ -147,7 +147,7 @@ The crate defines well-known identifiers for: ## Important Design Patterns 1. **Reference-based access**: `ModuleEnv`, `FunctionEnv` are references, not owned data -2. **Lazy caching**: Call graphs computed on first access via `RefCell>` +2. **LazyLock caching**: Call graphs computed on first access via `RefCell>` 3. **Source mapping**: `FileId` → codespan Files database for error reporting 4. **Extensions**: `BTreeMap>` for tool-specific data diff --git a/crates/move-model/Cargo.toml b/crates/move-model/Cargo.toml index 158237c596..68a67b616a 100644 --- a/crates/move-model/Cargo.toml +++ b/crates/move-model/Cargo.toml @@ -3,9 +3,8 @@ name = "move-model" version = "0.1.0" authors = ["Diem Association "] publish = false -edition = "2021" +edition = "2024" license = "Apache-2.0" - [lints] workspace = true @@ -27,7 +26,6 @@ internment.workspace = true itertools.workspace = true log.workspace = true num.workspace = true -once_cell.workspace = true regex.workspace = true anyhow.workspace = true serde.workspace = true diff --git a/crates/move-model/src/ast.rs b/crates/move-model/src/ast.rs index 2c23a9da06..e999fb2ec5 100644 --- a/crates/move-model/src/ast.rs +++ b/crates/move-model/src/ast.rs @@ -10,10 +10,10 @@ use std::{ fmt, fmt::{Debug, Error, Formatter}, hash::Hash, + sync::LazyLock, }; use num::{BigInt, BigUint, Num}; -use once_cell::sync::Lazy; use crate::{ model::{GlobalId, NodeId}, @@ -99,8 +99,8 @@ impl ModuleName { /// Determine whether this is a script. The move-compiler infrastructure uses MAX_ADDR /// for pseudo modules created from scripts, so use this address to check. pub fn is_script(&self) -> bool { - static MAX_ADDR: Lazy = - Lazy::new(|| BigUint::from_str_radix(MAX_ADDR_STRING, 16).expect("valid hex")); + static MAX_ADDR: LazyLock = + LazyLock::new(|| BigUint::from_str_radix(MAX_ADDR_STRING, 16).expect("valid hex")); self.0 == *MAX_ADDR } } diff --git a/crates/move-model/src/builder/exp_translator.rs b/crates/move-model/src/builder/exp_translator.rs index d65b9ba76a..47f0635c84 100644 --- a/crates/move-model/src/builder/exp_translator.rs +++ b/crates/move-model/src/builder/exp_translator.rs @@ -484,7 +484,7 @@ impl ExpTranslator<'_, '_, '_> { return check_zero_args(self, Type::new_prim(PrimitiveType::U128)); } "u256" => { - return check_zero_args(self, Type::new_prim(PrimitiveType::U256)) + return check_zero_args(self, Type::new_prim(PrimitiveType::U256)); } "num" => return check_zero_args(self, Type::new_prim(PrimitiveType::Num)), "range" => { diff --git a/crates/move-model/src/builder/module_builder.rs b/crates/move-model/src/builder/module_builder.rs index 1f5aafb6a9..07ccb5a68d 100644 --- a/crates/move-model/src/builder/module_builder.rs +++ b/crates/move-model/src/builder/module_builder.rs @@ -6,15 +6,15 @@ use itertools::Itertools; use std::collections::BTreeMap; use move_binary_format::{ - file_format::{Constant, EnumDefinitionIndex, FunctionDefinitionIndex, StructDefinitionIndex}, CompiledModule, + file_format::{Constant, EnumDefinitionIndex, FunctionDefinitionIndex, StructDefinitionIndex}, }; use move_bytecode_source_map::source_map::SourceMap; use move_compiler::{ compiled_unit::FunctionInfo, expansion::ast as EA, parser::ast::{self as PA}, - shared::{unique_map::UniqueMap, Name}, + shared::{Name, unique_map::UniqueMap}, }; use move_ir_types::ast::ConstantName; @@ -26,7 +26,7 @@ use crate::{ }, model::{ DatatypeId, EnumData, FunId, FunctionData, FunctionVisibility, Loc, ModuleId, - NamedConstantData, NamedConstantId, StructData, SCRIPT_BYTECODE_FUN_NAME, + NamedConstantData, NamedConstantId, SCRIPT_BYTECODE_FUN_NAME, StructData, }, project_1st, symbol::{Symbol, SymbolPool}, diff --git a/crates/move-model/src/code_writer.rs b/crates/move-model/src/code_writer.rs index d316ca0368..cd19de8ca9 100644 --- a/crates/move-model/src/code_writer.rs +++ b/crates/move-model/src/code_writer.rs @@ -8,7 +8,7 @@ //! so its on the bottom of the dependency relation, and there is no `utility` crate //! where it could belong to. -use std::{collections::BTreeMap, fmt::Debug, ops::Bound}; +use std::{collections::BTreeMap, ops::Bound}; use codespan::{ByteIndex, ByteOffset, ColumnIndex, Files, LineIndex, RawIndex, RawOffset}; diff --git a/crates/move-model/src/lib.rs b/crates/move-model/src/lib.rs index dfdbdc5034..35c5462db0 100644 --- a/crates/move-model/src/lib.rs +++ b/crates/move-model/src/lib.rs @@ -20,14 +20,13 @@ use move_binary_format::file_format::{ CompiledModule, EnumDefinitionIndex, FunctionDefinitionIndex, StructDefinitionIndex, }; use move_compiler::{ - self, + self, Compiler, Flags, PASS_COMPILATION, PASS_EXPANSION, PASS_PARSER, PASS_TYPING, compiled_unit::{self, AnnotatedCompiledUnit}, - diagnostics::{warning_filters::WarningFiltersBuilder, Diagnostics}, + diagnostics::{Diagnostics, warning_filters::WarningFiltersBuilder}, expansion::ast::{self as E, ModuleIdent, ModuleIdent_}, parser::ast::{self as P, TargetKind}, - shared::{parse_named_address, unique_map::UniqueMap, NumericalAddress, PackagePaths}, + shared::{NumericalAddress, PackagePaths, parse_named_address, unique_map::UniqueMap}, typing::ast as T, - Compiler, Flags, PASS_COMPILATION, PASS_EXPANSION, PASS_PARSER, PASS_TYPING, }; use move_core_types::account_address::AccountAddress; use move_symbol_pool::Symbol as MoveSymbol; diff --git a/crates/move-model/src/model.rs b/crates/move-model/src/model.rs index e68a2656e8..719f5f9c35 100644 --- a/crates/move-model/src/model.rs +++ b/crates/move-model/src/model.rs @@ -28,7 +28,7 @@ use anyhow::bail; use codespan::{ByteIndex, ByteOffset, ColumnOffset, FileId, Files, LineOffset, Location, Span}; use codespan_reporting::{ diagnostic::{Diagnostic, Label, Severity}, - term::{emit, termcolor::WriteColor, Config}, + term::{Config, emit, termcolor::WriteColor}, }; use itertools::Itertools; #[allow(unused_imports)] @@ -41,13 +41,13 @@ use serde::{Deserialize, Serialize}; pub use move_binary_format::file_format::{AbilitySet, Visibility as FunctionVisibility}; use move_binary_format::{ + CompiledModule, file_format::{ AddressIdentifierIndex, Bytecode, Constant as VMConstant, ConstantPoolIndex, DatatypeHandleIndex, EnumDefinitionIndex, FunctionDefinition, FunctionDefinitionIndex, FunctionHandleIndex, IdentifierIndex, ModuleHandle, SignatureIndex, SignatureToken, StructDefinitionIndex, StructFieldInformation, VariantJumpTable, Visibility, }, - CompiledModule, }; use move_bytecode_source_map::{mapping::SourceMapping, source_map::SourceMap}; use move_command_line_common::files::FileHash; @@ -1088,7 +1088,7 @@ impl GlobalEnv { .make(module.identifier_at(variant.variant_name).as_str()); let loc = match enum_smap { None => Loc::default(), - Some(smap) => self.to_loc(&smap.variants[tag].0 .1), + Some(smap) => self.to_loc(&smap.variants[tag].0.1), }; variant_data.insert( VariantId(variant_name), @@ -6298,10 +6298,11 @@ impl<'env> FunctionEnv<'env> { .module .function_instantiation_at(*i) .handle; - vec![self - .module_env - .get_used_function(handle_idx) - .get_qualified_id()] + vec![ + self.module_env + .get_used_function(handle_idx) + .get_qualified_id(), + ] } Bytecode::VecPack { .. } => vec![ self.module_env.env.get_fun_qid("vector", "empty"), diff --git a/crates/move-model/src/pragmas.rs b/crates/move-model/src/pragmas.rs index b32c5f2141..0dfd4dfe47 100644 --- a/crates/move-model/src/pragmas.rs +++ b/crates/move-model/src/pragmas.rs @@ -4,9 +4,7 @@ //! Provides pragmas and properties of the specification language. -use std::collections::BTreeMap; - -use once_cell::sync::Lazy; +use std::{collections::BTreeMap, sync::LazyLock}; /// Pragma indicating whether verification should be performed for a function. pub const VERIFY_PRAGMA: &str = "verify"; @@ -152,8 +150,8 @@ pub const INTRINSIC_FUN_MAP_BORROW: &str = "map_borrow"; pub const INTRINSIC_FUN_MAP_BORROW_MUT: &str = "map_borrow_mut"; /// All intrinsic functions associated with the map type -pub static INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS: Lazy> = - Lazy::new(|| { +pub static INTRINSIC_TYPE_MAP_ASSOC_FUNCTIONS: LazyLock> = + LazyLock::new(|| { BTreeMap::from([ (INTRINSIC_FUN_MAP_NEW, true), (INTRINSIC_FUN_MAP_SPEC_NEW, false), diff --git a/crates/move-prover-boogie-backend/Cargo.toml b/crates/move-prover-boogie-backend/Cargo.toml index f98d622a4a..58246de7b3 100644 --- a/crates/move-prover-boogie-backend/Cargo.toml +++ b/crates/move-prover-boogie-backend/Cargo.toml @@ -21,7 +21,6 @@ itertools.workspace = true log.workspace = true serde.workspace = true anyhow.workspace = true -once_cell.workspace = true pretty.workspace = true regex.workspace = true rand.workspace = true diff --git a/crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs b/crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs index 5000bb8823..885e026539 100644 --- a/crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs +++ b/crates/move-prover-boogie-backend/src/boogie_backend/boogie_wrapper.rs @@ -19,12 +19,12 @@ use codespan_reporting::diagnostic::{Diagnostic, Label}; use itertools::Itertools; use log::{debug, info, warn}; use num::{BigInt, BigUint}; -use once_cell::sync::Lazy; use pretty::RcDoc; use regex::Regex; use reqwest; use serde::Deserialize; use serde_json::json; +use std::sync::LazyLock; use move_binary_format::file_format::FunctionDefinitionIndex; use move_model::{ @@ -113,30 +113,30 @@ pub enum TraceEntry { } // Error message matching -static VERIFICATION_DIAG_STARTS: Lazy = - Lazy::new(|| Regex::new(r"(?m)^assert_failed\((?P[^)]*)\): (?P.*)$").unwrap()); +static VERIFICATION_DIAG_STARTS: LazyLock = + LazyLock::new(|| Regex::new(r"(?m)^assert_failed\((?P[^)]*)\): (?P.*)$").unwrap()); /// Matches `assert {:msg "assert_failed(file_idx,start,end): message"}` in .bpl files. -static BPL_ASSERT_MSG: Lazy = Lazy::new(|| { +static BPL_ASSERT_MSG: LazyLock = LazyLock::new(|| { Regex::new(r#"assert \{:msg "assert_failed\((?P[^)]*)\): (?P[^"]*)"\}"#).unwrap() }); /// Matches `checking split N/M (line NNNN)` in Boogie trace output. -static CHECKING_SPLIT: Lazy = Lazy::new(|| { +static CHECKING_SPLIT: LazyLock = LazyLock::new(|| { Regex::new(r"checking split (?P\d+)/(?P\d+) \(line (?P\d+)\)").unwrap() }); -static INCONCLUSIVE_DIAG_STARTS: Lazy = Lazy::new(|| { +static INCONCLUSIVE_DIAG_STARTS: LazyLock = LazyLock::new(|| { Regex::new(r"(?m)^.*\((?P\d+),(?P\d+)\).*Verification(?P.*)(inconclusive|out of resource|timed out).*$") .unwrap() }); -static INCONSISTENCY_DIAG_STARTS: Lazy = - Lazy::new(|| Regex::new(r"(?m)^inconsistency_detected\((?P[^)]*)\)").unwrap()); +static INCONSISTENCY_DIAG_STARTS: LazyLock = + LazyLock::new(|| Regex::new(r"(?m)^inconsistency_detected\((?P[^)]*)\)").unwrap()); /// Matches Boogie verbose/trace output lines produced by `-trace -traceverify` flags. /// These are informational progress indicators, not verification diagnostics. -static BOOGIE_TRACE_NOISE: Lazy = Lazy::new(|| { +static BOOGIE_TRACE_NOISE: LazyLock = LazyLock::new(|| { Regex::new( r"(?m)^(Parsing |Coalescing blocks|Inlining|Verifying .+ \.\.\.|.*checking split |.*-->.*split|.*finished with |Boogie program verifier finished|New lambda:|Old lambda:|Desugaring of lambda|Running abstract interpretation|Implementation .* verified|\s*\[[\d.]+ s)", ) @@ -144,20 +144,21 @@ static BOOGIE_TRACE_NOISE: Lazy = Lazy::new(|| { }); /// Matches secondary label annotations embedded in error messages: ` @{(file,start,end):message}` -static SECONDARY_LABEL: Lazy = Lazy::new(|| { +static SECONDARY_LABEL: LazyLock = LazyLock::new(|| { Regex::new(r" @\{\((?P\d+),(?P\d+),(?P\d+)\):(?P[^}]*)\}").unwrap() }); /// Matches procedure declarations in .bpl files, capturing the procedure name. -static BPL_PROC_DECL: Lazy = - Lazy::new(|| Regex::new(r"^procedure\s+(?:\{[^}]*\}\s+)*(\$\S+)\(").unwrap()); +static BPL_PROC_DECL: LazyLock = + LazyLock::new(|| Regex::new(r"^procedure\s+(?:\{[^}]*\}\s+)*(\$\S+)\(").unwrap()); /// Matches call statements in .bpl files, capturing the called procedure name. -static BPL_CALL_STMT: Lazy = - Lazy::new(|| Regex::new(r"call\s+(?:.*:=\s+)?(\$[a-zA-Z0-9_'$#]+)\(").unwrap()); +static BPL_CALL_STMT: LazyLock = + LazyLock::new(|| Regex::new(r"call\s+(?:.*:=\s+)?(\$[a-zA-Z0-9_'$#]+)\(").unwrap()); /// Matches `$at(file_idx,start,end)` location annotations in .bpl files. -static BPL_AT_LOC: Lazy = Lazy::new(|| Regex::new(r#"\$at\((\d+),(\d+),(\d+)\)"#).unwrap()); +static BPL_AT_LOC: LazyLock = + LazyLock::new(|| Regex::new(r#"\$at\((\d+),(\d+),(\d+)\)"#).unwrap()); /// Information about an assertion in a .bpl file, for trace output. struct AssertInfo { @@ -1423,7 +1424,7 @@ impl<'env> BoogieWrapper<'env> { /// Extracts the model. fn extract_model(&self, model: &mut Model, out: &str, at: &mut usize) { - static MODEL_REGION: Lazy = Lazy::new(|| { + static MODEL_REGION: LazyLock = LazyLock::new(|| { Regex::new(r"(?m)^\*\*\* MODEL$(?P(?s:.)*?^\*\*\* END_MODEL$)").unwrap() }); @@ -1452,9 +1453,9 @@ impl<'env> BoogieWrapper<'env> { /// Extracts the plain execution trace. fn extract_execution_trace(&self, out: &str, at: &mut usize) -> Vec { - static TRACE_START: Lazy = - Lazy::new(|| Regex::new(r"(?m)^Execution trace:\s*$").unwrap()); - static TRACE_ENTRY: Lazy = Lazy::new(|| { + static TRACE_START: LazyLock = + LazyLock::new(|| Regex::new(r"(?m)^Execution trace:\s*$").unwrap()); + static TRACE_ENTRY: LazyLock = LazyLock::new(|| { Regex::new(r"^\s+(?P[^(]+)\((?P[^)]*)\): (?P.*)\n").unwrap() }); let mut result = vec![]; @@ -1473,9 +1474,9 @@ impl<'env> BoogieWrapper<'env> { /// Extracts augmented execution trace. fn extract_augmented_trace(&self, out: &str, at: &mut usize) -> Vec { - static TRACE_START: Lazy = - Lazy::new(|| Regex::new(r"(?m)^Augmented execution trace:\s*$").unwrap()); - static TRACE_ENTRY: Lazy = Lazy::new(|| { + static TRACE_START: LazyLock = + LazyLock::new(|| Regex::new(r"(?m)^Augmented execution trace:\s*$").unwrap()); + static TRACE_ENTRY: LazyLock = LazyLock::new(|| { Regex::new(r"^\s*\$(?P[a-zA-Z_]+)\((?P[^)]*)\)(:(?P.*))?\n").unwrap() }); let mut result = vec![]; diff --git a/crates/move-prover-boogie-backend/src/boogie_backend/options.rs b/crates/move-prover-boogie-backend/src/boogie_backend/options.rs index 9b946952df..47cfbf9c8d 100644 --- a/crates/move-prover-boogie-backend/src/boogie_backend/options.rs +++ b/crates/move-prover-boogie-backend/src/boogie_backend/options.rs @@ -152,7 +152,7 @@ pub struct BoogieOptions { pub keep_artifacts: bool, /// Eager threshold for quantifier instantiation. pub eager_threshold: usize, - /// Lazy threshold for quantifier instantiation. + /// LazyLock threshold for quantifier instantiation. pub lazy_threshold: usize, /// Whether to use the new Boogie `{:debug ..}` attribute for tracking debug values. pub stable_test_output: bool, diff --git a/crates/move-prover-boogie-backend/src/generator_options.rs b/crates/move-prover-boogie-backend/src/generator_options.rs index 8c6cd905bc..6144534f3b 100644 --- a/crates/move-prover-boogie-backend/src/generator_options.rs +++ b/crates/move-prover-boogie-backend/src/generator_options.rs @@ -16,11 +16,11 @@ use anyhow::anyhow; use clap::{Arg, Command}; use log::LevelFilter; use move_compiler::shared::NumericalAddress; -use once_cell::sync::Lazy; use serde::{Deserialize, Serialize}; use simplelog::{ CombinedLogger, Config, ConfigBuilder, LevelPadding, SimpleLogger, TermLogger, TerminalMode, }; +use std::sync::LazyLock; use crate::boogie_backend::options::{BoogieOptions, RemoteOptions, VectorTheory}; use codespan_reporting::diagnostic::Severity; @@ -100,7 +100,7 @@ impl Default for Options { } } -pub static DEFAULT_OPTIONS: Lazy = Lazy::new(|| Options::default()); +pub static DEFAULT_OPTIONS: LazyLock = LazyLock::new(|| Options::default()); impl Options { /// Creates options from toml configuration source. diff --git a/crates/move-stackless-bytecode/Cargo.toml b/crates/move-stackless-bytecode/Cargo.toml index c0cbfc0b87..471214e2ee 100644 --- a/crates/move-stackless-bytecode/Cargo.toml +++ b/crates/move-stackless-bytecode/Cargo.toml @@ -32,7 +32,6 @@ itertools.workspace = true log.workspace = true paste.workspace = true petgraph.workspace = true -once_cell.workspace = true serde.workspace = true clap.workspace = true diff --git a/crates/sui-prover/tests/snapshots/spec_paths/wrong_module.move.snap b/crates/sui-prover/tests/snapshots/spec_paths/wrong_module.move.snap index 7ee18a56de..2f2f68870b 100644 --- a/crates/sui-prover/tests/snapshots/spec_paths/wrong_module.move.snap +++ b/crates/sui-prover/tests/snapshots/spec_paths/wrong_module.move.snap @@ -6,11 +6,5 @@ exiting with model building errors error: unexpected name in this position ┌─ tests/inputs/spec_paths/wrong_module.move:12:28 │ -10 │ use 0x42::foo; - │ --- Similarly named defintion found here -11 │ 12 │ #[spec(prove, target = bar::inc)] - │ ^^^ - │ │ - │ Could not resolve the name 'bar' - │ Did you mean: 'foo' + │ ^^^^^^^^ Unexpected module identifier. A module identifier is not a valid expression