diff --git a/Cargo.lock b/Cargo.lock index a06faf7c9f0a7f..c0d749fc515d12 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -310,7 +310,7 @@ dependencies = [ "dashmap", "diesel", "diesel-async", - "dirs", + "dirs 5.0.1", "futures", "hex", "itertools 0.13.0", @@ -328,6 +328,7 @@ dependencies = [ "move-ir-types", "move-model", "move-package", + "move-prover-boogie-backend", "move-symbol-pool", "move-unit-test", "move-vm-runtime", @@ -342,6 +343,7 @@ dependencies = [ "serde_json", "serde_yaml 0.8.26", "server-framework", + "set_env", "shadow-rs", "tempfile", "thiserror", @@ -7314,13 +7316,22 @@ dependencies = [ "walkdir", ] +[[package]] +name = "dirs" +version = "4.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ca3aa72a6f96ea37bbc5aa912f6788242832f75369bdfdadcb0e38423f100059" +dependencies = [ + "dirs-sys 0.3.7", +] + [[package]] name = "dirs" version = "5.0.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "44c45a9d03d6676652bcb5e724c7e988de1acad23a711b5217ab9cbecbec2225" dependencies = [ - "dirs-sys", + "dirs-sys 0.4.1", ] [[package]] @@ -7333,6 +7344,17 @@ dependencies = [ "dirs-sys-next", ] +[[package]] +name = "dirs-sys" +version = "0.3.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1b1d1d91c932ef41c0f2663aa8b0ca0342d444d842c06914aa0a7e352d0bada6" +dependencies = [ + "libc", + "redox_users", + "winapi 0.3.9", +] + [[package]] name = "dirs-sys" version = "0.4.1" @@ -15174,6 +15196,15 @@ dependencies = [ "warp", ] +[[package]] +name = "set_env" +version = "1.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "51864fb62fd09b8a7d931a11832bfbbda5297425cfc9ce04b54bc86c945c58eb" +dependencies = [ + "dirs 4.0.0", +] + [[package]] name = "sha1" version = "0.10.6" diff --git a/Cargo.toml b/Cargo.toml index f58a1e238a2811..0a56d71213156e 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -741,6 +741,7 @@ serde-generate = { git = "https://github.com/aptos-labs/serde-reflection", rev = serde-reflection = { git = "https://github.com/aptos-labs/serde-reflection", rev = "73b6bbf748334b71ff6d7d09d06a29e3062ca075" } serde_with = "3.4.0" serde_yaml = "0.8.24" +set_env = "1.3.4" shadow-rs = "0.16.2" simplelog = "0.9.0" smallbitvec = "2.5.1" diff --git a/crates/aptos/CHANGELOG.md b/crates/aptos/CHANGELOG.md index de17a8a00bbfd2..11233848e532b7 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 +- Adds `aptos update prover-dependencies`, which installs the dependency of Move prover, boogie, z3 and cvc5. ## [4.2.2] - 2024/09/20 - Fix localnet indexer processors that were emitting spamming logs in 4.2.1. diff --git a/crates/aptos/Cargo.toml b/crates/aptos/Cargo.toml index 44a8a862819345..384ebc2d51e701 100644 --- a/crates/aptos/Cargo.toml +++ b/crates/aptos/Cargo.toml @@ -78,6 +78,7 @@ move-disassembler = { workspace = true } move-ir-types = { workspace = true } move-model = { workspace = true } move-package = { workspace = true } +move-prover-boogie-backend = { workspace = true } move-symbol-pool = { workspace = true } move-unit-test = { workspace = true, features = ["debugging"] } move-vm-runtime = { workspace = true, features = ["testing"] } @@ -94,6 +95,7 @@ serde = { workspace = true } serde_json = { workspace = true } serde_yaml = { workspace = true } server-framework = { git = "https://github.com/aptos-labs/aptos-indexer-processors.git", rev = "51a34901b40d7f75767ac907b4d2478104d6a515" } +set_env = { workspace = true } tempfile = { workspace = true } thiserror = { workspace = true } tokio = { workspace = true } diff --git a/crates/aptos/src/update/aptos.rs b/crates/aptos/src/update/aptos.rs index 56cab921e3a1f8..4a1d7e77d8ffd9 100644 --- a/crates/aptos/src/update/aptos.rs +++ b/crates/aptos/src/update/aptos.rs @@ -49,8 +49,8 @@ impl BinaryUpdater for AptosUpdateTool { self.check } - fn pretty_name(&self) -> &'static str { - "Aptos CLI" + fn pretty_name(&self) -> String { + "Aptos CLI".to_string() } /// Return information about whether an update is required. diff --git a/crates/aptos/src/update/mod.rs b/crates/aptos/src/update/mod.rs index f854bca2219fe8..58aee4cf5d688f 100644 --- a/crates/aptos/src/update/mod.rs +++ b/crates/aptos/src/update/mod.rs @@ -7,6 +7,8 @@ mod aptos; mod helpers; mod movefmt; +mod prover_dependencies; +mod prover_dependency_installer; mod revela; mod tool; mod update_helper; @@ -25,7 +27,7 @@ trait BinaryUpdater { fn check(&self) -> bool; /// Only used for messages we print to the user. - fn pretty_name(&self) -> &'static str; + fn pretty_name(&self) -> String; /// Return information about whether an update is required. fn get_update_info(&self) -> Result; diff --git a/crates/aptos/src/update/movefmt.rs b/crates/aptos/src/update/movefmt.rs index f614c1f3d5686d..bdf945a46945f1 100644 --- a/crates/aptos/src/update/movefmt.rs +++ b/crates/aptos/src/update/movefmt.rs @@ -64,8 +64,8 @@ impl BinaryUpdater for FormatterUpdateTool { self.check } - fn pretty_name(&self) -> &'static str { - "movefmt" + fn pretty_name(&self) -> String { + "movefmt".to_string() } /// Return information about whether an update is required. @@ -127,5 +127,6 @@ pub fn get_movefmt_path() -> Result { FORMATTER_EXE_ENV, FORMATTER_BINARY_NAME, FORMATTER_EXE, + true, ) } diff --git a/crates/aptos/src/update/prover_dependencies.rs b/crates/aptos/src/update/prover_dependencies.rs new file mode 100644 index 00000000000000..d7256d9fbaa251 --- /dev/null +++ b/crates/aptos/src/update/prover_dependencies.rs @@ -0,0 +1,213 @@ +// Copyright © Aptos Foundation +// SPDX-License-Identifier: Apache-2.0 + +use crate::{ + cli_build_information, + common::types::{CliCommand, CliError, CliTypedResult}, + update::{ + get_additional_binaries_dir, prover_dependency_installer::DependencyInstaller, + update_binary, + }, +}; +use anyhow::{Context, Result}; +use aptos_build_info::BUILD_OS; +use async_trait::async_trait; +use clap::Parser; +use move_prover_boogie_backend::options::{ + BoogieOptions, MAX_BOOGIE_VERSION, MAX_CVC5_VERSION, MAX_Z3_VERSION, MIN_BOOGIE_VERSION, + MIN_CVC5_VERSION, MIN_Z3_VERSION, +}; +use std::{ + env, + path::{Path, PathBuf}, +}; + +pub(crate) const REPO_NAME: &str = "prover-dependency"; +pub(crate) const REPO_OWNER: &str = "aptos-labs"; + +pub(crate) const BOOGIE_BINARY_NAME: &str = "boogie"; +pub(crate) const TARGET_BOOGIE_VERSION: &str = "3.2.4"; + +pub(crate) const BOOGIE_EXE_ENV: &str = "BOOGIE_EXE"; +#[cfg(target_os = "windows")] +pub(crate) const BOOGIE_EXE: &str = "boogie.exe"; +#[cfg(not(target_os = "windows"))] +pub(crate) const BOOGIE_EXE: &str = "boogie"; + +const Z3_BINARY_NAME: &str = "z3"; +const TARGET_Z3_VERSION: &str = "4.11.2"; + +const Z3_EXE_ENV: &str = "Z3_EXE"; +#[cfg(target_os = "windows")] +const Z3_EXE: &str = "z3.exe"; +#[cfg(not(target_os = "windows"))] +const Z3_EXE: &str = "z3"; + +const CVC5_BINARY_NAME: &str = "cvc5"; +const TARGET_CVC5_VERSION: &str = "0.0.3"; + +const CVC5_EXE_ENV: &str = "CVC5_EXE"; +#[cfg(target_os = "windows")] +const CVC5_EXE: &str = "cvc5.exe"; +#[cfg(not(target_os = "windows"))] +const CVC5_EXE: &str = "cvc5"; + +/// Install dependencies (boogie, z3 and cvc5) for Move prover +#[derive(Debug, Parser)] +pub struct ProverDependencyInstaller { + /// Where to install binaries of boogie, z3 and cvc5. If not + /// given we will put it in a standard location for your OS. + #[clap(long)] + install_dir: Option, +} + +impl ProverDependencyInstaller { + fn add_env_var(&self, env_var: &str, install_path: &Path) -> Result<(), CliError> { + if let Ok(current_value) = env::var(env_var) { + if current_value == install_path.to_string_lossy() { + return Ok(()); + } else { + return Err(CliError::UnexpectedError(format!( + "{} is already set to a different value: {}.", + env_var, current_value + ))); + } + } + + set_env::set(env_var, install_path.to_string_lossy()) + .map_err(|e| CliError::UnexpectedError(format!("Failed to set {}: {}", env_var, e)))?; + println!( + "Added {} to environment with value: {}.", + env_var, + install_path.to_string_lossy() + ); + if env::var(env_var).is_err() { + println!("Please use the `source` command or reboot the terminal to check whether {} is set with the correct value. \ + If not, please set it manually.", env_var); + } + Ok(()) + } + + async fn download_dependency(&self) -> CliTypedResult { + let build_info = cli_build_information(); + let _ = match build_info.get(BUILD_OS).context("Failed to determine build info of current CLI")?.as_str() { + "linux-x86_64" => Ok("linux"), + "macos-aarch64" | "macos-x86_64" => Ok("macos"), + "windows-x86_64" => Ok("win"), + wildcard => Err(CliError::UnexpectedError(format!("Self-updating is not supported on your OS ({}) right now, please download the binary manually", wildcard))), + }; + + let install_dir = match self.install_dir.clone() { + Some(dir) => dir, + None => { + let dir = get_additional_binaries_dir(); + // Make the directory if it doesn't already exist. + std::fs::create_dir_all(&dir) + .with_context(|| format!("Failed to create directory: {:?}", dir))?; + dir + }, + }; + + BoogieOptions::check_version_is_compatible( + BOOGIE_BINARY_NAME, + &format!("{}.0", TARGET_BOOGIE_VERSION), + MIN_BOOGIE_VERSION, + MAX_BOOGIE_VERSION, + )?; + let res = self + .install_binary( + install_dir.clone(), + BOOGIE_EXE, + BOOGIE_BINARY_NAME, + TARGET_BOOGIE_VERSION, + "/", + "Boogie program verifier version ", + BOOGIE_EXE_ENV, + ) + .await?; + println!("{}", res); + + BoogieOptions::check_version_is_compatible( + Z3_BINARY_NAME, + TARGET_Z3_VERSION, + MIN_Z3_VERSION, + MAX_Z3_VERSION, + )?; + let res = self + .install_binary( + install_dir.clone(), + Z3_EXE, + Z3_BINARY_NAME, + TARGET_Z3_VERSION, + "--", + "Z3 version ", + Z3_EXE_ENV, + ) + .await?; + println!("{}", res); + + #[cfg(unix)] + { + BoogieOptions::check_version_is_compatible( + CVC5_BINARY_NAME, + TARGET_CVC5_VERSION, + MIN_CVC5_VERSION, + MAX_CVC5_VERSION, + )?; + let res = self + .install_binary( + install_dir.clone(), + CVC5_EXE, + CVC5_BINARY_NAME, + TARGET_CVC5_VERSION, + "--", + "This is cvc5 version ", + CVC5_EXE_ENV, + ) + .await?; + println!("{}", res); + } + + Ok("Succeeded".to_string()) + } + + async fn install_binary( + &self, + install_dir: PathBuf, + exe_name: &str, + binary_name: &str, + version: &str, + version_option_string: &str, + version_match_string: &str, + env_name: &str, + ) -> CliTypedResult { + let installer = DependencyInstaller { + binary_name: binary_name.to_string(), + exe_name: exe_name.to_string(), + env_var: env_name.to_string(), + version_option_string: version_option_string.to_string(), + version_match_string: version_match_string.to_string(), + target_version: version.to_string(), + install_dir: Some(install_dir.clone()), + check: false, + }; + let result = update_binary(installer).await?; + + let install_dir = install_dir.join(exe_name); + if let Err(err) = self.add_env_var(env_name, &install_dir) { + eprintln!("{:#}. Please set it manually", err); + } + Ok(result) + } +} + +#[async_trait] +impl CliCommand for ProverDependencyInstaller { + fn command_name(&self) -> &'static str { + "InstallProverDependencies" + } + + async fn execute(self) -> CliTypedResult { + self.download_dependency().await + } +} diff --git a/crates/aptos/src/update/prover_dependency_installer.rs b/crates/aptos/src/update/prover_dependency_installer.rs new file mode 100644 index 00000000000000..39291235ff14a8 --- /dev/null +++ b/crates/aptos/src/update/prover_dependency_installer.rs @@ -0,0 +1,107 @@ +// Copyright © Aptos Foundation +// SPDX-License-Identifier: Apache-2.0 + +use super::{BinaryUpdater, UpdateRequiredInfo}; +use crate::update::{ + prover_dependencies::{REPO_NAME, REPO_OWNER}, + update_helper::{build_updater, get_path}, +}; +use anyhow::{Context, Result}; +use self_update::update::ReleaseUpdate; +use std::path::PathBuf; + +/// Update Prover dependency. +#[derive(Debug)] +pub struct DependencyInstaller { + pub binary_name: String, + + pub exe_name: String, + + pub env_var: String, + + pub version_match_string: String, + + pub version_option_string: String, + + pub target_version: String, + + pub install_dir: Option, + + pub check: bool, +} + +impl DependencyInstaller { + fn extract_version(&self, input: &str) -> String { + use regex::Regex; + let version_format = format!(r"{}{}", self.version_match_string, r"\d+\.\d+\.\d+"); + let re = Regex::new(&version_format).unwrap(); + if let Some(caps) = re.captures(input) { + let version = caps.get(0).unwrap().as_str().to_string(); + return version + .trim_start_matches(&self.version_match_string) + .to_string(); + } + String::new() + } + + pub fn get_path(&self) -> Result { + get_path( + &self.binary_name, + &self.env_var, + &self.binary_name, + &self.exe_name, + false, + ) + } +} + +impl BinaryUpdater for DependencyInstaller { + fn check(&self) -> bool { + false + } + + fn pretty_name(&self) -> String { + self.binary_name.clone() + } + + /// Return information about whether an update is required. + fn get_update_info(&self) -> Result { + // Get the current version, if any. + let dependency_path = self.get_path(); + let current_version = match dependency_path { + Ok(path) if path.exists() => { + let output = std::process::Command::new(path) + .arg(format!("{}version", self.version_option_string)) + .output() + .context("Failed to get current version")?; + let stdout = String::from_utf8(output.stdout) + .context("Failed to parse current version as UTF-8")?; + let version = self.extract_version(&stdout); + if !version.is_empty() { + Some(version) + } else { + None + } + }, + _ => None, + }; + + Ok(UpdateRequiredInfo { + current_version, + target_version: self.target_version.trim_start_matches('v').to_string(), + }) + } + + fn build_updater(&self, info: &UpdateRequiredInfo) -> Result> { + build_updater( + info, + self.install_dir.clone(), + REPO_OWNER.to_string(), + REPO_NAME.to_string(), + &self.binary_name, + "unknown-linux-gnu", + "apple-darwin", + "windows", + ) + } +} diff --git a/crates/aptos/src/update/revela.rs b/crates/aptos/src/update/revela.rs index 84fb0674793a33..3d4910a34d0887 100644 --- a/crates/aptos/src/update/revela.rs +++ b/crates/aptos/src/update/revela.rs @@ -54,8 +54,8 @@ impl BinaryUpdater for RevelaUpdateTool { self.check } - fn pretty_name(&self) -> &'static str { - "Revela" + fn pretty_name(&self) -> String { + "Revela".to_string() } /// Return information about whether an update is required. @@ -115,5 +115,11 @@ impl CliCommand for RevelaUpdateTool { } pub fn get_revela_path() -> Result { - get_path("decompiler", REVELA_EXE_ENV, REVELA_BINARY_NAME, REVELA_EXE) + get_path( + "decompiler", + REVELA_EXE_ENV, + REVELA_BINARY_NAME, + REVELA_EXE, + false, + ) } diff --git a/crates/aptos/src/update/tool.rs b/crates/aptos/src/update/tool.rs index c56fd9f58b65ba..79724cfb91c762 100644 --- a/crates/aptos/src/update/tool.rs +++ b/crates/aptos/src/update/tool.rs @@ -4,7 +4,7 @@ use super::{aptos::AptosUpdateTool, revela::RevelaUpdateTool}; use crate::{ common::types::{CliCommand, CliResult}, - update::movefmt::FormatterUpdateTool, + update::{movefmt::FormatterUpdateTool, prover_dependencies::ProverDependencyInstaller}, }; use clap::Subcommand; @@ -14,6 +14,7 @@ pub enum UpdateTool { Aptos(AptosUpdateTool), Revela(RevelaUpdateTool), Movefmt(FormatterUpdateTool), + ProverDependencies(ProverDependencyInstaller), } impl UpdateTool { @@ -22,6 +23,7 @@ impl UpdateTool { UpdateTool::Aptos(tool) => tool.execute_serialized().await, UpdateTool::Revela(tool) => tool.execute_serialized().await, UpdateTool::Movefmt(tool) => tool.execute_serialized().await, + UpdateTool::ProverDependencies(tool) => tool.execute_serialized().await, } } } diff --git a/crates/aptos/src/update/update_helper.rs b/crates/aptos/src/update/update_helper.rs index 50797eae0e85fa..e413fadc4fdd40 100644 --- a/crates/aptos/src/update/update_helper.rs +++ b/crates/aptos/src/update/update_helper.rs @@ -48,7 +48,10 @@ pub fn build_updater( let target = format!("{}-{}", arch_str, target); let install_dir = match install_dir.clone() { - Some(dir) => dir, + Some(dir) => { + println!("dir:{:?}", dir); + dir + }, None => { let dir = get_additional_binaries_dir(); // Make the directory if it doesn't already exist. @@ -63,6 +66,12 @@ pub fn build_updater( None => "0.0.0", }; + println!( + "install_dir:{:?}, is directory:{}", + install_dir, + install_dir.is_dir() + ); + Update::configure() .bin_install_dir(install_dir) .bin_name(binary_name) @@ -75,7 +84,13 @@ pub fn build_updater( .map_err(|e| anyhow!("Failed to build self-update configuration: {:#}", e)) } -pub fn get_path(name: &str, exe_env: &str, binary_name: &str, exe: &str) -> Result { +pub fn get_path( + name: &str, + exe_env: &str, + binary_name: &str, + exe: &str, + find_in_path: bool, +) -> Result { // Look at the environment variable first. if let Ok(path) = std::env::var(exe_env) { return Ok(PathBuf::from(path)); @@ -87,9 +102,11 @@ pub fn get_path(name: &str, exe_env: &str, binary_name: &str, exe: &str) -> Resu return Ok(path); } - // See if we can find the binary in the PATH. - if let Some(path) = pathsearch::find_executable_in_path(exe) { - return Ok(path); + if find_in_path { + // See if we can find the binary in the PATH. + if let Some(path) = pathsearch::find_executable_in_path(exe) { + return Ok(path); + } } Err(anyhow!( 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 947da3a5be5001..5c16b9faa66fda 100644 --- a/third_party/move/move-prover/boogie-backend/src/options.rs +++ b/third_party/move/move-prover/boogie-backend/src/options.rs @@ -21,14 +21,14 @@ const DEFAULT_BOOGIE_FLAGS: &[&str] = &[ /// Versions for boogie, z3, and cvc5. The upgrade of boogie and z3 is mostly backward compatible, /// but not always. Setting the max version allows Prover to warn users for the higher version of /// boogie and z3 because those may be incompatible. -const MIN_BOOGIE_VERSION: Option<&str> = Some("3.0.1.0"); -const MAX_BOOGIE_VERSION: Option<&str> = Some("3.2.4.0"); +pub const MIN_BOOGIE_VERSION: Option<&str> = Some("3.0.1.0"); +pub const MAX_BOOGIE_VERSION: Option<&str> = Some("3.2.4.0"); -const MIN_Z3_VERSION: Option<&str> = Some("4.11.2"); -const MAX_Z3_VERSION: Option<&str> = Some("4.11.2"); +pub const MIN_Z3_VERSION: Option<&str> = Some("4.11.2"); +pub const MAX_Z3_VERSION: Option<&str> = Some("4.11.2"); -const MIN_CVC5_VERSION: Option<&str> = Some("0.0.3"); -const MAX_CVC5_VERSION: Option<&str> = None; +pub const MIN_CVC5_VERSION: Option<&str> = Some("0.0.3"); +pub const MAX_CVC5_VERSION: Option<&str> = None; #[derive(Debug, Clone, Copy, Serialize, Deserialize)] pub enum VectorTheory { @@ -357,7 +357,7 @@ impl BoogieOptions { } } - fn check_version_is_compatible( + pub fn check_version_is_compatible( tool: &str, given: &str, expected_min: Option<&str>,