Fix Kani crash with const-generic [e; N] expression (rust-lang#1770)

Author: tedinski

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -204,7 +204,7 @@ impl<'tcx> GotocCtx<'tcx> {
     fn codegen_rvalue_repeat(
         &mut self,
         op: &Operand<'tcx>,
-        sz: &ty::Const<'tcx>,
+        sz: ty::Const<'tcx>,
         res_ty: Ty<'tcx>,
         loc: Location,
     ) -> Expr {
@@ -393,7 +393,10 @@ impl<'tcx> GotocCtx<'tcx> {
         debug!(?rv, "codegen_rvalue");
         match rv {
             Rvalue::Use(p) => self.codegen_operand(p),
-            Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, res_ty, loc),
+            Rvalue::Repeat(op, sz) => {
+                let sz = self.monomorphize(*sz);
+                self.codegen_rvalue_repeat(op, sz, res_ty, loc)
+            }
             Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => self.codegen_rvalue_ref(p, res_ty),
             Rvalue::Len(p) => self.codegen_rvalue_len(p),
             // Rust has begun distinguishing "ptr -> num" and "num -> ptr" (providence-relevant casts) but we do not yet:

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -708,7 +708,7 @@ impl<'tcx> GotocCtx<'tcx> {
     }
 
     /// codegen for types. it finds a C type which corresponds to a rust type.
-    /// that means [ty] has to be monomorphized.
+    /// that means [ty] has to be monomorphized before calling this function.
     ///
     /// check [rustc_middle::ty::layout::LayoutCx::layout_of_uncached] for LLVM codegen
     ///

tests/kani/Array/repeat_const_generic.rs

@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Ensure Kani can compile `[e; N]` when `N` is a const generic.
+// Test from <https://github.com/model-checking/kani/issues/1728>
+
+struct Foo<const N: usize> {
+    field: [u64; N],
+}
+
+impl<const N: usize> Foo<N> {
+    fn new() -> Self {
+        // Was a crash during codegen because N hadn't been "monomorphized"
+        // and so could not be evaluated to a compile-time constant.
+        Self { field: [0; N] }
+    }
+}
+
+#[cfg(kani)]
+mod proofs {
+    use super::*;
+
+    #[kani::proof]
+    fn hope_kani_does_not_crash() {
+        let x = Foo::<32>::new();
+        assert!(x.field.len() == 32);
+    }
+}