Partial fix for #2121

Throws a graceful type error for `ctpop` in the code gen.
Adds the expectation to the test case.
Marks the test case as no longer `fixme`

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

@@ -120,16 +120,71 @@ impl<'tcx> GotocCtx<'tcx> {
         }
     }
 
-    /// c.f. `rustc_codegen_llvm::intrinsic` `impl IntrinsicCallMethods<'tcx> for Builder<'a, 'll, 'tcx>`
-    /// `fn codegen_intrinsic_call`
-    /// c.f. <https://doc.rust-lang.org/std/intrinsics/index.html>
+    fn codegen_ctpop(
+        &mut self,
+        target_place: Place<'tcx>,
+        loc: Location,
+        span: Option<Span>,
+        arg: Expr,
+        arg_rust_ty: Ty<'tcx>,
+    ) -> Stmt {
+        if !arg.typ().is_integer() {
+            self.intrinsics_typecheck_fail(span, "ctpop", "integer type", arg_rust_ty);
+            Stmt::skip(loc)
+        } else {
+            self.codegen_expr_to_place(&target_place, arg.popcount())
+        }
+    }
+
+    /// Report that a delayed type check on an intrinsic failed.
+    ///
+    /// The idea is to blame one of the arguments on the failed type check and
+    /// report the type that was found for that argument in `actual`. The
+    /// `expected` type for that argument can be very permissive (e.g. "some
+    /// integer type") and as a result it allows a permissive string as
+    /// description.
+    ///
+    /// Calling this function will abort the compilation though that is not
+    /// obvious by the type.
+    fn intrinsics_typecheck_fail(
+        &self,
+        span: Option<Span>,
+        name: &str,
+        expected: &str,
+        actual: Ty,
+    ) {
+        self.tcx.sess.span_err(
+            span.into_iter().collect::<Vec<_>>(),
+            format!(
+                "Type check failed for intrinsic `{name}`: Expected {expected}, found {actual}"
+            ),
+        );
+        self.tcx.sess.abort_if_errors();
+    }
+
+    /// c.f. `rustc_codegen_llvm::intrinsic` `impl IntrinsicCallMethods<'tcx>
+    /// for Builder<'a, 'll, 'tcx>` `fn codegen_intrinsic_call` c.f.
+    /// <https://doc.rust-lang.org/std/intrinsics/index.html>
     fn codegen_intrinsic(
         &mut self,
         instance: Instance<'tcx>,
         mut fargs: Vec<Expr>,
         p: &Place<'tcx>,
         span: Option<Span>,
     ) -> Stmt {
+        // ### A note on type checking
+        //
+        // The backend/codegen generally assumes that at this point arguments
+        // have been type checked and that the given intrinsic is safe to call
+        // with the provided arguments. However in rare cases the intrinsics
+        // type signature is too permissive or has to be liberal because the
+        // types are enforced by the specific code gen/backend. In such cases we
+        // handle the type checking here. The type constraints are lifted
+        // straight from the assertions made in various functions in
+        // [`cprover_bindings::goto_program::expr`]. If the constraints in the
+        // type checks here ever disagree with those made in
+        // [`cprover_bindings`] you may always assume the one's in the bindigns
+        // to be the ultimate authority.
         let intrinsic = self.symbol_name(instance);
         let intrinsic = intrinsic.as_str();
         let loc = self.codegen_span_option(span);
@@ -445,7 +500,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "cosf64" => codegen_simple_intrinsic!(Cos),
             "ctlz" => codegen_count_intrinsic!(ctlz, true),
             "ctlz_nonzero" => codegen_count_intrinsic!(ctlz, false),
-            "ctpop" => self.codegen_expr_to_place(p, fargs.remove(0).popcount()),
+            "ctpop" => self.codegen_ctpop(*p, loc, span, fargs.remove(0), farg_types[0]),
             "cttz" => codegen_count_intrinsic!(cttz, true),
             "cttz_nonzero" => codegen_count_intrinsic!(cttz, false),
             "discriminant_value" => {

tests/expected/intrinsics/ctpop-ice/expected

@@ -0,0 +1,6 @@
+error: Type check failed for intrinsic `ctpop`: Expected integer type, found ()
+   |
+12 |     let n = ctpop(());
+   |             ^^^^^^^^^
+
+error: aborting due to previous error