Update to Boogie 3.0.0 (dafny-lang#4209)

This adds a couple of Dafny-relevant things:
* A soundness fix for boogie-org/boogie#749. I thought this would resolve dafny-lang#4053, because it resolves a soundness issue discovered during the investigation of that issue, but it doesn't. Apparently there's _another_ soundness issue hiding in there.
* Support for coverage analysis: which program constructs annotated with
an `{:id ...}` attribute contributed to verification? Dafny currently
does not add `{:id ..}` attributes, but we plan to make it automatically
do so (optionally) in the near future. See boogie-org/boogie#730.
* Allow absolute paths to Boogie solver plugins.

By submitting this pull request, I confirm that my contribution
is made under the terms of the MIT license.

Source/DafnyCore/AST/AstVisitor.cs

@@ -26,7 +26,7 @@ public ASTVisitor() {
  /// statement and expression using "visitor".
  /// </summary>
  public void VisitDeclarations(List<TopLevelDecl> declarations) {
- declarations.Iter(VisitOneDeclaration);
+ declarations.ForEach(VisitOneDeclaration);
  }
 
  protected virtual void VisitOneDeclaration(TopLevelDecl decl) {
@@ -57,7 +57,7 @@ protected virtual void VisitOneDeclaration(TopLevelDecl decl) {
  }
 
  if (decl is TopLevelDeclWithMembers cl) {
- cl.Members.Iter(VisitMember);
+ cl.Members.ForEach(VisitMember);
  }
  }
 
@@ -68,21 +68,21 @@ private void VisitIterator(IteratorDecl iteratorDecl) {
 
  VisitDefaultParameterValues(iteratorDecl.Ins, context);
 
- iteratorDecl.Requires.Iter(aexpr => VisitAttributedExpression(aexpr, context));
+ iteratorDecl.Requires.ForEach(aexpr => VisitAttributedExpression(aexpr, context));
 
  VisitAttributes(iteratorDecl.Modifies, iteratorDecl.EnclosingModuleDefinition);
- iteratorDecl.Modifies.Expressions.Iter(frameExpr => VisitTopLevelFrameExpression(frameExpr, context));
+ iteratorDecl.Modifies.Expressions.ForEach(frameExpr => VisitTopLevelFrameExpression(frameExpr, context));
 
- iteratorDecl.YieldRequires.Iter(aexpr => VisitAttributedExpression(aexpr, context));
+ iteratorDecl.YieldRequires.ForEach(aexpr => VisitAttributedExpression(aexpr, context));
 
- iteratorDecl.Reads.Expressions.Iter(frameExpr => VisitTopLevelFrameExpression(frameExpr, context));
+ iteratorDecl.Reads.Expressions.ForEach(frameExpr => VisitTopLevelFrameExpression(frameExpr, context));
 
- iteratorDecl.YieldEnsures.Iter(aexpr => VisitExpression(aexpr.E, context));
+ iteratorDecl.YieldEnsures.ForEach(aexpr => VisitExpression(aexpr.E, context));
 
- iteratorDecl.Ensures.Iter(aexpr => VisitExpression(aexpr.E, context));
+ iteratorDecl.Ensures.ForEach(aexpr => VisitExpression(aexpr.E, context));
 
  VisitAttributes(iteratorDecl.Decreases, iteratorDecl.EnclosingModuleDefinition);
- iteratorDecl.Decreases.Expressions.Iter(expr => VisitExpression(expr, context));
+ iteratorDecl.Decreases.Expressions.ForEach(expr => VisitExpression(expr, context));
 
  if (iteratorDecl.Body != null) {
  VisitStatement(iteratorDecl.Body, context);
@@ -143,14 +143,14 @@ public virtual void VisitFunction(Function function) {
 
  VisitDefaultParameterValues(function.Formals, context);
 
- function.Req.Iter(aexpr => VisitAttributedExpression(aexpr, context));
+ function.Req.ForEach(aexpr => VisitAttributedExpression(aexpr, context));
 
- function.Reads.Iter(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));
+ function.Reads.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));
 
- function.Ens.Iter(aexpr => VisitAttributedExpression(aexpr, GetContext(function, true)));
+ function.Ens.ForEach(aexpr => VisitAttributedExpression(aexpr, GetContext(function, true)));
 
  VisitAttributes(function.Decreases, function.EnclosingClass.EnclosingModuleDefinition);
- function.Decreases.Expressions.Iter(expr => VisitExpression(expr, context));
+ function.Decreases.Expressions.ForEach(expr => VisitExpression(expr, context));
 
  if (function.Body != null) {
  VisitExpression(function.Body, context);
@@ -171,15 +171,15 @@ public virtual void VisitMethod(Method method) {
 
  VisitDefaultParameterValues(method.Ins, context);
 
- method.Req.Iter(aexpr => VisitAttributedExpression(aexpr, context));
+ method.Req.ForEach(aexpr => VisitAttributedExpression(aexpr, context));
 
  VisitAttributes(method.Mod, method.EnclosingClass.EnclosingModuleDefinition);
- method.Mod.Expressions.Iter(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));
+ method.Mod.Expressions.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));
 
  VisitAttributes(method.Decreases, method.EnclosingClass.EnclosingModuleDefinition);
- method.Decreases.Expressions.Iter(expr => VisitExpression(expr, context));
+ method.Decreases.Expressions.ForEach(expr => VisitExpression(expr, context));
 
- method.Ens.Iter(aexpr => VisitAttributedExpression(aexpr, context));
+ method.Ens.ForEach(aexpr => VisitAttributedExpression(aexpr, context));
 
  if (method.Body != null) {
  VisitStatement(method.Body, context);
@@ -189,7 +189,7 @@ public virtual void VisitMethod(Method method) {
  private void VisitDefaultParameterValues(List<Formal> formals, VisitorContext context) {
  formals
  .Where(formal => formal.DefaultValue != null)
- .Iter(formal => VisitExpression(formal.DefaultValue, context));
+ .ForEach(formal => VisitExpression(formal.DefaultValue, context));
  }
 
  private void VisitAttributedExpression(AttributedExpression attributedExpression, VisitorContext context) {
@@ -265,7 +265,7 @@ protected virtual void VisitExpression(Expression expr, VisitorContext context)
  }
 
  // Visit subexpressions
- expr.SubExpressions.Iter(ee => VisitExpression(ee, context));
+ expr.SubExpressions.ForEach(ee => VisitExpression(ee, context));
 
  PostVisitOneExpression(expr, context);
  }
@@ -366,10 +366,10 @@ protected virtual void VisitStatement(Statement stmt, VisitorContext context) {
  }
 
  // Visit subexpressions
- stmt.SubExpressions.Iter(ee => VisitExpression(ee, context));
+ stmt.SubExpressions.ForEach(ee => VisitExpression(ee, context));
 
  // Visit substatements
- stmt.SubStatements.Iter(ss => VisitStatement(ss, context));
+ stmt.SubStatements.ForEach(ss => VisitStatement(ss, context));
 
  PostVisitOneStatement(stmt, context);
  }

Source/DafnyCore/AST/DafnyAst.cs

@@ -859,10 +859,10 @@ public bool HasAttributes() {
 
  public class BottomUpVisitor {
  public void Visit(IEnumerable<Expression> exprs) {
- exprs.Iter(Visit);
+ exprs.ForEach(Visit);
  }
  public void Visit(IEnumerable<Statement> stmts) {
- stmts.Iter(Visit);
+ stmts.ForEach(Visit);
  }
  public void Visit(AttributedExpression expr) {
  Visit(expr.E);
@@ -871,10 +871,10 @@ public void Visit(FrameExpression expr) {
  Visit(expr.E);
  }
  public void Visit(IEnumerable<AttributedExpression> exprs) {
- exprs.Iter(Visit);
+ exprs.ForEach(Visit);
  }
  public void Visit(IEnumerable<FrameExpression> exprs) {
- exprs.Iter(Visit);
+ exprs.ForEach(Visit);
  }
  public void Visit(ICallable decl) {
  if (decl is Function f) {
@@ -927,7 +927,7 @@ public void Visit(Function function) {
  public void Visit(Expression expr) {
  Contract.Requires(expr != null);
  // recursively visit all subexpressions and all substatements
- expr.SubExpressions.Iter(Visit);
+ expr.SubExpressions.ForEach(Visit);
  if (expr is StmtExpr) {
  // a StmtExpr also has a substatement
  var e = (StmtExpr)expr;
@@ -938,8 +938,8 @@ public void Visit(Expression expr) {
  public void Visit(Statement stmt) {
  Contract.Requires(stmt != null);
  // recursively visit all subexpressions and all substatements
- stmt.SubExpressions.Iter(Visit);
- stmt.SubStatements.Iter(Visit);
+ stmt.SubExpressions.ForEach(Visit);
+ stmt.SubStatements.ForEach(Visit);
  VisitOneStmt(stmt);
  }
  protected virtual void VisitOneExpr(Expression expr) {
@@ -958,13 +958,13 @@ public void Visit(Expression expr, State st) {
  Contract.Requires(expr != null);
  if (VisitOneExpr(expr, ref st)) {
  if (preResolve && expr is ConcreteSyntaxExpression concreteSyntaxExpression) {
- concreteSyntaxExpression.PreResolveSubExpressions.Iter(e => Visit(e, st));
+ concreteSyntaxExpression.PreResolveSubExpressions.ForEach(e => Visit(e, st));
  } else if (preResolve && expr is QuantifierExpr quantifierExpr) {
  // pre-resolve, split expressions are not children
- quantifierExpr.PreResolveSubExpressions.Iter(e => Visit(e, st));
+ quantifierExpr.PreResolveSubExpressions.ForEach(e => Visit(e, st));
  } else {
  // recursively visit all subexpressions and all substatements
- expr.SubExpressions.Iter(e => Visit(e, st));
+ expr.SubExpressions.ForEach(e => Visit(e, st));
  }
  if (expr is StmtExpr) {
  // a StmtExpr also has a substatement
@@ -978,19 +978,19 @@ public void Visit(Statement stmt, State st) {
  if (VisitOneStmt(stmt, ref st)) {
  // recursively visit all subexpressions and all substatements
  if (preResolve) {
- stmt.PreResolveSubExpressions.Iter(e => Visit(e, st));
- stmt.PreResolveSubStatements.Iter(s => Visit(s, st));
+ stmt.PreResolveSubExpressions.ForEach(e => Visit(e, st));
+ stmt.PreResolveSubStatements.ForEach(s => Visit(s, st));
  } else {
- stmt.SubExpressions.Iter(e => Visit(e, st));
- stmt.SubStatements.Iter(s => Visit(s, st));
+ stmt.SubExpressions.ForEach(e => Visit(e, st));
+ stmt.SubStatements.ForEach(s => Visit(s, st));
  }
  }
  }
  public void Visit(IEnumerable<Expression> exprs, State st) {
- exprs.Iter(e => Visit(e, st));
+ exprs.ForEach(e => Visit(e, st));
  }
  public void Visit(IEnumerable<Statement> stmts, State st) {
- stmts.Iter(e => Visit(e, st));
+ stmts.ForEach(e => Visit(e, st));
  }
  public void Visit(AttributedExpression expr, State st) {
  Visit(expr.E, st);
@@ -999,10 +999,10 @@ public void Visit(FrameExpression expr, State st) {
  Visit(expr.E, st);
  }
  public void Visit(IEnumerable<AttributedExpression> exprs, State st) {
- exprs.Iter(e => Visit(e, st));
+ exprs.ForEach(e => Visit(e, st));
  }
  public void Visit(IEnumerable<FrameExpression> exprs, State st) {
- exprs.Iter(e => Visit(e, st));
+ exprs.ForEach(e => Visit(e, st));
  }
  public void Visit(ICallable decl, State st) {
  if (decl is Function) {

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -800,9 +800,9 @@ public static Expression CreateLet(IToken tok, List<CasePattern<BoundVar>> LHSs,
  var newLHSs = LHSs.ConvertAll(cloner.CloneCasePattern);
 
  var oldVars = new List<BoundVar>();
- LHSs.Iter(p => oldVars.AddRange(p.Vars));
+ LHSs.ForEach(p => oldVars.AddRange(p.Vars));
  var newVars = new List<BoundVar>();
- newLHSs.Iter(p => newVars.AddRange(p.Vars));
+ newLHSs.ForEach(p => newVars.AddRange(p.Vars));
  body = VarSubstituter(oldVars.ConvertAll<NonglobalVariable>(x => (NonglobalVariable)x), newVars, body);
 
  var let = new LetExpr(tok, newLHSs, RHSs, body, exact);

Source/DafnyCore/AST/Modules/ScopeCloner.cs

@@ -83,7 +83,7 @@ bool RemovePredicate(TopLevelDecl topLevelDecl) {
  basem.ResolvedPrefixNamedModules.RemoveAll(RemovePredicate);
 
  basem.TopLevelDecls.OfType<TopLevelDeclWithMembers>().
- Iter(t => t.Members.RemoveAll(IsInvisibleClone));
+ ForEach(t => t.Members.RemoveAll(IsInvisibleClone));
 
  return basem;
  }

Source/DafnyCore/Compilers/Python/Compiler-python.cs

@@ -105,7 +105,7 @@ private void EmitImports(string moduleName, ConcreteSyntaxTree wr) {
  wr.WriteLine("from math import floor");
  wr.WriteLine("from itertools import count");
  wr.WriteLine();
- Imports.Iter(module => wr.WriteLine($"import {module}"));
+ Imports.ForEach(module => wr.WriteLine($"import {module}"));
  if (moduleName != null) {
  wr.WriteLine();
  wr.WriteLine($"assert \"{moduleName}\" == __name__");

Source/DafnyCore/Dafny.atg

@@ -4673,11 +4673,11 @@ LetExprWithLHS<out Expression e, bool allowLemma, bool allowLambda, bool allowBi
  [ "ghost" (. isGhost = true; x = t; .)
  ]
  "var" (. if (!isGhost) { x = t; } .)
- CasePattern<out pat> (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
+ CasePattern<out pat> (. if (isGhost) { pat.Vars.ForEach(bv => bv.IsGhost = true); }
  letLHSs.Add(pat);
  lastLHS = la;
  .)
- { "," CasePattern<out pat> (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); }
+ { "," CasePattern<out pat> (. if (isGhost) { pat.Vars.ForEach(bv => bv.IsGhost = true); }
  letLHSs.Add(pat);
  .)
  }

Source/DafnyCore/DafnyCore.csproj

@@ -32,7 +32,7 @@
  <PackageReference Include="System.CommandLine" Version="2.0.0-beta4.22272.1" />
  <PackageReference Include="System.Runtime.Numerics" Version="4.3.0" />
  <PackageReference Include="System.Collections.Immutable" Version="1.7.0" />
- <PackageReference Include="Boogie.ExecutionEngine" Version="2.16.8" />
+ <PackageReference Include="Boogie.ExecutionEngine" Version="3.0.0" />
  <PackageReference Include="Tomlyn" Version="0.16.2" />
  </ItemGroup>
 

Source/DafnyCore/Generic/Node.cs

@@ -328,7 +328,7 @@ void UpdateStartEndTokRecursive(Node node) {
  }
  }
 
- PreResolveChildren.Iter(UpdateStartEndTokRecursive);
+ PreResolveChildren.ForEach(UpdateStartEndTokRecursive);
 
  if (FormatTokens != null) {
  foreach (var token in FormatTokens) {
@@ -360,4 +360,4 @@ protected RangeNode(Cloner cloner, RangeNode original) {
  protected RangeNode(RangeToken rangeToken) {
  RangeToken = rangeToken;
  }
-}
+}

Source/DafnyCore/Generic/Util.cs

@@ -162,7 +162,7 @@ public static List<A> Concat<A>(List<A> xs, List<A> ys) {
  }
 
  public static Dictionary<A, B> Dict<A, B>(IEnumerable<A> xs, IEnumerable<B> ys) {
- return Dict<A, B>(LinqExtender.Zip(xs, ys));
+ return Dict<A, B>(Enumerable.Zip(xs, ys).Select(x => new Tuple<A, B>(x.First, x.Second)));
  }
 
  public static Dictionary<A, B> Dict<A, B>(IEnumerable<Tuple<A, B>> xys) {
@@ -254,9 +254,9 @@ public static string RemoveEscaping(DafnyOptions options, string s, bool isVerba
  Contract.Requires(s != null);
  var sb = new StringBuilder();
  if (options.Get(CommonOptionBag.UnicodeCharacters)) {
- UnescapedCharacters(options, s, isVerbatimString).Iter(ch => sb.Append(new Rune(ch)));
+ UnescapedCharacters(options, s, isVerbatimString).ForEach(ch => sb.Append(new Rune(ch)));
  } else {
- UnescapedCharacters(options, s, isVerbatimString).Iter(ch => sb.Append((char)ch));
+ UnescapedCharacters(options, s, isVerbatimString).ForEach(ch => sb.Append((char)ch));
  }
  return sb.ToString();
  }

Source/DafnyCore/Resolver/Abstemious.cs

@@ -73,6 +73,6 @@ private void CheckDestructsAreAbstemiousCompliant(Expression expr) {
  CheckDestructsAreAbstemiousCompliant(e.E);
  return;
  }
- expr.SubExpressions.Iter(CheckDestructsAreAbstemiousCompliant);
+ expr.SubExpressions.ForEach(CheckDestructsAreAbstemiousCompliant);
  }
 }

Source/DafnyCore/Resolver/BoundsDiscovery.cs

@@ -170,7 +170,7 @@ public static Expression FrameArrowToObjectSet(Expression e) {
 
  protected override void VisitExpression(Expression expr, BoundsDiscoveryContext context) {
  if (expr is LambdaExpr lambdaExpr) {
- lambdaExpr.Reads.Iter(DesugarFunctionsInFrameClause);
+ lambdaExpr.Reads.ForEach(DesugarFunctionsInFrameClause);
 
  // Make the context more specific when visiting inside a lambda expression
  context = new BoundsDiscoveryContext(context, lambdaExpr);
@@ -481,7 +481,7 @@ private static void DiscoverBoundsFunctionCallExpr<VT>(FunctionCallExpr fce, VT
 
  var formals = fce.Function.Formals;
  Contract.Assert(formals.Count == fce.Args.Count);
- if (LinqExtender.Zip(formals, fce.Args).Any(t => t.Item1.IsOlder && t.Item2.Resolved is IdentifierExpr ide && ide.Var == (IVariable)boundVariable)) {
+ if (Enumerable.Zip(formals, fce.Args).Any(t => t.Item1.IsOlder && t.Item2.Resolved is IdentifierExpr ide && ide.Var == (IVariable)boundVariable)) {
  bounds.Add(new ComprehensionExpr.OlderBoundedPool());
  return;
  }

Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs

@@ -11,7 +11,7 @@ public CheckDividedConstructorInit_Visitor(ErrorReporter reporter)
  }
  public void CheckInit(List<Statement> initStmts) {
  Contract.Requires(initStmts != null);
- initStmts.Iter(CheckInit);
+ initStmts.ForEach(CheckInit);
  }
  /// <summary>
  /// This method almost does what Visit(Statement) does, except that it handles assignments to
@@ -31,25 +31,25 @@ void CheckInit(Statement stmt) {
  // Visit(s.Lhs); (++)
  // s.Rhs.SubExpressions.Iter(Visit); (+++)
  // Here, we may do less; in particular, we may omit (++).
- Attributes.SubExpressions(s.Attributes).Iter(VisitExpr); // (+)
+ Attributes.SubExpressions(s.Attributes).ForEach(VisitExpr); // (+)
  var mse = s.Lhs as MemberSelectExpr;
  if (mse != null && Expression.AsThis(mse.Obj) != null) {
  if (s.Rhs is ExprRhs) {
  // This is a special case we allow. Omit s.Lhs in the recursive visits. That is, we omit (++).
  // Furthermore, because the assignment goes to a field of "this" and won't be available until after
  // the "new;", we can allow certain specific (and useful) uses of "this" in the RHS.
- s.Rhs.SubExpressions.Iter(LiberalRHSVisit); // (+++)
+ s.Rhs.SubExpressions.ForEach(LiberalRHSVisit); // (+++)
  } else {
- s.Rhs.SubExpressions.Iter(VisitExpr); // (+++)
+ s.Rhs.SubExpressions.ForEach(VisitExpr); // (+++)
  }
  } else {
  VisitExpr(s.Lhs); // (++)
- s.Rhs.SubExpressions.Iter(VisitExpr); // (+++)
+ s.Rhs.SubExpressions.ForEach(VisitExpr); // (+++)
  }
  } else {
- stmt.SubExpressions.Iter(VisitExpr); // (*)
+ stmt.SubExpressions.ForEach(VisitExpr); // (*)
  }
- stmt.SubStatements.Iter(CheckInit); // (**)
+ stmt.SubStatements.ForEach(CheckInit); // (**)
  int dummy = 0;
  VisitOneStmt(stmt, ref dummy); // (***)
  }
@@ -99,7 +99,7 @@ void LiberalRHSVisit(Expression expr) {
  VisitExpr(expr);
  return;
  }
- expr.SubExpressions.Iter(LiberalRHSVisit);
+ expr.SubExpressions.ForEach(LiberalRHSVisit);
  }
  static bool IsThisDotField(MemberSelectExpr expr) {
  Contract.Requires(expr != null);