diff --git a/.github/workflows/integration-tests-reusable.yml b/.github/workflows/integration-tests-reusable.yml index 3df76e1caea..ed6ee6687f3 100644 --- a/.github/workflows/integration-tests-reusable.yml +++ b/.github/workflows/integration-tests-reusable.yml @@ -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: | diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs index 596f761a6b4..38144c2d35e 100644 --- a/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs +++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs @@ -3516,15 +3516,15 @@ fn increment_strong_count(data: *const T) { impl Object { // 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 { let pt = r as *const T as *const UnsafeCell; // 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)) } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargoreleasefailure.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargoreleasefailure.dfy new file mode 100644 index 00000000000..e247b923cfc --- /dev/null +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargoreleasefailure.dfy @@ -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(); + } +} \ No newline at end of file