Skip to content

Commit

Permalink
Chore: Fix cargo release for Object::from_ref (#5867)
Browse files Browse the repository at this point in the history
This PR should run all deep tests and pass before being merged, so that
the test cargoreleasefailurefix.dfy passes

### Description
This PR adds more black-boxing around a critical function so that the
compiler won't optimize things away by for example moving the increment
strong count and the assignments to `previous_strong_count`, which could
have caused panicking;

### How has this been tested?
All deep tests should pass, so that cargoreleasefailurefix.dfy is tested
for each supported architecture

<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 29, 2024
1 parent 7279e16 commit 30b94b3
Show file tree
Hide file tree
Showing 3 changed files with 68 additions and 4 deletions.
16 changes: 16 additions & 0 deletions .github/workflows/integration-tests-reusable.yml
Original file line number Diff line number Diff line change
Expand Up @@ -128,6 +128,22 @@ jobs:
# - name: Clean up libraries for testing
# run: |
# rm dafny/Test/libraries/lit.site.cfg # we remove the lit configuration file in the library repo (a git submodule) to prevent override
- name: Use the default Rust linker (Non-Windows)
if: runner.os != 'Windows'
run: rustup default stable
- name: Use specific Toolchain (Windows)
if: runner.os == 'Windows'
run: rustup default stable-x86_64-pc-windows-gnu
- name: Rust-related System information
run: |
echo "What is the Rust version?"
rustc -vV
echo "What is the cargo version?"
cargo --version
echo "What is the architecture?"
uname -m
echo "What are Rust toolchains installed?"
rustup toolchain list
- name: Create release
if: inputs.all_platforms
run: |
Expand Down
8 changes: 4 additions & 4 deletions Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3516,15 +3516,15 @@ fn increment_strong_count<T: ?Sized>(data: *const T) {
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)]
#[inline(never)]
pub fn from_ref(r: &T) -> Object<T> {
let pt = r as *const T as *const UnsafeCell<T>;
// 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);
let rebuilt = ::std::hint::black_box(unsafe { Rc::from_raw(pt) });
let previous_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt));
::std::hint::black_box(crate::increment_strong_count(pt));
let new_strong_count = Rc::strong_count(&rebuilt);
let new_strong_count = ::std::hint::black_box(Rc::strong_count(&rebuilt));
assert_eq!(new_strong_count, previous_strong_count + 1); // Will panic if not
Object(Some(rebuilt))
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,48 @@
// NONUNIFORM: Rust-specific tests
// RUN: %baredafny build --target=rs "%s"
// If there is no '#[inline(never)]' in front of ::dafny_runtime::increment_strong_count
// then the release will think it's safe to remove the strong count increment, resulting ins a segfault
// RUN: "%S/cargoreleasefailure-rust/cargo" run --release

module TraitModule {
trait {:termination false} MyTrait {
method DoThing ( input: int ) returns (output: int)
}
}

module ImplModule {
import TraitModule
class MyImpl extends TraitModule.MyTrait {
constructor(){}
method DoThing ( input: int ) returns (output: int)
{
return 1;
}
}
}

module WorkModule {
import ImplModule
import TraitModule

method DoWork() {
var worker := new ImplModule.MyImpl();
DoMoreWork(worker, 1);
DoMoreWork(worker, 2);
DoMoreWork(worker, 3);
DoMoreWork(worker, 4);
DoMoreWork(worker, 5);
}

method DoMoreWork(client : TraitModule.MyTrait, num : int)
{
var _ := client.DoThing(num);
}
}

module MainModule {
import WorkModule
method Main() {
WorkModule.DoWork();
}
}

0 comments on commit 30b94b3

Please sign in to comment.