A lot of kani harnesses fail

[zjp-CN]

I've partitioned harnesses onto 8 machines in this dv CI, and all verification CI jobs (not all harnesses) fail.

After looking through the logs, I find proofs begin to fail for various reasons.

For example, run the following command to see one of the CI logs:

54179456668

gh api /repos/os-checker/distributed-verification/actions/jobs/54179456668/logs | less -R

# This is an intrinsic problem.
Thread 0: Autoharness: Checking function <u128 as intrinsics::fallback::FunnelShift>::unchecked_funnel_shl against all possible inputs...
Thread 0: 
VERIFICATION RESULT:
 ** 1 of 46 failed
Failed Checks: Rust intrinsic assumption failed
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/intrinsics/fallback.rs", line 176, in
<u128 as intrinsics::fallback::FunnelShift>::unchecked_funnel_shl

VERIFICATION:- FAILED
Verification Time: 0.16669011s

# CI: overflow problem
Thread 2: Checking harness ptr::non_null::verify::non_null_check_copy_from_nonoverlapping...
Thread 0: # ??? 🤔 Why this is a thread0, not thread2 as above???
VERIFICATION RESULT:
 ** 1 of 571 failed (3 unreachable)
Failed Checks: attempt to negate with overflow
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/ops/arith.rs", line 720, in <i128 as
ops::arith::Neg>::neg

VERIFICATION:- FAILED
Verification Time: 21.367514s

# When it's locally run, it turns into a pointer problem
$ kani autoharness --std /home/gh-zjp-CN/distributed-verification/verify-rust-std/library --output-format=terse -j \
  -Zautoharness -Zfunction-contracts -Zmem-predicates -Zfloat-lib -Zc-ffi -Zloop-contracts \
  -Zquantifiers -Zstubbing -Zunstable-options --harness-timeout=10m --default-unwind=1000 \
  --include-pattern ptr::non_null::verify::non_null_check_copy_from_nonoverlapping \
  --harness ptr::non_null::verify::non_null_check_copy_from_nonoverlapping

Thread 29: Checking harness ptr::non_null::verify::non_null_check_copy_from_nonoverlapping...
Thread 29:
VERIFICATION RESULT:
 ** 2 of 587 failed (1 unreachable)
Failed Checks: misaligned pointer to reference cast: address must be a multiple of its type's alignment
 File: "/home/gh-zjp-CN/distributed-verification/verify-rust-std/library/core/src/ptr/non_null.rs", line 469, in ptr::non_null::NonNull::<[i32]>::as_ref::<'_>::{closure#3}::{closure#0}
Failed Checks: dereference failure: pointer invalid
 File: "/home/gh-zjp-CN/distributed-verification/verify-rust-std/library/core/src/ptr/non_null.rs", line 469, in ptr::non_null::NonNull::<[i32]>::as_ref::<'_>::{closure#3}::{closure#0}

VERIFICATION:- FAILED
Verification Time: 26.768908s

54179456654

gh api /repos/os-checker/distributed-verification/actions/jobs/54179456654/logs | nvim

Thread 1: Autoharness: Checking function <isize as intrinsics::fallback::CarryingMulAdd>::carrying_mul_add against all possible inputs...
Thread 1:⋅
VERIFICATION RESULT:
 ** 3 of 4 failed
Failed Checks: attempt to multiply with overflow
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/intrinsics/fallback.rs", line 33, in
<isize as intrinsics::fallback::CarryingMulAdd>::carrying_mul_add
Failed Checks: attempt to add with overflow
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/intrinsics/fallback.rs", line 33, in
<isize as intrinsics::fallback::CarryingMulAdd>::carrying_mul_add
Failed Checks: attempt to add with overflow
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/intrinsics/fallback.rs", line 33, in
<isize as intrinsics::fallback::CarryingMulAdd>::carrying_mul_add

VERIFICATION:- FAILED
Verification Time: 0.71413803s

54179456648

gh api /repos/os-checker/distributed-verification/actions/jobs/54179456648/logs | nvim

Thread 0: Autoharness: Checking function num::<impl usize>::pow against all possible inputs...
Thread 3:⋅
VERIFICATION RESULT:
 ** 5 of 1850 failed (41 unreachable)
Failed Checks: attempt to compute `unchecked_sub` which would overflow
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/ops/index_range.rs", line 56, in ops::
index_range::IndexRange::len
Failed Checks: Offset in bytes overflows isize
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/lib.rs", line 391, in kani::
rustc_intrinsics::offset::<mem::maybe_uninit::MaybeUninit<char>, *mut mem::maybe_uninit::MaybeUninit<char>, usize>
Failed Checks: Offset result and original pointer must point to the same allocation
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/lib.rs", line 391, in kani::
rustc_intrinsics::offset::<mem::maybe_uninit::MaybeUninit<char>, *mut mem::maybe_uninit::MaybeUninit<char>, usize>
Failed Checks: dereference failure: pointer invalid
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/slice/mod.rs", line 693, in slice::
<impl [mem::maybe_uninit::MaybeUninit<char>]>::get_unchecked_mut::<ops::index_range::IndexRange>
Failed Checks: Offset value overflows isize
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/lib.rs", line 391, in <usize as kani::
rustc_intrinsics::ToISize>::to_isize

VERIFICATION:- FAILED
Verification Time: 22.577106s

Thread 3: Autoharness: Checking function <char::ToUppercase as iter::traits::iterator::Iterator>::size_hint against all possible inputs...
Thread 3:⋅
VERIFICATION RESULT:
 ** 1 of 1818 failed (41 unreachable)
Failed Checks: attempt to compute `unchecked_sub` which would overflow
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/ops/index_range.rs", line 56, in ops::
index_range::IndexRange::len

VERIFICATION:- FAILED
Verification Time: 22.602398s

Thread 3: Autoharness: Checking function <char::ToLowercase as iter::traits::iterator::Iterator>::size_hint against all possible inputs...
Thread 3:⋅
VERIFICATION RESULT:
 ** 1 of 1818 failed (41 unreachable)
Failed Checks: attempt to compute `unchecked_sub` which would overflow
 File: "/home/runner/work/distributed-verification/distributed-verification/verify-rust-std/library/core/src/ops/index_range.rs", line 56, in ops::
index_range::IndexRange::len

VERIFICATION:- FAILED
Verification Time: 20.168581s

[zjp-CN]

When it's locally run, it turns into a pointer problem

$ kani autoharness --std /home/gh-zjp-CN/distributed-verification/verify-rust-std/library --output-format=terse -j \
  -Zautoharness -Zfunction-contracts -Zmem-predicates -Zfloat-lib -Zc-ffi -Zloop-contracts \
  -Zquantifiers -Zstubbing -Zunstable-options --harness-timeout=10m --default-unwind=1000 \
  --include-pattern ptr::non_null::verify::non_null_check_copy_from_nonoverlapping \
  --harness ptr::non_null::verify::non_null_check_copy_from_nonoverlapping

Does any of these arguments cause side effects or troubles?

---

Another question: I also noticed that there are more unexpected auto harnesses generated, even though I specified the same filter patterns as in the verify-rust-std repo. (<u128 as intrinsics::fallback::FunnelShift>::unchecked_funnel_shl shown above is such an unexpected example)

[zjp-CN]

Thread 2: Checking harness ptr::non_null::verify::non_null_check_copy_from_nonoverlapping...
Thread 0: # ??? 🤔 Why this is a thread0, not thread2 as above???

I've created model-checking/kani#4438 for this problem.

[zjp-CN]

--no-assert-contracts and --exact help pass and shrink proofs.

But I still can't successfully make CI pass, because some Github runners always shutdown or lose communication to cause failure. (like this)

• cc Partitioned proof runners regularly receive shutdown or communication lost os-checker/distributed-verification#143

Closing this.