Merge remote-tracking branch 'origin/master' into projectAwareIDE

.github/workflows/msbuild.yml

@@ -127,12 +127,7 @@ jobs:
  reportgenerator \
  -reports:"./**/coverage.cobertura.xml" \
  -reporttypes:Cobertura -targetdir:coverage-cobertura \
- -classfilters:-Microsoft.Dafny.*PreType* \
- -classfilters:-Microsoft.Dafny.ResolverPass \
- -classfilters:-Microsoft.Dafny.*Underspecification* \
- -classfilters:-Microsoft.Dafny.DetectUnderspecificationVisitor \
- -classfilters:-Microsoft.Dafny.Microsoft.Dafny.UnderspecificationDetector \
- -classfilters:-Microsoft.Dafny.ResolverPass
+ -classfilters:"-Microsoft.Dafny.*PreType*;-Microsoft.Dafny.ResolverPass;-Microsoft.Dafny.*Underspecification*;-Microsoft.Dafny.DetectUnderspecificationVisitor;-Microsoft.Dafny.Microsoft.Dafny.UnderspecificationDetector"
  # Generate HTML from combined report, leaving out XUnitExtensions
  reportgenerator \
  -reports:"coverage-cobertura/Cobertura.xml" \

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.Test/ClonerTest.cs

@@ -0,0 +1,47 @@
+using Microsoft.Dafny;
+using Microsoft.Extensions.Logging;
+using Microsoft.Extensions.Logging.Abstractions;
+using Tomlyn;
+
+namespace DafnyCore.Test;
+
+public class ClonerTest {
+ class DummyDecl : Declaration {
+ public DummyDecl(Cloner cloner, Declaration original) : base(cloner, original) {
+ }
+
+ public DummyDecl(RangeToken rangeToken, Name name, Attributes attributes, bool isRefining) : base(rangeToken, name,
+ attributes, isRefining) {
+ }
+ }
+
+ [Fact]
+ public void ClonerKeepsBodyStartTok() {
+ var tokenBodyStart = new Token() { line = 2 };
+ var rangeToken = new RangeToken(Token.NoToken, Token.NoToken);
+ var specificationFrame = new LiteralExpr(Microsoft.Dafny.Token.NoToken, 1);
+ var formal1 = new Formal(Token.NoToken, "a", Microsoft.Dafny.Type.Bool, true, false, null) {
+ RangeToken = new RangeToken(tokenBodyStart, tokenBodyStart),
+ IsTypeExplicit = true
+ };
+ var formal2 = new Formal(Token.NoToken, "b", Microsoft.Dafny.Type.Bool, true, false, null) {
+ RangeToken = new RangeToken(tokenBodyStart, tokenBodyStart),
+ IsTypeExplicit = false
+ };
+ var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"),
+ false, false, new List<TypeParameter>(), new List<Formal> { formal1, formal2 },
+ new List<Formal>(), new List<AttributedExpression>(),
+ new Specification<FrameExpression>(new List<FrameExpression>(), null),
+ new List<AttributedExpression>(), new Specification<Expression>(new List<Expression>(), null),
+ new BlockStmt(rangeToken, new List<Statement>()), null, Token.NoToken, false);
+
+ dummyDecl.BodyStartTok = tokenBodyStart;
+ var cloner = new Cloner();
+ var dummyDecl2 = cloner.CloneMethod(dummyDecl);
+ Assert.Equal(2, dummyDecl2.BodyStartTok.line);
+ Assert.Equal(2, dummyDecl2.Ins[0].RangeToken.StartToken.line);
+ Assert.True(dummyDecl2.Ins[0].IsTypeExplicit);
+ Assert.Equal(2, dummyDecl2.Ins[1].RangeToken.StartToken.line);
+ Assert.False(dummyDecl2.Ins[1].IsTypeExplicit);
+ }
+}