Separate UI code and business logic for the resolve and verify comman…

…ds (#4798)

### Changes
At the heart of this PR is an architectural change: to lay the
foundation for separating UI code from business logic. Part of this is
to use Boogie purely as an API, instead of as a library that produces
textual output for the CLI.

This change is not _necessary_, but I believe it is a good step towards
giving us more control over the UI experience of our CLI, and to make it
easier to work with our codebase. In the future section down below are
some ideas of what this PR enables.

Because there is a lot of UI code intermingled with a lot of business
code, making this architectural change produces a lot of code changes,
so this PR only takes the first step: the pathway where UI and logic are
separated is only used when using `dafny resolve` or `dafny verify`. I
will update the remaining commands in follow-up PRs.

#### Refactoring
- Move `Compilation`, a UI agnostic back-end for driving the Dafny
compiler pipeline, from the project `LanguageServer` to `DafnyCore`, so
it can be used by the CLI as well.
- Introduce `CliCompilation` which uses the CLI as a user interface to
track the results of `Compilation`.
- Let the commands `dafny resolve` and `dafny verify` use
`CliCompilation` instead of `CompilerDriver `.
- Due to the introduction of `CliCompilation`, rename `CompilerDriver`
to `LegacyCliCompilation`, even though there are many features
`CliCompilation` does not support yet.
- Remove `DafnySymbolKind` from DafnyCore, which was a duplicate of an
LSP enum that is now directly accessible in DafnyCore

#### Behavior
- Make it easy to update .expect files by setting the flag
`DiffCommand.UpdateExpectFile` to true. This was broken before this PR.
- Configure littish tests so they time out after running for 120
minutes. They normally complete in less than 30m on all platforms, so
120m should be ample.
- Fix a bug in the cloning code, that was discovered because the CLI
tests are using the server back-end code, which clones the program after
parsing. (Is this good or bad? In the future I hope we'll have an
immutable AST so then the question becomes redundant)
- Make the order in which verification error are shown on the CLI
consistent. Now errors are always shown in the order in which they occur
in the file

  Example diff:
```
- git-issue-4074.dfy(24,11): Error: assertion might not hold
git-issue-4074.dfy(5,9): Error: assertion might not hold
git-issue-4074.dfy(14,11): Error: assertion might not hold
+ git-issue-4074.dfy(24,11): Error: assertion might not hold
```

- Consistently let CLI diagnostics have a Warning/Error label. Example
diff:
```
- github-issue-4804.dfy(19,8): Verification out of resource (Power.LemmaPowSubAddCancel (correctness))
+ github-issue-4804.dfy(19,8): Error: Verification out of resource (Power.LemmaPowSubAddCancel (correctness))
```
- The way in which custom error messages is shown is slightly different.
Example diff:
```
CustomErrorMesage.dfy(42,63): Error: this loop invariant could not be proved on entry
- CustomErrorMesage.dfy(42,63): Related message: position variable out of range
+  Related message: position variable out of range
```

### Future
This PR paves the way for:
- Adding a `--filter` option that operates on Dafny symbols/files, and
possibly also filters parsing and resolution
- Update the CLI output. 
  - Removed useless "related message" output. Example below this list.
- Improve summary output. Dafny currently reports `Dafny program
verifier finished with 21 verified, 0 errors` but the number 21 does not
refer to anything visible to the user. It would be better to report the
number of Dafny symbols that were verified.
- Do not report `Dafny program verifier did not attempt verification`
when running `dafny resolve`

```
Definedness.dfy(175,27): Error: this loop invariant could not be proved on entry
- Definedness.dfy(175,27): Related message: loop invariant violation
```

### How has this been tested?
- Updated existing tests to account for behavioral changes

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

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

@@ -53,6 +53,7 @@ jobs:
       shard-list: ${{ steps.populate-shard-list.outputs.shard-list }}
   test:
     needs: populate-matrix-dimensions
+    timeout-minutes: 120
     runs-on: ${{ matrix.os }}
     strategy:
       matrix:

Source/DafnyCore/AST/Cloner.cs

@@ -232,9 +232,8 @@ public virtual Type CloneType(Type t) {
       } else if (t is MultiSetType) {
         var tt = (MultiSetType)t;
         return new MultiSetType(tt.HasTypeArg() ? CloneType(tt.Arg) : null);
-      } else if (t is MapType) {
-        var tt = (MapType)t;
-        return new MapType(tt.Finite, CloneType(tt.Domain), CloneType(tt.Range));
+      } else if (t is MapType mapType) {
+        return new MapType(this, mapType);
       } else if (t is ArrowType) {
         var tt = (ArrowType)t;
         return new ArrowType(Tok(tt.tok), tt.Args.ConvertAll(CloneType), CloneType(tt.Result));

Source/DafnyCore/AST/Expressions/Variables/IVariableContracts.cs

@@ -1,5 +1,6 @@
 using System;
 using System.Diagnostics.Contracts;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -86,7 +87,7 @@ public string AssignUniqueName(FreshIdGenerator generator) {
   }
 
   public abstract IToken NameToken { get; }
-  public DafnySymbolKind Kind => throw new NotImplementedException();
+  public SymbolKind Kind => throw new NotImplementedException();
   public string GetDescription(DafnyOptions options) {
     throw new NotImplementedException();
   }

Source/DafnyCore/AST/Expressions/Variables/NonglobalVariable.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -134,7 +135,7 @@ public NonglobalVariable(IToken tok, string name, Type type, bool isGhost) {
   public IToken NameToken => tok;
   public override IEnumerable<INode> Children => IsTypeExplicit ? new List<Node> { Type } : Enumerable.Empty<Node>();
   public override IEnumerable<INode> PreResolveChildren => IsTypeExplicit ? new List<Node>() { Type } : Enumerable.Empty<Node>();
-  public DafnySymbolKind Kind => DafnySymbolKind.Variable;
+  public SymbolKind Kind => SymbolKind.Variable;
   public string GetDescription(DafnyOptions options) {
     return this.AsText();
   }

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -191,7 +191,9 @@ public static string ToStringWithoutNewline(System.IO.StringWriter wr) {
     }
 
     public void PrintProgramLargeStack(Program prog, bool afterResolver) {
+#pragma warning disable VSTHRD002
       DafnyMain.LargeStackFactory.StartNew(() => PrintProgram(prog, afterResolver)).Wait();
+#pragma warning restore VSTHRD002
     }
 
     public void PrintProgram(Program prog, bool afterResolver) {

Source/DafnyCore/AST/IHasUsages.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -53,7 +54,7 @@ public static string AsText(this IVariable variable) {
 }
 
 public interface ISymbol : IDeclarationOrUsage {
-  DafnySymbolKind Kind { get; }
+  SymbolKind Kind { get; }
 
   string GetDescription(DafnyOptions options);
 }
@@ -79,38 +80,4 @@ public static ISet<ISymbol> GetSymbolDescendants(ISymbol node) {
     }
     return result;
   }
-}
-
-/// <summary>
-/// This is a copy of OmniSharp.Extensions.LanguageServer.Protocol.Models.SymbolKind
-/// In the future, we'll include that package in this project, and then this copy can be removed.
-/// For now, adding that package reference is not worth its weight.
-/// </summary>
-public enum DafnySymbolKind {
-  File = 1,
-  Module = 2,
-  Namespace = 3,
-  Package = 4,
-  Class = 5,
-  Method = 6,
-  Property = 7,
-  Field = 8,
-  Constructor = 9,
-  Enum = 10,
-  Interface = 11,
-  Function = 12,
-  Variable = 13,
-  Constant = 14,
-  String = 15,
-  Number = 16,
-  Boolean = 17,
-  Array = 18,
-  Object = 19,
-  Key = 20,
-  Null = 21,
-  EnumMember = 22,
-  Struct = 23,
-  Event = 24,
-  Operator = 25,
-  TypeParameter = 26,
 }

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -46,7 +47,7 @@ public bool InferredDecreases {
   public bool AllowsAllocation => true;
 
   public override IEnumerable<INode> Children => base.Children.Concat(new[] { Rhs }.Where(x => x != null));
-  public override DafnySymbolKind Kind => DafnySymbolKind.Constant;
+  public override SymbolKind Kind => SymbolKind.Constant;
 
   public override IEnumerable<INode> PreResolveChildren => Children;
   public ModuleDefinition ContainingModule => EnclosingModule;

Source/DafnyCore/AST/Members/Constructor.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -10,7 +11,7 @@ void ObjectInvariant() {
     Contract.Invariant(Body == null || Body is DividedBlockStmt);
   }
 
-  public override DafnySymbolKind Kind => DafnySymbolKind.Constructor;
+  public override SymbolKind Kind => SymbolKind.Constructor;
   protected override string GetQualifiedName() {
     return EnclosingClass.Name;
   }

Source/DafnyCore/AST/Members/Field.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -95,7 +96,7 @@ public string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public virtual DafnySymbolKind Kind => DafnySymbolKind.Field;
+  public virtual SymbolKind Kind => SymbolKind.Field;
 
   public string GetDescription(DafnyOptions options) {
     var prefix = IsMutable ? "var" : "const";

Source/DafnyCore/AST/Members/Function.cs

@@ -5,6 +5,7 @@
 using System.Numerics;
 using DafnyCore;
 using Microsoft.Dafny.Auditor;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -485,7 +486,7 @@ public string GetTriviaContainingDocstring() {
     return null;
   }
 
-  public DafnySymbolKind Kind => DafnySymbolKind.Function;
+  public SymbolKind Kind => SymbolKind.Function;
   public bool ShouldVerify => true; // This could be made more accurate
   public ModuleDefinition ContainingModule => EnclosingClass.EnclosingModuleDefinition;
   public string GetDescription(DafnyOptions options) {

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -93,7 +94,7 @@ public bool InferredDecreases {
   public IEnumerable<IToken> OwnedTokens => CwInner.OwnedTokens;
   public RangeToken RangeToken => CwInner.RangeToken;
   public IToken NameToken => CwInner.NameToken;
-  public DafnySymbolKind Kind => CwInner.Kind;
+  public SymbolKind Kind => CwInner.Kind;
   public string GetDescription(DafnyOptions options) {
     return CwInner.GetDescription(options);
   }
@@ -127,7 +128,7 @@ public IEnumerable<INode> GetConcreteChildren() {
   public IEnumerable<IToken> OwnedTokens => throw new cce.UnreachableException();
   public RangeToken RangeToken => throw new cce.UnreachableException();
   public IToken NameToken => throw new cce.UnreachableException();
-  public DafnySymbolKind Kind => throw new cce.UnreachableException();
+  public SymbolKind Kind => throw new cce.UnreachableException();
   public string GetDescription(DafnyOptions options) {
     throw new cce.UnreachableException();
   }

Source/DafnyCore/AST/Members/Method.cs

@@ -3,6 +3,7 @@
 using System.Linq;
 using System.Numerics;
 using Microsoft.Dafny.Auditor;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -388,7 +389,7 @@ public string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public virtual DafnySymbolKind Kind => DafnySymbolKind.Method;
+  public virtual SymbolKind Kind => SymbolKind.Method;
   public string GetDescription(DafnyOptions options) {
     var qualifiedName = GetQualifiedName();
     var signatureWithoutReturn = $"{WhatKind} {qualifiedName}({string.Join(", ", Ins.Select(i => i.AsText()))})";

Source/DafnyCore/AST/Modules/ModuleDecl.cs

@@ -2,6 +2,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -80,7 +81,7 @@ public virtual string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public DafnySymbolKind Kind => DafnySymbolKind.Namespace;
+  public SymbolKind Kind => SymbolKind.Namespace;
   public string GetDescription(DafnyOptions options) {
     return $"module {Name}";
   }

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -4,6 +4,7 @@
 using System.Diagnostics.Contracts;
 using System.Linq;
 using Microsoft.Dafny.Auditor;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -1046,7 +1047,7 @@ bool InheritsFromObject(TraitDecl traitDecl) {
     return Enumerable.Empty<ISymbol>();
   });
 
-  public DafnySymbolKind Kind => DafnySymbolKind.Namespace;
+  public SymbolKind Kind => SymbolKind.Namespace;
   public string GetDescription(DafnyOptions options) {
     return $"module {Name}";
   }

Source/DafnyCore/AST/Modules/ModuleQualifiedId.cs

@@ -95,6 +95,9 @@ public ModuleDecl ResolveTarget(ErrorReporter reporter) {
   }
 
   private ModuleDecl ResolveTargetUncached(ErrorReporter reporter) {
+    if (Root == null) {
+      return null;
+    }
     var decl = Root;
     for (int k = 1; k < Path.Count; k++) {
       ModuleSignature p;

Source/DafnyCore/AST/Program.cs

@@ -15,6 +15,7 @@ void ObjectInvariant() {
     Contract.Invariant(DefaultModule != null);
   }
 
+  public bool HasParseErrors { get; set; }
   public readonly string FullName;
 
   // Resolution essentially flattens the module hierarchy, for
@@ -52,6 +53,7 @@ public Program(Cloner cloner, Program original) {
     SystemModuleManager = original.SystemModuleManager;
     Reporter = original.Reporter;
     Compilation = original.Compilation;
+    HasParseErrors = original.HasParseErrors;
 
     if (cloner.CloneResolvedFields) {
       throw new NotImplementedException();

Source/DafnyCore/AST/Statements/Assignment/LocalVariable.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -130,7 +131,7 @@ public void MakeGhost() {
     (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()).Concat(
       IsTypeExplicit ? new List<Node>() { OptionalType ?? type } : Enumerable.Empty<Node>());
 
-  public DafnySymbolKind Kind => DafnySymbolKind.Variable;
+  public SymbolKind Kind => SymbolKind.Variable;
   public string GetDescription(DafnyOptions options) {
     return this.AsText();
   }

Source/DafnyCore/AST/Tokens.cs

@@ -56,8 +56,8 @@ string Boogie.IToken.filename {
 public class Token : IToken {
 
   public Token peekedTokens; // Used only internally by Coco when the scanner "peeks" tokens. Normally null at the end of parsing
-  public static readonly Token NoToken = new Token();
-  public static readonly Token Cli = new Token();
+  public static readonly Token NoToken = new();
+  public static readonly Token Cli = new();
   public Token() : this(0, 0) { }
 
   public Token(int linenum, int colnum) {
@@ -218,6 +218,10 @@ public static RangeToken ToRange(this IToken token) {
     if (token is BoogieRangeToken boogieRangeToken) {
       return new RangeToken(boogieRangeToken.StartToken, boogieRangeToken.EndToken);
     }
+
+    if (token is NestedToken nestedToken) {
+      return ToRange(nestedToken.Outer);
+    }
     return token as RangeToken ?? new RangeToken(token, token);
   }
 }

Source/DafnyCore/AST/TypeDeclarations/DatatypeCtor.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -49,7 +50,7 @@ public string GetTriviaContainingDocstring() {
     return GetTriviaContainingDocstringFromStartTokenOrNull();
   }
 
-  public DafnySymbolKind Kind => DafnySymbolKind.EnumMember;
+  public SymbolKind Kind => SymbolKind.EnumMember;
   public string GetDescription(DafnyOptions options) {
     var formals = string.Join(", ", Formals.Select(f => f.AsText()));
     return $"{EnclosingDatatype.Name}.{Name}({formals})";

Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -81,7 +82,7 @@ public override bool IsEssentiallyEmpty() {
   }
 
   public override IEnumerable<ISymbol> ChildSymbols => base.ChildSymbols.Concat(Ctors);
-  public override DafnySymbolKind Kind => DafnySymbolKind.Enum;
+  public override SymbolKind Kind => SymbolKind.Enum;
 
   public bool SetIndent(int indent, TokenNewIndentCollector formatter) {
     var indent2 = indent + formatter.SpaceTab;

Source/DafnyCore/AST/TypeDeclarations/NonNullTypeDecl.cs

@@ -1,5 +1,6 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -45,7 +46,7 @@ public override List<Type> ParentTypes(List<Type> typeArgs) {
     return result;
   }
 
-  public override DafnySymbolKind Kind => Class.Kind;
+  public override SymbolKind Kind => Class.Kind;
 
   public override string GetDescription(DafnyOptions options) {
     return Class.GetDescription(options);

Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using OmniSharp.Extensions.LanguageServer.Protocol.Models;
 
 namespace Microsoft.Dafny;
 
@@ -48,7 +49,7 @@ public override List<Type> ParentTypes(List<Type> typeArgs) {
   }
   public bool ShouldVerify => true; // This could be made more accurate
   public ModuleDefinition ContainingModule => EnclosingModuleDefinition;
-  public override DafnySymbolKind Kind => DafnySymbolKind.Class;
+  public override SymbolKind Kind => SymbolKind.Class;
   public override string GetDescription(DafnyOptions options) {
     return "subset type";
   }