Merge pull request #596 from os-checker/subcommand/pretty-print

feat: add pretty-print subcommand

Author: Nadrieril

charon/src/bin/charon-driver/main.rs

@@ -90,7 +90,7 @@ fn main() {
                 use clap::Parser;
                 let mut charon_args = compiler_args.split_off(i);
                 charon_args[0] = origin_args[0].clone(); // Replace `--` with the name of the binary
-                options::CliOpts::parse_from(charon_args)
+                options::OldCliOpts::parse_from(charon_args).opts
             } else {
                 Default::default()
             }

charon/src/bin/charon/cli_rework/mod.rs

@@ -0,0 +1,27 @@
+use charon_lib::options::CliOpts;
+use clap::{Args, Parser, Subcommand};
+use std::path::PathBuf;
+
+#[derive(Debug, Parser)]
+#[clap(name = "Charon")]
+pub struct Cli {
+    // Makes CliOpts parsable.
+    // This should be removed once subcommands are fully implemented.
+    #[command(flatten)]
+    pub opts: CliOpts,
+
+    #[command(subcommand)]
+    pub command: Option<Charon>,
+}
+
+#[derive(Debug, Subcommand)]
+pub enum Charon {
+    PrettyPrint(PrettyPrintArgs),
+}
+
+/// Read a llbc or ullbc file and pretty print it.
+#[derive(Args, Debug)]
+pub struct PrettyPrintArgs {
+    /// Single file path to llbc or ullbc
+    pub file: PathBuf,
+}

charon/src/bin/charon/main.rs

@@ -35,7 +35,7 @@
 
 use anyhow::bail;
 use clap::Parser;
-use options::{CliOpts, CHARON_ARGS};
+use options::CHARON_ARGS;
 use serde::Deserialize;
 use std::env;
 use std::ffi::OsStr;
@@ -47,6 +47,8 @@ use charon_lib::logger;
 use charon_lib::options;
 use charon_lib::trace;
 
+/// Rename this module once subcommand migration finishes.
+mod cli_rework;
 mod toml_config;
 
 // Store the toolchain details directly in the binary.
@@ -158,8 +160,21 @@ pub fn main() -> anyhow::Result<()> {
     // Initialize the logger
     logger::initialize_logger();
 
+    let cli = cli_rework::Cli::parse();
+
+    match cli.command {
+        Some(cli_rework::Charon::PrettyPrint(pretty_print)) => {
+            let krate = charon_lib::deserialize_llbc(&pretty_print.file)?;
+            println!("{krate}");
+            return Ok(());
+        }
+        _ => (),
+    }
+
+    // ******* Old cli args parsing *******
+
     // Parse the command-line
-    let mut options = CliOpts::parse();
+    let mut options = cli.opts;
     trace!("Arguments: {:?}", std::env::args());
     options.validate();
 

charon/src/options.rs

@@ -1,5 +1,4 @@
 //! The options that control charon behavior.
-use clap::Parser;
 use indoc::indoc;
 use serde::{Deserialize, Serialize};
 use std::path::PathBuf;
@@ -10,6 +9,15 @@ use crate::{ast::*, errors::ErrorCtx, name_matcher::NamePattern, raise_error, re
 /// when calling charon-driver from cargo-charon.
 pub const CHARON_ARGS: &str = "CHARON_ARGS";
 
+// Makes CliOpts parsable. This should be removed once subcommands are fully implemented.
+#[derive(Debug, clap::Parser)]
+#[clap(name = "Charon")]
+#[charon::rename("cli_options")]
+pub struct OldCliOpts {
+    #[command(flatten)]
+    pub opts: CliOpts,
+}
+
 // This structure is used to store the command-line instructions.
 // We automatically derive a command-line parser based on this structure.
 // Note that the doc comments are used to generate the help message when using
@@ -18,7 +26,7 @@ pub const CHARON_ARGS: &str = "CHARON_ARGS";
 // Note that because we need to transmit the options to the charon driver,
 // we store them in a file before calling this driver (hence the `Serialize`,
 // `Deserialize` options).
-#[derive(Debug, Default, Clone, Parser, Serialize, Deserialize)]
+#[derive(Debug, Default, Clone, clap::Args, Serialize, Deserialize)]
 #[clap(name = "Charon")]
 #[charon::rename("cli_options")]
 pub struct CliOpts {

charon/tests/cli.rs

@@ -0,0 +1,63 @@
+use anyhow::{ensure, Context, Result};
+use assert_cmd::prelude::CommandCargoExt;
+use itertools::Itertools;
+use std::process::Command;
+
+fn charon<T>(args: &[&str], f: impl FnOnce(String) -> Result<T>) -> Result<T> {
+    let cmd_str = || {
+        std::iter::once("charon")
+            .chain(args.iter().copied())
+            .join(" ")
+    };
+
+    let mut cmd = Command::cargo_bin("charon")?;
+    let output = cmd.args(args).output()?;
+    let stdout = String::from_utf8(output.stdout).with_context(|| {
+        format!(
+            "`{}`:\nthe content of stdout is not UTF8 encoded.",
+            cmd_str()
+        )
+    })?;
+    let stderr = String::from_utf8(output.stderr).with_context(|| {
+        format!(
+            "`{}`:\nthe content of stderr is not UTF8 encoded.",
+            cmd_str()
+        )
+    })?;
+
+    let status = output.status;
+    ensure!(
+        status.success(),
+        "Error when executing `{}`:\nstderr={stderr:?}\nstdout={stdout:?}",
+        cmd_str()
+    );
+
+    f(stdout)
+}
+
+#[test]
+fn charon_pretty_print() -> Result<()> {
+    // charon --rustc-flag=--crate-type=rlib --no-cargo --input tests/ui/arrays.rs
+    charon(
+        &[
+            "--rustc-flag=--crate-type=rlib",
+            "--no-cargo",
+            "--input",
+            "tests/ui/arrays.rs",
+        ],
+        |_| {
+            // arrays.llbc is generated
+            let llbc = "arrays.llbc";
+            ensure!(std::fs::exists(llbc)?, "{llbc} doesn't exist!");
+
+            charon(&["pretty-print", llbc], |stdout| {
+                let search = "pub fn arrays::";
+                ensure!(
+                    stdout.contains(search),
+                    "Output of pretty-printing {llbc} is:\n{stdout:?}\nIt doesn't contain {search:?}."
+                );
+                Ok(())
+            })
+        },
+    )
+}