Kani crashes when handling code related to AtomicPtr

[jaisnan]

Caught by the M1 regression, Kani seems to crash when handling harness that use atomic pointers.

Here is a minimal example that causes the crash, in both linux and mac versions of Kani

#![feature(strict_provenance_atomic_ptr, strict_provenance)]
use std::sync::atomic::{AtomicPtr, Ordering};

#[kani::proof]
fn check_fetch_byte() {
    let atom = AtomicPtr::<i64>::new(core::ptr::invalid_mut(1));
    assert_eq!(atom.fetch_byte_sub(1, Ordering::Relaxed).addr(), 1);
    assert_eq!(atom.load(Ordering::Relaxed).addr(), 0);
}

This is the crash

Kani Rust Verifier 0.42.0 (standalone)
thread 'rustc' panicked at cprover_bindings/src/goto_program/stmt.rs:170:9:
assertion `left == right` failed: Error: assign statement with unequal types lhs Pointer { typ: Signedbv { width: 64 } } rhs CInteger(SSizeT)
  left: Pointer { typ: Signedbv { width: 64 } }
 right: CInteger(SSizeT)
note: run with `RUST_BACKTRACE=1` environment variable to display a 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

[Kani] current codegen item: codegen_function: std::sync::atomic::atomic_sub::<*mut i64>
_RINvNtNtCslE7LfYgGyNS_4core4sync6atomic10atomic_subOxECsgohT1pLHQU2_4main
[Kani] current codegen location: Loc { file: "./.rustup/toolchains/nightly-2023-11-28-aarch64-apple-darwin/lib/rustlib/src/rust/library/core/src/sync/atomic.rs", function: None, start_line: 3334, start_col: Some(1), end_line: 3334, end_col: Some(73) }
error: ./.kani/kani-0.42.0/bin/kani-compiler exited with status exit status: 101

using the following command line invocation:

kani main.rs

with Kani version: 0.46.0, 0.45.0, 0.42.0 (and possible older versions).

[jaisnan]

Found by @zhassan-aws , this seems to be the change commit in rust that likely caused the panic: rust-lang/rust@b17491c

[celinval]

FYI, the test case was based on the test here: https://doc.rust-lang.org/std/sync/atomic/struct.AtomicPtr.html#method.fetch_byte_sub

[celinval]

Hi @qinheping, did you make any progress in this issue? I would be fantastic if we could fix the M1 job sooner rather than later. Let me know if you have any questions.

[qinheping]

The atomic intrinsics such us atomic_xsub_relaxed allow arguments of the type (*mut *mut T, *mut T) while it is not supported in Kani codegen_atomic_binop. An minimal example to reproduce the issue:

#![feature(core_intrinsics)]
use std::intrinsics::{
    atomic_xsub_relaxed
};


#[kani::proof]
fn main() {
    let mut a = 1 as u8;

    let mut ptr: *mut u8 = &mut a;
    let ptr_ptr: *mut *mut u8 = &mut ptr;

    unsafe {
        let x = atomic_xsub_relaxed(ptr_ptr, ptr);

    }
}

We might need to also support such arguments in https://github.com/model-checking/kani/blob/main/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs#L243