Merge branch 'chore-compatibility-mpl' of https://github.com/dafny-la…

…ng/dafny 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/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -655,6 +655,9 @@ private class ClassWriter : IClassWriter {
  // so we buffer it here
  _IOption<DAST._IExpression> bufferedInitializationValue = null;
 
+ // And its statements here
+ _IOption<List<DAST.Statement>> bufferedInitializationStmts = null;
+
  protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree wr, IToken tok,
  bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) {
  if (bufferedInitializationValue != null) {
@@ -663,15 +666,22 @@ private class ClassWriter : IClassWriter {
  type = type.NormalizeExpandKeepConstraints();
  if (usePlaceboValue) {
  bufferedInitializationValue = Option<DAST._IExpression>.create_None();
+ bufferedInitializationStmts = Option<List<DAST.Statement>>.create_None();
  } else {
  if (type.AsNewtype != null && type.AsNewtype.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
  var buf = new ExprBuffer(null);
- EmitExpr(type.AsNewtype.Witness, false, new BuilderSyntaxTree<ExprContainer>(buf, this), null);
+ var bufStmt = new StatementBuffer();
+ EmitExpr(type.AsNewtype.Witness, false, new BuilderSyntaxTree<ExprContainer>(buf, this),
+ new BuilderSyntaxTree<StatementContainer>(bufStmt, this));
  bufferedInitializationValue = Option<DAST._IExpression>.create_Some(buf.Finish());
+ bufferedInitializationStmts = Option<List<DAST.Statement>>.create_Some(bufStmt.PopAll());
  } else if (type.AsSubsetType != null && type.AsSubsetType.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
  var buf = new ExprBuffer(null);
- EmitExpr(type.AsSubsetType.Witness, false, new BuilderSyntaxTree<ExprContainer>(buf, this), null);
+ var bufStmt = new StatementBuffer();
+ EmitExpr(type.AsSubsetType.Witness, false, new BuilderSyntaxTree<ExprContainer>(buf, this),
+ new BuilderSyntaxTree<StatementContainer>(bufStmt, this));
  bufferedInitializationValue = Option<DAST._IExpression>.create_Some(buf.Finish());
+ bufferedInitializationStmts = Option<List<DAST.Statement>>.create_Some(bufStmt.PopAll());
  } else if (type.AsDatatype != null && type.AsDatatype.Ctors.Count == 1 && type.AsDatatype.Ctors[0].EnclosingDatatype is TupleTypeDecl tupleDecl) {
  var elems = new List<DAST._IExpression>();
  for (var i = 0; i < tupleDecl.Ctors[0].Formals.Count; i++) {
@@ -689,12 +699,14 @@ private class ClassWriter : IClassWriter {
  DAST.Expression.create_Tuple(Sequence<DAST._IExpression>.FromArray(elems.ToArray()))
  );
  }
+ bufferedInitializationStmts = Option<List<DAST.Statement>>.create_None();
  } else if (type.IsArrowType) {
  this.AddUnsupported("<i>Initializer for arrow type</i>");
  } else {
  bufferedInitializationValue = Option<DAST._IExpression>.create_Some(
  DAST.Expression.create_InitializationValue(GenType(type))
  );
+ bufferedInitializationStmts = Option<List<DAST.Statement>>.create_None();
  }
  }
  return "BUFFERED"; // used by DeclareLocal(Out)Var
@@ -786,6 +798,14 @@ private class ClassWriter : IClassWriter {
  var rhsValue = bufferedInitializationValue;
  bufferedInitializationValue = null;
 
+ if (bufferedInitializationStmts.is_Some) {
+ foreach (var stmt in bufferedInitializationStmts.dtor_value) {
+ stmtContainer.Builder.AddStatement(stmt);
+ }
+
+ bufferedInitializationStmts = null;
+ }
+
  stmtContainer.Builder.AddStatement(
  (DAST.Statement)DAST.Statement.create_DeclareVar(
  Sequence<Rune>.UnicodeFromString(name),

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -4513,8 +4513,8 @@ private class ArrayLvalueImpl : ILvalue {
  wr.Write(sep);
  var fromType = s.Args[i].Type;
  var toType = s.Method.Ins[i].Type;
- var w = EmitCoercionIfNecessary(fromType, toType, s.Tok, wr);
  var instantiatedToType = toType.Subst(s.MethodSelect.TypeArgumentSubstitutionsWithParents());
+ var w = EmitCoercionIfNecessary(fromType, instantiatedToType, s.Tok, wr, toType);
  w = EmitDowncastIfNecessary(fromType, instantiatedToType, s.Tok, w);
  EmitExpr(s.Args[i], false, w, wStmts);
  sep = ", ";
@@ -5268,8 +5268,8 @@ private class ArrayLvalueImpl : ILvalue {
  if (!e.Function.Ins[i].IsGhost) {
  wr.Write(sep);
  var fromType = e.Args[i].Type;
- var w = EmitCoercionIfNecessary(fromType, e.Function.Ins[i].Type, tok: e.tok, wr: wr);
  var instantiatedToType = e.Function.Ins[i].Type.Subst(e.TypeArgumentSubstitutionsWithParents());
+ var w = EmitCoercionIfNecessary(fromType, instantiatedToType, tok: e.tok, wr: wr, e.Function.Ins[i].Type);
  w = EmitDowncastIfNecessary(fromType, instantiatedToType, e.tok, w);
  tr(e.Args[i], w, inLetExprBody, wStmts);
  sep = ", ";

Source/DafnyLanguageServer.Test/CodeActions/CodeActionsTest.cs

@@ -27,6 +27,19 @@ public class CodeActionTest : ClientBasedLanguageServerTest {
  return await client.ResolveCodeAction(codeAction, CancellationToken);
  }
 
+ [Fact]
+ public async Task MethodKeywordCodeAction() {
+ await SetUp(o => o.Set(CommonOptionBag.RelaxDefiniteAssignment, true));
+
+ MarkupTestFile.GetPositionsAndAnnotatedRanges(@"
+method><".TrimStart(), out var source, out var positions,
+ out var ranges);
+ var documentItem = await CreateOpenAndWaitForResolve(source);
+ var position = positions[0];
+ var completionList = await RequestCodeActionAsync(documentItem, new Range(position, position));
+ Assert.Empty(completionList);
+ }
+
  [Fact]
  public async Task GitIssue4401CorrectInsertionPlace() {
  await TestCodeAction(@"

Source/DafnyLanguageServer/Plugins/DafnyCodeActionProvider.cs

@@ -89,6 +89,12 @@ public abstract class DiagnosticDafnyCodeActionProvider : DafnyCodeActionProvide
  public RangeToken? FindTokenRangeFromLspRange(IDafnyCodeActionInput input, Range range) {
  var start = range.Start;
  var startNode = input.Program.FindNode<Node>(input.Uri.ToUri(), start.ToDafnyPosition());
+ if (startNode == null) {
+ // A program should have FileModuleDefinition nodes whose ranges span the entire contents of files,
+ // But currently those nodes are missing
+ return null;
+ }
+
  var startToken = startNode.CoveredTokens.FirstOrDefault(t => t.line - 1 == start.Line && t.col - 1 == start.Character);
  if (startToken == null) {
  logger.LogError($"Could not find starting token for position {start} in node {startNode}");

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 @@ public class BasicTypes : Setup {
 }
 ".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 @@ public class BasicTypes : Setup {
 }
 ".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 @@ public class BasicTypes : Setup {
 }
 ".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 @@ public class BasicTypes : Setup {
 }
 ".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 @@ public class BasicTypes : Setup {
 }
 ".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 @@ public class BasicTypes : Setup {
 }
 ".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 @@ public class Collections : Setup {
 }
 ".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 @@ public class Collections : Setup {
 
 ".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 class Setup {
  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 @@ public class ShortCircuitRemoval : Setup {
  // 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