From ebc35a8594fba8d9907f482c4a3730a7170decdd Mon Sep 17 00:00:00 2001 From: Wolfgang Grieskamp Date: Mon, 20 Jan 2025 11:57:58 -0800 Subject: [PATCH] [move-prover] Sharding feature + re-animate Prover.toml Boogie is using exhaustive amounts of memory if run as part of proving aptos-framework (100GB+), which makes CI and local testing fail randomly. This PR introduces a new `--shards` option which splits the Boogie job into multiple shards, if specified. Also re-animates the use of `Prover.toml` in a package directory allowing to set such options. --- .../framework/aptos-framework/Prover.toml | 2 + aptos-move/framework/aptos-stdlib/Prover.toml | 2 + aptos-move/framework/aptos-token/Prover.toml | 2 + aptos-move/framework/src/prover.rs | 116 +++++++++--------- .../framework/tests/move_prover_tests.rs | 14 ++- .../boogie-backend/src/bytecode_translator.rs | 45 +++++-- .../move-prover/boogie-backend/src/options.rs | 9 +- .../move/move-prover/lab/src/benchmark.rs | 2 +- third_party/move/move-prover/src/lib.rs | 75 +++++++---- 9 files changed, 168 insertions(+), 99 deletions(-) create mode 100644 aptos-move/framework/aptos-framework/Prover.toml create mode 100644 aptos-move/framework/aptos-stdlib/Prover.toml create mode 100644 aptos-move/framework/aptos-token/Prover.toml diff --git a/aptos-move/framework/aptos-framework/Prover.toml b/aptos-move/framework/aptos-framework/Prover.toml new file mode 100644 index 00000000000000..cb697d343cc1c7 --- /dev/null +++ b/aptos-move/framework/aptos-framework/Prover.toml @@ -0,0 +1,2 @@ +[backend] +shards = 6 diff --git a/aptos-move/framework/aptos-stdlib/Prover.toml b/aptos-move/framework/aptos-stdlib/Prover.toml new file mode 100644 index 00000000000000..9d985f260bbf98 --- /dev/null +++ b/aptos-move/framework/aptos-stdlib/Prover.toml @@ -0,0 +1,2 @@ +[backend] +shards = 2 diff --git a/aptos-move/framework/aptos-token/Prover.toml b/aptos-move/framework/aptos-token/Prover.toml new file mode 100644 index 00000000000000..9d985f260bbf98 --- /dev/null +++ b/aptos-move/framework/aptos-token/Prover.toml @@ -0,0 +1,2 @@ +[backend] +shards = 2 diff --git a/aptos-move/framework/src/prover.rs b/aptos-move/framework/src/prover.rs index 56952fbae1a9bc..ccf3a5acfbf76e 100644 --- a/aptos-move/framework/src/prover.rs +++ b/aptos-move/framework/src/prover.rs @@ -22,7 +22,7 @@ use std::{ }; use tempfile::TempDir; -#[derive(Debug, Clone, clap::Parser, serde::Serialize, serde::Deserialize)] +#[derive(Debug, Clone, Default, clap::Parser, serde::Serialize, serde::Deserialize)] pub struct ProverOptions { /// Verbosity level #[clap(long, short)] @@ -50,20 +50,30 @@ pub struct ProverOptions { pub cvc5: bool, /// The depth until which stratified functions are expanded. - #[clap(long, default_value_t = 6)] - pub stratification_depth: usize, + #[clap(long)] + pub stratification_depth: Option, /// A seed for the prover. - #[clap(long, default_value_t = 0)] - pub random_seed: usize, + #[clap(long)] + pub random_seed: Option, /// The number of cores to use for parallel processing of verification conditions. - #[clap(long, default_value_t = 4)] - pub proc_cores: usize, + #[clap(long)] + pub proc_cores: Option, + + /// The number of shards to split the verification problem into. Shards are + /// processed sequentially. This can be used to ease memory pressure for verification + /// of large packages. + #[clap(long)] + pub shards: Option, + + /// If there are multiple shards, the shard to which verification shall be narrowed. + #[clap(long)] + pub only_shard: Option, /// A (soft) timeout for the solver, per verification condition, in seconds. - #[clap(long, default_value_t = 40)] - pub vc_timeout: usize, + #[clap(long)] + pub vc_timeout: Option, /// Whether to disable global timeout overwrite. /// With this flag set to true, the value set by "--vc-timeout" will be used globally @@ -118,32 +128,6 @@ pub struct ProverOptions { pub for_test: bool, } -impl Default for ProverOptions { - fn default() -> Self { - Self { - verbosity: None, - filter: None, - only: None, - trace: false, - cvc5: false, - stratification_depth: 6, - random_seed: 0, - proc_cores: 4, - vc_timeout: 40, - disallow_global_timeout_to_be_overwritten: false, - check_inconsistency: false, - unconditional_abort_as_inconsistency: false, - keep_loops: false, - loop_unroll: None, - stable_test_output: false, - dump: false, - benchmark: false, - for_test: false, - skip_instance_check: false, - } - } -} - impl ProverOptions { /// Runs the move prover on the package. pub fn prove( @@ -173,7 +157,7 @@ impl ProverOptions { known_attributes.clone(), experiments.to_vec(), )?; - let mut options = self.convert_options(); + let mut options = self.convert_options(package_path)?; options.language_version = language_version; options.model_builder.language_version = language_version.unwrap_or_default(); if compiler_version.unwrap_or_default() >= CompilerVersion::V2_0 @@ -225,65 +209,79 @@ impl ProverOptions { Ok(()) } - fn convert_options(self) -> move_prover::cli::Options { + fn convert_options(self, package_path: &Path) -> anyhow::Result { + let prover_toml = package_path.join("Prover.toml"); + let base_opts = if prover_toml.exists() { + Options::create_from_toml_file(prover_toml.to_string_lossy().as_ref())? + } else { + Options::default() + }; let verbosity_level = if let Some(level) = self.verbosity { level } else if self.for_test { LevelFilter::Warn } else { - LevelFilter::Info + base_opts.verbosity_level }; - let opts = move_prover::cli::Options { + let opts = Options { output_path: "".to_string(), verbosity_level, prover: move_prover_bytecode_pipeline::options::ProverOptions { verify_scope: if let Some(name) = self.only { VerificationScope::Only(name) } else { - VerificationScope::All + base_opts.prover.verify_scope.clone() }, - stable_test_output: self.stable_test_output, + stable_test_output: self.stable_test_output || base_opts.prover.stable_test_output, auto_trace_level: if self.trace { move_prover_bytecode_pipeline::options::AutoTraceLevel::VerifiedFunction } else { - move_prover_bytecode_pipeline::options::AutoTraceLevel::Off + base_opts.prover.auto_trace_level }, report_severity: Severity::Warning, - dump_bytecode: self.dump, + dump_bytecode: self.dump || base_opts.prover.dump_bytecode, dump_cfg: false, - check_inconsistency: self.check_inconsistency, - unconditional_abort_as_inconsistency: self.unconditional_abort_as_inconsistency, - skip_loop_analysis: self.keep_loops, - ..Default::default() + check_inconsistency: self.check_inconsistency + || base_opts.prover.check_inconsistency, + unconditional_abort_as_inconsistency: self.unconditional_abort_as_inconsistency + || base_opts.prover.unconditional_abort_as_inconsistency, + skip_loop_analysis: self.keep_loops + || base_opts.prover.unconditional_abort_as_inconsistency, + ..base_opts.prover.clone() }, backend: move_prover_boogie_backend::options::BoogieOptions { - use_cvc5: self.cvc5, + use_cvc5: self.cvc5 || base_opts.backend.use_cvc5, boogie_flags: vec![], - generate_smt: self.dump, - stratification_depth: self.stratification_depth, - proc_cores: self.proc_cores, - vc_timeout: self.vc_timeout, + generate_smt: self.dump || base_opts.backend.generate_smt, + stratification_depth: self + .stratification_depth + .unwrap_or(base_opts.backend.stratification_depth), + proc_cores: self.proc_cores.unwrap_or(base_opts.backend.proc_cores), + shards: self.shards.unwrap_or(base_opts.backend.shards), + only_shard: self.only_shard.or(base_opts.backend.only_shard), + vc_timeout: self.vc_timeout.unwrap_or(base_opts.backend.vc_timeout), global_timeout_overwrite: !self.disallow_global_timeout_to_be_overwritten, - keep_artifacts: self.dump, - stable_test_output: self.stable_test_output, + keep_artifacts: self.dump || base_opts.backend.keep_artifacts, + stable_test_output: self.stable_test_output || base_opts.backend.stable_test_output, z3_trace_file: if self.dump { Some("z3.trace".to_string()) } else { None }, custom_natives: None, - loop_unroll: self.loop_unroll, - skip_instance_check: self.skip_instance_check, - ..Default::default() + loop_unroll: self.loop_unroll.or(base_opts.backend.loop_unroll), + skip_instance_check: self.skip_instance_check + || base_opts.backend.skip_instance_check, + ..base_opts.backend }, - ..Default::default() + ..base_opts }; if self.for_test { opts.setup_logging_for_test(); } else { opts.setup_logging() } - opts + Ok(opts) } pub fn default_for_test() -> Self { diff --git a/aptos-move/framework/tests/move_prover_tests.rs b/aptos-move/framework/tests/move_prover_tests.rs index 9bb09f7314e18d..bccca82863001c 100644 --- a/aptos-move/framework/tests/move_prover_tests.rs +++ b/aptos-move/framework/tests/move_prover_tests.rs @@ -29,7 +29,7 @@ pub fn read_env_var(v: &str) -> String { std::env::var(v).unwrap_or_else(|_| String::new()) } -pub fn run_prover_for_pkg(path_to_pkg: impl Into) { +pub fn run_prover_for_pkg(path_to_pkg: impl Into, shards: usize) { let pkg_path = path_in_crate(path_to_pkg); let mut options = ProverOptions::default_for_test(); let no_tools = read_env_var("BOOGIE_EXE").is_empty() @@ -47,12 +47,14 @@ pub fn run_prover_for_pkg(path_to_pkg: impl Into) { let unconditional_abort_inconsistency_flag = read_env_var(ENV_TEST_UNCONDITIONAL_ABORT_AS_INCONSISTENCY) == "1"; let disallow_timeout_overwrite = read_env_var(ENV_TEST_DISALLOW_TIMEOUT_OVERWRITE) == "1"; + options.shards = Some(shards); options.check_inconsistency = inconsistency_flag; options.unconditional_abort_as_inconsistency = unconditional_abort_inconsistency_flag; options.disallow_global_timeout_to_be_overwritten = disallow_timeout_overwrite; options.vc_timeout = read_env_var(ENV_TEST_VC_TIMEOUT) .parse::() - .unwrap_or(options.vc_timeout); + .ok() + .or(options.vc_timeout); let skip_attribute_checks = false; options .prove( @@ -72,20 +74,20 @@ pub fn run_prover_for_pkg(path_to_pkg: impl Into) { #[test] fn move_framework_prover_tests() { - run_prover_for_pkg("aptos-framework"); + run_prover_for_pkg("aptos-framework", 6); } #[test] fn move_token_prover_tests() { - run_prover_for_pkg("aptos-token"); + run_prover_for_pkg("aptos-token", 2); } #[test] fn move_aptos_stdlib_prover_tests() { - run_prover_for_pkg("aptos-stdlib"); + run_prover_for_pkg("aptos-stdlib", 2); } #[test] fn move_stdlib_prover_tests() { - run_prover_for_pkg("move-stdlib"); + run_prover_for_pkg("move-stdlib", 1); } diff --git a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs index 83dfb499d20247..0b9298358be9cd 100644 --- a/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs +++ b/third_party/move/move-prover/boogie-backend/src/bytecode_translator.rs @@ -59,11 +59,15 @@ use move_stackless_bytecode::{ Operation, PropKind, }, }; -use std::collections::{BTreeMap, BTreeSet}; +use std::{ + collections::{BTreeMap, BTreeSet}, + hash::{DefaultHasher, Hash, Hasher}, +}; pub struct BoogieTranslator<'env> { env: &'env GlobalEnv, options: &'env BoogieOptions, + for_shard: Option, writer: &'env CodeWriter, spec_translator: SpecTranslator<'env>, targets: &'env FunctionTargetsHolder, @@ -85,12 +89,14 @@ impl<'env> BoogieTranslator<'env> { pub fn new( env: &'env GlobalEnv, options: &'env BoogieOptions, + for_shard: Option, targets: &'env FunctionTargetsHolder, writer: &'env CodeWriter, ) -> Self { Self { env, options, + for_shard, targets, writer, spec_translator: SpecTranslator::new(writer, env, options), @@ -113,7 +119,24 @@ impl<'env> BoogieTranslator<'env> { .unwrap_or(default_timeout) } - pub fn is_not_verified_timeout(&self, fun_target: &FunctionTarget) -> bool { + /// Checks whether the given function is a verification target. + fn is_verified(&self, fun_variant: &FunctionVariant, fun_target: &FunctionTarget) -> bool { + if !fun_variant.is_verified() { + return false; + } + if let Some(shard) = self.for_shard { + // Check whether the shard is included. + if self.options.only_shard.is_some() && self.options.only_shard != Some(shard + 1) { + return false; + } + // Check whether it is part of the shard. + let mut hasher = DefaultHasher::new(); + fun_target.func_env.get_full_name_str().hash(&mut hasher); + if (hasher.finish() as usize) % self.options.shards != shard { + return false; + } + } + // Check whether the estimated duration is too large for configured timeout let options = self.options; let estimate_timeout_opt = fun_target .func_env @@ -123,9 +146,9 @@ impl<'env> BoogieTranslator<'env> { .func_env .get_num_pragma(TIMEOUT_PRAGMA) .unwrap_or(options.vc_timeout); - estimate_timeout > timeout + estimate_timeout <= timeout } else { - false + true } } @@ -279,7 +302,7 @@ impl<'env> BoogieTranslator<'env> { continue; } for (variant, ref fun_target) in self.targets.get_targets(fun_env) { - if variant.is_verified() && !self.is_not_verified_timeout(fun_target) { + if self.is_verified(&variant, fun_target) { verified_functions_count += 1; debug!( "will verify primary function `{}`", @@ -363,7 +386,15 @@ impl<'env> BoogieTranslator<'env> { } // Emit any finalization items required by spec translation. self.spec_translator.finalize(); - info!("{} verification conditions", verified_functions_count); + let shard_info = if let Some(shard) = self.for_shard { + format!(" (for shard #{} of {})", shard + 1, self.options.shards) + } else { + "".to_string() + }; + info!( + "{} verification conditions{}", + verified_functions_count, shard_info + ); } } @@ -1106,7 +1137,7 @@ impl<'env> FunctionTranslator<'env> { } // Initial assumptions - if variant.is_verified() && !self.parent.is_not_verified_timeout(fun_target) { + if self.parent.is_verified(variant, fun_target) { self.translate_verify_entry_assumptions(fun_target); } diff --git a/third_party/move/move-prover/boogie-backend/src/options.rs b/third_party/move/move-prover/boogie-backend/src/options.rs index ea88b5c113704f..8efd7bfb3f2385 100644 --- a/third_party/move/move-prover/boogie-backend/src/options.rs +++ b/third_party/move/move-prover/boogie-backend/src/options.rs @@ -140,6 +140,11 @@ pub struct BoogieOptions { pub random_seed: usize, /// The number of cores to use for parallel processing of verification conditions. pub proc_cores: usize, + /// The number of shards to split the verification problem into. + pub shards: usize, + /// If there are shards, specifies to only run the given shard. Shards are numbered + /// starting at 1. + pub only_shard: Option, /// A (soft) timeout for the solver, per verification condition, in seconds. pub vc_timeout: usize, /// Whether allow local timeout overwrites the global one @@ -198,7 +203,9 @@ impl Default for BoogieOptions { vector_using_sequences: false, random_seed: 1, proc_cores: 4, - vc_timeout: 80, + shards: 1, + only_shard: None, + vc_timeout: 40, global_timeout_overwrite: true, keep_artifacts: false, eager_threshold: 100, diff --git a/third_party/move/move-prover/lab/src/benchmark.rs b/third_party/move/move-prover/lab/src/benchmark.rs index edc750c34ef2d2..fb19b90bf4954d 100644 --- a/third_party/move/move-prover/lab/src/benchmark.rs +++ b/third_party/move/move-prover/lab/src/benchmark.rs @@ -274,7 +274,7 @@ impl Runner { )?; // Generate boogie code. - let code_writer = generate_boogie(env, &self.options, &targets)?; + let code_writer = generate_boogie(env, &self.options, None, &targets)?; check_errors( env, &self.options, diff --git a/third_party/move/move-prover/src/lib.rs b/third_party/move/move-prover/src/lib.rs index c3057c7ee12075..f3062ec466f1f6 100644 --- a/third_party/move/move-prover/src/lib.rs +++ b/third_party/move/move-prover/src/lib.rs @@ -7,6 +7,7 @@ use crate::cli::Options; use anyhow::anyhow; use codespan_reporting::term::termcolor::{ColorChoice, StandardStream, WriteColor}; +use itertools::Itertools; #[allow(unused_imports)] use log::{debug, info, warn}; use move_abigen::Abigen; @@ -19,7 +20,7 @@ use move_model::{ parse_addresses_from_options, run_model_builder_with_options, }; use move_prover_boogie_backend::{ - add_prelude, boogie_wrapper::BoogieWrapper, bytecode_translator::BoogieTranslator, + add_prelude, boogie_wrapper::BoogieWrapper, bytecode_translator::BoogieTranslator, options, }; use move_prover_bytecode_pipeline::{ number_operation::GlobalNumberOperationState, pipeline_factory, @@ -28,7 +29,7 @@ use move_stackless_bytecode::function_target_pipeline::FunctionTargetsHolder; use std::{ fs, path::{Path, PathBuf}, - time::Instant, + time::{Duration, Instant}, }; pub mod cli; @@ -146,7 +147,7 @@ pub fn run_move_prover_with_model( pub fn run_move_prover_with_model_v2( env: &mut GlobalEnv, error_writer: &mut W, - options: Options, + mut options: Options, start_time: Instant, ) -> anyhow::Result<()> { let build_duration = start_time.elapsed(); @@ -194,33 +195,56 @@ pub fn run_move_prover_with_model_v2( "exiting with bytecode transformation errors", )?; - // Generate boogie code - let now = Instant::now(); - let code_writer = generate_boogie(env, &options, &targets)?; - let gen_duration = now.elapsed(); - check_errors( - env, - &options, - error_writer, - "exiting with condition generation errors", - )?; - - // Verify boogie code. - let now = Instant::now(); - verify_boogie(env, &options, &targets, code_writer)?; - let verify_duration = now.elapsed(); - + let mut gen_durations = vec![]; + let mut verify_durations = vec![]; + let has_shards = options.backend.shards > 1; + let output_base_file = options.output_path.clone(); + for shard in 0..options.backend.shards { + // If there are shards, modify the output name + if has_shards { + options.output_path = Path::new(&output_base_file) + .with_extension(format!("shard_{}.bpl", shard + 1)) + .to_string_lossy() + .to_string(); + } + // Generate boogie code. + let now = Instant::now(); + let code_writer = generate_boogie( + env, + &options, + if has_shards { Some(shard) } else { None }, + &targets, + )?; + gen_durations.push(now.elapsed()); + check_errors( + env, + &options, + error_writer, + "exiting with condition generation errors", + )?; + + // Verify boogie code. + let now = Instant::now(); + verify_boogie(env, &options, &targets, code_writer)?; + verify_durations.push(now.elapsed()); + } + options.output_path = output_base_file; // Report durations. + let dur_list = |ds: &[Duration]| { + ds.iter() + .map(|d| format!("{:.2}", d.as_secs_f64())) + .join("/") + }; info!( - "{:.3}s build, {:.3}s trafo, {:.3}s gen, {:.3}s verify, total {:.3}s", + "{:.2}s build, {:.2}s trafo, {}s gen, {}s verify, total {:.2}s", build_duration.as_secs_f64(), trafo_duration.as_secs_f64(), - gen_duration.as_secs_f64(), - verify_duration.as_secs_f64(), + dur_list(&gen_durations), + dur_list(&verify_durations), build_duration.as_secs_f64() + trafo_duration.as_secs_f64() - + gen_duration.as_secs_f64() - + verify_duration.as_secs_f64() + + gen_durations.iter().sum::().as_secs_f64() + + verify_durations.iter().sum::().as_secs_f64() ); check_errors( env, @@ -247,11 +271,12 @@ pub fn check_errors( pub fn generate_boogie( env: &GlobalEnv, options: &Options, + shard: Option, targets: &FunctionTargetsHolder, ) -> anyhow::Result { let writer = CodeWriter::new(env.internal_loc()); add_prelude(env, &options.backend, &writer)?; - let mut translator = BoogieTranslator::new(env, &options.backend, targets, &writer); + let mut translator = BoogieTranslator::new(env, &options.backend, shard, targets, &writer); translator.translate(); Ok(writer) }