Merge branch 'master' into fix-5864-rust-module-name-extern

.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: |

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<string> TypeParameterList(string prefix) {
           var l = arity switch {

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')

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<U, UResult> DowncastClone<T, TResult, U, UResult>(this Func<T, TResult> F, Func<U, T> ArgConv, Func<TResult, UResult> ResConv) {
+    return arg => ResConv(F(ArgConv(arg)));
+  }
+  public static Func<UResult> DowncastClone<TResult, UResult>(this Func<TResult> F, Func<TResult, UResult> ResConv) {
+    return () => ResConv(F());
+  }
+  public static Func<U1, U2, UResult> DowncastClone<T1, T2, TResult, U1, U2, UResult>(this Func<T1, T2, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2)));
+  }
+  public static Func<U1, U2, U3, UResult> DowncastClone<T1, T2, T3, TResult, U1, U2, U3, UResult>(this Func<T1, T2, T3, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3)));
+  }
+  public static Func<U1, U2, U3, U4, UResult> DowncastClone<T1, T2, T3, T4, TResult, U1, U2, U3, U4, UResult>(this Func<T1, T2, T3, T4, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<U4, T4> ArgConv4, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3, arg4) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4)));
+  }
+  public static Func<U1, U2, U3, U4, U5, U6, U7, UResult> DowncastClone<T1, T2, T3, T4, T5, T6, T7, TResult, U1, U2, U3, U4, U5, U6, U7, UResult>(this Func<T1, T2, T3, T4, T5, T6, T7, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<U4, T4> ArgConv4, Func<U5, T5> ArgConv5, Func<U6, T6> ArgConv6, Func<U7, T7> ArgConv7, Func<TResult, UResult> 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<U1, U2, U3, U4, U5, UResult> DowncastClone<T1, T2, T3, T4, T5, TResult, U1, U2, U3, U4, U5, UResult>(this Func<T1, T2, T3, T4, T5, TResult> F, Func<U1, T1> ArgConv1, Func<U2, T2> ArgConv2, Func<U3, T3> ArgConv3, Func<U4, T4> ArgConv4, Func<U5, T5> ArgConv5, Func<TResult, UResult> ResConv) {
+    return (arg1, arg2, arg3, arg4, arg5) => ResConv(F(ArgConv1(arg1), ArgConv2(arg2), ArgConv3(arg3), ArgConv4(arg4), ArgConv5(arg5)));
+  }
+}
+// end of class FuncExtensions

Source/DafnyRuntime/DafnyRuntimeRust/src/lib.rs

@@ -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))
     }

Source/DafnyRuntime/DafnyRuntimeSystemModule.cs

@@ -503,7 +503,7 @@ public static T[] InitNewArray1<T>(T z, BigInteger size0) {
     }
   }
 } // end of namespace Dafny
-public static class FuncExtensions {
+internal static class FuncExtensions {
   public static Func<U, UResult> DowncastClone<T, TResult, U, UResult>(this Func<T, TResult> F, Func<U, T> ArgConv, Func<TResult, UResult> ResConv) {
     return arg => ResConv(F(ArgConv(arg)));
   }
@@ -556,6 +556,7 @@ public static Func<U1, U2, U3, U4, U5, U6, U7, U8, U9, U10, U11, U12, U13, U14,
     return (arg1, arg2, arg3, arg4, arg5, arg6, arg7, arg8, arg9, arg10, arg11, arg12, arg13, arg14, arg15, arg16) => 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 {
 

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();
+  }
+}