feat: Benchmarking plugin (dafny-lang#4215)

Adds a compiler plugin to implement support for a class-level
`{:benchmarks}` attribute. See `DafnyBenchmarkingPlugin/README.md` for
details.

Since the existing plugin interface didn't support this use case, and
we'd like it to so other similar features like `{:test}` and coverage
instrumentation can also be plugins in the future, I also added a new
`CompilerInstrumenter` plugin interface similar to `Rewriter`.

The integration test for this plugin is also a negative test for
dafny-lang#1454, which will be fixed in
a separate pending PR.

<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>

---------

Co-authored-by: Remy Willems <rwillems@amazon.com>

Source/Dafny.sln

@@ -33,6 +33,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyTestGeneration.Test",
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "TestDafny", "TestDafny\TestDafny.csproj", "{FBE70430-9890-405C-A282-61D33259CE30}"
 EndProject
+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyBenchmarkingPlugin", "DafnyBenchmarkingPlugin\DafnyBenchmarkingPlugin.csproj", "{96B8ADA8-6190-49F7-8C38-CDA60DC92293}"
+EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern", "AutoExtern\AutoExtern.csproj", "{F185BDC2-1327-47A4-A293-D3FCDC419867}"
 EndProject
 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern.Test", "AutoExtern.Test\AutoExtern.Test.csproj", "{A47E2F45-DEA3-4700-A82F-9506FEEB199A}"
@@ -124,6 +126,10 @@ Global
  {33C29F26-A27B-474D-B436-83EA615B09FC}.Debug|Any CPU.Build.0 = Debug|Any CPU
  {33C29F26-A27B-474D-B436-83EA615B09FC}.Release|Any CPU.ActiveCfg = Release|Any CPU
  {33C29F26-A27B-474D-B436-83EA615B09FC}.Release|Any CPU.Build.0 = Release|Any CPU
+ {96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
+ {96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Debug|Any CPU.Build.0 = Debug|Any CPU
+ {96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.ActiveCfg = Release|Any CPU
+ {96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.Build.0 = Release|Any CPU
  EndGlobalSection
  GlobalSection(SolutionProperties) = preSolution
  HideSolutionNode = FALSE

Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs

@@ -0,0 +1,17 @@
+using DafnyBenchmarkingPlugin;
+using Microsoft.Dafny;
+using Microsoft.Dafny.Compilers;
+using Microsoft.Dafny.Plugins;
+
+public class BenchmarkingCompilerInstrumenter : CompilerInstrumenter {
+ public BenchmarkingCompilerInstrumenter(ErrorReporter reporter) : base(reporter) { }
+
+ public override void Instrument(IExecutableBackend backend, SinglePassCompiler compiler, Program program) {
+ if (compiler is JavaCompiler javaCompiler) {
+ javaCompiler.AddInstrumenter(new JavaBenchmarkCompilationInstrumenter(Reporter));
+ } else {
+ Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, program.GetFirstTopLevelToken(),
+ $"The benchmarking plugin does not support this compilation target: {compiler} (--target:{backend.TargetId})");
+ }
+ }
+}

Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj

@@ -0,0 +1,14 @@
+<Project Sdk="Microsoft.NET.Sdk">
+
+ <PropertyGroup>
+ <TargetFramework>net6.0</TargetFramework>
+ <ImplicitUsings>enable</ImplicitUsings>
+ <Nullable>enable</Nullable>
+ <OutputPath>..\..\Binaries\</OutputPath>
+ </PropertyGroup>
+
+ <ItemGroup>
+ <ProjectReference Include="..\DafnyCore\DafnyCore.csproj" />
+ </ItemGroup>
+
+</Project>

Source/DafnyBenchmarkingPlugin/JavaBenchmarkCompilationInstrumenter.cs

@@ -0,0 +1,40 @@
+using Microsoft.Dafny;
+using Microsoft.Dafny.Plugins;
+
+namespace DafnyBenchmarkingPlugin;
+
+public class JavaBenchmarkCompilationInstrumenter : GenericCompilationInstrumenter {
+
+ private readonly ErrorReporter Reporter;
+
+ public JavaBenchmarkCompilationInstrumenter(ErrorReporter reporter) {
+ Reporter = reporter;
+ }
+
+ public override void BeforeClass(TopLevelDecl cls, ConcreteSyntaxTree wr) {
+ if (Attributes.Contains(cls.Attributes, "benchmarks")) {
+ wr.WriteLine("@org.openjdk.jmh.annotations.State(org.openjdk.jmh.annotations.Scope.Benchmark)");
+ }
+ }
+
+ public override void BeforeMethod(Method m, ConcreteSyntaxTree wr) {
+ if (Attributes.Contains(m.EnclosingClass.Attributes, "benchmarks")) {
+ if (m is Constructor) {
+ if (m.Ins.Any()) {
+ Reporter.Error(MessageSource.Compiler, ResolutionErrors.ErrorId.none, m.tok,
+ $"Classes with {{:benchmarks}} can not accept parameters in their constructors");
+ }
+
+ // _ctor() needs to be explicitly invoked as usual,
+ // and it's convenient (but a bit of a hack) to do this by marking it as Setup.
+ // It's not safe in general to run a Dafny compiled constructor
+ // multiple times on the same object,
+ // so the better solution in the future is probably to maintain the benchmark object
+ // as a separate object that Setup instantiates every time.
+ wr.WriteLine("@org.openjdk.jmh.annotations.Setup(org.openjdk.jmh.annotations.Level.Iteration)");
+ } else {
+ wr.WriteLine("@org.openjdk.jmh.annotations.Benchmark");
+ }
+ }
+ }
+}

Source/DafnyBenchmarkingPlugin/README.md

@@ -0,0 +1,14 @@
+# DafnyBenchmarkingPlugin
+
+This compiler plugin adds support for a class-level `{:benchmarks}` attribute,
+for defining harnesses to measure the performance of Dafny code.
+It can also be used to check for concurrent execution bugs
+just by verifying the benchmarking process doesn't crash.
+
+For now this plugin only supports the Java backend,
+but support for the other languages will be added in the future.
+
+## Example
+
+See [this regression test](../../Test/benchmarks/sequence-race/SequenceRace.dfy) 
+for a race condition in the Dafny runtime.

Source/DafnyCore/Compilers/ExecutableBackend.cs

@@ -5,8 +5,10 @@
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
+using System.Runtime.InteropServices;
 using System.Text;
 using System.Threading.Tasks;
+using Microsoft.Dafny.Plugins;
 using Microsoft.Win32;
 
 namespace Microsoft.Dafny.Compilers;
@@ -137,6 +139,14 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
  return true;
  }
 
+ public override void InstrumentCompiler(CompilerInstrumenter instrumenter, Program dafnyProgram) {
+ if (compiler == null) {
+ return;
+ }
+
+ instrumenter.Instrument(this, compiler, dafnyProgram);
+ }
+
  protected static void WriteFromFile(string inputFilename, TextWriter outputWriter) {
  var rd = new StreamReader(new FileStream(inputFilename, FileMode.Open, FileAccess.Read));
  SinglePassCompiler.WriteFromStream(rd, outputWriter);

Source/DafnyCore/Compilers/GenericCompilationInstrumenter.cs

@@ -0,0 +1,17 @@
+using Microsoft.Dafny;
+
+// Some common hooks for instrumenters,
+// since the compilation of these program elements tends to be similar
+// across the different backends.
+public abstract class GenericCompilationInstrumenter {
+
+ // <summary>
+ // Invoked just before outputting the code for a Dafny class.
+ // </summary>
+ public virtual void BeforeClass(TopLevelDecl cls, ConcreteSyntaxTree wr) { }
+
+ // <summary>
+ // Invoked just before outputting the code for a Dafny method.
+ // </summary>
+ public virtual void BeforeMethod(Method m, ConcreteSyntaxTree wr) { }
+}

Source/DafnyCore/Compilers/Java/Compiler-java.cs

@@ -17,7 +17,7 @@
 using static Microsoft.Dafny.ConcreteSyntaxTreeUtils;
 
 namespace Microsoft.Dafny.Compilers {
- class JavaCompiler : SinglePassCompiler {
+ public class JavaCompiler : SinglePassCompiler {
  public JavaCompiler(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
  IntSelect = ",java.math.BigInteger";
  LambdaExecute = ".apply";
@@ -76,6 +76,12 @@ string FormatTypeDescriptorVariable(TypeParameter tp) =>
 
  private record Import(string Name, string Path);
 
+ private readonly List<GenericCompilationInstrumenter> Instrumenters = new();
+
+ public void AddInstrumenter(GenericCompilationInstrumenter compilationInstrumenter) {
+ Instrumenters.Add(compilationInstrumenter);
+ }
+
  protected override bool UseReturnStyleOuts(Method m, int nonGhostOutCount) => true;
 
 
@@ -337,8 +343,8 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete
  var wBody = wr.NewNamedBlock("public static void main(String[] args)");
  var addCompileSuffix = Options.Get(CommonOptionBag.AddCompileSuffix);
  var defaultModuleCompileName = addCompileSuffix ? "_module_Compile" : "_module";
- var enclosingModuleCompileNAme = mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options);
- var modName = enclosingModuleCompileNAme == defaultModuleCompileName
+ var enclosingModuleCompileName = mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options);
+ var modName = enclosingModuleCompileName == defaultModuleCompileName
  ? (addCompileSuffix ? "_System_Compile." : "_System.")
  : "";
  companion = modName + companion;
@@ -526,6 +532,9 @@ protected ConcreteSyntaxTree CreateMethod(Method m, List<TypeArgumentInstantiati
  }
  var customReceiver = createBody && !forBodyInheritance && NeedsCustomReceiver(m);
  var receiverType = UserDefinedType.FromTopLevelDecl(m.tok, m.EnclosingClass);
+ foreach (var instrumenter in Instrumenters) {
+ instrumenter.BeforeMethod(m, wr);
+ }
  wr.Write("public {0}{1}", !createBody && !(m.EnclosingClass is TraitDecl) ? "abstract " : "", m.IsStatic || customReceiver ? "static " : "");
  wr.Write(TypeParameters(TypeArgumentInstantiation.ToFormals(ForTypeParameters(typeArgs, m, lookasideBody)), " "));
  wr.Write("{0} {1}", targetReturnTypeReplacement ?? "void", IdName(m));
@@ -894,6 +903,9 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
  w.WriteLine();
  //TODO: Fix implementations so they do not need this suppression
  EmitSuppression(w);
+ foreach (var instrumenter in Instrumenters) {
+ instrumenter.BeforeClass(cls, w);
+ }
  var abstractness = isExtern ? "abstract " : "";
  w.Write($"public {abstractness}class {javaName}{TypeParameters(typeParameters)}");
  string sep;

Source/DafnyCore/Plugin.cs

@@ -12,6 +12,7 @@ public interface Plugin {
  public IEnumerable<IExecutableBackend> GetCompilers(DafnyOptions options);
  public IEnumerable<IRewriter> GetRewriters(ErrorReporter reporter);
  public IEnumerable<DocstringRewriter> GetDocstringRewriters(DafnyOptions options);
+ public IEnumerable<CompilerInstrumenter> GetCompilerInstrumenters(ErrorReporter reporter);
 }
 
 record ErrorPlugin(string AssemblyAndArgument, Exception Exception) : Plugin {
@@ -27,6 +28,10 @@ public IEnumerable<DocstringRewriter> GetDocstringRewriters(DafnyOptions options
  return Enumerable.Empty<DocstringRewriter>();
  }
 
+ public IEnumerable<CompilerInstrumenter> GetCompilerInstrumenters(ErrorReporter reporter) {
+ return Enumerable.Empty<CompilerInstrumenter>();
+ }
+
  class ErrorRewriter : IRewriter {
  private readonly ErrorPlugin errorPlugin;
 
@@ -59,6 +64,10 @@ public IEnumerable<IRewriter> GetRewriters(ErrorReporter reporter) {
  public IEnumerable<DocstringRewriter> GetDocstringRewriters(DafnyOptions options) {
  return Configuration.GetDocstringRewriters(options);
  }
+
+ public IEnumerable<CompilerInstrumenter> GetCompilerInstrumenters(ErrorReporter reporter) {
+ return Configuration.GetCompilerInstrumenters(reporter);
+ }
 }
 
 /// <summary>
@@ -79,15 +88,17 @@ public AutomaticPluginConfiguration(Assembly assembly) {
 
  Rewriters = FindPluginComponents<Rewriter, Func<ErrorReporter, Rewriter>>(assembly, CreateRewriterFactory);
  Compilers = FindPluginComponents<IExecutableBackend, Func<IExecutableBackend>>(assembly, CreateCompilerFactory);
+ CompilerInstrumenters = FindPluginComponents<CompilerInstrumenter, Func<ErrorReporter, CompilerInstrumenter>>(assembly, CreateCompilerInstrumenterFactory);
 
  // Report an error if this assembly doesn't contain any plugins. We only
  // get to this point if we have not found a `PluginConfiguration` either,
  // so no need to check for one here.
- if (Rewriters.Length == 0 && Compilers.Length == 0) {
+ if (Rewriters.Length == 0 && Compilers.Length == 0 && CompilerInstrumenters.Length == 0) {
  throw new Exception($"Plugin {assembly.Location} does not contain any supported plugin classes. " +
  "Expecting one of the following:\n" +
  $"- ${typeof(Plugins.Rewriter).FullName}\n" +
  $"- ${typeof(Plugins.IExecutableBackend).FullName}\n" +
+ $"- ${typeof(Plugins.CompilerInstrumenter).FullName}\n" +
  $"- ${typeof(Plugins.PluginConfiguration).FullName}");
  }
  }
@@ -104,15 +115,23 @@ Func<ErrorReporter, Rewriter> CreateRewriterFactory(System.Type type) =>
 
  private Func<IExecutableBackend>[] Compilers { get; init; }
 
+ private Func<ErrorReporter, CompilerInstrumenter>[] CompilerInstrumenters { get; init; }
+
  Func<IExecutableBackend> CreateCompilerFactory(System.Type type) =>
  () => (IExecutableBackend)Activator.CreateInstance(type);
 
+ Func<ErrorReporter, CompilerInstrumenter> CreateCompilerInstrumenterFactory(System.Type type) =>
+ errorReporter => (CompilerInstrumenter)Activator.CreateInstance(type, errorReporter);
+
  public override Rewriter[] GetRewriters(ErrorReporter errorReporter) =>
  Rewriters.Select(funcErrorReporterRewriter =>
  funcErrorReporterRewriter(errorReporter)).ToArray();
 
  public override IExecutableBackend[] GetCompilers(DafnyOptions options) =>
  Compilers.Select(c => c()).ToArray();
+
+ public override CompilerInstrumenter[] GetCompilerInstrumenters(ErrorReporter reporter) =>
+ CompilerInstrumenters.Select(c => c(reporter)).ToArray();
  }
 
  public static IEnumerable<System.Type> GetConfigurationsTypes(Assembly assembly) {

Source/DafnyCore/Plugins/CompilerInstrumenter.cs

@@ -0,0 +1,25 @@
+using Microsoft.Dafny.Compilers;
+
+namespace Microsoft.Dafny.Plugins; 
+
+/// <summary>
+/// A hook for plugins to customize some of the code generation of other IExecutableBackends.
+/// </summary>
+public abstract class CompilerInstrumenter : ErrorReportingBase {
+
+ public CompilerInstrumenter(ErrorReporter reporter) : base(reporter) { }
+
+ /// <summary>
+ /// Instrument the given compiler.
+ /// 
+ /// Unlike with Rewriters, there is less consistent structure
+ /// to the implementation of the various compilers.
+ /// Therefore there isn't a single generic interface for instrumentation support
+ /// for an arbitrary SinglePassCompiler subclass.
+ /// CompilerInstrumenters will generally want to check for known subtypes
+ /// and downcast to interface with them,
+ /// possibly reporting an error if they don't recognize the compiler.
+ /// </summary>
+ public virtual void Instrument(IExecutableBackend backend, SinglePassCompiler compiler, Program program) {
+ }
+}

Source/DafnyCore/Plugins/ErrorReportingBase.cs

@@ -0,0 +1,32 @@
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Dafny.Plugins; 
+
+/// <summary>
+/// Abstract base class for plugin interfaces that may report errors.
+/// </summary>
+public abstract class ErrorReportingBase {
+ /// <summary>
+ /// Used to report errors and warnings, with positional information.
+ /// </summary>
+ protected readonly ErrorReporter Reporter;
+
+ /// <summary>
+ /// Constructor that accepts an ErrorReporter
+ /// You can obtain an ErrorReporter in either of the two following ways:
+ /// * Extend a PluginConfiguration class, and override the appropriate Get***() method whose first argument is an ErrorReporter
+ /// * Have no PluginConfiguration class, and an ErrorReporter will be provided to your class's constructor.
+ /// 
+ /// Then you can use the protected field "reporter" like the following:
+ /// 
+ /// reporter.Error(MessageSource.Compiler, token, "[Your plugin] Your error message here");
+ ///
+ /// The token is usually obtained on expressions and statements in the field `tok`
+ /// If you do not have access to them, use program.GetFirstTopLevelToken()
+ /// </summary>
+ /// <param name="reporter">The error reporter. Usually outputs automatically to IDE or command-line</param>
+ public ErrorReportingBase(ErrorReporter reporter) {
+ Contract.Requires(reporter != null);
+ Reporter = reporter;
+ }
+}

Source/DafnyCore/Plugins/IExecutableBackend.cs

@@ -11,7 +11,7 @@ namespace Microsoft.Dafny.Plugins;
 /// 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 Compiler from the plugin.
+/// of IExecutableBackend from the plugin.
 /// </summary>
 public abstract class IExecutableBackend {
  /// <summary>
@@ -160,4 +160,9 @@ public abstract bool RunTargetProgram(string dafnyProgramName, string targetProg
  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);
 }

Source/DafnyCore/Plugins/PluginConfiguration.cs

@@ -48,4 +48,13 @@ public virtual IExecutableBackend[] GetCompilers(DafnyOptions options) {
  public virtual DocstringRewriter[] GetDocstringRewriters(DafnyOptions options) {
  return Array.Empty<DocstringRewriter>();
  }
+
+ /// <summary>
+ /// Override this method to provide compiler instrumenters
+ /// </summary>
+ /// <param name="options"></param>
+ /// <returns>A list of compiler instrumenters implemented by this plugin</returns>
+ public virtual CompilerInstrumenter[] GetCompilerInstrumenters(ErrorReporter reporter) {
+ return Array.Empty<CompilerInstrumenter>();
+ }
 }