Merge functionality to filter out tests

.github/CONTRIBUTING.md

@@ -26,3 +26,14 @@ All other pull requests and issues can be submitted here.
 ## Code of Conduct
 
 See [`CODE_OF_CONDUCT.md`](./CODE_OF_CONDUCT.md).
+
+## FAQ
+
+### What to do if the nightly build failed but because of a "download failure"?
+
+If the test in a PR named `Build and Test / check-deep-tests / check-deep-tests` failed, clicking on its "details" reveals a view (view 1) in which you can see a failed run with the failure being something like "Error: Last run of deep-tests.yml did not succeed (some URL in parentheses).
+
+Clicking on this URL will reveal the deep tests that were run (view 2). If one of this test is just a "download failure", then one simply needs to re-run it (button on the top right).
+Once it succeeds, one has to go back to (view 1) and re-run the failed jobs, so that it will retrieve the latest successful deep tests.
+
+After doing these steps once, for other PRs, one only needs to re-run deep checks in (view 1)

RELEASE_NOTES.md

@@ -1,13 +1,15 @@
 # Upcoming
 
+- fix: Hovering over variables and methods inside cases of nested match statements work again (https://github.com/dafny-lang/dafny/pull/2334)
 - fix: Fix bug in translation of two-state predicates with heap labels. (https://github.com/dafny-lang/dafny/pull/2300)
 - fix: Check that arguments of 'unchanged' satisfy enclosing reads clause. (https://github.com/dafny-lang/dafny/pull/2302)
+- fix: Caching in the language server does not prevent gutter icons from being updated correctly. (https://github.com/dafny-lang/dafny/pull/2312)
 - fix: Correctly infer type of numeric arguments, where the type is a subset type of a newtype. (https://github.com/dafny-lang/dafny/pull/2314)
 
 # 3.7.1
 
 - fix: The Dafny runtime library for C# is now compatible with .NET Standard 2.1, as it was before 3.7.0. Its version has been updated to 1.2.0 to reflect this. (https://github.com/dafny-lang/dafny/pull/2277)
-
+- fix: Methods produced by the test generation code can now be compiled directly to C# XUnit tests (https://github.com/dafny-lang/dafny/pull/2269)
 
 # 3.7.0
 
@@ -22,7 +24,6 @@
 - fix: Prevent the language server from crashing and not responding on resolution or ghost diagnostics errors (https://github.com/dafny-lang/dafny/pull/2080)
 - fix: Various improvements to language server robustness (https://github.com/dafny-lang/dafny/pull/2254)
 
-
 # 3.6.0
 
 - feat: The `synthesize` attribute on methods with no body allows synthesizing objects based on method postconditions at compile time (currently only available for C#). See Section [22.2.20](https://dafny-lang.github.io/dafny/DafnyRef/DafnyRef#sec-synthesize-attr) of the Reference Manual. (https://github.com/dafny-lang/dafny/pull/1809)

Source/Dafny/Resolver.cs

@@ -11964,7 +11964,7 @@ public RBranchStmt(IToken tok, int branchid, List<ExtendedPattern> patterns, Lis
  }
 
  public RBranchStmt(int branchid, NestedMatchCaseStmt x, Attributes attrs = null) : base(x.Tok, branchid, new List<ExtendedPattern>()) {
- this.Body = x.Body.ConvertAll((new Cloner()).CloneStmt);
+ this.Body = new List<Statement>(x.Body); // Resolving the body will insert new elements. 
  this.Attributes = attrs;
  this.Patterns.Add(x.Pat);
  }

Source/Dafny/TestGenerationOptions.cs

@@ -7,11 +7,13 @@ namespace Microsoft.Dafny {
  public class TestGenerationOptions {
 
  public bool WarnDeadCode = false;
+ public bool PruneFailedTests = false;
  public enum Modes { None, Block, Path };
  public Modes Mode = Modes.None;
  [CanBeNull] public string TargetMethod = null;
  public uint? SeqLengthLimit = null;
  public uint TestInlineDepth = 0;
+ public uint Timeout = 100;
 
  public bool ParseOption(string name, Bpl.CommandLineParseState ps) {
  var args = ps.args;
@@ -53,6 +55,17 @@ public bool ParseOption(string name, Bpl.CommandLineParseState ps) {
  TestInlineDepth = (uint)depth;
  }
  return true;
+
+ case "generateTestTimeout":
+ var timeout = 0;
+ if (ps.GetIntArgument(ref timeout)) {
+ Timeout = (uint)timeout;
+ }
+ return true;
+
+ case "generateTestPruneFailed":
+ PruneFailedTests = true;
+ return true;
  }
 
  return false;
@@ -76,7 +89,11 @@ conjunction with loop unrolling.
 /generateTestInlineDepth:<n>
  0 is the default. When used in conjunction with /testTargetMethod, this
  argument specifies the depth up to which all non-tested methods should be
- inlined.";
+ inlined.
+/generateTestTimeout:<n>
+ Timeout generation of a test for a particular block/path after n seconds
+/generateTestPruneFailed
+ verify generated tests and remove any that flag a verification error";
 
  }
 }

Source/DafnyLanguageServer.Test/GutterStatus/CachedLinearVerificationGutterStatusTester.cs

@@ -0,0 +1,51 @@
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text.RegularExpressions;
+using System.Threading.Tasks;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Extensions;
+using Microsoft.Dafny.LanguageServer.IntegrationTest.Util;
+using Microsoft.Dafny.LanguageServer.Language;
+using Microsoft.Dafny.LanguageServer.Workspace;
+using Microsoft.Dafny.LanguageServer.Workspace.Notifications;
+using Microsoft.VisualStudio.TestTools.UnitTesting;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
+using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
+
+namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Diagnostics;
+
+[TestClass]
+public class CachedLinearVerificationGutterStatusTester : LinearVerificationGutterStatusTester {
+ private const int MaxTestExecutionTimeMs = 10000;
+
+
+
+ // To add a new test, just call VerifyTrace on a given program,
+ // the test will fail and give the correct output that can be use for the test
+ // Add '//Next<n>:' to edit a line multiple times
+
+ [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ public async Task EnsureCachingDoesNotMakeSquigglyLinesToRemain() {
+ await SetUp(new Dictionary<string, string>() {
+ { $"{VerifierOptions.Section}:{nameof(VerifierOptions.VerifySnapshots)}", "1" }
+ });
+ await VerifyTrace(@"
+ . S S | I $ | :method test() {
+ . S | | I $ | : assert true;
+ . S S | I $ | : //Next: 
+ . S S | I $ | :}");
+ }
+
+ [TestMethod, Timeout(MaxTestExecutionTimeMs)]
+ public async Task EnsureCachingDoesNotHideErrors() {
+ await SetUp(new Dictionary<string, string>() {
+ { $"{VerifierOptions.Section}:{nameof(VerifierOptions.VerifySnapshots)}", "1" }
+ });
+ await VerifyTrace(@"
+ . S [S][ ][I][S][S][ ]:method test() {
+ . S [O][O][o][Q][O][O]: assert true;
+ . S [=][=][-][~][=][=]: assert false;
+ . S [S][ ][I][S][S][ ]: //Next: 
+ . S [S][ ][I][S][S][ ]:}");
+ }
+}

Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs

@@ -427,5 +427,16 @@ function ToRelativeIndependent(): (p: Position)
 }
 ");
  }
+
+ [TestMethod]
+ public async Task HoveringVariablesInsideNestedMatchStmtWorks() {
+ await AssertHover(@"
+lemma dummy(e: int) {
+ match e {
+ case _ => var xx := 1;
+ ^[```dafny\nghost xx: int\n```]
+ }
+}");
+ }
  }
 }

Source/DafnyLanguageServer/Language/AssertionBatchCompletedObserver.cs

@@ -55,7 +55,7 @@ public void ReportEndVerifyImplementation(Implementation implementation, Boogie.
 
  public void ReportSplitResult(Split split, VCResult vcResult) {
  if (reportVerificationDiagnostics) {
- completedBatches.OnNext(new AssertionBatchResult(split, vcResult));
+ completedBatches.OnNext(new AssertionBatchResult(split.Implementation, vcResult));
  }
  }
 

Source/DafnyLanguageServer/Language/IProgramVerifier.cs

@@ -7,7 +7,7 @@
 using VC;
 
 namespace Microsoft.Dafny.LanguageServer.Language {
- public record AssertionBatchResult(Split Split, VCResult Result);
+ public record AssertionBatchResult(Implementation Implementation, VCResult Result);
 
  public record ProgramVerificationTasks(IReadOnlyList<IImplementationTask> Tasks);
 

Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

@@ -134,7 +134,7 @@ public async Task<DafnyDocument> PrepareVerificationTasksAsync(DafnyDocument loa
  }
  var implementations = verificationTasks.Select(t => t.Implementation).ToHashSet();
  var subscription = verifier.BatchCompletions.Where(c =>
- implementations.Contains(c.Split.Implementation)).Subscribe(progressReporter.ReportAssertionBatchResult);
+ implementations.Contains(c.Implementation)).Subscribe(progressReporter.ReportAssertionBatchResult);
  cancellationToken.Register(() => subscription.Dispose());
  result.GutterProgressReporter = progressReporter;
  return result;
@@ -245,6 +245,12 @@ public IObservable<DafnyDocument> Verify(DafnyDocument dafnyDocument, IImplement
 
  var statusUpdates = implementationTask.TryRun();
  if (statusUpdates == null) {
+ if (VerifierOptions.GutterStatus && implementationTask.CacheStatus is Completed completedCache) {
+ foreach (var result in completedCache.Result.VCResults) {
+ dafnyDocument.GutterProgressReporter!.ReportAssertionBatchResult(new AssertionBatchResult(implementationTask.Implementation, result));
+ }
+ dafnyDocument.GutterProgressReporter!.ReportEndVerifyImplementation(implementationTask.Implementation, completedCache.Result);
+ }
  return Observable.Empty<DafnyDocument>();
  }
 

Source/DafnyLanguageServer/Workspace/VerificationProgressReporter.cs

@@ -358,9 +358,8 @@ public void ReportAssertionBatchResult(AssertionBatchResult batchResult) {
  return;
  }
  lock (LockProcessing) {
- var split = batchResult.Split;
+ var implementation = batchResult.Implementation;
  var result = batchResult.Result;
- var implementation = split.Implementation;
  // While there is no error, just add successful nodes.
  var targetMethodNode = GetTargetMethodTree(implementation, out var implementationNode);
  if (targetMethodNode == null) {

Source/DafnyTestGeneration/Main.cs

@@ -4,6 +4,7 @@
 using System.Linq;
 using System.Threading.Tasks;
 using Microsoft.Dafny;
+
 using Program = Microsoft.Dafny.Program;
 
 namespace DafnyTestGeneration {
@@ -101,33 +102,83 @@ public static async IAsyncEnumerable<TestMethod> GetTestMethodsForProgram(
  }
  }
 
+ public static IEnumerable<string> GetTestClassPrelude(string sourceFile, DafnyInfo dafnyInfo) {
+
+ var rawName = Path.GetFileName(sourceFile).Split(".").First();
+
+ string EscapeDafnyStringLiteral(string str) {
+ return $"\"{str.Replace(@"\", @"\\")}\"";
+ }
+
+ yield return $"include {EscapeDafnyStringLiteral(sourceFile)}";
+ yield return $"module {rawName}UnitTests {{";
+ foreach (var module in dafnyInfo.ToImport) {
+ yield return $"import {module}";
+ }
+ }
+
+ private static async Task<string> RetMethodIfVerified(string sourceFile, DafnyInfo dafnyInfo, string methodStr) {
+ try {
+ string testClassPrelude = GetTestClassPrelude(sourceFile, dafnyInfo).Aggregate("", (x, y) => x = x + y + '\n');
+ string testClassWithSingleMethod = testClassPrelude + methodStr 
+ + TestMethod.EmitSynthesizeMethods() + "\n}";
+ Program? dafnyProgram = Utils.Parse(testClassWithSingleMethod, 
+ Path.GetFileName(sourceFile), new ErrorReporterSink());
+
+ if (dafnyProgram != null) {
+ var engine = Microsoft.Boogie.ExecutionEngine.CreateWithoutSharedCache(DafnyOptions.O);
+ var boogiePrograms = Translator.Translate(dafnyProgram, dafnyProgram.Reporter).ToList().ConvertAll(tuple => tuple.Item2);
+ var boogieProgram = ProgramModifier.MergeBoogiePrograms(boogiePrograms);
+ var writer = new StringWriter();
+ var uniqueId = System.Guid.NewGuid().ToString();
+
+ Task<(Microsoft.Boogie.PipelineOutcome, Microsoft.Boogie.PipelineStatistics)> 
+ boogieTask = Microsoft.Dafny.Main.BoogieOnce(writer, engine, "", "", boogieProgram, uniqueId);
+
+ var task = await Task.WhenAny(
+ boogieTask,
+ Task.Delay(System.TimeSpan.FromSeconds(DafnyOptions.O.TestGenOptions.Timeout)));
+
+ if (task == boogieTask) {
+ var (outcome, stats) = await boogieTask;
+
+ if (Microsoft.Dafny.Main.IsBoogieVerified(outcome, stats)) 
+ return methodStr;
+ }
+ }
+ return "";
+ } catch (System.Exception) {
+ return "";
+ }
+ }
+
  /// <summary>
  /// Return a Dafny class (list of lines) with tests for the given Dafny file
  /// </summary>
  public static async IAsyncEnumerable<string> GetTestClassForProgram(string sourceFile) {
 
+ TestMethod.ClearTypesToSynthesize();
  var source = new StreamReader(sourceFile).ReadToEnd();
  var program = Utils.Parse(source, sourceFile);
  if (program == null) {
  yield break;
  }
  var dafnyInfo = new DafnyInfo(program);
- var rawName = Path.GetFileName(sourceFile).Split(".").First();
-
- string EscapeDafnyStringLiteral(string str) {
- return $"\"{str.Replace(@"\", @"\\")}\"";
- }
 
- yield return $"include {EscapeDafnyStringLiteral(sourceFile)}";
- yield return $"module {rawName}UnitTests {{";
- foreach (var module in dafnyInfo.ToImport) {
- yield return $"import {module}";
- }
+ foreach (var line in GetTestClassPrelude(sourceFile, dafnyInfo))
+ yield return line;
 
  await foreach (var method in GetTestMethodsForProgram(program, dafnyInfo)) {
- yield return method.ToString();
+ string methodStr = method.ToString();
+ if (DafnyOptions.O.TestGenOptions.PruneFailedTests) {
+ yield return await RetMethodIfVerified(sourceFile, dafnyInfo, methodStr);
+ } else {
+ yield return methodStr;
+ }
  }
 
+ yield return TestMethod.EmitSynthesizeMethods();
+
  yield return "}";
  }
  }

Source/DafnyTestGeneration/ProgramModification.cs

@@ -87,9 +87,10 @@ private static DafnyOptions SetupOptions(string procedure) {
  engine.CoalesceBlocks(program);
  engine.Inline(program);
  var writer = new StringWriter();
- await engine.InferAndVerify(writer, program,
+ await Task.WhenAny(engine.InferAndVerify(writer, program,
  new PipelineStatistics(), null,
- _ => { }, uniqueId);
+ _ => { }, uniqueId),
+ Task.Delay(TimeSpan.FromSeconds(oldOptions.TestGenOptions.Timeout)));
  var log = writer.ToString();
  DafnyOptions.Install(oldOptions);
  // make sure that there is a counterexample (i.e. no parse errors, etc):

Source/DafnyTestGeneration/ProgramModifier.cs

@@ -67,7 +67,7 @@ private static void AddAxioms(Program program) {
  /// Merge Boogie Programs by removing any duplicate top level declarations
  /// (these typically come from DafnyPrelude.bpl)
  /// </summary>
- private static Program MergeBoogiePrograms(IEnumerable<Program> programs) {
+ public static Program MergeBoogiePrograms(IEnumerable<Program> programs) {
  // Merge all programs into one first:
  var program = new Program();
  foreach (var p in programs) {