Merge pull request #99 from os-checker/sync

Sync: update toolchain to 2025-08-01

Author: zjp-CN

.github/gen_core.json.sh

@@ -13,7 +13,7 @@ export VERIFY_RUST_STD_LIBRARY=$WORKSPACE/verify-rust-std/library
 # * update runid after verify-rust-std submodule syncs
 # * update snapshots after runid changes
 rm tmp -rf
-gh run download -D tmp -R model-checking/verify-rust-std 16057809811
+gh run download -D tmp -R model-checking/verify-rust-std 16777123952
 
 ls -alh $VERIFY_RUST_STD_LIBRARY
 

.github/workflows/test.yml

@@ -9,7 +9,8 @@ env:
 
 jobs:
   test:
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04-arm
+    # runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v4
 
@@ -30,7 +31,7 @@ jobs:
         working-directory: assets
         run: |
           ls -alh core.json
-          head -n 1000 core.json
+          head -n 100 core.json
 
       - name: Upload core.json
         uses: actions/upload-artifact@v4
@@ -73,16 +74,16 @@ jobs:
       - name: Kani list
         working-directory: verify-rust-std
         if: ${{ env.AUTO == '' }}
-        run:  kani list -Zlist ${{ env.UNSTABLE_ARGS }} --std ./library --format=json
+        run:  kani list ${{ env.UNSTABLE_ARGS }} --std ./library --format=json
 
       - name: Kani list with Autoharness
         working-directory: verify-rust-std
         if: ${{ env.AUTO == '-autoharness' }}
-        run: kani autoharness -Z autoharness --list -Z list ${{ env.UNSTABLE_ARGS }} --std ./library --format=json
+        run: kani autoharness -Z autoharness --list ${{ env.UNSTABLE_ARGS }} --std ./library --format=json
 
       - name: View list
         working-directory: verify-rust-std
-        run: ls -alh kani-list.json && cat kani-list.json
+        run: ls -alh kani-list.json && head -n 100 kani-list.json
 
       - name: Upload kani-list.json
         uses: actions/upload-artifact@v4

kani

@@ -7,8 +7,8 @@ use distributed_verification::{SerFunction, SourceCode};
 use indexmap::IndexSet;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_middle::ty::TyCtxt;
+use rustc_public::mir::mono::Instance;
 use rustc_span::source_map::{SourceMap, get_source_map};
-use stable_mir::mir::mono::Instance;
 use std::{
     cell::RefCell,
     cmp::{Ordering, Reverse},

src/bin/distributed-verification/functions/cache/mod.rs

@@ -18,10 +18,10 @@ use rustc_middle::traits::{ImplSource, ImplSourceUserDefinedData};
 use rustc_middle::ty::TraitRef;
 use rustc_middle::ty::adjustment::CustomCoerceUnsized;
 use rustc_middle::ty::{PseudoCanonicalInput, Ty, TyCtxt, TypingEnv};
-use rustc_smir::rustc_internal;
+use rustc_public::Symbol;
+use rustc_public::rustc_internal;
+use rustc_public::ty::{RigidTy, Ty as TyStable, TyKind};
 use rustc_span::DUMMY_SP;
-use stable_mir::Symbol;
-use stable_mir::ty::{RigidTy, Ty as TyStable, TyKind};
 
 /// Given an unsized coercion (e.g. from `&u8` to `&dyn Debug`), extract the pair of
 /// corresponding base types `T`, `U` (e.g. `u8`, `dyn Debug`), where the source base type `T` must

src/bin/distributed-verification/functions/kani/coercion.rs

@@ -23,17 +23,17 @@ use rustc_data_structures::fingerprint::Fingerprint;
 use rustc_data_structures::fx::FxHashSet;
 use rustc_data_structures::stable_hasher::{HashStable, StableHasher};
 use rustc_middle::ty::{TyCtxt, VtblEntry};
-use rustc_session::config::OutputType;
-use rustc_smir::rustc_internal;
-use stable_mir::mir::alloc::{AllocId, GlobalAlloc};
-use stable_mir::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
-use stable_mir::mir::{
+use rustc_public::mir::alloc::{AllocId, GlobalAlloc};
+use rustc_public::mir::mono::{Instance, InstanceKind, MonoItem, StaticDef};
+use rustc_public::mir::{
     Body, CastKind, ConstOperand, MirVisitor, PointerCoercion, Rvalue, Terminator, TerminatorKind,
     visit::Location,
 };
-use stable_mir::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
-use stable_mir::{CrateDef, ItemKind};
-use stable_mir::{CrateItem, DefId};
+use rustc_public::rustc_internal;
+use rustc_public::ty::{Allocation, ClosureKind, ConstantKind, RigidTy, Ty, TyKind};
+use rustc_public::{CrateDef, ItemKind};
+use rustc_public::{CrateItem, DefId};
+use rustc_session::config::OutputType;
 use std::fmt::{Display, Formatter};
 use std::{
     collections::{HashMap, HashSet},
@@ -75,7 +75,7 @@ pub fn filter_crate_items<F>(tcx: TyCtxt, predicate: F) -> Vec<Instance>
 where
     F: Fn(TyCtxt, Instance) -> bool,
 {
-    let crate_items = stable_mir::all_local_items();
+    let crate_items = rustc_public::all_local_items();
     // Filter regular items.
     crate_items
         .iter()
@@ -109,7 +109,7 @@ pub fn filter_const_crate_items<F>(tcx: TyCtxt, mut predicate: F) -> Vec<MonoIte
 where
     F: FnMut(TyCtxt, Instance) -> bool,
 {
-    let crate_items = stable_mir::all_local_items();
+    let crate_items = rustc_public::all_local_items();
     let mut roots = Vec::new();
     // Filter regular items.
     for item in crate_items {
@@ -552,6 +552,7 @@ fn collect_alloc_items(tcx: TyCtxt, alloc_id: AllocId) -> Vec<MonoItem> {
             let vtable_id = vtable_alloc.vtable_allocation().unwrap();
             items = collect_alloc_items(tcx, vtable_id);
         }
+        GlobalAlloc::TypeId { ty: _ } => {}
     };
     items
 }

src/bin/distributed-verification/functions/kani/reachability.rs

@@ -2,7 +2,10 @@ use distributed_verification::SerFunction;
 use indexmap::IndexSet;
 use kani::{CallGraph, collect_reachable_items};
 use rustc_middle::ty::TyCtxt;
-use stable_mir::mir::mono::{Instance, MonoItem};
+use rustc_public::{
+    all_local_items,
+    mir::mono::{Instance, MonoItem},
+};
 
 mod cache;
 pub use cache::{clear_rustc_ctx, set_rustc_ctx};
@@ -13,7 +16,7 @@ pub use kani::TOOL;
 mod utils;
 
 pub fn analyze(tcx: TyCtxt) -> Vec<SerFunction> {
-    let local_items = stable_mir::all_local_items();
+    let local_items = all_local_items();
     let cap = local_items.len();
 
     let mut entries = Vec::with_capacity(cap);

src/bin/distributed-verification/functions/mod.rs

@@ -1,15 +1,15 @@
 use distributed_verification::{InstKind, MacroBacktrace, ProofKind, SourceCode};
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal::internal;
+use rustc_public::{
+    CrateDef,
+    mir::mono::{Instance, InstanceKind},
+    rustc_internal::internal,
+};
 use rustc_span::{Span, source_map::SourceMap};
 use rustc_stable_hash::{
     FromStableHash, StableHasher,
     hashers::{SipHasher128, SipHasher128Hash},
 };
-use stable_mir::{
-    CrateDef,
-    mir::mono::{Instance, InstanceKind},
-};
 use std::hash::Hash;
 
 fn new_inst_kind(kind: InstanceKind) -> Option<InstKind> {
@@ -28,7 +28,7 @@ fn span_to_snippet(span: Span, src_map: &SourceMap) -> String {
 /// Source code for a stable_mir span.
 pub fn source_code_with(
     inst: &Instance,
-    stable_mir_span: stable_mir::ty::Span,
+    stable_mir_span: rustc_public::ty::Span,
     tcx: TyCtxt,
     src_map: &SourceMap,
     path_prefixes: [&str; 2],
@@ -68,13 +68,14 @@ pub fn source_code_with(
 
 fn get_all_attrs(tcx: TyCtxt, inst: &Instance) -> (Vec<String>, Option<ProofKind>) {
     use super::kani::{PROOF, PROOF_FOR_CONTRACT};
-    use rustc_attr_data_structures::AttributeKind;
     use rustc_hir::Attribute;
+    use rustc_hir::attrs::AttributeKind;
 
     let def_id = internal(tcx, inst.def.def_id());
     let mut proof_kind = None;
     let attrs = tcx
         .get_all_attrs(def_id)
+        .iter()
         .filter(|attr| match attr {
             Attribute::Unparsed(unparsed) => {
                 let idents = &unparsed.path.segments;
@@ -93,9 +94,8 @@ fn get_all_attrs(tcx: TyCtxt, inst: &Instance) -> (Vec<String>, Option<ProofKind
                 }
                 false
             }
-            Attribute::Parsed(AttributeKind::Repr(_)) => true,
-            // FIXME: add support for #[align] when the toolchain bumps over 2025-06-19
-            //
+            Attribute::Parsed(AttributeKind::Repr { .. }) => true,
+            Attribute::Parsed(AttributeKind::Align { .. }) => true,
             // * https://github.com/rust-lang/rust/commit/1fdf2b562070ec98c5b32ee67b8c6d8145127a6e
             // * https://github.com/rust-lang/rfcs/pull/3806
             // Attribute::Parsed(AttributeKind::Align(_)) => true,

src/bin/distributed-verification/functions/utils.rs

@@ -1,6 +1,5 @@
-#![feature(rustc_private, let_chains, hash_set_entry, hasher_prefixfree_extras)]
+#![feature(rustc_private, hash_set_entry, hasher_prefixfree_extras)]
 
-extern crate rustc_attr_data_structures;
 extern crate rustc_data_structures;
 extern crate rustc_driver;
 extern crate rustc_hir;
@@ -9,11 +8,10 @@ extern crate rustc_interface;
 extern crate rustc_middle;
 extern crate rustc_session;
 #[macro_use]
-extern crate rustc_smir;
+extern crate rustc_public;
 extern crate itertools;
 extern crate rustc_span;
 extern crate rustc_stable_hash;
-extern crate stable_mir;
 
 use distributed_verification::kani_list::check_proofs;
 use eyre::Result;
@@ -65,7 +63,7 @@ fn main() -> Result<()> {
     });
 
     match res {
-        Ok(res_inner) | Err(stable_mir::CompilerError::Interrupted(res_inner)) => res_inner,
+        Ok(res_inner) | Err(rustc_public::CompilerError::Interrupted(res_inner)) => res_inner,
         Err(err) => Err(eyre!("Unexpected error {err:?}")),
     }
 }

src/bin/distributed-verification/main.rs

@@ -3,15 +3,14 @@ use distributed_verification::statistics::*;
 use indexmap::IndexMap;
 use itertools::Itertools;
 use rustc_middle::ty::TyCtxt;
-use rustc_smir::rustc_internal::internal;
-use stable_mir::CrateDef;
+use rustc_public::{CrateDef, external_crates, local_crate, rustc_internal::internal};
 
 fn new_stat(tcx: TyCtxt) -> Stat {
     Stat { local: new_local_crate(tcx), external: new_external_crates() }
 }
 
 fn new_external_crates() -> ExternalCrates {
-    let external_crates = stable_mir::external_crates();
+    let external_crates = external_crates();
     let count = external_crates.len();
     // // NOTE: crate name may duplicate, like std will appear twice
     // let crates = external_crates.into_iter().map(|krate| krate.name).sorted().collect();
@@ -22,7 +21,7 @@ fn new_local_crate(tcx: TyCtxt) -> LocalCrateFnDefs {
     let mut this = LocalCrateFnDefs::default();
 
     // for krate in stable_mir::find_crates("core") {
-    let krate = stable_mir::local_crate();
+    let krate = local_crate();
     let fn_defs = krate.fn_defs();
     this.fn_defs.total = fn_defs.len();
 
@@ -32,7 +31,7 @@ fn new_local_crate(tcx: TyCtxt) -> LocalCrateFnDefs {
 
         let did = internal(tcx, fn_def.def_id());
         // cc https://github.com/rust-lang/project-stable-mir/issues/83
-        let kanitools_attrs = tcx.get_all_attrs(did).filter_map(|attr| {
+        let kanitools_attrs = tcx.get_all_attrs(did).iter().filter_map(|attr| {
             if let rustc_hir::Attribute::Unparsed(attr) = attr {
                 this.attrs.all_tool_attrs += 1;
                 let paths = &attr.path.segments;