Replace more panics with errors

AeneasVerif · Jul 4, 2024 · 7bf53b4 · 7bf53b4
1 parent 3225827
commit 7bf53b4
Show file tree

Hide file tree

Showing 13 changed files with 56 additions and 50 deletions.
diff --git a/charon/Cargo.lock b/charon/Cargo.lock
diff --git a/charon/Cargo.toml b/charon/Cargo.toml
@@ -49,7 +49,7 @@ tracing-tree = "0.3"
 tracing = { version = "0.1", features = [ "max_level_trace", "release_max_level_warn" ] }
 which = "6.0.1"
 
-hax-frontend-exporter = { git = "https://github.com/hacspec/hax", branch = "main" }
+hax-frontend-exporter = { git = "https://github.com/Nadrieril/hax", branch = "downgrade-errors" }
 # hax-frontend-exporter = { path = "../../hax/frontend/exporter" }
 macros = { path = "./macros" }
 

diff --git a/charon/src/bin/charon-driver/main.rs b/charon/src/bin/charon-driver/main.rs
@@ -207,24 +207,27 @@ fn main() {
 
     if !options.no_serialize {
         // # Final step: generate the files.
-        res = res.and_then(|()| {
+        if res.is_ok() || options.errors_as_warnings {
             // `crate_data` is set by our callbacks when there is no fatal error.
-            let crate_data = crate_data.unwrap();
-            let dest_file = match options.dest_file.clone() {
-                Some(f) => f,
-                None => {
-                    let mut target_filename = options.dest_dir.clone().unwrap_or_default();
-                    let crate_name = &crate_data.name;
-                    let extension = if options.ullbc { "ullbc" } else { "llbc" };
-                    target_filename.push(format!("{crate_name}.{extension}"));
-                    target_filename
-                }
-            };
-            trace!("Target file: {:?}", dest_file);
-            crate_data
-                .serialize_to_file(&dest_file)
-                .map_err(|()| CharonFailure::Serialize)
-        });
+            if let Some(crate_data) = crate_data {
+                let dest_file = match options.dest_file.clone() {
+                    Some(f) => f,
+                    None => {
+                        let mut target_filename = options.dest_dir.clone().unwrap_or_default();
+                        let crate_name = &crate_data.name;
+                        let extension = if options.ullbc { "ullbc" } else { "llbc" };
+                        target_filename.push(format!("{crate_name}.{extension}"));
+                        target_filename
+                    }
+                };
+                trace!("Target file: {:?}", dest_file);
+                res = res.and(
+                    crate_data
+                        .serialize_to_file(&dest_file)
+                        .map_err(|()| CharonFailure::Serialize),
+                );
+            }
+        }
     }
 
     match res {

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
@@ -346,6 +346,7 @@ pub fn translate<'tcx, 'ctx>(
         tcx,
         hax::options::Options {
             inline_macro_calls: Vec::new(),
+            downgrade_errors: options.errors_as_warnings,
         },
     );
     let mut ctx = TranslateCtx {
@@ -393,11 +394,17 @@ pub fn translate<'tcx, 'ctx>(
     let hir = tcx.hir();
     for item_id in hir.root_module().item_ids {
         let item_id = item_id.hir_id();
-        let rustc_hir::Node::Item(item) = tcx.hir_node(item_id) else {
-            unreachable!()
-        };
-        // If registration fails we simply skip the item.
-        let _ = ctx.register_local_hir_item(true, item);
+        {
+            let mut ctx = std::panic::AssertUnwindSafe(&mut ctx);
+            // Stopgap measure because there are still many panics in charon and hax.
+            // If registration fails we simply skip the item.
+            let _ = std::panic::catch_unwind(move || {
+                let rustc_hir::Node::Item(item) = ctx.tcx.hir_node(item_id) else {
+                    unreachable!()
+                };
+                ctx.register_local_hir_item(true, item)
+            });
+        }
     }
 
     trace!(

diff --git a/charon/src/bin/charon-driver/translate/translate_ctx.rs b/charon/src/bin/charon-driver/translate/translate_ctx.rs
@@ -301,7 +301,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
             use rustc_hir::definitions::DefPathData;
             match &data.data {
                 DefPathData::TypeNs(symbol) => {
-                    assert!(data.disambiguator == 0); // Sanity check
+                    error_assert!(self, span, data.disambiguator == 0); // Sanity check
                     name.push(PathElem::Ident(symbol.to_string(), disambiguator));
                 }
                 DefPathData::ValueNs(symbol) => {
@@ -311,10 +311,10 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                 }
                 DefPathData::CrateRoot => {
                     // Sanity check
-                    assert!(data.disambiguator == 0);
+                    error_assert!(self, span, data.disambiguator == 0);
 
                     // This should be the beginning of the path
-                    assert!(name.is_empty());
+                    error_assert!(self, span, name.is_empty());
                     found_crate_name = true;
                     name.push(PathElem::Ident(crate_name.clone(), disambiguator));
                 }
@@ -379,7 +379,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                     // TODO: do nothing for now
                 }
                 DefPathData::MacroNs(symbol) => {
-                    assert!(data.disambiguator == 0); // Sanity check
+                    error_assert!(self, span, data.disambiguator == 0); // Sanity check
 
                     // There may be namespace collisions between, say, function
                     // names and macros (not sure). However, this isn't much
@@ -399,8 +399,7 @@ impl<'tcx, 'ctx> TranslateCtx<'tcx, 'ctx> {
                     // block.
                 }
                 _ => {
-                    error!("Unexpected DefPathData: {:?}", data);
-                    unreachable!("Unexpected DefPathData: {:?}", data);
+                    error_or_panic!(self, span, format!("Unexpected DefPathData: {:?}", data));
                 }
             }
         }

diff --git a/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs b/charon/src/bin/charon-driver/translate/translate_functions_to_ullbc.rs
@@ -5,6 +5,7 @@
 
 use std::mem;
 use std::panic;
+use std::rc::Rc;
 
 use super::get_mir::{boxes_are_desugared, get_mir_for_def_id_and_level};
 use super::translate_ctx::*;
@@ -16,7 +17,7 @@ use charon_lib::ids::Vector;
 use charon_lib::pretty::FmtWithCtx;
 use charon_lib::ullbc_ast::*;
 use hax_frontend_exporter as hax;
-use hax_frontend_exporter::SInto;
+use hax_frontend_exporter::{HasMirSetter, HasOwnerIdSetter, SInto};
 use rustc_hir::def_id::DefId;
 use rustc_middle::mir::START_BLOCK;
 use rustc_middle::ty;
@@ -1443,16 +1444,12 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         };
 
         // Here, we have to create a MIR state, which contains the body
-        let state = hax::state::State::new_from_mir(
-            tcx,
-            hax::options::Options {
-                inline_macro_calls: Vec::new(),
-            },
-            // Yes, we have to clone, this is annoying: we end up cloning the body twice
-            body.clone(),
-            // Owner id
-            rust_id,
-        );
+        // Yes, we have to clone, this is annoying: we end up cloning the body twice
+        let state = self
+            .hax_state
+            .clone()
+            .with_owner_id(rust_id)
+            .with_mir(Rc::new(body.clone()));
         // Translate
         let body: hax::MirBody<()> = body.sinto(&state);
 

diff --git a/charon/tests/ui/issue-91-enum-to-discriminant-cast.out b/charon/tests/ui/issue-91-enum-to-discriminant-cast.out
@@ -6,5 +6,5 @@ error: Unsupported statement kind: intrinsic
 
 error: aborting due to 1 previous error
 
-[ERROR charon_driver:243] Compilation encountered 1 errors
+[ERROR charon_driver:246] Compilation encountered 1 errors
 Error: Charon driver exited with code 1
diff --git a/charon/tests/ui/rename_attribute_failure.out b/charon/tests/ui/rename_attribute_failure.out
@@ -36,5 +36,5 @@ error: Error parsing attribute: Unrecognized attribute: `charon::something_else(
 
 error: aborting due to 6 previous errors
 
-[ERROR charon_driver:243] Compilation encountered 6 errors
+[ERROR charon_driver:246] Compilation encountered 6 errors
 Error: Charon driver exited with code 1
diff --git a/charon/tests/ui/unsupported/gat.out b/charon/tests/ui/unsupported/gat.out
@@ -18,5 +18,5 @@ error: Ignoring the following item due to an error: test_crate::ArraySize
 
 error: aborting due to 3 previous errors
 
-[ERROR charon_driver:243] Compilation encountered 2 errors
+[ERROR charon_driver:246] Compilation encountered 2 errors
 Error: Charon driver exited with code 1
diff --git a/charon/tests/ui/unsupported/issue-165-vec-macro.out b/charon/tests/ui/unsupported/issue-165-vec-macro.out
@@ -8,5 +8,5 @@ error: Nullary operations are not supported
 
 error: aborting due to 1 previous error
 
-[ERROR charon_driver:243] Compilation encountered 1 errors
+[ERROR charon_driver:246] Compilation encountered 1 errors
 Error: Charon driver exited with code 1
diff --git a/charon/tests/ui/unsupported/projection-index-from-end.out b/charon/tests/ui/unsupported/projection-index-from-end.out
@@ -6,5 +6,5 @@ error: Unexpected ProjectionElem::ConstantIndex
 
 error: aborting due to 1 previous error
 
-[ERROR charon_driver:243] Compilation encountered 1 errors
+[ERROR charon_driver:246] Compilation encountered 1 errors
 Error: Charon driver exited with code 1
diff --git a/charon/tests/ui/unsupported/unbound-lifetime.out b/charon/tests/ui/unsupported/unbound-lifetime.out
@@ -27,5 +27,5 @@ error: Ignoring the following item due to an error: test_crate::get
 error: aborting due to 3 previous errors
 
 For more information about this error, try `rustc --explain E0261`.
-[ERROR charon_driver:243] Compilation encountered 2 errors
+[ERROR charon_driver:246] Compilation encountered 2 errors
 Error: Charon driver exited with code 1
diff --git a/charon/tests/ui/unsupported/well-formedness-bound.out b/charon/tests/ui/unsupported/well-formedness-bound.out
@@ -14,5 +14,5 @@ error: Ignoring the following item due to an error: test_crate::get
 
 error: aborting due to 2 previous errors
 
-[ERROR charon_driver:243] Compilation encountered 2 errors
+[ERROR charon_driver:246] Compilation encountered 2 errors
 Error: Charon driver exited with code 1