Verified-harness baseline for autoharness, 2026-10 #713

Activity

1. Tianshu-Huang commented on Oct 7, 2026

   

   Tianshu-Huang

   on Oct 7, 2026

   Last edited by Tianshu-Huang

   Author

   More actions

   Why the failed harnesses fail

   Every harness that did not pass, grouped by its first failed check.

   group	the check that failed	aarch64	x86_64
   1. Kani does not support the construct	SIMD or LLVM intrinsic, inline asm, no body	2,312 (27%)	5,002 (45%)
   2. Arithmetic on an unconstrained input	shift or add overflow, divide by zero, NaN	3,561 (41%)	3,599 (32%)
   3. The function panics on purpose	panic!, assert!	806 (9%)	884 (8%)
   4. Pointer check	null, misaligned, out of bounds	719 (8%)	312 (3%)
   5. Unreachable code reached		128 (1%)	134 (1%)
   6. Other		201 (2%)	246 (2%)
   7. Timed out at 60 s	no result	984 (11%)	1,062 (9%)

   Highlights

   • Most of what fails has nothing to do with memory safety. Only about 8% of the non-passes could: unsafe fn that fail because their documented precondition is not in the code, and pointer failures inside safe functions with unsafe code. The other 92% are documented panics in safe code, constructs Kani does not support, timeouts, and dependency crates.
   • The contract work is small and concentrated: under 200 functions per machine outside core_arch, mostly ptr, sync::atomic, Rc/Arc.
   • No std bug found in these failures. A real bug could only show up as a pointer failure inside a safe function with unsafe code, and all of those come from autoharness building invalid NonNull values (kani#4864). Not checked: dependency crates, timeouts, anything that passed.

   Group 1 by construct, top 5

   aarch64 (2,312)		x86_64 (5,002)
   simd_cast	165	simd_select_bitmask	769
   function with no body	135	function with no body	387
   simd_as	132	simd_cast	252
   simd_bswap	132	simd_bitmask	225
   C string literal	54	inline asm	166

   unsafe fn missing a contract (failures in groups 2, 3 and 4 above; unsafe from the scanner)

   	aarch64	x86_64
   core_arch intrinsics	483 (305 null-pointer vld/vst, 178 simd_* overflow)	374, not classified (scanner data is aarch64)
   ptr	75	73
   sync::atomic	27	13
   Rc, Arc, Weak	25	20
   btree, linked_list, vec_deque	18	1
   generic impls	23	19
   other	20	26
   general std total	188	152
   pointer failures inside safe functions with unsafe code (group 4)	51	1

   Setup

   • aarch64: library sync 2026-08-21, Kani 6b5e2a3f9, macOS 14 cores / 48 GB, jobs 10, wall 112 + 185 min, peak 30.9 GB
   • x86_64: library sync 2026-09-23, Kani 5c2234ee5 + kani#4864, WSL2 24 threads / 47 GB, jobs 16, wall 6 h 16 min, peak 32.6 GB
   • both: run-kani.sh --run autoharness --kani-args --exclude-pattern '::precondition_check' --harness-timeout 60s --default-unwind 1000
   • function kind: scanner {crate}_scan_functions.csv, joined by name; 6,575 of 7,727 aarch64 failures matched

   Potential to-dos from these numbers

   • The output does not say which failures are memory-safety problems. To find the unsafe fn missing a precondition and the UB inside safe code above, we had to join the results with the scanner and write scripts. The summary should mark them directly.
   • A failed unsafe fn does not say which input broke it, and that input is where the contract starts. --concrete-playback gives it for hand-written harnesses; autoharness should too.
   • Kani cannot analyze SIMD intrinsics, so safe code built on them (is_ascii, str pattern search) cannot be verified at all (check_is_ascii runs on no CI platform #718). Five primitives account for most of group 1.
2. Tianshu-Huang commented on Oct 7, 2026

   

   Tianshu-Huang

   on Oct 7, 2026

   Author

   More actions

   @srivatsansamraj
3. srivatsansamraj commented on Oct 23, 2026

   

   srivatsansamraj

   on Oct 23, 2026

   More actions

   More from the x86_64 run

   Verified harnesses are two kinds

   	generated
   verified, with checks	10,110
   verified, nothing to check ("0 of 0")	5,260
   failed	10,177
   timed out	1,062

   • A third kind is not visible in the log: a harness whose inputs never reach the function. Autoharness: fail a harness that no generated input reaches kani#4978 reports those.

   Timeouts depend on load

   rerun of the timeouts	verified	failed	out of memory	timed out
   all 1,057, 60 s, 16 jobs	0	0	0	1,057
   200 at random, 600 s, 8 jobs	23	15	8	155

   • 50 timeouts at random, run one by one with nothing beside them: 7 got a verdict in 30-53 s.
   • The --dfcc hang (goto-instrument --dfcc hangs for hours on some std harnesses; --harness-timeout does not cover it kani#4967) is quadratic work in CBMC's goto-instrument. Cause, fix and numbers: Faster standard-library verification runs: load-independent timeouts, largest-first starts, a memory check and a faster --dfcc kani#5043.

   The 93 failures no rule explains

   We read a random 60 of them. No library bug.

   • 34: the generated value breaks the documented invariant of a type with private fields (IndexRange start <= end in array::IntoIter and char::CaseMappingIter, StepBy, map_windows::Buffer). Safe code cannot build these values.
   • 6: the contract in verify-rust-std is incomplete. ptr::write_volatile has requires but no modifies. The System allocator contracts (deallocate, grow, shrink, __rdl_dealloc, __rdl_realloc) do not require ptr to come from this allocator.
   • 4: CBMC's same-object rule on < or >= between two pointers (NonNull's Ord and PartialOrd, offset_from_unsigned). Rust compares raw pointers by address.
   • 15: a documented precondition with no contract. The rest: other generated-input problems, and 2 unclear (HashMap and HashSet::with_capacity_and_hasher).

   To-dos these add

   • Autoharness: generated values of types with private fields should keep the type's invariant.
   • verify-rust-std: a modifies clause for ptr::write_volatile, and the allocator requirement in the System contracts.
   • Kani: compare raw pointers by address, as Rust does.