Repository navigation
goto-instrument --dfcc hangs for hours on some std harnesses; --harness-timeout does not cover it #4967
Description
I tried this code:
No code of mine. I ran kani autoharness on the whole Rust standard library from model-checking/verify-rust-std.
using the following command line invocation:
kani autoharness -Z autoharness -Z unstable-options --std ./library \
--harness-timeout 60s --default-unwind 1000 \
--exclude-pattern '::precondition_check' --jobs=16 --output-format=terse
Both runs went through verify-rust-std's scripts/run-kani.sh --run autoharness, which adds -Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing --no-assert-contracts --cbmc-args --object-bits 12 to the command above. The dfcc step only runs under those flags.
with Kani version: 5c2234ee5 (main of 2026-09-28) on x86_64, and 6b5e2a3 (main of 2026-08) on aarch64.
I expected to see this happen: every harness finishes, or stops at a timeout.
Instead, this happened: for a few harnesses, the goto-instrument --dfcc step never finishes. It runs at 100% CPU for hours. --harness-timeout only covers CBMC, so nothing stops it.
On x86_64, six harnesses spent 2 to 3 hours in this step and then finished on their own. All are panic, allocation-error, or backtrace code:
panicking::take_hookbridge::client::maybe_install_panic_hook(proc_macro)<sys::backtrace::BacktraceLock<_>::print::DisplayBacktrace as core::fmt::Display>::fmtalloc::_::__rust_alloc_error_handleralloc::default_alloc_error_hookalloc::rust_oom
On aarch64, three std harnesses and one proc_macro harness hung. We killed them after 1 hour.
The same step also crashed once on aarch64, with find_used_functions calling itself repeatedly:
Invariant check failed
File: src/util/std_expr.h:223 function: to_symbol_expr
5 goto-instrument find_used_functions
6 goto-instrument find_used_functions
...
11 goto-instrument dfcct::link_model_and_load_dfcc_library
Related: #4966 (killing the stuck step aborts the whole run), #4965, #4961. The two runs are summarised in model-checking/verify-rust-std#713.
Activity
Tianshu-Huang commentedon Oct 5, 2026
@srivatsansamraj this is the goto-instrument hang we both hit in the verification runs. The x86_64 part is from your report; could you check that the six harnesses and the timings are right?
srivatsansamraj commentedon Oct 5, 2026
Checked against the x86_64 run's samples: the six names are right. Their
goto-instrument --dfccsteps ran 187, 181, 162, 151, 132 and 124 minutes, in the order listed, and then finished on their own; nothing was killed on x86_64, and CBMC then ran each harness (five hit the 60 s limit,DisplayBacktrace::fmtfailed in 14 s). The Kani was5c2234ee5, the head of #4864 on main of 2026-09-28. The run went throughscripts/run-kani.sh --run autoharness, which adds-Z function-contracts -Z mem-predicates -Z float-lib -Z c-ffi -Z loop-contracts -Z quantifiers -Z stubbing --no-assert-contracts --cbmc-args --object-bits 12to the command above. Kani runs the dfcc step only for a harness with a contract or, under-Z loop-contracts, loop contracts (kani-driver/src/call_goto_instrument.rs), so the command as written may not reach it.Tianshu-Huang commentedon Oct 5, 2026
Thanks for checking. I fixed the issue text: the x86_64 harnesses were not killed, they finished on their own after 2 to 3 hours. I also added the run-kani.sh flags, since the dfcc step only runs with -Z loop-contracts.