Opaque block

Source/DafnyCore/AST/Expressions/Applications/MemberSelectExpr.cs

@@ -15,25 +15,25 @@ public class MemberSelectExpr : Expression, IHasReferences, ICloneable<MemberSel
   /// PreTypeApplication_AtEnclosingClass is the list of type arguments used to instantiate the type that
   /// declares Member (which is some supertype of the receiver type).
   /// </summary>
-  [FilledInDuringResolution] public List<PreType> PreTypeApplication_AtEnclosingClass;
+  [FilledInDuringResolution] public List<PreType> PreTypeApplicationAtEnclosingClass;
 
   /// <summary>
   /// PreTypeApplication_JustMember is the list of type arguments used to instantiate the type parameters
   /// of Member.
   /// </summary>
-  [FilledInDuringResolution] public List<PreType> PreTypeApplication_JustMember;
+  [FilledInDuringResolution] public List<PreType> PreTypeApplicationJustMember;
 
   /// <summary>
   /// TypeApplication_AtEnclosingClass is the list of type arguments used to instantiate the type that
   /// declares Member (which is some supertype of the receiver type).
   /// </summary>
-  [FilledInDuringResolution] public List<Type> TypeApplication_AtEnclosingClass;
+  [FilledInDuringResolution] public List<Type> TypeApplicationAtEnclosingClass;
 
   /// <summary>
   /// TypeApplication_JustMember is the list of type arguments used to instantiate the type parameters
   /// of Member.
   /// </summary>
-  [FilledInDuringResolution] public List<Type> TypeApplication_JustMember;
+  [FilledInDuringResolution] public List<Type> TypeApplicationJustMember;
 
   /// <summary>
   /// Returns a mapping from formal type parameters to actual type arguments. For example, given
@@ -54,21 +54,21 @@ public Dictionary<TypeParameter, Type> TypeArgumentSubstitutionsAtMemberDeclarat
 
     // Add the mappings from the member's own type parameters
     if (Member is ICallable icallable) {
-      Contract.Assert(TypeApplication_JustMember.Count == icallable.TypeArgs.Count);
+      Contract.Assert(TypeApplicationJustMember.Count == icallable.TypeArgs.Count);
       for (var i = 0; i < icallable.TypeArgs.Count; i++) {
-        subst.Add(icallable.TypeArgs[i], TypeApplication_JustMember[i]);
+        subst.Add(icallable.TypeArgs[i], TypeApplicationJustMember[i]);
       }
     } else {
-      Contract.Assert(TypeApplication_JustMember.Count == 0);
+      Contract.Assert(TypeApplicationJustMember.Count == 0);
     }
 
     // Add the mappings from the enclosing class.
     TopLevelDecl cl = Member.EnclosingClass;
     // Expand the type down to its non-null type, if any
     if (cl != null) {
-      Contract.Assert(cl.TypeArgs.Count == TypeApplication_AtEnclosingClass.Count);
+      Contract.Assert(cl.TypeArgs.Count == TypeApplicationAtEnclosingClass.Count);
       for (var i = 0; i < cl.TypeArgs.Count; i++) {
-        subst.Add(cl.TypeArgs[i], TypeApplication_AtEnclosingClass[i]);
+        subst.Add(cl.TypeArgs[i], TypeApplicationAtEnclosingClass[i]);
       }
     }
 
@@ -94,21 +94,21 @@ public Dictionary<TypeParameter, PreType> PreTypeArgumentSubstitutionsAtMemberDe
 
     // Add the mappings from the member's own type parameters
     if (Member is ICallable icallable) {
-      Contract.Assert(PreTypeApplication_JustMember.Count == icallable.TypeArgs.Count);
+      Contract.Assert(PreTypeApplicationJustMember.Count == icallable.TypeArgs.Count);
       for (var i = 0; i < icallable.TypeArgs.Count; i++) {
-        subst.Add(icallable.TypeArgs[i], PreTypeApplication_JustMember[i]);
+        subst.Add(icallable.TypeArgs[i], PreTypeApplicationJustMember[i]);
       }
     } else {
-      Contract.Assert(PreTypeApplication_JustMember.Count == 0);
+      Contract.Assert(PreTypeApplicationJustMember.Count == 0);
     }
 
     // Add the mappings from the enclosing class.
     TopLevelDecl cl = Member.EnclosingClass;
     // Expand the type down to its non-null type, if any
     if (cl != null) {
-      Contract.Assert(cl.TypeArgs.Count == PreTypeApplication_AtEnclosingClass.Count);
+      Contract.Assert(cl.TypeArgs.Count == PreTypeApplicationAtEnclosingClass.Count);
       for (var i = 0; i < cl.TypeArgs.Count; i++) {
-        subst.Add(cl.TypeArgs[i], PreTypeApplication_AtEnclosingClass[i]);
+        subst.Add(cl.TypeArgs[i], PreTypeApplicationAtEnclosingClass[i]);
       }
     }
 
@@ -134,7 +134,7 @@ public Dictionary<TypeParameter, Type> TypeArgumentSubstitutionsWithParents() {
     Contract.Requires(WasResolved());
     Contract.Ensures(Contract.Result<Dictionary<TypeParameter, Type>>() != null);
 
-    return TypeArgumentSubstitutionsWithParentsAux(Obj.Type, Member, TypeApplication_JustMember);
+    return TypeArgumentSubstitutionsWithParentsAux(Obj.Type, Member, TypeApplicationJustMember);
   }
 
   public static Dictionary<TypeParameter, Type> TypeArgumentSubstitutionsWithParentsAux(Type receiverType, MemberDecl member, List<Type> typeApplicationMember) {
@@ -193,8 +193,8 @@ public static Dictionary<TypeParameter, Type> TypeArgumentSubstitutionsWithParen
   void ObjectInvariant() {
     Contract.Invariant(Obj != null);
     Contract.Invariant(MemberName != null);
-    Contract.Invariant((Member != null) == (TypeApplication_AtEnclosingClass != null));  // TypeApplication_* are set whenever Member is set
-    Contract.Invariant((Member != null) == (TypeApplication_JustMember != null));  // TypeApplication_* are set whenever Member is set
+    Contract.Invariant((Member != null) == (TypeApplicationAtEnclosingClass != null));  // TypeApplication_* are set whenever Member is set
+    Contract.Invariant((Member != null) == (TypeApplicationJustMember != null));  // TypeApplication_* are set whenever Member is set
   }
 
   public MemberSelectExpr Clone(Cloner cloner) {
@@ -209,8 +209,8 @@ public MemberSelectExpr(Cloner cloner, MemberSelectExpr original) : base(cloner,
       Member = cloner.CloneMember(original.Member, true);
       AtLabel = original.AtLabel;
       InCompiledContext = original.InCompiledContext;
-      TypeApplication_AtEnclosingClass = original.TypeApplication_AtEnclosingClass;
-      TypeApplication_JustMember = original.TypeApplication_JustMember;
+      TypeApplicationAtEnclosingClass = original.TypeApplicationAtEnclosingClass;
+      TypeApplicationJustMember = original.TypeApplicationJustMember;
     }
   }
 
@@ -236,16 +236,16 @@ public MemberSelectExpr(IToken tok, Expression obj, Field field)
     this.Member = field;  // resolve here
 
     var receiverType = obj.Type.NormalizeExpand();
-    this.TypeApplication_AtEnclosingClass = receiverType.TypeArgs;
-    this.TypeApplication_JustMember = new List<Type>();
+    this.TypeApplicationAtEnclosingClass = receiverType.TypeArgs;
+    this.TypeApplicationJustMember = new List<Type>();
 
     var typeMap = new Dictionary<TypeParameter, Type>();
     if (receiverType is UserDefinedType udt) {
       var cl = udt.ResolvedClass as TopLevelDeclWithMembers;
       Contract.Assert(cl != null);
-      Contract.Assert(cl.TypeArgs.Count == TypeApplication_AtEnclosingClass.Count);
+      Contract.Assert(cl.TypeArgs.Count == TypeApplicationAtEnclosingClass.Count);
       for (var i = 0; i < cl.TypeArgs.Count; i++) {
-        typeMap.Add(cl.TypeArgs[i], TypeApplication_AtEnclosingClass[i]);
+        typeMap.Add(cl.TypeArgs[i], TypeApplicationAtEnclosingClass[i]);
       }
       foreach (var entry in cl.ParentFormalTypeParametersToActuals) {
         var v = entry.Value.Subst(typeMap);
@@ -254,9 +254,9 @@ public MemberSelectExpr(IToken tok, Expression obj, Field field)
     } else if (field.EnclosingClass == null) {
       // leave typeMap as the empty substitution
     } else {
-      Contract.Assert(field.EnclosingClass.TypeArgs.Count == TypeApplication_AtEnclosingClass.Count);
+      Contract.Assert(field.EnclosingClass.TypeArgs.Count == TypeApplicationAtEnclosingClass.Count);
       for (var i = 0; i < field.EnclosingClass.TypeArgs.Count; i++) {
-        typeMap.Add(field.EnclosingClass.TypeArgs[i], TypeApplication_AtEnclosingClass[i]);
+        typeMap.Add(field.EnclosingClass.TypeArgs[i], TypeApplicationAtEnclosingClass[i]);
       }
     }
     this.Type = field.Type.Subst(typeMap);  // resolve here
@@ -289,7 +289,7 @@ public override IEnumerable<Expression> SubExpressions {
     get { yield return Obj; }
   }
 
-  public override IEnumerable<Type> ComponentTypes => Util.Concat(TypeApplication_AtEnclosingClass, TypeApplication_JustMember);
+  public override IEnumerable<Type> ComponentTypes => Util.Concat(TypeApplicationAtEnclosingClass, TypeApplicationJustMember);
 
   [FilledInDuringResolution] public List<Type> ResolvedOutparameterTypes;
 

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Linq;
 using System.Numerics;
 
 namespace Microsoft.Dafny;
@@ -49,7 +50,7 @@ public virtual IEnumerable<Expression> TerminalExpressions {
   public Type Type {
     get {
       Contract.Ensures(type != null || Contract.Result<Type>() == null);  // useful in conjunction with postcondition of constructor
-      return type == null ? null : type.Normalize();
+      return type?.Normalize();
     }
     set {
       Contract.Requires(!WasResolved());  // set it only once
@@ -127,6 +128,23 @@ public virtual IEnumerable<Expression> SubExpressions {
     get { yield break; }
   }
 
+  public IEnumerable<Expression> DescendantsAndSelf {
+    get {
+      Stack<Expression> todo = new();
+      List<Expression> result = new();
+      todo.Push(this);
+      while (todo.Any()) {
+        var current = todo.Pop();
+        result.Add(current);
+        foreach (var child in current.SubExpressions) {
+          todo.Push(child);
+        }
+      }
+
+      return result;
+    }
+  }
+
   /// <summary>
   /// Returns the list of types that appear in this expression proper (that is, not including types that
   /// may appear in subexpressions). Types occurring in substatements of the expression are not included.
@@ -136,9 +154,7 @@ public virtual IEnumerable<Type> ComponentTypes {
     get { yield break; }
   }
 
-  public virtual bool IsImplicit {
-    get { return false; }
-  }
+  public virtual bool IsImplicit => false;
 
   public static IEnumerable<Expression> Conjuncts(Expression expr) {
     Contract.Requires(expr != null);
@@ -769,7 +785,7 @@ public static Expression CreateFieldSelect(IToken tok, Expression receiver, Fiel
   /// Wrap the resolved MemberSelectExpr in the usual unresolved structure, in case the expression is cloned and re-resolved.
   /// </summary>
   public static Expression WrapResolvedMemberSelect(MemberSelectExpr memberSelectExpr) {
-    List<Type> optTypeArguments = memberSelectExpr.TypeApplication_JustMember.Count == 0 ? null : memberSelectExpr.TypeApplication_JustMember;
+    List<Type> optTypeArguments = memberSelectExpr.TypeApplicationJustMember.Count == 0 ? null : memberSelectExpr.TypeApplicationJustMember;
     return new ExprDotName(memberSelectExpr.tok, memberSelectExpr.Obj, memberSelectExpr.MemberName, optTypeArguments) {
       ResolvedExpression = memberSelectExpr,
       Type = memberSelectExpr.Type
@@ -908,4 +924,10 @@ public string AsStringLiteral() {
 
   public override IEnumerable<INode> Children => SubExpressions;
   public override IEnumerable<INode> PreResolveChildren => Children;
+
+  public static Expression CreateAssigned(IToken tok, IdentifierExpr inner) {
+    return new UnaryOpExpr(tok, UnaryOpExpr.Opcode.Assigned, inner) {
+      Type = Type.Bool
+    };
+  }
 }

Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs

@@ -114,14 +114,14 @@ public enum ResolvedOpcode {
   }
   private ResolvedOpcode _theResolvedOp = ResolvedOpcode.YetUndetermined;
   public ResolvedOpcode ResolvedOp {
-    set {
-      Contract.Assume(_theResolvedOp == ResolvedOpcode.YetUndetermined || _theResolvedOp == value);  // there's never a reason for resolution to change its mind, is there?
-      _theResolvedOp = value;
-    }
     get {
       Debug.Assert(_theResolvedOp != ResolvedOpcode.YetUndetermined);  // shouldn't read it until it has been properly initialized
       return _theResolvedOp;
     }
+    set {
+      Contract.Assume(_theResolvedOp == ResolvedOpcode.YetUndetermined || _theResolvedOp == value);  // there's never a reason for resolution to change its mind, is there?
+      _theResolvedOp = value;
+    }
   }
   public ResolvedOpcode ResolvedOp_PossiblyStillUndetermined {  // offer a way to return _theResolveOp -- for experts only!
     get { return _theResolvedOp; }

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

@@ -9,6 +9,11 @@ public class AssignStmt : Statement, ICloneable<AssignStmt> {
   public readonly AssignmentRhs Rhs;
   public override IEnumerable<INode> Children => new List<Node> { Lhs, Rhs }.Where(x => x != null);
   public override IEnumerable<INode> PreResolveChildren => Children;
+
+  public override IEnumerable<IdentifierExpr> GetAssignedLocals() {
+    return new[] { Lhs.Resolved }.OfType<IdentifierExpr>();
+  }
+
   [ContractInvariantMethod]
   void ObjectInvariant() {
     Contract.Invariant(Lhs != null);

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

@@ -22,6 +22,9 @@ public ConcreteUpdateStatement(RangeToken rangeToken, List<Expression> lhss, Att
 
   public override IEnumerable<INode> Children => Lhss;
   public override IEnumerable<INode> PreResolveChildren => Lhss;
+  public override IEnumerable<IdentifierExpr> GetAssignedLocals() {
+    return Lhss.Select(lhs => lhs.Resolved).OfType<IdentifierExpr>();
+  }
 
   public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     return formatter.SetIndentUpdateStmt(this, indentBefore, false);

Source/DafnyCore/AST/Statements/Methods/CallStmt.cs

@@ -19,6 +19,10 @@ void ObjectInvariant() {
   }
 
   public override IEnumerable<INode> Children => Lhs.Concat(new Node[] { MethodSelect, Bindings });
+  public override IEnumerable<IdentifierExpr> GetAssignedLocals() {
+    return Lhs.Select(lhs => lhs.Resolved).OfType<IdentifierExpr>();
+  }
+
   public readonly List<Expression> Lhs;
   public readonly MemberSelectExpr MethodSelect;
   private readonly IToken overrideToken;

Source/DafnyCore/AST/Statements/OpaqueBlock.cs

@@ -0,0 +1,53 @@
+using System.Collections.Generic;
+using System.Linq;
+
+namespace Microsoft.Dafny;
+
+public class OpaqueBlock : BlockStmt, ICanResolveNewAndOld {
+  public readonly List<AttributedExpression> Ensures;
+  public readonly Specification<FrameExpression> Modifies;
+
+  protected OpaqueBlock(Cloner cloner, OpaqueBlock original) : base(cloner, original) {
+    Ensures = original.Ensures.Select(cloner.CloneAttributedExpr).ToList();
+    Modifies = cloner.CloneSpecFrameExpr(original.Modifies);
+  }
+
+  public override IEnumerable<Expression> SpecificationSubExpressions {
+    get {
+      foreach (var e in Ensures) {
+        yield return e.E;
+      }
+      foreach (var e in Modifies.Expressions) {
+        yield return e.E;
+      }
+    }
+  }
+
+  public OpaqueBlock(RangeToken rangeToken, List<Statement> body,
+    List<AttributedExpression> ensures,
+    Specification<FrameExpression> modifies) : base(rangeToken, body) {
+    Ensures = ensures;
+    Modifies = modifies;
+  }
+
+  public override void GenResolve(INewOrOldResolver resolver, ResolutionContext resolutionContext) {
+
+    resolver.Scope.PushMarker();
+    foreach (Statement ss in Body) {
+      resolver.ResolveStatementWithLabels(ss, resolutionContext);
+    }
+    resolver.Scope.PopMarker();
+
+    resolver.ResolveAttributes(Modifies, resolutionContext);
+    foreach (var fe in Modifies.Expressions) {
+      resolver.ResolveFrameExpression(fe, FrameExpressionUse.Modifies, resolutionContext);
+    }
+
+    foreach (var ensure in Ensures) {
+      resolver.ResolveAttributes(ensure, resolutionContext);
+      resolver.ResolveExpression(ensure.E, resolutionContext);
+      resolver.ConstrainTypeExprBool(ensure.E, "Postcondition must be a boolean (got {0})");
+    }
+    base.GenResolve(resolver, resolutionContext);
+  }
+}

Source/DafnyCore/AST/Statements/Statement.cs

@@ -77,6 +77,23 @@ public virtual IEnumerable<Statement> SubStatements {
     get { yield break; }
   }
 
+  public IEnumerable<Statement> DescendantsAndSelf {
+    get {
+      Stack<Statement> todo = new();
+      List<Statement> result = new();
+      todo.Push(this);
+      while (todo.Any()) {
+        var current = todo.Pop();
+        result.Add(current);
+        foreach (var child in current.SubStatements) {
+          todo.Push(child);
+        }
+      }
+
+      return result;
+    }
+  }
+
   /// <summary>
   /// Returns the non-null substatements of the Statements, before resolution occurs
   /// </summary>
@@ -175,4 +192,6 @@ public override string ToString() {
   public override IEnumerable<INode> PreResolveChildren =>
     (Attributes != null ? new List<Node> { Attributes } : Enumerable.Empty<Node>()).Concat(
       PreResolveSubStatements).Concat(PreResolveSubExpressions);
+
+  public virtual IEnumerable<IdentifierExpr> GetAssignedLocals() => Enumerable.Empty<IdentifierExpr>();
 }

Source/DafnyCore/AST/Substituter.cs

@@ -118,15 +118,15 @@ public virtual Expression Substitute(Expression expr) {
       } else if (expr is MemberSelectExpr) {
         var mse = (MemberSelectExpr)expr;
         var newObj = Substitute(mse.Obj);
-        var newTypeApplicationAtEnclosingClass = SubstituteTypeList(mse.TypeApplication_AtEnclosingClass);
-        var newTypeApplicationJustMember = SubstituteTypeList(mse.TypeApplication_JustMember);
+        var newTypeApplicationAtEnclosingClass = SubstituteTypeList(mse.TypeApplicationAtEnclosingClass);
+        var newTypeApplicationJustMember = SubstituteTypeList(mse.TypeApplicationJustMember);
         if (newObj != mse.Obj ||
-            newTypeApplicationAtEnclosingClass != mse.TypeApplication_AtEnclosingClass ||
-            newTypeApplicationJustMember != mse.TypeApplication_JustMember) {
+            newTypeApplicationAtEnclosingClass != mse.TypeApplicationAtEnclosingClass ||
+            newTypeApplicationJustMember != mse.TypeApplicationJustMember) {
           var fseNew = new MemberSelectExpr(mse.tok, newObj, mse.MemberName) {
             Member = mse.Member,
-            TypeApplication_AtEnclosingClass = newTypeApplicationAtEnclosingClass,
-            TypeApplication_JustMember = newTypeApplicationJustMember,
+            TypeApplicationAtEnclosingClass = newTypeApplicationAtEnclosingClass,
+            TypeApplicationJustMember = newTypeApplicationJustMember,
             AtLabel = mse.AtLabel ?? oldHeapLabel
           };
           newExpr = fseNew;