From a6e516e294a8ea1569673996f9f0bfdc5000c105 Mon Sep 17 00:00:00 2001 From: Justus Adam Date: Wed, 28 Jun 2023 10:48:31 -0700 Subject: [PATCH] Throw a graceful error when type checking for `ctpop` fails (#2504) Co-authored-by: Kareem Khazem Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- .../codegen/intrinsic.rs | 61 +++++++++++++++++-- .../ctpop_ice.rs} | 0 tests/expected/intrinsics/ctpop-ice/expected | 6 ++ .../arithmetic_zst_fixme.rs | 0 .../expected | 0 .../sub_with_workflow_ice_fixme/expected | 1 - 6 files changed, 63 insertions(+), 5 deletions(-) rename tests/expected/intrinsics/{ctpop_ice_fixme/fixme_ctpop_ice.rs => ctpop-ice/ctpop_ice.rs} (100%) create mode 100644 tests/expected/intrinsics/ctpop-ice/expected rename tests/expected/intrinsics/{sub_with_workflow_ice_fixme => sub_with_overflow_ice_fixme}/arithmetic_zst_fixme.rs (100%) rename tests/expected/intrinsics/{ctpop_ice_fixme => sub_with_overflow_ice_fixme}/expected (100%) delete mode 100644 tests/expected/intrinsics/sub_with_workflow_ice_fixme/expected diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 7eef6b877523..8c6674d26f26 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -120,9 +120,20 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// c.f. `rustc_codegen_llvm::intrinsic` `impl IntrinsicCallMethods<'tcx> for Builder<'a, 'll, 'tcx>` - /// `fn codegen_intrinsic_call` - /// c.f. + /// c.f. `rustc_codegen_llvm::intrinsic` `impl IntrinsicCallMethods<'tcx> + /// for Builder<'a, 'll, 'tcx>` `fn codegen_intrinsic_call` c.f. + /// + /// + /// ### 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 enforced here must be at least as strict as + /// the assertions made in in the builder functions in + /// [`Expr`]. fn codegen_intrinsic( &mut self, instance: Instance<'tcx>, @@ -445,7 +456,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, span, fargs.remove(0), farg_types[0]), "cttz" => codegen_count_intrinsic!(cttz, true), "cttz_nonzero" => codegen_count_intrinsic!(cttz, false), "discriminant_value" => { @@ -650,6 +661,48 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Perform type checking and code generation for the `ctpop` rust intrinsic. + fn codegen_ctpop( + &mut self, + target_place: Place<'tcx>, + span: Option, + arg: Expr, + arg_rust_ty: Ty<'tcx>, + ) -> Stmt { + if !arg.typ().is_integer() { + self.intrinsics_typecheck_fail(span, "ctpop", "integer type", arg_rust_ty) + } 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, + name: &str, + expected: &str, + actual: Ty, + ) -> ! { + self.tcx.sess.span_err( + span.into_iter().collect::>(), + format!( + "Type check failed for intrinsic `{name}`: Expected {expected}, found {actual}" + ), + ); + self.tcx.sess.abort_if_errors(); + unreachable!("Rustc should have aborted already") + } + // Fast math intrinsics for floating point operations like `fadd_fast` // assume that their inputs are finite: // https://doc.rust-lang.org/std/intrinsics/fn.fadd_fast.html diff --git a/tests/expected/intrinsics/ctpop_ice_fixme/fixme_ctpop_ice.rs b/tests/expected/intrinsics/ctpop-ice/ctpop_ice.rs similarity index 100% rename from tests/expected/intrinsics/ctpop_ice_fixme/fixme_ctpop_ice.rs rename to tests/expected/intrinsics/ctpop-ice/ctpop_ice.rs diff --git a/tests/expected/intrinsics/ctpop-ice/expected b/tests/expected/intrinsics/ctpop-ice/expected new file mode 100644 index 000000000000..25fbb79d9551 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/tests/expected/intrinsics/sub_with_workflow_ice_fixme/arithmetic_zst_fixme.rs b/tests/expected/intrinsics/sub_with_overflow_ice_fixme/arithmetic_zst_fixme.rs similarity index 100% rename from tests/expected/intrinsics/sub_with_workflow_ice_fixme/arithmetic_zst_fixme.rs rename to tests/expected/intrinsics/sub_with_overflow_ice_fixme/arithmetic_zst_fixme.rs diff --git a/tests/expected/intrinsics/ctpop_ice_fixme/expected b/tests/expected/intrinsics/sub_with_overflow_ice_fixme/expected similarity index 100% rename from tests/expected/intrinsics/ctpop_ice_fixme/expected rename to tests/expected/intrinsics/sub_with_overflow_ice_fixme/expected diff --git a/tests/expected/intrinsics/sub_with_workflow_ice_fixme/expected b/tests/expected/intrinsics/sub_with_workflow_ice_fixme/expected deleted file mode 100644 index dca276fb90c0..000000000000 --- a/tests/expected/intrinsics/sub_with_workflow_ice_fixme/expected +++ /dev/null @@ -1 +0,0 @@ -Kani unexpectedly panicked during compilation.