Make reorder_decls succeed if there are missing definitions

charon/src/charon-driver.rs

@@ -205,16 +205,18 @@ fn main() {
     // We don't need to check this case in order to use the default Rustc callbacks
     // instead of the Charon callback: because there is nothing to build, Rustc will
     // take care of everything and actually not call us back.
-    let continue_on_failure = options.continue_on_failure;
-    let res = RunCompiler::new(&compiler_args, &mut CharonCallbacks { options }).run();
+    let mut callback = CharonCallbacks {
+        options,
+        error_count: 0,
+    };
+    let res = RunCompiler::new(&compiler_args, &mut callback).run();
 
     match res {
         Ok(()) => (),
         Err(_) => {
-            log::error!("The extraction encountered errors");
-            if !continue_on_failure {
-                panic!("The extraction encountered errors");
-            }
+            let msg = format!("The extraction encountered {} errors", callback.error_count);
+            log::error!("{}", msg);
+            std::process::exit(1);
         }
     }
 }

charon/src/driver.rs

@@ -28,6 +28,8 @@ use std::ops::Deref;
 /// The callbacks for Charon
 pub struct CharonCallbacks {
     pub options: cli_options::CliOpts,
+    /// This is to be filled during the extraction
+    pub error_count: usize,
 }
 
 impl Callbacks for CharonCallbacks {
@@ -114,7 +116,7 @@ pub fn get_args_crate_index<T: Deref<Target = str>>(args: &[T]) -> Option<usize>
 /// Translate a crate to LLBC (Low-Level Borrow Calculus).
 ///
 /// This function is a callback function for the Rust compiler.
-pub fn translate(sess: &Session, tcx: TyCtxt, internal: &CharonCallbacks) -> Result<(), ()> {
+pub fn translate(sess: &Session, tcx: TyCtxt, internal: &mut CharonCallbacks) -> Result<(), ()> {
     trace!();
     let options = &internal.options;
 
@@ -188,6 +190,7 @@ pub fn translate(sess: &Session, tcx: TyCtxt, internal: &CharonCallbacks) -> Res
     if options.ullbc {
         // # Extract the files
         export::export_ullbc(
+            ctx.error_count > 0,
             crate_name,
             &ctx.id_to_file,
             &ordered_decls,
@@ -282,6 +285,7 @@ pub fn translate(sess: &Session, tcx: TyCtxt, internal: &CharonCallbacks) -> Res
 
         // # Final step: generate the files.
         export::export_llbc(
+            ctx.error_count > 0,
             crate_name,
             &ctx.id_to_file,
             &ordered_decls,
@@ -295,5 +299,8 @@ pub fn translate(sess: &Session, tcx: TyCtxt, internal: &CharonCallbacks) -> Res
     }
     trace!("Done");
 
+    // Update the error count
+    internal.error_count = ctx.error_count;
+
     Ok(())
 }

charon/src/export.rs

@@ -54,6 +54,7 @@ struct GCrateSerializer<'a, FD, GD> {
 ///
 /// This is a generic function, used both for LLBC and ULLBC.
 pub fn gexport<FD: Serialize + Clone, GD: Serialize + Clone>(
+    errors: bool,
     crate_name: String,
     id_to_file: &HashMap<FileId::Id, FileName>,
     ordered_decls: &DeclarationsGroups,
@@ -64,7 +65,7 @@ pub fn gexport<FD: Serialize + Clone, GD: Serialize + Clone>(
     trait_impls: &TraitImplId::Map<TraitImpl>,
     dest_dir: &Option<PathBuf>,
     extension: &str,
-) -> Result<(),()> {
+) -> Result<(), ()> {
     // Generate the destination file - we use the crate name for the file name
     let mut target_filename = dest_dir
         .as_deref()
@@ -123,7 +124,14 @@ pub fn gexport<FD: Serialize + Clone, GD: Serialize + Clone>(
                 // We canonicalize (i.e., make absolute) the path before printing it:
                 // this makes it clearer to the user where to find the file.
                 let path = std::fs::canonicalize(target_filename).unwrap();
-                info!("Generated the file: {}", path.to_str().unwrap());
+                if errors {
+                    info!(
+                        "Generated the partial (because we encountered errors) file: {}",
+                        path.to_str().unwrap()
+                    );
+                } else {
+                    info!("Generated the file: {}", path.to_str().unwrap());
+                }
                 Ok(())
             }
             std::result::Result::Err(_) => {
@@ -140,6 +148,7 @@ pub fn gexport<FD: Serialize + Clone, GD: Serialize + Clone>(
 
 /// Export the translated ULLBC definitions to a JSON file.
 pub fn export_ullbc(
+    errors: bool,
     crate_name: String,
     id_to_file: &HashMap<FileId::Id, FileName>,
     ordered_decls: &DeclarationsGroups,
@@ -149,8 +158,9 @@ pub fn export_ullbc(
     trait_decls: &TraitDecls,
     trait_impls: &TraitImpls,
     dest_dir: &Option<PathBuf>,
-) -> Result<(),()> {
+) -> Result<(), ()> {
     gexport(
+        errors,
         crate_name,
         id_to_file,
         ordered_decls,
@@ -166,6 +176,7 @@ pub fn export_ullbc(
 
 /// Export the translated LLBC definitions to a JSON file.
 pub fn export_llbc(
+    errors: bool,
     crate_name: String,
     id_to_file: &HashMap<FileId::Id, FileName>,
     ordered_decls: &DeclarationsGroups,
@@ -175,8 +186,9 @@ pub fn export_llbc(
     trait_decls: &TraitDecls,
     trait_impls: &TraitImpls,
     dest_dir: &Option<PathBuf>,
-) -> Result<(),()> {
+) -> Result<(), ()> {
     gexport(
+        errors,
         crate_name,
         id_to_file,
         ordered_decls,