diff --git a/charon/src/bin/charon-driver/driver.rs b/charon/src/bin/charon-driver/driver.rs index cd6c7bff..a105966b 100644 --- a/charon/src/bin/charon-driver/driver.rs +++ b/charon/src/bin/charon-driver/driver.rs @@ -1,7 +1,7 @@ -use crate::cli_options; use crate::translate::translate_crate_to_ullbc; -use charon_lib::cli_options::MirLevel; use charon_lib::export; +use charon_lib::options; +use charon_lib::options::MirLevel; use charon_lib::reorder_decls::compute_reordered_decls; use charon_lib::transform::{LLBC_PASSES, ULLBC_PASSES}; use charon_lib::ullbc_to_llbc; @@ -15,7 +15,7 @@ use std::panic::{self, AssertUnwindSafe}; /// The callbacks for Charon pub struct CharonCallbacks { - pub options: cli_options::CliOpts, + pub options: options::CliOpts, /// This is to be filled during the extraction pub crate_data: Option, pub error_count: usize, @@ -41,7 +41,7 @@ impl fmt::Display for CharonFailure { } impl CharonCallbacks { - pub fn new(options: cli_options::CliOpts) -> Self { + pub fn new(options: options::CliOpts) -> Self { Self { options, crate_data: None, diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs index 7e38ca04..ee76349c 100644 --- a/charon/src/bin/charon-driver/main.rs +++ b/charon/src/bin/charon-driver/main.rs @@ -32,8 +32,8 @@ use crate::driver::{ arg_values, get_args_crate_index, get_args_source_index, CharonCallbacks, CharonFailure, RunCompilerNormallyCallbacks, }; -use charon_lib::cli_options; use charon_lib::logger; +use charon_lib::options; use charon_lib::trace; fn main() { @@ -76,7 +76,7 @@ fn main() { // Retrieve the Charon options by deserializing them from the environment variable // (cargo-charon serialized the arguments and stored them in a specific environment // variable before calling cargo with RUSTC_WORKSPACE_WRAPPER=charon-driver). - let options: cli_options::CliOpts = match std::env::var(cli_options::CHARON_ARGS) { + let options: options::CliOpts = match std::env::var(options::CHARON_ARGS) { Ok(opts) => serde_json::from_str(opts.as_str()).unwrap(), Err(_) => { // Parse any arguments after `--` as charon arguments. @@ -84,7 +84,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 - cli_options::CliOpts::parse_from(charon_args) + options::CliOpts::parse_from(charon_args) } else { Default::default() } diff --git a/charon/src/bin/charon-driver/translate/get_mir.rs b/charon/src/bin/charon-driver/translate/get_mir.rs index 88ec4322..b4bf1ab6 100644 --- a/charon/src/bin/charon-driver/translate/get_mir.rs +++ b/charon/src/bin/charon-driver/translate/get_mir.rs @@ -1,7 +1,7 @@ //! Various utilities to load MIR. //! Allow to easily load the MIR code generated by a specific pass. -use crate::cli_options::MirLevel; +use crate::options::MirLevel; use rustc_hir::def_id::DefId; use rustc_middle::mir::Body; use rustc_middle::ty::TyCtxt; diff --git a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs index 2cea6da1..98e1ff9c 100644 --- a/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs +++ b/charon/src/bin/charon-driver/translate/translate_crate_to_ullbc.rs @@ -1,8 +1,8 @@ use super::get_mir::extract_constants_at_top_level; use super::translate_ctx::*; use charon_lib::ast::krate::*; -use charon_lib::cli_options::{CliOpts, MirLevel, TransOptions}; use charon_lib::common::*; +use charon_lib::options::{CliOpts, MirLevel, TransOptions}; use charon_lib::transform::TransformCtx; use hax_frontend_exporter as hax; diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs index d9b1727d..1c5d1ff3 100644 --- a/charon/src/bin/charon-driver/translate/translate_ctx.rs +++ b/charon/src/bin/charon-driver/translate/translate_ctx.rs @@ -2,10 +2,10 @@ use super::translate_predicates::NonLocalTraitClause; use super::translate_traits::ClauseTransCtx; use charon_lib::ast::*; -use charon_lib::cli_options::TransOptions; use charon_lib::common::*; use charon_lib::formatter::{FmtCtx, IntoFormatter}; use charon_lib::ids::{MapGenerator, Vector}; +use charon_lib::options::TransOptions; use charon_lib::ullbc_ast as ast; use hax_frontend_exporter as hax; use hax_frontend_exporter::SInto; @@ -23,7 +23,7 @@ use std::fmt; use std::path::Component; // Re-export to avoid having to fix imports. -pub(crate) use charon_lib::deps_errors::{ +pub(crate) use charon_lib::errors::{ error_assert, error_or_panic, register_error_or_panic, DepSource, ErrorCtx, }; diff --git a/charon/src/bin/charon/main.rs b/charon/src/bin/charon/main.rs index 4b7ffa03..dde5953c 100644 --- a/charon/src/bin/charon/main.rs +++ b/charon/src/bin/charon/main.rs @@ -32,15 +32,15 @@ // Don't link with the `charon_lib` crate so that the `charon` binary doesn't have to dynamically // link to `librustc_driver.so` etc. -#[path = "../../cli_options.rs"] -mod cli_options; #[path = "../../logger.rs"] mod logger; +#[path = "../../options.rs"] +mod options; mod toml_config; use anyhow::bail; use clap::Parser; -use cli_options::{CliOpts, CHARON_ARGS}; +use options::{CliOpts, CHARON_ARGS}; use serde::Deserialize; use std::env; use std::ffi::OsStr; diff --git a/charon/src/bin/charon/toml_config.rs b/charon/src/bin/charon/toml_config.rs index 8c0ef03e..64b02556 100644 --- a/charon/src/bin/charon/toml_config.rs +++ b/charon/src/bin/charon/toml_config.rs @@ -2,7 +2,7 @@ use serde::Deserialize; use std::path::PathBuf; -use crate::{cli_options::CliOpts, trace}; +use crate::{options::CliOpts, trace}; /// The struct used to define the options available in `Charon.toml` files. #[derive(Debug, Deserialize)] diff --git a/charon/src/deps_errors.rs b/charon/src/errors.rs similarity index 97% rename from charon/src/deps_errors.rs rename to charon/src/errors.rs index 02c3facc..d2c2d71b 100644 --- a/charon/src/deps_errors.rs +++ b/charon/src/errors.rs @@ -23,7 +23,7 @@ pub use register_error_or_panic; #[macro_export] macro_rules! error_or_panic { ($ctx:expr, $span:expr, $msg:expr) => {{ - $crate::deps_errors::register_error_or_panic!($ctx, $span, $msg); + $crate::errors::register_error_or_panic!($ctx, $span, $msg); let e = $crate::common::Error { span: $span, msg: $msg.to_string(), @@ -39,12 +39,12 @@ macro_rules! error_assert { ($ctx:expr, $span: expr, $b: expr) => { if !$b { let msg = format!("assertion failure: {:?}", stringify!($b)); - $crate::deps_errors::error_or_panic!($ctx, $span, msg); + $crate::errors::error_or_panic!($ctx, $span, msg); } }; ($ctx:expr, $span: expr, $b: expr, $msg: expr) => { if !$b { - $crate::deps_errors::error_or_panic!($ctx, $span, $msg); + $crate::errors::error_or_panic!($ctx, $span, $msg); } }; } diff --git a/charon/src/lib.rs b/charon/src/lib.rs index 90e22bb6..1e7c9917 100644 --- a/charon/src/lib.rs +++ b/charon/src/lib.rs @@ -35,10 +35,10 @@ pub mod ids; #[macro_use] pub mod logger; pub mod ast; -pub mod cli_options; pub mod common; -pub mod deps_errors; +pub mod errors; pub mod export; +pub mod options; pub mod pretty; pub mod transform; diff --git a/charon/src/cli_options.rs b/charon/src/options.rs similarity index 100% rename from charon/src/cli_options.rs rename to charon/src/options.rs diff --git a/charon/src/transform/ctx.rs b/charon/src/transform/ctx.rs index 95dc7cca..2b08221f 100644 --- a/charon/src/transform/ctx.rs +++ b/charon/src/transform/ctx.rs @@ -1,9 +1,9 @@ use crate::ast::*; -use crate::cli_options::TransOptions; -use crate::deps_errors::ErrorCtx; +use crate::errors::ErrorCtx; use crate::formatter::{FmtCtx, IntoFormatter}; use crate::ids::Vector; use crate::llbc_ast; +use crate::options::TransOptions; use crate::pretty::FmtWithCtx; use crate::ullbc_ast; use rustc_error_messages::MultiSpan; diff --git a/charon/src/transform/remove_dynamic_checks.rs b/charon/src/transform/remove_dynamic_checks.rs index 11016f79..df3559ad 100644 --- a/charon/src/transform/remove_dynamic_checks.rs +++ b/charon/src/transform/remove_dynamic_checks.rs @@ -4,7 +4,7 @@ //! compiling for release). In our case, we take this into account in the semantics of our //! array/slice manipulation and arithmetic functions, on the verification side. -use crate::deps_errors::register_error_or_panic; +use crate::errors::register_error_or_panic; use crate::formatter::IntoFormatter; use crate::llbc_ast::{BinOp, FieldProjKind, Operand, ProjectionElem, Rvalue}; use crate::pretty::FmtWithCtx; diff --git a/charon/src/transform/remove_read_discriminant.rs b/charon/src/transform/remove_read_discriminant.rs index 4901e943..c17a44ea 100644 --- a/charon/src/transform/remove_read_discriminant.rs +++ b/charon/src/transform/remove_read_discriminant.rs @@ -4,7 +4,7 @@ //! filtering). Then, we filter the unused variables ([crate::remove_unused_locals]). use crate::ast::*; -use crate::deps_errors::register_error_or_panic; +use crate::errors::register_error_or_panic; use crate::llbc_ast::*; use crate::transform::TransformCtx; use derive_visitor::visitor_enter_fn_mut;