Merge pull request #1104 from oliver-butterley/config-file-updates

feat: refactor Charon.toml to use Cargo.toml and add support for start_from, hide_marker_traits

Author: Nadrieril

charon/src/bin/charon/cli.rs

@@ -13,7 +13,8 @@ pub struct Cli {
 pub enum Charon {
     /// Runs charon on a single rust file (and the modules it references, if any).
     Rustc(RustcArgs),
-    /// Runs charon on a cargo project.
+    /// Runs charon on a cargo project. If a `[package.metadata.charon]` section is present in
+    /// `Cargo.toml`, options are also read from it.
     Cargo(CargoArgs),
     /// Print the path to the rustc toolchain used by charon.
     ToolchainPath(ToolchainPathArgs),

charon/src/bin/charon/toml_config.rs

@@ -1,29 +1,31 @@
-//! Processing of the contents of a `Charon.toml` file.
+//! Processing of the contents of `[package.metadata.charon]` in `Cargo.toml`.
 use charon_lib::options::CliOpts;
 use serde::Deserialize;
-use std::path::PathBuf;
 
-/// The struct used to define the options available in `Charon.toml` files.
+/// The struct used to define the options available under `[package.metadata.charon]` in
+/// `Cargo.toml`. These all mirror the corresponding cli option.
 #[derive(Debug, Deserialize)]
 pub struct TomlConfig {
     #[serde(default)]
-    pub charon: CharonTomlConfig,
+    pub extract_opaque_bodies: bool,
     #[serde(default)]
-    pub rustc: RustcTomlConfig,
-}
-
-/// The struct used to define the options available in `Charon.toml` files. These all mirror the
-/// corresponding cli option.
-#[derive(Debug, Default, Deserialize)]
-pub struct CharonTomlConfig {
+    pub start_from: Vec<String>,
     #[serde(default)]
-    pub extract_opaque_bodies: bool,
+    pub start_from_if_exists: Vec<String>,
+    #[serde(default)]
+    pub start_from_attribute: Option<String>,
+    #[serde(default)]
+    pub start_from_pub: bool,
+    #[serde(default)]
+    pub hide_marker_traits: bool,
     #[serde(default)]
     pub include: Vec<String>,
     #[serde(default)]
     pub opaque: Vec<String>,
     #[serde(default)]
     pub exclude: Vec<String>,
+    #[serde(default)]
+    pub rustc: RustcTomlConfig,
 }
 
 #[derive(Debug, Default, Deserialize)]
@@ -36,23 +38,29 @@ impl TomlConfig {
     /// Applies the options specified in the toml file to the cli options. In case of conflict, cli
     /// options take precedence.
     pub(crate) fn apply(self, mut config: CliOpts) -> CliOpts {
-        config.extract_opaque_bodies |= self.charon.extract_opaque_bodies;
-        config.include.extend(self.charon.include);
-        config.opaque.extend(self.charon.opaque);
-        config.exclude.extend(self.charon.exclude);
+        config.extract_opaque_bodies |= self.extract_opaque_bodies;
+        config.start_from.extend(self.start_from);
+        config
+            .start_from_if_exists
+            .extend(self.start_from_if_exists);
+        if config.start_from_attribute.is_none() {
+            config.start_from_attribute = self.start_from_attribute;
+        }
+        config.start_from_pub |= self.start_from_pub;
+        config.hide_marker_traits |= self.hide_marker_traits;
+        config.include.extend(self.include);
+        config.opaque.extend(self.opaque);
+        config.exclude.extend(self.exclude);
         config.rustc_args.extend(self.rustc.flags);
         config
     }
 }
 
-/// Read `./Charon.toml` if there is such a file.
+/// Read `[package.metadata.charon]` from `./Cargo.toml` if present.
 pub(crate) fn read_toml() -> Option<TomlConfig> {
-    trace!("Reading options from the `Charon.toml` file");
-    let path = PathBuf::from("./Charon.toml");
-    if path.exists() {
-        let contents = std::fs::read_to_string(path).unwrap();
-        Some(toml::from_str(&contents).unwrap())
-    } else {
-        None
-    }
+    trace!("Reading options from `[package.metadata.charon]` in `Cargo.toml`");
+    let contents = std::fs::read_to_string("./Cargo.toml").ok()?;
+    let full: toml::Value = toml::from_str(&contents).ok()?;
+    let charon_meta = full.get("package")?.get("metadata")?.get("charon")?.clone();
+    Some(charon_meta.try_into().unwrap())
 }

charon/tests/cargo/toml.out

@@ -49,8 +49,8 @@ fn UNIT_METADATA()
 // Full name: UNIT_METADATA
 const UNIT_METADATA: () = UNIT_METADATA()
 
-// Full name: test_cargo_toml::main
-fn main()
+// Full name: test_cargo_toml::included::run
+pub fn run()
 {
     let _0: (); // return
     let _1: bool; // anonymous local

charon/tests/cargo/toml/Cargo.toml

@@ -5,3 +5,10 @@ name = "test-cargo-toml"
 version = "0.1.0"
 authors = ["Son Ho <hosonmarc@gmail.com>"]
 edition = "2021"
+
+[package.metadata.charon]
+extract_opaque_bodies = true
+start_from = ["crate::included"]
+
+[package.metadata.charon.rustc]
+flags = ["--cfg", "abc"]

charon/tests/cargo/toml/Charon.toml

@@ -1,7 +1,23 @@
 #![allow(unexpected_cfgs)]
-// The `cfg` is here to test that we correctly passed rustc flags from the `Charon.toml`. The call
-// to `is_some` is here to exercice the `extract_opaque_bodies` option.
+
+// `[cfg(abc)]` is here to test that we correctly passed rustc flags from `[package.metadata.charon.rustc]`:
+// without `--cfg abc`, `main` does not exist and the build fails.
+// The call to `is_some` exercises the `extract_opaque_bodies` option.
+#[cfg(abc)]
+pub mod included {
+    pub fn run() {
+        let _ = Some(false).is_some();
+    }
+}
+
+// Must NOT appear in the output: `start_from = ["crate::included"]` filters this out.
+pub mod excluded {
+    pub fn unreachable() -> u32 {
+        42
+    }
+}
+
 #[cfg(abc)]
 fn main() {
-    let _ = Some(false).is_some();
+    included::run();
 }

charon/tests/cargo/toml/src/main.rs

@@ -9,15 +9,9 @@ provides various options and flags to tweak its behaviour: you can display a
 detailed documentation with `--help`.
 In particular, you can pretty-print the translated crate with both `--print-ullbc` and `--print-llbc`, depending on the Charon intermediate representation you wish to use.
 
-If there is a `Charon.toml` file at the root of your project, `charon` will also take options from it.
-The file supports the same options at the cli interface, except for the options that relate to
-input/output like `--print-llbc`. Example `Charon.toml`:
-```toml
-[charon]
-extract_opaque_bodies = true
-[rustc]
-flags = ["--cfg", "abc"]
-```
+Charon supports per-crate configuration via the `[package.metadata.charon]` section in `Cargo.toml`. 
+The exact list can be found by looking at `src/bin/charon/toml_config.rs`. 
+If an option is set both as a CLI flag and as a toml value and we can't merge them, the CLI flag wins.
 
 **Remark**: because Charon is compiled with Rust nightly (this is a requirement to implement a rustc
 driver), it will build your crate with Rust nightly. You can find the nightly version pinned for