Update Rust toolchain to 2023-09-15 (model-checking#2768)

zhassan-aws · Sep 15, 2023 · c3ff9ea · c3ff9ea
1 parent 7e692bb
commit c3ff9ea
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 6 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
@@ -128,7 +128,8 @@ impl<'tcx> GotocCtx<'tcx> {
             ConstValue::Slice { data, start, end } => {
                 self.codegen_slice_value(v, lit_ty, span, data.inner(), start, end)
             }
-            ConstValue::ByRef { alloc, offset } => {
+            ConstValue::Indirect { alloc_id, offset } => {
+                let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory();
                 debug!("ConstValue by ref {:?} {:?}", alloc, offset);
                 let mem_var = self.codegen_const_allocation(alloc.inner(), None);
                 mem_var

diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
@@ -34,7 +34,6 @@ use rustc_hir::definitions::DefPathHash;
 use rustc_interface::Config;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::{ErrorOutputType, OutputType};
-use rustc_session::EarlyErrorHandler;
 use rustc_span::ErrorGuaranteed;
 use std::collections::{BTreeMap, HashMap};
 use std::fs::File;
@@ -396,7 +395,6 @@ impl Callbacks for KaniCompiler {
     /// During the initialization state, we collect the crate harnesses and prepare for codegen.
     fn after_analysis<'tcx>(
         &mut self,
-        _handler: &EarlyErrorHandler,
         _compiler: &rustc_interface::interface::Compiler,
         rustc_queries: &'tcx rustc_interface::Queries<'tcx>,
     ) -> Compilation {

diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs
@@ -320,8 +320,13 @@ impl<'a, 'tcx> MonoItemsFnCollector<'a, 'tcx> {
             ConstValue::Scalar(Scalar::Ptr(ptr, _size)) => {
                 self.collected.extend(collect_alloc_items(self.tcx, ptr.provenance).iter());
             }
-            ConstValue::Slice { data: alloc, start: _, end: _ }
-            | ConstValue::ByRef { alloc, .. } => {
+            ConstValue::Slice { data: alloc, start: _, end: _ } => {
+                for id in alloc.inner().provenance().provenances() {
+                    self.collected.extend(collect_alloc_items(self.tcx, id).iter())
+                }
+            }
+            ConstValue::Indirect { alloc_id, .. } => {
+                let alloc = self.tcx.global_alloc(alloc_id).unwrap_memory();
                 for id in alloc.inner().provenance().provenances() {
                     self.collected.extend(collect_alloc_items(self.tcx, id).iter())
                 }

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-2023-09-11"
+channel = "nightly-2023-09-15"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]