chore: Revert "feat: Benchmarking plugin (#4215)"

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

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

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<GenericCompilationInstrumenter> 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<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));
@@ -903,9 +894,6 @@ 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,7 +12,6 @@ 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 {
@@ -28,10 +27,6 @@ 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;
 
@@ -64,10 +59,6 @@ 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>
@@ -88,17 +79,15 @@ 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 && 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<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/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.
 /// </summary>
 public abstract class IExecutableBackend {
  /// <summary>
@@ -160,9 +160,4 @@ 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,13 +48,4 @@ 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>();
- }
 }