From cd03feeb2ae1af727210b73cc0d447154d77ecde Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 20 Jun 2023 16:41:04 -0700 Subject: [PATCH 1/6] Upgrade toolchain version and clean compilation - Still need to clean regression --- .../codegen/intrinsic.rs | 70 +----------- .../codegen_cprover_gotoc/codegen/rvalue.rs | 104 +++++++++++++++++- .../codegen/statement.rs | 6 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 10 +- .../compiler_interface.rs | 33 +++--- .../codegen_cprover_gotoc/context/goto_ctx.rs | 4 +- kani-compiler/src/kani_middle/attributes.rs | 7 +- kani-compiler/src/kani_middle/coercion.rs | 10 +- kani-compiler/src/kani_middle/mod.rs | 6 +- kani-compiler/src/kani_middle/provide.rs | 9 +- kani-compiler/src/kani_middle/reachability.rs | 8 +- rust-toolchain.toml | 2 +- 12 files changed, 159 insertions(+), 110 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 8c6674d26f26..7084b38bf75a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -5,8 +5,7 @@ use super::typ::{self, pointee_type}; use super::PropertyClass; use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{ - arithmetic_overflow_result_type, ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, - Location, Stmt, Type, ARITH_OVERFLOW_OVERFLOWED_FIELD, ARITH_OVERFLOW_RESULT_FIELD, + ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type, }; use rustc_middle::mir::{BasicBlock, Operand, Place}; use rustc_middle::ty::layout::{LayoutOf, ValidityRequirement}; @@ -183,43 +182,6 @@ impl<'tcx> GotocCtx<'tcx> { }}; } - // Intrinsics which encode a simple arithmetic operation with overflow check - macro_rules! codegen_op_with_overflow_check { - ($f:ident) => {{ - let a = fargs.remove(0); - let b = fargs.remove(0); - let op_type = a.typ().clone(); - let res = a.$f(b); - // add to symbol table - let struct_tag = self.codegen_arithmetic_overflow_result_type(op_type.clone()); - assert_eq!(*res.typ(), struct_tag); - - // store the result in a temporary variable - let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc); - let check = self.codegen_assert( - var.clone() - .member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table) - .cast_to(Type::c_bool()) - .not(), - PropertyClass::ArithmeticOverflow, - format!("attempt to compute {} which would overflow", intrinsic).as_str(), - loc, - ); - self.codegen_expr_to_place( - p, - Expr::statement_expression( - vec![ - decl, - check, - var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table) - .as_stmt(loc), - ], - op_type, - ), - ) - }}; - } - // Intrinsics which encode a division operation with overflow check macro_rules! codegen_op_with_div_overflow_check { ($f:ident) => {{ @@ -617,19 +579,12 @@ impl<'tcx> GotocCtx<'tcx> { "unaligned_volatile_load" => { unstable_codegen!(self.codegen_expr_to_place(p, fargs.remove(0).dereference())) } - "unchecked_add" => codegen_op_with_overflow_check!(add_overflow_result), + "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr" + | "unchecked_sub" => { + unreachable!("Expect intrinsic {intrinsic} to be lowered before codegen") + } "unchecked_div" => codegen_op_with_div_overflow_check!(div), - "unchecked_mul" => codegen_op_with_overflow_check!(mul_overflow_result), "unchecked_rem" => codegen_op_with_div_overflow_check!(rem), - "unchecked_shl" => codegen_intrinsic_binop!(shl), - "unchecked_shr" => { - if fargs[0].typ().is_signed(self.symbol_table.machine_model()) { - codegen_intrinsic_binop!(ashr) - } else { - codegen_intrinsic_binop!(lshr) - } - } - "unchecked_sub" => codegen_op_with_overflow_check!(sub_overflow_result), "unlikely" => self.codegen_expr_to_place(p, fargs.remove(0)), "unreachable" => unreachable!( "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`" @@ -1808,19 +1763,4 @@ impl<'tcx> GotocCtx<'tcx> { ); (size_of_count_elems.result, assert_stmt) } - - /// Codegens the struct type that CBMC produces for its arithmetic with overflow operators: - /// ``` - /// struct overflow_result_ { - /// operand_type result; // the result of the operation - /// bool overflowed; // whether the operation overflowed - /// } - /// ``` - /// and adds the type to the symbol table - fn codegen_arithmetic_overflow_result_type(&mut self, operand_type: Type) -> Type { - let res_type = arithmetic_overflow_result_type(operand_type); - self.ensure_struct(res_type.tag().unwrap(), res_type.tag().unwrap(), |_, _| { - res_type.components().unwrap().clone() - }) - } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 8a652f0833e1..097d501a72bc 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -163,6 +163,52 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Generate code for a binary operation with an overflow and returns a tuple (res, overflow). + fn codegen_binop_with_overflow_check( + &mut self, + op: &BinOp, + left_op: &Operand<'tcx>, + right_op: &Operand<'tcx>, + loc: Location, + ) -> Expr { + debug!(?op, "codegen_binop_with_overflow_check"); + let left = self.codegen_operand(left_op); + let right = self.codegen_operand(right_op); + let ret_type = left.typ().clone(); + let (bin_op, op_name) = match op { + BinOp::AddUnchecked => (BinaryOperator::OverflowResultPlus, "unchecked_add"), + BinOp::SubUnchecked => (BinaryOperator::OverflowResultMinus, "unchecked_sub"), + BinOp::MulUnchecked => (BinaryOperator::OverflowResultMult, "unchecked_mul"), + _ => unreachable!("Expected Add/Sub/Mul but got {op:?}"), + }; + // Create CBMC result type and add to the symbol table. + let res_type = arithmetic_overflow_result_type(left.typ().clone()); + let tag = res_type.tag().unwrap(); + let struct_tag = + self.ensure_struct(tag, tag, |_, _| res_type.components().unwrap().clone()); + let res = left.overflow_op(bin_op, right); + // store the result in a temporary variable + let (var, decl) = self.decl_temp_variable(struct_tag, Some(res), loc); + // cast into result type + let check = self.codegen_assert( + var.clone() + .member(ARITH_OVERFLOW_OVERFLOWED_FIELD, &self.symbol_table) + .cast_to(Type::c_bool()) + .not(), + PropertyClass::ArithmeticOverflow, + format!("attempt to compute `{op_name}` which would overflow").as_str(), + loc, + ); + Expr::statement_expression( + vec![ + decl, + check, + var.member(ARITH_OVERFLOW_RESULT_FIELD, &self.symbol_table).as_stmt(loc), + ], + ret_type, + ) + } + /// Generate code for a binary operation with an overflow and returns a tuple (res, overflow). pub fn codegen_binop_with_overflow( &mut self, @@ -297,7 +343,27 @@ impl<'tcx> GotocCtx<'tcx> { BinOp::Add | BinOp::Sub | BinOp::Mul | BinOp::Shl | BinOp::Shr => { self.codegen_scalar_binop(op, e1, e2) } - BinOp::Div | BinOp::Rem | BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => { + // We currently rely on CBMC's UB checks for shift which isn't always accurate. + // We should implement the checks ourselves. + // See https://github.com/model-checking/kani/issues/2374 + BinOp::ShlUnchecked => self.codegen_scalar_binop(&BinOp::Shl, e1, e2), + BinOp::ShrUnchecked => self.codegen_scalar_binop(&BinOp::Shr, e1, e2), + BinOp::AddUnchecked | BinOp::MulUnchecked | BinOp::SubUnchecked => { + self.codegen_binop_with_overflow_check(op, e1, e2, loc) + } + BinOp::Div | BinOp::Rem => { + let result = self.codegen_unchecked_scalar_binop(op, e1, e2); + if self.operand_ty(e1).is_integral() { + let check = self.check_div_overflow(e1, e2, loc); + Expr::statement_expression( + vec![check, result.clone().as_stmt(loc)], + result.typ().clone(), + ) + } else { + result + } + } + BinOp::BitXor | BinOp::BitAnd | BinOp::BitOr => { self.codegen_unchecked_scalar_binop(op, e1, e2) } BinOp::Eq | BinOp::Lt | BinOp::Le | BinOp::Ne | BinOp::Ge | BinOp::Gt => { @@ -341,6 +407,42 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Check that a division does not overflow. + /// For integer types, division by zero is UB, as is MIN / -1 for signed. + /// Note that the compiler already inserts these checks for regular division. + /// However, since , unchecked divisions are + /// lowered to BinOp::Div. Prefer adding duplicated checks for now. + fn check_div_overflow( + &mut self, + dividend: &Operand<'tcx>, + divisor: &Operand<'tcx>, + loc: Location, + ) -> Stmt { + let divisor_expr = self.codegen_operand(divisor); + let div_by_zero_check = self.codegen_assert_assume( + divisor_expr.clone().is_zero().not(), + PropertyClass::ArithmeticOverflow, + "Attempt to divide by 0", + loc, + ); + if self.operand_ty(dividend).is_signed() { + let dividend_expr = self.codegen_operand(dividend); + let overflow_expr = dividend_expr + .clone() + .eq(dividend_expr.typ().min_int_expr(self.symbol_table.machine_model())) + .and(divisor_expr.clone().eq(Expr::int_constant(-1, divisor_expr.typ().clone()))); + let overflow_check = self.codegen_assert_assume( + overflow_expr.not(), + PropertyClass::ArithmeticOverflow, + "Attempt to compute `MIN / -1` which would overflow", + loc, + ); + Stmt::block(vec![overflow_check, div_by_zero_check], loc) + } else { + div_by_zero_check + } + } + /// Create an initializer for a generator struct. fn codegen_rvalue_generator( &mut self, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 18f510dc7a56..fbabe7e112cd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -149,7 +149,7 @@ impl<'tcx> GotocCtx<'tcx> { "unreachable code", loc, ), - TerminatorKind::Drop { place, target, unwind: _ } => { + TerminatorKind::Drop { place, target, unwind: _, replace: _ } => { self.codegen_drop(place, target, loc) } TerminatorKind::Call { func, args, destination, target, .. } => { @@ -161,12 +161,12 @@ impl<'tcx> GotocCtx<'tcx> { if *expected { r } else { Expr::not(r) } }; - let msg = if let AssertKind::BoundsCheck { .. } = msg { + let msg = if let AssertKind::BoundsCheck { .. } = &**msg { // For bounds check the following panic message is generated at runtime: // "index out of bounds: the length is {len} but the index is {index}", // but CBMC only accepts static messages so we don't add values to the message. "index out of bounds: the length is less than or equal to the given index" - } else if let AssertKind::MisalignedPointerDereference { .. } = msg { + } else if let AssertKind::MisalignedPointerDereference { .. } = &**msg { // Misaligned pointer dereference check messages is also a runtime messages. // Generate a generic one here. "misaligned pointer dereference: address must be a multiple of its type's alignment" diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 955edb615bd6..69da5f1c7ad1 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -303,7 +303,7 @@ impl<'tcx> GotocCtx<'tcx> { var: ty::BoundVar::from_usize(bound_vars.len() - 1), kind: ty::BoundRegionKind::BrEnv, }; - let env_region = self.tcx.mk_re_late_bound(ty::INNERMOST, br); + let env_region = ty::Region::new_late_bound(self.tcx, ty::INNERMOST, br); let env_ty = self.tcx.closure_env_ty(def_id, substs, env_region).unwrap(); let sig = sig.skip_binder(); @@ -345,7 +345,7 @@ impl<'tcx> GotocCtx<'tcx> { kind: ty::BoundRegionKind::BrEnv, }; let env_region = ty::ReLateBound(ty::INNERMOST, br); - let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region_from_kind(env_region), ty); + let env_ty = self.tcx.mk_mut_ref(ty::Region::new_from_kind(self.tcx, env_region), ty); let pin_did = self.tcx.require_lang_item(LangItem::Pin, None); let pin_adt_ref = self.tcx.adt_def(pin_did); @@ -429,7 +429,7 @@ impl<'tcx> GotocCtx<'tcx> { current_fn.instance().subst_mir_and_normalize_erasing_regions( self.tcx, ty::ParamEnv::reveal_all(), - value, + ty::EarlyBinder::bind(value), ) } else { // TODO: confirm with rust team there is no way to monomorphize @@ -665,8 +665,8 @@ impl<'tcx> GotocCtx<'tcx> { } _ => { // This hash is documented to be the same no matter the crate context - let id_u64 = self.tcx.type_id_hash(t).as_u64(); - format!("_{id_u64}").intern() + let id = self.tcx.type_id_hash(t).as_u128(); + format!("_{id}").intern() } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 985cbe1efc47..64e2ae3f4d4c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -27,7 +27,7 @@ use rustc_codegen_ssa::back::archive::{ use rustc_codegen_ssa::back::metadata::create_wrapper_file; use rustc_codegen_ssa::traits::CodegenBackend; use rustc_codegen_ssa::{CodegenResults, CrateInfo}; -use rustc_data_structures::fx::FxHashMap; +use rustc_data_structures::fx::{FxHashMap, FxIndexMap}; use rustc_data_structures::temp_dir::MaybeTempDir; use rustc_errors::{ErrorGuaranteed, DEFAULT_LOCALE_RESOURCE}; use rustc_hir::def_id::LOCAL_CRATE; @@ -36,8 +36,8 @@ use rustc_metadata::fs::{emit_wrapper_file, METADATA_FILENAME}; use rustc_metadata::EncodedMetadata; use rustc_middle::dep_graph::{WorkProduct, WorkProductId}; use rustc_middle::mir::mono::MonoItem; -use rustc_middle::ty::query::Providers; -use rustc_middle::ty::{self, TyCtxt}; +use rustc_middle::query::{ExternProviders, Providers}; +use rustc_middle::ty::TyCtxt; use rustc_session::config::{CrateType, OutputFilenames, OutputType}; use rustc_session::cstore::MetadataLoaderDyn; use rustc_session::output::out_filename; @@ -192,7 +192,7 @@ impl CodegenBackend for GotocCodegenBackend { provide::provide(providers, &self.queries.lock().unwrap()); } - fn provide_extern(&self, providers: &mut ty::query::ExternProviders) { + fn provide_extern(&self, providers: &mut ExternProviders) { provide::provide_extern(providers); } @@ -317,10 +317,12 @@ impl CodegenBackend for GotocCodegenBackend { ongoing_codegen: Box, _sess: &Session, _filenames: &OutputFilenames, - ) -> Result<(CodegenResults, FxHashMap), ErrorGuaranteed> { - Ok(*ongoing_codegen - .downcast::<(CodegenResults, FxHashMap)>() - .unwrap()) + ) -> Result<(CodegenResults, FxIndexMap), ErrorGuaranteed> { + match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() + { + Ok(val) => Ok(*val), + Err(val) => panic!("Oh no: {:?}", val.type_id()), + } } /// Emit output files during the link stage if it was requested. @@ -345,12 +347,13 @@ impl CodegenBackend for GotocCodegenBackend { ) -> Result<(), ErrorGuaranteed> { let requested_crate_types = sess.crate_types(); for crate_type in requested_crate_types { - let out_path = out_filename( + let out_fname = out_filename( sess, *crate_type, outputs, codegen_results.crate_info.local_crate_name, ); + let out_path = out_fname.as_path(); debug!(?crate_type, ?out_path, "link"); if *crate_type == CrateType::Rlib { // Emit the `rlib` that contains just one file: `.rmeta` @@ -396,7 +399,7 @@ fn check_target(session: &Session) { `x86_64-apple-*` or `arm64-apple-*`, but it is {}", &session.target.llvm_target ); - session.err(&err_msg); + session.err(err_msg); } session.abort_if_errors(); @@ -412,7 +415,7 @@ fn check_options(session: &Session) { let err_msg = format!( "Kani requires the target architecture option `min_global_align` to be 1, but it is {align}." ); - session.err(&err_msg); + session.err(err_msg); } _ => (), } @@ -441,7 +444,7 @@ fn codegen_results( rustc_metadata: EncodedMetadata, machine: &MachineModel, ) -> Box { - let work_products = FxHashMap::::default(); + let work_products = FxIndexMap::::default(); Box::new(( CodegenResults { modules: vec![], @@ -482,7 +485,7 @@ fn symbol_table_to_gotoc(tcx: &TyCtxt, base_path: &Path) -> PathBuf { "Failed to generate goto model:\n\tsymtab2gb failed on file {}.", input_filename.display() ); - tcx.sess.err(&err_msg); + tcx.sess.err(err_msg); tcx.sess.abort_if_errors(); }; output_filename @@ -591,7 +594,7 @@ impl<'tcx> GotoCodegenResults<'tcx> { msg += "\nVerification will fail if one or more of these constructs is reachable."; msg += "\nSee https://model-checking.github.io/kani/rust-feature-support.html for more \ details."; - tcx.sess.warn(&msg); + tcx.sess.warn(msg); } if !self.concurrent_constructs.is_empty() { @@ -602,7 +605,7 @@ impl<'tcx> GotoCodegenResults<'tcx> { for (construct, locations) in self.concurrent_constructs.iter() { writeln!(&mut msg, " - {construct} ({})", locations.len()).unwrap(); } - tcx.sess.warn(&msg); + tcx.sess.warn(msg); } // Print some compilation stats. diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs index 836444a78165..dd43c96f27ea 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs @@ -377,13 +377,13 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for GotocCtx<'tcx> { FnAbiRequest::OfFnPtr { sig, extra_args } => { span_bug!( span, - "Error: {err}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`", + "Error: {err:?}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`", ); } FnAbiRequest::OfInstance { instance, extra_args } => { span_bug!( span, - "Error: {err}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`", + "Error: {err:?}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`", ); } } diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 24726e0f9655..6ee5136e12e5 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -58,8 +58,7 @@ pub(super) fn check_attributes(tcx: TyCtxt, def_id: DefId) { format!( "the `{}` attribute also requires the `#[kani::proof]` attribute", kind.as_ref() - ) - .as_str(), + ), ); } match kind { @@ -147,7 +146,7 @@ pub fn extract_harness_attributes(tcx: TyCtxt, def_id: DefId) -> HarnessAttribut /// /// TODO: Improve error message by printing the span of the harness instead of the definition. pub fn check_unstable_features(tcx: TyCtxt, enabled_features: &[String], def_id: DefId) { - if !matches!(tcx.type_of(def_id).0.kind(), TyKind::FnDef(..)) { + if !matches!(tcx.type_of(def_id).skip_binder().kind(), TyKind::FnDef(..)) { // skip closures due to an issue with rustc. // https://github.com/model-checking/kani/pull/2406#issuecomment-1534333862 return; @@ -195,7 +194,7 @@ fn expect_single<'a>( if attributes.len() > 1 { tcx.sess.span_err( attr.span, - &format!("only one '#[kani::{}]' attribute is allowed per harness", kind.as_ref()), + format!("only one '#[kani::{}]' attribute is allowed per harness", kind.as_ref()), ); } attr diff --git a/kani-compiler/src/kani_middle/coercion.rs b/kani-compiler/src/kani_middle/coercion.rs index 3c87a8173b3f..42f3cfb0a702 100644 --- a/kani-compiler/src/kani_middle/coercion.rs +++ b/kani-compiler/src/kani_middle/coercion.rs @@ -16,8 +16,8 @@ use rustc_hir::lang_items::LangItem; use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData}; use rustc_middle::ty::adjustment::CustomCoerceUnsized; -use rustc_middle::ty::TypeAndMut; use rustc_middle::ty::{self, ParamEnv, Ty, TyCtxt}; +use rustc_middle::ty::{TraitRef, TypeAndMut}; use rustc_span::symbol::Symbol; use tracing::trace; @@ -213,9 +213,11 @@ fn custom_coerce_unsize_info<'tcx>( ) -> CustomCoerceUnsized { let def_id = tcx.require_lang_item(LangItem::CoerceUnsized, None); - let trait_ref = ty::Binder::dummy( - tcx.mk_trait_ref(def_id, tcx.mk_substs_trait(source_ty, [target_ty.into()])), - ); + let trait_ref = ty::Binder::dummy(TraitRef::new( + tcx, + def_id, + tcx.mk_substs_trait(source_ty, [target_ty.into()]), + )); match tcx.codegen_select_candidate((ParamEnv::reveal_all(), trait_ref)) { Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { impl_def_id, .. })) => { diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index fc60c0cc1a14..ba235db26805 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -51,7 +51,7 @@ pub fn check_crate_items(tcx: TyCtxt, ignore_asm: bool) { `--enable-unstable --ignore-global-asm` to suppress this error \ (**Verification results may be impacted**).", ); - tcx.sess.err(&error_msg); + tcx.sess.err(error_msg); } else { tcx.sess.warn(format!( "Ignoring global ASM in crate {krate}. Verification results may be impacted.", @@ -192,13 +192,13 @@ impl<'tcx> FnAbiOfHelpers<'tcx> for CompilerHelpers<'tcx> { FnAbiRequest::OfFnPtr { sig, extra_args } => { span_bug!( span, - "Error: {err}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`", + "Error: {err:?}\n while running `fn_abi_of_fn_ptr. ({sig}, {extra_args:?})`", ); } FnAbiRequest::OfInstance { instance, extra_args } => { span_bug!( span, - "Error: {err}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`", + "Error: {err:?}\n while running `fn_abi_of_instance. ({instance}, {extra_args:?})`", ); } } diff --git a/kani-compiler/src/kani_middle/provide.rs b/kani-compiler/src/kani_middle/provide.rs index a3a0a37f6a2e..bdca51f43129 100644 --- a/kani-compiler/src/kani_middle/provide.rs +++ b/kani-compiler/src/kani_middle/provide.rs @@ -6,13 +6,13 @@ use crate::kani_middle::reachability::{collect_reachable_items, filter_crate_items}; use crate::kani_middle::stubbing; -use crate::kani_middle::ty::query::query_provided::collect_and_partition_mono_items; use crate::kani_queries::QueryDb; use rustc_hir::def_id::{DefId, LocalDefId}; use rustc_interface; use rustc_middle::{ mir::Body, - ty::{query::ExternProviders, query::Providers, TyCtxt}, + query::{queries, ExternProviders, Providers}, + ty::TyCtxt, }; /// Sets up rustc's query mechanism to apply Kani's custom queries to code from @@ -65,7 +65,10 @@ fn run_kani_mir_passes<'tcx>( /// This is an issue when compiling a library, since the crate metadata is /// generated (using this query) before code generation begins (which is /// when we normally run the reachability analysis). -fn collect_and_partition_mono_items(tcx: TyCtxt, key: ()) -> collect_and_partition_mono_items { +fn collect_and_partition_mono_items( + tcx: TyCtxt, + key: (), +) -> queries::collect_and_partition_mono_items::ProvidedValue { let entry_fn = tcx.entry_fn(()).map(|(id, _)| id); let local_reachable = filter_crate_items(tcx, |_, def_id| { tcx.is_reachable_non_generic(def_id) || entry_fn == Some(def_id) diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index 4d32a09f7d28..a3110426dc57 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -30,8 +30,8 @@ use rustc_middle::mir::{ use rustc_middle::span_bug; use rustc_middle::ty::adjustment::PointerCast; use rustc_middle::ty::{ - Closure, ClosureKind, ConstKind, Instance, InstanceDef, ParamEnv, Ty, TyCtxt, TyKind, - TypeFoldable, VtblEntry, + Closure, ClosureKind, ConstKind, EarlyBinder, Instance, InstanceDef, ParamEnv, Ty, TyCtxt, + TyKind, TypeFoldable, VtblEntry, }; use crate::kani_middle::coercion; @@ -243,7 +243,7 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> { self.instance.subst_mir_and_normalize_erasing_regions( self.tcx, ParamEnv::reveal_all(), - value, + EarlyBinder::bind(value), ) } @@ -483,7 +483,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> { let receiver_ty = tcx.subst_and_normalize_erasing_regions( substs, ParamEnv::reveal_all(), - generic_ty, + EarlyBinder::bind(generic_ty), ); let sep = callee.rfind("::").unwrap(); let trait_ = &callee[..sep]; diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 0015b8619839..e1e134733598 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-04-30" +channel = "nightly-2023-06-20" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 07bbcbffb72f10368f21babc7b9f851a7d40d80e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 21 Jun 2023 14:12:43 -0700 Subject: [PATCH 2/6] Add codegen_unimplemented for c literal - We were crashing while compiling the standard library --- .../codegen_cprover_gotoc/codegen/operand.rs | 13 +++++++++++ tests/expected/slice_c_str/c_str.rs | 22 +++++++++++++++++++ tests/expected/slice_c_str/expected | 7 ++++++ 3 files changed, 42 insertions(+) create mode 100644 tests/expected/slice_c_str/c_str.rs create mode 100644 tests/expected/slice_c_str/expected diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index a756a42b0388..fa8565a51cf2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -227,6 +227,19 @@ impl<'tcx> GotocCtx<'tcx> { ); } } + ty::Adt(def, _) if Some(def.did()) == self.tcx.lang_items().c_str() => { + // TODO: Handle CString + // https://github.com/model-checking/kani/issues/2549 + let loc = self.codegen_span_option(span.cloned()); + let typ = self.codegen_ty(lit_ty); + let operation_name = "C string literal"; + return self.codegen_unimplemented_expr( + &operation_name, + typ, + loc, + "https://github.com/model-checking/kani/issues/2549", + ); + } _ => {} } } diff --git a/tests/expected/slice_c_str/c_str.rs b/tests/expected/slice_c_str/c_str.rs new file mode 100644 index 000000000000..9fa2feedc6ea --- /dev/null +++ b/tests/expected/slice_c_str/c_str.rs @@ -0,0 +1,22 @@ +#![feature(rustc_private)] +#![feature(c_str_literals)] + +extern crate libc; +use libc::c_char; + +#[kani::proof] +fn check_c_str() { + assert_eq!(unsafe { *empty_c_str() }, 0); + let (s, len) = non_empty_c_str(); + assert_ne!(unsafe { *s.offset(0) }, 0); + assert_eq!(unsafe { *s.offset(len as isize) }, 0); +} + +fn empty_c_str() -> *const c_char { + c"".as_ptr() as *const c_char +} + +/// Return a C string and its length (without the null character). +fn non_empty_c_str() -> (*const c_char, usize) { + (c"hi".as_ptr() as *const c_char, 2) +} diff --git a/tests/expected/slice_c_str/expected b/tests/expected/slice_c_str/expected new file mode 100644 index 000000000000..2138044e5b88 --- /dev/null +++ b/tests/expected/slice_c_str/expected @@ -0,0 +1,7 @@ +warning: Found the following unsupported constructs: +- C string literal + +Checking harness check_c_str... +Failed Checks: C string literal is not currently supported by Kani. + +VERIFICATION:- FAILED From 37a6acc6296b9777e96ff480574097f4afbd7139 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 21 Jun 2023 14:20:42 -0700 Subject: [PATCH 3/6] Small changes to tests after toolchain upgrade --- tests/ui/Property-Class-UI/arithmetic_overflow/expected | 6 +++--- tests/ui/code-location/expected | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/ui/Property-Class-UI/arithmetic_overflow/expected b/tests/ui/Property-Class-UI/arithmetic_overflow/expected index 67fc7dd6c0cd..9b445e995385 100644 --- a/tests/ui/Property-Class-UI/arithmetic_overflow/expected +++ b/tests/ui/Property-Class-UI/arithmetic_overflow/expected @@ -1,11 +1,11 @@ core::num::::unchecked_mul.arithmetic_overflow.1\ Status: SUCCESS -Description: "attempt to compute unchecked_mul which would overflow" +Description: "attempt to compute `unchecked_mul` which would overflow" core::num::::unchecked_add.arithmetic_overflow.1\ Status: SUCCESS -Description: "attempt to compute unchecked_add which would overflow" +Description: "attempt to compute `unchecked_add` which would overflow" core::num::::unchecked_sub.arithmetic_overflow.1\ Status: SUCCESS -Description: "attempt to compute unchecked_sub which would overflow" +Description: "attempt to compute `unchecked_sub` which would overflow" diff --git a/tests/ui/code-location/expected b/tests/ui/code-location/expected index cced065e9f1a..bacda6b16a29 100644 --- a/tests/ui/code-location/expected +++ b/tests/ui/code-location/expected @@ -1,6 +1,6 @@ module/mod.rs:10:5 in function module::not_empty main.rs:13:5 in function same_file /toolchains/ -alloc/src/vec/mod.rs:3018:81 in function as std::ops::Drop>::drop +alloc/src/vec/mod.rs:3007:81 in function as std::ops::Drop>::drop VERIFICATION:- SUCCESSFUL From 8ef1847ab49d8f0ca443948c0a4bcd71f416ab58 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 21 Jun 2023 14:21:07 -0700 Subject: [PATCH 4/6] Workaround performance issue for regression test Use u8 instead of i8 for now and add a performance test to capture this issue. --- tests/cargo-kani/itoa_dep/src/main.rs | 2 +- tests/perf/format/Cargo.toml | 11 +++++++++++ tests/perf/format/expected | 1 + tests/perf/format/src/lib.rs | 20 ++++++++++++++++++++ 4 files changed, 33 insertions(+), 1 deletion(-) create mode 100644 tests/perf/format/Cargo.toml create mode 100644 tests/perf/format/expected create mode 100644 tests/perf/format/src/lib.rs diff --git a/tests/cargo-kani/itoa_dep/src/main.rs b/tests/cargo-kani/itoa_dep/src/main.rs index 9bda87de7339..ea729e7c1c20 100644 --- a/tests/cargo-kani/itoa_dep/src/main.rs +++ b/tests/cargo-kani/itoa_dep/src/main.rs @@ -20,7 +20,7 @@ fn check_itoa() { #[kani::proof] #[kani::unwind(10)] fn check_signed() { - check_itoa::(); + check_itoa::(); } fn main() {} diff --git a/tests/perf/format/Cargo.toml b/tests/perf/format/Cargo.toml new file mode 100644 index 000000000000..3fe392e07c04 --- /dev/null +++ b/tests/perf/format/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "format" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/tests/perf/format/expected b/tests/perf/format/expected new file mode 100644 index 000000000000..44572d1c72bf --- /dev/null +++ b/tests/perf/format/expected @@ -0,0 +1 @@ +Complete - 2 successfully verified harnesses, 0 failures, 2 total diff --git a/tests/perf/format/src/lib.rs b/tests/perf/format/src/lib.rs new file mode 100644 index 000000000000..ad14c6288e7c --- /dev/null +++ b/tests/perf/format/src/lib.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks the performance of calling format. +//! This tests capture the performance regression introduced by the toolchain upgrade #2551. +//! See https://github.com/model-checking/kani/issues/2576 for more details. + +#[kani::proof] +fn fmt_i8() { + let num: i8 = kani::any(); + let s = format!("{num}"); + assert!(s.len() <= 4); +} + +#[kani::proof] +fn fmt_u8() { + let num: u8 = kani::any(); + let s = format!("{num}"); + assert!(s.len() <= 3); +} From a2fa98ac87cc59de3905e1ecad803e61f97576ee Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 3 Jul 2023 14:51:36 -0700 Subject: [PATCH 5/6] Apply suggestions from code review Co-authored-by: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> --- .../src/codegen_cprover_gotoc/codegen/intrinsic.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/operand.rs | 2 +- kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 8 ++++---- tests/perf/format/src/lib.rs | 4 ++-- 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 7084b38bf75a..4bd5566f9d7c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -581,7 +581,7 @@ impl<'tcx> GotocCtx<'tcx> { } "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr" | "unchecked_sub" => { - unreachable!("Expect intrinsic {intrinsic} to be lowered before codegen") + unreachable!("Expected intrinsic `{intrinsic}` to be lowered before codegen") } "unchecked_div" => codegen_op_with_div_overflow_check!(div), "unchecked_rem" => codegen_op_with_div_overflow_check!(rem), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index fa8565a51cf2..23211f022b23 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -229,7 +229,7 @@ impl<'tcx> GotocCtx<'tcx> { } ty::Adt(def, _) if Some(def.did()) == self.tcx.lang_items().c_str() => { // TODO: Handle CString - // https://github.com/model-checking/kani/issues/2549 + // let loc = self.codegen_span_option(span.cloned()); let typ = self.codegen_ty(lit_ty); let operation_name = "C string literal"; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 097d501a72bc..cefa994d963e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -163,7 +163,7 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// Generate code for a binary operation with an overflow and returns a tuple (res, overflow). + /// Generate code for a binary operation with an overflow check. fn codegen_binop_with_overflow_check( &mut self, op: &BinOp, @@ -411,7 +411,7 @@ impl<'tcx> GotocCtx<'tcx> { /// For integer types, division by zero is UB, as is MIN / -1 for signed. /// Note that the compiler already inserts these checks for regular division. /// However, since , unchecked divisions are - /// lowered to BinOp::Div. Prefer adding duplicated checks for now. + /// lowered to `BinOp::Div`. Prefer adding duplicated checks for now. fn check_div_overflow( &mut self, dividend: &Operand<'tcx>, @@ -422,7 +422,7 @@ impl<'tcx> GotocCtx<'tcx> { let div_by_zero_check = self.codegen_assert_assume( divisor_expr.clone().is_zero().not(), PropertyClass::ArithmeticOverflow, - "Attempt to divide by 0", + "attempt to divide by 0", loc, ); if self.operand_ty(dividend).is_signed() { @@ -434,7 +434,7 @@ impl<'tcx> GotocCtx<'tcx> { let overflow_check = self.codegen_assert_assume( overflow_expr.not(), PropertyClass::ArithmeticOverflow, - "Attempt to compute `MIN / -1` which would overflow", + "attempt to compute `MIN / -1` which would overflow", loc, ); Stmt::block(vec![overflow_check, div_by_zero_check], loc) diff --git a/tests/perf/format/src/lib.rs b/tests/perf/format/src/lib.rs index ad14c6288e7c..1986a08222ba 100644 --- a/tests/perf/format/src/lib.rs +++ b/tests/perf/format/src/lib.rs @@ -2,8 +2,8 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This test checks the performance of calling format. -//! This tests capture the performance regression introduced by the toolchain upgrade #2551. -//! See https://github.com/model-checking/kani/issues/2576 for more details. +//! This test captures the performance regression introduced by the toolchain upgrade in +//! See for more details. #[kani::proof] fn fmt_i8() { From 441734bede507932eaf72d213031fc0251ce6216 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 3 Jul 2023 15:40:45 -0700 Subject: [PATCH 6/6] Address PR comments + improve check message --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 18 +++++-- .../compiler_interface.rs | 2 +- ...igned.expected => check_unsigned.expected} | 0 tests/cargo-kani/itoa_dep/src/main.rs | 8 +++ tests/ui/duplicates/dup_checks.rs | 19 +++++++ tests/ui/duplicates/expected | 49 +++++++++++++++++++ 6 files changed, 92 insertions(+), 4 deletions(-) rename tests/cargo-kani/itoa_dep/{check_signed.expected => check_unsigned.expected} (100%) create mode 100644 tests/ui/duplicates/dup_checks.rs create mode 100644 tests/ui/duplicates/expected diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index cefa994d963e..22b26a3489b4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -354,7 +354,8 @@ impl<'tcx> GotocCtx<'tcx> { BinOp::Div | BinOp::Rem => { let result = self.codegen_unchecked_scalar_binop(op, e1, e2); if self.operand_ty(e1).is_integral() { - let check = self.check_div_overflow(e1, e2, loc); + let is_rem = matches!(op, BinOp::Rem); + let check = self.check_div_overflow(e1, e2, is_rem, loc); Expr::statement_expression( vec![check, result.clone().as_stmt(loc)], result.typ().clone(), @@ -416,17 +417,28 @@ impl<'tcx> GotocCtx<'tcx> { &mut self, dividend: &Operand<'tcx>, divisor: &Operand<'tcx>, + is_remainder: bool, loc: Location, ) -> Stmt { let divisor_expr = self.codegen_operand(divisor); + let msg = if is_remainder { + "attempt to calculate the remainder with a divisor of zero" + } else { + "attempt to divide by zero" + }; let div_by_zero_check = self.codegen_assert_assume( divisor_expr.clone().is_zero().not(), PropertyClass::ArithmeticOverflow, - "attempt to divide by 0", + msg, loc, ); if self.operand_ty(dividend).is_signed() { let dividend_expr = self.codegen_operand(dividend); + let overflow_msg = if is_remainder { + "attempt to calculate the remainder with overflow" + } else { + "attempt to divide with overflow" + }; let overflow_expr = dividend_expr .clone() .eq(dividend_expr.typ().min_int_expr(self.symbol_table.machine_model())) @@ -434,7 +446,7 @@ impl<'tcx> GotocCtx<'tcx> { let overflow_check = self.codegen_assert_assume( overflow_expr.not(), PropertyClass::ArithmeticOverflow, - "attempt to compute `MIN / -1` which would overflow", + overflow_msg, loc, ); Stmt::block(vec![overflow_check, div_by_zero_check], loc) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 64e2ae3f4d4c..a89e5035f2a2 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -321,7 +321,7 @@ impl CodegenBackend for GotocCodegenBackend { match ongoing_codegen.downcast::<(CodegenResults, FxIndexMap)>() { Ok(val) => Ok(*val), - Err(val) => panic!("Oh no: {:?}", val.type_id()), + Err(val) => panic!("unexpected error: {:?}", val.type_id()), } } diff --git a/tests/cargo-kani/itoa_dep/check_signed.expected b/tests/cargo-kani/itoa_dep/check_unsigned.expected similarity index 100% rename from tests/cargo-kani/itoa_dep/check_signed.expected rename to tests/cargo-kani/itoa_dep/check_unsigned.expected diff --git a/tests/cargo-kani/itoa_dep/src/main.rs b/tests/cargo-kani/itoa_dep/src/main.rs index ea729e7c1c20..c2d1a165a409 100644 --- a/tests/cargo-kani/itoa_dep/src/main.rs +++ b/tests/cargo-kani/itoa_dep/src/main.rs @@ -17,9 +17,17 @@ fn check_itoa() { assert_eq!(result, &output); } +/// Note: We ignore this harness for now due to a performance regression. +/// See for more details. #[kani::proof] #[kani::unwind(10)] fn check_signed() { + check_itoa::(); +} + +#[kani::proof] +#[kani::unwind(10)] +fn check_unsigned() { check_itoa::(); } diff --git a/tests/ui/duplicates/dup_checks.rs b/tests/ui/duplicates/dup_checks.rs new file mode 100644 index 000000000000..a1b45d52cc05 --- /dev/null +++ b/tests/ui/duplicates/dup_checks.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Test that captures how Kani implements various redundant checks +//! for the same operation. This can be confusing for the user, since +//! the duplicated check will always succeed, even when the first check fails. +//! + +use std::hint::black_box; + +#[kani::proof] +fn check_division() { + black_box(kani::any::() / kani::any::()); +} + +#[kani::proof] +fn check_remainder() { + black_box(kani::any::() % kani::any::()); +} diff --git a/tests/ui/duplicates/expected b/tests/ui/duplicates/expected new file mode 100644 index 000000000000..9e6b135283d6 --- /dev/null +++ b/tests/ui/duplicates/expected @@ -0,0 +1,49 @@ +Checking harness check_remainder... + +RESULTS: +check_remainder.assertion\ +Status: FAILURE\ +Description: "attempt to calculate the remainder with a divisor of zero" + +check_remainder.assertion\ +Status: FAILURE\ +Description: "attempt to calculate the remainder with overflow" + +check_remainder.arithmetic_overflow\ +Status: SUCCESS\ +Description: "attempt to calculate the remainder with overflow" + +check_remainder.arithmetic_overflow\ +Status: SUCCESS\ +Description: "attempt to calculate the remainder with a divisor of zero" + +check_remainder.division-by-zero\ +Status: SUCCESS\ +Description: "division by zero" + +Failed Checks: attempt to calculate the remainder with a divisor of zero +Failed Checks: attempt to calculate the remainder with overflow + +Checking harness check_division... +check_division.assertion\ +Status: FAILURE\ +Description: "attempt to divide by zero" + +check_division.assertion\ +Status: FAILURE\ +Description: "attempt to divide with overflow" + +check_division.arithmetic_overflow\ +Status: SUCCESS\ +Description: "attempt to divide with overflow" + +check_division.arithmetic_overflow\ +Status: SUCCESS\ +Description: "attempt to divide by zero" + +check_division.division-by-zero\ +Status: SUCCESS\ +Description: "division by zero" + +Failed Checks: attempt to divide by zero +Failed Checks: attempt to divide with overflow