diff --git a/Cargo.lock b/Cargo.lock index 4c4fd47f16..0159b6764b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -114,7 +114,6 @@ name = "cargo-creusot" version = "0.1.0" dependencies = [ "clap", - "creusot", "env_logger", "serde", "serde_json", @@ -254,6 +253,18 @@ dependencies = [ "indexmap", ] +[[package]] +name = "creusot-rustc" +version = "0.1.0" +dependencies = [ + "clap", + "creusot", + "env_logger", + "serde", + "serde_json", + "toml", +] + [[package]] name = "difflib" version = "0.4.0" diff --git a/Cargo.toml b/Cargo.toml index 82f3616beb..276e763adb 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -2,6 +2,7 @@ resolver = "2" members = [ "cargo-creusot", + "creusot-rustc", "creusot", "creusot-contracts", "creusot-contracts-proc", diff --git a/cargo-creusot/Cargo.toml b/cargo-creusot/Cargo.toml index dff3e6dd7f..2de97cd5fa 100644 --- a/cargo-creusot/Cargo.toml +++ b/cargo-creusot/Cargo.toml @@ -7,8 +7,7 @@ edition = "2021" [dependencies] serde_json = { version = "1.0" } -clap = { version = "4.2", features = ["derive", "env"] } -creusot = { path = "../creusot", version = "*" } +clap = { version = "4.2.5", features = ["derive", "env"] } toml = "0.5.8" env_logger = "*" serde = { version = "1.0", features = ["derive"] } diff --git a/cargo-creusot/src/bin/cargo-creusot.rs b/cargo-creusot/src/main.rs similarity index 67% rename from cargo-creusot/src/bin/cargo-creusot.rs rename to cargo-creusot/src/main.rs index 990e0cac00..1ffceb5fbb 100644 --- a/cargo-creusot/src/bin/cargo-creusot.rs +++ b/cargo-creusot/src/main.rs @@ -5,6 +5,8 @@ use std::{ process::{exit, Command}, }; +mod options; + fn main() { let args = Args::parse_from(std::env::args().skip(1)); @@ -14,8 +16,11 @@ fn main() { let cargo_path = env::var("CARGO_PATH").unwrap_or_else(|_| "cargo".to_string()); let cargo_cmd = if std::env::var_os("CREUSOT_CONTINUE").is_some() { "build" } else { "check" }; + let toolchain = toolchain_channel() + .expect("Expected `cargo-creusot` to be built with a valid toolchain file"); let mut cmd = Command::new(cargo_path); - cmd.arg(&cargo_cmd) + cmd.arg(format!("+{toolchain}")) + .arg(&cargo_cmd) .args(args.rust_flags) .env("RUSTC_WRAPPER", creusot_rustc_path) .env("CARGO_CREUSOT", "1"); @@ -27,3 +32,9 @@ fn main() { exit(exit_status.code().unwrap_or(-1)); } } + +fn toolchain_channel() -> Option { + let toolchain: toml::Value = toml::from_str(include_str!("../../rust-toolchain")).ok()?; + let channel = toolchain["toolchain"]["channel"].as_str()?; + Some(channel.into()) +} diff --git a/cargo-creusot/src/options.rs b/cargo-creusot/src/options.rs index b97e4ab7a1..e4a7897a78 100644 --- a/cargo-creusot/src/options.rs +++ b/cargo-creusot/src/options.rs @@ -1,10 +1,7 @@ use clap::*; -use creusot::options::{self, OutputFile}; use serde::{Deserialize, Serialize}; use std::error::Error; -pub use creusot::options::Options; - #[derive(Parser, Serialize, Deserialize)] pub struct CreusotArgs { /// Determines how to format the spans in generated code to loading in Why3. @@ -63,36 +60,3 @@ pub enum SpanMode { Absolute, Off, } - -impl CreusotArgs { - pub fn to_options(self) -> Options { - let metadata_path = self.metadata_path; - let extern_paths = self.extern_paths.into_iter().collect(); - - let cargo_creusot = std::env::var("CARGO_CREUSOT").is_ok(); - let should_output = !cargo_creusot || std::env::var("CARGO_PRIMARY_PACKAGE").is_ok(); - - let output_file = match (self.stdout, self.output_file) { - (true, _) => Some(OutputFile::Stdout), - (_, Some(f)) => Some(OutputFile::File(f)), - _ => None, - }; - - let span_mode = match self.span_mode { - SpanMode::Relative => options::SpanMode::Relative, - SpanMode::Absolute => options::SpanMode::Absolute, - SpanMode::Off => options::SpanMode::Off, - }; - - Options { - extern_paths, - metadata_path, - export_metadata: self.export_metadata, - should_output, - output_file, - in_cargo: cargo_creusot, - span_mode: span_mode, - match_str: self.focus_on, - } - } -} diff --git a/creusot-rustc/Cargo.toml b/creusot-rustc/Cargo.toml new file mode 100644 index 0000000000..c4a115df4a --- /dev/null +++ b/creusot-rustc/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "creusot-rustc" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] +serde_json = { version = "1.0" } +clap = { version = "4.2.5", features = ["derive", "env"] } +creusot = { path = "../creusot", version = "*" } +toml = "0.5.8" +env_logger = "*" +serde = { version = "1.0", features = ["derive"] } diff --git a/cargo-creusot/src/bin/creusot-rustc.rs b/creusot-rustc/src/main.rs similarity index 98% rename from cargo-creusot/src/bin/creusot-rustc.rs rename to creusot-rustc/src/main.rs index af37fa2a03..b0adaf7374 100644 --- a/cargo-creusot/src/bin/creusot-rustc.rs +++ b/creusot-rustc/src/main.rs @@ -1,17 +1,19 @@ #![feature(rustc_private)] - extern crate lazy_static; extern crate rustc_driver; extern crate rustc_errors; extern crate rustc_interface; extern crate rustc_session; +mod options; +use options::Args; + #[macro_use] extern crate log; -use cargo_creusot::options::{Args, CreusotArgs}; use clap::*; use creusot::callbacks::*; +use options::CreusotArgs; use rustc_driver::{RunCompiler, DEFAULT_LOCALE_RESOURCES}; use rustc_errors::{emitter::EmitterWriter, TerminalUrl}; use rustc_interface::interface::try_print_query_stack; @@ -140,7 +142,7 @@ fn setup_plugin() { } fn sysroot_path() -> String { - let toolchain: toml::Value = toml::from_str(include_str!("../../../rust-toolchain")).unwrap(); + let toolchain: toml::Value = toml::from_str(include_str!("../../rust-toolchain")).unwrap(); let channel = toolchain["toolchain"]["channel"].as_str().unwrap(); let output = Command::new("rustup") diff --git a/creusot-rustc/src/options.rs b/creusot-rustc/src/options.rs new file mode 100644 index 0000000000..b97e4ab7a1 --- /dev/null +++ b/creusot-rustc/src/options.rs @@ -0,0 +1,98 @@ +use clap::*; +use creusot::options::{self, OutputFile}; +use serde::{Deserialize, Serialize}; +use std::error::Error; + +pub use creusot::options::Options; + +#[derive(Parser, Serialize, Deserialize)] +pub struct CreusotArgs { + /// Determines how to format the spans in generated code to loading in Why3. + /// [Relative] is better if the generated code is meant to be checked into VCS. + /// [Absolute] means the files can easily be moved around your system and still work. + /// [None] provides the clearest diffs. + #[clap(long, value_enum, default_value_t=SpanMode::Relative)] + span_mode: SpanMode, + #[clap(long)] + /// Only generate proofs for items matching the provided string. The string is treated + /// as a Rust qualified path. + focus_on: Option, + #[clap(long)] + /// Location that Creusot metadata for this crate should be emitted to. + metadata_path: Option, + /// Tell creusot to disable metadata exports. + #[arg(long, default_value_t = true, action = clap::ArgAction::Set)] + export_metadata: bool, + /// Print to stdout. + #[clap(group = "output", long)] + stdout: bool, + /// Print to a file. + #[clap(group = "output", long, env)] + output_file: Option, + /// Specify locations of metadata for external crates. The format is the same as rustc's `--extern` flag. + #[clap(long = "creusot-extern", value_parser= parse_key_val::, required=false)] + extern_paths: Vec<(String, String)>, + /// Check the installed why3 version. + #[clap(long, default_value_t = true, action = clap::ArgAction::Set)] + pub check_why3: bool, +} + +/// Parse a single key-value pair +fn parse_key_val(s: &str) -> Result<(T, U), Box> +where + T: std::str::FromStr, + T::Err: Error + Send + Sync + 'static, + U: std::str::FromStr, + U::Err: Error + Send + Sync + 'static, +{ + let pos = s.find('=').ok_or_else(|| format!("invalid KEY=value: no `=` found in `{}`", s))?; + Ok((s[..pos].parse()?, s[pos + 1..].parse()?)) +} + +#[derive(Parser)] +pub struct Args { + #[clap(flatten)] + pub creusot: CreusotArgs, + #[clap(last = true)] + pub rust_flags: Vec, +} + +#[derive(clap::ValueEnum, Clone, Deserialize, Serialize)] +pub enum SpanMode { + Relative, + Absolute, + Off, +} + +impl CreusotArgs { + pub fn to_options(self) -> Options { + let metadata_path = self.metadata_path; + let extern_paths = self.extern_paths.into_iter().collect(); + + let cargo_creusot = std::env::var("CARGO_CREUSOT").is_ok(); + let should_output = !cargo_creusot || std::env::var("CARGO_PRIMARY_PACKAGE").is_ok(); + + let output_file = match (self.stdout, self.output_file) { + (true, _) => Some(OutputFile::Stdout), + (_, Some(f)) => Some(OutputFile::File(f)), + _ => None, + }; + + let span_mode = match self.span_mode { + SpanMode::Relative => options::SpanMode::Relative, + SpanMode::Absolute => options::SpanMode::Absolute, + SpanMode::Off => options::SpanMode::Off, + }; + + Options { + extern_paths, + metadata_path, + export_metadata: self.export_metadata, + should_output, + output_file, + in_cargo: cargo_creusot, + span_mode: span_mode, + match_str: self.focus_on, + } + } +} diff --git a/creusot/tests/ui.rs b/creusot/tests/ui.rs index c6f66ca19a..41c80ba545 100644 --- a/creusot/tests/ui.rs +++ b/creusot/tests/ui.rs @@ -18,7 +18,7 @@ fn main() { let creusot_rustc = escargot::CargoBuild::new() .bin("creusot-rustc") .current_release() - .manifest_path("../cargo-creusot/Cargo.toml") + .manifest_path("../creusot-rustc/Cargo.toml") .current_target() .run() .unwrap();