Merge branch 'main' into simd-div-overflow

.github/actions/setup/action.yml

@@ -12,6 +12,14 @@ inputs:
 runs:
   using: composite
   steps:
+      - name: Remove unnecessary software to free up disk space
+        shell: bash
+        run: |
+          # inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
+          df -h
+          sudo rm -rf /usr/share/dotnet /usr/local/lib/android /opt/ghc
+          df -h
+
       - name: Install dependencies
         run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh
         shell: bash

kani-compiler/src/kani_middle/attributes.rs

@@ -374,7 +374,7 @@ fn parse_unwind(tcx: TyCtxt, attr: &Attribute) -> Option<u32> {
 fn parse_stubs(tcx: TyCtxt, harness: DefId, attributes: &[&Attribute]) -> Vec<Stub> {
     let current_module = tcx.parent_module_from_def_id(harness.expect_local());
     let check_resolve = |attr: &Attribute, name: &str| {
-        let result = resolve::resolve_fn(tcx, current_module, name);
+        let result = resolve::resolve_fn(tcx, current_module.to_local_def_id(), name);
         if let Err(err) = result {
             tcx.sess.span_err(attr.span, format!("failed to resolve `{name}`: {err}"));
         }

kani-compiler/src/kani_middle/resolve.rs

@@ -14,7 +14,7 @@ use std::fmt;
 use std::iter::Peekable;
 
 use rustc_hir::def::{DefKind, Res};
-use rustc_hir::def_id::{DefId, LocalDefId, CRATE_DEF_INDEX, LOCAL_CRATE};
+use rustc_hir::def_id::{DefId, LocalDefId, LocalModDefId, CRATE_DEF_INDEX, LOCAL_CRATE};
 use rustc_hir::{ItemKind, UseKind};
 use rustc_middle::ty::TyCtxt;
 use tracing::debug;
@@ -278,7 +278,7 @@ enum RelativeResolution {
 }
 
 /// Resolves a path relative to a local module.
-fn resolve_relative(tcx: TyCtxt, current_module: LocalDefId, name: &str) -> RelativeResolution {
+fn resolve_relative(tcx: TyCtxt, current_module: LocalModDefId, name: &str) -> RelativeResolution {
     debug!(?name, ?current_module, "resolve_relative");
 
     let mut glob_imports = vec![];
@@ -318,7 +318,7 @@ fn resolve_in_module<'tcx>(
             ResolveError::MissingItem { tcx, base: current_module, unresolved: name.to_string() }
         }),
         Some(local_id) => {
-            let result = resolve_relative(tcx, local_id, name);
+            let result = resolve_relative(tcx, LocalModDefId::new_unchecked(local_id), name);
             match result {
                 RelativeResolution::Found(def_id) => Ok(def_id),
                 RelativeResolution::Globs(globs) => {
@@ -372,7 +372,7 @@ fn resolve_in_glob_uses<'tcx>(
 fn resolve_in_glob_use(tcx: TyCtxt, res: &Res, name: &str) -> RelativeResolution {
     if let Res::Def(DefKind::Mod, def_id) = res {
         if let Some(local_id) = def_id.as_local() {
-            resolve_relative(tcx, local_id, name)
+            resolve_relative(tcx, LocalModDefId::new_unchecked(local_id), name)
         } else {
             resolve_in_foreign_module(tcx, *def_id, name)
                 .map_or(RelativeResolution::Globs(vec![]), RelativeResolution::Found)

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

@@ -18,7 +18,7 @@ fn stub_def_ids(tcx: TyCtxt, harness: LocalDefId, stub: &Stub) -> Option<(DefId,
     // Resolve the attribute arguments to `DefId`s
     let current_module = tcx.parent_module_from_def_id(harness);
     let resolve = |name: &str| -> Option<DefId> {
-        let maybe_resolved = resolve_fn(tcx, current_module, name);
+        let maybe_resolved = resolve_fn(tcx, current_module.to_local_def_id(), name);
         match maybe_resolved {
             Ok(def_id) => {
                 tracing::debug!(?def_id, "Resolved {name} to {}", tcx.def_path_str(def_id));

rust-toolchain.toml

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