Skip to content

Commit

Permalink
Separate execution and compilation code of back-ends (#3407)
Browse files Browse the repository at this point in the history 
This is a refactoring that separates translation from Dafny to a string
in a particular language, from other language specific tasks, such as
running a program in that language or building a native executable
artifact for that language.

While I think this refactoring is good on its own, the main driver for
it is to enable another refactoring. I'd like to extract logic that
doesn't relate to string manipulation out of `SinglePassCompiler` by
moving it to a base class, so that this logic can be reused when
compiling Dafny to an AST (as opposed to compiling to a string or
concrete syntax tree). This PR removes the base class from
`SinglePassCompiler`, freeing it up to have another base class to which
logic can be extracted.

<small>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).</small>
  • Loading branch information
@keyboardDrummer
keyboardDrummer authored Jan 27, 2023
1 parent 5bd9203 commit acb7991
Show file tree
Hide file tree
Showing 28 changed files with 1,096 additions and 954 deletions.
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/BuiltIns.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -240,7 +240,7 @@ public TupleTypeDecl TupleType(IToken tok, int dims, bool allowCreationOfNewType
var nonGhostDims = argumentGhostness.Count(x => !x);
TupleTypeDecl nonGhostTupleTypeDecl = null;
if (nonGhostDims != dims &&
(nonGhostDims != 1 || !DafnyOptions.O.Compiler.SupportsDatatypeWrapperErasure || !DafnyOptions.O.Get(CommonOptionBag.OptimizeErasableDatatypeWrapper))) {
(nonGhostDims != 1 || !DafnyOptions.O.Backend.SupportsDatatypeWrapperErasure || !DafnyOptions.O.Get(CommonOptionBag.OptimizeErasableDatatypeWrapper))) {
// make sure the corresponding non-ghost tuple type also exists
nonGhostTupleTypeDecl = TupleType(tok, nonGhostDims, allowCreationOfNewType);
}
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/AST/TopLevelDeclarations.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ void ObjectInvariant() {
}

public static string IdProtect(string name) {
return DafnyOptions.O.Compiler.PublicIdProtect(name);
return DafnyOptions.O.Backend.PublicIdProtect(name);
}

public IToken BodyStartTok = Token.NoToken;
Expand Down Expand Up @@ -1022,7 +1022,7 @@ public string FullCompileName {
}
}

return DafnyOptions.O.Compiler.GetCompileName(EnclosingModuleDefinition.IsDefaultModule,
return DafnyOptions.O.Backend.GetCompileName(EnclosingModuleDefinition.IsDefaultModule,
EnclosingModuleDefinition.CompileName, CompileName);
}
}
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Types/Types.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1885,7 +1885,7 @@ public BitvectorType(int width)
Contract.Requires(0 <= width);
Width = width;
foreach (var nativeType in Resolver.NativeTypes) {
if (DafnyOptions.O.Compiler.SupportedNativeTypes.Contains(nativeType.Name) && width <= nativeType.Bitwidth) {
if (DafnyOptions.O.Backend.SupportedNativeTypes.Contains(nativeType.Name) && width <= nativeType.Bitwidth) {
NativeType = nativeType;
break;
}
Expand Down
172 changes: 1 addition & 171 deletions ...ce/DafnyCore/Compilers/Compiler-Csharp.cs → ...yCore/Compilers/CSharp/Compiler-Csharp.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,40 +11,24 @@
using System.Numerics;
using System.IO;
using System.Diagnostics.Contracts;
using System.Reflection;
using System.Collections.ObjectModel;
using Microsoft.CodeAnalysis.CSharp;
using Microsoft.CodeAnalysis;
using System.Runtime.Loader;
using System.Text.Json;
using System.Text.RegularExpressions;
using JetBrains.Annotations;
using Microsoft.BaseTypes;
using static Microsoft.Dafny.ConcreteSyntaxTreeUtils;

namespace Microsoft.Dafny.Compilers {
public class CsharpCompiler : SinglePassCompiler {
public override IReadOnlySet<string> SupportedExtensions => new HashSet<string> { ".cs", ".dll" };

public override string TargetLanguage => "C#";
public override string TargetExtension => "cs";

// True if the most recently visited AST has a method annotated with {:synthesize}:
protected bool Synthesize = false;

public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
Feature.SubsetTypeTests,
Feature.TuplesWiderThan20
};

public override string GetCompileName(bool isDefaultModule, string moduleName, string compileName) {
return isDefaultModule ? PublicIdProtect(compileName) :
base.GetCompileName(isDefaultModule, moduleName, compileName);
public CsharpCompiler(ErrorReporter reporter) : base(reporter) {
}

public override bool SupportsInMemoryCompilation => true;
public override bool TextualTargetIsExecutable => false;

const string DafnyISet = "Dafny.ISet";
const string DafnyIMultiset = "Dafny.IMultiSet";
const string DafnyISeq = "Dafny.ISequence";
Expand Down Expand Up @@ -3229,160 +3213,6 @@ protected override void EmitSingleValueGenerator(Expression e, bool inLetExprBod
TrParenExpr(e, wr, inLetExprBody, wStmts);
}

// ----- Target compilation and execution -------------------------------------------------------------

private class CSharpCompilationResult {
public Assembly CompiledAssembly;
}

public override bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string/*?*/ callToMain, string/*?*/ targetFilename, ReadOnlyCollection<string> otherFileNames,
bool runAfterCompile, TextWriter outputWriter, out object compilationResult) {

compilationResult = null;

// .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 inMemory = runAfterCompile;
compilation = compilation.WithOptions(compilation.Options.WithOutputKind(callToMain != null ? OutputKind.ConsoleApplication : OutputKind.DynamicallyLinkedLibrary));

var tempCompilationResult = new CSharpCompilationResult();
var libPath = Path.GetDirectoryName(Assembly.GetExecutingAssembly().Location);
if (DafnyOptions.O.UseRuntimeLib) {
compilation = compilation.AddReferences(MetadataReference.CreateFromFile(Path.Join(libPath, "DafnyRuntime.dll")));
compilation = compilation.AddReferences(MetadataReference.CreateFromFile(Assembly.Load("netstandard").Location));
}

var standardLibraries = new List<string>() {
"System.Runtime",
"System.Runtime.Numerics",
"System.Collections",
"System.Collections.Immutable",
"System.Console"
};
compilation = compilation.AddReferences(standardLibraries.Select(fileName => MetadataReference.CreateFromFile(Assembly.Load(fileName).Location)));

if (DafnyOptions.O.Optimize) {
compilation = compilation.WithOptions(compilation.Options.WithOptimizationLevel(
DafnyOptions.O.Optimize ? OptimizationLevel.Release : OptimizationLevel.Debug));
}

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);
} else {
outputWriter.WriteLine("Errors compiling program: Could not find {0}", file);
return false;
}
} else if (extension == ".dll") {
compilation = compilation.AddReferences(MetadataReference.CreateFromFile(Path.GetFullPath(file)));
}
}

var source = callToMain == null ? targetProgramText : targetProgramText + callToMain;
compilation = compilation.AddSyntaxTrees(CSharpSyntaxTree.ParseText(source));
foreach (var sourceFile in otherSourceFiles) {
compilation = compilation.AddSyntaxTrees(CSharpSyntaxTree.ParseText(File.ReadAllText(sourceFile)));
}
var outputDir = targetFilename == null ? Directory.GetCurrentDirectory() : Path.GetDirectoryName(Path.GetFullPath(targetFilename));
var outputPath = Path.Join(outputDir, Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName)) + ".dll");
var outputJson = Path.Join(outputDir, Path.GetFileNameWithoutExtension(Path.GetFileName(dafnyProgramName)) + ".runtimeconfig.json");
if (inMemory) {
using var stream = new MemoryStream();
var emitResult = compilation.Emit(stream);
if (emitResult.Success) {
tempCompilationResult.CompiledAssembly = Assembly.Load(stream.GetBuffer());
} else {
outputWriter.WriteLine("Errors compiling program:");
var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList();
foreach (var ce in errors) {
outputWriter.WriteLine(ce.ToString());
outputWriter.WriteLine();
}
return false;
}
} else {
var emitResult = compilation.Emit(outputPath);

if (emitResult.Success) {
tempCompilationResult.CompiledAssembly = Assembly.LoadFile(outputPath);
if (DafnyOptions.O.CompileVerbose) {
outputWriter.WriteLine("Compiled assembly into {0}.dll", compilation.AssemblyName);
}
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 });
File.WriteAllText(outputJson, configuration + Environment.NewLine);
} catch (Exception e) {
outputWriter.WriteLine($"Error trying to write '{outputJson}': {e.Message}");
return false;
}
} else {
outputWriter.WriteLine("Errors compiling program into {0}", compilation.AssemblyName);
var errors = emitResult.Diagnostics.Where(d => d.Severity == DiagnosticSeverity.Error).ToList();
foreach (var ce in errors) {
outputWriter.WriteLine(ce.ToString());
outputWriter.WriteLine();
}
return false;
}
}

compilationResult = tempCompilationResult;
return true;
}

public override bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string/*?*/ targetFilename, ReadOnlyCollection<string> otherFileNames,
object compilationResult, TextWriter outputWriter) {

var crx = (CSharpCompilationResult)compilationResult;

foreach (var otherFileName in otherFileNames) {
if (Path.GetExtension(otherFileName) == ".dll") {
AssemblyLoadContext.Default.LoadFromAssemblyPath(Path.GetFullPath(otherFileName));
}
}

if (crx.CompiledAssembly == null) {
throw new Exception("Cannot call run target program on a compilation that failed");
}
var entry = crx.CompiledAssembly.EntryPoint;
if (entry == null) {
throw new Exception("Cannot call run target on a compilation whose assembly has no entry.");
}
try {
Console.OutputEncoding = System.Text.Encoding.UTF8; // Force UTF-8 output in dafny run (#2999)
object[] parameters = entry.GetParameters().Length == 0 ? new object[] { } : new object[] { DafnyOptions.O.MainArgs.ToArray() };
entry.Invoke(null, parameters);
return true;
} catch (System.Reflection.TargetInvocationException e) {
outputWriter.WriteLine("Error: Execution resulted in exception: {0}", e.Message);
outputWriter.WriteLine(e.InnerException.ToString());
} catch (System.Exception e) {
outputWriter.WriteLine("Error: Execution resulted in exception: {0}", e.Message);
outputWriter.WriteLine(e.ToString());
}
return false;
}

private void AddTestCheckerIfNeeded(string name, Declaration decl, ConcreteSyntaxTree wr) {
if (DafnyOptions.O.Compile || DafnyOptions.O.RunAllTests || !Attributes.Contains(decl.Attributes, "test")) {
return;
Expand Down
Loading

0 comments on commit acb7991

Please sign in to comment.