Macos13 and indirect c#backend (#5601)

Variation of #5596 that also updates the C# back-end to use `dotnet` instead of an in process build. For a follow-up, it would probably be better to move the Dafny projects to dotnet8, instead of having a RollForward policy in all our projects. Also I would prefer including this Boogie change to deal with the stack overflows: boogie-org/boogie#899, instead of the change this PR makes in `SynchronousCliCompilation` --------- Co-authored-by: Fabio Madge <[email protected]> Co-authored-by: Alex Chew <[email protected]> Co-authored-by: Robin Salkeld <[email protected]>
dafny-lang · Jul 5, 2024 · 9a952b3 · 9a952b3
1 parent 040b54c
commit 9a952b3
Show file tree

Hide file tree

Showing 36 changed files with 127 additions and 155 deletions.
diff --git a/.github/workflows/release-downloads-nuget.yml b/.github/workflows/release-downloads-nuget.yml
@@ -32,7 +32,7 @@ jobs:
       fail-fast: false
       matrix:
         # This workflow breaks on windows-2022: https://github.com/dafny-lang/dafny/issues/1906
-        os: [ ubuntu-22.04, ubuntu-20.04, macos-11, windows-2019 ]
+        os: [ ubuntu-22.04, ubuntu-20.04, macos-13, windows-2019 ]
 
     steps:
     - name: OS

diff --git a/.github/workflows/release-downloads.yml b/.github/workflows/release-downloads.yml
@@ -25,7 +25,7 @@ jobs:
         - os:  'ubuntu-20.04'
           osn: 'ubuntu-20.04'
         - os:  'macos-13'
-          osn: 'x64-macos-11'
+          osn: 'x64-macos-13'
         - os:  'windows-2019'
           osn: 'windows-2019'
     # There is no hosted environment for Ubuntu 14.04 or for debian

diff --git a/.github/workflows/standard-libraries.yml b/.github/workflows/standard-libraries.yml
@@ -17,7 +17,7 @@ jobs:
   build:
     needs: check-deep-tests
     if: always() && (( github.event_name == 'pull_request' && (needs.check-deep-tests.result == 'success' || contains(github.event.pull_request.labels.*.name, 'run-deep-tests'))) || ( github.event_name == 'push' && ( github.ref_name == 'master' || vars.TEST_ON_FORK == 'true' )))
-    runs-on: macos-11
+    runs-on: macos-13
 
     steps:
       - name: Checkout Dafny

diff --git a/.github/workflows/xunit-tests-reusable.yml b/.github/workflows/xunit-tests-reusable.yml
@@ -49,10 +49,10 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ubuntu-20.04, windows-2019, macos-11]
+        os: [ubuntu-20.04, windows-2019, macos-13]
         iteration: ${{ fromJson(needs.populate-matrix-dimensions.outputs.iterations) }}
         include:
-          - os: macos-11
+          - os: macos-13
             suffix: osx
             chmod: true
           - os: windows-2019
@@ -63,7 +63,7 @@ jobs:
             chmod: true
     env:
       solutionPath: Source/Dafny.sln
-      z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02
+      z3BaseUri: https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2024-04-10
       Logging__LogLevel__Microsoft: Debug
     steps:
     - uses: actions/checkout@v4

diff --git a/Source/Dafny/Dafny.csproj b/Source/Dafny/Dafny.csproj
@@ -6,6 +6,7 @@
       <GenerateAssemblyInfo>true</GenerateAssemblyInfo>
       <DefineConstants>TRACE</DefineConstants>
       <TargetFramework>net6.0</TargetFramework>
+      <RollForward>Major</RollForward>
       <OutputPath>..\..\Binaries\</OutputPath>
       <ValidateExecutableReferencesMatchSelfContained>false</ValidateExecutableReferencesMatchSelfContained>
 

diff --git a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj
@@ -2,6 +2,7 @@
 
     <PropertyGroup>
         <TargetFramework>net6.0</TargetFramework>
+        <RollForward>Major</RollForward>
         <ImplicitUsings>enable</ImplicitUsings>
         <Nullable>enable</Nullable>
         <OutputPath>..\..\Binaries\</OutputPath>

diff --git a/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs b/Source/DafnyCore/AST/Expressions/Conditional/Patterns/IdPattern.cs
@@ -1,10 +1,7 @@
 using System;
 using System.Collections.Generic;
-using System.Diagnostics;
 using System.Diagnostics.Contracts;
 using System.Linq;
-using System.Security.AccessControl;
-using Microsoft.CodeAnalysis.CSharp.Syntax;
 
 namespace Microsoft.Dafny;
 

diff --git a/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs b/Source/DafnyCore/Backends/CSharp/CsharpBackend.cs
@@ -1,13 +1,9 @@
-using System;
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
 using System.IO;
-using System.Linq;
 using System.Reflection;
-using System.Text.Json;
+using System.Text;
 using System.Threading.Tasks;
-using Microsoft.CodeAnalysis;
-using Microsoft.CodeAnalysis.CSharp;
 
 namespace Microsoft.Dafny.Compilers;
 
@@ -39,123 +35,107 @@ public override string GetCompileName(bool isDefaultModule, string moduleName, s
     string callToMain /*?*/, string targetFilename /*?*/, ReadOnlyCollection<string> otherFileNames,
     bool runAfterCompile, TextWriter outputWriter) {
 
-    // .NET Core does not allow C# compilation on all platforms using System.CodeDom. You need to use Roslyn libraries. Context: https://github.com/dotnet/runtime/issues/18768
-    var compilation = CSharpCompilation.Create(Path.GetFileNameWithoutExtension(dafnyProgramName))
-      .WithOptions(new CSharpCompilationOptions(OutputKind.DynamicallyLinkedLibrary))
-      .AddReferences(
-        MetadataReference.CreateFromFile(typeof(object).GetTypeInfo().Assembly.Location),
-        MetadataReference.CreateFromFile(Assembly.Load("mscorlib").Location));
+    var outputDir = targetFilename == null ? Directory.GetCurrentDirectory() : Path.GetDirectoryName(Path.GetFullPath(targetFilename));
+    var fileNames = Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName));
+    var sourcePath = Path.Join(outputDir, fileNames + ".cs");
+    var csprojPath = Path.Join(outputDir, fileNames + ".csproj");
+    Directory.CreateDirectory(outputDir);
 
-    compilation = compilation.WithOptions(compilation.Options.WithOutputKind(callToMain != null ? OutputKind.ConsoleApplication : OutputKind.DynamicallyLinkedLibrary));
+    var source = callToMain == null ? targetProgramText : targetProgramText + callToMain;
+    await File.WriteAllTextAsync(sourcePath, source);
 
-    var tempCompilationResult = new CSharpCompilationResult();
+    var outputType = callToMain == null ? "Library" : "Exe";
+
+    var itemGroupExtra = @"";
     if (!Options.IncludeRuntime) {
       var libPath = Path.GetDirectoryName(Assembly.GetExecutingAssembly().Location);
-      compilation = compilation.AddReferences(MetadataReference.CreateFromFile(Path.Join(libPath, "DafnyRuntime.dll")));
-      compilation = compilation.AddReferences(MetadataReference.CreateFromFile(Assembly.Load("netstandard").Location));
+      var runtimePath = Path.Join(libPath, "DafnyRuntime.dll");
+      itemGroupExtra = @$"
+    <Reference Include=""DafnyRuntime"">
+      <HintPath>{runtimePath}</HintPath>
+    </Reference>";
     }
 
-    var standardLibraries = new List<string>() {
-      "System.Runtime",
-      "System.Runtime.Numerics",
-      "System.Collections",
-      "System.Collections.Immutable",
-      "System.Collections.Concurrent",
-      "System.Console"
-    };
-    compilation = compilation.AddReferences(standardLibraries.Select(fileName => MetadataReference.CreateFromFile(Assembly.Load((string)fileName).Location)));
-
-    if (Options.Optimize) {
-      compilation = compilation.WithOptions(compilation.Options.WithOptimizationLevel(
-        Options.Optimize ? OptimizationLevel.Release : OptimizationLevel.Debug));
-    }
+    var sourceFiles = new StringBuilder();
+    sourceFiles.AppendLine(@$"<Compile Include=""{sourcePath}"" />");
 
-    var otherSourceFiles = new List<string>();
     foreach (var file in otherFileNames) {
       string extension = Path.GetExtension(file);
       if (extension != null) { extension = extension.ToLower(); }
       if (extension == ".cs") {
         var normalizedPath = Path.Combine(Path.GetDirectoryName(file), Path.GetFileName(file));
         if (File.Exists(normalizedPath)) {
-          otherSourceFiles.Add(normalizedPath);
+          sourceFiles.AppendLine(@$"<Compile Include=""{normalizedPath}"" />");
         } else {
           await outputWriter.WriteLineAsync($"Errors compiling program: Could not find {file}");
           return (false, null);
         }
       } else if (extension == ".dll") {
-        compilation = compilation.AddReferences(MetadataReference.CreateFromFile(Path.GetFullPath(file)));
+        sourceFiles.Append(@$"
+    <Reference Include=""{Path.GetFileNameWithoutExtension(file)}"">
+      <HintPath>{Path.GetFullPath(file)}</HintPath>
+    </Reference>");
       }
     }
 
-    var source = callToMain == null ? targetProgramText : targetProgramText + callToMain;
-    compilation = compilation.AddSyntaxTrees(CSharpSyntaxTree.ParseText(source, null, "source"));
-    foreach (var sourceFile in otherSourceFiles) {
-      compilation = compilation.AddSyntaxTrees(CSharpSyntaxTree.ParseText(File.ReadAllText(sourceFile), null, sourceFile));
-    }
-    var outputDir = targetFilename == null ? Directory.GetCurrentDirectory() : Path.GetDirectoryName(Path.GetFullPath(targetFilename));
-    Directory.CreateDirectory(outputDir);
-    var outputPath = Path.Join(outputDir, Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName)) + ".dll");
-    var outputJson = Path.Join(outputDir, Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName)) + ".runtimeconfig.json");
-    var emitResult = compilation.Emit(outputPath);
-
-    if (emitResult.Success) {
-      tempCompilationResult.CompiledAssembly = Assembly.LoadFile(outputPath);
-      if (Options.Verbose) {
-        await outputWriter.WriteLineAsync($"Compiled assembly into {compilation.AssemblyName}.dll");
-      }
-
-      try {
-        var configuration = JsonSerializer.Serialize(
-          new {
-            runtimeOptions = new {
-              tfm = "net6.0",
-              framework = new {
-                name = "Microsoft.NETCore.App",
-                version = "6.0.0",
-                rollForward = "LatestMinor"
-              }
-            }
-          }, new JsonSerializerOptions() { WriteIndented = true });
-        await File.WriteAllTextAsync(outputJson, configuration + Environment.NewLine);
-      } catch (Exception e) {
-        await outputWriter.WriteLineAsync($"Error trying to write '{outputJson}': {e.Message}");
-        return (false, null);
-      }
+    var itemGroup = @$"
+  <ItemGroup>
+      {sourceFiles}
+      <PackageReference Include=""System.Runtime.Numerics"" Version=""4.3.0"" />
+      <PackageReference Include=""System.Collections.Immutable"" Version=""1.7.1"" />
+      {itemGroupExtra}
+  </ItemGroup>";
+
+    var projectFile = @$"<Project Sdk=""Microsoft.NET.Sdk"">
+
+  <PropertyGroup>
+    <OutputType>{outputType}</OutputType>
+    <TargetFramework>net6.0</TargetFramework>
+    <ImplicitUsings>enable</ImplicitUsings>
+    <EnableDefaultCompileItems>false</EnableDefaultCompileItems>
+    <NoWarn>CS8600;CS8603;CS8604;CS8605;CS8625;CS8629;CS8714;CS8765;CS8769;CS8981</NoWarn>
+    <Nullable>enable</Nullable>
+    <RollForward>Major</RollForward>
+  </PropertyGroup>
+
+  {itemGroup}
+</Project>
+";
+
+    await File.WriteAllTextAsync(csprojPath, projectFile);
+
+    var arguments = new[] { "build", csprojPath, "-o", outputDir };
+    var psi = PrepareProcessStartInfo("dotnet", arguments);
+    var dotnetOutputWriter = new StringWriter();
+    var dotnetErrorWriter = new StringWriter();
+    var exitCode = await RunProcess(psi, dotnetOutputWriter, dotnetErrorWriter);
+    var dllPath = Path.Combine(outputDir, fileNames + ".dll");
+    if (exitCode != 0 || !File.Exists(dllPath)) {
+      await outputWriter.WriteLineAsync($@"Failed to compile C# source code using 'dotnet {string.Join(" ", arguments)}'. Command output was:");
+      await outputWriter.WriteAsync(dotnetOutputWriter.ToString());
+      await outputWriter.WriteAsync(dotnetErrorWriter.ToString());
     } else {
-      await outputWriter.WriteLineAsync($"Errors compiling program into {compilation.AssemblyName}");
-      var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList();
-      foreach (var ce in errors) {
-        await outputWriter.WriteLineAsync(ce.ToString());
-        await outputWriter.WriteLineAsync();
+      if (Options.Verbose) {
+        await outputWriter.WriteLineAsync($"Compiled assembly into {Path.GetFileName(dllPath)}");
       }
-
-      return (false, null);
     }
-
-    return (true, tempCompilationResult);
-  }
-
-  private class CSharpCompilationResult {
-    public Assembly CompiledAssembly;
+    return (exitCode == 0, dllPath);
   }
 
   public override async Task<bool> RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain,
     string targetFilename /*?*/, ReadOnlyCollection<string> otherFileNames,
     object compilationResult, TextWriter outputWriter, TextWriter errorWriter) {
 
-    var crx = (CSharpCompilationResult)compilationResult;
+    var dllPath = (string)compilationResult;
+    var dllFolder = Path.GetDirectoryName(dllPath)!;
 
     foreach (var otherFileName in otherFileNames) {
       if (Path.GetExtension(otherFileName) == ".dll") {
-        var targetDirectory = Path.GetDirectoryName(crx.CompiledAssembly.Location);
-        File.Copy(otherFileName, Path.Combine(targetDirectory!, Path.GetFileName(otherFileName)), true);
+        File.Copy(otherFileName, Path.Combine(dllFolder, Path.GetFileName(otherFileName)), true);
       }
     }
 
-    if (crx.CompiledAssembly == null) {
-      throw new Exception("Cannot call run target program on a compilation that failed");
-    }
-    var psi = PrepareProcessStartInfo("dotnet", new[] { crx.CompiledAssembly.Location }.Concat(Options.MainArgs));
+    var psi = PrepareProcessStartInfo("dotnet", new[] { dllPath }.Concat(Options.MainArgs));
     return await RunProcess(psi, outputWriter, errorWriter) == 0;
   }
 

diff --git a/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs b/Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
@@ -11,8 +11,6 @@
 using System.Numerics;
 using System.IO;
 using System.Diagnostics.Contracts;
-using Microsoft.CodeAnalysis.CSharp;
-using System.Text.RegularExpressions;
 using JetBrains.Annotations;
 using Microsoft.BaseTypes;
 using Microsoft.Boogie;
@@ -2037,7 +2035,7 @@ protected override void EmitAbsurd(string/*?*/ message, ConcreteSyntaxTree wr) {
     protected override void EmitHalt(IToken tok, Expression/*?*/ messageExpr, ConcreteSyntaxTree wr) {
       var exceptionMessage = Expr(messageExpr, false, wr.Fork());
       if (tok != null) {
-        exceptionMessage.Prepend(new LineSegment(SymbolDisplay.FormatLiteral(tok.TokenToString(Options) + ": ", true) + " + "));
+        exceptionMessage.Prepend(new LineSegment($"\"{tok.TokenToString(Options)}: \" + "));
       }
       if (UnicodeCharEnabled && messageExpr.Type.IsStringType) {
         exceptionMessage.Write(".ToVerbatimString(false)");

diff --git a/Source/DafnyCore/Backends/CSharp/CsharpSynthesizer.cs b/Source/DafnyCore/Backends/CSharp/CsharpSynthesizer.cs
@@ -2,7 +2,6 @@
 using System.Collections.Generic;
 using System.Linq;
 using System.Text.RegularExpressions;
-using Microsoft.CodeAnalysis.CSharp;
 
 namespace Microsoft.Dafny.Compilers;
 
@@ -341,8 +340,7 @@ public bool Match(object argument) {
         return result;
       }
     }";
-    var memberDeclaration = SyntaxFactory.ParseMemberDeclaration(multiMatcher);
-    dafnyNamespace.WriteLine(memberDeclaration.ToFullString());
+    dafnyNamespace.WriteLine(multiMatcher);
   }
 
   internal static void EmitImports(ConcreteSyntaxTree wr) {

diff --git a/Source/DafnyCore/Backends/ExecutableBackend.cs b/Source/DafnyCore/Backends/ExecutableBackend.cs
@@ -177,9 +177,11 @@ public Task<int> RunProcess(ProcessStartInfo psi,
 
   public async Task<int> WaitForExit(Process process, TextWriter outputWriter, TextWriter errorWriter, string errorMessage = null) {
 
-    await PassthroughBuffer(process.StandardError, errorWriter);
-    await PassthroughBuffer(process.StandardOutput, outputWriter);
+    var errorTask = PassthroughBuffer(process.StandardError, errorWriter);
+    var outputTask = PassthroughBuffer(process.StandardOutput, outputWriter);
     await process.WaitForExitAsync();
+    await errorTask;
+    await outputTask;
     if (process.ExitCode != 0 && errorMessage != null) {
       await outputWriter.WriteLineAsync($"{errorMessage} Process exited with exit code {process.ExitCode}");
     }

diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj
@@ -18,6 +18,7 @@
     <OutputPath>..\..\Binaries\</OutputPath>
     <DefineConstants>TRACE</DefineConstants>
     <TargetFramework>net6.0</TargetFramework>
+    <RollForward>Major</RollForward>
     <PackageLicenseExpression>MIT</PackageLicenseExpression>
 
     <NoWarn>$(NoWarn);NU5104</NoWarn> <!-- Required because System.CommandLine is in beta. -->
@@ -26,7 +27,6 @@
 
   <ItemGroup>
       <PackageReference Include="JetBrains.Annotations" Version="2021.1.0" />
-      <PackageReference Include="Microsoft.CodeAnalysis.CSharp" Version="3.7.0" />
       <PackageReference Include="Microsoft.Extensions.FileSystemGlobbing" Version="5.0.0" />
       <PackageReference Include="Microsoft.Extensions.Logging.Abstractions" Version="5.0.0" />
       <PackageReference Include="OmniSharp.Extensions.LanguageServer" Version="0.19.5" />

diff --git a/Source/DafnyCore/DafnyFile.cs b/Source/DafnyCore/DafnyFile.cs
@@ -8,6 +8,7 @@
 using System.Reflection.Metadata;
 using System.Reflection.PortableExecutable;
 using System.Threading.Tasks;
+using DafnyAssembly;
 using DafnyCore;
 using DafnyCore.Options;
 
@@ -298,26 +299,15 @@ public static List<string> FileNames(IReadOnlyList<DafnyFile> dafnyFiles) {
     if (!File.Exists(dllPath)) {
       return null;
     }
-    using var dllFs = new FileStream(dllPath, FileMode.Open, FileAccess.Read, FileShare.ReadWrite);
-    using var dllPeReader = new PEReader(dllFs);
-    var dllMetadataReader = dllPeReader.GetMetadataReader();
 
-    foreach (var attrHandle in dllMetadataReader.CustomAttributes) {
-      var attr = dllMetadataReader.GetCustomAttribute(attrHandle);
-      try {
-        /* The cast from EntityHandle to MemberReferenceHandle is overriden, uses private members, and throws
-         * an InvalidCastException if it fails. We have no other option than to use it and catch the exception.
-         */
-        var constructor = dllMetadataReader.GetMemberReference((MemberReferenceHandle)attr.Constructor);
-        var attrType = dllMetadataReader.GetTypeReference((TypeReferenceHandle)constructor.Parent);
-        if (dllMetadataReader.GetString(attrType.Name) == "DafnySourceAttribute") {
-          var decoded = attr.DecodeValue(new StringOnlyCustomAttributeTypeProvider());
-          return decoded.FixedArguments[0].Value as string;
-        }
-      } catch (InvalidCastException) {
-        // Ignore - the Handle casts are handled as custom explicit operators,
-        // and there's no way I can see to test if the cases will succeed ahead of time.
+    try {
+      var assembly = Assembly.LoadFile(dllPath);
+
+      foreach (DafnySourceAttribute attr in assembly.GetCustomAttributes(typeof(DafnySourceAttribute), true)) {
+        return attr.dafnySourceText;
       }
+    } catch (Exception) {
+      // ignored
     }
 
     return null;

diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs
@@ -16,7 +16,6 @@
 using DafnyCore;
 using JetBrains.Annotations;
 using Microsoft.BaseTypes;
-using Microsoft.CodeAnalysis.CSharp.Syntax;
 using Microsoft.Dafny.Plugins;
 
 namespace Microsoft.Dafny {