Regression now passes

- Use internal to go around is_foreign_item() issue
- Update tests after an issue:
  rust-lang/rust#116915
- Update the toolchain

Author: celinval

kani-compiler/src/kani_middle/reachability.rs

@@ -153,7 +153,11 @@ impl<'tcx> MonoItemsCollector<'tcx> {
     /// instruction looking for the items that should be included in the compilation.
     fn reachable_items(&mut self) {
         while let Some(to_visit) = self.queue.pop() {
-            if !self.collected.contains(&to_visit) {
+            // TODO: This should only check is_foreign_item() or even `has_body()`.
+            // We need https://github.com/rust-lang/rust/pull/118681 to land first.
+            if !self.collected.contains(&to_visit)
+                && !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id())
+            {
                 self.collected.insert(to_visit.clone());
                 let next_items = match &to_visit {
                     MonoItem::Fn(instance) => self.visit_fn(*instance),
@@ -485,10 +489,7 @@ fn to_fingerprint(tcx: TyCtxt, item: &InternalMonoItem) -> Fingerprint {
 
 /// Return whether we should include the item into codegen.
 fn should_codegen_locally(instance: &Instance) -> bool {
-    // TODO: This should only check is_foreign_item() or even `has_body()`.
-    // We need https://github.com/rust-lang/rust/pull/118681 to land first.
-    //!instance.is_foreign_item()
-    instance.body().is_some()
+    !instance.is_foreign_item()
 }
 
 fn collect_alloc_items(alloc_id: AllocId) -> Vec<MonoItem> {

kani-compiler/src/kani_middle/stubbing/mod.rs

@@ -46,6 +46,7 @@ pub fn harness_stub_map(
 pub fn validate_instance(tcx: TyCtxt, instance: Instance) -> bool {
     let internal_instance = rustc_internal::internal(instance);
     if get_stub(tcx, internal_instance.def_id()).is_some() {
+        debug!(?instance, "validate_instance");
         let item = CrateItem::try_from(instance).unwrap();
         let mut checker = StubConstChecker::new(tcx, internal_instance, item);
         checker.visit_body(&item.body());

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-12-03"
+channel = "nightly-2023-12-07"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

tests/expected/any_vec/exact_length.expected

@@ -1,12 +1,12 @@
 Checking harness check_access_length_17...
 
-Failed Checks: dereference failure: pointer outside object bounds\
-in check_access_length_17
+Failed Checks: assumption failed\
+in <usize as std::slice::SliceIndex<[Dummy]>>::get_unchecked
 
 Checking harness check_access_length_zero...
 
-Failed Checks: dereference failure: pointer outside object bounds\
-in check_access_length_zero
+Failed Checks: assumption failed\
+in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
 Verification failed for - check_access_length_17
 Verification failed for - check_access_length_zero

tests/expected/any_vec/out_bounds.expected

@@ -1,61 +1,6 @@
-check_always_out_bounds::check_0.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer NULL"\
-function check_always_out_bounds::check_0
-
-check_always_out_bounds::check_0.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_0
-
-check_always_out_bounds::check_0.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: invalid integer address"\
-function check_always_out_bounds::check_0
-
-check_always_out_bounds::check_1.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_1
-
-check_always_out_bounds::check_2.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_2
-
-check_always_out_bounds::check_3.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_3
-
-check_always_out_bounds::check_4.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_4
-
-check_always_out_bounds::check_5.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_5
-
-check_always_out_bounds::check_6.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_6
-
-check_always_out_bounds::check_7.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_7
-
-check_always_out_bounds::check_8.pointer_dereference\
-Status: FAILURE\
-Description: "dereference failure: pointer outside object bounds"\
-function check_always_out_bounds::check_8
-
-check_always_out_bounds::check_9.cover\
-Status: UNREACHABLE\
-Description: "cover condition: *val == 0"\
-function check_always_out_bounds::check_9
+Checking harness check_always_out_bounds...
 
+Failed Checks: assumption failed
+in <usize as std::slice::SliceIndex<[u8]>>::get_unchecked
 
+Verification failed for - check_always_out_bounds