Skip to content

Commit

Permalink
Fix: Object::from_ref no longer forgetting to increment the strong co…
Browse files Browse the repository at this point in the history
…unt (#5858)

Fixes #5851
I haven't been able to produce consistently any program that could
exhibit the issue this PR is solving, the only hint I had that this
happened was the report of #5851, which I reasoned manually must come
from this function that is being skipped. By making it opaque to the
compiler, we prevent optimizations that would skip the strong count from
increasing. Alternative to this would be to pass &Rc<Self> instead of
&Self, which is what
https://github.com/dafny-lang/dafny/tree/fix-object-safety-rust does,
but &Rc does not make traits object-safe, which means we can't yet use
them in the code. I tried also passing a second arguments so that we
directly have a `Rc<>` and don't need to recover it from the &T, but
`this: Rc<Self>` again makes the trait not object-safe, and `this:
Rc<dyn Any>` causes an issue because we can't create this argument when
what we have is only the trait, and trait upcast to Any is currently
unsound in Rust. This PR is the best workaround I found so far.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
MikaelMayer authored Oct 24, 2024
1 parent a38e8a4 commit fc90edc
Showing 1 changed file with 11 additions and 2 deletions.
13 changes: 11 additions & 2 deletions Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3508,15 +3508,24 @@ impl <T: ?Sized> AsRef<T> for Object<T> {
fn increment_strong_count<T: ?Sized>(data: *const T) {
// SAFETY: This method is called only on values that were constructed from an Rc
unsafe {
Rc::increment_strong_count(data);
// Black box avoids the compiler wrongly inferring that increment strong count does nothing since the data it was applied to can be traced to be borrowed
::std::hint::black_box(Rc::increment_strong_count(data));
}
}

impl <T: ?Sized> Object<T> {
// SAFETY: This function needs to be called from a reference obtained by calling read!(o) on an object
// We never inline this function, otherwise the compiler might figure out a way to remove the increment_strong_count
#[inline(never)]
pub fn from_ref(r: &T) -> Object<T> {
let pt = r as *const T as *const UnsafeCell<T>;
crate::increment_strong_count(pt);
// SAFETY: Not guaranteed unfortunately. But looking at the sources of from_raw as of today 10/24/2024
// it will will correctly rebuilt the Rc
let rebuilt = unsafe { Rc::from_raw(pt) };
let previous_strong_count = Rc::strong_count(&rebuilt);
::std::hint::black_box(crate::increment_strong_count(pt));
let new_strong_count = Rc::strong_count(&rebuilt);
assert_eq!(new_strong_count, previous_strong_count + 1); // Will panic if not
Object(Some(rebuilt))
}
}
Expand Down

0 comments on commit fc90edc

Please sign in to comment.