From 30b94b302a81ae3e15a24b8f20b259e79a196dc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Tue, 29 Oct 2024 12:56:40 -0500 Subject: [PATCH 1/2] Chore: Fix cargo release for Object::from_ref (#5867) 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 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). --- .../workflows/integration-tests-reusable.yml | 16 +++++++ .../DafnyRuntime/DafnyRuntimeRust/src/lib.rs | 8 ++-- .../LitTest/comp/rust/cargoreleasefailure.dfy | 48 +++++++++++++++++++ 3 files changed, 68 insertions(+), 4 deletions(-) create mode 100644 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/cargoreleasefailure.dfy 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 From 77cb3ba4699264045976d443469e6adaa08dbd4a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 29 Oct 2024 11:29:14 -0700 Subject: [PATCH 2/2] fix: Make FuncExtensions internal again, handle it in DafnyGeneratedFromDafnyPost.py instead (#5860) ### Description #5757 made `FuncExtensions` in the C# runtime public instead of internal, which is not ideal since it increases the API surface area of the runtime and is a one-way door (and causes false positives in prerelease regressions testing). It was done because it seemed to be necessary, but the actual root cause was dropping these extension methods when post-processing Dafny's output. This PR reverts the change and special-cases the class in the python script instead. ### How has this been tested? Existing tests. 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). --------- Co-authored-by: Mikael Mayer --- .../Backends/CSharp/CsharpCodeGenerator.cs | 9 +---- .../DafnyCore/DafnyGeneratedFromDafnyPost.py | 12 ++++++ .../GeneratedFromDafny/FuncExtensions.cs | 38 +++++++++++++++++++ .../DafnyRuntime/DafnyRuntimeSystemModule.cs | 3 +- 4 files changed, 54 insertions(+), 8 deletions(-) create mode 100644 Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs index 770aeb9a096..8f1af398528 100644 --- a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs +++ b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs @@ -185,15 +185,10 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager // } // They aren't in any namespace to make them universally accessible. private void EmitFuncExtensions(SystemModuleManager systemModuleManager, ConcreteSyntaxTree wr) { - // An extension for this arity will be provided in the Runtime which has to be linked. - var omitAritiesBefore16 = !Options.IncludeRuntime && Options.SystemModuleTranslationMode is not CommonOptionBag.SystemModuleMode.OmitAllOtherModules; - var name = omitAritiesBefore16 ? "FuncExtensionsAfterArity16" : "FuncExtensions"; - var funcExtensions = wr.NewNamedBlock("public static class " + name); + var funcExtensions = wr.NewNamedBlock("internal static class FuncExtensions"); + wr.WriteLine("// end of class FuncExtensions"); foreach (var kv in systemModuleManager.ArrowTypeDecls) { int arity = kv.Key; - if (omitAritiesBefore16 && arity <= 16) { - continue; - } List TypeParameterList(string prefix) { var l = arity switch { diff --git a/Source/DafnyCore/DafnyGeneratedFromDafnyPost.py b/Source/DafnyCore/DafnyGeneratedFromDafnyPost.py index f493acfaea3..af5eadec414 100644 --- a/Source/DafnyCore/DafnyGeneratedFromDafnyPost.py +++ b/Source/DafnyCore/DafnyGeneratedFromDafnyPost.py @@ -67,6 +67,18 @@ print(f"File generated: {file_path}") + # Special-case the FuncExtensions class, which isn't declared inside a namespace + func_extensions_pattern = re.compile(r'(internal\s+static\s+class\s+FuncExtensions\s*{[\s\S]*?}\s*//\s*end\s*of\s*class\s*FuncExtensions)') + match = func_extensions_pattern.search(content) + func_extensions_content = match[0] + + file_content = f"{prelude}\n\n{func_extensions_content}" + file_path = f"{output}/FuncExtensions.cs" + with open(file_path, 'w') as file: + file.write(file_content) + + print(f"File generated: {file_path}") + # Now delete the file output.cs os.remove(output + '.cs') print("File deleted: " + output + '.cs') diff --git a/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs b/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs new file mode 100644 index 00000000000..39894fcdf07 --- /dev/null +++ b/Source/DafnyCore/GeneratedFromDafny/FuncExtensions.cs @@ -0,0 +1,38 @@ +// Dafny program the_program compiled into C# +// To recompile, you will need the libraries +// System.Runtime.Numerics.dll System.Collections.Immutable.dll +// but the 'dotnet' tool in net6.0 should pick those up automatically. +// Optionally, you may want to include compiler switches like +// /debug /nowarn:162,164,168,183,219,436,1717,1718 + +using System; +using System.Numerics; +using System.Collections; +#pragma warning disable CS0164 // This label has not been referenced +#pragma warning disable CS0162 // Unreachable code detected +#pragma warning disable CS1717 // Assignment made to same variable + +internal static class FuncExtensions { + public static Func DowncastClone(this Func F, Func ArgConv, Func ResConv) { + return arg => ResConv(F(ArgConv(arg))); + } + public static Func DowncastClone(this Func F, Func ResConv) { + return () => ResConv(F()); + } + public static Func DowncastClone(this Func F, Func ArgConv1, Func ArgConv2, Func ResConv) { + return (arg1, arg2) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2))); + } + public static Func DowncastClone(this Func F, Func ArgConv1, Func ArgConv2, Func ArgConv3, Func ResConv) { + return (arg1, arg2, arg3) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3))); + } + public static Func DowncastClone(this Func F, Func ArgConv1, Func ArgConv2, Func ArgConv3, Func ArgConv4, Func ResConv) { + return (arg1, arg2, arg3, arg4) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4))); + } + public static Func DowncastClone(this Func F, Func ArgConv1, Func ArgConv2, Func ArgConv3, Func ArgConv4, Func ArgConv5, Func ArgConv6, Func ArgConv7, Func ResConv) { + return (arg1, arg2, arg3, arg4, arg5, arg6, arg7) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4), ArgConv5(arg5), ArgConv6(arg6), ArgConv7(arg7))); + } + public static Func DowncastClone(this Func F, Func ArgConv1, Func ArgConv2, Func ArgConv3, Func ArgConv4, Func ArgConv5, Func ResConv) { + return (arg1, arg2, arg3, arg4, arg5) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4), ArgConv5(arg5))); + } +} +// end of class FuncExtensions \ No newline at end of file diff --git a/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs b/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs index 2c19c6eacb4..b5b6988b139 100644 --- a/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs +++ b/Source/DafnyRuntime/DafnyRuntimeSystemModule.cs @@ -503,7 +503,7 @@ public static T[] InitNewArray1(T z, BigInteger size0) { } } } // end of namespace Dafny -public static class FuncExtensions { +internal static class FuncExtensions { public static Func DowncastClone(this Func F, Func ArgConv, Func ResConv) { return arg => ResConv(F(ArgConv(arg))); } @@ -556,6 +556,7 @@ public static Func ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4), ArgConv5(arg5), ArgConv6(arg6), ArgConv7(arg7), ArgConv8(arg8), ArgConv9(arg9), ArgConv10(arg10), ArgConv11(arg11), ArgConv12(arg12), ArgConv13(arg13), ArgConv14(arg14), ArgConv15(arg15), ArgConv16(arg16))); } } +// end of class FuncExtensions #endif namespace _System {