Fix: Formatting within the IDE wasn't working anymore (#4274)

This PR fixes #4269 and fixes #4270
I first added unit tests for the cases that were failing. What really
solved the issue was that I had to implement proper cloning for
- methods, that were not keeping BodyStartTok
- formals, that were not keeping RangeToken

Then I also added for all formatting test a case when it tries to clone
all members before formatting, like VSCode does, which unveiled 3 more
formatting issues:
```
method Test() {
  g := new ClassName.ConstructorName(
      argument1b, // Two extra spaces
      argument2b,
      argument3b
    );
  var g := new ClassName.ConstructorName(
           argument1, // Missing two extra spaces (when block mode activated)
           argument2,
           argument3
         );
...
  && unchanged(
       this,
       c
     )
     && old( // Extra undesired space here
         c.c
       ) == c.c
  && fresh(
       c.c
     )
```
I also solved the above issues by:
* Ensuring the `RangeToken` of `TypeRHS` is preserved after cloning by
modifying its topmost cloning parent `AssignmentRHS`
* Ensure we iterate on pre resolved children to get `OwnedToken`
(otherwise some cloned expressions were crashing)
* Ensure `UnchangedExpr` is cloned with the same pattern as everyone
else (otherwise the `RangeToken` wasn't kept)


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

Source/DafnyCore.Test/ClonerTest.cs

@@ -0,0 +1,47 @@
+using Microsoft.Dafny;
+using Microsoft.Extensions.Logging;
+using Microsoft.Extensions.Logging.Abstractions;
+using Tomlyn;
+
+namespace DafnyCore.Test;
+
+public class ClonerTest {
+  class DummyDecl : Declaration {
+    public DummyDecl(Cloner cloner, Declaration original) : base(cloner, original) {
+    }
+
+    public DummyDecl(RangeToken rangeToken, Name name, Attributes attributes, bool isRefining) : base(rangeToken, name,
+      attributes, isRefining) {
+    }
+  }
+
+  [Fact]
+  public void ClonerKeepsBodyStartTok() {
+    var tokenBodyStart = new Token() { line = 2 };
+    var rangeToken = new RangeToken(Token.NoToken, Token.NoToken);
+    var specificationFrame = new LiteralExpr(Microsoft.Dafny.Token.NoToken, 1);
+    var formal1 = new Formal(Token.NoToken, "a", Microsoft.Dafny.Type.Bool, true, false, null) {
+      RangeToken = new RangeToken(tokenBodyStart, tokenBodyStart),
+      IsTypeExplicit = true
+    };
+    var formal2 = new Formal(Token.NoToken, "b", Microsoft.Dafny.Type.Bool, true, false, null) {
+      RangeToken = new RangeToken(tokenBodyStart, tokenBodyStart),
+      IsTypeExplicit = false
+    };
+    var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"),
+      false, false, new List<TypeParameter>(), new List<Formal> { formal1, formal2 },
+      new List<Formal>(), new List<AttributedExpression>(),
+      new Specification<FrameExpression>(new List<FrameExpression>(), null),
+      new List<AttributedExpression>(), new Specification<Expression>(new List<Expression>(), null),
+      new BlockStmt(rangeToken, new List<Statement>()), null, Token.NoToken, false);
+
+    dummyDecl.BodyStartTok = tokenBodyStart;
+    var cloner = new Cloner();
+    var dummyDecl2 = cloner.CloneMethod(dummyDecl);
+    Assert.Equal(2, dummyDecl2.BodyStartTok.line);
+    Assert.Equal(2, dummyDecl2.Ins[0].RangeToken.StartToken.line);
+    Assert.True(dummyDecl2.Ins[0].IsTypeExplicit);
+    Assert.Equal(2, dummyDecl2.Ins[1].RangeToken.StartToken.line);
+    Assert.False(dummyDecl2.Ins[1].IsTypeExplicit);
+  }
+}

Source/DafnyCore/AST/Expressions/Heap/UnchangedExpr.cs

@@ -13,11 +13,15 @@ void ObjectInvariant() {
   }
 
   public UnchangedExpr Clone(Cloner cloner) {
-    var result = new UnchangedExpr(cloner.Tok(tok), Frame.ConvertAll(cloner.CloneFrameExpr), At);
+    return new UnchangedExpr(cloner, this);
+  }
+
+  public UnchangedExpr(Cloner cloner, UnchangedExpr original) : base(cloner, original) {
+    Frame = original.Frame.ConvertAll(cloner.CloneFrameExpr);
+    At = original.At;
     if (cloner.CloneResolvedFields) {
-      result.AtLabel = AtLabel;
+      AtLabel = original.AtLabel;
     }
-    return result;
   }
 
   public UnchangedExpr(IToken tok, List<FrameExpression> frame, string/*?*/ at)

Source/DafnyCore/AST/Members/Constructor.cs

@@ -47,6 +47,9 @@ public Constructor(RangeToken rangeToken, Name name,
     Contract.Requires(decreases != null);
   }
 
+  public Constructor(Cloner cloner, Constructor original) : base(cloner, original) {
+  }
+
   public bool HasName {
     get {
       return Name != "_ctor";

Source/DafnyCore/AST/Members/ExtremeLemma.cs

@@ -14,6 +14,10 @@ public abstract class ExtremeLemma : Method {
 
   public override IEnumerable<Node> PreResolveChildren => base.Children;
 
+  public ExtremeLemma(Cloner cloner, ExtremeLemma lemma) : base(cloner, lemma) {
+    TypeOfK = lemma.TypeOfK;
+  }
+
   public ExtremeLemma(RangeToken rangeToken, Name name,
     bool hasStaticKeyword, ExtremePredicate.KType typeOfK,
     List<TypeParameter> typeArgs,
@@ -62,6 +66,9 @@ public LeastLemma(RangeToken rangeToken, Name name,
     Contract.Requires(cce.NonNullElements(ens));
     Contract.Requires(decreases != null);
   }
+
+  public LeastLemma(Cloner cloner, LeastLemma leastLemma) : base(cloner, leastLemma) {
+  }
 }
 
 public class GreatestLemma : ExtremeLemma {
@@ -87,4 +94,7 @@ public GreatestLemma(RangeToken rangeToken, Name name,
     Contract.Requires(cce.NonNullElements(ens));
     Contract.Requires(decreases != null);
   }
+
+  public GreatestLemma(Cloner cloner, GreatestLemma greatestLemma) : base(cloner, greatestLemma) {
+  }
 }

Source/DafnyCore/AST/Members/Lemma.cs

@@ -18,6 +18,9 @@ public Lemma(RangeToken rangeToken, Name name,
     : base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
   }
 
+  public Lemma(Cloner cloner, Lemma lemma) : base(cloner, lemma) {
+  }
+
   public override bool AllowsAllocation => false;
 }
 
@@ -47,5 +50,8 @@ public TwoStateLemma(RangeToken rangeToken, Name name,
     Contract.Requires(decreases != null);
   }
 
+  public TwoStateLemma(Cloner cloner, TwoStateLemma lemma) : base(cloner, lemma) {
+  }
+
   public override bool AllowsAllocation => false;
 }

Source/DafnyCore/AST/Members/MemberDecl.cs

@@ -8,7 +8,8 @@ namespace Microsoft.Dafny;
 public abstract class MemberDecl : Declaration {
   public abstract string WhatKind { get; }
   public virtual string WhatKindMentionGhost => (IsGhost ? "ghost " : "") + WhatKind;
-  public readonly bool HasStaticKeyword;
+  protected bool hasStaticKeyword;
+  public bool HasStaticKeyword => hasStaticKeyword;
   public virtual bool IsStatic {
     get {
       return HasStaticKeyword || EnclosingClass is DefaultClassDecl;
@@ -17,7 +18,7 @@ public virtual bool IsStatic {
 
   public virtual bool IsOpaque => false;
 
-  protected readonly bool isGhost;
+  protected bool isGhost;
   public bool IsGhost { get { return isGhost; } }
 
   public string ModifiersAsString() {
@@ -58,11 +59,17 @@ public bool Overrides(MemberDecl possiblyOverriddenMember) {
     return false;
   }
 
+  protected MemberDecl(Cloner cloner, MemberDecl original) : base(cloner, original) {
+    this.hasStaticKeyword = original.hasStaticKeyword;
+    this.EnclosingClass = original.EnclosingClass;
+    this.isGhost = original.isGhost;
+  }
+
   protected MemberDecl(RangeToken rangeToken, Name name, bool hasStaticKeyword, bool isGhost, Attributes attributes, bool isRefining)
     : base(rangeToken, name, attributes, isRefining) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
-    HasStaticKeyword = hasStaticKeyword;
+    this.hasStaticKeyword = hasStaticKeyword;
     this.isGhost = isGhost;
   }
   /// <summary>

Source/DafnyCore/AST/Members/Method.cs

@@ -1,6 +1,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using System.Threading;
 using Microsoft.Dafny.Auditor;
 
 namespace Microsoft.Dafny;
@@ -101,6 +102,22 @@ void ObjectInvariant() {
     Contract.Invariant(Decreases != null);
   }
 
+  public Method(Cloner cloner, Method original) : base(cloner, original) {
+    this.TypeArgs = cloner.CloneResolvedFields ? original.TypeArgs : original.TypeArgs.ConvertAll(cloner.CloneTypeParam);
+    this.Ins = original.Ins.ConvertAll(p => cloner.CloneFormal(p, false));
+    if (original.Outs != null) {
+      this.Outs = original.Outs.ConvertAll(p => cloner.CloneFormal(p, false));
+    }
+
+    this.Req = original.Req.ConvertAll(cloner.CloneAttributedExpr);
+    this.Mod = cloner.CloneSpecFrameExpr(original.Mod);
+    this.Decreases = cloner.CloneSpecExpr(original.Decreases);
+    this.Ens = original.Ens.ConvertAll(cloner.CloneAttributedExpr);
+    this.Body = cloner.CloneMethodBody(original);
+    this.SignatureEllipsis = original.SignatureEllipsis;
+    this.IsByMethod = original.IsByMethod;
+  }
+
   public Method(RangeToken rangeToken, Name name,
     bool hasStaticKeyword, bool isGhost,
     [Captured] List<TypeParameter> typeArgs,

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

@@ -5,13 +5,10 @@ namespace Microsoft.Dafny;
 
 public abstract class AssignmentRhs : TokenNode, IAttributeBearingDeclaration {
   private Attributes attributes;
+
   public Attributes Attributes {
-    get {
-      return attributes;
-    }
-    set {
-      attributes = value;
-    }
+    get { return attributes; }
+    set { attributes = value; }
   }
 
   public bool HasAttributes() {
@@ -21,12 +18,14 @@ public bool HasAttributes() {
   internal AssignmentRhs(Cloner cloner, AssignmentRhs original) {
     tok = cloner.Tok(original.tok);
     Attributes = cloner.CloneAttributes(original.Attributes);
+    RangeToken = cloner.Range(original.rangeToken);
   }
 
   internal AssignmentRhs(IToken tok, Attributes attrs = null) {
     this.tok = tok;
     Attributes = attrs;
   }
+
   public abstract bool CanAffectPreviouslyKnownExpressions { get; }
 
   /// <summary>
@@ -38,9 +37,7 @@ internal AssignmentRhs(IToken tok, Attributes attrs = null) {
   /// Returns the non-null non-specification subexpressions of the AssignmentRhs.
   /// </summary>
   public virtual IEnumerable<Expression> NonSpecificationSubExpressions {
-    get {
-      yield break;
-    }
+    get { yield break; }
   }
 
   /// <summary>

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

@@ -3,12 +3,19 @@
 
 namespace Microsoft.Dafny;
 
-public class ExprRhs : AssignmentRhs {
+public class ExprRhs : AssignmentRhs, ICloneable<ExprRhs> {
   public readonly Expression Expr;
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(Expr != null);
   }
+  public ExprRhs Clone(Cloner cloner) {
+    return new ExprRhs(cloner, this);
+  }
+
+  public ExprRhs(Cloner cloner, ExprRhs original) : base(cloner, original) {
+    Expr = cloner.CloneExpr(original.Expr);
+  }
 
   public ExprRhs(Expression expr, Attributes attrs = null)
     : base(expr.tok, attrs) {

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

@@ -3,10 +3,16 @@
 
 namespace Microsoft.Dafny;
 
-public class HavocRhs : AssignmentRhs {
-  public HavocRhs(IToken tok)
-    : base(tok) {
+public class HavocRhs : AssignmentRhs, ICloneable<HavocRhs> {
+  public HavocRhs Clone(Cloner cloner) {
+    return new HavocRhs(cloner, this);
   }
+  public HavocRhs(IToken tok) : base(tok) {
+  }
+
+  private HavocRhs(Cloner cloner, HavocRhs havocRhs) : base(cloner, havocRhs) {
+  }
+
   public override bool CanAffectPreviouslyKnownExpressions { get { return false; } }
   public override IEnumerable<Node> Children => Enumerable.Empty<Node>();
   public override IEnumerable<Node> PreResolveChildren => Enumerable.Empty<Node>();

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

@@ -192,11 +192,14 @@ public override IEnumerable<Node> Children {
     }
   }
   public override IEnumerable<Node> PreResolveChildren =>
-    new[] { EType, Type }.OfType<UserDefinedType>()
+    new[] { EType, Type, Path }.OfType<Node>()
       .Concat<Node>(ArrayDimensions ?? Enumerable.Empty<Node>())
       .Concat<Node>(ElementInit != null ? new[] { ElementInit } : Enumerable.Empty<Node>())
       .Concat<Node>(InitDisplay ?? Enumerable.Empty<Node>())
-      .Concat<Node>((Bindings != null ? Arguments : null) ?? Enumerable.Empty<Node>());
+      .Concat<Node>((Bindings != null && Bindings.ArgumentBindings != null ?
+                       Bindings.ArgumentBindings.Select(a => a.Actual) : null) ??
+                    (Bindings != null ? Arguments : null) ??
+                    Enumerable.Empty<Node>());
 
   public override IEnumerable<Statement> PreResolveSubStatements => Enumerable.Empty<Statement>();
 }

Source/DafnyCore/AST/Statements/BlockStmt.cs

@@ -11,7 +11,7 @@ public BlockStmt Clone(Cloner cloner) {
     return new BlockStmt(cloner, this);
   }
 
-  public BlockStmt(Cloner cloner, BlockStmt original) : base(cloner, original) {
+  protected BlockStmt(Cloner cloner, BlockStmt original) : base(cloner, original) {
     Body = original.Body.Select(cloner.CloneStmt).ToList();
   }
 

Source/DafnyCore/AST/TypeDeclarations/Declaration.cs

@@ -28,6 +28,8 @@ void ObjectInvariant() {
 
   protected Declaration(Cloner cloner, Declaration original) : base(cloner, original) {
     NameNode = original.NameNode.Clone(cloner);
+    BodyStartTok = cloner.Tok(original.BodyStartTok);
+    Attributes = cloner.CloneAttributes(original.Attributes);
   }
 
   protected Declaration(RangeToken rangeToken, Name name, Attributes attributes, bool isRefining) : base(rangeToken) {

Source/DafnyCore/Generic/Node.cs

@@ -328,7 +328,7 @@ void UpdateStartEndTokRecursive(Node node) {
           }
         }
 
-        Children.Iter(UpdateStartEndTokRecursive);
+        PreResolveChildren.Iter(UpdateStartEndTokRecursive);
 
         if (FormatTokens != null) {
           foreach (var token in FormatTokens) {