Merge remote-tracking branch 'upstream/master' into decreasesto

Source/DafnyCore/AST/Substituter.cs

@@ -12,9 +12,9 @@ namespace Microsoft.Dafny {
   /// particular, the substituter does not copy parts of an expression that are used only for well-formedness checks.
   /// </summary>
   public class Substituter {
-    protected readonly Expression receiverReplacement;
-    protected readonly Dictionary<IVariable, Expression> substMap;
-    protected readonly Dictionary<TypeParameter, Type> typeMap;
+    protected Expression receiverReplacement { get; }
+    public Dictionary<IVariable, Expression> substMap { get; }
+    public Dictionary<TypeParameter, Type> typeMap { get; }
     protected readonly Label oldHeapLabel;
     [CanBeNull] protected readonly SystemModuleManager SystemModuleManager; // if non-null, substitutions into FunctionCallExpr's will be wrapped
 

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -1184,7 +1184,7 @@ protected override string FullTypeName(UserDefinedType udt, MemberDecl member =
       };
     }
 
-    protected override void EmitThis(ConcreteSyntaxTree wr, bool callToInheritedMember) {
+    protected override void EmitThis(ConcreteSyntaxTree wr, bool _ = false) {
       var isTailRecursive = enclosingMethod is { IsTailRecursive: true } || enclosingFunction is { IsTailRecursive: true };
       wr.Write(isTailRecursive ? "_this" : "self");
     }

Source/DafnyCore/Backends/SinglePassCodeGenerator.cs

@@ -7,7 +7,6 @@
 //-----------------------------------------------------------------------------
 using System;
 using System.Collections.Generic;
-using System.CommandLine;
 using System.Linq;
 using System.Numerics;
 using System.IO;
@@ -3792,7 +3791,7 @@ protected virtual ConcreteSyntaxTree EmitAnd(Action<ConcreteSyntaxTree> lhs, Con
     /// <summary>
     /// Returns a type whose target type is the same as the target type of the values returned by the emitted enumeration.
     /// The output value of "collectionWriter" is an action that emits the enumeration.
-    /// Note that, while the values returned bny the enumeration have the target representation of "bv.Type", they may
+    /// Note that, while the values returned by the enumeration have the target representation of "bv.Type", they may
     /// not be legal "bv.Type" values -- that is, it could be that "bv.Type" has further constraints that need to be checked.
     /// </summary>
     Type CompileCollection(BoundedPool bound, IVariable bv, bool inLetExprBody, bool includeDuplicates,
@@ -5568,6 +5567,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
         //   }
         //   return Dafny.Set<G>.FromCollection(_coll);
         // }))()
+        // We also split R(i,j,k,l) to evaluate it as early as possible.
         wr = CaptureFreeVariables(e, true, out var su, inLetExprBody, wr, ref wStmts);
         e = (SetComprehension)su.Substitute(e);
 
@@ -5580,18 +5580,22 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
         EmitSetBuilder_New(wr, e, collectionName);
         var n = e.BoundVars.Count;
         Contract.Assert(e.Bounds.Count == n);
+        var processedBounds = new HashSet<IVariable>();
+        List<(Expression conj, ISet<IVariable> frees)> unusedConjuncts = Expression.Conjuncts(e.Range).Select(conj => (conj, ModuleResolver.FreeVariables(conj))).ToList();
+        unusedConjuncts.ForEach(entry => entry.frees.IntersectWith(e.BoundVars));
+        wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr);
         for (var i = 0; i < n; i++) {
           var bound = e.Bounds[i];
           var bv = e.BoundVars[i];
+          processedBounds.Add(bv);
           var tmpVar = ProtectedFreshId("_compr_");
           var wStmtsLoop = wr.Fork();
           var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, wStmtsLoop);
           wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, true, inLetExprBody, e.tok, collection, wr);
+          wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr);
         }
 
-        var thn = EmitIf(out var guardWriter, false, wr);
-        EmitExpr(e.Range, inLetExprBody, guardWriter, wStmts);
-        EmitSetBuilder_Add(setType, collectionName, e.Term, inLetExprBody, thn);
+        EmitSetBuilder_Add(setType, collectionName, e.Term, inLetExprBody, wr);
         var returned = EmitReturnExpr(bwr);
         GetCollectionBuilder_Build(setType, e.tok, collectionName, returned, wStmts);
 
@@ -5613,6 +5617,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
         //   }
         //   return Dafny.Map<U, V>.FromCollection(_coll);
         // }))()
+        // We also split R(i,j,k,l) to evaluate it as early as possible.
         wr = CaptureFreeVariables(e, true, out var su, inLetExprBody, wr, ref wStmts);
         e = (MapComprehension)su.Substitute(e);
 
@@ -5627,18 +5632,22 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
         EmitMapBuilder_New(wr, e, collection_name);
         var n = e.BoundVars.Count;
         Contract.Assert(e.Bounds.Count == n);
+        var processedBounds = new HashSet<IVariable>();
+        List<(Expression conj, ISet<IVariable> frees)> unusedConjuncts = Expression.Conjuncts(e.Range).Select(conj => (conj, ModuleResolver.FreeVariables(conj))).ToList();
+        unusedConjuncts.ForEach(entry => entry.frees.IntersectWith(e.BoundVars));
+        wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr);
         for (var i = 0; i < n; i++) {
           var bound = e.Bounds[i];
           var bv = e.BoundVars[i];
+          processedBounds.Add(bv);
           var tmpVar = ProtectedFreshId("_compr_");
           var wStmtsLoop = wr.Fork();
           var elementType = CompileCollection(bound, bv, inLetExprBody, true, null, out var collection, wStmtsLoop);
           wr = CreateGuardedForeachLoop(tmpVar, elementType, bv, true, false, bv.tok, collection, wr);
+          wr = EmitGuardFragment(unusedConjuncts, processedBounds, wr);
         }
 
-        var thn = EmitIf(out var guardWriter, false, wr);
-        EmitExpr(e.Range, inLetExprBody, guardWriter, wStmts);
-        var termLeftWriter = EmitMapBuilder_Add(mapType, e.tok, collection_name, e.Term, inLetExprBody, thn);
+        var termLeftWriter = EmitMapBuilder_Add(mapType, e.tok, collection_name, e.Term, inLetExprBody, wr);
         if (e.TermLeft == null) {
           Contract.Assert(e.BoundVars.Count == 1);
           EmitIdentifier(IdName(e.BoundVars[0]), termLeftWriter);
@@ -5652,7 +5661,22 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
       } else if (expr is LambdaExpr) {
         var e = (LambdaExpr)expr;
 
+        IVariable receiver = null;
+        if (enclosingMethod is { IsTailRecursive: true } || enclosingFunction is { IsTailRecursive: true }) {
+          var name = ProtectedFreshId("_this");
+          var ty = ModuleResolver.GetThisType(e.tok, thisContext);
+          receiver = new LocalVariable(RangeToken.NoToken, name, ty, false) {
+            type = ty
+          };
+          var _this = new ThisExpr(thisContext);
+          wr = EmitBetaRedex(new List<string>() { IdName(receiver) }, new List<Expression>() { _this }, new List<Type>() { _this.Type }, expr.Type, expr.tok, inLetExprBody, wr, ref wStmts);
+        }
+
         wr = CaptureFreeVariables(e, false, out var su, inLetExprBody, wr, ref wStmts);
+        if (receiver != null) {
+          su = new Substituter(new IdentifierExpr(e.tok, receiver), su.substMap, su.typeMap);
+        }
+
         wr = CreateLambda(e.BoundVars.ConvertAll(bv => bv.Type), Token.NoToken, e.BoundVars.ConvertAll(IdName), e.Body.Type, wr, wStmts);
         wStmts = wr.Fork();
         wr = EmitReturnExpr(wr);
@@ -5678,6 +5702,21 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression
       }
+      ConcreteSyntaxTree EmitGuardFragment(List<(Expression conj, ISet<IVariable> frees)> unusedConjuncts, HashSet<IVariable> processedBounds, ConcreteSyntaxTree wr) {
+        Expression localGuard = Expression.CreateBoolLiteral(expr.tok, true);
+
+        foreach (var entry in unusedConjuncts.ToList().Where(entry => entry.frees.IsSubsetOf(processedBounds))) {
+          localGuard = Expression.CreateAnd(localGuard, entry.conj);
+          unusedConjuncts.Remove(entry);
+        }
+
+        if (!LiteralExpr.IsTrue(localGuard)) {
+          wr = EmitIf(out var guardWriter, false, wr);
+          EmitExpr(localGuard, inLetExprBody, guardWriter, wStmts);
+        }
+
+        return wr;
+      }
     }
 
     private void CompileTypeTest(TypeTestExpr expr, bool inLetExprBody, ConcreteSyntaxTree wr, ref ConcreteSyntaxTree wStmts) {

Source/DafnyCore/Generic/Name.cs

@@ -12,7 +12,7 @@ namespace Microsoft.Dafny;
 public class Name : RangeNode {
 
   public Name Prepend(string prefix) {
-    return new Name(RangeToken, prefix + Value);
+    return new Name(RangeToken.MakeAutoGenerated(), prefix + Value);
   }
 
   public Name Append(string suffix) {

Source/DafnyLanguageServer.Test/Lookup/WorkspaceSymbolTest.cs

@@ -51,11 +51,13 @@ public async Task WorkspaceSymbolsAcrossFiles() {
     [Fact]
     public async Task AllRelevantSymbolKindsDetected() {
       var documentItem = await GetDocumentItem(@"
+
 class TestClass {}
 
 module TestModule {}
 
-function TestFunction(): int { 42 }
+function TransparentTestFunction(): int { 42 }
+opaque function OpaqueTestFunction(): int { 42 }
 
 method TestMethod() returns (x: int) {
   x := 42;
@@ -72,18 +74,25 @@ trait TestTrait {}
       var testSymbols = new List<string> {
         "TestClass",
         "TestModule",
-        "TestFunction",
+        "TestMethod",
+        "TransparentTestFunction",
+        "OpaqueTestFunction",
         "TestDatatype",
         "TestConstructor",
         "TestTrait",
         "TestPredicate",
       };
 
-      var response = await client.RequestWorkspaceSymbols(new WorkspaceSymbolParams {
+      var allResponse = await client.RequestWorkspaceSymbols(new WorkspaceSymbolParams {
         Query = "test"
       });
+      Assert.Equal(testSymbols.Count, allResponse.Count());
       foreach (var testSymbol in testSymbols) {
-        Assert.True(response.Any(symbol => symbol.Name.Contains(testSymbol)),
+        var singleResponse = await client.RequestWorkspaceSymbols(new WorkspaceSymbolParams() {
+          Query = testSymbol
+        });
+        Assert.Single(singleResponse);
+        Assert.True(allResponse.Count(symbol => symbol.Name == testSymbol) == 1,
           $"Could not find {testSymbol}");
       }
     }

Source/DafnyLanguageServer/Handlers/DafnyWorkspaceSymbolHandler.cs

@@ -35,36 +35,39 @@ protected override WorkspaceSymbolRegistrationOptions CreateRegistrationOptions(
       foreach (var projectManager in projects.Managers) {
         cancellationToken.ThrowIfCancellationRequested();
         var state = await projectManager.GetStateAfterParsingAsync();
-        foreach (var def in state.SymbolTable.Definitions) {
+        foreach (ISymbol symbol in state.SymbolTable.Definitions) {
           cancellationToken.ThrowIfCancellationRequested();
 
-          if (!def.Kind.HasValue) {
-            logger.LogWarning($"Definition without kind in symbol table: {def}");
+          if (!symbol.Kind.HasValue) {
+            logger.LogWarning($"Definition without kind in symbol table: {symbol}");
             continue;
           }
 
           // CreateLocation called below uses the .Uri field of Tokens which
           // seems to occasionally be null while testing this from VSCode
-          if (def.NameToken == null || def.NameToken.Uri == null) {
-            logger.LogWarning($"Definition without name token in symbol table: {def}");
+          if (symbol.NameToken == null || symbol.NameToken.Uri == null) {
+            logger.LogWarning($"Definition without name token in symbol table: {symbol}");
             continue;
           }
-          if (def.NameToken.val == null) {
-            logger.LogWarning($"Definition without name in symbol table: {def}");
+
+          if (symbol.NameToken.val == null) {
+            logger.LogWarning($"Definition without name in symbol table: {symbol}");
+          }
+          if (AutoGeneratedToken.Is(symbol.NameToken)) {
             continue;
           }
 
           // This matching could be improved by using the qualified name of the symbol here.
-          var name = def.NameToken.val;
+          var name = symbol.NameToken.val!;
           if (name.ToLower().Contains(queryText)) {
             // The fewer extra characters there are in the string, the
             // better the match.
             var matchDistance = name.Length - queryText.Length;
             result.TryAdd(new SymbolInformation {
               Name = name,
-              ContainerName = def.Kind.ToString(),
-              Kind = def.Kind.Value,
-              Location = DiagnosticUtil.CreateLocation(def.NameToken)
+              ContainerName = symbol.Kind.ToString(),
+              Kind = symbol.Kind.Value,
+              Location = DiagnosticUtil.CreateLocation(symbol.NameToken)
             }, matchDistance);
           }
         }

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3320.dfy

@@ -0,0 +1,17 @@
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
+
+datatype Dt = A | B(b: set<nat>)
+
+function SetComprehension(s: seq<Dt>): set<nat> {
+  set i, b | 0 <= i < |s| && s[i].B? && b in s[i].b && 1 != 2 :: b
+}
+
+function MapComprehension(s: seq<Dt>): map<int, int> {
+  map i, b | 0 <= i < |s| && s[i].B? && b in s[i].b && 1 != 2 :: b := b
+}
+
+method Main() {
+  var s := [A, B({0})];
+  print SetComprehension(s), "\n";
+  print MapComprehension(s), "\n";
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3320.dfy.expect

@@ -0,0 +1,2 @@
+{0}
+map[0 := 0]

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-3320.dfy.rs.check

@@ -0,0 +1 @@
+CHECK: error: expected identifier, found `<`

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy

@@ -0,0 +1,44 @@
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
+
+class C {
+  var data: nat
+  var next: C?
+
+  constructor (n: nat) {
+    data := n;
+    if n == 0 {
+      next := null;
+    } else {
+      next := new C(n - 1);
+    }
+  }
+
+  function FWithoutTailRecursion(n: nat, g: () ~> int): int
+    requires g.requires()
+    reads *
+  {
+    if n == 0 || next == null then
+      g()
+    else
+      var h := () reads this => this.data;
+      var r := next.FWithoutTailRecursion(n - 1, if n < 20 then g else h);
+      r
+  }
+
+  function F(n: nat, g: () ~> int): int
+    requires g.requires()
+    reads *
+  {
+    if n == 0 || next == null then
+      g()
+    else
+      var h := () reads this => this.data;
+      next.F(n - 1, if n < 20 then g else h)
+  }
+}
+
+method Main() {
+  var c := new C(25);
+  print c.FWithoutTailRecursion(25, () => -1), "\n"; // 20
+  print c.F(25, () => -1), "\n"; // 20
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.expect

@@ -0,0 +1,2 @@
+20
+20

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4684.dfy.rs.check

@@ -0,0 +1 @@
+CHECK: error

docs/dev/news/5402.fix

@@ -0,0 +1 @@
+Unguarded enumeration of bound variables in set and map comprehensions

docs/dev/news/5474.fix

@@ -0,0 +1 @@
+Reference the correct `this` after removing the tail call of a function or method