Repository navigation
panic: autoharness: assertion failed: !self.c_variadic || matches!(self.conv, CanonAbi::C) #4817
Description
I tried this code:
fn main() {
unsafe { assert_eq!(variadic_sysv64(), 3) }
}
#[unsafe(naked)]
unsafe extern "sysv64" fn variadic_sysv64(_: ...) -> u32 {
core::arch::naked_asm!("")
}using the following command line invocation:
kani autoharness -Z autoharness code.rs
with Kani version:
I expected to see this happen: explanation
Instead, this happened: explanation
Kani Rust Verifier 0.68.0 (standalone)
CBMC 6.11.0
warning: use of an unstable feature
--> <crate attribute>:1:12
|
1 | #![feature(register_tool)]
| ^^^^^^^^^^^^^
|
= note: requested on the command line with `--force-warn unstable-features`
warning: function `main` is never used
--> code.rs:1:4
|
1 | fn main() {
| ^^^^
|
= note: `#[warn(dead_code)]` (part of `#[warn(unused)]`) on by default
warning: function `variadic_sysv64` is never used
--> code.rs:5:27
|
5 | unsafe extern "sysv64" fn variadic_sysv64(_: ...) -> u32 {
| ^^^^^^^^^^^^^^^
thread 'rustc' (1327157) panicked at /rustc-dev/8925ea358a0f265ca61026aadc7ecc506c545cbe/compiler/rustc_public/src/unstable/convert/stable/abi.rs:92:9:
assertion failed: !self.c_variadic || matches!(self.conv, CanonAbi::C)
stack backtrace:
0: __rustc::rust_begin_unwind
1: core::panicking::panic_fmt
2: core::panicking::panic
3: <rustc_target::callconv::FnAbi<rustc_middle::ty::Ty> as rustc_public::unstable::Stable>::stable
4: <rustc_public::mir::mono::Instance>::fn_abi
5: <kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::declare_function
6: <std::thread::local::LocalKey<core::cell::RefCell<(core::option::Option<alloc::boxed::Box<dyn core::ops::function::Fn<(), Output = alloc::string::String>>>, core::option::Option<cprover_bindings::goto_program::location::Location>)>>>::with::<<kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::call_with_panic_debug_info<rustc_public::mir::mono::InstanceDef, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#0}, <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items::{closure#4}::{closure#1}>::{closure#0}, ()>
7: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend>::codegen_items
8: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#0}
9: rustc_public::compiler_interface::run::<rustc_public::rustc_internal::run<<kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>
10: rustc_public::rustc_internal::run::<<kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate::{closure#0}, alloc::boxed::Box<dyn core::any::Any>>
11: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate
12: <rustc_interface::queries::Linker>::codegen_and_build_linker
13: rustc_interface::interface::run_compiler::<(), rustc_driver_impl::run_compiler::{closure#0}>::{closure#2}
14: <rustc_thread_pool::job::StackJob<rustc_thread_pool::latch::LatchRef<rustc_thread_pool::latch::LockLatch>, <rustc_thread_pool::registry::Registry>::in_worker_cold<<rustc_thread_pool::thread_pool::ThreadPool>::install<rustc_interface::util::run_in_thread_pool_with_globals<rustc_interface::interface::run_compiler<(), rustc_driver_impl::run_compiler::{closure#0}>::{closure#2}, ()>::{closure#5}::{closure#0}::{closure#1}::{closure#0}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()> as rustc_thread_pool::job::Job>::execute
15: <rustc_thread_pool::registry::WorkerThread>::wait_or_steal_until_cold
16: <rustc_thread_pool::registry::ThreadBuilder>::run
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
Kani unexpectedly panicked during compilation.
Please file an issue here: https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md
panicked at /rustc-dev/8925ea358a0f265ca61026aadc7ecc506c545cbe/compiler/rustc_public/src/compiler_interface.rs:86:38:
thread panicked while processing panic. aborting.
error: /home/matthias/.kani/kani-0.68.0/bin/kani-compiler exited with status signal: 6 (SIGABRT)
Activity
feliperodri commentedon Sep 23, 2026
Fix in #4836. Two notes from investigating: it isn't autoharness-specific (a hand-written harness calling the function ICEs the same way — autoharness just makes every function reachable), and it isn't variadics in general (
extern "C"variadics work and keep working). The root cause is thatrustc_publiconly models C-variadics whose calling convention canonicalizes toCanonAbi::C, so Kani now checks the internal ABI first and reports an unsupported construct instead of asking for a stable ABI that cannot be built.Report variadic functions with a non-C ABI as unsupported
Report variadic functions with a non-C ABI as unsupported (model-chec…