Merge pull request #130 from AeneasVerif/cleanup

Some clean-ups

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

charon/src/common.rs

@@ -61,67 +61,3 @@ pub fn write_vec<T>(
 ) -> 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:
-/// <https://stackoverflow.com/questions/38088067/equivalent-of-func-or-function-in-rust>
-/// Note that we can't define it in macros due to technical reasons
-macro_rules! function_name {
-    () => {{
-        fn f() {}
-        fn type_name_of<T>(_: T) -> &'static str {
-            std::any::type_name::<T>()
-        }
-        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())
-    }};
-}

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};

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;

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:
+/// <https://stackoverflow.com/questions/38088067/equivalent-of-func-or-function-in-rust>
+/// 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>(_: T) -> &'static str {
+            std::any::type_name::<T>()
+        }
+        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())
+    }};
+}

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;

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;