Merge pull request #997 from laurentder/issue_943

Issue 943

cargo-creusot/Cargo.toml

@@ -13,3 +13,6 @@ serde = { version = "1.0", features = ["derive"] }
 creusot-args = {path = "../creusot-args"}
 creusot-setup = {path = "../creusot-setup"}
 anyhow = "1.0"
+cargo_metadata = "0.18.1"
+include_dir = "0.7.3"
+tempdir = "0.3.7"

cargo-creusot/src/helpers.rs

@@ -0,0 +1,52 @@
+use std::path::PathBuf;
+
+use anyhow::anyhow;
+use cargo_metadata::{self, Package};
+pub type Result<T> = anyhow::Result<T>;
+
+pub(crate) fn make_cargo_metadata() -> Result<cargo_metadata::Metadata> {
+    let mut args = std::env::args().skip_while(|val| !val.starts_with("--manifest-path"));
+
+    let mut cmd = cargo_metadata::MetadataCommand::new();
+    match args.next() {
+        Some(ref p) if p == "--manifest-path" => {
+            cmd.manifest_path(args.next().unwrap());
+        }
+        Some(p) => {
+            cmd.manifest_path(p.trim_start_matches("--manifest-path="));
+        }
+        None => {}
+    };
+
+    cmd.exec().map_err(|e| e.into())
+}
+
+fn select_root_crate(m: &cargo_metadata::Metadata) -> Result<&Package> {
+    if m.workspace_default_members.is_empty() {
+        return Err(anyhow!("can't create mlcfg file, no default workspace"));
+    }
+
+    // cargo metadata doesn't specify one particular crate.
+    // We consider that the first crate in the list of workspace_default_members will give the name of the file
+    let crate_id = &m.workspace_default_members[0];
+    let Some(package) = m.packages.iter().find(|p| &p.id == crate_id) else {
+        return Err(anyhow!("can't create mlcfg file, no default package"));
+    };
+
+    Ok(package)
+}
+
+pub(crate) fn make_mlcfg_filename(m: &cargo_metadata::Metadata) -> Result<PathBuf> {
+    let root_crate = select_root_crate(m)?;
+
+    // to specify the crate kind in the file name: lib, bin
+    if root_crate.targets.is_empty() || root_crate.targets[0].kind.is_empty() {
+        return Err(anyhow!("can't create mlcfg file, default package without target"));
+    }
+
+    let crate_type = &root_crate.targets[0].kind[0];
+    let filename = format!("{}-{}.mlcfg", root_crate.name, crate_type);
+
+    // put the file at the root of the target directory
+    Ok(m.target_directory.join(filename).into())
+}

cargo-creusot/src/main.rs

@@ -2,8 +2,15 @@ use creusot_args::options::*;
 use creusot_setup as setup;
 use std::{
     env,
+    path::PathBuf,
     process::{exit, Command},
 };
+use tempdir::TempDir;
+
+mod helpers;
+use helpers::*;
+mod why3_launcher;
+use why3_launcher::*;
 
 enum Subcommand {
     // subcommand to pass on to creusot-rustc
@@ -13,8 +20,20 @@ enum Subcommand {
 }
 use Subcommand::*;
 
-fn main() -> anyhow::Result<()> {
-    let cargs = CargoCreusotArgs::parse_from(std::env::args().skip(1));
+fn main() -> Result<()> {
+    let cargo_md = make_cargo_metadata()?;
+    let mlcfg_filename: PathBuf; //  mlcfg output file name container
+
+    let mut cargs = CargoCreusotArgs::parse_from(std::env::args().skip(1));
+
+    // select mlcfg output file name
+    if let Some(f) = &cargs.options.output_file {
+        mlcfg_filename = f.into();
+    } else {
+        mlcfg_filename = make_mlcfg_filename(&cargo_md)?;
+        cargs.options.output_file = Some(mlcfg_filename.to_string_lossy().into_owned());
+        cargs.options.span_mode = SpanMode::Absolute;
+    }
 
     let subcommand = match cargs.subcommand {
         None => Creusot(None),
@@ -24,15 +43,54 @@ fn main() -> anyhow::Result<()> {
 
     match subcommand {
         Creusot(subcmd) => {
+            // subcommand analysis:
+            //   we want to launch Why3 Ide in cargo-creusot not by creusot-rustc.
+            //   however we want to keep the current behavior for other commands: prove and replay
+            let (creusot_rustc_subcmd, launch_why3) = if let Some(CreusotSubCommand::Why3 {
+                command: Why3SubCommand::Ide,
+                ..
+            }) = subcmd
+            {
+                (None, true)
+            } else {
+                (subcmd, false)
+            };
+
             let config_args = setup::status_for_creusot(&cargs.config_dir)?;
             let creusot_args = CreusotArgs {
                 options: cargs.options,
-                why3_path: config_args.why3_path,
-                why3_config_file: config_args.why3_config,
-                subcommand: subcmd,
+                why3_path: config_args.why3_path.clone(),
+                why3_config_file: config_args.why3_config.clone(),
+                subcommand: creusot_rustc_subcmd.clone(),
                 rust_flags: cargs.rust_flags,
             };
-            Ok(invoke_cargo(&creusot_args))
+
+            invoke_cargo(&creusot_args);
+
+            if launch_why3 {
+                // why3 configuration
+                let mut b = Why3LauncherBuilder::new();
+                b.why3_path(config_args.why3_path);
+                if let Some(p) = &config_args.why3_config {
+                    b.config_file(p.clone());
+                }
+                b.output_file(mlcfg_filename);
+                // temporary: for the moment we only launch why3 via cargo-creusot in Ide mode
+                b.mode(Why3Mode::Ide);
+                if let Some(subcmd) = &creusot_rustc_subcmd {
+                    let CreusotSubCommand::Why3 { args, .. } = subcmd;
+                    b.args(args.clone());
+                }
+
+                let why3 = b.build()?;
+                let prelude_dir =
+                    TempDir::new("creusot_why3_prelude").expect("could not create temp dir");
+                let mut command = why3.make(prelude_dir.path())?;
+
+                command.status().expect("could not run why3");
+            }
+
+            Ok(())
         }
         Setup(SetupSubCommand::Status) => setup::status(&cargs.config_dir),
         Setup(SetupSubCommand::Install) => {

cargo-creusot/src/why3_launcher.rs

@@ -0,0 +1,125 @@
+use std::{
+    path::{Path, PathBuf},
+    process::Command,
+};
+
+use super::helpers::Result;
+use anyhow::anyhow;
+use include_dir::{include_dir, Dir};
+
+static PRELUDE: Dir<'static> = include_dir!("$CARGO_MANIFEST_DIR/../prelude");
+
+#[derive(Copy, Clone, Debug)]
+pub enum Why3Mode {
+    Ide,
+}
+
+impl std::fmt::Display for Why3Mode {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        match self {
+            Why3Mode::Ide => f.write_str("ide"),
+        }
+    }
+}
+
+#[derive(Debug)]
+pub struct Why3Launcher {
+    mode: Why3Mode,
+    why3_path: Option<PathBuf>,
+    config_file: Option<PathBuf>,
+    args: Option<String>,
+    output_file: PathBuf,
+}
+
+impl Why3Launcher {
+    pub fn new(
+        mode: Why3Mode,
+        why3_path: Option<PathBuf>,
+        config_file: Option<PathBuf>,
+        args: Option<String>,
+        output_file: PathBuf,
+    ) -> Self {
+        Self { mode, why3_path, config_file, args, output_file }
+    }
+
+    pub fn make(&self, temp_dir: &Path) -> Result<Command> {
+        let mode = self.mode.to_string();
+        PRELUDE.extract(temp_dir).expect("can't launch why3, could extract prelude into temp dir");
+
+        let mut command =
+            if let Some(p) = &self.why3_path { Command::new(p) } else { Command::new("why3") };
+        command
+            .args([
+                "--warn-off=unused_variable",
+                "--warn-off=clone_not_abstract",
+                "--warn-off=axiom_abstract",
+                &mode,
+                "-L",
+            ])
+            .arg(temp_dir.as_os_str())
+            .arg(&self.output_file);
+        if let Some(cfg) = &self.config_file {
+            command.arg("-C").arg(cfg);
+        }
+        if let Some(args) = &self.args {
+            if !args.is_empty() {
+                command.args(args.split_ascii_whitespace());
+            }
+        }
+
+        Ok(command)
+    }
+}
+
+pub struct Why3LauncherBuilder {
+    mode: Why3Mode,
+    why3_path: Option<PathBuf>,
+    config_file: Option<PathBuf>,
+    args: Option<String>,
+    output_file: Option<PathBuf>,
+}
+
+impl Why3LauncherBuilder {
+    pub fn new() -> Self {
+        Self {
+            mode: Why3Mode::Ide,
+            why3_path: None,
+            config_file: None,
+            args: None,
+            output_file: None,
+        }
+    }
+
+    pub fn mode(&mut self, m: Why3Mode) -> &mut Self {
+        self.mode = m;
+        self
+    }
+
+    pub fn why3_path(&mut self, p: PathBuf) -> &mut Self {
+        self.why3_path = Some(p);
+        self
+    }
+
+    pub fn config_file(&mut self, p: PathBuf) -> &mut Self {
+        self.config_file = Some(p);
+        self
+    }
+
+    pub fn args(&mut self, a: String) -> &mut Self {
+        self.args = Some(a);
+        self
+    }
+
+    pub fn output_file(&mut self, p: PathBuf) -> &mut Self {
+        self.output_file = Some(p);
+        self
+    }
+
+    pub fn build(self) -> Result<Why3Launcher> {
+        let Some(mlcfg_file) = self.output_file else {
+            return Err(anyhow!("can't launch why3, no mlcfg_file specify"));
+        };
+
+        Ok(Why3Launcher::new(self.mode, self.why3_path, self.config_file, self.args, mlcfg_file))
+    }
+}