Merge commit '86840e6b14386c1e88480854dd8ce64ad17cb2ff' into tb-exper…

…iment-trsplitexpr

* commit '86840e6b14386c1e88480854dd8ce64ad17cb2ff':
  Map eq range (#4567)
  Fix: Declarations with {:only} ensure that other declarations aren't displayed as verified in the gutter icons (#4433)
  Fix caching of export declarations (#4556)
  Do not return exceptions when doing hover in a program with parse errors (#4557)
  Proof dependency warnings (#4542)
  [Test Generation] Reduce memory footprint by reusing the same Boogie program for multiple test generation queries (#4530)
  Fix a variety of bugs in Rust backend based on ESDK testing (#4538)
  Checker for .Values and .Items on maps (#4551)
  feat: Allow more assumptions in library backend (#4545)
  feat: Attributes on reads clauses (#4554)
  Fix gutter icons fields (#4549)
  Report errors that occur in the project file, in the IDE as well (#4539)
  Switch to ubuntu-20.04 for the refman build (#4555)

.github/workflows/refman.yml

@@ -22,7 +22,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [ ubuntu-latest ]
+        os: [ ubuntu-20.04 ]
     steps:
     - name: OS
       run: echo ${{ runner.os }} ${{ matrix.os }}
@@ -40,6 +40,7 @@ jobs:
     - name: Install latex pandoc - Linux
       if: runner.os == 'Linux'
       run: |
+        sudo apt-get update
         sudo apt-get install texlive-full
         wget https://github.com/jgm/pandoc/releases/download/3.1.7/pandoc-3.1.7-1-amd64.deb
         sudo dpkg -i *.deb

Source/DafnyCore.Test/ClonerTest.cs

@@ -31,7 +31,7 @@ public void ClonerKeepsBodyStartTok() {
     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 List<FrameExpression>(), new Specification<FrameExpression>(new List<FrameExpression>(), null),
+      new Specification<FrameExpression>(), 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);
 

Source/DafnyCore/AST/AstVisitor.cs

@@ -145,7 +145,8 @@ public virtual void VisitFunction(Function function) {
 
       function.Req.ForEach(aexpr => VisitAttributedExpression(aexpr, context));
 
-      function.Reads.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));
+      VisitAttributes(function.Reads, function.EnclosingClass.EnclosingModuleDefinition);
+      function.Reads.Expressions.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));
 
       function.Ens.ForEach(aexpr => VisitAttributedExpression(aexpr, GetContext(function, true)));
 
@@ -173,7 +174,7 @@ public virtual void VisitMethod(Method method) {
 
       method.Req.ForEach(aexpr => VisitAttributedExpression(aexpr, context));
 
-      method.Reads.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));
+      method.Reads.Expressions.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));
 
       VisitAttributes(method.Mod, method.EnclosingClass.EnclosingModuleDefinition);
       method.Mod.Expressions.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));

Source/DafnyCore/AST/BottomUpVisitor.cs

@@ -56,7 +56,7 @@ public void Visit(NewtypeDecl ntd) {
   }
   public void Visit(Method method) {
     Visit(method.Req);
-    Visit(method.Reads);
+    Visit(method.Reads.Expressions);
     Visit(method.Mod.Expressions);
     Visit(method.Ens);
     Visit(method.Decreases.Expressions);
@@ -65,7 +65,7 @@ public void Visit(Method method) {
   }
   public void Visit(Function function) {
     Visit(function.Req);
-    Visit(function.Reads);
+    Visit(function.Reads.Expressions);
     Visit(function.Ens);
     Visit(function.Decreases.Expressions);
     if (function.Body != null) { Visit(function.Body); }

Source/DafnyCore/AST/Cloner.cs

@@ -515,7 +515,7 @@ public virtual Function CloneFunction(Function f, string newName = null) {
       var formals = f.Formals.ConvertAll(p => CloneFormal(p, false));
       var result = f.Result != null ? CloneFormal(f.Result, false) : null;
       var req = f.Req.ConvertAll(CloneAttributedExpr);
-      var reads = f.Reads.ConvertAll(CloneFrameExpr);
+      var reads = CloneSpecFrameExpr(f.Reads);
       var decreases = CloneSpecExpr(f.Decreases);
       var ens = f.Ens.ConvertAll(CloneAttributedExpr);
       Expression body = CloneExpr(f.Body);

Source/DafnyCore/AST/Expressions/Comprehensions/LambdaExpr.cs

@@ -8,9 +8,9 @@ public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr> {
 
   public Expression Body => Term;
 
-  public readonly List<FrameExpression> Reads;
+  public readonly Specification<FrameExpression> Reads;
 
-  public LambdaExpr(IToken tok, RangeToken rangeToken, List<BoundVar> bvars, Expression requires, List<FrameExpression> reads, Expression body)
+  public LambdaExpr(IToken tok, RangeToken rangeToken, List<BoundVar> bvars, Expression requires, Specification<FrameExpression> reads, Expression body)
     : base(tok, rangeToken, bvars, requires, body, null) {
     Contract.Requires(reads != null);
     Reads = reads;
@@ -22,14 +22,14 @@ public override IEnumerable<Expression> SubExpressions {
       if (Range != null) {
         yield return Range;
       }
-      foreach (var read in Reads) {
+      foreach (var read in Reads.Expressions) {
         yield return read.E;
       }
     }
   }
 
   public LambdaExpr(Cloner cloner, LambdaExpr original) : base(cloner, original) {
-    Reads = original.Reads.ConvertAll(cloner.CloneFrameExpr);
+    Reads = cloner.CloneSpecFrameExpr(original.Reads);
   }
 
   public LambdaExpr Clone(Cloner cloner) {

Source/DafnyCore/AST/Expressions/DefaultValueExpression.cs

@@ -73,6 +73,8 @@ public void FillIn(ModuleResolver resolver, Dictionary<DefaultValueExpression, W
     var s = new DefaultValueSubstituter(resolver, visited, this.receiver, this.substMap, typeMap);
     this.ResolvedExpression = s.Substitute(this.formal.DefaultValue);
     visited[this] = WorkProgress.Done;
+
+    this.ResolvedExpression.Type = this.Type;
   }
 
   class DefaultValueSubstituter : Substituter {

Source/DafnyCore/AST/Expressions/Specification.cs

@@ -12,6 +12,11 @@ private void ObjectInvariant() {
     Contract.Invariant(Expressions == null || cce.NonNullElements<T>(Expressions));
   }
 
+  public Specification() {
+    Expressions = new List<T>();
+    Attributes = null;
+  }
+
   public Specification(List<T> exprs, Attributes attrs) {
     Contract.Requires(exprs == null || cce.NonNullElements<T>(exprs));
     Expressions = exprs;

Source/DafnyCore/AST/Grammar/Printer.cs

@@ -629,10 +629,10 @@ void PrintIteratorSignature(IteratorDecl iter, int indent) {
       int ind = indent + IndentAmount;
       PrintSpec("requires", iter.Requires, ind);
       if (iter.Reads.Expressions != null) {
-        PrintFrameSpecLine("reads", iter.Reads.Expressions, ind, iter.Reads.HasAttributes() ? iter.Reads.Attributes : null);
+        PrintFrameSpecLine("reads", iter.Reads, ind);
       }
       if (iter.Modifies.Expressions != null) {
-        PrintFrameSpecLine("modifies", iter.Modifies.Expressions, ind, iter.Modifies.HasAttributes() ? iter.Modifies.Attributes : null);
+        PrintFrameSpecLine("modifies", iter.Modifies, ind);
       }
       PrintSpec("yield requires", iter.YieldRequires, ind);
       PrintSpec("yield ensures", iter.YieldEnsures, ind);
@@ -933,7 +933,7 @@ public void PrintFunction(Function f, int indent, bool printSignatureOnly) {
 
       int ind = indent + IndentAmount;
       PrintSpec("requires", f.Req, ind);
-      PrintFrameSpecLine("reads", f.Reads, ind, null);
+      PrintFrameSpecLine("reads", f.Reads, ind);
       PrintSpec("ensures", f.Ens, ind);
       PrintDecreasesSpec(f.Decreases, ind);
       wr.WriteLine();
@@ -1019,7 +1019,7 @@ public void PrintMethod(Method method, int indent, bool printSignatureOnly) {
       int ind = indent + IndentAmount;
       PrintSpec("requires", method.Req, ind);
       if (method.Mod.Expressions != null) {
-        PrintFrameSpecLine("modifies", method.Mod.Expressions, ind, method.Mod.HasAttributes() ? method.Mod.Attributes : null);
+        PrintFrameSpecLine("modifies", method.Mod, ind);
       }
       PrintSpec("ensures", method.Ens, ind);
       PrintDecreasesSpec(method.Decreases, ind);
@@ -1108,18 +1108,16 @@ internal void PrintDecreasesSpec(Specification<Expression> decs, int indent) {
       }
     }
 
-    internal void PrintFrameSpecLine(string kind, List<FrameExpression> ee, int indent, Attributes attrs) {
+    internal void PrintFrameSpecLine(string kind, Specification<FrameExpression> ee, int indent) {
       Contract.Requires(kind != null);
-      Contract.Requires(cce.NonNullElements(ee));
-      if (ee != null && ee.Count != 0) {
+      Contract.Requires(ee != null);
+      if (ee != null && ee.Expressions != null && ee.Expressions.Count != 0) {
         wr.WriteLine();
         Indent(indent);
         wr.Write("{0}", kind);
-        if (attrs != null) {
-          PrintAttributes(attrs);
-        }
+        PrintAttributes(ee.Attributes);
         wr.Write(" ");
-        PrintFrameExpressionList(ee);
+        PrintFrameExpressionList(ee.Expressions);
       }
     }
 
@@ -1353,7 +1351,7 @@ public void PrintStatement(Statement stmt, int indent) {
         PrintAttributes(s.Attributes);
         PrintSpec("invariant", s.Invariants, indent + IndentAmount);
         PrintDecreasesSpec(s.Decreases, indent + IndentAmount);
-        PrintFrameSpecLine("modifies", s.Mod.Expressions, indent + IndentAmount, s.Mod.Attributes);
+        PrintFrameSpecLine("modifies", s.Mod, indent + IndentAmount);
         bool hasSpecs = s.Invariants.Count != 0 || (s.Decreases.Expressions != null && s.Decreases.Expressions.Count != 0) || s.Mod.Expressions != null;
         if (s.UsesOptionalBraces) {
           if (hasSpecs) {
@@ -1767,7 +1765,7 @@ void PrintWhileStatement(int indent, WhileStmt s, bool omitGuard, bool omitBody)
 
       PrintSpec("invariant", s.Invariants, indent + IndentAmount);
       PrintDecreasesSpec(s.Decreases, indent + IndentAmount);
-      PrintFrameSpecLine("modifies", s.Mod.Expressions, indent + IndentAmount, s.Mod.Attributes);
+      PrintFrameSpecLine("modifies", s.Mod, indent + IndentAmount);
       if (omitBody) {
         wr.WriteLine();
         Indent(indent + IndentAmount);
@@ -1829,7 +1827,7 @@ void PrintForLoopStatement(int indent, ForLoopStmt s) {
       PrintSpec("invariant", s.Invariants, indent + IndentAmount);
       PrintDecreasesSpec(s.Decreases, indent + IndentAmount);
       if (s.Mod.Expressions != null) {
-        PrintFrameSpecLine("modifies", s.Mod.Expressions, indent + IndentAmount, s.Mod.HasAttributes() ? s.Mod.Attributes : null);
+        PrintFrameSpecLine("modifies", s.Mod, indent + IndentAmount);
       }
       if (s.Body != null) {
         if (s.Invariants.Count == 0 && s.Decreases.Expressions.Count == 0 && (s.Mod.Expressions == null || s.Mod.Expressions.Count == 0)) {
@@ -2775,7 +2773,8 @@ void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext,
           PrintExpression(e.Range, false);
         }
         var readsPrefix = " reads ";
-        foreach (var read in e.Reads) {
+        PrintAttributes(e.Reads.Attributes);
+        foreach (var read in e.Reads.Expressions) {
           wr.Write(readsPrefix);
           PrintExpression(read.E, false);
           readsPrefix = ", ";

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -155,10 +155,7 @@ private static void AddParseResultToProgram(DfyParseResult parseResult, Program
       modify(program.SystemModuleManager);
     }
 
-    foreach (var diagnostic in parseResult.ErrorReporter.AllMessages) {
-      program.Reporter.Message(diagnostic.Source, diagnostic.Level, diagnostic.ErrorId, diagnostic.Token,
-        diagnostic.Message);
-    }
+    parseResult.ErrorReporter.CopyDiagnostics(program.Reporter);
 
     foreach (var declToMove in fileModule.DefaultClasses.Concat(fileModule.SourceDecls)) {
       declToMove.EnclosingModuleDefinition = defaultModule;

Source/DafnyCore/AST/Members/Constructor.cs

@@ -38,7 +38,7 @@ public Constructor(RangeToken rangeToken, Name name,
     List<TypeParameter> typeArgs,
     List<Formal> ins,
     List<AttributedExpression> req,
-    List<FrameExpression> reads,
+    Specification<FrameExpression> reads,
     [Captured] Specification<FrameExpression> mod,
     List<AttributedExpression> ens,
     Specification<Expression> decreases,

Source/DafnyCore/AST/Members/ExtremeLemma.cs

@@ -23,7 +23,7 @@ public ExtremeLemma(RangeToken rangeToken, Name name,
     List<TypeParameter> typeArgs,
     List<Formal> ins, [Captured] List<Formal> outs,
     List<AttributedExpression> req,
-    List<FrameExpression> reads,
+    Specification<FrameExpression> reads,
     [Captured] Specification<FrameExpression> mod,
     List<AttributedExpression> ens,
     Specification<Expression> decreases,
@@ -53,7 +53,7 @@ public LeastLemma(RangeToken rangeToken, Name name,
     List<TypeParameter> typeArgs,
     List<Formal> ins, [Captured] List<Formal> outs,
     List<AttributedExpression> req,
-    List<FrameExpression> reads,
+    Specification<FrameExpression> reads,
     [Captured] Specification<FrameExpression> mod,
     List<AttributedExpression> ens,
     Specification<Expression> decreases,
@@ -83,7 +83,7 @@ public GreatestLemma(RangeToken rangeToken, Name name,
     List<TypeParameter> typeArgs,
     List<Formal> ins, [Captured] List<Formal> outs,
     List<AttributedExpression> req,
-    List<FrameExpression> reads,
+    Specification<FrameExpression> reads,
     [Captured] Specification<FrameExpression> mod,
     List<AttributedExpression> ens,
     Specification<Expression> decreases,

Source/DafnyCore/AST/Members/ExtremePredicate.cs

@@ -21,7 +21,7 @@ public bool KNat {
 
   public ExtremePredicate(RangeToken rangeToken, Name name, bool hasStaticKeyword, bool isOpaque, KType typeOfK,
     List<TypeParameter> typeArgs, List<Formal> formals, Formal result,
-    List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens,
+    List<AttributedExpression> req, Specification<FrameExpression> reads, List<AttributedExpression> ens,
     Expression body, Attributes attributes, IToken signatureEllipsis)
     : base(rangeToken, name, hasStaticKeyword, true, isOpaque, typeArgs, formals, result, Type.Bool,
       req, reads, ens, new Specification<Expression>(new List<Expression>(), null), body, null, null, attributes, signatureEllipsis) {
@@ -54,7 +54,7 @@ public class GreatestPredicate : ExtremePredicate {
   public override string WhatKind => "greatest predicate";
   public GreatestPredicate(RangeToken rangeToken, Name name, bool hasStaticKeyword, bool isOpaque, KType typeOfK,
     List<TypeParameter> typeArgs, List<Formal> formals, Formal result,
-    List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens,
+    List<AttributedExpression> req, Specification<FrameExpression> reads, List<AttributedExpression> ens,
     Expression body, Attributes attributes, IToken signatureEllipsis)
     : base(rangeToken, name, hasStaticKeyword, isOpaque, typeOfK, typeArgs, formals, result,
       req, reads, ens, body, attributes, signatureEllipsis) {
@@ -65,7 +65,7 @@ public class LeastPredicate : ExtremePredicate {
   public override string WhatKind => "least predicate";
   public LeastPredicate(RangeToken rangeToken, Name name, bool hasStaticKeyword, bool isOpaque, KType typeOfK,
     List<TypeParameter> typeArgs, List<Formal> formals, Formal result,
-    List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens,
+    List<AttributedExpression> req, Specification<FrameExpression> reads, List<AttributedExpression> ens,
     Expression body, Attributes attributes, IToken signatureEllipsis)
     : base(rangeToken, name, hasStaticKeyword, isOpaque, typeOfK, typeArgs, formals, result,
       req, reads, ens, body, attributes, signatureEllipsis) {

Source/DafnyCore/AST/Members/Function.cs

@@ -98,7 +98,7 @@ public TailStatus
   public PreType ResultPreType;
   public readonly Type ResultType;
   public readonly List<AttributedExpression> Req;
-  public readonly List<FrameExpression> Reads;
+  public readonly Specification<FrameExpression> Reads;
   public readonly List<AttributedExpression> Ens;
   public readonly Specification<Expression> Decreases;
   public Expression Body; // an extended expression; Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution
@@ -136,7 +136,7 @@ public enum TailStatus {
 
   public override IEnumerable<INode> Children => new[] { ByMethodBody }.Where(x => x != null).
     Concat<Node>(TypeArgs).
-    Concat<Node>(Reads).
+    Concat<Node>(Reads.Expressions).
     Concat<Node>(Req).
     Concat(Ens.Select(e => e.E)).
     Concat(Decreases.Expressions).
@@ -147,7 +147,7 @@ public enum TailStatus {
 
   public override IEnumerable<INode> PreResolveChildren =>
     TypeArgs.
-    Concat<Node>(Reads).
+    Concat<Node>(Reads.Expressions).
     Concat<Node>(Req).
     Concat(Ens).
     Concat(Decreases.Expressions.Where(expression => expression is not AutoGeneratedExpression)).
@@ -163,7 +163,7 @@ public override IEnumerable<Expression> SubExpressions {
       foreach (var e in Req) {
         yield return e.E;
       }
-      foreach (var e in Reads) {
+      foreach (var e in Reads.Expressions) {
         yield return e.E;
       }
       foreach (var e in Ens) {
@@ -212,14 +212,14 @@ void ObjectInvariant() {
     Contract.Invariant(cce.NonNullElements(Formals));
     Contract.Invariant(ResultType != null);
     Contract.Invariant(cce.NonNullElements(Req));
-    Contract.Invariant(cce.NonNullElements(Reads));
+    Contract.Invariant(Reads != null);
     Contract.Invariant(cce.NonNullElements(Ens));
     Contract.Invariant(Decreases != null);
   }
 
   public Function(RangeToken range, Name name, bool hasStaticKeyword, bool isGhost, bool isOpaque,
     List<TypeParameter> typeArgs, List<Formal> formals, Formal result, Type resultType,
-    List<AttributedExpression> req, List<FrameExpression> reads, List<AttributedExpression> ens, Specification<Expression> decreases,
+    List<AttributedExpression> req, Specification<FrameExpression> reads, List<AttributedExpression> ens, Specification<Expression> decreases,
     Expression/*?*/ body, IToken/*?*/ byMethodTok, BlockStmt/*?*/ byMethodBody,
     Attributes attributes, IToken/*?*/ signatureEllipsis)
     : base(range, name, hasStaticKeyword, isGhost, attributes, signatureEllipsis != null) {
@@ -230,7 +230,7 @@ public Function(RangeToken range, Name name, bool hasStaticKeyword, bool isGhost
     Contract.Requires(cce.NonNullElements(formals));
     Contract.Requires(resultType != null);
     Contract.Requires(cce.NonNullElements(req));
-    Contract.Requires(cce.NonNullElements(reads));
+    Contract.Requires(reads != null);
     Contract.Requires(cce.NonNullElements(ens));
     Contract.Requires(decreases != null);
     Contract.Requires(byMethodBody == null || (!isGhost && body != null)); // function-by-method has a ghost expr and non-ghost stmt, but to callers appears like a functiion-method
@@ -292,7 +292,7 @@ bool ICallable.InferredDecreases {
 
   [Pure]
   public bool IsFuelAware() { return IsRecursive || IsFueled || (OverriddenFunction != null && OverriddenFunction.IsFuelAware()); }
-  public virtual bool ReadsHeap { get { return Reads.Count != 0; } }
+  public virtual bool ReadsHeap { get { return Reads.Expressions.Count != 0; } }
 
   public static readonly Option<string> FunctionSyntaxOption = new("--function-syntax",
     () => "4",
@@ -343,7 +343,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
       formatter.SetAttributedExpressionIndentation(req, indentBefore + formatter.SpaceTab);
     }
 
-    foreach (var frame in Reads) {
+    foreach (var frame in Reads.Expressions) {
       formatter.SetFrameExpressionIndentation(frame, indentBefore + formatter.SpaceTab);
     }
 
@@ -399,7 +399,8 @@ public void Resolve(ModuleResolver resolver) {
       Contract.Assert(r.Type != null);  // follows from postcondition of ResolveExpression
       resolver.ConstrainTypeExprBool(r, "Precondition must be a boolean (got {0})");
     }
-    foreach (FrameExpression fr in Reads) {
+    resolver.ResolveAttributes(Reads, new ResolutionContext(this, this is TwoStateFunction));
+    foreach (FrameExpression fr in Reads.Expressions) {
       resolver.ResolveFrameExpressionTopLevel(fr, FrameExpressionUse.Reads, this);
     }
 

Source/DafnyCore/AST/Members/Lemma.cs

@@ -11,7 +11,7 @@ public Lemma(RangeToken rangeToken, Name name,
     [Captured] List<TypeParameter> typeArgs,
     [Captured] List<Formal> ins, [Captured] List<Formal> outs,
     [Captured] List<AttributedExpression> req,
-    [Captured] List<FrameExpression> reads,
+    [Captured] Specification<FrameExpression> reads,
     [Captured] Specification<FrameExpression> mod,
     [Captured] List<AttributedExpression> ens,
     [Captured] Specification<Expression> decreases,
@@ -35,7 +35,7 @@ public TwoStateLemma(RangeToken rangeToken, Name name,
     [Captured] List<TypeParameter> typeArgs,
     [Captured] List<Formal> ins, [Captured] List<Formal> outs,
     [Captured] List<AttributedExpression> req,
-    [Captured] List<FrameExpression> reads,
+    [Captured] Specification<FrameExpression> reads,
     [Captured] Specification<FrameExpression> mod,
     [Captured] List<AttributedExpression> ens,
     [Captured] Specification<Expression> decreases,