From 3a8b35523855711df501aa774732d538ac8d7533 Mon Sep 17 00:00:00 2001 From: Wolfgang Grieskamp Date: Tue, 17 Dec 2024 19:48:35 -0800 Subject: [PATCH] [move-prover][cli] Add benchmark functionality 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 `/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.lock | 40 +- Cargo.toml | 1 + aptos-move/framework/Cargo.toml | 2 + aptos-move/framework/src/prover.rs | 162 +++- crates/aptos/CHANGELOG.md | 1 + third_party/move/move-model/src/model.rs | 5 + .../boogie-backend/src/bytecode_translator.rs | 220 +++-- .../move-prover/boogie-backend/src/options.rs | 6 + .../move-prover/bytecode-pipeline/Cargo.toml | 1 - .../global_invariant_instrumentation_v2.rs | 794 ----------------- .../move-prover/bytecode-pipeline/src/lib.rs | 2 - .../src/verification_analysis_v2.rs | 800 ------------------ third_party/move/move-prover/lab/Cargo.toml | 6 +- .../move/move-prover/lab/src/benchmark.rs | 55 +- third_party/move/move-prover/lab/src/main.rs | 2 +- third_party/move/move-prover/src/lib.rs | 24 +- 16 files changed, 344 insertions(+), 1777 deletions(-) delete mode 100644 third_party/move/move-prover/bytecode-pipeline/src/global_invariant_instrumentation_v2.rs delete mode 100644 third_party/move/move-prover/bytecode-pipeline/src/verification_analysis_v2.rs diff --git a/Cargo.lock b/Cargo.lock index 15f52e4b304bb6..1d82d5ce72d448 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1923,6 +1923,7 @@ dependencies = [ "move-prover", "move-prover-boogie-backend", "move-prover-bytecode-pipeline", + "move-prover-lab", "move-stackless-bytecode", "move-unit-test", "move-vm-runtime", @@ -1942,6 +1943,7 @@ dependencies = [ "tempfile", "thiserror", "tiny-keccak", + "toml 0.7.8", ] [[package]] @@ -11649,7 +11651,6 @@ dependencies = [ "codespan-reporting", "datatest-stable", "itertools 0.13.0", - "log", "move-binary-format", "move-core-types", "move-model", @@ -11661,6 +11662,23 @@ dependencies = [ "walkdir", ] +[[package]] +name = "move-prover-lab" +version = "0.1.0" +dependencies = [ + "anyhow", + "chrono", + "clap 4.5.21", + "codespan-reporting", + "itertools 0.13.0", + "move-model", + "move-prover", + "move-prover-boogie-backend", + "move-prover-bytecode-pipeline", + "plotters", + "z3tracer", +] + [[package]] name = "move-prover-test-utils" version = "0.1.0" @@ -13981,26 +13999,6 @@ dependencies = [ "protobuf-codegen", ] -[[package]] -name = "prover-lab" -version = "0.1.0" -dependencies = [ - "anyhow", - "chrono", - "clap 4.5.21", - "codespan-reporting", - "itertools 0.13.0", - "log", - "move-compiler", - "move-compiler-v2", - "move-model", - "move-prover", - "move-prover-boogie-backend", - "move-prover-bytecode-pipeline", - "plotters", - "z3tracer", -] - [[package]] name = "psl-types" version = "2.0.11" diff --git a/Cargo.toml b/Cargo.toml index 85473f6bb3de50..fe006c548de841 100644 --- a/Cargo.toml +++ b/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" } diff --git a/aptos-move/framework/Cargo.toml b/aptos-move/framework/Cargo.toml index fb7d4cb4d44957..35946a9a6bc765 100644 --- a/aptos-move/framework/Cargo.toml +++ b/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"] } diff --git a/aptos-move/framework/src/prover.rs b/aptos-move/framework/src/prover.rs index fbe8a7fed97a1c..c78ad40a475b1c 100644 --- a/aptos-move/framework/src/prover.rs +++ b/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, +}; +use move_prover::cli::Options; use std::{ collections::{BTreeMap, BTreeSet}, + fs, path::Path, time::Instant, }; @@ -84,6 +90,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, } @@ -106,7 +130,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 +153,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 +167,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 +199,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(()) } @@ -215,6 +261,7 @@ impl ProverOptions { }, custom_natives: None, loop_unroll: self.loop_unroll, + skip_instance_check: self.skip_instance_check, ..Default::default() }, ..Default::default() @@ -234,3 +281,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 = 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 `.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) +} diff --git a/crates/aptos/CHANGELOG.md b/crates/aptos/CHANGELOG.md index 591c7bff8abb63..737fae7cd1e0a2 100644 --- a/crates/aptos/CHANGELOG.md +++ b/crates/aptos/CHANGELOG.md @@ -3,6 +3,7 @@ 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 ## [5.1.0] - 2024/12/13 - More optimizations are now default for compiler v2. diff --git a/third_party/move/move-model/src/model.rs b/third_party/move/move-model/src/model.rs index 63e47494019656..c4d08a9f63b744 100644 --- a/third_party/move/move-model/src/model.rs +++ b/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 { + &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 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 350e912f8f2841..5ebb919eff17f3 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 @@ -31,7 +31,10 @@ use move_model::{ ast::{Attribute, TempIndex, TraceKind}, code_writer::CodeWriter, emit, emitln, - model::{FieldEnv, FieldId, GlobalEnv, Loc, NodeId, QualifiedInstId, StructEnv, StructId}, + model::{ + FieldEnv, FieldId, FunctionEnv, GlobalEnv, Loc, NodeId, QualifiedInstId, StructEnv, + StructId, + }, pragmas::{ ADDITION_OVERFLOW_UNCHECKED_PRAGMA, SEED_PRAGMA, TIMEOUT_PRAGMA, VERIFY_DURATION_ESTIMATE_PRAGMA, @@ -278,6 +281,10 @@ impl<'env> BoogieTranslator<'env> { for (variant, ref fun_target) in self.targets.get_targets(fun_env) { if variant.is_verified() && !self.is_not_verified_timeout(fun_target) { verified_functions_count += 1; + debug!( + "will verify primary function `{}`", + env.display(&module_env.get_id().qualified(fun_target.get_id())) + ); // Always produce a verified functions with an empty instantiation such that // there is at least one top-level entry points for a VC. FunctionTranslator { @@ -289,28 +296,45 @@ impl<'env> BoogieTranslator<'env> { // There maybe more verification targets that needs to be produced as we // defer the instantiation of verified functions to this stage - for type_inst in mono_info - .funs - .get(&(fun_target.func_env.get_qualified_id(), variant)) - .unwrap_or(empty) - { - // Skip the none instantiation (i.e., each type parameter is - // instantiated to itself as a concrete type). This has the same - // effect as `type_inst: &[]` and is already captured above. - let is_none_inst = type_inst.iter().enumerate().all( - |(i, t)| matches!(t, Type::TypeParameter(idx) if *idx == i as u16), - ); - if is_none_inst { - continue; - } + if !self.options.skip_instance_check { + for type_inst in mono_info + .funs + .get(&(fun_target.func_env.get_qualified_id(), variant)) + .unwrap_or(empty) + { + // Skip redundant instantiations. Those are any permutation of + // type parameters. We can simple test this by the same number + // of disjoint type parameters equals the count of type parameters. + // Verifying a disjoint set of type parameters is the same + // as the `&[]` verification already done above. + let type_params_in_inst = type_inst + .iter() + .filter(|t| matches!(t, Type::TypeParameter(_))) + .cloned() + .collect::>(); + if type_params_in_inst.len() == type_inst.len() { + continue; + } - verified_functions_count += 1; - FunctionTranslator { - parent: self, - fun_target, - type_inst, + verified_functions_count += 1; + let tctx = &fun_env.get_type_display_ctx(); + debug!( + "will verify function instantiation `{}`<{}>", + env.display( + &module_env.get_id().qualified(fun_target.get_id()) + ), + type_inst + .iter() + .map(|t| t.display(tctx).to_string()) + .join(", ") + ); + FunctionTranslator { + parent: self, + fun_target, + type_inst, + } + .translate(); } - .translate(); } } else { // This variant is inlined, so translate for all type instantiations. @@ -1464,80 +1488,13 @@ impl<'env> FunctionTranslator<'env> { ) .join(","); - // special casing for type reflection - let mut processed = false; - - // TODO(mengxu): change it to a better address name instead of extlib - if env.get_extlib_address() == *module_env.get_name().addr() { - let qualified_name = format!( - "{}::{}", - module_env.get_name().name().display(env.symbol_pool()), - callee_env.get_name().display(env.symbol_pool()), - ); - if qualified_name == TYPE_NAME_MOVE { - assert_eq!(inst.len(), 1); - if dest_str.is_empty() { - emitln!( - writer, - "{}", - boogie_reflection_type_name(env, &inst[0], false) - ); - } else { - emitln!( - writer, - "{} := {};", - dest_str, - boogie_reflection_type_name(env, &inst[0], false) - ); - } - processed = true; - } else if qualified_name == TYPE_INFO_MOVE { - assert_eq!(inst.len(), 1); - let (flag, info) = boogie_reflection_type_info(env, &inst[0]); - emitln!(writer, "if (!{}) {{", flag); - writer.with_indent(|| emitln!(writer, "call $ExecFailureAbort();")); - emitln!(writer, "}"); - if !dest_str.is_empty() { - emitln!(writer, "else {"); - writer.with_indent(|| { - emitln!(writer, "{} := {};", dest_str, info) - }); - emitln!(writer, "}"); - } - processed = true; - } - } - - if env.get_stdlib_address() == *module_env.get_name().addr() { - let qualified_name = format!( - "{}::{}", - module_env.get_name().name().display(env.symbol_pool()), - callee_env.get_name().display(env.symbol_pool()), - ); - if qualified_name == TYPE_NAME_GET_MOVE { - assert_eq!(inst.len(), 1); - if dest_str.is_empty() { - emitln!( - writer, - "{}", - boogie_reflection_type_name(env, &inst[0], true) - ); - } else { - emitln!( - writer, - "{} := {};", - dest_str, - boogie_reflection_type_name(env, &inst[0], true) - ); - } - processed = true; - } - } - - // regular path - if !processed { + if self.try_reflection_call(writer, env, inst, &callee_env, &dest_str) { + // Special case of reflection call, code is generated + } else { + // regular path let targeted = self.fun_target.module_env().is_target(); - // If the callee has been generated from a native interface, return an error + // If the callee has been generated from a native interface, return + // an error if callee_env.is_native() && targeted { for attr in callee_env.get_attributes() { if let Attribute::Apply(_, name, _) = attr { @@ -2601,6 +2558,81 @@ impl<'env> FunctionTranslator<'env> { emitln!(writer); } + fn try_reflection_call( + &self, + writer: &CodeWriter, + env: &GlobalEnv, + inst: &[Type], + callee_env: &FunctionEnv, + dest_str: &String, + ) -> bool { + let module_env = &callee_env.module_env; + let mk_qualified_name = || { + format!( + "{}::{}", + module_env.get_name().name().display(env.symbol_pool()), + callee_env.get_name().display(env.symbol_pool()), + ) + }; + if env.get_extlib_address() == *module_env.get_name().addr() { + let qualified_name = mk_qualified_name(); + if qualified_name == TYPE_NAME_MOVE { + assert_eq!(inst.len(), 1); + if dest_str.is_empty() { + emitln!( + writer, + "{}", + boogie_reflection_type_name(env, &inst[0], false) + ); + } else { + emitln!( + writer, + "{} := {};", + dest_str, + boogie_reflection_type_name(env, &inst[0], false) + ); + } + return true; + } else if qualified_name == TYPE_INFO_MOVE { + assert_eq!(inst.len(), 1); + let (flag, info) = boogie_reflection_type_info(env, &inst[0]); + emitln!(writer, "if (!{}) {{", flag); + writer.with_indent(|| emitln!(writer, "call $ExecFailureAbort();")); + emitln!(writer, "}"); + if !dest_str.is_empty() { + emitln!(writer, "else {"); + writer.with_indent(|| emitln!(writer, "{} := {};", dest_str, info)); + emitln!(writer, "}"); + } + return true; + } + } + + if env.get_stdlib_address() == *module_env.get_name().addr() { + let qualified_name = mk_qualified_name(); + if qualified_name == TYPE_NAME_GET_MOVE { + assert_eq!(inst.len(), 1); + if dest_str.is_empty() { + emitln!( + writer, + "{}", + boogie_reflection_type_name(env, &inst[0], true) + ); + } else { + emitln!( + writer, + "{} := {};", + dest_str, + boogie_reflection_type_name(env, &inst[0], true) + ); + } + return true; + } + } + + false + } + fn translate_write_back(&self, dest: &BorrowNode, edge: &BorrowEdge, src: TempIndex) { use BorrowNode::*; let writer = self.parent.writer; 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 989095b5659f30..ea88b5c113704f 100644 --- a/third_party/move/move-prover/boogie-backend/src/options.rs +++ b/third_party/move/move-prover/boogie-backend/src/options.rs @@ -159,6 +159,11 @@ pub struct BoogieOptions { /// A hard timeout for boogie execution; if the process does not terminate within /// this time frame, it will be killed. Zero for no timeout. pub hard_timeout_secs: u64, + /// 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. + pub skip_instance_check: bool, /// What vector theory to use. pub vector_theory: VectorTheory, /// Whether to generate a z3 trace file and where to put it. @@ -207,6 +212,7 @@ impl Default for BoogieOptions { custom_natives: None, loop_unroll: None, borrow_aggregates: vec![], + skip_instance_check: false, } } } diff --git a/third_party/move/move-prover/bytecode-pipeline/Cargo.toml b/third_party/move/move-prover/bytecode-pipeline/Cargo.toml index 366973ed14db22..2d41dd22fa8a43 100644 --- a/third_party/move/move-prover/bytecode-pipeline/Cargo.toml +++ b/third_party/move/move-prover/bytecode-pipeline/Cargo.toml @@ -11,7 +11,6 @@ abstract-domain-derive = { path = "../../move-model/bytecode/abstract_domain_der anyhow = { workspace = true } codespan-reporting = { workspace = true } itertools = { workspace = true } -log = { workspace = true, features = ["serde"] } move-binary-format = { workspace = true } move-core-types = { workspace = true } move-model = { workspace = true } diff --git a/third_party/move/move-prover/bytecode-pipeline/src/global_invariant_instrumentation_v2.rs b/third_party/move/move-prover/bytecode-pipeline/src/global_invariant_instrumentation_v2.rs deleted file mode 100644 index a71b9be51b73ae..00000000000000 --- a/third_party/move/move-prover/bytecode-pipeline/src/global_invariant_instrumentation_v2.rs +++ /dev/null @@ -1,794 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// Copyright (c) The Move Contributors -// SPDX-License-Identifier: Apache-2.0 - -// Transformation which injects global invariants into the bytecode. - -use crate::{options::ProverOptions, verification_analysis_v2::InvariantAnalysisData}; -use itertools::Itertools; -#[allow(unused_imports)] -use log::{debug, info, log, warn}; -#[cfg(invariant_trace)] -use move_model::ty::TypeDisplayContext; -use move_model::{ - ast::{ConditionKind, Exp, GlobalInvariant}, - exp_generator::ExpGenerator, - model::{FunId, FunctionEnv, GlobalEnv, GlobalId, Loc, QualifiedId, QualifiedInstId, StructId}, - pragmas::CONDITION_ISOLATED_PROP, - spec_translator::{SpecTranslator, TranslatedSpec}, - ty::{NoUnificationContext, Type, TypeUnificationAdapter, Variance}, -}; -use move_stackless_bytecode::{ - function_data_builder::FunctionDataBuilder, - function_target::{FunctionData, FunctionTarget}, - function_target_pipeline::{ - FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant, VerificationFlavor, - }, - stackless_bytecode::{BorrowNode, Bytecode, Operation, PropKind}, - usage_analysis, -}; -use std::collections::{BTreeMap, BTreeSet}; - -const GLOBAL_INVARIANT_FAILS_MESSAGE: &str = "global memory invariant does not hold"; - -pub struct GlobalInvariantInstrumentationProcessorV2 {} - -impl GlobalInvariantInstrumentationProcessorV2 { - pub fn new() -> Box { - Box::new(Self {}) - } -} - -impl FunctionTargetProcessor for GlobalInvariantInstrumentationProcessorV2 { - fn process( - &self, - targets: &mut FunctionTargetsHolder, - fun_env: &FunctionEnv, - data: FunctionData, - _scc_opt: Option<&[FunctionEnv]>, - ) -> FunctionData { - if fun_env.is_native() || fun_env.is_intrinsic() { - // Nothing to do. - return data; - } - if !data.variant.is_verified() { - // Only need to instrument if this is a verification variant - return data; - } - - // Analyze invariants - let target = FunctionTarget::new(fun_env, &data); - let Analyzer { plain, func_insts } = Analyzer::analyze(&target); - - // Collect information - let env = target.global_env(); - - // Create variants for possible function instantiations - let mut func_variants = vec![]; - for (i, (ty_args, mut global_ids)) in func_insts.into_iter().enumerate() { - let variant_data = data.fork_with_instantiation( - env, - &ty_args, - FunctionVariant::Verification(VerificationFlavor::Instantiated(i)), - ); - global_ids.extend(plain.clone().into_iter()); - func_variants.push((variant_data, global_ids)); - } - - // Instrument the main variant - let main = Instrumenter::run(fun_env, data, plain); - - // Instrument the variants representing different instantiations - for (variant_data, variant_global_invariants) in func_variants { - let variant = Instrumenter::run(fun_env, variant_data, variant_global_invariants); - targets.insert_target_data( - &fun_env.get_qualified_id(), - variant.variant.clone(), - variant, - ); - } - - // Return the main variant - main - } - - fn name(&self) -> String { - "global_invariant_instrumenter_v2".to_string() - } -} - -struct Analyzer { - plain: BTreeSet, - func_insts: BTreeMap, BTreeSet>, -} - -impl Analyzer { - pub fn analyze(target: &FunctionTarget) -> Self { - let mut analyzer = Self { - plain: BTreeSet::new(), - func_insts: BTreeMap::new(), - }; - analyzer.collect_related_global_invariants(target); - analyzer - } - - /// Collect global invariants that are read and written by this function - fn collect_related_global_invariants(&mut self, target: &FunctionTarget) { - let env = target.global_env(); - - // get memory (list of structs) read or written by the function target, - // then find all invariants in loaded modules that refer to that memory. - let mut invariants_for_used_memory = BTreeSet::new(); - for mem in usage_analysis::get_memory_usage(target).accessed.all.iter() { - invariants_for_used_memory.extend(env.get_global_invariants_for_memory(mem)); - } - - // filter non-applicable global invariants - for invariant_id in invariants_for_used_memory { - self.check_global_invariant_applicability( - target, - env.get_global_invariant(invariant_id).unwrap(), - ); - } - } - - fn check_global_invariant_applicability( - &mut self, - target: &FunctionTarget, - invariant: &GlobalInvariant, - ) { - // marks whether the invariant will be checked in all instantiations of this function - let mut is_generic = false; - - // collect instantiations of this function that are needed to check this global invariant - let mut func_insts = BTreeSet::new(); - - let fun_mems = &usage_analysis::get_memory_usage(target).accessed.all; - let fun_arity = target.get_type_parameter_count(); - for inv_mem in &invariant.mem_usage { - for fun_mem in fun_mems.iter() { - if inv_mem.module_id != fun_mem.module_id || inv_mem.id != fun_mem.id { - continue; - } - let adapter = - TypeUnificationAdapter::new_vec(&fun_mem.inst, &inv_mem.inst, true, true); - let rel = adapter.unify( - &mut NoUnificationContext, - Variance::SpecVariance, - /* shallow_subst */ false, - ); - match rel { - None => continue, - Some((subs_fun, _)) => { - if subs_fun.is_empty() { - is_generic = true; - } else { - func_insts.insert(Type::type_param_map_to_inst(fun_arity, subs_fun)); - } - }, - } - } - } - - // save the instantiation required to evaluate this invariant - for inst in func_insts { - self.func_insts - .entry(inst) - .or_default() - .insert(invariant.id); - } - if is_generic { - self.plain.insert(invariant.id); - } - } -} - -struct Instrumenter<'a> { - options: &'a ProverOptions, - builder: FunctionDataBuilder<'a>, - _function_inst: Vec, - used_memory: BTreeSet>, - // Invariants that unify with the state used in a function instantiation - related_invariants: BTreeSet, - saved_from_before_instr_or_call: Option<(TranslatedSpec, BTreeSet)>, -} - -impl<'a> Instrumenter<'a> { - fn run( - fun_env: &FunctionEnv<'a>, - data: FunctionData, - related_invariants: BTreeSet, - ) -> FunctionData { - if !data.variant.is_verified() { - // Run the instrumentation only if this is a verification variant. - return data; - } - - let global_env = fun_env.module_env.env; - let options = ProverOptions::get(global_env); - let function_inst = data.get_type_instantiation(fun_env); - let builder = FunctionDataBuilder::new(fun_env, data); - let used_memory: BTreeSet<_> = usage_analysis::get_memory_usage(&builder.get_target()) - .accessed - .get_all_inst(&function_inst); - - #[cfg(invariant_trace)] - { - let tctx = TypeDisplayContext::WithEnv { - env: global_env, - type_param_names: None, - }; - println!( - "{}<{}>: {}", - builder.data.variant, - function_inst - .iter() - .map(|t| t.display(&tctx).to_string()) - .join(","), - used_memory - .iter() - .map(|m| global_env.display(m).to_string()) - .join(",") - ); - } - - let mut instrumenter = Instrumenter { - options: options.as_ref(), - builder, - _function_inst: function_inst, - used_memory, - related_invariants, - saved_from_before_instr_or_call: None, - }; - instrumenter.instrument(global_env); - instrumenter.builder.data - } - - fn instrument(&mut self, global_env: &GlobalEnv) { - // Collect information - let fun_env = self.builder.fun_env; - let fun_id = fun_env.get_qualified_id(); - - let inv_ana_data = global_env.get_extension::().unwrap(); - let disabled_inv_fun_set = &inv_ana_data.disabled_inv_fun_set; - let non_inv_fun_set = &inv_ana_data.non_inv_fun_set; - let target_invariants = &inv_ana_data.target_invariants; - let disabled_invs_for_fun = &inv_ana_data.disabled_invs_for_fun; - - // Extract and clear current code - let old_code = std::mem::take(&mut self.builder.data.code); - - // Emit entrypoint assumptions - let mut entrypoint_invariants = self.filter_entrypoint_invariants(&self.related_invariants); - if non_inv_fun_set.contains(&fun_id) { - if let Some(invs_disabled) = disabled_invs_for_fun.get(&fun_id) { - entrypoint_invariants = entrypoint_invariants - .difference(invs_disabled) - .cloned() - .collect(); - } - } - let xlated_spec = self.translate_invariants(&entrypoint_invariants); - self.assert_or_assume_translated_invariants( - &xlated_spec.invariants, - &entrypoint_invariants, - PropKind::Assume, - ); - - // In addition to the entrypoint invariants assumed just above, it is necessary - // to assume more invariants in a special case. When invariants are disabled in - // this function but not in callers, we will later assert those invariants just - // before return instructions. - // We need to assume those invariants at the beginning of the function in order - // to prove them later. They aren't necessarily entrypoint invariants if we are - // verifying a function in a strict dependency, or in a friend module that does not - // have the target module in its dependencies. - // So, the next code finds the set of target invariants (which will be assumed on return) - // and assumes those that are not entrypoint invariants. - if disabled_inv_fun_set.contains(&fun_id) { - // Separate the update invariants, because we never want to assume them. - let (global_target_invs, _update_target_invs) = - self.separate_update_invariants(target_invariants); - let return_invariants: BTreeSet<_> = global_target_invs - .difference(&entrypoint_invariants) - .cloned() - .collect(); - let xlated_spec = self.translate_invariants(&return_invariants); - self.assert_or_assume_translated_invariants( - &xlated_spec.invariants, - &return_invariants, - PropKind::Assume, - ); - } - - // Generate new instrumented code. - for bc in old_code { - self.instrument_bytecode(bc, fun_id, &inv_ana_data, &entrypoint_invariants); - } - } - - /// Returns list of invariant ids to be assumed at the beginning of the current function. - fn filter_entrypoint_invariants( - &self, - related_invariants: &BTreeSet, - ) -> BTreeSet { - // Emit an assume of each invariant over memory touched by this function. - // Such invariants include - // - invariants declared in this module, or - // - invariants declared in transitively dependent modules - // - // Excludes global invariants that - // - are marked by the user explicitly as `[isolated]`, or - // - are not declared in dependent modules of the module defining the - // function (which may not be the target module) and upon which the - // code should therefore not depend, apart from the update itself, or - // - are "update" invariants. - - // Adds back target invariants that are modified (directly or indirectly) in the function. - - let env = self.builder.global_env(); - let module_env = &self.builder.fun_env.module_env; - - related_invariants - .iter() - .filter_map(|id| { - env.get_global_invariant(*id).filter(|inv| { - // excludes "update invariants" - matches!(inv.kind, ConditionKind::GlobalInvariant(..)) - && module_env.is_transitive_dependency(inv.declaring_module) - && !module_env - .env - .is_property_true(&inv.properties, CONDITION_ISOLATED_PROP) - .unwrap_or(false) - }) - }) - .map(|inv| inv.id) - .collect() - } - - fn instrument_bytecode( - &mut self, - bc: Bytecode, - fun_id: QualifiedId, - inv_ana_data: &InvariantAnalysisData, - entrypoint_invariants: &BTreeSet, - ) { - use BorrowNode::*; - use Bytecode::*; - use Operation::*; - let target_invariants = &inv_ana_data.target_invariants; - let disabled_inv_fun_set = &inv_ana_data.disabled_inv_fun_set; - let always_check_invs: BTreeSet; - if let Some(disabled_invs) = &inv_ana_data.disabled_invs_for_fun.get(&fun_id) { - always_check_invs = entrypoint_invariants - .difference(disabled_invs) - .cloned() - .collect(); - } else { - always_check_invs = entrypoint_invariants.clone(); - } - - match &bc { - Call(_, _, WriteBack(GlobalRoot(mem), ..), ..) => { - self.emit_invariants_for_bytecode( - &bc, - &fun_id, - inv_ana_data, - mem, - &always_check_invs, - ); - }, - Call(_, _, MoveTo(mid, sid, inst), ..) | Call(_, _, MoveFrom(mid, sid, inst), ..) => { - let mem = mid.qualified_inst(*sid, inst.to_owned()); - self.emit_invariants_for_bytecode( - &bc, - &fun_id, - inv_ana_data, - &mem, - &always_check_invs, - ); - }, - // Emit assumes before procedure calls. This also deals with saves for update invariants. - Call(_, _, OpaqueCallBegin(module_id, id, _), _, _) => { - self.assume_invariants_for_opaque_begin( - module_id.qualified(*id), - entrypoint_invariants, - inv_ana_data, - ); - // Then emit the call instruction. - self.builder.emit(bc); - }, - // Emit asserts after procedure calls - Call(_, _, OpaqueCallEnd(module_id, id, _), _, _) => { - // First, emit the call instruction. - self.builder.emit(bc.clone()); - self.assert_invariants_for_opaque_end(module_id.qualified(*id), inv_ana_data) - }, - // An inline call needs to be treated similarly (but there is just one instruction. - Call(_, _, Function(module_id, id, _), _, _) => { - self.assume_invariants_for_opaque_begin( - module_id.qualified(*id), - entrypoint_invariants, - inv_ana_data, - ); - // Then emit the call instruction. - self.builder.emit(bc.clone()); - self.assert_invariants_for_opaque_end(module_id.qualified(*id), inv_ana_data) - }, - // When invariants are disabled in the body of this function but not in its - // callers, assert them just before a return instruction (the caller will be - // assuming they hold). - Ret(_, _) => { - if disabled_inv_fun_set.contains(&fun_id) { - // TODO: It is only necessary to assert invariants that were disabled here. - // Asserting more won't hurt, but generates unnecessary work for the prover. - let (global_target_invs, _update_target_invs) = - self.separate_update_invariants(target_invariants); - let xlated_spec = self.translate_invariants(&global_target_invs); - self.assert_or_assume_translated_invariants( - &xlated_spec.invariants, - &global_target_invs, - PropKind::Assert, - ); - } - self.builder.emit(bc); - }, - _ => self.builder.emit(bc), - } - } - - /// Emit invariants and saves for call to OpaqueCallBegin in the - /// special case where the invariants are not checked in the - /// called function. - fn assume_invariants_for_opaque_begin( - &mut self, - called_fun_id: QualifiedId, - entrypoint_invariants: &BTreeSet, - inv_ana_data: &InvariantAnalysisData, - ) { - let target_invariants = &inv_ana_data.target_invariants; - let disabled_inv_fun_set = &inv_ana_data.disabled_inv_fun_set; - let non_inv_fun_set = &inv_ana_data.non_inv_fun_set; - let funs_that_modify_inv = &inv_ana_data.funs_that_modify_inv; - // Normally, invariants would be assumed and asserted in - // a called function, and so there would be no need to assume - // the invariant before the call. - // When invariants are not disabled in the current function - // but the called function doesn't check them, we are going to - // need to assert the invariant when the call returns (at the - // matching OpaqueCallEnd instruction). So, we assume the - // invariant here, before the OpaqueCallBegin, so that we have - // a hope of proving it later. - let fun_id = self.builder.fun_env.get_qualified_id(); - if !disabled_inv_fun_set.contains(&fun_id) - && !non_inv_fun_set.contains(&fun_id) - && non_inv_fun_set.contains(&called_fun_id) - { - // Do not assume update invs - // This prevents ASSERTING the updates because emit_assumes_and_saves - // stores translated invariants for assertion in assume_invariants_for_opaque_end, - // and we don't want updates to be asserted there. - // TODO: This should all be refactored to eliminate hacks like the previous - // sentence. - let (global_invs, _update_invs) = self.separate_update_invariants(target_invariants); - // assume the invariants that are modified by the called function - let modified_invs = - self.get_invs_modified_by_fun(&global_invs, called_fun_id, funs_that_modify_inv); - self.emit_assumes_and_saves_before_bytecode(modified_invs, entrypoint_invariants); - } - } - - /// Called when invariants need to be checked, but an opaque called function - /// doesn't check them. - fn assert_invariants_for_opaque_end( - &mut self, - called_fun_id: QualifiedId, - inv_ana_data: &InvariantAnalysisData, - ) { - let disabled_inv_fun_set = &inv_ana_data.disabled_inv_fun_set; - let non_inv_fun_set = &inv_ana_data.non_inv_fun_set; - // Add invariant assertions after function call when invariant holds in the - // body of the current function, but the called function does not assert - // invariants. - // The asserted invariant ensures the invariant - // holds in the body of the current function, as is required. - let fun_id = self.builder.fun_env.get_qualified_id(); - if !disabled_inv_fun_set.contains(&fun_id) - && !non_inv_fun_set.contains(&fun_id) - && non_inv_fun_set.contains(&called_fun_id) - { - self.emit_asserts_after_bytecode(); - } - } - - /// Emit invariant-related assumptions and assertions around a bytecode. - /// Before instruction, emit assumptions of global invariants, if necessary, - /// and emit saves of old state for update invariants. - fn emit_invariants_for_bytecode( - &mut self, - bc: &Bytecode, - fun_id: &QualifiedId, - inv_ana_data: &InvariantAnalysisData, - mem: &QualifiedInstId, - entrypoint_invariants: &BTreeSet, - ) { - // When invariants are enabled during the body of the current function, add asserts after - // the operation for each invariant that the operation could modify. Such an operation - // includes write-backs to a GlobalRoot or MoveTo/MoveFrom a location in the global storage. - let target_invariants = &inv_ana_data.target_invariants; - - let env = self.builder.global_env(); - // consider only the invariants that are modified by instruction - // TODO (IMPORTANT): target_invariants and disabled_invs were not computed with unification, - // so it may be that some invariants are not going to be emitted that should be. - let mut modified_invariants: BTreeSet = env - .get_global_invariants_for_memory(mem) - .intersection(target_invariants) - .copied() - .collect(); - - if let Some(disabled_invs) = &inv_ana_data.disabled_invs_for_fun.get(fun_id) { - modified_invariants = modified_invariants - .difference(disabled_invs) - .cloned() - .collect(); - } - self.emit_assumes_and_saves_before_bytecode(modified_invariants, entrypoint_invariants); - // put out the modifying instruction byte code. - self.builder.emit(bc.clone()); - self.emit_asserts_after_bytecode(); - } - - // emit assumptions for invariants that were not assumed on entry and saves for types that are embedded - // in "old" in update invariants. - // When processing assumes before an opaque instruction, modified_invs contains no update invariants. - fn emit_assumes_and_saves_before_bytecode( - &mut self, - modified_invs: BTreeSet, - entrypoint_invariants: &BTreeSet, - ) { - // translate all the invariants. Some were already translated at the entrypoint, but - // that's ok because entrypoint invariants are global invariants that don't have "old", - // so redundant state tags are not going to be a problem. - let mut xlated_invs = self.translate_invariants(&modified_invs); - - let (global_invs, _update_invs) = self.separate_update_invariants(&modified_invs); - - // remove entrypoint invariants so we don't assume them again here. - let modified_assumes: BTreeSet = global_invs - .difference(entrypoint_invariants) - .cloned() - .collect(); - // assume the global invariants that weren't assumed at entrypoint - self.assert_or_assume_translated_invariants( - &xlated_invs.invariants, - &modified_assumes, - PropKind::Assume, - ); - // emit the instructions to save state in the state tags assigned in the previous step - self.emit_state_saves_for_update_invs(&mut xlated_invs); - // Save the translated invariants for use in asserts after instruction or opaque call end - if self.saved_from_before_instr_or_call.is_none() { - self.saved_from_before_instr_or_call = Some((xlated_invs, modified_invs)); - } else { - panic!("self.saved_from_pre should be None"); - } - } - - fn emit_asserts_after_bytecode(&mut self) { - // assert the global and update invariants that instruction modifies, regardless of where they - // were assumed - if let Some((xlated_invs, modified_invs)) = - std::mem::take(&mut self.saved_from_before_instr_or_call) - { - self.assert_or_assume_translated_invariants( - &xlated_invs.invariants, - &modified_invs, - PropKind::Assert, - ); - } else { - // This should never happen - panic!("saved_from_pre should be Some"); - } - } - - /// Given a set of invariants, return a pair of sets: global invariants and update invariants - fn separate_update_invariants( - &self, - invariants: &BTreeSet, - ) -> (BTreeSet, BTreeSet) { - let global_env = self.builder.fun_env.module_env.env; - let mut global_invs: BTreeSet = BTreeSet::new(); - let mut update_invs: BTreeSet = BTreeSet::new(); - for inv_id in invariants { - let inv = global_env.get_global_invariant(*inv_id).unwrap(); - if matches!(inv.kind, ConditionKind::GlobalInvariantUpdate(..)) { - update_invs.insert(*inv_id); - } else { - global_invs.insert(*inv_id); - } - } - (global_invs, update_invs) - } - - /// Returns the set of invariants modified by a function - fn get_invs_modified_by_fun( - &self, - inv_set: &BTreeSet, - fun_id: QualifiedId, - funs_that_modify_inv: &BTreeMap>>, - ) -> BTreeSet { - let mut modified_inv_set: BTreeSet = BTreeSet::new(); - for inv_id in inv_set { - if let Some(fun_id_set) = funs_that_modify_inv.get(inv_id) { - if fun_id_set.contains(&fun_id) { - modified_inv_set.insert(*inv_id); - } - } - } - modified_inv_set - } - - /// Update invariants contain "old" expressions, so it is necessary to save any types in the - /// state that appear in the old expressions. "update_invs" argument must contain only update - /// invariants (not checked). - fn emit_state_saves_for_update_invs(&mut self, xlated_spec: &mut TranslatedSpec) { - // Emit all necessary state saves - self.builder - .set_next_debug_comment("state save for global update invariants".to_string()); - for (mem, label) in std::mem::take(&mut xlated_spec.saved_memory) { - self.builder - .emit_with(|id| Bytecode::SaveMem(id, label, mem)); - } - for (var, label) in std::mem::take(&mut xlated_spec.saved_spec_vars) { - self.builder - .emit_with(|id| Bytecode::SaveSpecVar(id, label, var)); - } - self.builder.clear_next_debug_comment(); - } - - /// emit asserts or assumes (depending on prop_kind argument) for the invariants in - /// xlated_invariants that is also in inv_set at the current location, - fn assert_or_assume_translated_invariants( - &mut self, - xlated_invariants: &[(Loc, GlobalId, Exp)], - inv_set: &BTreeSet, - prop_kind: PropKind, - ) { - let global_env = self.builder.global_env(); - for (loc, mid, cond) in xlated_invariants { - if inv_set.contains(mid) { - // Check for hard-to-debug coding error (this is not a user error) - if inv_set.contains(mid) - && matches!(prop_kind, PropKind::Assume) - && matches!( - global_env.get_global_invariant(*mid).unwrap().kind, - ConditionKind::GlobalInvariantUpdate(..) - ) - { - panic!("Not allowed to assume update invariant"); - } - self.emit_invariant(loc, cond, prop_kind); - } - } - } - - /// Emit an assert or assume for one invariant, give location and expression for the property - fn emit_invariant(&mut self, loc: &Loc, cond: &Exp, prop_kind: PropKind) { - self.builder.set_next_debug_comment(format!( - "global invariant {}", - loc.display(self.builder.global_env()) - )); - // No error messages on assumes - if prop_kind == PropKind::Assert { - self.builder - .set_loc_and_vc_info(loc.clone(), GLOBAL_INVARIANT_FAILS_MESSAGE); - } - self.builder - .emit_with(|id| Bytecode::Prop(id, prop_kind, cond.clone())); - } - - /// Translate the given set of invariants. This will care for instantiating the - /// invariants in the function context. - fn translate_invariants(&mut self, invs: &BTreeSet) -> TranslatedSpec { - let inst_invs = self.compute_instances_for_invariants(invs); - SpecTranslator::translate_invariants_by_id( - self.options.auto_trace_level.invariants(), - &mut self.builder, - inst_invs.into_iter(), - ) - } - - /// Compute the instantiations which need to be verified for each invariant in the input. - /// This may filter out certain invariants which do not have a valid instantiation. - fn compute_instances_for_invariants( - &self, - invs: &BTreeSet, - ) -> Vec<(GlobalId, Vec)> { - invs.iter() - .flat_map(|id| { - let inv = self.builder.global_env().get_global_invariant(*id).unwrap(); - self.compute_invariant_instances(inv).into_iter() - }) - .collect() - } - - /// Compute the instantiations for the given invariant, by comparing the memory accessed - /// by the invariant with that of the enclosing function. - fn compute_invariant_instances( - &self, - inv: &GlobalInvariant, - ) -> BTreeSet<(GlobalId, Vec)> { - // Determine the type arity of this invariant. If it is 0, we shortcut with just - // returning a single empty instance. - let arity = match &inv.kind { - ConditionKind::GlobalInvariant(ps) | ConditionKind::GlobalInvariantUpdate(ps) => { - ps.len() as u16 - }, - _ => 0, - }; - if arity == 0 { - return vec![(inv.id, vec![])].into_iter().collect(); - } - - // Holds possible instantiations per type parameter - let mut per_type_param_insts = BTreeMap::new(); - - // Pairwise unify memory used by the invariant against memory in the function. - // Notice that the function memory is already instantiated for the function variant - // we are instrumenting. - for inv_mem in &inv.mem_usage { - for fun_mem in &self.used_memory { - let adapter = TypeUnificationAdapter::new_vec( - &fun_mem.inst, - &inv_mem.inst, - /* treat_lhs_type_param_as_var */ false, - /* treat_rhs_type_local_as_var */ true, - ); - #[cfg(invariant_trace)] - println!( - "{} =?= {} for inv {}", - self.builder.global_env().display(fun_mem), - self.builder.global_env().display(inv_mem), - inv.loc.display(self.builder.global_env()) - ); - let rel = adapter.unify( - &mut NoUnificationContext, - Variance::SpecVariance, - /* shallow_subst */ false, - ); - match rel { - None => continue, - Some((_, subst_rhs)) => { - #[cfg(invariant_trace)] - println!("unifies {:?}", subst_rhs); - for (k, v) in subst_rhs { - per_type_param_insts - .entry(k) - .or_insert_with(BTreeSet::new) - .insert(v); - } - }, - } - } - } - - // Check whether all type parameters have at least one instantiation. If not, this - // invariant is not applicable (this corresponds to an unbound TypeLocal in the older - // translation scheme). - // TODO: we should generate a type check error if an invariant has unused, dead - // type parameters because such an invariant can never pass this test. - let mut all_insts = BTreeSet::new(); - if (0..arity).collect::>() == per_type_param_insts.keys().cloned().collect() { - // Compute the cartesian product of all individual type parameter instantiations. - for inst in per_type_param_insts - .values() - .map(|tys| tys.iter().cloned()) - .multi_cartesian_product() - { - all_insts.insert((inv.id, inst)); - } - } - all_insts - } -} diff --git a/third_party/move/move-prover/bytecode-pipeline/src/lib.rs b/third_party/move/move-prover/bytecode-pipeline/src/lib.rs index f8d8d9ad95e083..d80434244951d7 100644 --- a/third_party/move/move-prover/bytecode-pipeline/src/lib.rs +++ b/third_party/move/move-prover/bytecode-pipeline/src/lib.rs @@ -6,7 +6,6 @@ pub mod data_invariant_instrumentation; pub mod eliminate_imm_refs; pub mod global_invariant_analysis; pub mod global_invariant_instrumentation; -pub mod global_invariant_instrumentation_v2; pub mod inconsistency_check; pub mod loop_analysis; pub mod memory_instrumentation; @@ -20,5 +19,4 @@ pub mod packed_types_analysis; pub mod pipeline_factory; pub mod spec_instrumentation; pub mod verification_analysis; -pub mod verification_analysis_v2; pub mod well_formed_instrumentation; diff --git a/third_party/move/move-prover/bytecode-pipeline/src/verification_analysis_v2.rs b/third_party/move/move-prover/bytecode-pipeline/src/verification_analysis_v2.rs deleted file mode 100644 index 58082005094998..00000000000000 --- a/third_party/move/move-prover/bytecode-pipeline/src/verification_analysis_v2.rs +++ /dev/null @@ -1,800 +0,0 @@ -// Copyright (c) The Diem Core Contributors -// Copyright (c) The Move Contributors -// SPDX-License-Identifier: Apache-2.0 - -//! Analysis which computes an annotation for each function whether - -use crate::options::ProverOptions; -use itertools::Itertools; -use log::debug; -use move_model::{ - model::{FunId, FunctionEnv, GlobalEnv, GlobalId, ModuleEnv, QualifiedId, VerificationScope}, - pragmas::{ - CONDITION_SUSPENDABLE_PROP, DELEGATE_INVARIANTS_TO_CALLER_PRAGMA, - DISABLE_INVARIANTS_IN_BODY_PRAGMA, VERIFY_PRAGMA, - }, -}; -use move_stackless_bytecode::{ - dataflow_domains::SetDomain, - function_target::{FunctionData, FunctionTarget}, - function_target_pipeline::{FunctionTargetProcessor, FunctionTargetsHolder, FunctionVariant}, - usage_analysis, COMPILED_MODULE_AVAILABLE, -}; -use std::collections::{BTreeMap, BTreeSet, VecDeque}; - -/// The annotation for information about verification. -#[derive(Clone, Default)] -pub struct VerificationInfoV2 { - /// Whether the function is target of verification. - pub verified: bool, - /// Whether the function needs to have an inlined variant since it is called from a verified - /// function and is not opaque. - pub inlined: bool, -} - -/// Get verification information for this function. -pub fn get_info(target: &FunctionTarget<'_>) -> VerificationInfoV2 { - target - .get_annotations() - .get::() - .cloned() - .unwrap_or_default() -} - -// Analysis info to save for global_invariant_instrumentation phase -pub struct InvariantAnalysisData { - /// The set of all functions in target module. - pub target_fun_ids: BTreeSet>, - /// Functions in dependent modules that are transitively called by functions in target module. - pub dep_fun_ids: BTreeSet>, - /// functions where invariants are disabled by pragma disable_invariants_in_body - pub disabled_inv_fun_set: BTreeSet>, - /// Functions where invariants are disabled in a transitive caller, or by - /// pragma delegate_invariant_to_caller - pub non_inv_fun_set: BTreeSet>, - /// global and update invariants in the target module - pub target_invariants: BTreeSet, - /// Maps invariant ID to set of functions that modify the invariant - /// Does not include update invariants - pub funs_that_modify_inv: BTreeMap>>, - /// Maps function to the set of invariants that it modifies - /// Does not include update invariants - pub invs_modified_by_fun: BTreeMap, BTreeSet>, - /// Functions that modify some invariant in the target - /// Does not include update invariants - pub funs_that_modify_some_inv: BTreeSet>, - /// functions that are in non_inv_fun_set and `M[I]` for some `I`. - /// We have to verify the callers, which may be in friend modules. - pub funs_that_delegate_to_caller: BTreeSet>, - /// Functions that are not in target or deps, but that call a function - /// in non_inv_fun_set that modifies some invariant from target module - /// and eventually calls a function in target mod or a dependency. - pub friend_fun_ids: BTreeSet>, - /// For each function, give the set of invariants that are disabled in that function. - /// This is defined as the least set satisfying set inequalities: (1) in a function where - /// invariants are disabled, it is the set of invariants modified in the function, and - /// (2) in a function in non_inv_fun_set, it is the least set that includes all disabled_invs - /// for calling functions. - pub disabled_invs_for_fun: BTreeMap, BTreeSet>, -} - -/// Get all invariants from target modules -fn get_target_invariants( - global_env: &GlobalEnv, - target_modules: &[ModuleEnv], -) -> BTreeSet { - let target_mod_ids = target_modules - .iter() - .map(|mod_env| mod_env.get_id()) - .flat_map(|target_mod_id| global_env.get_global_invariants_by_module(target_mod_id)) - .collect(); - target_mod_ids -} - -/// Computes and returns the set of disabled invariants for each function in disabled_inv_fun_set -/// Disabled invariants for a function are the invariants modified (directly or indirectly) by the fun -/// that are also declared to be suspendable via "invariant [suspendable] ..." -fn compute_disabled_invs_for_fun( - global_env: &GlobalEnv, - disabled_inv_fun_set: &BTreeSet>, - invs_modified_by_fun: &BTreeMap, BTreeSet>, -) -> BTreeMap, BTreeSet> { - let mut disabled_invs_for_fun: BTreeMap, BTreeSet> = - BTreeMap::new(); - for module_env in global_env.get_modules() { - for fun_env in module_env.get_functions() { - let fun_id = fun_env.get_qualified_id(); - // If function disables invariants, get the set of invariants modified in the function - // and keep only those that are declared to be suspendable - if disabled_inv_fun_set.contains(&fun_id) { - if let Some(modified_invs) = invs_modified_by_fun.get(&fun_id) { - let disabled_invs: BTreeSet = modified_invs - .iter() - .filter(|inv_id| { - global_env - .is_property_true( - &global_env - .get_global_invariant(**inv_id) - .unwrap() - .properties, - CONDITION_SUSPENDABLE_PROP, - ) - .unwrap_or(false) - }) - .cloned() - .collect(); - debug_print_inv_set( - global_env, - &disabled_invs, - "$$$$$$$$$$$$$$$$\ncompute_disabled_invs_for_fun", - ); - disabled_invs_for_fun.insert(fun_id, disabled_invs.clone()); - } - } - } - } - - // Compute a least fixed point of disable_invs_for_fun. Starts with disabled inv functions and - // all invariants that they modify. Then propagate those to called functions. They're not top-sorted - // (which may not be good enough for recursion, in this case, I'm not sure). So fun_ids go back - // into the worklist until the disable_inv_set for each fun converges (worklist will be empty). - let mut worklist: VecDeque> = disabled_inv_fun_set.iter().cloned().collect(); - while let Some(caller_fun_id) = worklist.pop_front() { - // If None, it's ok to skip because there are no disabled_invs to propagate to called funs - if let Some(disabled_invs_for_caller) = disabled_invs_for_fun.remove(&caller_fun_id) { - let called_funs = global_env - .get_function(caller_fun_id) - .get_called_functions() - .cloned() - .expect(COMPILED_MODULE_AVAILABLE); - for called_fun_id in called_funs { - let disabled_invs_for_called = - disabled_invs_for_fun.entry(called_fun_id).or_default(); - // if caller has any disabled_invs that callee does not, add them to called - // and add called to the worklist for further processing - if !disabled_invs_for_caller.is_subset(disabled_invs_for_called) { - // Add missing inv_ids to called set - for inv_id in &disabled_invs_for_caller { - disabled_invs_for_called.insert(*inv_id); - } - worklist.push_back(called_fun_id); - } - } - // put back disabled_invs_for_caller - disabled_invs_for_fun.insert(caller_fun_id, disabled_invs_for_caller); - } - } - disabled_invs_for_fun -} - -/// Check whether function is callable from unknown sites (i.e., it is public or -/// a script fun) and modifies some invariant in the target module. -/// The second condition is an exception for functions that cannot invalidate -/// any invariants. -fn check_legal_disabled_invariants( - fun_env: &FunctionEnv, - disabled_inv_fun_set: &BTreeSet>, - non_inv_fun_set: &BTreeSet>, - funs_that_modify_some_inv: &BTreeSet>, -) { - let global_env = fun_env.module_env.env; - let fun_id = fun_env.get_qualified_id(); - if non_inv_fun_set.contains(&fun_id) && funs_that_modify_some_inv.contains(&fun_id) { - if disabled_inv_fun_set.contains(&fun_id) { - global_env.error( - &fun_env.get_loc(), - "Functions must not have a disable invariant pragma when invariants are \ - disabled in a transitive caller or there is a \ - pragma delegate_invariants_to_caller", - ); - } else if fun_env.has_unknown_callers() { - if is_fun_delegating(fun_env) { - global_env.error( - &fun_env.get_loc(), - "Public or script functions cannot delegate invariants", - ) - } else { - global_env.error_with_notes( - &fun_env.get_loc(), - "Public or script functions cannot be transitively called by \ - functions disabling or delegating invariants", - compute_non_inv_cause_chain(fun_env), - ) - } - } - } -} - -/// Compute the chain of calls which leads to an implicit non-inv function. -fn compute_non_inv_cause_chain(fun_env: &FunctionEnv<'_>) -> Vec { - let global_env = fun_env.module_env.env; - let mut worklist: BTreeSet>> = fun_env - .get_calling_functions() - .expect(COMPILED_MODULE_AVAILABLE) - .into_iter() - .map(|id| vec![id]) - .collect(); - let mut done = BTreeSet::new(); - let mut result = vec![]; - while let Some(caller_list) = worklist.iter().next().cloned() { - worklist.remove(&caller_list); - let caller_id = *caller_list.iter().last().unwrap(); - done.insert(caller_id); - let caller_env = global_env.get_function_qid(caller_id); - let display_chain = || { - vec![fun_env.get_qualified_id()] - .into_iter() - .chain(caller_list.iter().cloned()) - .map(|id| global_env.get_function_qid(id).get_full_name_str()) - .join(" <- ") - }; - if is_fun_disabled(&caller_env) { - result.push(format!("disabled by {}", display_chain())); - } else if is_fun_delegating(&caller_env) { - result.push(format!("delegated by {}", display_chain())); - } else { - worklist.extend( - caller_env - .get_calling_functions() - .expect(COMPILED_MODULE_AVAILABLE) - .into_iter() - .filter_map(|id| { - if done.contains(&id) { - None - } else { - let mut new_caller_list = caller_list.clone(); - new_caller_list.push(id); - Some(new_caller_list) - } - }), - ); - } - } - if result.is_empty() { - result.push("cannot determine disabling reason (bug?)".to_owned()) - } - result -} - -// Using pragmas, find functions called from a context where invariant -// checking is disabled. -// disabled_inv_fun set are disabled by pragma -// non_inv_fun_set are disabled by pragma or because they're called from -// another function in disabled_inv_fun_set or non_inv_fun_set. -fn compute_disabled_and_non_inv_fun_sets( - global_env: &GlobalEnv, -) -> (BTreeSet>, BTreeSet>) { - let mut non_inv_fun_set: BTreeSet> = BTreeSet::new(); - let mut disabled_inv_fun_set: BTreeSet> = BTreeSet::new(); - // invariant: If a function is in non_inv_fun_set and not in worklist, - // then all the functions it calls are also in fun_set - // or in worklist. When worklist is empty, all callees of a function - // in non_inv_fun_set will also be in non_inv_fun_set. - // Each function is added at most once to the worklist. - let mut worklist = vec![]; - for module_env in global_env.get_modules() { - for fun_env in module_env.get_functions() { - if is_fun_disabled(&fun_env) { - let fun_id = fun_env.get_qualified_id(); - disabled_inv_fun_set.insert(fun_id); - worklist.push(fun_id); - } - if is_fun_delegating(&fun_env) { - let fun_id = fun_env.get_qualified_id(); - if non_inv_fun_set.insert(fun_id) { - // Add to work_list only if fun_id is not in non_inv_fun_set (may have inferred - // this from a caller already). - worklist.push(fun_id); - } - } - // Downward closure of non_inv_fun_set - while let Some(called_fun_id) = worklist.pop() { - let called_funs = global_env - .get_function(called_fun_id) - .get_called_functions() - .cloned() - .expect(COMPILED_MODULE_AVAILABLE); - for called_fun_id in called_funs { - if non_inv_fun_set.insert(called_fun_id) { - // Add to work_list only if fun_id is not in fun_set - worklist.push(called_fun_id); - } - } - } - } - } - (disabled_inv_fun_set, non_inv_fun_set) -} - -fn is_fun_disabled(fun_env: &FunctionEnv<'_>) -> bool { - fun_env.is_pragma_true(DISABLE_INVARIANTS_IN_BODY_PRAGMA, || false) -} - -fn is_fun_delegating(fun_env: &FunctionEnv<'_>) -> bool { - fun_env.is_pragma_true(DELEGATE_INVARIANTS_TO_CALLER_PRAGMA, || false) -} - -/// Collect all functions that are defined in the target module, or called transitively -/// from those functions. -/// TODO: This is not very efficient. It would be better to compute the transitive closure. -fn compute_dep_fun_ids( - global_env: &GlobalEnv, - target_modules: &[ModuleEnv], -) -> BTreeSet> { - let mut dep_fun_ids = BTreeSet::new(); - for module_env in global_env.get_modules() { - for target_env in target_modules { - if target_env.is_transitive_dependency(module_env.get_id()) { - for fun_env in module_env.get_functions() { - dep_fun_ids.insert(fun_env.get_qualified_id()); - } - } - } - } - dep_fun_ids -} - -/// Compute a map from each invariant to the set of functions that modify state -/// appearing in the invariant. Return that, and a second value that is the union -/// of functions over all invariants in the first map. -/// This is not applied to update invariants? -fn compute_funs_that_modify_inv( - global_env: &GlobalEnv, - target_invariants: &BTreeSet, - targets: &mut FunctionTargetsHolder, - variant: FunctionVariant, -) -> ( - BTreeMap>>, - BTreeMap, BTreeSet>, - BTreeSet>, -) { - let mut funs_that_modify_inv: BTreeMap>> = - BTreeMap::new(); - let mut funs_that_modify_some_inv: BTreeSet> = BTreeSet::new(); - let mut invs_modified_by_fun: BTreeMap, BTreeSet> = - BTreeMap::new(); - for inv_id in target_invariants { - // Collect the global state used by inv_id (this is computed in usage_analysis.rs) - let inv_mem_use: SetDomain<_> = global_env - .get_global_invariant(*inv_id) - .unwrap() - .mem_usage - .iter() - .cloned() - .collect(); - // set of functions that modify state in inv_id that we are building - let mut fun_id_set: BTreeSet> = BTreeSet::new(); - // Iterate over all functions in the module cluster - for module_env in global_env.get_modules() { - for fun_env in module_env.get_functions() { - // Get all memory modified by this function. - let fun_target = targets.get_target(&fun_env, &variant); - let modified_memory = &usage_analysis::get_memory_usage(&fun_target).modified.all; - // Add functions to set if it modifies mem used in invariant - // TODO: This should be using unification. - if !modified_memory.is_disjoint(&inv_mem_use) { - let fun_id = fun_env.get_qualified_id(); - fun_id_set.insert(fun_id); - funs_that_modify_some_inv.insert(fun_id); - let inv_set = invs_modified_by_fun.entry(fun_id).or_default(); - inv_set.insert(*inv_id); - } - } - } - if !fun_id_set.is_empty() { - funs_that_modify_inv.insert(*inv_id, fun_id_set); - } - } - ( - funs_that_modify_inv, - invs_modified_by_fun, - funs_that_modify_some_inv, - ) -} - -/// Compute the set of functions that are friend modules of target or deps, but not in -/// target or deps, and that call a function in non_inv_fun_set that modifies some target -/// invariant. The Prover needs to verify that these functions preserve the target invariants. -fn compute_friend_fun_ids( - global_env: &GlobalEnv, - target_fun_ids: &BTreeSet>, - dep_fun_ids: &BTreeSet>, - funs_that_delegate_to_caller: &BTreeSet>, -) -> BTreeSet> { - let mut friend_fun_set: BTreeSet> = BTreeSet::new(); - let mut worklist: Vec> = target_fun_ids.iter().cloned().collect(); - worklist.extend(dep_fun_ids.iter().cloned()); - while let Some(fun_id) = worklist.pop() { - // Check for legacy friend pragma - // TODO: Delete when we stop using pragma friend in DiemFramework - let fun_env = global_env.get_function(fun_id); - let friend_env = fun_env.get_transitive_friend(); - let friend_id = friend_env.get_qualified_id(); - // if no transitive friend, it just returns the original fun_env - if friend_id != fun_env.get_qualified_id() && friend_fun_set.insert(friend_id) { - worklist.push(friend_id); - } - if funs_that_delegate_to_caller.contains(&fun_id) { - let callers = fun_env - .get_calling_functions() - .expect(COMPILED_MODULE_AVAILABLE); - for caller_fun_id in callers { - // Exclude callers that are in target or dep modules, because we will verify them, anyway. - // We also don't need to put them in the worklist, because they were in there initially. - // Also, don't need to process if it's already in friend_fun_set - if !target_fun_ids.contains(&caller_fun_id) - && !dep_fun_ids.contains(&caller_fun_id) - && friend_fun_set.insert(caller_fun_id) - { - worklist.push(caller_fun_id); - } - } - } - } - friend_fun_set -} - -#[allow(dead_code)] -/// Debug print: Print global id and body of each invariant, so we can just print the global -/// id's in sets for compactness -fn debug_print_global_ids(global_env: &GlobalEnv, global_ids: &BTreeSet) { - for inv_id in global_ids { - debug_print_inv_full(global_env, inv_id); - } -} - -/// Debugging function to print a set of function id's using their -/// symbolic function names. -#[allow(dead_code)] -fn debug_print_fun_id_set( - global_env: &GlobalEnv, - fun_ids: &BTreeSet>, - set_name: &str, -) { - debug!( - "****************\n{}: {:?}", - set_name, - fun_ids - .iter() - .map(|fun_id| global_env.get_function(*fun_id).get_name_string()) - .collect::>() - ); -} - -/// Debugging code to print sets of invariants -#[allow(dead_code)] -pub fn debug_print_inv_set( - global_env: &GlobalEnv, - global_ids: &BTreeSet, - set_name: &str, -) { - if global_ids.is_empty() { - return; - } - debug!("{}:", set_name); - // for global_id in global_ids { - // debug!("global_id: {:?}", *global_id); - // } - debug!("++++++++++++++++\n{}:", set_name); - for inv_id in global_ids { - debug_print_inv_full(global_env, inv_id); - } -} - -/// Given global id of invariant, prints the global ID and the source code -/// of the invariant -#[allow(dead_code)] -fn debug_print_inv_full(global_env: &GlobalEnv, inv_id: &GlobalId) { - let inv = global_env.get_global_invariant(*inv_id); - let loc = &inv.unwrap().loc; - debug!( - "{:?} {:?}: {}", - *inv_id, - inv.unwrap().kind, - global_env.get_source(loc).unwrap(), - ); -} - -#[allow(dead_code)] -fn debug_print_fun_inv_map( - global_env: &GlobalEnv, - fun_inv_map: &BTreeMap, BTreeSet>, - map_name: &str, -) { - debug!("****************\nMAP NAME {}:", map_name); - for (fun_id, inv_id_set) in fun_inv_map.iter() { - let fname = global_env.get_function(*fun_id).get_name_string(); - debug!("FUNCTION {}:", fname); - for inv_id in inv_id_set { - debug_print_inv_full(global_env, inv_id); - } - // debug_print_inv_set(global_env, inv_id_set, &fname); - } -} - -// global_env.get_function(*fun_id).get_name_string(); - -/// Print sets and maps computed during verification analysis -#[allow(dead_code)] -fn debug_print_invariant_analysis_data( - global_env: &GlobalEnv, - inv_ana_data: &InvariantAnalysisData, -) { - debug_print_fun_id_set(global_env, &inv_ana_data.target_fun_ids, "target_fun_ids"); - debug_print_fun_id_set(global_env, &inv_ana_data.dep_fun_ids, "dep_fun_ids"); - debug_print_fun_id_set( - global_env, - &inv_ana_data.disabled_inv_fun_set, - "disabled_inv_fun_set", - ); - debug_print_fun_id_set(global_env, &inv_ana_data.non_inv_fun_set, "non_inv_fun_set"); - debug_print_inv_set( - global_env, - &inv_ana_data.target_invariants, - "target_invariants", - ); - - // "funs_modified_by_inv" map - - debug_print_fun_inv_map( - global_env, - &inv_ana_data.invs_modified_by_fun, - "invs_modified_by_fun", - ); - - debug_print_fun_id_set( - global_env, - &inv_ana_data.funs_that_modify_some_inv, - "funs_that_modify_some_inv", - ); - debug_print_fun_id_set( - global_env, - &inv_ana_data.funs_that_delegate_to_caller, - "funs_that_delegate_to_caller", - ); - debug_print_fun_id_set(global_env, &inv_ana_data.friend_fun_ids, "friend_fun_ids"); - - debug_print_fun_inv_map( - global_env, - &inv_ana_data.disabled_invs_for_fun, - "disabled_invs_for_fun", - ); -} - -pub struct VerificationAnalysisProcessorV2(); - -impl VerificationAnalysisProcessorV2 { - pub fn new() -> Box { - Box::new(Self()) - } -} - -impl FunctionTargetProcessor for VerificationAnalysisProcessorV2 { - fn process( - &self, - targets: &mut FunctionTargetsHolder, - fun_env: &FunctionEnv, - data: FunctionData, - _scc_opt: Option<&[FunctionEnv]>, - ) -> FunctionData { - let global_env = fun_env.module_env.env; - let fun_id = fun_env.get_qualified_id(); - let variant = data.variant.clone(); - // When this is called, the data of this function is removed from targets so it can - // be mutated, as per pipeline processor design. We put it back temporarily to have - // a unique model of targets. - targets.insert_target_data(&fun_id, variant.clone(), data); - let inv_ana_data = global_env.get_extension::().unwrap(); - let target_fun_ids = &inv_ana_data.target_fun_ids; - let dep_fun_ids = &inv_ana_data.dep_fun_ids; - let friend_fun_ids = &inv_ana_data.friend_fun_ids; - let funs_that_modify_some_inv = &inv_ana_data.funs_that_modify_some_inv; - // Logic to decide whether to verify this function - // Never verify if "pragma verify = false;" - if fun_env.is_pragma_true(VERIFY_PRAGMA, || true) { - let is_in_target_mod = target_fun_ids.contains(&fun_id); - let is_in_deps_and_modifies_inv = - dep_fun_ids.contains(&fun_id) && funs_that_modify_some_inv.contains(&fun_id); - let is_in_friends = friend_fun_ids.contains(&fun_id); - let is_normally_verified = - is_in_target_mod || is_in_deps_and_modifies_inv || is_in_friends; - let options = ProverOptions::get(global_env); - let is_verified = match &options.verify_scope { - VerificationScope::Public => { - (is_in_target_mod && fun_env.is_exposed()) - || is_in_deps_and_modifies_inv - || is_in_friends - }, - VerificationScope::All => is_normally_verified, - VerificationScope::Only(function_name) => { - fun_env.matches_name(function_name) && is_in_target_mod - }, - VerificationScope::OnlyModule(module_name) => { - is_in_target_mod && fun_env.module_env.matches_name(module_name) - }, - VerificationScope::None => false, - }; - if is_verified { - debug!("marking `{}` to be verified", fun_env.get_full_name_str()); - mark_verified(fun_env, variant.clone(), targets); - } - } - - targets.remove_target_data(&fun_id, &variant) - } - - fn name(&self) -> String { - "verification_analysis_v2".to_string() - } - - fn initialize(&self, global_env: &GlobalEnv, targets: &mut FunctionTargetsHolder) { - let options = ProverOptions::get(global_env); - - // If we are verifying only one function or module, check that this indeed exists. - match &options.verify_scope { - VerificationScope::Only(name) | VerificationScope::OnlyModule(name) => { - let for_module = matches!(&options.verify_scope, VerificationScope::OnlyModule(_)); - let mut target_exists = false; - for module in global_env.get_modules() { - if module.is_target() { - if for_module { - target_exists = module.matches_name(name) - } else { - target_exists = module.get_functions().any(|f| f.matches_name(name)); - } - if target_exists { - break; - } - } - } - if !target_exists { - global_env.error( - &global_env.unknown_loc(), - &format!( - "{} target {} does not exist in target modules", - if for_module { "module" } else { "function" }, - name - ), - ) - } - }, - _ => {}, - } - - let target_modules = global_env.get_primary_target_modules(); - let target_fun_ids: BTreeSet> = target_modules - .iter() - .flat_map(|mod_env| mod_env.get_functions()) - .map(|fun| fun.get_qualified_id()) - .collect(); - let dep_fun_ids = compute_dep_fun_ids(global_env, &target_modules); - let (disabled_inv_fun_set, non_inv_fun_set) = - compute_disabled_and_non_inv_fun_sets(global_env); - let target_invariants = get_target_invariants(global_env, &target_modules); - let (funs_that_modify_inv, invs_modified_by_fun, funs_that_modify_some_inv) = - compute_funs_that_modify_inv( - global_env, - &target_invariants, - targets, - FunctionVariant::Baseline, - ); - let funs_that_delegate_to_caller = non_inv_fun_set - .intersection(&funs_that_modify_some_inv) - .cloned() - .collect(); - let friend_fun_ids = compute_friend_fun_ids( - global_env, - &target_fun_ids, - &dep_fun_ids, - &funs_that_delegate_to_caller, - ); - let disabled_invs_for_fun = - compute_disabled_invs_for_fun(global_env, &disabled_inv_fun_set, &invs_modified_by_fun); - - // Check for public or script functions that are in non_inv_fun_set - for module_env in global_env.get_modules() { - for fun_env in module_env.get_functions() { - check_legal_disabled_invariants( - &fun_env, - &disabled_inv_fun_set, - &non_inv_fun_set, - &funs_that_modify_some_inv, - ); - } - } - let inv_ana_data = InvariantAnalysisData { - target_fun_ids, - dep_fun_ids, - disabled_inv_fun_set, - non_inv_fun_set, - target_invariants, - funs_that_modify_inv, - invs_modified_by_fun, - funs_that_modify_some_inv, - funs_that_delegate_to_caller, - friend_fun_ids, - disabled_invs_for_fun, - }; - - // Note: To print verbose debugging info, use - debug_print_invariant_analysis_data(global_env, &inv_ana_data); - - global_env.set_extension(inv_ana_data); - } -} - -/// Mark this function as being verified. If it has a friend and is verified only in the -/// friends context, mark the friend instead. This also marks all functions directly or -/// indirectly called by this function as inlined if they are not opaque. -fn mark_verified( - fun_env: &FunctionEnv<'_>, - variant: FunctionVariant, - targets: &mut FunctionTargetsHolder, -) { - let actual_env = fun_env.get_transitive_friend(); - if actual_env.get_qualified_id() != fun_env.get_qualified_id() { - // Instead of verifying this function directly, we mark the friend as being verified, - // and this function as inlined. - mark_inlined(fun_env, variant.clone(), targets); - } - // The user can override with `pragma verify = false`, so respect this. - let options = ProverOptions::get(fun_env.module_env.env); - if !actual_env.is_explicitly_not_verified(&options.verify_scope) { - let info = targets - .get_data_mut(&actual_env.get_qualified_id(), &variant) - .expect("function data available") - .annotations - .get_or_default_mut::(true); - if !info.verified { - info.verified = true; - mark_callees_inlined(&actual_env, variant, targets); - } - } -} - -/// Mark this function as inlined if it is not opaque, and if it is -/// are called from a verified function via a chain of zero-or-more -/// inline functions. If it is not called from a verified function, -/// it does not need to be inlined. -fn mark_inlined( - fun_env: &FunctionEnv<'_>, - variant: FunctionVariant, - targets: &mut FunctionTargetsHolder, -) { - if fun_env.is_native() || fun_env.is_intrinsic() { - return; - } - debug_assert!( - targets.get_target_variants(fun_env).contains(&variant), - "`{}` has variant `{:?}`", - fun_env.get_name().display(fun_env.symbol_pool()), - variant - ); - let data = targets - .get_data_mut(&fun_env.get_qualified_id(), &variant) - .expect("function data defined"); - let info = data - .annotations - .get_or_default_mut::(true); - if !info.inlined { - info.inlined = true; - mark_callees_inlined(fun_env, variant, targets); - } -} - -/// Continue transitively marking callees as inlined. -fn mark_callees_inlined( - fun_env: &FunctionEnv<'_>, - variant: FunctionVariant, - targets: &mut FunctionTargetsHolder, -) { - for callee in fun_env - .get_called_functions() - .expect(COMPILED_MODULE_AVAILABLE) - { - let callee_env = fun_env.module_env.env.get_function(*callee); - if !callee_env.is_opaque() { - mark_inlined(&callee_env, variant.clone(), targets); - } - } -} diff --git a/third_party/move/move-prover/lab/Cargo.toml b/third_party/move/move-prover/lab/Cargo.toml index 5ebf0e18075a0d..dc90304f53b02a 100644 --- a/third_party/move/move-prover/lab/Cargo.toml +++ b/third_party/move/move-prover/lab/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "prover-lab" +name = "move-prover-lab" version = "0.1.0" authors = ["Diem Association "] publish = false @@ -12,13 +12,9 @@ chrono = { workspace = true } clap = { workspace = true, features = ["derive"] } codespan-reporting = { workspace = true } itertools = { workspace = true } -log = { workspace = true, features = ["serde"] } -move-compiler = { workspace = true } -move-compiler-v2 = { workspace = true } move-model = { workspace = true } move-prover = { workspace = true } move-prover-boogie-backend = { workspace = true } move-prover-bytecode-pipeline = { workspace = true } plotters = { workspace = true, features = ["evcxr", "line_series", "histogram"] } z3tracer = { workspace = true } - diff --git a/third_party/move/move-prover/lab/src/benchmark.rs b/third_party/move/move-prover/lab/src/benchmark.rs index b05b6515083a40..edc750c34ef2d2 100644 --- a/third_party/move/move-prover/lab/src/benchmark.rs +++ b/third_party/move/move-prover/lab/src/benchmark.rs @@ -13,13 +13,7 @@ use clap::{ }; use codespan_reporting::term::termcolor::{ColorChoice, StandardStream}; use itertools::Itertools; -use log::LevelFilter; -use move_compiler::shared::{known_attributes::KnownAttribute, PackagePaths}; -use move_compiler_v2::{env_pipeline::rewrite_target::RewritingScope, Experiment}; -use move_model::{ - model::{FunctionEnv, GlobalEnv, ModuleEnv, VerificationScope}, - parse_addresses_from_options, run_model_builder_with_options, -}; +use move_model::model::{FunctionEnv, GlobalEnv, ModuleEnv, VerificationScope}; use move_prover::{ check_errors, cli::Options, create_and_process_bytecode, create_init_num_operation_state, generate_boogie, verify_boogie, @@ -149,27 +143,9 @@ fn run_benchmark( } else { Options::default() }; - let addrs = parse_addresses_from_options(options.move_named_address_values.clone())?; + options.move_sources.append(&mut modules.to_vec()); options.move_deps.append(&mut dep_dirs.to_vec()); - let skip_attribute_checks = true; - let known_attributes = KnownAttribute::get_all_attribute_names().clone(); - let mut env = run_model_builder_with_options( - vec![PackagePaths { - name: None, - paths: modules.to_vec(), - named_address_map: addrs.clone(), - }], - vec![], - vec![PackagePaths { - name: None, - paths: options.move_deps.clone(), - named_address_map: addrs, - }], - options.model_builder.clone(), - skip_attribute_checks, - &known_attributes, - )?; - let mut error_writer = StandardStream::stderr(ColorChoice::Auto); + options.skip_attribute_checks = true; if use_aptos_natives { options.backend.custom_natives = @@ -184,14 +160,16 @@ fn run_benchmark( // Do not allow any benchmark to run longer than 60s. If this is exceeded it usually // indicates a bug in boogie or the solver, because we already propagate soft timeouts, but // they are ignored. - options.backend.hard_timeout_secs = 400; + options.backend.hard_timeout_secs = 60; options.backend.global_timeout_overwrite = false; - options.backend.vc_timeout = 300; - - options.verbosity_level = LevelFilter::Warn; + options.backend.vc_timeout = 400; + options.set_quiet(); options.backend.proc_cores = 1; options.backend.derive_options(); options.setup_logging(); + + let mut error_writer = StandardStream::stderr(ColorChoice::Auto); + let env = move_prover::create_move_prover_v2_model(&mut error_writer, options.clone())?; check_errors(&env, &options, &mut error_writer, "unexpected build errors")?; let config_descr = if let Some(config) = config_file_opt { @@ -216,17 +194,6 @@ fn run_benchmark( Notice that execution is slow because we enforce single core execution.", config_descr ); - // Need to run the pipeline to - let compiler_options = move_compiler_v2::Options::default() - .set_experiment(Experiment::OPTIMIZE, false) - .set_experiment(Experiment::SPEC_REWRITE, true); - env.set_extension(compiler_options.clone()); - let pipeline = move_compiler_v2::check_and_rewrite_pipeline( - &compiler_options, - true, - RewritingScope::Everything, - ); - pipeline.run(&mut env); runner.bench(&env) } @@ -261,13 +228,13 @@ impl Runner { // Write data record of benchmark result writeln!( self.out, - "{:<40} {:>12} {:>12}", + "{:<50} {:>15} {:>15}", fun.get_full_name_str(), duration.as_millis(), status )?; - println!("\x08\x08{:.3}s {}.", duration.as_secs_f64(), status); + println!(" {:.3}s {}.", duration.as_secs_f64(), status); Ok(()) } diff --git a/third_party/move/move-prover/lab/src/main.rs b/third_party/move/move-prover/lab/src/main.rs index 1db9219c151c98..a9a8c38bae7aee 100644 --- a/third_party/move/move-prover/lab/src/main.rs +++ b/third_party/move/move-prover/lab/src/main.rs @@ -5,7 +5,7 @@ #![forbid(unsafe_code)] use itertools::Itertools; -use prover_lab::{benchmark, plot}; +use move_prover_lab::{benchmark, plot}; fn main() { let args = std::env::args().collect_vec(); diff --git a/third_party/move/move-prover/src/lib.rs b/third_party/move/move-prover/src/lib.rs index 46810fe825d9db..57fff879e0e094 100644 --- a/third_party/move/move-prover/src/lib.rs +++ b/third_party/move/move-prover/src/lib.rs @@ -71,19 +71,26 @@ pub fn run_move_prover_v2( options: Options, ) -> anyhow::Result<()> { let now = Instant::now(); - let cloned_options = options.clone(); + let mut env = create_move_prover_v2_model(error_writer, options.clone())?; + run_move_prover_with_model_v2(&mut env, error_writer, options, now) +} + +pub fn create_move_prover_v2_model( + error_writer: &mut W, + options: Options, +) -> anyhow::Result { let compiler_options = move_compiler_v2::Options { - dependencies: cloned_options.move_deps, - named_address_mapping: cloned_options.move_named_address_values, - output_dir: cloned_options.output_path, - language_version: cloned_options.language_version, + dependencies: options.move_deps, + named_address_mapping: options.move_named_address_values, + output_dir: options.output_path, + language_version: options.language_version, compiler_version: None, // TODO: need to pass v2.x here skip_attribute_checks: true, known_attributes: Default::default(), - testing: cloned_options.backend.stable_test_output, + testing: options.backend.stable_test_output, experiments: vec![], experiment_cache: Default::default(), - sources: cloned_options.move_sources, + sources: options.move_sources, sources_deps: vec![], warn_deprecated: false, warn_of_deprecation_use_in_aptos_libs: false, @@ -94,8 +101,7 @@ pub fn run_move_prover_v2( external_checks: vec![], }; - let mut env = move_compiler_v2::run_move_compiler_for_analysis(error_writer, compiler_options)?; - run_move_prover_with_model_v2(&mut env, error_writer, options, now) + move_compiler_v2::run_move_compiler_for_analysis(error_writer, compiler_options) } /// Create the initial number operation state for each function and struct