[move-prover][cli] Add benchmark functionality (#15636)

This adds a new option `aptos move prove --benchmark` which lets verification run in the benchmark framework of the `move-prover/lab` tool. This tool verifies function by function and detects timeouts as well as measure verification time.

The result of the benchmark will be stored in `<move-package>/prover_benchmark.fun_data`. A graphic representation will be stored as well in `prover_benchmark.svg`.

The PR fixes also some other things on the way which came apparent when working on it, namely trying to identify the reasons for #15605:

- Adds new debug print for which verification targets are generated. This is reachable via `move prove -v debug`
- Reduces unnecessary verification of symmetric type instantiations `f<#1, #2>` and `f<#2, #1>`
- Adds an option `--skip-instance-check` to completely turn off verification of type instantiations.
- Removed legacy verification_analysis_v2 and global_invariant_instrumentation_v2. These are dead code since long  and confusing when trying to understand what functions are verified

Cargo.toml

@@ -875,6 +875,7 @@ move-prover = { path = "third_party/move/move-prover" }
 move-prover-boogie-backend = { path = "third_party/move/move-prover/boogie-backend" }
 move-prover-bytecode-pipeline = { path = "third_party/move/move-prover/bytecode-pipeline" }
 move-prover-test-utils = { path = "third_party/move/move-prover/test-utils" }
+move-prover-lab = { path = "third_party/move/move-prover/lab" }
 aptos-move-stdlib = { path = "aptos-move/framework/move-stdlib" }
 aptos-table-natives = { path = "aptos-move/framework/table-natives" }
 move-resource-viewer = { path = "third_party/move/tools/move-resource-viewer" }

aptos-move/framework/Cargo.toml

@@ -60,6 +60,7 @@ move-package = { workspace = true }
 move-prover = { workspace = true }
 move-prover-boogie-backend = { workspace = true }
 move-prover-bytecode-pipeline = { workspace = true }
+move-prover-lab = { workspace = true }
 move-stackless-bytecode = { workspace = true }
 move-vm-runtime = { workspace = true }
 move-vm-types = { workspace = true }
@@ -78,6 +79,7 @@ smallvec = { workspace = true }
 tempfile = { workspace = true }
 thiserror = { workspace = true }
 tiny-keccak = { workspace = true }
+toml = { workspace = true }
 
 [dev-dependencies]
 aptos-aggregator = { workspace = true, features = ["testing"] }

aptos-move/framework/src/prover.rs

@@ -2,15 +2,21 @@
 // SPDX-License-Identifier: Apache-2.0
 
 use crate::build_model;
+use anyhow::bail;
 use codespan_reporting::{
     diagnostic::Severity,
     term::termcolor::{ColorChoice, StandardStream},
 };
-use log::LevelFilter;
+use log::{info, LevelFilter};
 use move_core_types::account_address::AccountAddress;
-use move_model::metadata::{CompilerVersion, LanguageVersion};
+use move_model::{
+    metadata::{CompilerVersion, LanguageVersion},
+    model::{GlobalEnv, VerificationScope},
+};
+use move_prover::cli::Options;
 use std::{
     collections::{BTreeMap, BTreeSet},
+    fs,
     path::Path,
     time::Instant,
 };
@@ -27,6 +33,12 @@ pub struct ProverOptions {
     #[clap(long, short)]
     pub filter: Option<String>,
 
+    /// Scopes verification to the specified function. This can either be a name of the
+    /// form "mod::func" or simply "func", in the later case every matching function is
+    /// taken.
+    #[clap(long, short)]
+    pub only: Option<String>,
+
     /// Whether to display additional information in error reports. This may help
     /// debugging but also can make verification slower.
     #[clap(long, short)]
@@ -84,6 +96,24 @@ pub struct ProverOptions {
     #[clap(long)]
     pub dump: bool,
 
+    /// Whether to benchmark verification. If selected, each verification target in the
+    /// current package will be verified independently with timing recorded. This attempts
+    /// to detect timeouts. A benchmark report will be written to `prover_benchmark.fun_data` in the
+    /// package directory. The command also writes a `prover_benchmark.svg` graphic, which
+    /// is build from the data in the file above, comparing with any other `*.fun_data` files
+    /// in the package directory. Thus, you can rename the data file to something like
+    /// `prover_benchmark_v1.fun_data` and in the next run, compare benchmarks in the `.svg`
+    /// file from multiple runs.
+    #[clap(long = "benchmark")]
+    pub benchmark: bool,
+
+    /// Whether to skip verification of type instantiations of functions. This may miss
+    /// some verification conditions if different type instantiations can create
+    /// different behavior via type reflection or storage access, but can speed up
+    /// verification.
+    #[clap(long = "skip-instance-check")]
+    pub skip_instance_check: bool,
+
     #[clap(skip)]
     pub for_test: bool,
 }
@@ -93,6 +123,7 @@ impl Default for ProverOptions {
         Self {
             verbosity: None,
             filter: None,
+            only: None,
             trace: false,
             cvc5: false,
             stratification_depth: 6,
@@ -106,7 +137,9 @@ impl Default for ProverOptions {
             loop_unroll: None,
             stable_test_output: false,
             dump: false,
+            benchmark: false,
             for_test: false,
+            skip_instance_check: false,
         }
     }
 }
@@ -127,6 +160,7 @@ impl ProverOptions {
     ) -> anyhow::Result<()> {
         let now = Instant::now();
         let for_test = self.for_test;
+        let benchmark = self.benchmark;
         let mut model = build_model(
             dev_mode,
             package_path,
@@ -140,6 +174,15 @@ impl ProverOptions {
             experiments.to_vec(),
         )?;
         let mut options = self.convert_options();
+        options.language_version = language_version;
+        options.model_builder.language_version = language_version.unwrap_or_default();
+        if compiler_version.unwrap_or_default() >= CompilerVersion::V2_0
+            || language_version
+                .unwrap_or_default()
+                .is_at_least(LanguageVersion::V2_0)
+        {
+            options.compiler_v2 = true;
+        }
         // Need to ensure a distinct output.bpl file for concurrent execution. In non-test
         // mode, we actually want to use the static output.bpl for debugging purposes
         let _temp_holder = if for_test {
@@ -163,11 +206,21 @@ impl ProverOptions {
                 template_bytes: include_bytes!("aptos-natives.bpl").to_vec(),
                 module_instance_names: move_prover_boogie_backend::options::custom_native_options(),
             });
-        let mut writer = StandardStream::stderr(ColorChoice::Auto);
-        if compiler_version.unwrap_or_default() == CompilerVersion::V1 {
-            move_prover::run_move_prover_with_model(&mut model, &mut writer, options, Some(now))?;
+        if benchmark {
+            // Special mode of benchmarking
+            run_prover_benchmark(package_path, &mut model, options)?;
         } else {
-            move_prover::run_move_prover_with_model_v2(&mut model, &mut writer, options, now)?;
+            let mut writer = StandardStream::stderr(ColorChoice::Auto);
+            if compiler_version.unwrap_or_default() == CompilerVersion::V1 {
+                move_prover::run_move_prover_with_model(
+                    &mut model,
+                    &mut writer,
+                    options,
+                    Some(now),
+                )?;
+            } else {
+                move_prover::run_move_prover_with_model_v2(&mut model, &mut writer, options, now)?;
+            }
         }
         Ok(())
     }
@@ -184,6 +237,11 @@ impl ProverOptions {
             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
+                },
                 stable_test_output: self.stable_test_output,
                 auto_trace_level: if self.trace {
                     move_prover_bytecode_pipeline::options::AutoTraceLevel::VerifiedFunction
@@ -215,6 +273,7 @@ impl ProverOptions {
                 },
                 custom_natives: None,
                 loop_unroll: self.loop_unroll,
+                skip_instance_check: self.skip_instance_check,
                 ..Default::default()
             },
             ..Default::default()
@@ -234,3 +293,106 @@ impl ProverOptions {
         }
     }
 }
+
+fn run_prover_benchmark(
+    package_path: &Path,
+    env: &mut GlobalEnv,
+    mut options: Options,
+) -> anyhow::Result<()> {
+    info!("starting prover benchmark");
+    // Determine sources and dependencies from the env
+    let mut sources = BTreeSet::new();
+    let mut deps: Vec<String> = vec![];
+    for module in env.get_modules() {
+        let file_name = module.get_source_path().to_string_lossy().to_string();
+        if module.is_primary_target() {
+            sources.insert(module.get_source_path().to_string_lossy().to_string());
+        } else if let Some(p) = Path::new(&file_name)
+            .parent()
+            .and_then(|p| p.canonicalize().ok())
+        {
+            // The prover doesn't like to have `p` and `p/s` as dep paths, filter those out
+            let p = p.to_string_lossy().to_string();
+            let mut done = false;
+            for d in &mut deps {
+                if p.starts_with(&*d) {
+                    // p is subsumed
+                    done = true;
+                    break;
+                } else if d.starts_with(&p) {
+                    // p is more general or equal to d, swap it out
+                    *d = p.to_string();
+                    done = true;
+                    break;
+                }
+            }
+            if !done {
+                deps.push(p)
+            }
+        } else {
+            bail!("invalid file path `{}`", file_name)
+        }
+    }
+
+    // Enrich the prover options by the aliases in the env
+    for (alias, address) in env.get_address_alias_map() {
+        options.move_named_address_values.push(format!(
+            "{}={}",
+            alias.display(env.symbol_pool()),
+            address.to_hex_literal()
+        ))
+    }
+
+    // Create or override a prover_benchmark.toml in the package dir, reflection `options`
+    let config_file = package_path.join("prover_benchmark.toml");
+    let toml = toml::to_string(&options)?;
+    std::fs::write(&config_file, toml)?;
+
+    // Args for the benchmark API
+    let mut args = vec![
+        // Command name
+        "bench".to_string(),
+        // Benchmark by function not module
+        "--func".to_string(),
+        // Use as the config the file we derived from `options`
+        "--config".to_string(),
+        config_file.to_string_lossy().to_string(),
+    ];
+
+    // Add deps and sources to args and run the tool
+    for dep in deps {
+        args.push("-d".to_string());
+        args.push(dep)
+    }
+    args.extend(sources);
+    move_prover_lab::benchmark::benchmark(&args);
+
+    // The benchmark stores the result in `<config_file>.fun_data`, now plot it.
+    // If there are any other `*.fun_data` files, add them to the plot.
+    let mut args = vec![
+        "plot".to_string(),
+        format!(
+            "--out={}",
+            config_file
+                .as_path()
+                .with_extension("svg")
+                .to_string_lossy()
+        ),
+        "--sort".to_string(),
+    ];
+    let main_data_file = config_file
+        .as_path()
+        .with_extension("fun_data")
+        .to_string_lossy()
+        .to_string();
+    args.push(main_data_file.clone());
+    let paths = fs::read_dir(package_path)?;
+    for p in paths.flatten() {
+        let p = p.path().as_path().to_string_lossy().to_string();
+        // Only use this if its is not the main data file we already added
+        if p.ends_with(".fun_data") && !p.ends_with("/prover_benchmark.fun_data") {
+            args.push(p)
+        }
+    }
+    move_prover_lab::plot::plot_svg(&args)
+}

crates/aptos/CHANGELOG.md

@@ -3,6 +3,8 @@
 All notable changes to the Aptos CLI will be captured in this file. This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html) and the format set out by [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 # Unreleased
+- Add flag `--benchmark` to `aptos move prove`, which allows to benchmark verification times of individual functions in a package.
+- Add flag `--only <name>` to `aptos move prove`, which allows to scope verification to a function.
 
 ## [5.1.0] - 2024/12/13
 - More optimizations are now default for compiler v2.

third_party/move/move-model/src/model.rs

@@ -700,6 +700,11 @@ impl GlobalEnv {
         self.address_alias_map = map
     }
 
+    /// Gets the global address alias map
+    pub fn get_address_alias_map(&self) -> &BTreeMap<Symbol, AccountAddress> {
+        &self.address_alias_map
+    }
+
     /// Indicates that all modules in the environment should be treated as
     /// target modules, i.e. `module.is_target()` returns true. This can be
     /// used to temporarily override the default which distinguishes