Merge branch 'master' into fix-4823-general-traits-bug-extends

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

@@ -3,7 +3,7 @@
 
 namespace Microsoft.Dafny;
 
-public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr> {
+public class LambdaExpr : ComprehensionExpr, ICloneable<LambdaExpr>, IFrameScope {
   public override string WhatKind => Reads.Expressions.Count != 0 ? "lambda" : Range != null ? "partial lambda" : "total lambda";
 
   public Expression Body => Term;
@@ -84,4 +84,6 @@ public override bool SetIndent(int indentBefore, TokenNewIndentCollector formatt
 
     return true;
   }
+
+  public string Designator => "lambda";
 }

Source/DafnyCore/AST/IHasUsages.cs

@@ -28,6 +28,10 @@ public interface ICanVerify : ISymbol {
   string FullDafnyName { get; }
 }
 
+public interface IFrameScope {
+  string Designator { get; } // "lambda expression", "method", "function"...
+}
+
 public static class AstExtensions {
 
   public static string GetMemberQualification(MemberDecl memberDecl) {

Source/DafnyCore/AST/Members/ConstantField.cs

@@ -65,4 +65,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
         AutoRevealFunctionDependencies.GenerateMessage(addedReveals.ToList()));
     }
   }
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/Members/Function.cs

@@ -564,4 +564,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
         AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth));
     }
   }
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/Members/ICodeContext.cs

@@ -50,7 +50,7 @@ public static ICodeContext Unwrap(ICodeContext codeContext) {
 /// <summary>
 /// An ICallable is a Function, Method, IteratorDecl, or (less fitting for the name ICallable) RedirectingTypeDecl or DatatypeDecl.
 /// </summary>
-public interface ICallable : ICodeContext, ISymbol {
+public interface ICallable : ICodeContext, ISymbol, IFrameScope {
   string WhatKind { get; }
   string NameRelativeToModule { get; }
   Specification<Expression> Decreases { get; }
@@ -98,6 +98,8 @@ public bool InferredDecreases {
   public string GetDescription(DafnyOptions options) {
     return CwInner.GetDescription(options);
   }
+
+  public string Designator => WhatKind;
 }
 
 
@@ -132,6 +134,7 @@ public IEnumerable<INode> GetConcreteChildren() {
   public string GetDescription(DafnyOptions options) {
     throw new cce.UnreachableException();
   }
+  public string Designator => WhatKind;
 }
 
 /// <summary>

Source/DafnyCore/AST/Members/Method.cs

@@ -472,4 +472,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
         AutoRevealFunctionDependencies.GenerateMessage(addedReveals, autoRevealDepth));
     }
   }
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/TypeDeclarations/DatatypeDecl.cs

@@ -196,4 +196,5 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
       }
     }
   }
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs

@@ -513,4 +513,5 @@ public override string GetTriviaContainingDocstring() {
   }
   public bool ShouldVerify => true; // This could be made more accurate
   public ModuleDefinition ContainingModule => EnclosingModuleDefinition;
+  public string Designator => WhatKind;
 }

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -166,6 +166,7 @@ public string GetTriviaContainingDocstring() {
 
   public ModuleDefinition ContainingModule => EnclosingModuleDefinition;
   public bool ShouldVerify => true; // This could be made more accurate
+  public string Designator => WhatKind;
 }
 
 public class NativeType {

Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs

@@ -125,4 +125,5 @@ public string GetTriviaContainingDocstring() {
 
   public abstract SymbolKind Kind { get; }
   public abstract string GetDescription(DafnyOptions options);
+  public string Designator => WhatKind;
 }

Source/DafnyCore/Verifier/BoogieGenerator.BoogieFactory.cs

@@ -39,7 +39,7 @@ internal Bpl.Expr BplBvLiteralExpr(Bpl.IToken tok, BaseTypes.BigNum n, int width
         // Bpl.LiteralExpr for a bitvector.
         var zero = new Bpl.LiteralExpr(tok, BaseTypes.BigNum.ZERO, width);
         var absN = new Bpl.LiteralExpr(tok, -n, width);
-        var etran = new ExpressionTranslator(this, predef, tok);
+        var etran = new ExpressionTranslator(this, predef, tok, null);
         return etran.TrToFunctionCall(tok, "sub_bv" + width, BplBvType(width), zero, absN, false);
       } else {
         return new Bpl.LiteralExpr(tok, n, width);

Source/DafnyCore/Verifier/BoogieGenerator.DefiniteAssignment.cs

@@ -202,7 +202,7 @@ void AssumeCanCallForByMethodDecl(Method method, BoogieStmtListBuilder builder)
         // fn == new FunctionCallExpr(tok, f.Name, receiver, tok, tok, f.Formals.ConvertAll(Expression.CreateIdentExpr));
         Bpl.IdentifierExpr canCallFuncID =
           new Bpl.IdentifierExpr(method.tok, method.FullSanitizedName + "#canCall", Bpl.Type.Bool);
-        var etran = new ExpressionTranslator(this, predef, method.tok);
+        var etran = new ExpressionTranslator(this, predef, method.tok, method);
         List<Bpl.Expr> args = arguments.Select(arg => etran.TrExpr(arg)).ToList();
         var formals = MkTyParamBinders(GetTypeParams(method), out var tyargs);
         if (method.FunctionFromWhichThisIsByMethodDecl.ReadsHeap) {

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -38,6 +38,7 @@ public Boogie.IdentifierExpr HeapCastToIdentifierExpr {
       public readonly string This;
       public readonly string readsFrame; // the name of the context's frame variable for reading state.
                                          // May be null to indicate the context's reads frame is * and doesn't require any reads checks.
+      public readonly IFrameScope scope; // lambda, function or predicate 
       public readonly string modifiesFrame; // the name of the context's frame variable for writing state.
       readonly Function applyLimited_CurrentFunction;
       internal readonly FuelSetting layerInterCluster;
@@ -64,7 +65,8 @@ void ObjectInvariant() {
       /// one ExpressionTranslator is constructed from another, unchanged parameters are just copied in.
       /// </summary>
       ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, string thisVar,
-        Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, string readsFrame, string modifiesFrame, bool stripLits) {
+        Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, IFrameScope scope,
+        string readsFrame, string modifiesFrame, bool stripLits) {
 
         Contract.Requires(boogieGenerator != null);
         Contract.Requires(predef != null);
@@ -84,6 +86,7 @@ void ObjectInvariant() {
           this.layerIntraCluster = layerIntraCluster;
         }
 
+        this.scope = scope;
         this.readsFrame = readsFrame;
         this.modifiesFrame = modifiesFrame;
         this.stripLits = stripLits;
@@ -94,48 +97,51 @@ public static Boogie.IdentifierExpr HeapIdentifierExpr(PredefinedDecls predef, B
         return new Boogie.IdentifierExpr(heapToken, predef.HeapVarName, predef.HeapType);
       }
 
-      public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.IToken heapToken)
-        : this(boogieGenerator, predef, HeapIdentifierExpr(predef, heapToken)) {
+      public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.IToken heapToken, IFrameScope scope)
+        : this(boogieGenerator, predef, HeapIdentifierExpr(predef, heapToken), scope) {
         Contract.Requires(boogieGenerator != null);
         Contract.Requires(predef != null);
         Contract.Requires(heapToken != null);
       }
 
-      public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap)
-        : this(boogieGenerator, predef, heap, "this") {
+      public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, IFrameScope scope)
+        : this(boogieGenerator, predef, heap, scope, "this") {
         Contract.Requires(boogieGenerator != null);
         Contract.Requires(predef != null);
       }
 
-      public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, Boogie.Expr oldHeap)
-        : this(boogieGenerator, predef, heap, "this") {
+      public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, Boogie.Expr oldHeap, IFrameScope scope)
+        : this(boogieGenerator, predef, heap, scope, "this") {
         Contract.Requires(boogieGenerator != null);
         Contract.Requires(predef != null);
         Contract.Requires(oldHeap != null);
 
-        var old = new ExpressionTranslator(boogieGenerator, predef, oldHeap);
+        var old = new ExpressionTranslator(boogieGenerator, predef, oldHeap, scope);
         old.oldEtran = old;
         this.oldEtran = old;
       }
 
-      public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, string thisVar)
-        : this(boogieGenerator, predef, heap, thisVar, null, new FuelSetting(boogieGenerator, 1), null, "$_ReadsFrame", "$_ModifiesFrame", false) {
+      public ExpressionTranslator(BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, IFrameScope scope, string thisVar)
+        : this(boogieGenerator, predef, heap, thisVar, null, new FuelSetting(boogieGenerator, 1), null, scope, "$_ReadsFrame", "$_ModifiesFrame", false) {
         Contract.Requires(boogieGenerator != null);
         Contract.Requires(predef != null);
         Contract.Requires(thisVar != null);
       }
 
       public ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap)
-        : this(etran.BoogieGenerator, etran.predef, heap, etran.This, etran.applyLimited_CurrentFunction, etran.layerInterCluster, etran.layerIntraCluster, etran.readsFrame, etran.modifiesFrame, etran.stripLits) {
+        : this(etran.BoogieGenerator, etran.predef, heap, etran.This, etran.applyLimited_CurrentFunction, etran.layerInterCluster, etran.layerIntraCluster, etran.scope, etran.readsFrame, etran.modifiesFrame, etran.stripLits) {
         Contract.Requires(etran != null);
       }
 
+      public ExpressionTranslator WithReadsFrame(string newReadsFrame, IFrameScope frameScope) {
+        return new ExpressionTranslator(BoogieGenerator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, frameScope, newReadsFrame, modifiesFrame, stripLits);
+      }
       public ExpressionTranslator WithReadsFrame(string newReadsFrame) {
-        return new ExpressionTranslator(BoogieGenerator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, newReadsFrame, modifiesFrame, stripLits);
+        return new ExpressionTranslator(BoogieGenerator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, scope, newReadsFrame, modifiesFrame, stripLits);
       }
 
       public ExpressionTranslator WithModifiesFrame(string newModifiesFrame) {
-        return new ExpressionTranslator(BoogieGenerator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, newModifiesFrame, stripLits);
+        return new ExpressionTranslator(BoogieGenerator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, scope, readsFrame, newModifiesFrame, stripLits);
       }
 
       internal IToken GetToken(Expression expression) {
@@ -148,7 +154,7 @@ public ExpressionTranslator Old {
           Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
 
           if (oldEtran == null) {
-            oldEtran = new ExpressionTranslator(BoogieGenerator, predef, new Boogie.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits);
+            oldEtran = new ExpressionTranslator(BoogieGenerator, predef, new Boogie.OldExpr(HeapExpr.tok, HeapExpr), This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, scope, readsFrame, modifiesFrame, stripLits);
             oldEtran.oldEtran = oldEtran;
           }
           return oldEtran;
@@ -161,7 +167,7 @@ public ExpressionTranslator OldAt(Label/*?*/ label) {
           return Old;
         }
         var heapAt = new Boogie.IdentifierExpr(Token.NoToken, "$Heap_at_" + label.AssignUniqueId(BoogieGenerator.CurrentIdGenerator), predef.HeapType);
-        return new ExpressionTranslator(BoogieGenerator, predef, heapAt, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits);
+        return new ExpressionTranslator(BoogieGenerator, predef, heapAt, This, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, scope, readsFrame, modifiesFrame, stripLits);
       }
 
       public bool UsesOldHeap {
@@ -224,9 +230,9 @@ public ExpressionTranslator DecreaseFuel(int offset) {
       private static ExpressionTranslator CloneExpressionTranslator(ExpressionTranslator orig,
         BoogieGenerator boogieGenerator, PredefinedDecls predef, Boogie.Expr heap, string thisVar,
         Function applyLimited_CurrentFunction, FuelSetting layerInterCluster, FuelSetting layerIntraCluster, string readsFrame, string modifiesFrame, bool stripLits) {
-        var et = new ExpressionTranslator(boogieGenerator, predef, heap, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits);
+        var et = new ExpressionTranslator(boogieGenerator, predef, heap, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, orig.scope, readsFrame, modifiesFrame, stripLits);
         if (orig.oldEtran != null) {
-          var etOld = new ExpressionTranslator(boogieGenerator, predef, orig.Old.HeapExpr, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, readsFrame, modifiesFrame, stripLits);
+          var etOld = new ExpressionTranslator(boogieGenerator, predef, orig.Old.HeapExpr, thisVar, applyLimited_CurrentFunction, layerInterCluster, layerIntraCluster, orig.scope, readsFrame, modifiesFrame, stripLits);
           etOld.oldEtran = etOld;
           et.oldEtran = etOld;
         }