Bad pointer deref in SizeAndAlignOfDst/main_fail.rs

[markrtuttle]

RMC fails to cast a "mutable raw pointer to a trait object" to a "mutable raw pointer to a unit" that arises in the regression test rust-tests/cbmc-reg/SizeAndAlignOfDst/main_fail.rs described in issue #33 that was used initially to illustrate an issue with the unsized pointer cast.

The mir generated by rustc on the test includes

handling rc::is_dangling::<alloc::sync::ArcInner<Mutex<dyn Subscriber>>>, std::rc::is_dangling

let _1: *mut alloc::sync::ArcInner<std::sync::Mutex<dyn Subscriber>>
let _3: *mut ()
let _4: *mut alloc::sync::ArcInner<std::sync::Mutex<dyn Subscriber>>
_4 = _1
_3 = move _4 as *mut () (Misc)

where you can see that the pointer to the trait object (a fat pointer) is being cast to a pointer to a unit (thin pointer), and codegen_misc_cast fails because the cast_to predicate says you can't cast a goto struct to a goto pointer.

[avanhatt]

The cast now succeeds; but the test itself fails with a verification failure. Not sure if this is expected behavior because CBMC can't reason about locks. Will confirm and close issue if expected. Code in question:

    let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
    let mut data = s.lock().unwrap();
    data.increment();
    assert!(data.get() == 1);

[avanhatt]

The test does also fail with invalid references when you pass --pointer-check, likely related to #240. Keeping open.

[zhassan-aws]

This test (which was moved to tests/kani/SizeAndAlignOfDst/main_assert_fixme.rs) fails due to an unlinked std function:

Check 12: _ZN3std10sys_common5mutex12MovableMutex3new17h6cb854a7d3d229c6E.assertion.1
	 - Status: FAILURE
	 - Description: "assertion false"
	 - Location: Unknown File in function _ZN3std10sys_common5mutex12MovableMutex3new17h6cb854a7d3d229c6E

So it is related to #576 (comment). Removing "MLP - Must Have" label.

[celinval]

The issue described here seems to be fixed, but we can't fully validate this until we fix the issue with linking std library.

[celinval]

Linking the standard library is no longer an issue here, but it looks like we are still incorrectly generating code for this. I added a new simple harness to this tests that should succeed but it still fails:

#[kani::proof]
#[kani::unwind(2)]
fn simplified() {
    let s: Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
    let data = s.lock().unwrap();
    assert!(data.get() == 0);
}