Gracefully fail when compiling structs with too large array (#4461)

Fixes an internal compiler error (ICE) in Kani that occurs when
compiling code containing structs with extremely large array sizes.
Instead of triggering an ICE with `span_bug!`, the compiler now emits a
proper error message. This aligns with how `rustc` handles similar size
overflow errors.

Resolves: #2236

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Zyad Hassan <[email protected]>

Author: tautschnig

kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs

@@ -848,7 +848,20 @@ impl<'tcx> LayoutOfHelpers<'tcx> for GotocCtx<'tcx, '_> {
 
     #[inline]
     fn handle_layout_err(&self, err: LayoutError<'tcx>, span: Span, ty: Ty<'tcx>) -> ! {
-        span_bug!(span, "failed to get layout for `{}`: {}", ty, err)
+        // Handle SizeOverflow errors gracefully instead of causing an ICE
+        if let LayoutError::SizeOverflow(_) = err {
+            self.tcx
+                .dcx()
+                .struct_span_err(
+                    span,
+                    format!("values of the type `{}` are too big for the target architecture", ty),
+                )
+                .emit();
+            self.tcx.dcx().abort_if_errors();
+            unreachable!()
+        } else {
+            span_bug!(span, "failed to get layout for `{}`: {}", ty, err)
+        }
     }
 }
 

tests/ui/ice-size-overflow/expected

@@ -0,0 +1,13 @@
+error[E0080]: values of the type `[u8; usize::MAX]` are too big for the target architecture\
+lib/rustlib/src/rust/library/core/src/mem/mod.rs\
+|\
+const SIZE: usize = intrinsics::size_of::<Self>();\
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ evaluation of `<S<u8> as std::mem::SizedTypeProperties>::SIZE` failed here\
+
+note: the above error was encountered while instantiating `fn std::mem::size_of::<S<u8>>`\
+tests/ui/ice-size-overflow/large_array.rs\
+|\
+std::mem::size_of::<S<u8>>()\
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+error: aborting due to 1 previous error; 1 warning emitted

tests/ui/ice-size-overflow/large_array.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that the compiler handles extremely large array sizes
+//! gracefully with a proper error message instead of causing an ICE.
+//! Previously, this would trigger an internal compiler error at
+//! kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs:371:9
+
+struct S<T> {
+    x: [T; !0],
+}
+
+pub fn f() -> usize {
+    std::mem::size_of::<S<u8>>()
+}
+
+#[kani::proof]
+fn main() {
+    let _x = f();
+}