charon_driver/
main.rs

1//! The Charon driver, which calls Rustc with callbacks to compile some Rust
2//! crate to LLBC.
3#![feature(rustc_private)]
4#![allow(clippy::useless_format)]
5#![allow(clippy::manual_map)]
6#![allow(clippy::mem_replace_with_default)]
7#![allow(clippy::derivable_impls)]
8#![allow(clippy::borrowed_box)]
9#![allow(clippy::field_reassign_with_default)]
10#![expect(incomplete_features)]
11#![feature(box_patterns)]
12#![feature(deref_patterns)]
13#![feature(if_let_guard)]
14#![feature(iter_array_chunks)]
15#![feature(iterator_try_collect)]
16#![feature(macro_metavar_expr)]
17#![feature(sized_hierarchy)]
18#![feature(trait_alias)]
19#![feature(type_changing_struct_update)]
20
21extern crate rustc_abi;
22extern crate rustc_apfloat;
23extern crate rustc_ast;
24extern crate rustc_ast_pretty;
25extern crate rustc_const_eval;
26extern crate rustc_data_structures;
27extern crate rustc_driver;
28extern crate rustc_error_messages;
29extern crate rustc_errors;
30extern crate rustc_hashes;
31extern crate rustc_hir;
32extern crate rustc_hir_analysis;
33extern crate rustc_index;
34extern crate rustc_infer;
35extern crate rustc_interface;
36extern crate rustc_lexer;
37extern crate rustc_middle;
38extern crate rustc_mir_build;
39extern crate rustc_session;
40extern crate rustc_span;
41extern crate rustc_target;
42extern crate rustc_trait_selection;
43extern crate rustc_type_ir;
44
45#[macro_use]
46extern crate charon_lib;
47
48mod driver;
49#[macro_use]
50pub mod hax;
51mod translate;
52
53use charon_lib::{
54    export, logger,
55    options::CliOpts,
56    transform::{
57        FINAL_CLEANUP_PASSES, INITIAL_CLEANUP_PASSES, LLBC_PASSES, Pass, PrintCtxPass,
58        SHARED_FINALIZING_PASSES, ULLBC_PASSES,
59    },
60};
61use std::{fmt, panic};
62
63pub enum CharonFailure {
64    /// The usize is the number of errors.
65    CharonError(usize),
66    RustcError,
67    Panic,
68    Serialize,
69}
70
71impl fmt::Display for CharonFailure {
72    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
73        match self {
74            CharonFailure::RustcError => write!(f, "Code failed to compile")?,
75            CharonFailure::CharonError(err_count) => write!(
76                f,
77                "Charon failed to translate this code ({err_count} errors)"
78            )?,
79            CharonFailure::Panic => write!(f, "Compilation panicked")?,
80            CharonFailure::Serialize => write!(f, "Could not serialize output file")?,
81        }
82        Ok(())
83    }
84}
85
86/// Calculate the list of passes we will run on the crate before outputting it.
87pub fn transformation_passes(options: &CliOpts) -> Vec<Pass> {
88    let mut passes: Vec<Pass> = vec![];
89
90    passes.push(Pass::NonBody(PrintCtxPass::new(
91        options.print_original_ullbc,
92        "# ULLBC after translation from MIR".to_string(),
93    )));
94
95    passes.extend(INITIAL_CLEANUP_PASSES);
96    passes.extend(ULLBC_PASSES);
97
98    if !options.ullbc {
99        // If we're reconstructing control-flow, print the ullbc here.
100        passes.push(Pass::NonBody(PrintCtxPass::new(
101            options.print_ullbc,
102            "# Final ULLBC before control-flow reconstruction".to_string(),
103        )));
104    }
105
106    if !options.ullbc {
107        passes.extend(LLBC_PASSES);
108    }
109    passes.extend(SHARED_FINALIZING_PASSES);
110
111    if options.ullbc {
112        // If we're not reconstructing control-flow, print the ullbc after finalizing passes.
113        passes.push(Pass::NonBody(PrintCtxPass::new(
114            options.print_ullbc,
115            "# Final ULLBC before serialization".to_string(),
116        )));
117    } else {
118        passes.push(Pass::NonBody(PrintCtxPass::new(
119            options.print_llbc,
120            "# Final LLBC before serialization".to_string(),
121        )));
122    }
123
124    // Run the final passes after pretty-printing so that we get some output even if check_generics
125    // fails.
126    passes.extend(FINAL_CLEANUP_PASSES);
127    passes
128}
129
130/// Run charon. Returns the number of warnings generated.
131fn run_charon() -> Result<usize, CharonFailure> {
132    // Run the driver machinery.
133    let Some((mut ctx, options)) = driver::run_rustc_driver()? else {
134        // We didn't run charon.
135        return Ok(0);
136    };
137
138    // The bulk of the translation is done, we no longer need to interact with rustc internals. We
139    // run several passes that simplify the items and cleanup the bodies.
140    for pass in transformation_passes(&options) {
141        pass.run(&mut ctx);
142    }
143
144    let error_count = ctx.errors.borrow().error_count;
145
146    // # Final step: generate the files.
147    if !options.no_serialize {
148        let dest_file = options.target_filename(&ctx.translated.crate_name);
149        trace!("Target file: {:?}", dest_file);
150        export::CrateData::new(ctx)
151            .serialize_to_file(&dest_file)
152            .map_err(|()| CharonFailure::Serialize)?;
153    }
154
155    if options.error_on_warnings && error_count != 0 {
156        return Err(CharonFailure::CharonError(error_count));
157    }
158
159    Ok(error_count)
160}
161
162fn main() {
163    // Initialize the logger
164    logger::initialize_logger();
165
166    // Catch any and all panics coming from charon to display a clear error.
167    let res = panic::catch_unwind(run_charon)
168        .map_err(|_| CharonFailure::Panic)
169        .and_then(|x| x);
170
171    match res {
172        Ok(warn_count) => {
173            if warn_count != 0 {
174                let msg = format!("The extraction generated {} warnings", warn_count);
175                eprintln!("warning: {}", msg);
176            }
177        }
178        Err(err) => {
179            log::error!("{err}");
180            let exit_code = match err {
181                CharonFailure::CharonError(_) | CharonFailure::Serialize => 1,
182                CharonFailure::RustcError => 2,
183                // This is a real panic, exit with the standard rust panic error code.
184                CharonFailure::Panic => 101,
185            };
186            std::process::exit(exit_code);
187        }
188    }
189}
charon_driver/main.rs

charon_driver/
main.rs
