forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
/
IExecutableBackend.cs
205 lines (176 loc) · 8.66 KB
/
IExecutableBackend.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
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
// SPDX-License-Identifier: MIT
#nullable enable
using System;
using System.Collections.Generic;
using System.Collections.ObjectModel;
using System.CommandLine;
using System.IO;
using System.Linq;
using DafnyCore;
using Microsoft.Dafny.Compilers;
namespace Microsoft.Dafny.Plugins;
/// <summary>
/// A class that plugins should extend in order to provide an extra Compiler to the pipeline.
///
/// If the plugin defines no PluginConfiguration, then Dafny will instantiate every sub-class
/// of IExecutableBackend from the plugin.
/// </summary>
public abstract class IExecutableBackend {
protected DafnyOptions Options { get; }
/// <summary>
/// Supported file extensions for additional compilation units (e.g. <c>.cs</c> for C#).
/// </summary>
public abstract IReadOnlySet<string> SupportedExtensions { get; }
/// <summary>
/// Human-readable string describing the target of this compiler.
/// </summary>
public abstract string TargetName { get; }
/// <summary>
/// Is this a stable, supported backend (should it be run in integration tests).
/// </summary>
public abstract bool IsStable { get; }
/// <summary>
/// Extension given to generated code files (e.g. <c>cs</c> for C#)
/// </summary>
public abstract string TargetExtension { get; }
/// <summary>
/// Value passed to the <c>/compileTarget:</c> command line flag to select this compiler (e.g. <c>cs</c> for C#)
/// </summary>
public virtual string TargetId => TargetExtension;
/// <summary>
/// Spaces added by a single indentation level.
/// </summary>
public virtual int TargetIndentSize => 2;
/// <summary>
/// Convert a Dafny file name into a file name without extension suitable for the target language (needed in e.g.
/// in Java where the file name must match the class name).
/// </summary>
public virtual string TargetBasename(string dafnyProgramName) =>
Path.GetFileNameWithoutExtension(dafnyProgramName);
/// <summary>
/// Compute where to store code files generated from a given Dafny file. For most languages there is no need to
/// create a separate directory for compilation, so this can be <c>""</c>.
/// </summary>
/// <returns>A directory name.</returns>
public virtual string TargetBaseDir(string dafnyProgramName) =>
"";
/// <summary>
/// Change <c>name</c> into a valid identifier in the target language.
/// </summary>
public abstract string PublicIdProtect(string name);
/// <summary>
/// Qualify the name <c>compileName</c> in module <c>moduleName</c>.
/// </summary>
public virtual string GetCompileName(bool isDefaultModule, string moduleName, string compileName) =>
$"{PublicIdProtect(moduleName)}.{PublicIdProtect(compileName)}";
/// <summary>
/// Which native formats this compiler supports (members of <c>Dafny.NativeType.Selection</c>).
/// </summary>
public virtual IReadOnlySet<string> SupportedNativeTypes =>
new HashSet<string> { "byte", "sbyte", "ushort", "short", "uint", "int", "ulong", "long" };
/// <summary>
/// Whether compiled code can be run without being compiled (e.g. Python but not Java).
/// </summary>
public abstract bool TextualTargetIsExecutable { get; }
/// <summary>
/// Whether generated code can be compiled without being written to disk.
/// </summary>
public abstract bool SupportsInMemoryCompilation { get; }
/// <summary>
/// Whether or not the compiler turns
/// datatype Record = R(oneThing: X)
/// into just X, including the case where "Record" is a tuple type with 1 non-ghost component.
/// </summary>
public virtual bool SupportsDatatypeWrapperErasure => true;
/// <summary>
/// Dafny features this compiler is known to not support.
/// </summary>
public virtual IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature>();
/// <summary>
/// Marks backends that should not be documented in the reference manual.
/// </summary>
public virtual bool IsInternal => false;
public abstract string ModuleSeparator { get; }
// The following two fields are not initialized until OnPreCompile
protected ErrorReporter? Reporter;
protected ReadOnlyCollection<string>? OtherFileNames;
protected IExecutableBackend(DafnyOptions options) {
Options = options;
}
/// <summary>
/// Initialize <c>Reporter</c> and <c>OtherFileNames</c>.
///
/// This method exists because compilers are constructed very early in the pipeline (to consult their
/// <c>SupportedExtensions</c>, <c>TargetLanguage</c>, etc.). C# doesn't support static fields in abstract classes,
/// so we have to create an instance to access these parameters. The alternative is to have a factory class, but we
/// deemed the added complexity unnecessary.
/// </summary>
public virtual void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection<string> otherFileNames) {
Reporter = reporter;
OtherFileNames = otherFileNames;
}
/// <summary>
/// Perform any required cleanups after generating code with <c>Compile</c> and <c>EmitCallToMain</c>.
/// </summary>
public virtual void OnPostCompile() { }
/// <summary>
/// Remove previously generated source files. This is only applicable to compilers that put sources in a separate
/// directory (e.g. Java). For other compilers, this method should do nothing.
/// </summary>
/// <param name="sourceDirectory">Name of the directory to delete.</param>
public virtual void CleanSourceDirectory(string sourceDirectory) { }
public abstract void Compile(Program dafnyProgram, ConcreteSyntaxTree output);
/// <summary>
/// Emits a call to <c>mainMethod</c> as the program's entry point, if such an explicit call is
/// required in the target language.
/// </summary>
public abstract void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree callToMainTree);
/// <summary>
/// Compile the target program known as <c>dafnyProgramName</c>.
/// <c>targetProgramText</c> contains the program text.
/// If <c>targetFilename</c> is non-null, it is the name of the target program text stored as a
/// file. <c>targetFileName</c> must be non-null if <c>otherFileNames</c> is nonempty.
/// <c>otherFileNames</c> is a list of other files to include in the compilation.
///
/// When <c>callToMain</c> is non-null, the program contains a <c>Main()</c> program.
///
/// Upon successful compilation, <c>runAfterCompile</c> says whether or not to execute the program.
///
/// Output any errors to <c>outputWriter</c>.
/// Returns <c>false</c> if there were errors. Then, <c>compilationResult</c> should not be used.
/// Returns <c>true</c> on success. Then, <c>compilationResult</c> is a value that can be passed in to
/// the instance's <c>RunTargetProgram</c> method.
/// </summary>
public abstract bool CompileTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain, string targetFilename,
ReadOnlyCollection<string> otherFileNames, bool runAfterCompile, TextWriter outputWriter, out object compilationResult);
/// <summary>
/// Runs a target program after it has been successfully compiled.
/// dafnyProgram, targetProgramText, targetFilename, and otherFileNames are the same as the corresponding parameters to <c>CompileTargetProgram</c>.
/// <c>callToMain</c> is an explicit call to Main, as required by the target compilation language.
/// <c>compilationResult</c> is a value returned by <c>CompileTargetProgram</c> for these parameters.
///
/// Returns <c>true</c> on success, <c>false</c> on error. Any errors are output to <c>outputWriter</c>.
/// </summary>
public abstract bool RunTargetProgram(string dafnyProgramName, string targetProgramText, string callToMain,
string pathsFilename,
ReadOnlyCollection<string> otherFileNames, object compilationResult, TextWriter outputWriter,
TextWriter errorWriter);
/// <summary>
/// Instruments the underlying SinglePassCompiler, if it exists.
/// </summary>
public abstract void InstrumentCompiler(CompilerInstrumenter instrumenter, Program dafnyProgram);
public static readonly Option<string> OuterModule =
new("--outer-module", "Nest all code in this module. Can be used to customize generated code. Use dots as separators (foo.baz.zoo) for deeper nesting. The first specified module will be the outermost one.");
public virtual IEnumerable<string> GetOuterModules() {
return Options.Get(OuterModule)?.Split(".") ?? Enumerable.Empty<string>();
}
static IExecutableBackend() {
DooFile.RegisterNoChecksNeeded(OuterModule);
}
public virtual Command GetCommand() {
return new Command(TargetId, $"Translate Dafny sources to {TargetName} source and build files.");
}
public virtual void PopulateCoverageReport(CoverageReport coverageReport) {
throw new NotImplementedException();
}
}