From c544d13076c4b456c32451020656100120ec459c Mon Sep 17 00:00:00 2001
From: Nadrieril <nadrieril+git@gmail.com>
Date: Fri, 19 Apr 2024 11:00:27 +0200
Subject: [PATCH] Catch panics in `translate_body`

---
 charon/src/translate_functions_to_ullbc.rs | 25 ++++++++-
 charon/tests/ui/unsupported/slice_index.rs |  2 +-
 charon/tests/ui/unsupported/vec-push.out   | 59 +++++++++++++++++++++-
 charon/tests/ui/unsupported/vec-push.rs    |  2 +-
 4 files changed, 83 insertions(+), 5 deletions(-)

diff --git a/charon/src/translate_functions_to_ullbc.rs b/charon/src/translate_functions_to_ullbc.rs
index 1c0f825e0..d08fe7027 100644
--- a/charon/src/translate_functions_to_ullbc.rs
+++ b/charon/src/translate_functions_to_ullbc.rs
@@ -3,6 +3,9 @@
 //! us to handle, and easier to maintain - rustc's representation can evolve
 //! independently.
 
+use std::mem;
+use std::panic;
+
 use crate::assumed;
 use crate::common::*;
 use crate::expressions::*;
@@ -1443,6 +1446,24 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         mut self,
         rust_id: DefId,
         arg_count: usize,
+    ) -> Result<Option<ExprBody>, Error> {
+        // Stopgap measure because there are still many panics in charon and hax.
+        let mut this = panic::AssertUnwindSafe(&mut self);
+        let res = panic::catch_unwind(move || this.translate_body_aux(rust_id, arg_count));
+        match res {
+            Ok(Ok(body)) => Ok(body),
+            Ok(Err(e)) => Err(e),
+            Err(_) => {
+                let span = self.t_ctx.tcx.def_span(rust_id);
+                error_or_panic!(self, span, "Thread panicked when extracting body.");
+            }
+        }
+    }
+
+    fn translate_body_aux(
+        &mut self,
+        rust_id: DefId,
+        arg_count: usize,
     ) -> Result<Option<ExprBody>, Error> {
         let tcx = self.t_ctx.tcx;
 
@@ -1486,7 +1507,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         // We need to convert the blocks map to an index vector
         // We clone things while we could move them...
         let mut blocks = BlockId::Vector::new();
-        for (id, block) in self.blocks {
+        for (id, block) in mem::take(&mut self.blocks) {
             let new_id = blocks.push(block);
             // Sanity check to make sure we don't mess with the indices
             assert!(id == new_id);
@@ -1496,7 +1517,7 @@ impl<'tcx, 'ctx, 'ctx1> BodyTransCtx<'tcx, 'ctx, 'ctx1> {
         Ok(Some(ExprBody {
             meta,
             arg_count,
-            locals: self.vars,
+            locals: mem::take(&mut self.vars),
             body: blocks,
         }))
     }
diff --git a/charon/tests/ui/unsupported/slice_index.rs b/charon/tests/ui/unsupported/slice_index.rs
index 5c4c76bd0..c00ac698b 100644
--- a/charon/tests/ui/unsupported/slice_index.rs
+++ b/charon/tests/ui/unsupported/slice_index.rs
@@ -1,4 +1,4 @@
-//@ known-panic
+//@ known-failure
 //@ no-check-output
 //@ charon-args=--extract-opaque-bodies
 
diff --git a/charon/tests/ui/unsupported/vec-push.out b/charon/tests/ui/unsupported/vec-push.out
index cd0cbefbc..9237529ea 100644
--- a/charon/tests/ui/unsupported/vec-push.out
+++ b/charon/tests/ui/unsupported/vec-push.out
@@ -13,5 +13,62 @@ error[HaxFront]: Supposely unreachable place in the Rust AST. The label is "Plac
   = note: ⚠️ This is a bug in Hax's frontend.
           Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!
 
-error: aborting due to previous error
+error: Thread panicked when extracting body.
+ --> /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/vec/mod.rs:1824:5
 
+[ INFO charon_lib::driver:332] [translate]: # Final LLBC before serialization:
+
+struct core::ptr::non_null::NonNull<T> =
+{
+  pointer: *mut T
+}
+
+struct core::marker::PhantomData<T> = {}
+
+struct core::ptr::unique::Unique<T> =
+{
+  pointer: core::ptr::non_null::NonNull<T>,
+  _marker: core::marker::PhantomData<T>
+}
+
+struct alloc::raw_vec::RawVec<T, A> =
+{
+  ptr: core::ptr::unique::Unique<T>,
+  cap: usize,
+  alloc: A
+}
+
+struct alloc::vec::Vec<T, A> =
+{
+  buf: alloc::raw_vec::RawVec<T, A>,
+  len: usize
+}
+
+struct alloc::alloc::Global = {}
+
+fn alloc::vec::{alloc::vec::Vec<T, A>#1}::push<'_0, T, A>(@1: &'_0 mut (alloc::vec::Vec<T, A>), @2: T)
+
+fn test_crate::vec<'_0>(@1: &'_0 mut (alloc::vec::Vec<u32, alloc::alloc::Global>))
+{
+    let @0: (); // return
+    let x@1: &'_ mut (alloc::vec::Vec<u32, alloc::alloc::Global>); // arg #1
+    let @2: &'_ mut (alloc::vec::Vec<u32, alloc::alloc::Global>); // anonymous local
+
+    @2 := &two-phase-mut *(x@1)
+    @0 := alloc::vec::{alloc::vec::Vec<T, A>#1}::push<u32, alloc::alloc::Global>(move (@2), const (42 : u32))
+    drop @2
+    @0 := ()
+    return
+}
+
+
+
+error: The external definition DefId(5:6777 ~ alloc[6cf4]::vec::{impl#1}::push) triggered errors. It is (transitively) used at the following location(s):
+ --> tests/ui/unsupported/vec-push.rs:5:5
+  |
+5 |     x.push(42)
+  |     ^^^^^^^^^^
+
+error: aborting due to 3 previous errors
+
+[ ERROR charon_driver:180] The extraction encountered 1 errors
diff --git a/charon/tests/ui/unsupported/vec-push.rs b/charon/tests/ui/unsupported/vec-push.rs
index 100e44a02..9a099fa04 100644
--- a/charon/tests/ui/unsupported/vec-push.rs
+++ b/charon/tests/ui/unsupported/vec-push.rs
@@ -1,4 +1,4 @@
-//@ known-panic
+//@ known-failure
 //@ charon-args=--extract-opaque-bodies
 
 fn vec(x: &mut Vec<u32>) {