forked from dafny-lang/dafny
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
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>
- Loading branch information
1 parent
4df64dd
commit cabd236
Showing
25 changed files
with
697 additions
and
29 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
17 changes: 17 additions & 0 deletions
17
Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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})"); | ||
} | ||
} | ||
} |
14 changes: 14 additions & 0 deletions
14
Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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> |
40 changes: 40 additions & 0 deletions
40
Source/DafnyBenchmarkingPlugin/JavaBenchmarkCompilationInstrumenter.cs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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"); | ||
} | ||
} | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
17 changes: 17 additions & 0 deletions
17
Source/DafnyCore/Compilers/GenericCompilationInstrumenter.cs
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) { } | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) { | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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; | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.