diff --git a/crates/move-prover-boogie-backend/src/generator.rs b/crates/move-prover-boogie-backend/src/generator.rs index 293fd60ad8..0a237c6999 100644 --- a/crates/move-prover-boogie-backend/src/generator.rs +++ b/crates/move-prover-boogie-backend/src/generator.rs @@ -314,6 +314,8 @@ fn generate_function_bpl( let target_type = FunctionHolderTarget::Function(*qid); let (mut targets, _) = create_and_process_bytecode(options, env, package_targets, target_type); + write_spec_hierarchy_logs(env, &targets, &options, asserts_mode); + check_errors( env, &options, @@ -378,6 +380,8 @@ fn generate_module_bpl( let (mut targets, _) = create_and_process_bytecode(options, env, package_targets, target_type); + write_spec_hierarchy_logs(env, &targets, &options, asserts_mode); + check_errors( env, &options, @@ -731,6 +735,20 @@ pub async fn verify_boogie( Ok(()) } +/// Write spec hierarchy log files for all specs in the given targets. +/// Only writes during `AssertsMode::Check` to avoid duplicate writes. +fn write_spec_hierarchy_logs( + env: &GlobalEnv, + targets: &FunctionTargetsHolder, + options: &Options, + asserts_mode: AssertsMode, +) { + if asserts_mode == AssertsMode::Check { + let output_dir = Path::new(&options.output_path); + spec_hierarchy::display_spec_hierarchy(env, targets, output_dir); + } +} + /// Create bytecode and process it. pub fn create_and_process_bytecode( options: &Options, diff --git a/crates/move-stackless-bytecode/src/spec_hierarchy.rs b/crates/move-stackless-bytecode/src/spec_hierarchy.rs index 69a0016734..ca992b8f79 100644 --- a/crates/move-stackless-bytecode/src/spec_hierarchy.rs +++ b/crates/move-stackless-bytecode/src/spec_hierarchy.rs @@ -30,56 +30,57 @@ struct CallInfo { spec_id: Option>, } -/// Generates and writes specification hierarchy trees to log files. +/// Writes the hierarchy log file for a single spec using already-built targets. /// -/// For each spec in the targets, creates a `.log.txt` file in the output directory -/// showing the complete call hierarchy including: -/// - All functions called by the spec's underlying implementation -/// - Spec properties (prove, no_opaque) for functions that have specs -/// - System functions are excluded (stdlib, Sui framework, etc.) -/// - Tree structure with proper indentation using box-drawing characters -/// -/// # Tree Traversal -/// - Recurses into functions without specs to find nested specs -/// - Stops recursing at opaque specs (specs without `no_opaque`) -/// - Recurses into `no_opaque` specs since the prover uses their implementation -/// - Prevents infinite recursion by tracking displayed functions +/// This is designed to be called during verification, reusing the +/// `FunctionTargetsHolder` that was already created with proper per-spec +/// filtering (e.g. `FunctionHolderTarget::Function`). /// /// # Arguments -/// * `env` - Global environment containing all function and module information -/// * `targets` - Holder containing all specs and their relationships +/// * `env` - Global environment +/// * `targets` - Targets holder with spec mappings (already built for this spec's context) +/// * `spec_id` - The spec to write the hierarchy for /// * `output_dir` - Directory where .log.txt files will be written -pub fn display_spec_hierarchy(env: &GlobalEnv, targets: &FunctionTargetsHolder, output_dir: &Path) { +pub fn write_spec_hierarchy_log( + env: &GlobalEnv, + targets: &FunctionTargetsHolder, + spec_id: &QualifiedId, + output_dir: &Path, +) { let excluded_addresses = get_excluded_addresses(); + let spec_env = env.get_function(*spec_id); + let spec_name = spec_env.get_full_name_str(); - for spec_id in targets.specs() { - let spec_env = env.get_function(*spec_id); - let spec_name = spec_env.get_full_name_str(); + if let Some(fun_id) = targets.get_fun_by_spec(spec_id) { + let func_env = env.get_function(*fun_id); + let header = func_env.get_full_name_str(); + write_spec_log_file( + env, + targets, + &func_env, + spec_name, + &header, + output_dir, + &excluded_addresses, + ); + } else if targets.is_scenario_spec(spec_id) { + let header = format!("{} {}", spec_env.get_full_name_str(), SCENARIO_LABEL); + write_spec_log_file( + env, + targets, + &spec_env, + spec_name, + &header, + output_dir, + &excluded_addresses, + ); + } +} - if let Some(fun_id) = targets.get_fun_by_spec(spec_id) { - let func_env = env.get_function(*fun_id); - let header = func_env.get_full_name_str(); - write_spec_log_file( - env, - targets, - &func_env, - spec_name, - &header, - output_dir, - &excluded_addresses, - ); - } else if targets.is_scenario_spec(spec_id) { - let header = format!("{} {}", spec_env.get_full_name_str(), SCENARIO_LABEL); - write_spec_log_file( - env, - targets, - &spec_env, - spec_name, - &header, - output_dir, - &excluded_addresses, - ); - } +/// Writes hierarchy log files for all specs in the given targets. +pub fn display_spec_hierarchy(env: &GlobalEnv, targets: &FunctionTargetsHolder, output_dir: &Path) { + for spec_id in targets.specs() { + write_spec_hierarchy_log(env, targets, spec_id, output_dir); } } diff --git a/crates/sui-prover/src/prove.rs b/crates/sui-prover/src/prove.rs index 7a27f6db29..770412b295 100644 --- a/crates/sui-prover/src/prove.rs +++ b/crates/sui-prover/src/prove.rs @@ -10,11 +10,9 @@ use move_core_types::account_address::AccountAddress; use move_model::model::GlobalEnv; use move_package::{BuildConfig as MoveBuildConfig, LintFlag}; use move_prover_boogie_backend::boogie_backend::options::BoogieFileMode; -use move_prover_boogie_backend::generator::{create_and_process_bytecode, run_boogie_gen}; +use move_prover_boogie_backend::generator::run_boogie_gen; use move_stackless_bytecode::function_stats; -use move_stackless_bytecode::function_target_pipeline::FunctionHolderTarget; use move_stackless_bytecode::package_targets::PackageTargets; -use move_stackless_bytecode::spec_hierarchy; use move_stackless_bytecode::target_filter::TargetFilterOptions; use std::{ collections::BTreeMap, @@ -184,21 +182,6 @@ pub async fn execute( return Ok(()); } - let mut options = move_prover_boogie_backend::generator_options::Options::default(); - options.filter = filter.clone(); - let (targets, _) = create_and_process_bytecode( - &options, - &model, - &package_targets, - FunctionHolderTarget::All, - ); - - let output_dir = std::path::Path::new(&options.output_path); - if !output_dir.exists() { - std::fs::create_dir_all(output_dir)?; - } - spec_hierarchy::display_spec_hierarchy(&model, &targets, output_dir); - execute_backend_boogie(model, &general_config, remote_config, boogie_config, filter).await }