Skip to content

ReachabilityMode::AllPubFns crashes by trying to treat ordinary types as functions #2047

@tedinski

Description

@tedinski

The following crates exhibit this behavior:

$ grep -l "Can't get function signature" */*.kani-assess.log
autocfg/autocfg.kani-assess.log
bytes/bytes.kani-assess.log
chrono/chrono.kani-assess.log
clap/clap.kani-assess.log
crossbeam/crossbeam-channel.kani-assess.log
crossbeam/crossbeam-epoch.kani-assess.log
crossbeam/crossbeam-utils.kani-assess.log
futures-rs/futures-task.kani-assess.log
log/log.kani-assess.log
parking_lot/parking_lot_core.kani-assess.log
regex/regex.kani-assess.log
rust-ansi-term/ansi_term.kani-assess.log
rust-url/idna.kani-assess.log
ryu/ryu.kani-assess.log
serde/serde.kani-assess.log
thread_local-rs/thread_local.kani-assess.log
tokio/tokio-util.kani-assess.log
tokio/tokio.kani-assess.log
toml/toml.kani-assess.log
tracing/tracing-core.kani-assess.log

The panic messages look something like this:

thread '<unnamed>' panicked at 'internal error: entered unreachable code: Can't get function signature of type: u32', kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:386:18
thread '<unnamed>' panicked at 'internal error: entered unreachable code: Can't get function signature of type: [naive::internals::YearFlags; 400]', kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:386:18
thread '<unnamed>' panicked at 'internal error: entered unreachable code: Can't get function signature of type: [std::vec::Vec<parser::matches::any_value::AnyValue>; 0]', kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:386:18
thread '<unnamed>' panicked at 'internal error: entered unreachable code: Can't get function signature of type: std::thread::__FastLocalKeyInner<std::thread::ThreadId>', kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:386:18
thread '<unnamed>' panicked at 'internal error: entered unreachable code: Can't get function signature of type: guard::unprotected::GuardWrapper', kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs:386:18

The abbreviated stack trace looks like this:

   2: kani_compiler::codegen_cprover_gotoc::codegen::typ::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::fn_sig_of_instance
   3: kani_compiler::codegen_cprover_gotoc::context::current_fn::CurrentFnCtx::new
   4: kani_compiler::codegen_cprover_gotoc::codegen::function::<impl kani_compiler::codegen_cprover_gotoc::context::goto_ctx::GotocCtx>::declare_function
   6: <kani_compiler::codegen_cprover_gotoc::compiler_interface::GotocCodegenBackend as rustc_codegen_ssa::traits::backend::CodegenBackend>::codegen_crate

Looks like we try to treat some public variable (a root for reachability perhaps) as a function.

Metadata

Metadata

Assignees

Labels

[C] BugThis is a bug. Something isn't working.[F] CrashKani crashed

Type

No type

Projects

Milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions