diff --git a/charon/src/charon-driver.rs b/charon/src/charon-driver.rs index a8b78f558..3326a3a27 100644 --- a/charon/src/charon-driver.rs +++ b/charon/src/charon-driver.rs @@ -1,97 +1,13 @@ //! The Charon driver, which calls Rustc with callbacks to compile some Rust //! crate to LLBC. -#![allow(dead_code)] -#![feature(rustc_private, register_tool)] -#![feature(box_patterns)] -#![feature(cell_leak)] // For Ref::leak -// For rustdoc: prevents overflows -#![recursion_limit = "256"] -#![feature(trait_alias)] -#![feature(let_chains)] -#![feature(iterator_try_collect)] -#![feature(associated_type_defaults)] - -extern crate hashlink; -extern crate im; -extern crate linked_hash_set; -extern crate log; -extern crate rustc_abi; -extern crate rustc_ast; -extern crate rustc_ast_pretty; -extern crate rustc_attr; -extern crate rustc_borrowck; -extern crate rustc_const_eval; -extern crate rustc_driver; -extern crate rustc_error_messages; -extern crate rustc_errors; -extern crate rustc_hir; -extern crate rustc_index; -extern crate rustc_interface; -extern crate rustc_middle; -extern crate rustc_mir_dataflow; -extern crate rustc_mir_transform; -extern crate rustc_monomorphize; -extern crate rustc_resolve; -extern crate rustc_session; -extern crate rustc_span; -extern crate rustc_target; -extern crate take_mut; - -#[macro_use] -mod common; -mod assumed; -mod cli_options; -mod deps_errors; -mod driver; -mod export; -mod expressions; -mod expressions_utils; -mod formatter; -mod gast; -mod gast_utils; -mod get_mir; -mod graphs; -#[macro_use] -mod ids; -mod index_to_function_calls; -mod insert_assign_return_unit; -mod llbc_ast; -mod llbc_ast_utils; -mod logger; -mod meta; -mod meta_utils; -mod names; -mod names_utils; -mod ops_to_function_calls; -mod reconstruct_asserts; -mod remove_drop_never; -mod remove_dynamic_checks; -mod remove_nops; -mod remove_read_discriminant; -mod remove_unused_locals; -mod reorder_decls; -mod simplify_constants; -mod translate_constants; -mod translate_crate_to_ullbc; -mod translate_ctx; -mod translate_functions_to_ullbc; -mod translate_predicates; -mod translate_traits; -mod translate_types; -mod types; -mod types_utils; -mod ullbc_ast; -mod ullbc_ast_utils; -mod ullbc_to_llbc; -mod update_closure_signatures; -mod values; -mod values_utils; - -use crate::driver::{ +use charon_lib::cli_options; +use charon_lib::driver::{ arg_value, get_args_crate_index, get_args_source_index, CharonCallbacks, CharonFailure, }; -use crate::export::CrateData; +use charon_lib::export::CrateData; +use charon_lib::logger; +use charon_lib::trace; fn main() { // Initialize the logger diff --git a/charon/src/common.rs b/charon/src/common.rs index a2027d6f8..fa22cc60d 100644 --- a/charon/src/common.rs +++ b/charon/src/common.rs @@ -61,67 +61,3 @@ pub fn write_vec( ) -> std::result::Result<(), std::fmt::Error> { write_iterator(write_t, f, v.iter()) } - -/// This macro computes the name of the function in which it is called. -/// We adapted it from: -/// -/// Note that we can't define it in macros due to technical reasons -macro_rules! function_name { - () => {{ - fn f() {} - fn type_name_of(_: T) -> &'static str { - std::any::type_name::() - } - let name = type_name_of(f); - - // Remove the "::f" suffix - let name = &name[..name.len() - 3]; - - // Remove the CRATE::MODULE:: prefix - let name = match &name.find("::") { - Some(pos) => &name[pos + 2..name.len()], - None => name, - }; - - match &name.find("::") { - Some(pos) => &name[pos + 2..name.len()], - None => name, - } - }}; -} - -/// A custom log trace macro. Uses the log crate. -macro_rules! trace { - ($($arg:tt)+) => {{ - use colored::Colorize; - let msg = format!($($arg)+); - log::trace!("[{}]:\n{}", function_name!().yellow(), msg) - }}; - () => {{ - use colored::Colorize; - log::trace!("[{}]", function_name!().yellow()) - }}; -} - -/// A custom log error macro. Uses the log crate. -macro_rules! error { - ($($arg:tt)+) => {{ - use colored::Colorize; - let msg = format!($($arg)+); - log::error!("[{}]:\n{}", function_name!().red(), msg) - }}; -} - -/// A custom log info macro. Uses the log crate. -macro_rules! info { - ($($arg:tt)+) => {{ - use colored::Colorize; - let msg = format!($($arg)+); - // As for info we generally output simple messages, we don't insert - // a breakline - log::info!("[{}]: {}", function_name!().yellow(), msg) - }}; - () => {{ - log::info!("[{}]", function_name!().yellow()) - }}; -} diff --git a/charon/src/driver.rs b/charon/src/driver.rs index e439a3526..65762b287 100644 --- a/charon/src/driver.rs +++ b/charon/src/driver.rs @@ -1,21 +1,15 @@ use crate::cli_options; use crate::export; use crate::get_mir::MirLevel; -use crate::index_to_function_calls; -use crate::insert_assign_return_unit; -use crate::ops_to_function_calls; -use crate::reconstruct_asserts; -use crate::remove_drop_never; -use crate::remove_dynamic_checks; -use crate::remove_nops; -use crate::remove_read_discriminant; -use crate::remove_unused_locals; use crate::reorder_decls; -use crate::simplify_constants; +use crate::transform::{ + index_to_function_calls, insert_assign_return_unit, ops_to_function_calls, reconstruct_asserts, + remove_drop_never, remove_dynamic_checks, remove_nops, remove_read_discriminant, + remove_unused_locals, simplify_constants, update_closure_signatures, +}; use crate::translate_crate_to_ullbc; use crate::translate_ctx; use crate::ullbc_to_llbc; -use crate::update_closure_signatures; use regex::Regex; use rustc_driver::{Callbacks, Compilation}; use rustc_interface::{interface::Compiler, Queries}; diff --git a/charon/src/lib.rs b/charon/src/lib.rs index ecd8cd557..4423a6c3c 100644 --- a/charon/src/lib.rs +++ b/charon/src/lib.rs @@ -13,44 +13,30 @@ #![feature(rustc_private, register_tool)] #![feature(box_patterns)] -#![feature(cell_leak)] // For Ref::leak // For rustdoc: prevents overflows #![recursion_limit = "256"] #![feature(trait_alias)] #![feature(let_chains)] #![feature(iterator_try_collect)] -#![feature(associated_type_defaults)] -extern crate hashlink; -extern crate im; -extern crate linked_hash_set; -extern crate log; -extern crate rustc_abi; extern crate rustc_ast; extern crate rustc_ast_pretty; extern crate rustc_attr; -extern crate rustc_borrowck; -extern crate rustc_const_eval; extern crate rustc_driver; extern crate rustc_error_messages; -extern crate rustc_errors; extern crate rustc_hir; extern crate rustc_index; extern crate rustc_interface; extern crate rustc_middle; -extern crate rustc_mir_dataflow; -extern crate rustc_mir_transform; -extern crate rustc_monomorphize; -extern crate rustc_resolve; extern crate rustc_session; extern crate rustc_span; extern crate rustc_target; -extern crate take_mut; #[macro_use] -pub mod common; +pub mod logger; pub mod assumed; pub mod cli_options; +pub mod common; pub mod deps_errors; pub mod driver; pub mod export; @@ -63,24 +49,14 @@ pub mod get_mir; pub mod graphs; #[macro_use] pub mod ids; -pub mod index_to_function_calls; -pub mod insert_assign_return_unit; pub mod llbc_ast; pub mod llbc_ast_utils; -pub mod logger; pub mod meta; pub mod meta_utils; pub mod names; pub mod names_utils; -pub mod ops_to_function_calls; -pub mod reconstruct_asserts; -pub mod remove_drop_never; -pub mod remove_dynamic_checks; -pub mod remove_nops; -pub mod remove_read_discriminant; -pub mod remove_unused_locals; pub mod reorder_decls; -pub mod simplify_constants; +pub mod transform; pub mod translate_constants; pub mod translate_crate_to_ullbc; pub mod translate_ctx; @@ -93,6 +69,5 @@ pub mod types_utils; pub mod ullbc_ast; pub mod ullbc_ast_utils; pub mod ullbc_to_llbc; -pub mod update_closure_signatures; pub mod values; pub mod values_utils; diff --git a/charon/src/logger.rs b/charon/src/logger.rs index a21a280e0..2d04c83d2 100644 --- a/charon/src/logger.rs +++ b/charon/src/logger.rs @@ -52,3 +52,71 @@ pub fn initialize_logger() { builder.init(); } + +/// This macro computes the name of the function in which it is called. +/// We adapted it from: +/// +/// Note that we can't define it in macros due to technical reasons +#[macro_export] +macro_rules! function_name { + () => {{ + fn f() {} + fn type_name_of(_: T) -> &'static str { + std::any::type_name::() + } + let name = type_name_of(f); + + // Remove the "::f" suffix + let name = &name[..name.len() - 3]; + + // Remove the CRATE::MODULE:: prefix + let name = match &name.find("::") { + Some(pos) => &name[pos + 2..name.len()], + None => name, + }; + + match &name.find("::") { + Some(pos) => &name[pos + 2..name.len()], + None => name, + } + }}; +} + +/// A custom log trace macro. Uses the log crate. +#[macro_export] +macro_rules! trace { + ($($arg:tt)+) => {{ + use colored::Colorize; + let msg = format!($($arg)+); + log::trace!("[{}]:\n{}", $crate::function_name!().yellow(), msg) + }}; + () => {{ + use colored::Colorize; + log::trace!("[{}]", $crate::function_name!().yellow()) + }}; +} + +/// A custom log error macro. Uses the log crate. +#[macro_export] +macro_rules! error { + ($($arg:tt)+) => {{ + use colored::Colorize; + let msg = format!($($arg)+); + log::error!("[{}]:\n{}", $crate::function_name!().red(), msg) + }}; +} + +/// A custom log info macro. Uses the log crate. +#[macro_export] +macro_rules! info { + ($($arg:tt)+) => {{ + use colored::Colorize; + let msg = format!($($arg)+); + // As for info we generally output simple messages, we don't insert + // a breakline + log::info!("[{}]: {}", $crate::function_name!().yellow(), msg) + }}; + () => {{ + log::info!("[{}]", $crate::function_name!().yellow()) + }}; +} diff --git a/charon/src/main.rs b/charon/src/main.rs index 2458063fb..5fc102c8d 100644 --- a/charon/src/main.rs +++ b/charon/src/main.rs @@ -32,13 +32,9 @@ #![cfg_attr(feature = "deny-warnings", deny(warnings))] -extern crate rustc_tools_util; - -mod cli_options; -mod logger; - +use charon_lib::cli_options::{CliOpts, CHARON_ARGS}; +use charon_lib::logger; use clap::Parser; -use cli_options::{CliOpts, CHARON_ARGS}; use log::trace; use std::env; use std::path::PathBuf; diff --git a/charon/src/index_to_function_calls.rs b/charon/src/transform/index_to_function_calls.rs similarity index 100% rename from charon/src/index_to_function_calls.rs rename to charon/src/transform/index_to_function_calls.rs diff --git a/charon/src/insert_assign_return_unit.rs b/charon/src/transform/insert_assign_return_unit.rs similarity index 100% rename from charon/src/insert_assign_return_unit.rs rename to charon/src/transform/insert_assign_return_unit.rs diff --git a/charon/src/transform/mod.rs b/charon/src/transform/mod.rs new file mode 100644 index 000000000..ae2e8f860 --- /dev/null +++ b/charon/src/transform/mod.rs @@ -0,0 +1,11 @@ +pub mod index_to_function_calls; +pub mod insert_assign_return_unit; +pub mod ops_to_function_calls; +pub mod reconstruct_asserts; +pub mod remove_drop_never; +pub mod remove_dynamic_checks; +pub mod remove_nops; +pub mod remove_read_discriminant; +pub mod remove_unused_locals; +pub mod simplify_constants; +pub mod update_closure_signatures; diff --git a/charon/src/ops_to_function_calls.rs b/charon/src/transform/ops_to_function_calls.rs similarity index 100% rename from charon/src/ops_to_function_calls.rs rename to charon/src/transform/ops_to_function_calls.rs diff --git a/charon/src/reconstruct_asserts.rs b/charon/src/transform/reconstruct_asserts.rs similarity index 100% rename from charon/src/reconstruct_asserts.rs rename to charon/src/transform/reconstruct_asserts.rs diff --git a/charon/src/remove_drop_never.rs b/charon/src/transform/remove_drop_never.rs similarity index 100% rename from charon/src/remove_drop_never.rs rename to charon/src/transform/remove_drop_never.rs diff --git a/charon/src/remove_dynamic_checks.rs b/charon/src/transform/remove_dynamic_checks.rs similarity index 100% rename from charon/src/remove_dynamic_checks.rs rename to charon/src/transform/remove_dynamic_checks.rs diff --git a/charon/src/remove_nops.rs b/charon/src/transform/remove_nops.rs similarity index 100% rename from charon/src/remove_nops.rs rename to charon/src/transform/remove_nops.rs diff --git a/charon/src/remove_read_discriminant.rs b/charon/src/transform/remove_read_discriminant.rs similarity index 100% rename from charon/src/remove_read_discriminant.rs rename to charon/src/transform/remove_read_discriminant.rs diff --git a/charon/src/remove_unused_locals.rs b/charon/src/transform/remove_unused_locals.rs similarity index 100% rename from charon/src/remove_unused_locals.rs rename to charon/src/transform/remove_unused_locals.rs diff --git a/charon/src/simplify_constants.rs b/charon/src/transform/simplify_constants.rs similarity index 100% rename from charon/src/simplify_constants.rs rename to charon/src/transform/simplify_constants.rs diff --git a/charon/src/update_closure_signatures.rs b/charon/src/transform/update_closure_signatures.rs similarity index 100% rename from charon/src/update_closure_signatures.rs rename to charon/src/transform/update_closure_signatures.rs diff --git a/charon/src/translate_ctx.rs b/charon/src/translate_ctx.rs index d2b95d99b..27a0902dd 100644 --- a/charon/src/translate_ctx.rs +++ b/charon/src/translate_ctx.rs @@ -26,21 +26,27 @@ use std::cmp::{Ord, Ordering, PartialOrd}; use std::collections::{BTreeSet, HashMap, HashSet, VecDeque}; use std::fmt; -/// Macro to either panic or return on error, depending on the CLI options -macro_rules! error_or_panic { +macro_rules! register_error_or_panic { ($ctx:expr, $span: expr, $msg: expr) => {{ $ctx.span_err($span, &$msg); - if $ctx.continue_on_failure() { - let e = crate::common::Error { - span: $span, - msg: $msg.to_string(), - }; - return (Err(e)); - } else { + if !$ctx.continue_on_failure() { panic!("{}", $msg); } }}; } +pub(crate) use register_error_or_panic; + +/// Macro to either panic or return on error, depending on the CLI options +macro_rules! error_or_panic { + ($ctx:expr, $span:expr, $msg:expr) => {{ + $crate::translate_ctx::register_error_or_panic!($ctx, $span, $msg); + let e = crate::common::Error { + span: $span, + msg: $msg.to_string(), + }; + return Err(e); + }}; +} pub(crate) use error_or_panic; /// Custom assert to either panic or return an error @@ -48,27 +54,12 @@ macro_rules! error_assert { ($ctx:expr, $span: expr, $b: expr) => { if !$b { let msg = format!("assertion failure: {:?}", stringify!($b)); - $ctx.span_err($span, &msg); - if $ctx.continue_on_failure() { - let e = crate::common::Error { span: $span, msg }; - return (Err(e)); - } else { - panic!("{}", msg); - } + $crate::translate_ctx::error_or_panic!($ctx, $span, msg); } }; ($ctx:expr, $span: expr, $b: expr, $msg: expr) => { if !$b { - $ctx.span_err($span, &$msg); - if $ctx.continue_on_failure() { - let e = crate::common::Error { - span: $span, - msg: $msg.to_string(), - }; - return (Err(e)); - } else { - panic!("{}", $msg); - } + $crate::translate_ctx::error_or_panic!($ctx, $span, $msg); } }; } @@ -79,44 +70,19 @@ macro_rules! error_assert_then { ($ctx:expr, $span: expr, $b: expr, $then: expr) => { if !$b { let msg = format!("assertion failure: {:?}", stringify!($b)); - $ctx.span_err($span.rust_span_data.span(), &msg); - if $ctx.continue_on_failure() { - { - $then - } - } else { - panic!("{}", msg); - } + $crate::translate_ctx::register_error_or_panic!($ctx, $span, msg); + $then; } }; ($ctx:expr, $span: expr, $b: expr, $then: expr, $msg:expr) => { if !$b { - $ctx.span_err($span.rust_span_data.span(), &$msg); - if $ctx.continue_on_failure() { - { - $then - } - } else { - panic!("{}", $msg); - } + $crate::translate_ctx::register_error_or_panic!($ctx, $span, $msg); + $then; } }; } pub(crate) use error_assert_then; -macro_rules! register_error_or_panic { - ($ctx:expr, $span: expr, $msg: expr) => {{ - $ctx.span_err($span, &$msg); - if $ctx.continue_on_failure() { - // Nothing to do - (); - } else { - panic!("{}", $msg); - } - }}; -} -pub(crate) use register_error_or_panic; - /// We use this to save the origin of an id. This is useful for the external /// dependencies, especially if some external dependencies don't extract: /// we use this information to tell the user what is the code which diff --git a/charon/tests/ui/binop-simplifications.out b/charon/tests/ui/binop-simplifications.out index f2943cc84..eb6dc4d40 100644 --- a/charon/tests/ui/binop-simplifications.out +++ b/charon/tests/ui/binop-simplifications.out @@ -1,4 +1,4 @@ -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: fn test_crate::neg_test(@1: i32) -> i32 { diff --git a/charon/tests/ui/closures.out b/charon/tests/ui/closures.out index f65c058f3..0cd2f6414 100644 --- a/charon/tests/ui/closures.out +++ b/charon/tests/ui/closures.out @@ -1,4 +1,4 @@ -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: fn test_crate::incr_u32(@1: u32) -> u32 { diff --git a/charon/tests/ui/issue-114-opaque-bodies.out b/charon/tests/ui/issue-114-opaque-bodies.out index 2d00f6510..dcbd57611 100644 --- a/charon/tests/ui/issue-114-opaque-bodies.out +++ b/charon/tests/ui/issue-114-opaque-bodies.out @@ -1,4 +1,4 @@ -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: fn issue_114_opaque_bodies_aux::inline_always() -> u32 { diff --git a/charon/tests/ui/issue-118-generic-copy.out b/charon/tests/ui/issue-118-generic-copy.out index ca049cfa4..55632e90c 100644 --- a/charon/tests/ui/issue-118-generic-copy.out +++ b/charon/tests/ui/issue-118-generic-copy.out @@ -1,4 +1,4 @@ -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: struct test_crate::Foo = {} diff --git a/charon/tests/ui/issue-4-traits.out b/charon/tests/ui/issue-4-traits.out index 41b3e170b..63cc8ab06 100644 --- a/charon/tests/ui/issue-4-traits.out +++ b/charon/tests/ui/issue-4-traits.out @@ -1,4 +1,4 @@ -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: enum core::result::Result = | Ok(T) diff --git a/charon/tests/ui/issue-45-misc.out b/charon/tests/ui/issue-45-misc.out index 1f9654323..c955af94d 100644 --- a/charon/tests/ui/issue-45-misc.out +++ b/charon/tests/ui/issue-45-misc.out @@ -1,4 +1,4 @@ -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: fn test_crate::map::closure<'_0>(@1: &'_0 mut (()), @2: (i32)) -> i32 { diff --git a/charon/tests/ui/issue-72-hash-missing-impl.out b/charon/tests/ui/issue-72-hash-missing-impl.out index 0b4b97bfb..d8f8d8608 100644 --- a/charon/tests/ui/issue-72-hash-missing-impl.out +++ b/charon/tests/ui/issue-72-hash-missing-impl.out @@ -1,4 +1,4 @@ -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: trait test_crate::Hasher diff --git a/charon/tests/ui/issue-73-extern.out b/charon/tests/ui/issue-73-extern.out index 7ba5040e7..578b51e31 100644 --- a/charon/tests/ui/issue-73-extern.out +++ b/charon/tests/ui/issue-73-extern.out @@ -1,4 +1,4 @@ -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: unsafe fn test_crate::foo(@1: i32) diff --git a/charon/tests/ui/issue-92-nonpositive-variant-indices.out b/charon/tests/ui/issue-92-nonpositive-variant-indices.out index 549590b98..8e079c97c 100644 --- a/charon/tests/ui/issue-92-nonpositive-variant-indices.out +++ b/charon/tests/ui/issue-92-nonpositive-variant-indices.out @@ -1,4 +1,4 @@ -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: enum test_crate::Ordering = | Less() diff --git a/charon/tests/ui/issue-97-missing-parent-item-clause.out b/charon/tests/ui/issue-97-missing-parent-item-clause.out index 90e3c0187..12ca32023 100644 --- a/charon/tests/ui/issue-97-missing-parent-item-clause.out +++ b/charon/tests/ui/issue-97-missing-parent-item-clause.out @@ -1,4 +1,4 @@ -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: trait test_crate::Ord diff --git a/charon/tests/ui/unsupported/option-is_some.out b/charon/tests/ui/unsupported/option-is_some.out index 83e6d000f..4689fb253 100644 --- a/charon/tests/ui/unsupported/option-is_some.out +++ b/charon/tests/ui/unsupported/option-is_some.out @@ -1,7 +1,7 @@ error: A discriminant read must be followed by a `SwitchInt` --> /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs:598:5 -[ INFO charon_driver::driver:338] [translate]: # Final LLBC before serialization: +[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization: enum core::option::Option = | None() @@ -39,4 +39,4 @@ error: The external definition DefId(2:7981 ~ core[6c80]::option::{impl#0}::is_s error: aborting due to 2 previous errors -[ ERROR charon_driver:264] The extraction encountered 1 errors +[ ERROR charon_driver:180] The extraction encountered 1 errors