Merge branch 'master' into chore-compatibility-mpl

.github/workflows/xunit-tests-reusable.yml

@@ -100,7 +100,7 @@ jobs:
  - name: Run DafnyLanguageServer Tests (soak test - iteration ${{matrix.iteration}})
  if: inputs.soak_test
  run: |
- dotnet test --no-restore --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyLanguageServer.Test/coverlet.runsettings Source/DafnyLanguageServer.Test
+ dotnet test --no-restore --blame-crash --blame-hang-timeout 360s --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyLanguageServer.Test/coverlet.runsettings Source/DafnyLanguageServer.Test
  - name: Run DafnyLanguageServer Tests
  if: "!inputs.soak_test"
  run: |
@@ -114,7 +114,7 @@ jobs:
  run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyPipeline.Test/coverlet.runsettings Source/DafnyPipeline.Test
  - name: Run DafnyTestGeneration Tests
  if: "!inputs.soak_test"
- run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyTestGeneration.Test/coverlet.runsettings Source/DafnyTestGeneration.Test
+ run: dotnet test --no-restore --blame-hang-timeout 5m --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/DafnyTestGeneration.Test/coverlet.runsettings Source/DafnyTestGeneration.Test
  - name: Run AutoExtern Tests
  if: "!inputs.soak_test"
  run: dotnet test --no-restore --logger "console;verbosity=normal" --logger trx --collect:"XPlat Code Coverage" --settings Source/AutoExtern.Test/coverlet.runsettings Source/AutoExtern.Test

.gitignore

@@ -81,3 +81,6 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/server/*.bvd
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/model
 Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/*.html
 Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/**/*.html
+Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.dtr
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary-lib
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/libs/usesLibrary.doo

.pre-commit-config.yaml

@@ -4,5 +4,6 @@ repos:
  - id: dotnet-format
  name: dotnet-format
  language: system
- entry: dotnet format whitespace Source/Dafny.sln -v:d --include 
+ entry: dotnet format whitespace Source/Dafny.sln -v:d --include
+ exclude: 'GeneratedFromDafny|Source/DafnyRuntime/DafnyRuntimeSystemModule.cs'
  types_or: ["c#"]

Source/DafnyTestGeneration.Test/BasicTypes.cs

@@ -7,6 +7,7 @@
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
+using System.Threading;
 using System.Threading.Tasks;
 using DafnyCore.Test;
 using Microsoft.Dafny;
@@ -37,8 +38,8 @@ module SimpleTest {
 }
 ".TrimStart();
  var options = GetDafnyOptions(optionSettings, output);
- var program = await Utils.Parse(new BatchErrorReporter(options), source, false);
- var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync();
+ var program = await Parse(new BatchErrorReporter(options), source, false);
+ var methods = await GetTestMethodsForProgram(program);
  Assert.True(3 <= methods.Count);
  Assert.True(methods.All(m =>
  m.MethodName == "SimpleTest.compareToZero"));
@@ -67,8 +68,8 @@ module SimpleTest {
 }
 ".TrimStart();
  var options = GetDafnyOptions(optionSettings, output);
- var program = await Utils.Parse(new BatchErrorReporter(options), source, false);
- var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync();
+ var program = await Parse(new BatchErrorReporter(options), source, false);
+ var methods = await GetTestMethodsForProgram(program);
  Assert.True(2 <= methods.Count);
  Assert.True(methods.All(m => m.MethodName == "SimpleTest.checkIfTrue"));
  Assert.True(methods.All(m =>
@@ -103,8 +104,8 @@ module SimpleTest {
 }
 ".TrimStart();
  var options = GetDafnyOptions(optionSettings, output);
- var program = await Utils.Parse(new BatchErrorReporter(options), source, false);
- var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync();
+ var program = await Parse(new BatchErrorReporter(options), source, false);
+ var methods = await GetTestMethodsForProgram(program);
  Assert.True(7 <= methods.Count);
  Assert.True(
  methods.All(m => m.MethodName == "SimpleTest.compareToZero"));
@@ -138,8 +139,8 @@ module SimpleTest {
 }
 ".TrimStart();
  var options = GetDafnyOptions(optionSettings, output);
- var program = await Utils.Parse(new BatchErrorReporter(options), source, false);
- var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync();
+ var program = await Parse(new BatchErrorReporter(options), source, false);
+ var methods = await GetTestMethodsForProgram(program);
  Assert.True(3 <= methods.Count);
  Assert.True(
  methods.All(m => m.MethodName == "SimpleTest.compareToBase"));
@@ -171,8 +172,8 @@ module SimpleTest {
 }
 ".TrimStart();
  var options = GetDafnyOptions(optionSettings, output);
- var program = await Utils.Parse(new BatchErrorReporter(options), source, false);
- var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync();
+ var program = await Parse(new BatchErrorReporter(options), source, false);
+ var methods = await GetTestMethodsForProgram(program);
  Assert.True(3 <= methods.Count);
  Assert.True(methods.All(m => m.MethodName == "SimpleTest.compareToB"));
  Assert.True(methods.All(m =>
@@ -204,8 +205,8 @@ module SimpleTest {
 }
 ".TrimStart();
  var options = GetDafnyOptions(optionSettings, output);
- var program = await Utils.Parse(new BatchErrorReporter(options), source, false);
- var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync();
+ var program = await Parse(new BatchErrorReporter(options), source, false);
+ var methods = await GetTestMethodsForProgram(program);
  Assert.True(2 <= methods.Count);
  Assert.True(methods.All(m => m.MethodName == "SimpleTest.compareToB"));
  Assert.True(methods.All(m =>

Source/DafnyTestGeneration.Test/Collections.cs

@@ -40,8 +40,8 @@ module SimpleTest {
 }
 ".TrimStart();
  var options = GetDafnyOptions(optionSettings, output);
- var program = await Utils.Parse(new BatchErrorReporter(options), source, false);
- var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync();
+ var program = await Parse(new BatchErrorReporter(options), source, false);
+ var methods = await GetTestMethodsForProgram(program);
  Assert.True(3 <= methods.Count);
  Assert.True(methods.All(m =>
  m.MethodName == "SimpleTest.tuple"));
@@ -84,8 +84,8 @@ module C {
 
 ".TrimStart();
  var options = GetDafnyOptions(optionSettings, output);
- var program = await Utils.Parse(new BatchErrorReporter(options), source, false);
- var methods = await TestGenerator.GetTestMethodsForProgram(program).ToListAsync();
+ var program = await Parse(new BatchErrorReporter(options), source, false);
+ var methods = await GetTestMethodsForProgram(program);
  Assert.True(3 <= methods.Count);
  Assert.True(methods.All(m =>
  m.MethodName == "C.compareStringLengthToOne"));

Source/DafnyTestGeneration.Test/Setup.cs

@@ -4,15 +4,28 @@
 #nullable disable
 using System;
 using System.Collections.Generic;
+using System.Collections.Immutable;
 using System.IO;
+using System.Linq;
+using System.Threading;
+using System.Threading.Tasks;
 using Microsoft.Boogie;
 using Microsoft.Dafny;
 using Xunit;
+using Program = Microsoft.Dafny.Program;
 using Token = Microsoft.Dafny.Token;
 
 namespace DafnyTestGeneration.Test {
 
  public class Setup {
+ private readonly CancellationTokenSource cancellationTokenSource = new();
+
+ public Setup() {
+ cancellationTokenSource.CancelAfter(TimeSpan.FromSeconds(50));
+ }
+
+ public CancellationToken CancellationToken => cancellationTokenSource.Token;
+
  protected static DafnyOptions GetDafnyOptions(List<Action<DafnyOptions>> optionSettings, TextWriter writer, params string[] arguments) {
  var options = DafnyOptions.CreateUsingOldParser(writer, TextReader.Null, arguments ?? System.Array.Empty<string>());
  options.DefiniteAssignmentLevel = 3;
@@ -33,5 +46,16 @@ public static TheoryData<List<Action<DafnyOptions>>> OptionSettings() {
  optionSettings.Add(new() { options => options.TypeEncodingMethod = CoreOptions.TypeEncoding.Predicates });
  return optionSettings;
  }
+
+ /// <summary>
+ /// Parse a string read (from a certain file) to a Dafny Program
+ /// </summary>
+ public Task<Program> /*?*/ Parse(ErrorReporter reporter, string source, bool resolve = true, Uri uri = null) {
+ return Utils.Parse(reporter, source, resolve, uri, cancellationToken: CancellationToken);
+ }
+
+ protected Task<List<TestMethod>> GetTestMethodsForProgram(Program program) {
+ return TestGenerator.GetTestMethodsForProgram(program).ToListAsync(CancellationToken).AsTask().WaitAsync(CancellationToken);
+ }
  }
 }

Source/DafnyTestGeneration.Test/ShortCircuitRemoval.cs

@@ -35,7 +35,7 @@ private async Task<Method> ShortCircuitRemovalTest(string source, string expecte
  // If the following assertion fails, rename the corresponding variables in expected output of each test
  Assert.Equal(RemoveShortCircuitingRewriter.TmpVarPrefix, "#tmp");
  var options = GetDafnyOptions(new List<Action<DafnyOptions>>(), output);
- var program = await Utils.Parse(new BatchErrorReporter(options), source, false);
+ var program = await Parse(new BatchErrorReporter(options), source, false);
  var success = InliningTranslator.TranslateForFutureInlining(program, options, out var boogieProgram);
  Assert.True(success);
  var method = program.DefaultModuleDef.Children