Update toolchain to nightly-2022-07-19 (#1399)

* Update toolchain to nightly-2022-07-19 This update required the following changes: - Add support to ProjectionElem::OpaqueCast - Add support to Rvalue::CopyForDeref - Add support to ConstValue::ZST - Rename debugging_opts to unstable_opts - Change to mem::uninit/zeroed validity checks - Change vecdeque harness due to std capacity check Co-authored-by: Adrian Palacios <[email protected]>
model-checking · Jul 22, 2022 · b154ec9 · b154ec9
1 parent 5c590a4
commit b154ec9
Show file tree

Hide file tree

Showing 11 changed files with 106 additions and 17 deletions.
diff --git 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
@@ -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,19 +766,15 @@ 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),
                 span,
             );
         }
 
-        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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -0,0 +1,16 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+/// Adapted from:
+/// <https://github.com/rust-lang/rust/blob/29c5a028b0c92aa5da6a8eb6d6585a389fcf1035/src/test/mir-opt/derefer_test.rs>
+#[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
@@ -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:
+/// <https://github.com/rust-lang/rust/blob/29c5a028b0c92aa5da6a8eb6d6585a389fcf1035/src/test/ui/type-alias-impl-trait/issue-96572-unconstrained-upvar.rs>
+#[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:
+/// <https://github.com/rust-lang/rust/blob/29c5a028b0c92aa5da6a8eb6d6585a389fcf1035/src/test/ui/type-alias-impl-trait/issue-96572-unconstrained-struct.rs>
+#[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:
+/// <https://github.com/rust-lang/rust/issues/96572#issuecomment-1125117692>
+#[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)
+        }
+    }
+}