Bug: Panic with attempted .def_id() on invalid res: PrimTy(Bool)

[antoyo]

Hi.
I found a panic with the following code when running Charon.

(I've been told Charon now relies on an internal fork of hax, so I'm transferring the issue here. I guess the error message should be updated to stop mentioning to open the issue in their repo.)

Code snippet to reproduce the bug:

use fs2::available_space;

fn main() {
    println!("{:?}", available_space("/"));
}

[package]
name = "charon-test3"
version = "0.1.0"
edition = "2024"

[dependencies]
fs2 = "0.4.3"

Charon version: c84b66a

Charon command: charon cargo --extract-opaque-bodies --start-from fs2

Charon output:

Complete logs: logs.txt

The first trace of the logs look like this:

thread 'rustc' (147106) panicked at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_hir/src/def.rs:823:45:
attempted .def_id() on invalid res: PrimTy(Bool)
stack backtrace:
   0: __rustc::rust_begin_unwind
   1: core::panicking::panic_fmt
   2: <rustc_hir::def::Res<!>>::def_id::{closure#0}
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_hir/src/def.rs:823:45
   3: <core::option::Option<rustc_span::def_id::DefId>>::unwrap_or_else::<<rustc_hir::def::Res<!>>::def_id::{closure#0}>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/option.rs:1067:21
   4: <rustc_hir::def::Res<!>>::def_id
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/rustc-src/rust/compiler/rustc_hir/src/def.rs:823:27
   5: hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}
             at /home/user/path/charon/charon/hax-frontend/src/rustc_utils.rs:116:56
   6: core::iter::adapters::map::map_fold::<&rustc_middle::metadata::ModChild, (core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId), (), hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}, core::iter::traits::iterator::Iterator::for_each::call<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId), <alloc::vec::Vec<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)>>::extend_trusted<core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}>>::{closure#0}>::{closure#0}>::{closure#0}
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:88:28
   7: <core::slice::iter::Iter<rustc_middle::metadata::ModChild> as core::iter::traits::iterator::Iterator>::fold::<(), core::iter::adapters::map::map_fold<&rustc_middle::metadata::ModChild, (core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId), (), hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}, core::iter::traits::iterator::Iterator::for_each::call<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId), <alloc::vec::Vec<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)>>::extend_trusted<core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}>>::{closure#0}>::{closure#0}>::{closure#0}>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/slice/iter/macros.rs:279:27
   8: <core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}> as core::iter::traits::iterator::Iterator>::fold::<(), core::iter::traits::iterator::Iterator::for_each::call<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId), <alloc::vec::Vec<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)>>::extend_trusted<core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}>>::{closure#0}>::{closure#0}>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/adapters/map.rs:128:19
   9: <core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}> as core::iter::traits::iterator::Iterator>::for_each::<<alloc::vec::Vec<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)>>::extend_trusted<core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}>>::{closure#0}>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:845:14
  10: <alloc::vec::Vec<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)>>::extend_trusted::<core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}>>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs:3936:26
  11: <alloc::vec::Vec<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)> as alloc::vec::spec_extend::SpecExtend<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId), core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}>>>::spec_extend
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/spec_extend.rs:27:14
  12: <alloc::vec::Vec<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)> as alloc::vec::spec_from_iter_nested::SpecFromIterNested<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId), core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}>>>::from_iter
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/spec_from_iter_nested.rs:60:16
  13: <alloc::vec::Vec<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)> as alloc::vec::spec_from_iter::SpecFromIter<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId), core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}>>>::from_iter
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/spec_from_iter.rs:33:9
  14: <alloc::vec::Vec<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)> as core::iter::traits::collect::FromIterator<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)>>::from_iter::<core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}>>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/alloc/src/vec/mod.rs:3800:9
  15: <core::iter::adapters::map::Map<core::slice::iter::Iter<rustc_middle::metadata::ModChild>, hax_frontend_exporter::rustc_utils::get_mod_children::{closure#1}> as core::iter::traits::iterator::Iterator>::collect::<alloc::vec::Vec<(core::option::Option<rustc_span::symbol::Ident>, rustc_span::def_id::DefId)>>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/iter/traits/iterator.rs:2064:9
  16: hax_frontend_exporter::rustc_utils::get_mod_children
             at /home/user/path/charon/charon/hax-frontend/src/rustc_utils.rs:117:14
  17: hax_frontend_exporter::types::new::full_def::translate_full_def_kind::<hax_frontend_exporter::state::State<hax_frontend_exporter::state::types::Base, hax_frontend_exporter::types::def_id::DefId, ()>>
             at /home/user/path/charon/charon/hax-frontend/src/types/new/full_def.rs:953:20
  18: hax_frontend_exporter::types::new::full_def::translate_full_def::<hax_frontend_exporter::state::State<hax_frontend_exporter::state::types::Base, hax_frontend_exporter::types::def_id::DefId, ()>>
             at /home/user/path/charon/charon/hax-frontend/src/types/new/full_def.rs:114:20
  19: <hax_frontend_exporter::types::def_id::DefId>::full_def_maybe_instantiated::<hax_frontend_exporter::state::State<hax_frontend_exporter::state::types::Base, (), ()>>
             at /home/user/path/charon/charon/hax-frontend/src/types/new/full_def.rs:200:28
  20: <charon_driver::translate::translate_ctx::TranslateCtx>::hax_def_for_item::{closure#0}
  21: std::panicking::catch_unwind::do_call::<<charon_driver::translate::translate_ctx::TranslateCtx>::hax_def_for_item::{closure#0}, alloc::sync::Arc<hax_frontend_exporter::types::new::full_def::FullDef>>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/panicking.rs:581:40
  22: std::panicking::catch_unwind::<alloc::sync::Arc<hax_frontend_exporter::types::new::full_def::FullDef>, <charon_driver::translate::translate_ctx::TranslateCtx>::hax_def_for_item::{closure#0}>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/panicking.rs:544:19
  23: std::panic::catch_unwind::<<charon_driver::translate::translate_ctx::TranslateCtx>::hax_def_for_item::{closure#0}, alloc::sync::Arc<hax_frontend_exporter::types::new::full_def::FullDef>>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/panic.rs:359:14
  24: <charon_driver::translate::translate_ctx::TranslateCtx>::hax_def_for_item
             at /home/user/path/charon/charon/src/bin/charon-driver/translate/translate_ctx.rs:177:9
  25: <charon_driver::translate::translate_ctx::TranslateCtx>::name_for_item
             at /home/user/path/charon/charon/src/bin/charon-driver/translate/translate_meta.rs:330:28
  26: <charon_driver::translate::translate_ctx::TranslateCtx>::name_for_src
             at /home/user/path/charon/charon/src/bin/charon-driver/translate/translate_meta.rs:358:18
  27: <charon_driver::translate::translate_ctx::TranslateCtx>::translate_name
             at /home/user/path/charon/charon/src/bin/charon-driver/translate/translate_meta.rs:442:29
  28: <charon_driver::translate::translate_ctx::TranslateCtx>::translate_item_aux
             at /home/user/path/charon/charon/src/bin/charon-driver/translate/translate_items.rs:63:25
  29: <charon_driver::translate::translate_ctx::TranslateCtx>::translate_item::{closure#0}::{closure#0}
             at /home/user/path/charon/charon/src/bin/charon-driver/translate/translate_items.rs:37:54
  30: std::panicking::catch_unwind::do_call::<<charon_driver::translate::translate_ctx::TranslateCtx>::translate_item::{closure#0}::{closure#0}, core::result::Result<(), charon_lib::errors::Error>>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/panicking.rs:581:40
  31: std::panicking::catch_unwind::<core::result::Result<(), charon_lib::errors::Error>, <charon_driver::translate::translate_ctx::TranslateCtx>::translate_item::{closure#0}::{closure#0}>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/panicking.rs:544:19
  32: std::panic::catch_unwind::<<charon_driver::translate::translate_ctx::TranslateCtx>::translate_item::{closure#0}::{closure#0}, core::result::Result<(), charon_lib::errors::Error>>
             at /home/user/.rustup/toolchains/nightly-2026-02-07-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/std/src/panic.rs:359:14
  33: <charon_driver::translate::translate_ctx::TranslateCtx>::translate_item::{closure#0}
             at /home/user/path/charon/charon/src/bin/charon-driver/translate/translate_items.rs:37:17
  34: <charon_driver::translate::translate_ctx::TranslateCtx>::with_def_id::<<charon_driver::translate::translate_ctx::TranslateCtx>::translate_item::{closure#0}, ()>
             at /home/user/path/charon/charon/src/bin/charon-driver/translate/translate_ctx.rs:198:19
  35: <charon_driver::translate::translate_ctx::TranslateCtx>::translate_item
             at /home/user/path/charon/charon/src/bin/charon-driver/translate/translate_items.rs:31:14
  36: charon_driver::translate::translate_crate::translate
             at /home/user/path/charon/charon/src/bin/charon-driver/translate/translate_crate.rs:821:17
  37: <charon_driver::driver::CharonCallbacks as rustc_driver_impl::Callbacks>::after_expansion
             at /home/user/path/charon/charon/src/bin/charon-driver/driver.rs:161:30
  38: <rustc_interface::passes::create_and_enter_global_ctxt<core::option::Option<rustc_interface::queries::Linker>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2}>::{closure#2} as core::ops::function::FnOnce<(&rustc_session::session::Session, rustc_middle::ty::context::CurrentGcx, alloc::sync::Arc<rustc_data_structures::jobserver::Proxy>, &std::sync::once_lock::OnceLock<rustc_middle::ty::context::GlobalCtxt>, &rustc_data_structures::sync::worker_local::WorkerLocal<rustc_middle::arena::Arena>, &rustc_data_structures::sync::worker_local::WorkerLocal<rustc_hir::Arena>, rustc_driver_impl::run_compiler::{closure#0}::{closure#2})>>::call_once::{shim:vtable#0}
  39: rustc_interface::interface::run_compiler::<(), rustc_driver_impl::run_compiler::{closure#0}>::{closure#1}
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
warning: Hax panicked when translating `core::primitive`.
 --> /rustc/library/core/src/lib.rs:359:1

Thanks.

[Nadrieril]

Minimized: charon rustc --extract-opaque-bodies --start-from core::primitive -- random_file.rs