-
Notifications
You must be signed in to change notification settings - Fork 254
/
LibraryBackend.cs
96 lines (73 loc) · 3.36 KB
/
LibraryBackend.cs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
using System;
using System.Collections.Generic;
using System.Collections.ObjectModel;
using System.IO;
using System.IO.Compression;
using System.Linq;
using System.Threading.Tasks;
using DafnyCore;
namespace Microsoft.Dafny.Compilers;
public class LibraryBackend : ExecutableBackend {
public LibraryBackend(DafnyOptions options) : base(options) {
}
public override IReadOnlySet<string> SupportedExtensions => new HashSet<string> { };
public override string TargetName => "Dafny Library (.doo)";
/// Some tests still fail when using the lib back-end, for example due to disallowed assumptions being present in the test,
/// such as empty constructors with ensures clauses, generated from iterators
public override bool IsStable => false;
public override string TargetExtension => "doo";
public override string TargetId => "lib";
public override string TargetBaseDir(string dafnyProgramName) =>
$"{Path.GetFileNameWithoutExtension(dafnyProgramName)}-lib";
public override bool TextualTargetIsExecutable => false;
public override bool SupportsInMemoryCompilation => false;
public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
Feature.LegacyCLI,
Feature.RuntimeCoverageReport
};
// Necessary since Compiler is null
public override string ModuleSeparator => ".";
protected override SinglePassCodeGenerator CreateCodeGenerator() {
return null;
}
public override Task<bool> OnPostGenerate(string dafnyProgramName, string targetFilename, TextWriter outputWriter) {
// Not calling base.OnPostCompile() since it references `compiler`
return Task.FromResult(true);
}
public override string PublicIdProtect(string name) {
throw new NotSupportedException();
}
public override void Compile(Program dafnyProgram, string dafnyProgramName, ConcreteSyntaxTree output) {
if (!Options.UsingNewCli) {
throw new UnsupportedFeatureException(dafnyProgram.GetStartOfFirstFileToken(), Feature.LegacyCLI);
}
var dooFile = new DooFile(dafnyProgram.AfterParsingClone);
dooFile.Write(output);
}
public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree callToMainTree) {
// No-op
}
private string DooFilePath(string dafnyProgramName) {
return Path.GetFullPath(Path.ChangeExtension(dafnyProgramName, DooFile.Extension));
}
public override async Task<(bool Success, object CompilationResult)> CompileTargetProgram(string dafnyProgramName,
string targetProgramText, string callToMain,
string targetFilename,
ReadOnlyCollection<string> otherFileNames, bool runAfterCompile, TextWriter outputWriter) {
var targetDirectory = Path.GetFullPath(Path.GetDirectoryName(targetFilename));
var dooPath = DooFilePath(dafnyProgramName);
File.Delete(dooPath);
ZipFile.CreateFromDirectory(targetDirectory, dooPath);
if (Options.Verbose) {
await outputWriter.WriteLineAsync($"Wrote Dafny library to {dooPath}");
}
return (true, null);
}
public override Task<bool> RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain,
string targetFilename,
ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter,
TextWriter errorWriter) {
var dooPath = DooFilePath(dafnyProgramName);
return RunTargetDafnyProgram(dooPath, outputWriter, errorWriter, true);
}
}