Skip to content

Bad pointer deref in SizeAndAlignOfDst/main_fail.rs #87

Closed
@markrtuttle

Description

@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.

Activity

self-assigned this
on Jun 14, 2021
avanhatt

avanhatt commented on Jun 28, 2021

@avanhatt
Contributor

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

avanhatt commented on Jul 7, 2021

@avanhatt
Contributor

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

changed the title Failing to cast *mut trait object to *mut unit Bad pointer deref in `SizeAndAlignOfDst/main_fail.rs` on Jul 7, 2021
added a commit that references this issue on Nov 16, 2021

Merge pull request #87 from rust-lang/feat/sat-abs-neg

4e6d440

31 remaining items

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

[C] BugThis is a bug. Something isn't working.

Type

No type

Projects

Relationships

None yet

Development

No branches or pull requests

Issue actions

    Bad pointer deref in `SizeAndAlignOfDst/main_fail.rs` · Issue #87 · model-checking/kani