From 77cb3ba4699264045976d443469e6adaa08dbd4a Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 29 Oct 2024 11:29:14 -0700 Subject: [PATCH] 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 {