diff --git a/Source/Dafny.sln b/Source/Dafny.sln index 23297b185ed..5db938783a0 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln @@ -33,8 +33,6 @@ 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}" @@ -126,10 +124,6 @@ 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 diff --git a/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs b/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs deleted file mode 100644 index 79daf0fd340..00000000000 --- a/Source/DafnyBenchmarkingPlugin/BenchmarkInstrumentation.cs +++ /dev/null @@ -1,17 +0,0 @@ -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})"); - } - } -} \ No newline at end of file diff --git a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj b/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj deleted file mode 100644 index badfad3b141..00000000000 --- a/Source/DafnyBenchmarkingPlugin/DafnyBenchmarkingPlugin.csproj +++ /dev/null @@ -1,14 +0,0 @@ - - - - net6.0 - enable - enable - ..\..\Binaries\ - - - - - - - diff --git a/Source/DafnyBenchmarkingPlugin/JavaBenchmarkCompilationInstrumenter.cs b/Source/DafnyBenchmarkingPlugin/JavaBenchmarkCompilationInstrumenter.cs deleted file mode 100644 index 98b39fdc261..00000000000 --- a/Source/DafnyBenchmarkingPlugin/JavaBenchmarkCompilationInstrumenter.cs +++ /dev/null @@ -1,40 +0,0 @@ -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"); - } - } - } -} diff --git a/Source/DafnyBenchmarkingPlugin/README.md b/Source/DafnyBenchmarkingPlugin/README.md deleted file mode 100644 index 3101287cb3c..00000000000 --- a/Source/DafnyBenchmarkingPlugin/README.md +++ /dev/null @@ -1,14 +0,0 @@ -# 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. \ No newline at end of file diff --git a/Source/DafnyCore/Compilers/ExecutableBackend.cs b/Source/DafnyCore/Compilers/ExecutableBackend.cs index 0fe0b82bcc4..1c5e4ebff8f 100644 --- a/Source/DafnyCore/Compilers/ExecutableBackend.cs +++ b/Source/DafnyCore/Compilers/ExecutableBackend.cs @@ -5,10 +5,8 @@ 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; @@ -139,14 +137,6 @@ 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); diff --git a/Source/DafnyCore/Compilers/GenericCompilationInstrumenter.cs b/Source/DafnyCore/Compilers/GenericCompilationInstrumenter.cs deleted file mode 100644 index 3d20be3af68..00000000000 --- a/Source/DafnyCore/Compilers/GenericCompilationInstrumenter.cs +++ /dev/null @@ -1,17 +0,0 @@ -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 { - - // - // Invoked just before outputting the code for a Dafny class. - // - public virtual void BeforeClass(TopLevelDecl cls, ConcreteSyntaxTree wr) { } - - // - // Invoked just before outputting the code for a Dafny method. - // - public virtual void BeforeMethod(Method m, ConcreteSyntaxTree wr) { } -} \ No newline at end of file diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index 283e08b327f..459e03508b5 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -17,7 +17,7 @@ using static Microsoft.Dafny.ConcreteSyntaxTreeUtils; namespace Microsoft.Dafny.Compilers { - public class JavaCompiler : SinglePassCompiler { + class JavaCompiler : SinglePassCompiler { public JavaCompiler(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) { IntSelect = ",java.math.BigInteger"; LambdaExecute = ".apply"; @@ -76,12 +76,6 @@ string FormatTypeDescriptorVariable(TypeParameter tp) => private record Import(string Name, string Path); - private readonly List Instrumenters = new(); - - public void AddInstrumenter(GenericCompilationInstrumenter compilationInstrumenter) { - Instrumenters.Add(compilationInstrumenter); - } - protected override bool UseReturnStyleOuts(Method m, int nonGhostOutCount) => true; @@ -343,8 +337,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; @@ -532,9 +526,6 @@ protected ConcreteSyntaxTree CreateMethod(Method m, List GetCompilers(DafnyOptions options); public IEnumerable GetRewriters(ErrorReporter reporter); public IEnumerable GetDocstringRewriters(DafnyOptions options); - public IEnumerable GetCompilerInstrumenters(ErrorReporter reporter); } record ErrorPlugin(string AssemblyAndArgument, Exception Exception) : Plugin { @@ -28,10 +27,6 @@ public IEnumerable GetDocstringRewriters(DafnyOptions options return Enumerable.Empty(); } - public IEnumerable GetCompilerInstrumenters(ErrorReporter reporter) { - return Enumerable.Empty(); - } - class ErrorRewriter : IRewriter { private readonly ErrorPlugin errorPlugin; @@ -64,10 +59,6 @@ public IEnumerable GetRewriters(ErrorReporter reporter) { public IEnumerable GetDocstringRewriters(DafnyOptions options) { return Configuration.GetDocstringRewriters(options); } - - public IEnumerable GetCompilerInstrumenters(ErrorReporter reporter) { - return Configuration.GetCompilerInstrumenters(reporter); - } } /// @@ -88,17 +79,15 @@ public AutomaticPluginConfiguration(Assembly assembly) { Rewriters = FindPluginComponents>(assembly, CreateRewriterFactory); Compilers = FindPluginComponents>(assembly, CreateCompilerFactory); - CompilerInstrumenters = FindPluginComponents>(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 && CompilerInstrumenters.Length == 0) { + if (Rewriters.Length == 0 && Compilers.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}"); } } @@ -115,23 +104,15 @@ Func CreateRewriterFactory(System.Type type) => private Func[] Compilers { get; init; } - private Func[] CompilerInstrumenters { get; init; } - Func CreateCompilerFactory(System.Type type) => () => (IExecutableBackend)Activator.CreateInstance(type); - Func 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 GetConfigurationsTypes(Assembly assembly) { diff --git a/Source/DafnyCore/Plugins/CompilerInstrumenter.cs b/Source/DafnyCore/Plugins/CompilerInstrumenter.cs deleted file mode 100644 index 4b8e5ca0b56..00000000000 --- a/Source/DafnyCore/Plugins/CompilerInstrumenter.cs +++ /dev/null @@ -1,25 +0,0 @@ -using Microsoft.Dafny.Compilers; - -namespace Microsoft.Dafny.Plugins; - -/// -/// A hook for plugins to customize some of the code generation of other IExecutableBackends. -/// -public abstract class CompilerInstrumenter : ErrorReportingBase { - - public CompilerInstrumenter(ErrorReporter reporter) : base(reporter) { } - - /// - /// 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. - /// - public virtual void Instrument(IExecutableBackend backend, SinglePassCompiler compiler, Program program) { - } -} \ No newline at end of file diff --git a/Source/DafnyCore/Plugins/ErrorReportingBase.cs b/Source/DafnyCore/Plugins/ErrorReportingBase.cs deleted file mode 100644 index f9425b31492..00000000000 --- a/Source/DafnyCore/Plugins/ErrorReportingBase.cs +++ /dev/null @@ -1,32 +0,0 @@ -using System.Diagnostics.Contracts; - -namespace Microsoft.Dafny.Plugins; - -/// -/// Abstract base class for plugin interfaces that may report errors. -/// -public abstract class ErrorReportingBase { - /// - /// Used to report errors and warnings, with positional information. - /// - protected readonly ErrorReporter Reporter; - - /// - /// 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() - /// - /// The error reporter. Usually outputs automatically to IDE or command-line - public ErrorReportingBase(ErrorReporter reporter) { - Contract.Requires(reporter != null); - Reporter = reporter; - } -} \ No newline at end of file diff --git a/Source/DafnyCore/Plugins/IExecutableBackend.cs b/Source/DafnyCore/Plugins/IExecutableBackend.cs index 0ae1812c0de..23f5316554a 100644 --- a/Source/DafnyCore/Plugins/IExecutableBackend.cs +++ b/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 IExecutableBackend from the plugin. +/// of Compiler from the plugin. /// public abstract class IExecutableBackend { /// @@ -160,9 +160,4 @@ public abstract bool RunTargetProgram(string dafnyProgramName, string targetProg string pathsFilename, ReadOnlyCollection otherFileNames, object compilationResult, TextWriter outputWriter, TextWriter errorWriter); - - /// - /// Instruments the underlying SinglePassCompiler, if it exists. - /// - public abstract void InstrumentCompiler(CompilerInstrumenter instrumenter, Program dafnyProgram); } diff --git a/Source/DafnyCore/Plugins/PluginConfiguration.cs b/Source/DafnyCore/Plugins/PluginConfiguration.cs index 06bacc332ad..1b1b2a3fb71 100644 --- a/Source/DafnyCore/Plugins/PluginConfiguration.cs +++ b/Source/DafnyCore/Plugins/PluginConfiguration.cs @@ -48,13 +48,4 @@ public virtual IExecutableBackend[] GetCompilers(DafnyOptions options) { public virtual DocstringRewriter[] GetDocstringRewriters(DafnyOptions options) { return Array.Empty(); } - - /// - /// Override this method to provide compiler instrumenters - /// - /// - /// A list of compiler instrumenters implemented by this plugin - public virtual CompilerInstrumenter[] GetCompilerInstrumenters(ErrorReporter reporter) { - return Array.Empty(); - } } \ No newline at end of file diff --git a/Source/DafnyCore/Plugins/Rewriter.cs b/Source/DafnyCore/Plugins/Rewriter.cs index 5c681bc1103..c382a30d76d 100644 --- a/Source/DafnyCore/Plugins/Rewriter.cs +++ b/Source/DafnyCore/Plugins/Rewriter.cs @@ -9,9 +9,30 @@ namespace Microsoft.Dafny.Plugins { /// of Rewriter from the plugin, providing them with an ErrorReporter in the constructor /// as the first and only argument. /// - public abstract class Rewriter : ErrorReportingBase { - public Rewriter(ErrorReporter reporter) : base(reporter) { } + public abstract class Rewriter { + /// + /// Used to report errors and warnings, with positional information. + /// + protected readonly ErrorReporter Reporter; + /// + /// Constructor that accepts an ErrorReporter + /// You can obtain an ErrorReporter two following ways: + /// * Extend a PluginConfiguration class, and override the method GetRewriters(), 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 moduleDefinition.GetFirstTopLevelToken() + /// + /// The error reporter. Usually outputs automatically to IDE or command-line + public Rewriter(ErrorReporter reporter) { + Contract.Requires(reporter != null); + Reporter = reporter; + } /// /// Override this method to obtain a module definition after the entire resolution pipeline /// You can then report errors using reporter.Error (see above) diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 2110c89eadf..293394f8e22 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/Source/DafnyDriver/DafnyDriver.cs @@ -875,12 +875,6 @@ public static async Task CompileDafnyProgram(Program dafnyProgram, string var oldErrorCount = dafnyProgram.Reporter.Count(ErrorLevel.Error); var options = dafnyProgram.Options; options.Backend.OnPreCompile(dafnyProgram.Reporter, otherFileNames); - - // Now that an internal compiler is instantiated, apply any plugin instrumentation. - foreach (var compilerInstrumenter in options.Plugins.SelectMany(p => p.GetCompilerInstrumenters(dafnyProgram.Reporter))) { - options.Backend.InstrumentCompiler(compilerInstrumenter, dafnyProgram); - } - var compiler = options.Backend; var hasMain = Compilers.SinglePassCompiler.HasMain(dafnyProgram, out var mainMethod); @@ -991,9 +985,5 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg TextWriter errorWriter) { throw new NotSupportedException(); } - - public override void InstrumentCompiler(CompilerInstrumenter instrumenter, Program dafnyProgram) { - throw new NotSupportedException(); - } } } diff --git a/Source/IntegrationTests/IntegrationTests.csproj b/Source/IntegrationTests/IntegrationTests.csproj index 593fc17142e..b25f9c5d185 100644 --- a/Source/IntegrationTests/IntegrationTests.csproj +++ b/Source/IntegrationTests/IntegrationTests.csproj @@ -21,7 +21,6 @@ - diff --git a/Test/benchmarks/sequence-race/SequenceRace.dfy b/Test/benchmarks/sequence-race/SequenceRace.dfy deleted file mode 100644 index af391ef6eaa..00000000000 --- a/Test/benchmarks/sequence-race/SequenceRace.dfy +++ /dev/null @@ -1,45 +0,0 @@ - -// Ensure trying to use an unsupported compilation target results in a clean error message. -// RUN: %exits-with 3 %baredafny translate cs %args "%s" --plugin:DafnyBenchmarkingPlugin.dll > "%t" -// RUN: %diff "%s.expect" "%t" - -// RUN: %baredafny translate java %args "%s" --plugin:DafnyBenchmarkingPlugin.dll -// RUN: mkdir -p %S/java/src/jmh -// RUN: cp -r %S/SequenceRace-java %S/java/src/jmh/java - -// Note the intentional ">" as opposed to ">>", so we can check just the benchmark run output. -// RUN: %S/java/gradlew jmh -p %S/java > "%t" -// RUN: %OutputCheck --file-to-check "%t" "%s" -// We manually verify the benchmark fails (since the bug isn't fixed yet), because unfortunately -// we can't trust the JMH gradle plugin to: https://github.com/melix/jmh-gradle-plugin/issues/255 -// CHECK: - -// -// Sanity test of the benchmarking plugin, -// and a regression test for https://github.com/dafny-lang/dafny/issues/1454. -// -// A class with {:benchmarks} will be translated to a form that target language -// benchmarking frameworks can integrate with relatively easily. -// For each method on such classes, -// a single instance of the class will be instantiated using the no-argument constructor, -// and then one or more concurrent executions of the method will be triggered. -// -class {:benchmarks} SequenceRace { - - const s: seq - - constructor() { - s := []; - for x := 0 to 1000 { - s := s + [x]; - } - } - - method LazyRace() { - // Using expect means compilers can't optimize calculations away - // since they could lead to throwing exceptions. - expect 0 < |s|; - expect s[0] == 0; - } - -} \ No newline at end of file diff --git a/Test/benchmarks/sequence-race/SequenceRace.dfy.expect b/Test/benchmarks/sequence-race/SequenceRace.dfy.expect deleted file mode 100644 index cb68b237a1e..00000000000 --- a/Test/benchmarks/sequence-race/SequenceRace.dfy.expect +++ /dev/null @@ -1,4 +0,0 @@ - -Dafny program verifier finished with 2 verified, 0 errors -SequenceRace.dfy(27,0): Error: The benchmarking plugin does not support this compilation target: Microsoft.Dafny.Compilers.CsharpCompiler (--target:cs) -Wrote textual form of partial target program to SequenceRace.cs diff --git a/Test/benchmarks/sequence-race/java/build.gradle.kts b/Test/benchmarks/sequence-race/java/build.gradle.kts deleted file mode 100644 index 9a549ad4e70..00000000000 --- a/Test/benchmarks/sequence-race/java/build.gradle.kts +++ /dev/null @@ -1,43 +0,0 @@ -/* - * Copyright 2014-2021 the original author or authors. - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -plugins { - `java-library` - id("me.champeau.jmh") version "0.7.0" -} - -repositories { - mavenLocal() - mavenCentral() -} - -dependencies { - implementation("org.dafny:DafnyRuntime:4.1.0") - testImplementation("org.junit.jupiter:junit-jupiter-api:5.9.2") - testRuntimeOnly("org.junit.jupiter:junit-jupiter-engine") -} - -tasks.test { - useJUnitPlatform() -} - -jmh { - failOnError.set(true) - warmupIterations.set(2) - iterations.set(20) - timeOnIteration.set("1s") - fork.set(2) - threads.set(10) -} diff --git a/Test/benchmarks/sequence-race/java/gradle/wrapper/gradle-wrapper.jar b/Test/benchmarks/sequence-race/java/gradle/wrapper/gradle-wrapper.jar deleted file mode 100644 index c1962a79e29..00000000000 Binary files a/Test/benchmarks/sequence-race/java/gradle/wrapper/gradle-wrapper.jar and /dev/null differ diff --git a/Test/benchmarks/sequence-race/java/gradle/wrapper/gradle-wrapper.properties b/Test/benchmarks/sequence-race/java/gradle/wrapper/gradle-wrapper.properties deleted file mode 100644 index 37aef8d3f0c..00000000000 --- a/Test/benchmarks/sequence-race/java/gradle/wrapper/gradle-wrapper.properties +++ /dev/null @@ -1,6 +0,0 @@ -distributionBase=GRADLE_USER_HOME -distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.1.1-bin.zip -networkTimeout=10000 -zipStoreBase=GRADLE_USER_HOME -zipStorePath=wrapper/dists diff --git a/Test/benchmarks/sequence-race/java/gradlew b/Test/benchmarks/sequence-race/java/gradlew deleted file mode 100755 index a9fe6045e20..00000000000 --- a/Test/benchmarks/sequence-race/java/gradlew +++ /dev/null @@ -1,245 +0,0 @@ -#!/bin/sh - -# -# Copyright © 2015-2021 the original authors. -# -# Licensed under the Apache License, Version 2.0 (the "License"); -# you may not use this file except in compliance with the License. -# You may obtain a copy of the License at -# -# https://www.apache.org/licenses/LICENSE-2.0 -# -# Unless required by applicable law or agreed to in writing, software -# distributed under the License is distributed on an "AS IS" BASIS, -# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -# See the License for the specific language governing permissions and -# limitations under the License. -# - -############################################################################## -# -# Gradle start up script for POSIX generated by Gradle. -# -# Important for running: -# -# (1) You need a POSIX-compliant shell to run this script. If your /bin/sh is -# noncompliant, but you have some other compliant shell such as ksh or -# bash, then to run this script, type that shell name before the whole -# command line, like: -# -# ksh Gradle -# -# Busybox and similar reduced shells will NOT work, because this script -# requires all of these POSIX shell features: -# * functions; -# * expansions «$var», «${var}», «${var:-default}», «${var+SET}», -# «${var#prefix}», «${var%suffix}», and «$( cmd )»; -# * compound commands having a testable exit status, especially «case»; -# * various built-in commands including «command», «set», and «ulimit». -# -# Important for patching: -# -# (2) This script targets any POSIX shell, so it avoids extensions provided -# by Bash, Ksh, etc; in particular arrays are avoided. -# -# The "traditional" practice of packing multiple parameters into a -# space-separated string is a well documented source of bugs and security -# problems, so this is (mostly) avoided, by progressively accumulating -# options in "$@", and eventually passing that to Java. -# -# Where the inherited environment variables (DEFAULT_JVM_OPTS, JAVA_OPTS, -# and GRADLE_OPTS) rely on word-splitting, this is performed explicitly; -# see the in-line comments for details. -# -# There are tweaks for specific operating systems such as AIX, CygWin, -# Darwin, MinGW, and NonStop. -# -# (3) This script is generated from the Groovy template -# https://github.com/gradle/gradle/blob/HEAD/subprojects/plugins/src/main/resources/org/gradle/api/internal/plugins/unixStartScript.txt -# within the Gradle project. -# -# You can find Gradle at https://github.com/gradle/gradle/. -# -############################################################################## - -# Attempt to set APP_HOME - -# Resolve links: $0 may be a link -app_path=$0 - -# Need this for daisy-chained symlinks. -while - APP_HOME=${app_path%"${app_path##*/}"} # leaves a trailing /; empty if no leading path - [ -h "$app_path" ] -do - ls=$( ls -ld "$app_path" ) - link=${ls#*' -> '} - case $link in #( - /*) app_path=$link ;; #( - *) app_path=$APP_HOME$link ;; - esac -done - -# This is normally unused -# shellcheck disable=SC2034 -APP_BASE_NAME=${0##*/} -APP_HOME=$( cd "${APP_HOME:-./}" && pwd -P ) || exit - -# Use the maximum available, or set MAX_FD != -1 to use that value. -MAX_FD=maximum - -warn () { - echo "$*" -} >&2 - -die () { - echo - echo "$*" - echo - exit 1 -} >&2 - -# OS specific support (must be 'true' or 'false'). -cygwin=false -msys=false -darwin=false -nonstop=false -case "$( uname )" in #( - CYGWIN* ) cygwin=true ;; #( - Darwin* ) darwin=true ;; #( - MSYS* | MINGW* ) msys=true ;; #( - NONSTOP* ) nonstop=true ;; -esac - -CLASSPATH=$APP_HOME/gradle/wrapper/gradle-wrapper.jar - - -# Determine the Java command to use to start the JVM. -if [ -n "$JAVA_HOME" ] ; then - if [ -x "$JAVA_HOME/jre/sh/java" ] ; then - # IBM's JDK on AIX uses strange locations for the executables - JAVACMD=$JAVA_HOME/jre/sh/java - else - JAVACMD=$JAVA_HOME/bin/java - fi - if [ ! -x "$JAVACMD" ] ; then - die "ERROR: JAVA_HOME is set to an invalid directory: $JAVA_HOME - -Please set the JAVA_HOME variable in your environment to match the -location of your Java installation." - fi -else - JAVACMD=java - which java >/dev/null 2>&1 || die "ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. - -Please set the JAVA_HOME variable in your environment to match the -location of your Java installation." -fi - -# Increase the maximum file descriptors if we can. -if ! "$cygwin" && ! "$darwin" && ! "$nonstop" ; then - case $MAX_FD in #( - max*) - # In POSIX sh, ulimit -H is undefined. That's why the result is checked to see if it worked. - # shellcheck disable=SC3045 - MAX_FD=$( ulimit -H -n ) || - warn "Could not query maximum file descriptor limit" - esac - case $MAX_FD in #( - '' | soft) :;; #( - *) - # In POSIX sh, ulimit -n is undefined. That's why the result is checked to see if it worked. - # shellcheck disable=SC3045 - ulimit -n "$MAX_FD" || - warn "Could not set maximum file descriptor limit to $MAX_FD" - esac -fi - -# Collect all arguments for the java command, stacking in reverse order: -# * args from the command line -# * the main class name -# * -classpath -# * -D...appname settings -# * --module-path (only if needed) -# * DEFAULT_JVM_OPTS, JAVA_OPTS, and GRADLE_OPTS environment variables. - -# For Cygwin or MSYS, switch paths to Windows format before running java -if "$cygwin" || "$msys" ; then - APP_HOME=$( cygpath --path --mixed "$APP_HOME" ) - CLASSPATH=$( cygpath --path --mixed "$CLASSPATH" ) - - JAVACMD=$( cygpath --unix "$JAVACMD" ) - - # Now convert the arguments - kludge to limit ourselves to /bin/sh - for arg do - if - case $arg in #( - -*) false ;; # don't mess with options #( - /?*) t=${arg#/} t=/${t%%/*} # looks like a POSIX filepath - [ -e "$t" ] ;; #( - *) false ;; - esac - then - arg=$( cygpath --path --ignore --mixed "$arg" ) - fi - # Roll the args list around exactly as many times as the number of - # args, so each arg winds up back in the position where it started, but - # possibly modified. - # - # NB: a `for` loop captures its iteration list before it begins, so - # changing the positional parameters here affects neither the number of - # iterations, nor the values presented in `arg`. - shift # remove old arg - set -- "$@" "$arg" # push replacement arg - done -fi - - -# Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. -DEFAULT_JVM_OPTS='"-Xmx64m" "-Xms64m"' - -# Collect all arguments for the java command; -# * $DEFAULT_JVM_OPTS, $JAVA_OPTS, and $GRADLE_OPTS can contain fragments of -# shell script including quotes and variable substitutions, so put them in -# double quotes to make sure that they get re-expanded; and -# * put everything else in single quotes, so that it's not re-expanded. - -set -- \ - "-Dorg.gradle.appname=$APP_BASE_NAME" \ - -classpath "$CLASSPATH" \ - org.gradle.wrapper.GradleWrapperMain \ - "$@" - -# Stop when "xargs" is not available. -if ! command -v xargs >/dev/null 2>&1 -then - die "xargs is not available" -fi - -# Use "xargs" to parse quoted args. -# -# With -n1 it outputs one arg per line, with the quotes and backslashes removed. -# -# In Bash we could simply go: -# -# readarray ARGS < <( xargs -n1 <<<"$var" ) && -# set -- "${ARGS[@]}" "$@" -# -# but POSIX shell has neither arrays nor command substitution, so instead we -# post-process each arg (as a line of input to sed) to backslash-escape any -# character that might be a shell metacharacter, then use eval to reverse -# that process (while maintaining the separation between arguments), and wrap -# the whole thing up as a single "set" statement. -# -# This will of course break if any of these variables contains a newline or -# an unmatched quote. -# - -eval "set -- $( - printf '%s\n' "$DEFAULT_JVM_OPTS $JAVA_OPTS $GRADLE_OPTS" | - xargs -n1 | - sed ' s~[^-[:alnum:]+,./:=@_]~\\&~g; ' | - tr '\n' ' ' - )" '"$@"' - -for i in 1 2 3 4 5; do "$JAVACMD" "$@" && break || sleep 15; done diff --git a/Test/benchmarks/sequence-race/java/gradlew.bat b/Test/benchmarks/sequence-race/java/gradlew.bat deleted file mode 100644 index 230c6176a5d..00000000000 --- a/Test/benchmarks/sequence-race/java/gradlew.bat +++ /dev/null @@ -1,98 +0,0 @@ -@rem -@rem Copyright 2015 the original author or authors. -@rem -@rem Licensed under the Apache License, Version 2.0 (the "License"); -@rem you may not use this file except in compliance with the License. -@rem You may obtain a copy of the License at -@rem -@rem https://www.apache.org/licenses/LICENSE-2.0 -@rem -@rem Unless required by applicable law or agreed to in writing, software -@rem distributed under the License is distributed on an "AS IS" BASIS, -@rem WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -@rem See the License for the specific language governing permissions and -@rem limitations under the License. -@rem - -@if "%DEBUG%"=="" @echo off -@rem ########################################################################## -@rem -@rem Gradle startup script for Windows -@rem -@rem ########################################################################## - -@rem Set local scope for the variables with windows NT shell -if "%OS%"=="Windows_NT" setlocal - -set DIRNAME=%~dp0 -if "%DIRNAME%"=="" set DIRNAME=. -@rem This is normally unused -set APP_BASE_NAME=%~n0 -set APP_HOME=%DIRNAME% - -@rem Resolve any "." and ".." in APP_HOME to make it shorter. -for %%i in ("%APP_HOME%") do set APP_HOME=%%~fi - -@rem Add default JVM options here. You can also use JAVA_OPTS and GRADLE_OPTS to pass JVM options to this script. -set DEFAULT_JVM_OPTS="-Xmx64m" "-Xms64m" - -@rem Find java.exe -if defined JAVA_HOME goto findJavaFromJavaHome - -set JAVA_EXE=java.exe -%JAVA_EXE% -version >NUL 2>&1 -if %ERRORLEVEL% equ 0 goto execute - -echo. -echo ERROR: JAVA_HOME is not set and no 'java' command could be found in your PATH. -echo. -echo Please set the JAVA_HOME variable in your environment to match the -echo location of your Java installation. - -goto fail - -:findJavaFromJavaHome -set JAVA_HOME=%JAVA_HOME:"=% -set JAVA_EXE=%JAVA_HOME%/bin/java.exe - -if exist "%JAVA_EXE%" goto execute - -echo. -echo ERROR: JAVA_HOME is set to an invalid directory: %JAVA_HOME% -echo. -echo Please set the JAVA_HOME variable in your environment to match the -echo location of your Java installation. - -goto fail - -:execute -@rem Setup the command line - -set CLASSPATH=%APP_HOME%\gradle\wrapper\gradle-wrapper.jar - -@rem Execute Gradle, trying at least 5 times -for %%i in (1 2 3 4 5) do ( - "%JAVA_EXE%" %DEFAULT_JVM_OPTS% %JAVA_OPTS% %GRADLE_OPTS% "-Dorg.gradle.appname=%APP_BASE_NAME%" -classpath "%CLASSPATH%" org.gradle.wrapper.GradleWrapperMain %* - if errorlevel 1 ( - sleep 15 - ) else ( - goto end - ) -) - -:end -@rem End local scope for the variables with windows NT shell -if %ERRORLEVEL% equ 0 goto mainEnd - -:fail -rem Set variable GRADLE_EXIT_CONSOLE if you need the _script_ return code instead of -rem the _cmd.exe /c_ return code! -set EXIT_CODE=%ERRORLEVEL% -if %EXIT_CODE% equ 0 set EXIT_CODE=1 -if not ""=="%GRADLE_EXIT_CONSOLE%" exit %EXIT_CODE% -exit /b %EXIT_CODE% - -:mainEnd -if "%OS%"=="Windows_NT" endlocal - -:omega diff --git a/Test/benchmarks/sequence-race/java/settings.gradle.kts b/Test/benchmarks/sequence-race/java/settings.gradle.kts deleted file mode 100644 index 1f2cdcc521f..00000000000 --- a/Test/benchmarks/sequence-race/java/settings.gradle.kts +++ /dev/null @@ -1,17 +0,0 @@ -/* - * Copyright 2014-2021 the original author or authors. - * - * Licensed under the Apache License, Version 2.0 (the "License"); - * you may not use this file except in compliance with the License. - * You may obtain a copy of the License at - * - * http://www.apache.org/licenses/LICENSE-2.0 - * - * Unless required by applicable law or agreed to in writing, software - * distributed under the License is distributed on an "AS IS" BASIS, - * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. - * See the License for the specific language governing permissions and - * limitations under the License. - */ -rootProject.name = "sequence-race" - diff --git a/customBoogie.patch b/customBoogie.patch index ceab354ade0..939dca0e77b 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -2,7 +2,7 @@ diff --git a/Source/Dafny.sln b/Source/Dafny.sln index 426b132e2..18db4aebb 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln -@@ -43,6 +43,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern.Test", "AutoExte +@@ -41,6 +41,32 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "AutoExtern.Test", "AutoExte EndProject Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}" EndProject