Split cargo creusot and creusot-rustc in two separate directories

Cargo.toml

@@ -2,6 +2,7 @@
 resolver = "2"
 members = [
   "cargo-creusot",
+  "creusot-rustc",
   "creusot",
   "creusot-contracts",
   "creusot-contracts-proc",

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"] }

cargo-creusot/src/bin/cargo-creusot.rs → 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<String> {
+    let toolchain: toml::Value = toml::from_str(include_str!("../../rust-toolchain")).ok()?;
+    let channel = toolchain["toolchain"]["channel"].as_str()?;
+    Some(channel.into())
+}

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,
-        }
-    }
-}

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"] }

cargo-creusot/src/bin/creusot-rustc.rs → 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")

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<String>,
+    #[clap(long)]
+    /// Location that Creusot metadata for this crate should be emitted to.
+    metadata_path: Option<String>,
+    /// 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<String>,
+    /// 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::<String, String>, 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<T, U>(s: &str) -> Result<(T, U), Box<dyn Error + Send + Sync + 'static>>
+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<String>,
+}
+
+#[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,
+        }
+    }
+}

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();