Update Kani to Rust nightly-2022-10-11 (#1788)

tedinski · web-flow · commit 91a608d4082b · 2022-10-14T17:22:06.000-05:00
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -404,8 +404,11 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
-        if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") {
-            let _n: u64 = stripped.parse().unwrap();
+        if let Some(_stripped) = intrinsic.strip_prefix("simd_shuffle") {
+            // TODO: can be empty now (i.e. `simd_shuffle` instead of `simd_shuffle8`)
+            // `parse` fails on empty, so comment that bit of code out.
+            // To re-enable this we'll need to investigate how size is computed now.
+            // let n: u64 = stripped.parse().unwrap();
             return unstable_codegen!(self.codegen_intrinsic_simd_shuffle(
                 fargs,
                 p,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -9,7 +9,7 @@ use rustc_ast::ast::Mutability;
 use rustc_middle::mir::interpret::{
     read_target_uint, AllocId, Allocation, ConstValue, GlobalAlloc, Scalar,
 };
-use rustc_middle::mir::{Constant, ConstantKind, Operand};
+use rustc_middle::mir::{Constant, ConstantKind, Operand, UnevaluatedConst};
 use rustc_middle::ty::layout::LayoutOf;
 use rustc_middle::ty::{self, Const, ConstKind, FloatTy, Instance, IntTy, Ty, Uint, UintTy};
 use rustc_span::def_id::DefId;
@@ -47,28 +47,37 @@ 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)),
-        };
+        let span = Some(&c.span);
+        match self.monomorphize(c.literal) {
+            ConstantKind::Ty(ct) => self.codegen_const(ct, span),
+            ConstantKind::Val(val, ty) => self.codegen_const_value(val, ty, span),
+            ConstantKind::Unevaluated(unevaluated, ty) => {
+                self.codegen_const_unevaluated(unevaluated, ty, span)
+            }
+        }
+    }
 
-        self.codegen_const(const_, Some(&c.span))
+    fn codegen_const_unevaluated(
+        &mut self,
+        unevaluated: UnevaluatedConst<'tcx>,
+        ty: Ty<'tcx>,
+        span: Option<&Span>,
+    ) -> Expr {
+        debug!(?unevaluated, "codegen_const_unevaluated");
+        let const_val =
+            self.tcx.const_eval_resolve(ty::ParamEnv::reveal_all(), unevaluated, None).unwrap();
+        self.codegen_const_value(const_val, ty, span)
     }
 
     pub fn codegen_const(&mut self, lit: Const<'tcx>, span: Option<&Span>) -> Expr {
         debug!("found literal: {:?}", lit);
         let lit = self.monomorphize(lit);
 
         match lit.kind() {
-            // evaluate constant if it has no been evaluated yet
-            ConstKind::Unevaluated(unevaluated) => {
-                debug!("The literal was a Unevaluated");
-                let const_val = self
-                    .tcx
-                    .const_eval_resolve(ty::ParamEnv::reveal_all(), unevaluated, None)
-                    .unwrap();
-                self.codegen_const_value(const_val, lit.ty(), span)
-            }
+            // A `ConstantKind::Ty(ConstKind::Unevaluated)` should no longer show up
+            // and should be a `ConstantKind::Unevaluated` instead (and thus handled
+            // at the level of `codegen_constant` instead of `codegen_const`.)
+            ConstKind::Unevaluated(_) => unreachable!(),
 
             ConstKind::Value(valtree) => {
                 let value = self.tcx.valtree_to_const_val((lit.ty(), valtree));
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -547,6 +547,13 @@ impl<'tcx> GotocCtx<'tcx> {
                     self,
                 )
             }
+            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
@@ -402,7 +402,12 @@ impl<'tcx> GotocCtx<'tcx> {
             // Rust has begun distinguishing "ptr -> num" and "num -> ptr" (providence-relevant casts) but we do not yet:
             // Should we? Tracking ticket: https://github.com/model-checking/kani/issues/1274
             Rvalue::Cast(
-                CastKind::Misc
+                CastKind::IntToInt
+                | CastKind::FloatToFloat
+                | CastKind::FloatToInt
+                | CastKind::IntToFloat
+                | CastKind::FnPtrToPtr
+                | CastKind::PtrToPtr
                 | CastKind::PointerExposeAddress
                 | CastKind::PointerFromExposedAddress,
                 e,
@@ -411,6 +416,15 @@ impl<'tcx> GotocCtx<'tcx> {
                 let t = self.monomorphize(*t);
                 self.codegen_misc_cast(e, t)
             }
+            Rvalue::Cast(CastKind::DynStar, _, _) => {
+                let ty = self.codegen_ty(res_ty);
+                self.codegen_unimplemented_expr(
+                    "CastKind::DynStar",
+                    ty,
+                    loc,
+                    "https://github.com/model-checking/kani/issues/1784",
+                )
+            }
             Rvalue::Cast(CastKind::Pointer(k), e, t) => {
                 let t = self.monomorphize(*t);
                 self.codegen_pointer_cast(k, e, t, loc)
@@ -636,7 +650,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 // this is a noop in the case dst_subt is a Projection or Opaque type
                 dst_subt = self.tcx.normalize_erasing_regions(ty::ParamEnv::reveal_all(), dst_subt);
                 match dst_subt.kind() {
-                    ty::Slice(_) | ty::Str | ty::Dynamic(_, _) => {
+                    ty::Slice(_) | ty::Str | ty::Dynamic(_, _, _) => {
                         //TODO: this does the wrong thing on Strings/fixme_boxed_str.rs
                         // if we cast to slice or string, then we know the source is also a slice or string,
                         // so there shouldn't be anything to do
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -555,7 +555,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// We follow the order from the `TyCtxt::COMMON_VTABLE_ENTRIES`.
     fn trait_vtable_field_types(&mut self, t: ty::Ty<'tcx>) -> Vec<DatatypeComponent> {
         let mut vtable_base = common_vtable_fields(self.trait_vtable_drop_type(t));
-        if let ty::Dynamic(binder, _region) = t.kind() {
+        if let ty::Dynamic(binder, _, _) = t.kind() {
             // The virtual methods on the trait ref. Some auto traits have no methods.
             if let Some(principal) = binder.principal() {
                 let poly = principal.with_self_ty(self.tcx, t);
@@ -710,7 +710,7 @@ impl<'tcx> GotocCtx<'tcx> {
     /// codegen for types. it finds a C type which corresponds to a rust type.
     /// that means [ty] has to be monomorphized before calling this function.
     ///
-    /// check [rustc_middle::ty::layout::LayoutCx::layout_of_uncached] for LLVM codegen
+    /// check `rustc_ty_utils::layout::layout_of_uncached` for LLVM codegen
     ///
     /// also c.f. <https://www.ralfj.de/blog/2020/04/04/layout-debugging.html>
     ///      c.f. <https://rust-lang.github.io/unsafe-code-guidelines/introduction.html>
diff --git a/kani-compiler/src/codegen_cprover_gotoc/reachability.rs b/kani-compiler/src/codegen_cprover_gotoc/reachability.rs
@@ -29,8 +29,8 @@ use rustc_middle::ty::adjustment::CustomCoerceUnsized;
 use rustc_middle::ty::adjustment::PointerCast;
 use rustc_middle::ty::TypeAndMut;
 use rustc_middle::ty::{
-    self, Closure, ClosureKind, Const, ConstKind, Instance, InstanceDef, ParamEnv, TraitRef, Ty,
-    TyCtxt, TyKind, TypeFoldable, VtblEntry,
+    self, Closure, ClosureKind, ConstKind, Instance, InstanceDef, ParamEnv, TraitRef, Ty, TyCtxt,
+    TyKind, TypeFoldable, VtblEntry,
 };
 use rustc_span::def_id::DefId;
 use tracing::{debug, debug_span, trace, warn};
@@ -337,22 +337,7 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
             ConstantKind::Val(const_val, _) => const_val,
             ConstantKind::Ty(ct) => match ct.kind() {
                 ConstKind::Value(v) => self.tcx.valtree_to_const_val((ct.ty(), v)),
-                ConstKind::Unevaluated(un_eval) => {
-                    // Thread local fall into this category.
-                    match self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, None) {
-                        // The `monomorphize` call should have evaluated that constant already.
-                        Ok(const_val) => const_val,
-                        Err(ErrorHandled::TooGeneric) => span_bug!(
-                            self.body.source_info(location).span,
-                            "Unexpected polymorphic constant: {:?}",
-                            literal
-                        ),
-                        Err(error) => {
-                            warn!(?error, "Error already reported");
-                            return;
-                        }
-                    }
-                }
+                ConstKind::Unevaluated(_) => unreachable!(),
                 // Nothing to do
                 ConstKind::Param(..) | ConstKind::Infer(..) | ConstKind::Error(..) => return,
 
@@ -361,15 +346,26 @@ impl<'a, 'tcx> MirVisitor<'tcx> for MonoItemsFnCollector<'a, 'tcx> {
                     unreachable!("Unexpected constant type {:?} ({:?})", ct, ct.kind())
                 }
             },
+            ConstantKind::Unevaluated(un_eval, _) => {
+                // Thread local fall into this category.
+                match self.tcx.const_eval_resolve(ParamEnv::reveal_all(), un_eval, None) {
+                    // The `monomorphize` call should have evaluated that constant already.
+                    Ok(const_val) => const_val,
+                    Err(ErrorHandled::TooGeneric) => span_bug!(
+                        self.body.source_info(location).span,
+                        "Unexpected polymorphic constant: {:?}",
+                        literal
+                    ),
+                    Err(error) => {
+                        warn!(?error, "Error already reported");
+                        return;
+                    }
+                }
+            }
         };
         self.collect_const_value(val);
     }
 
-    fn visit_const(&mut self, constant: Const<'tcx>, location: Location) {
-        trace!(?constant, ?location, "visit_const");
-        self.super_const(constant);
-    }
-
     /// Collect function calls.
     fn visit_terminator(&mut self, terminator: &Terminator<'tcx>, location: Location) {
         trace!(?terminator, ?location, "visit_terminator");
diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs
@@ -12,7 +12,7 @@ use serde::{Deserialize, Serialize};
 /// The structure of `.kani-metadata.json` files, which are emitted for each crate
 #[derive(Debug, Clone, Serialize, Deserialize)]
 pub struct KaniMetadata {
-    /// The proof harnesses (#[kani::proof]) found in this crate.
+    /// The proof harnesses (`#[kani::proof]`) found in this crate.
     pub proof_harnesses: Vec<HarnessMetadata>,
     /// The features found in this crate that Kani does not support.
     /// (These general translate to `assert(false)` so we can still attempt verification.)
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-09-13"
+channel = "nightly-2022-10-11"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/tests/kani/Intrinsics/Assert/uninit_valid_panic.rs b/tests/kani/Intrinsics/Assert/uninit_valid_panic.rs
@@ -5,11 +5,11 @@
 #![feature(core_intrinsics)]
 use std::intrinsics;
 
-// The code below attempts to leave type `bool` uninitialized, causing the
+// The code below attempts to leave type `&u32` uninitialized, causing the
 // intrinsic `assert_uninit_valid` to generate a panic during compilation.
 #[kani::proof]
 fn main() {
     let _var: () = unsafe {
-        intrinsics::assert_uninit_valid::<bool>();
+        intrinsics::assert_uninit_valid::<&u32>();
     };
 }
diff --git a/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs b/tests/kani/ProjectionElem/OpaqueCast/check_opaque_cast.rs
@@ -2,10 +2,6 @@
 //
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
-//
-// NOTE: The initial fix for this has been reverted from rustc. I'm keeping this test here so we
-// will know when it has been reverted back.
-// kani-check-fail
 
 //! Tests that check handling of opaque casts. Tests were adapted from the rustc repository.
 
diff --git 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:2921:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
+alloc/src/vec/mod.rs:3031:81 in function <std::vec::Vec<i32> as std::ops::Drop>::drop
 
 VERIFICATION:- SUCCESSFUL
diff --git a/tools/bookrunner/librustdoc/lib.rs b/tools/bookrunner/librustdoc/lib.rs
@@ -12,7 +12,6 @@
 #![feature(box_patterns)]
 #![feature(control_flow_enum)]
 #![feature(box_syntax)]
-#![feature(let_else)]
 #![feature(test)]
 #![feature(never_type)]
 #![feature(once_cell)]
@@ -62,7 +61,6 @@ extern crate rustc_session;
 extern crate rustc_span;
 extern crate rustc_target;
 extern crate rustc_trait_selection;
-extern crate rustc_typeck;
 extern crate test;
 
 pub mod doctest;
diff --git a/tools/compiletest/src/main.rs b/tools/compiletest/src/main.rs
@@ -511,5 +511,8 @@ fn make_test_closure(
     let config = config.clone();
     let testpaths = testpaths.clone();
     let revision = revision.cloned();
-    test::DynTestFn(Box::new(move || runtest::run(config, &testpaths, revision.as_deref())))
+    test::DynTestFn(Box::new(move || {
+        runtest::run(config, &testpaths, revision.as_deref());
+        Ok(())
+    }))
 }

Original file line number	Diff line number	Diff line change
`@@ -547,6 +547,13 @@ impl<'tcx> GotocCtx<'tcx> {`
`547`	`547`	`self,`
`548`	`548`	`)`
`549`	`549`	`}`
	`550`	`+ ProjectionElem::OpaqueCast(ty) => ProjectedPlace::try_new(`
	`551`	`+ before.goto_expr.cast_to(self.codegen_ty(ty)),`
	`552`	`+ TypeOrVariant::Type(ty),`
	`553`	`+ before.fat_ptr_goto_expr,`
	`554`	`+ before.fat_ptr_mir_typ,`
	`555`	`+ self,`
	`556`	`+ ),`
`550`	`557`	`}`
`551`	`558`	`}`
`552`	`559`