diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 838ff8855840..6a176aaf20a6 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -562,7 +562,14 @@ impl Expr { // For variadic functions, all named arguments must match the type of their formal param. // Extra arguments (e.g the ... args) can have any type. fn typecheck_named_args(parameters: &[Parameter], arguments: &[Expr]) -> bool { - parameters.iter().zip(arguments.iter()).all(|(p, a)| a.typ() == p.typ()) + parameters.iter().zip(arguments.iter()).all(|(p, a)| { + if a.typ() == p.typ() { + true + } else { + tracing::error!(param=?p.typ(), arg=?a.typ(), "Argument doesn't check"); + false + } + }) } if function.typ().is_code() { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index c3bc7974dd74..f12a88c9ed3e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -10,7 +10,6 @@ use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{self, Ty}; use rustc_middle::ty::{Instance, InstanceDef}; use rustc_span::Span; -use rustc_target::abi::InitKind; use tracing::{debug, warn}; macro_rules! emit_concurrency_warning { @@ -767,9 +766,7 @@ impl<'tcx> GotocCtx<'tcx> { // Then we check if the type allows "raw" initialization for the cases // where memory is zero-initialized or entirely uninitialized - if intrinsic == "assert_zero_valid" - && !layout.might_permit_raw_init(self, InitKind::Zero, false) - { + if intrinsic == "assert_zero_valid" && !self.tcx.permits_zero_init(layout) { return self.codegen_fatal_error( PropertyClass::SafetyCheck, &format!("attempted to zero-initialize type `{}`, which is invalid", ty), @@ -777,9 +774,7 @@ impl<'tcx> GotocCtx<'tcx> { ); } - if intrinsic == "assert_uninit_valid" - && !layout.might_permit_raw_init(self, InitKind::Uninit, false) - { + if intrinsic == "assert_uninit_valid" && !self.tcx.permits_uninit_init(layout) { return self.codegen_fatal_error( PropertyClass::SafetyCheck, &format!("attempted to leave type `{}` uninitialized, which is invalid", ty), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 9ed99ca78d2d..4f8e8a11c8b4 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -14,7 +14,7 @@ use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uin use rustc_span::def_id::DefId; use rustc_span::Span; use rustc_target::abi::{FieldsShape, Size, TagEncoding, Variants}; -use tracing::debug; +use tracing::{debug, trace}; enum AllocData<'a> { Bytes(&'a [u8]), @@ -23,6 +23,7 @@ enum AllocData<'a> { impl<'tcx> GotocCtx<'tcx> { pub fn codegen_operand(&mut self, o: &Operand<'tcx>) -> Expr { + trace!(operand=?o, "codegen_operand"); match o { Operand::Copy(d) | Operand::Move(d) => // TODO: move shouldn't be the same as copy @@ -44,6 +45,7 @@ impl<'tcx> GotocCtx<'tcx> { } fn codegen_constant(&mut self, c: &Constant<'tcx>) -> Expr { + trace!(constant=?c, "codegen_constant"); let const_ = match self.monomorphize(c.literal) { ConstantKind::Ty(ct) => ct, ConstantKind::Val(val, ty) => return self.codegen_const_value(val, ty, Some(&c.span)), @@ -145,6 +147,7 @@ impl<'tcx> GotocCtx<'tcx> { lit_ty: Ty<'tcx>, span: Option<&Span>, ) -> Expr { + trace!(val=?v, ?lit_ty, "codegen_const_value"); match v { ConstValue::Scalar(s) => self.codegen_scalar(s, lit_ty, span), ConstValue::Slice { data, start, end } => { @@ -160,11 +163,15 @@ impl<'tcx> GotocCtx<'tcx> { .cast_to(self.codegen_ty(lit_ty).to_pointer()) .dereference() } + ConstValue::ZeroSized => match lit_ty.kind() { + ty::FnDef(d, substs) => self.codegen_fndef(*d, substs, span), + _ => unimplemented!(), + }, } } fn codegen_scalar(&mut self, s: Scalar, ty: Ty<'tcx>, span: Option<&Span>) -> Expr { - debug! {"codegen_scalar\n{:?}\n{:?}\n{:?}\n{:?}",s, ty, span, &ty.kind()}; + debug!(scalar=?s, ?ty, kind=?ty.kind(), ?span, "codegen_scalar"); match (s, &ty.kind()) { (Scalar::Int(_), ty::Int(it)) => match it { IntTy::I8 => Expr::int_constant(s.to_i8().unwrap(), Type::signed_int(8)), @@ -199,9 +206,9 @@ impl<'tcx> GotocCtx<'tcx> { FloatTy::F64 => Expr::double_constant_from_bitpattern(s.to_u64().unwrap()), } } - (Scalar::Int(int), ty::FnDef(d, substs)) => { - assert_eq!(int.size(), Size::ZERO); - self.codegen_fndef(*d, substs, span) + (Scalar::Int(..), ty::FnDef(..)) => { + // This was removed here: https://github.com/rust-lang/rust/pull/98957. + unreachable!("ZST is no longer represented as a scalar") } (Scalar::Int(_), ty::RawPtr(tm)) => { Expr::pointer_constant(s.to_u64().unwrap(), self.codegen_ty(tm.ty).to_pointer()) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index d35e6e6d8bf3..40ded58a10e9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -526,6 +526,13 @@ impl<'tcx> GotocCtx<'tcx> { _ => unreachable!("it's a bug to reach here!"), } } + ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new( + before.goto_expr.cast_to(self.codegen_ty(ty)), + TypeOrVariant::Type(ty), + before.fat_ptr_goto_expr, + before.fat_ptr_mir_typ, + self, + ), } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 2ebee75d7f0c..37ddb6e91ad7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -419,6 +419,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_rvalue(&mut self, rv: &Rvalue<'tcx>, loc: Location) -> Expr { let res_ty = self.rvalue_ty(rv); + 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), @@ -493,6 +494,11 @@ impl<'tcx> GotocCtx<'tcx> { "https://github.com/model-checking/kani/issues/541", ) } + // A CopyForDeref is equivalent to a read from a place at the codegen level. + // https://github.com/rust-lang/rust/blob/1673f1450eeaf4a5452e086db0fe2ae274a0144f/compiler/rustc_middle/src/mir/syntax.rs#L1055 + Rvalue::CopyForDeref(place) => { + unwrap_or_return_codegen_unimplemented!(self, self.codegen_place(place)).goto_expr + } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 39b2c7a0b009..d68f9481b31e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -361,6 +361,7 @@ impl<'tcx> GotocCtx<'tcx> { .filter_map(|o| { let ot = self.operand_ty(o); if self.ignore_var_ty(ot) { + trace!(operand=?o, typ=?ot, "codegen_funcall_args ignore"); None } else if ot.is_bool() { Some(self.codegen_operand(o).cast_to(Type::c_bool())) @@ -618,7 +619,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_statement(&mut self, stmt: &Statement<'tcx>) -> Stmt { let _trace_span = info_span!("CodegenStatement", statement = ?stmt).entered(); - debug!("handling statement {:?}", stmt); + debug!(?stmt, kind=?stmt.kind, "handling_statement"); let location = self.codegen_span(&stmt.source_info.span); match &stmt.kind { StatementKind::Assign(box (l, r)) => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index db3fbda9c69e..1918174a8c63 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -151,7 +151,7 @@ impl CodegenBackend for GotocCodegenBackend { let metadata = KaniMetadata { proof_harnesses: c.proof_harnesses }; // No output should be generated if user selected no_codegen. - if !tcx.sess.opts.debugging_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { + if !tcx.sess.opts.unstable_opts.no_codegen && tcx.sess.opts.output_types.should_codegen() { let outputs = tcx.output_filenames(()); let base_filename = outputs.output_path(OutputType::Object); let pretty = self.queries.get_output_pretty_json(); diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 468e8286bdab..a1e7f9af086c 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2022-07-05" +channel = "nightly-2022-07-19" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] diff --git a/tests/cargo-kani/vecdeque-cve/src/harness.rs b/tests/cargo-kani/vecdeque-cve/src/harness.rs index b4cb038f0f04..5a53c2c517d6 100644 --- a/tests/cargo-kani/vecdeque-cve/src/harness.rs +++ b/tests/cargo-kani/vecdeque-cve/src/harness.rs @@ -22,7 +22,7 @@ mod fixed; mod raw_vec; use abstract_vecdeque::*; -const MAX_CAPACITY: usize = usize::MAX >> 1; +const MAX_CAPACITY: usize = usize::MAX >> 2; /// This module uses a version of VecDeque that includes the CVE fix. mod fixed_proofs { diff --git a/tests/kani/DerefCopy/check_deref_copy.rs b/tests/kani/DerefCopy/check_deref_copy.rs new file mode 100644 index 000000000000..49444c37f34e --- /dev/null +++ b/tests/kani/DerefCopy/check_deref_copy.rs @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +/// Adapted from: +/// +#[kani::proof] +fn check_deref_copy() { + let mut a = (42, 43); + let mut b = (99, &mut a); + let x = &mut (*b.1).0; + let y = &mut (*b.1).1; + assert_eq!(*x, 42); + assert_eq!(*y, 43); +} diff --git a/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs b/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs new file mode 100644 index 000000000000..4fadabd92da2 --- /dev/null +++ b/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs @@ -0,0 +1,50 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +//! Tests that check handling of opaque casts. Tests were adapted from the rustc repository. + +#![feature(type_alias_impl_trait)] + +#[derive(Copy, Clone)] +struct Foo((u32, u32)); + +/// Adapted from: +/// +#[kani::proof] +fn check_unconstrained_upvar() { + type T = impl Copy; + let foo: T = Foo((1u32, 2u32)); + let x = move || { + let Foo((a, b)) = foo; + assert_eq!(a, 1u32); + assert_eq!(b, 2u32); + }; +} + +/// Adapted from: +/// +#[kani::proof] +fn check_unconstrained_struct() { + type U = impl Copy; + let foo: U = Foo((1u32, 2u32)); + let Foo((a, b)) = foo; + assert_eq!(a, 1u32); + assert_eq!(b, 2u32); +} + +/// Adapted from: +/// +#[kani::proof] +fn check_unpack_option_tuple() { + type T = impl Copy; + let foo: T = Some((1u32, 2u32)); + match foo { + None => (), + Some((a, b)) => { + assert_eq!(a, 1u32); + assert_eq!(b, 2u32) + } + } +}