-
Notifications
You must be signed in to change notification settings - Fork 3.7k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[move-prover] Sharding feature + re-animate Prover.toml #15775
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,2 @@ | ||
[backend] | ||
shards = 5 |
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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<usize>, | ||
|
||
/// A seed for the prover. | ||
#[clap(long, default_value_t = 0)] | ||
pub random_seed: usize, | ||
#[clap(long)] | ||
pub random_seed: Option<usize>, | ||
|
||
/// 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<usize>, | ||
|
||
/// 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<usize>, | ||
|
||
/// If there are multiple shards, the shard to which verification shall be narrowed. | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. From looking at other related code, it looks like the shards are numbered |
||
#[clap(long)] | ||
pub only_shard: Option<usize>, | ||
|
||
/// 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<usize>, | ||
|
||
/// 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<Options> { | ||
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, | ||
wrwg marked this conversation as resolved.
Show resolved
Hide resolved
|
||
..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 { | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -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<usize>, | ||
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<usize>, | ||
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) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. nit: could use |
||
return false; | ||
} | ||
// Check whether it is part of the shard. | ||
let mut hasher = DefaultHasher::new(); | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I think this hasher is non-deterministic? Thus, if you decide to shard one by one, a target might fall into different shards each time? Thus, we may want to use a deterministic hasher. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. @wrwg Checking in to see if you missed this before merging. |
||
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); | ||
} | ||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This PR does not touch anything in the execution stack, so this most be from previous PRs. (Perhaps permissioned signers? @igor-aptos
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Seems like signer has indeed added noise - here it the recalibration PR - #15778
generated by doing:
note - this particular line didn't regress as much as you saw from the first run - you can see your second run much closer to the original value. But I assume all the changes create way too much noise anyways.