Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Dafny to Rust : Object::from_ref is unsound #5851

Open
MikaelMayer opened this issue Oct 23, 2024 · 1 comment · Fixed by #5858
Open

Dafny to Rust : Object::from_ref is unsound #5851

MikaelMayer opened this issue Oct 23, 2024 · 1 comment · Fixed by #5858
Labels
during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label

Comments

@MikaelMayer
Copy link
Member

MikaelMayer commented Oct 23, 2024 •
edited
Loading

This soundness test failed for an unrelated change.
https://github.com/dafny-lang/dafny/actions/runs/11447012699/job/31848553864?pr=5845

 Compiling cargoreleasefailure v0.1.0 (/home/runner/work/dafny/dafny/dafny/Source/IntegrationTests/bin/Debug/net6.0/TestFiles/LitTests/LitTest/comp/rust/cargoreleasefailure-rust)
[xUnit.net 00:03:07.85]           Finished `release` profile [optimized] target(s) in 9.94s
[xUnit.net 00:03:07.85]            Running `target/release/cargoreleasefailure`
[xUnit.net 00:03:07.85]       )
[xUnit.net 00:03:07.85]       ---- System.Exception : Command returned non-zero exit code (132): cargo run --release

Exit code 132 is a segfault. The only likely segfaulting place for this code is the accidental removal of the manual incrementation of the strong count, which this test is verifying does not happen. That means the current workaround of #[inline(never)] wasn't sufficient and the method was skipped.

We need another solution that does not rely on converting the &self back to a &Rc<Self> manually.

Anything that upcast a reference to a trait (including object) or use "this" without dereferencing a field might trigger this soundness issue.
@MikaelMayer MikaelMayer added kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly labels Oct 23, 2024
@MikaelMayer MikaelMayer changed the title Upcast unsdund Dafny to Rust : Upcast is unsound Oct 23, 2024
@MikaelMayer MikaelMayer changed the title Dafny to Rust : Upcast is unsound Dafny to Rust : Object::from_ref is unsound Oct 24, 2024
MikaelMayer added a commit that referenced this issue Oct 24, 2024
@MikaelMayer
Fix: Object::from_ref no longer forgetting to increment the strong co…
4f89b4a 
…unt.

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.
@MikaelMayer MikaelMayer mentioned this issue Oct 24, 2024
Merged
@MikaelMayer MikaelMayer reopened this Oct 28, 2024
@MikaelMayer
Copy link
Member Author

Reopening because the issue reappeared in nightly.
https://github.com/dafny-lang/dafny/actions/runs/11541336510/job/32123214130

MikaelMayer added a commit that referenced this issue Oct 29, 2024
@MikaelMayer
Fix: Object::from_ref no longer forgetting to increment the strong co…
01586c6 
…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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix: Object::from_ref no longer forgetting to increment the strong count dafny-lang/dafny
1 participant
@MikaelMayer