From 0069a9d4dc1da52ea71fd47a7e4299013d52ec63 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 17 Jul 2023 18:07:54 -0700 Subject: [PATCH 1/6] Further reduce resource use of AppendOptimized --- .../DafnyRuntimeDafny/src/dafnyRuntime.dfy | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy index bab3320ce21..ba6a30699fd 100644 --- a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy @@ -212,7 +212,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { var storage: NativeArray var size: size_t - ghost predicate Valid() + opaque ghost predicate Valid() reads this, Repr decreases Repr, 1 ensures Valid() ==> this in Repr @@ -270,6 +270,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { requires size as int + 1 < SIZE_T_LIMIT modifies Repr ensures ValidAndDisjoint() + ensures Valid() ensures Value() == old(Value()) + [t] { EnsureCapacity(size + ONE_SIZE); @@ -310,6 +311,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { requires 0 < size modifies Repr ensures ValidAndDisjoint() + ensures Valid() ensures old(Value()) == Value() + [t] ensures Value() == old(Value()[..(size - 1)]) ensures t in old(Value()) @@ -324,6 +326,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { requires size as int + other.Length() as int < SIZE_T_LIMIT modifies Repr ensures ValidAndDisjoint() + ensures Valid() ensures Value() == old(Value()) + other.values { var newSize := size + other.Length(); @@ -766,11 +769,13 @@ abstract module {:options "/functionSyntax:4"} Dafny { expect SizeAdditionInRange(stack.size, ONE_SIZE); stack.AddLast(concat.right); label L1: + assert builder.Valid() by { reveal builder.Valid(); reveal ConcatValueOnStack(); } AppendOptimized(builder, concat.left, stack); assert builder.Value() == old@L1(builder.Value()) + concat.left.Value() + ConcatValueOnStack(old@L1(stack.Value())); } else if e is LazySequence { var lazy := e as LazySequence; var boxed := lazy.box.Get(); + assert builder.Valid() by { reveal builder.Valid(); reveal ConcatValueOnStack(); } AppendOptimized(builder, boxed, stack); assert builder.Value() == old(builder.Value()) + boxed.Value() + ConcatValueOnStack(old(stack.Value())); } else if e is ArraySequence { @@ -779,6 +784,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { if 0 < stack.size { var next: Sequence := stack.RemoveLast(); label L2: + assert builder.Valid() by { reveal builder.Valid(); reveal ConcatValueOnStack(); } AppendOptimized(builder, next, stack); assert builder.Value() == old@L2(builder.Value()) + next.Value() + ConcatValueOnStack(old@L2(stack.Value())); } @@ -787,12 +793,19 @@ abstract module {:options "/functionSyntax:4"} Dafny { // but Dafny doesn't support tail recursion optimization of mutually-recursive functions. // Alternatively we could use a datatype, which would be a significant rewrite. expect false, "Unsupported Sequence implementation"; - assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value())); + assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value())) by { + reveal builder.Valid(); + reveal ConcatValueOnStack(); + } + } + assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value())) by { + reveal builder.Valid(); + reveal ConcatValueOnStack(); } assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value())); } - ghost function ConcatValueOnStack(s: seq>): seq + opaque ghost function ConcatValueOnStack(s: seq>): seq requires (forall e <- s :: e.Valid()) { if |s| == 0 then From 01419b9f99346f2b120d0e599ac833a013ce40d0 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 17 Jul 2023 21:11:51 -0700 Subject: [PATCH 2/6] Revert "Further reduce resource use of AppendOptimized" This reverts commit 7f65b4561a8b92f26a1a20da0caf2d14a1402c84. --- .../DafnyRuntimeDafny/src/dafnyRuntime.dfy | 24 ++++--------------- 1 file changed, 4 insertions(+), 20 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy index ba6a30699fd..5f00e9b532f 100644 --- a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy @@ -212,7 +212,7 @@ abstract module {:options "/functionSyntax:4"} Dafny { var storage: NativeArray var size: size_t - opaque ghost predicate Valid() + ghost predicate Valid() reads this, Repr decreases Repr, 1 ensures Valid() ==> this in Repr @@ -270,7 +270,6 @@ abstract module {:options "/functionSyntax:4"} Dafny { requires size as int + 1 < SIZE_T_LIMIT modifies Repr ensures ValidAndDisjoint() - ensures Valid() ensures Value() == old(Value()) + [t] { EnsureCapacity(size + ONE_SIZE); @@ -311,7 +310,6 @@ abstract module {:options "/functionSyntax:4"} Dafny { requires 0 < size modifies Repr ensures ValidAndDisjoint() - ensures Valid() ensures old(Value()) == Value() + [t] ensures Value() == old(Value()[..(size - 1)]) ensures t in old(Value()) @@ -326,7 +324,6 @@ abstract module {:options "/functionSyntax:4"} Dafny { requires size as int + other.Length() as int < SIZE_T_LIMIT modifies Repr ensures ValidAndDisjoint() - ensures Valid() ensures Value() == old(Value()) + other.values { var newSize := size + other.Length(); @@ -768,14 +765,11 @@ abstract module {:options "/functionSyntax:4"} Dafny { // Length() if we add the invariant that no leaf nodes are empty. expect SizeAdditionInRange(stack.size, ONE_SIZE); stack.AddLast(concat.right); - label L1: - assert builder.Valid() by { reveal builder.Valid(); reveal ConcatValueOnStack(); } AppendOptimized(builder, concat.left, stack); - assert builder.Value() == old@L1(builder.Value()) + concat.left.Value() + ConcatValueOnStack(old@L1(stack.Value())); + assert builder.Value() == old(builder.Value()) + concat.left.Value() + ConcatValueOnStack(old(stack.Value())); } else if e is LazySequence { var lazy := e as LazySequence; var boxed := lazy.box.Get(); - assert builder.Valid() by { reveal builder.Valid(); reveal ConcatValueOnStack(); } AppendOptimized(builder, boxed, stack); assert builder.Value() == old(builder.Value()) + boxed.Value() + ConcatValueOnStack(old(stack.Value())); } else if e is ArraySequence { @@ -783,29 +777,19 @@ abstract module {:options "/functionSyntax:4"} Dafny { builder.Append(a.values); if 0 < stack.size { var next: Sequence := stack.RemoveLast(); - label L2: - assert builder.Valid() by { reveal builder.Valid(); reveal ConcatValueOnStack(); } AppendOptimized(builder, next, stack); - assert builder.Value() == old@L2(builder.Value()) + next.Value() + ConcatValueOnStack(old@L2(stack.Value())); + assert builder.Value() == old(builder.Value()) + next.Value() + ConcatValueOnStack(old(stack.Value())); } } else { // I'd prefer to just call Sequence.ToArray(), // but Dafny doesn't support tail recursion optimization of mutually-recursive functions. // Alternatively we could use a datatype, which would be a significant rewrite. expect false, "Unsupported Sequence implementation"; - assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value())) by { - reveal builder.Valid(); - reveal ConcatValueOnStack(); - } - } - assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value())) by { - reveal builder.Valid(); - reveal ConcatValueOnStack(); } assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value())); } - opaque ghost function ConcatValueOnStack(s: seq>): seq + ghost function ConcatValueOnStack(s: seq>): seq requires (forall e <- s :: e.Valid()) { if |s| == 0 then From 88ec45d601e7b25f158cb11e6756d19d920d1c17 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Mon, 17 Jul 2023 21:19:23 -0700 Subject: [PATCH 3/6] Use correct old locations --- Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy index 5f00e9b532f..bab3320ce21 100644 --- a/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy +++ b/Source/DafnyRuntime/DafnyRuntimeDafny/src/dafnyRuntime.dfy @@ -765,8 +765,9 @@ abstract module {:options "/functionSyntax:4"} Dafny { // Length() if we add the invariant that no leaf nodes are empty. expect SizeAdditionInRange(stack.size, ONE_SIZE); stack.AddLast(concat.right); + label L1: AppendOptimized(builder, concat.left, stack); - assert builder.Value() == old(builder.Value()) + concat.left.Value() + ConcatValueOnStack(old(stack.Value())); + assert builder.Value() == old@L1(builder.Value()) + concat.left.Value() + ConcatValueOnStack(old@L1(stack.Value())); } else if e is LazySequence { var lazy := e as LazySequence; var boxed := lazy.box.Get(); @@ -777,14 +778,16 @@ abstract module {:options "/functionSyntax:4"} Dafny { builder.Append(a.values); if 0 < stack.size { var next: Sequence := stack.RemoveLast(); + label L2: AppendOptimized(builder, next, stack); - assert builder.Value() == old(builder.Value()) + next.Value() + ConcatValueOnStack(old(stack.Value())); + assert builder.Value() == old@L2(builder.Value()) + next.Value() + ConcatValueOnStack(old@L2(stack.Value())); } } else { // I'd prefer to just call Sequence.ToArray(), // but Dafny doesn't support tail recursion optimization of mutually-recursive functions. // Alternatively we could use a datatype, which would be a significant rewrite. expect false, "Unsupported Sequence implementation"; + assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value())); } assert builder.Value() == old(builder.Value()) + e.Value() + ConcatValueOnStack(old(stack.Value())); } From 93c04f75741f582d7b0806daf3c9a618c98590e1 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Wed, 21 Jun 2023 10:11:15 -0700 Subject: [PATCH 4/6] Update to Boogie 2.16.9 --- Source/DafnyCore/AST/AstVisitor.cs | 42 +++++++++---------- Source/DafnyCore/AST/DafnyAst.cs | 36 ++++++++-------- .../DafnyCore/AST/Expressions/Expression.cs | 4 +- Source/DafnyCore/AST/Modules/ScopeCloner.cs | 2 +- .../Compilers/Python/Compiler-python.cs | 2 +- Source/DafnyCore/Dafny.atg | 4 +- Source/DafnyCore/DafnyCore.csproj | 2 +- Source/DafnyCore/Generic/Node.cs | 4 +- Source/DafnyCore/Generic/Util.cs | 6 +-- Source/DafnyCore/Resolver/Abstemious.cs | 2 +- Source/DafnyCore/Resolver/BoundsDiscovery.cs | 4 +- .../CheckDividedConstructorInit_Visitor.cs | 16 +++---- .../Resolver/FindFriendlyCalls_Visitor.cs | 4 +- .../Resolver/GhostInterestVisitor.cs | 30 ++++++------- Source/DafnyCore/Resolver/ModuleResolver.cs | 12 +++--- .../CheckTypeInferenceVisitor.cs | 18 ++++---- .../NameResolutionAndTypeInference.cs | 2 +- .../PreType/UnderspecificationDetector.cs | 38 ++++++++--------- Source/DafnyCore/Resolver/TailRecursion.cs | 6 +-- .../DafnyCore/Rewriters/PrecedenceLinter.cs | 10 ++--- .../Rewriters/PrintEffectEnforcement.cs | 8 ++-- .../Triggers/QuantifiersCollection.cs | 4 +- .../DafnyCore/Triggers/TriggersCollector.cs | 2 +- .../Verifier/Translator.ClassMembers.cs | 6 +-- .../Translator.ExpressionWellformed.cs | 2 +- .../Verifier/Translator.TrStatement.cs | 8 ++-- Source/DafnyCore/Verifier/Translator.cs | 24 +++++------ Source/DafnyServer/Utilities.cs | 3 +- Source/DafnyTestGeneration/ProgramModifier.cs | 18 ++++---- Source/DafnyTestGeneration/Utils.cs | 2 +- customBoogie.patch | 2 +- 31 files changed, 163 insertions(+), 160 deletions(-) diff --git a/Source/DafnyCore/AST/AstVisitor.cs b/Source/DafnyCore/AST/AstVisitor.cs index 618fa9e73dc..9f5ea2ef5f9 100644 --- a/Source/DafnyCore/AST/AstVisitor.cs +++ b/Source/DafnyCore/AST/AstVisitor.cs @@ -26,7 +26,7 @@ public ASTVisitor() { /// statement and expression using "visitor". /// public void VisitDeclarations(List 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 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); } diff --git a/Source/DafnyCore/AST/DafnyAst.cs b/Source/DafnyCore/AST/DafnyAst.cs index 5f4e6305cb3..505a1b61c47 100644 --- a/Source/DafnyCore/AST/DafnyAst.cs +++ b/Source/DafnyCore/AST/DafnyAst.cs @@ -859,10 +859,10 @@ public bool HasAttributes() { public class BottomUpVisitor { public void Visit(IEnumerable exprs) { - exprs.Iter(Visit); + exprs.ForEach(Visit); } public void Visit(IEnumerable 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 exprs) { - exprs.Iter(Visit); + exprs.ForEach(Visit); } public void Visit(IEnumerable 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 exprs, State st) { - exprs.Iter(e => Visit(e, st)); + exprs.ForEach(e => Visit(e, st)); } public void Visit(IEnumerable 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 exprs, State st) { - exprs.Iter(e => Visit(e, st)); + exprs.ForEach(e => Visit(e, st)); } public void Visit(IEnumerable 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) { diff --git a/Source/DafnyCore/AST/Expressions/Expression.cs b/Source/DafnyCore/AST/Expressions/Expression.cs index 38aaefd5f56..d4604bae40a 100644 --- a/Source/DafnyCore/AST/Expressions/Expression.cs +++ b/Source/DafnyCore/AST/Expressions/Expression.cs @@ -800,9 +800,9 @@ public static Expression CreateLet(IToken tok, List> LHSs, var newLHSs = LHSs.ConvertAll(cloner.CloneCasePattern); var oldVars = new List(); - LHSs.Iter(p => oldVars.AddRange(p.Vars)); + LHSs.ForEach(p => oldVars.AddRange(p.Vars)); var newVars = new List(); - newLHSs.Iter(p => newVars.AddRange(p.Vars)); + newLHSs.ForEach(p => newVars.AddRange(p.Vars)); body = VarSubstituter(oldVars.ConvertAll(x => (NonglobalVariable)x), newVars, body); var let = new LetExpr(tok, newLHSs, RHSs, body, exact); diff --git a/Source/DafnyCore/AST/Modules/ScopeCloner.cs b/Source/DafnyCore/AST/Modules/ScopeCloner.cs index dda314bb834..8d459db5384 100644 --- a/Source/DafnyCore/AST/Modules/ScopeCloner.cs +++ b/Source/DafnyCore/AST/Modules/ScopeCloner.cs @@ -83,7 +83,7 @@ bool RemovePredicate(TopLevelDecl topLevelDecl) { basem.ResolvedPrefixNamedModules.RemoveAll(RemovePredicate); basem.TopLevelDecls.OfType(). - Iter(t => t.Members.RemoveAll(IsInvisibleClone)); + ForEach(t => t.Members.RemoveAll(IsInvisibleClone)); return basem; } diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs index 5ce2bbab50a..83b1ad0a5d8 100644 --- a/Source/DafnyCore/Compilers/Python/Compiler-python.cs +++ b/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__"); diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index 8ab92f95e9c..f791cbe2ee7 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -4673,11 +4673,11 @@ LetExprWithLHS (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); } + CasePattern (. if (isGhost) { pat.Vars.ForEach(bv => bv.IsGhost = true); } letLHSs.Add(pat); lastLHS = la; .) - { "," CasePattern (. if (isGhost) { pat.Vars.Iter(bv => bv.IsGhost = true); } + { "," CasePattern (. if (isGhost) { pat.Vars.ForEach(bv => bv.IsGhost = true); } letLHSs.Add(pat); .) } diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index fda4ae3b3a2..6ca50785589 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -32,7 +32,7 @@ - + diff --git a/Source/DafnyCore/Generic/Node.cs b/Source/DafnyCore/Generic/Node.cs index 2b1ad69ac3d..accdfdbdf7b 100644 --- a/Source/DafnyCore/Generic/Node.cs +++ b/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; } -} \ No newline at end of file +} diff --git a/Source/DafnyCore/Generic/Util.cs b/Source/DafnyCore/Generic/Util.cs index a4d0645c9fc..48efdac45c4 100644 --- a/Source/DafnyCore/Generic/Util.cs +++ b/Source/DafnyCore/Generic/Util.cs @@ -162,7 +162,7 @@ public static List Concat(List xs, List ys) { } public static Dictionary Dict(IEnumerable xs, IEnumerable ys) { - return Dict(LinqExtender.Zip(xs, ys)); + return Dict(Enumerable.Zip(xs, ys).Select(x => new Tuple(x.First, x.Second))); } public static Dictionary Dict(IEnumerable> 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(); } diff --git a/Source/DafnyCore/Resolver/Abstemious.cs b/Source/DafnyCore/Resolver/Abstemious.cs index 8362414e559..26bdf2a12d0 100644 --- a/Source/DafnyCore/Resolver/Abstemious.cs +++ b/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); } } \ No newline at end of file diff --git a/Source/DafnyCore/Resolver/BoundsDiscovery.cs b/Source/DafnyCore/Resolver/BoundsDiscovery.cs index ab2d00ec415..ffee04d0e13 100644 --- a/Source/DafnyCore/Resolver/BoundsDiscovery.cs +++ b/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(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; } diff --git a/Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs b/Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs index 64af2fa8b63..3c88cafc9bb 100644 --- a/Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs +++ b/Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs @@ -11,7 +11,7 @@ public CheckDividedConstructorInit_Visitor(ErrorReporter reporter) } public void CheckInit(List initStmts) { Contract.Requires(initStmts != null); - initStmts.Iter(CheckInit); + initStmts.ForEach(CheckInit); } /// /// 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); diff --git a/Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs b/Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs index 8e6eff8341d..27c58cc44f0 100644 --- a/Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs +++ b/Source/DafnyCore/Resolver/FindFriendlyCalls_Visitor.cs @@ -57,13 +57,13 @@ protected override bool VisitOneExpr(Expression expr, ref CallingPosition cp) { var e = (NestedMatchExpr)expr; Visit(e.Source, CallingPosition.Neither); var theCp = cp; - e.Cases.Iter(kase => Visit((Expression)kase.Body, theCp)); + e.Cases.ForEach(kase => Visit((Expression)kase.Body, theCp)); return false; } else if (expr is MatchExpr) { var e = (MatchExpr)expr; Visit(e.Source, CallingPosition.Neither); var theCp = cp; - e.Cases.Iter(kase => Visit(kase.Body, theCp)); + e.Cases.ForEach(kase => Visit(kase.Body, theCp)); return false; } else if (expr is ITEExpr) { var e = (ITEExpr)expr; diff --git a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs index 3bb36a5033c..b21503d47b0 100644 --- a/Source/DafnyCore/Resolver/GhostInterestVisitor.cs +++ b/Source/DafnyCore/Resolver/GhostInterestVisitor.cs @@ -99,12 +99,12 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC if (mustBeErasable) { Error(ErrorId.r_print_statement_is_not_ghost, stmt, "print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)"); } else { - s.Args.Iter(ee => ExpressionTester.CheckIsCompilable(resolver, reporter, ee, codeContext)); + s.Args.ForEach(ee => ExpressionTester.CheckIsCompilable(resolver, reporter, ee, codeContext)); } } else if (stmt is RevealStmt) { var s = (RevealStmt)stmt; - s.ResolvedStatements.Iter(ss => Visit(ss, true, "a reveal statement")); + s.ResolvedStatements.ForEach(ss => Visit(ss, true, "a reveal statement")); s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost); } else if (stmt is BreakStmt) { @@ -146,12 +146,12 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC } else if (stmt is UpdateStmt) { var s = (UpdateStmt)stmt; - s.ResolvedStatements.Iter(ss => Visit(ss, mustBeErasable, proofContext)); + s.ResolvedStatements.ForEach(ss => Visit(ss, mustBeErasable, proofContext)); s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost); } else if (stmt is AssignOrReturnStmt) { var s = (AssignOrReturnStmt)stmt; - s.ResolvedStatements.Iter(ss => Visit(ss, mustBeErasable, proofContext)); + s.ResolvedStatements.ForEach(ss => Visit(ss, mustBeErasable, proofContext)); s.IsGhost = s.ResolvedStatements.All(ss => ss.IsGhost); } else if (stmt is VarDeclStmt) { @@ -268,10 +268,10 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC s.IsGhost = mustBeErasable; // set .IsGhost before descending into substatements (since substatements may do a 'break' out of this block) if (s is DividedBlockStmt ds) { var giv = new GhostInterestVisitor(this.codeContext, this.resolver, this.reporter, true, allowAssumptionVariables); - ds.BodyInit.Iter(ss => giv.Visit(ss, mustBeErasable, proofContext)); - ds.BodyProper.Iter(ss => Visit(ss, mustBeErasable, proofContext)); + ds.BodyInit.ForEach(ss => giv.Visit(ss, mustBeErasable, proofContext)); + ds.BodyProper.ForEach(ss => Visit(ss, mustBeErasable, proofContext)); } else { - s.Body.Iter(ss => Visit(ss, mustBeErasable, proofContext)); + s.Body.ForEach(ss => Visit(ss, mustBeErasable, proofContext)); } s.IsGhost = s.IsGhost || s.Body.All(ss => ss.IsGhost); // mark the block statement as ghost if all its substatements are ghost @@ -299,7 +299,7 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC if (!mustBeErasable && s.IsGhost) { reporter.Info(MessageSource.Resolver, s.Tok, "ghost if"); } - s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost, proofContext))); + s.Alternatives.ForEach(alt => alt.Body.ForEach(ss => Visit(ss, s.IsGhost, proofContext))); s.IsGhost = s.IsGhost || s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost)); if (!s.IsGhost) { // If there were features in the guards that are treated differently in ghost and non-ghost @@ -323,7 +323,7 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC Error(ErrorId.r_decreases_forbidden_on_ghost_loops, s, "'decreases *' is not allowed on ghost loops"); } if (s.IsGhost && s.Mod.Expressions != null) { - s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); + s.Mod.Expressions.ForEach(resolver.DisallowNonGhostFieldSpecifiers); } if (s.Body != null) { Visit(s.Body, s.IsGhost, proofContext); @@ -351,9 +351,9 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC Error(ErrorId.r_decreases_forbidden_on_ghost_loops, s, "'decreases *' is not allowed on ghost loops"); } if (s.IsGhost && s.Mod.Expressions != null) { - s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); + s.Mod.Expressions.ForEach(resolver.DisallowNonGhostFieldSpecifiers); } - s.Alternatives.Iter(alt => alt.Body.Iter(ss => Visit(ss, s.IsGhost, proofContext))); + s.Alternatives.ForEach(alt => alt.Body.ForEach(ss => Visit(ss, s.IsGhost, proofContext))); s.IsGhost = s.IsGhost || (!s.Decreases.Expressions.Exists(e => e is WildcardExpr) && s.Alternatives.All(alt => alt.Body.All(ss => ss.IsGhost))); if (!s.IsGhost) { // If there were features in the guards that are treated differently in ghost and non-ghost @@ -381,7 +381,7 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC } } if (s.IsGhost && s.Mod.Expressions != null) { - s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); + s.Mod.Expressions.ForEach(resolver.DisallowNonGhostFieldSpecifiers); } if (s.Body != null) { Visit(s.Body, s.IsGhost, proofContext); @@ -430,7 +430,7 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC s.IsGhost = mustBeErasable; if (s.IsGhost) { - s.Mod.Expressions.Iter(resolver.DisallowNonGhostFieldSpecifiers); + s.Mod.Expressions.ForEach(resolver.DisallowNonGhostFieldSpecifiers); } if (s.Body != null) { Visit(s.Body, mustBeErasable, proofContext); @@ -452,7 +452,7 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC if (!mustBeErasable && nestedMatchStmt.IsGhost) { reporter.Info(MessageSource.Resolver, nestedMatchStmt.Tok, "ghost match"); } - nestedMatchStmt.Cases.Iter(kase => kase.Body.Iter(ss => Visit(ss, nestedMatchStmt.IsGhost, proofContext))); + nestedMatchStmt.Cases.ForEach(kase => kase.Body.ForEach(ss => Visit(ss, nestedMatchStmt.IsGhost, proofContext))); nestedMatchStmt.IsGhost = nestedMatchStmt.IsGhost || nestedMatchStmt.Cases.All(kase => kase.Body.All(ss => ss.IsGhost)); if (!nestedMatchStmt.IsGhost) { // If there were features in the source expression that are treated differently in ghost and non-ghost @@ -465,7 +465,7 @@ public void Visit(Statement stmt, bool mustBeErasable, [CanBeNull] string proofC if (!mustBeErasable && s.IsGhost) { reporter.Info(MessageSource.Resolver, s.Tok, "ghost match"); } - s.Cases.Iter(kase => kase.Body.Iter(ss => Visit(ss, s.IsGhost, proofContext))); + s.Cases.ForEach(kase => kase.Body.ForEach(ss => Visit(ss, s.IsGhost, proofContext))); s.IsGhost = s.IsGhost || s.Cases.All(kase => kase.Body.All(ss => ss.IsGhost)); if (!s.IsGhost) { // If there were features in the source expression that are treated differently in ghost and non-ghost diff --git a/Source/DafnyCore/Resolver/ModuleResolver.cs b/Source/DafnyCore/Resolver/ModuleResolver.cs index 3d79bfabafe..757b3e98bcb 100644 --- a/Source/DafnyCore/Resolver/ModuleResolver.cs +++ b/Source/DafnyCore/Resolver/ModuleResolver.cs @@ -414,7 +414,7 @@ public void ResolveModuleExport(LiteralModuleDecl literalDecl, ModuleSignature s } // final pass to propagate visibility of exported imports - var sigs = sortedExportDecls.Select(d => d.Signature).Concat1(sig); + var sigs = sortedExportDecls.Select(d => d.Signature).Append(sig); foreach (var s in sigs) { foreach (var decl in s.TopLevels) { @@ -1144,7 +1144,7 @@ public void ResolveTopLevelDecls_Core(List declarations, foreach (TopLevelDecl d in declarations) { if (d is IteratorDecl) { var iter = (IteratorDecl)d; - iter.SubExpressions.Iter(e => CheckExpression(e, this, iter)); + iter.SubExpressions.ForEach(e => CheckExpression(e, this, iter)); if (iter.Body != null) { ComputeGhostInterest(iter.Body, false, null, iter); CheckExpression(iter.Body, this, iter); @@ -1312,7 +1312,7 @@ public void ResolveTopLevelDecls_Core(List declarations, // Note that this check can only be done after determining which expressions are ghosts. foreach (var d in declarations) { for (var attr = d.Attributes; attr != null; attr = attr.Prev) { - attr.Args.Iter(e => CheckTypeCharacteristics_Expr(e, true)); + attr.Args.ForEach(e => CheckTypeCharacteristics_Expr(e, true)); } if (d is IteratorDecl) { @@ -1487,7 +1487,7 @@ public void ResolveTopLevelDecls_Core(List declarations, } else if (d is DatatypeDecl) { var dd = (DatatypeDecl)d; foreach (var ctor in dd.Ctors) { - ctor.Formals.Iter(formal => CheckVariance(formal.Type, dd, TypeParameter.TPVariance.Co, false)); + ctor.Formals.ForEach(formal => CheckVariance(formal.Type, dd, TypeParameter.TPVariance.Co, false)); } } @@ -1932,7 +1932,7 @@ private void ResolveClassMembers_Pass1(TopLevelDeclWithMembers cl) { } if (prevErrCnt == reporter.Count(ErrorLevel.Error) && member is ICodeContext) { - member.SubExpressions.Iter(e => CheckExpression(e, this, (ICodeContext)member)); + member.SubExpressions.ForEach(e => CheckExpression(e, this, (ICodeContext)member)); } } } @@ -3859,7 +3859,7 @@ public void CheckLocalityUpdates(Statement stmt, ISet localsAllow } } else if (stmt is VarDeclStmt) { var s = (VarDeclStmt)stmt; - s.Locals.Iter(local => localsAllowedInUpdates.Add(local)); + s.Locals.ForEach(local => localsAllowedInUpdates.Add(local)); } else if (stmt is ModifyStmt) { // no further complaints (note, ghost interests have already checked for 'modify' statements) } else if (stmt is BlockStmt) { diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs index 0900d20faf3..0ff8f8a163d 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/CheckTypeInferenceVisitor.cs @@ -66,10 +66,10 @@ protected override bool VisitOneStatement(Statement stmt, TypeInferenceCheckingC // The resolution of the calc statement builds up .Steps and .Result, which are of the form E0 OP E1, where // E0 and E1 are expressions from .Lines. These additional expressions still need to have their .ResolvedOp // fields filled in, so we visit them, rather than just the parsed .Lines. - Attributes.SubExpressions(calcStmt.Attributes).Iter(e => VisitExpression(e, context)); - calcStmt.Steps.Iter(e => VisitExpression(e, context)); + Attributes.SubExpressions(calcStmt.Attributes).ForEach(e => VisitExpression(e, context)); + calcStmt.Steps.ForEach(e => VisitExpression(e, context)); VisitExpression(calcStmt.Result, context); - calcStmt.Hints.Iter(hint => VisitStatement(hint, context)); + calcStmt.Hints.ForEach(hint => VisitStatement(hint, context)); return false; // we're done with all subcomponents of the CalcStmt } @@ -85,13 +85,13 @@ protected override void PostVisitOneStatement(Statement stmt, TypeInferenceCheck } } else if (stmt is VarDeclPattern) { var s = (VarDeclPattern)stmt; - s.LocalVars.Iter(local => CheckTypeIsDetermined(local.Tok, local.Type, "local variable")); - s.LocalVars.Iter(local => CheckTypeArgsContainNoOrdinal(local.Tok, local.Type, context)); + s.LocalVars.ForEach(local => CheckTypeIsDetermined(local.Tok, local.Type, "local variable")); + s.LocalVars.ForEach(local => CheckTypeArgsContainNoOrdinal(local.Tok, local.Type, context)); } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; - s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); - s.BoundVars.Iter(bv => CheckTypeArgsContainNoOrdinal(bv.tok, bv.Type, context)); + s.BoundVars.ForEach(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable")); + s.BoundVars.ForEach(bv => CheckTypeArgsContainNoOrdinal(bv.tok, bv.Type, context)); } else if (stmt is AssignSuchThatStmt) { var s = (AssignSuchThatStmt)stmt; @@ -398,7 +398,7 @@ public void CheckTypeArgsContainNoOrdinal(IToken tok, Type t, TypeInferenceCheck // need to do them here again for the prefix predicates/lemmas. } else { t = t.NormalizeExpand(); - t.TypeArgs.Iter(rg => CheckContainsNoOrdinal(ResolutionErrors.ErrorId.r_no_ORDINAL_as_type_parameter, tok, rg, "an ORDINAL type is not allowed to be used as a type argument")); + t.TypeArgs.ForEach(rg => CheckContainsNoOrdinal(ResolutionErrors.ErrorId.r_no_ORDINAL_as_type_parameter, tok, rg, "an ORDINAL type is not allowed to be used as a type argument")); } } @@ -410,6 +410,6 @@ public void CheckContainsNoOrdinal(ResolutionErrors.ErrorId errorId, IToken tok, if (t.IsBigOrdinalType) { resolver.ReportError(errorId, tok, errMsg); } - t.TypeArgs.Iter(rg => CheckContainsNoOrdinal(errorId, tok, rg, errMsg)); + t.TypeArgs.ForEach(rg => CheckContainsNoOrdinal(errorId, tok, rg, errMsg)); } } \ No newline at end of file diff --git a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs index 5650da0182d..01e0ea91ca5 100644 --- a/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs +++ b/Source/DafnyCore/Resolver/NameResolutionAndTypeInference/NameResolutionAndTypeInference.cs @@ -3502,7 +3502,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext } else if (stmt is PrintStmt) { var s = (PrintStmt)stmt; - s.Args.Iter(e => ResolveExpression(e, resolutionContext)); + s.Args.ForEach(e => ResolveExpression(e, resolutionContext)); } else if (stmt is RevealStmt) { var s = (RevealStmt)stmt; diff --git a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs index f33e162a1ef..feae6a236a9 100644 --- a/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs +++ b/Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs @@ -38,9 +38,9 @@ public void Check(List declarations) { if (d is IteratorDecl) { var iter = (IteratorDecl)d; var prevErrCnt = ErrorCount; - iter.Members.Iter(CheckMember); + iter.Members.ForEach(CheckMember); if (prevErrCnt == ErrorCount) { - iter.SubExpressions.Iter(e => CheckExpression(e, iter)); + iter.SubExpressions.ForEach(e => CheckExpression(e, iter)); } CheckParameterDefaultValues(iter.Ins, iter); if (iter.Body != null) { @@ -120,7 +120,7 @@ private void CheckMembers(TopLevelDeclWithMembers cl) { } } if (prevErrCnt == ErrorCount && member is ICodeContext) { - member.SubExpressions.Iter(e => CheckExpression(e, (ICodeContext)member)); + member.SubExpressions.ForEach(e => CheckExpression(e, (ICodeContext)member)); } } } @@ -135,9 +135,9 @@ private void CheckMember(MemberDecl member) { } else if (member is Method method) { CheckParameterDefaultValues(method.Ins, method); - method.Req.Iter(mfe => CheckAttributedExpression(mfe, method)); + method.Req.ForEach(mfe => CheckAttributedExpression(mfe, method)); CheckSpecFrameExpression(method.Mod, method); - method.Ens.Iter(mfe => CheckAttributedExpression(mfe, method)); + method.Ens.ForEach(mfe => CheckAttributedExpression(mfe, method)); CheckSpecExpression(method.Decreases, method); if (method.Body != null) { CheckStatement(method.Body, method); @@ -147,9 +147,9 @@ private void CheckMember(MemberDecl member) { var f = (Function)member; CheckParameterDefaultValues(f.Formals, f); var errorCount = ErrorCount; - f.Req.Iter(e => CheckExpression(e.E, f)); - f.Ens.Iter(e => CheckExpression(e.E, f)); - f.Reads.Iter(fe => CheckExpression(fe.E, f)); + f.Req.ForEach(e => CheckExpression(e.E, f)); + f.Ens.ForEach(e => CheckExpression(e.E, f)); + f.Reads.ForEach(fe => CheckExpression(fe.E, f)); CheckSpecExpression(f.Decreases, f); if (f.Body != null) { CheckExpression(f.Body, f); @@ -182,17 +182,17 @@ private void CheckExpression(Expression expr, ICodeContext codeContext) { } private void CheckSpecExpression(Specification spec, ICodeContext codeContext) { - Attributes.SubExpressions(spec.Attributes).Iter(e => CheckExpression(e, codeContext)); - spec.Expressions.Iter(e => CheckExpression(e, codeContext)); + Attributes.SubExpressions(spec.Attributes).ForEach(e => CheckExpression(e, codeContext)); + spec.Expressions.ForEach(e => CheckExpression(e, codeContext)); } private void CheckSpecFrameExpression(Specification spec, ICodeContext codeContext) { - Attributes.SubExpressions(spec.Attributes).Iter(e => CheckExpression(e, codeContext)); - spec.Expressions.Iter(fe => CheckExpression(fe.E, codeContext)); + Attributes.SubExpressions(spec.Attributes).ForEach(e => CheckExpression(e, codeContext)); + spec.Expressions.ForEach(fe => CheckExpression(fe.E, codeContext)); } private void CheckAttributedExpression(AttributedExpression ae, ICodeContext codeContext) { - Attributes.SubExpressions(ae.Attributes).Iter(e => CheckExpression(e, codeContext)); + Attributes.SubExpressions(ae.Attributes).ForEach(e => CheckExpression(e, codeContext)); CheckExpression(ae.E, codeContext); } @@ -225,13 +225,13 @@ protected override void VisitOneStmt(Statement stmt) { } } else if (stmt is VarDeclPattern) { var s = (VarDeclPattern)stmt; - s.LocalVars.Iter(local => CheckPreTypeIsDetermined(local.Tok, local.PreType, "local variable")); - s.LocalVars.Iter(local => CheckTypeArgsContainNoOrdinal(local.Tok, local.PreType)); + s.LocalVars.ForEach(local => CheckPreTypeIsDetermined(local.Tok, local.PreType, "local variable")); + s.LocalVars.ForEach(local => CheckTypeArgsContainNoOrdinal(local.Tok, local.PreType)); } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; - s.BoundVars.Iter(bv => CheckPreTypeIsDetermined(bv.tok, bv.PreType, "bound variable")); - s.BoundVars.Iter(bv => CheckTypeArgsContainNoOrdinal(bv.tok, bv.PreType)); + s.BoundVars.ForEach(bv => CheckPreTypeIsDetermined(bv.tok, bv.PreType, "bound variable")); + s.BoundVars.ForEach(bv => CheckTypeArgsContainNoOrdinal(bv.tok, bv.PreType)); } else if (stmt is AssignSuchThatStmt) { var s = (AssignSuchThatStmt)stmt; @@ -570,7 +570,7 @@ public void CheckTypeArgsContainNoOrdinal(IToken tok, PreType preType) { Contract.Requires(tok != null); Contract.Requires(preType != null); if (preType.Normalize() is DPreType dp) { - dp.Arguments.Iter(tt => CheckContainsNoOrdinal(tok, tt, "an ORDINAL type is not allowed to be used as a type argument")); + dp.Arguments.ForEach(tt => CheckContainsNoOrdinal(tok, tt, "an ORDINAL type is not allowed to be used as a type argument")); } } @@ -582,7 +582,7 @@ public void CheckContainsNoOrdinal(IToken tok, PreType preType, string errMsg) { if (PreTypeResolver.AncestorName(dp) == "ORDINAL") { cus.ReportError(tok, errMsg); } - dp.Arguments.Iter(tt => CheckContainsNoOrdinal(tok, tt, errMsg)); + dp.Arguments.ForEach(tt => CheckContainsNoOrdinal(tok, tt, errMsg)); } } } diff --git a/Source/DafnyCore/Resolver/TailRecursion.cs b/Source/DafnyCore/Resolver/TailRecursion.cs index f7d3d46908c..8bcda781d25 100644 --- a/Source/DafnyCore/Resolver/TailRecursion.cs +++ b/Source/DafnyCore/Resolver/TailRecursion.cs @@ -120,7 +120,7 @@ TailRecursionStatus CheckTailRecursive(Statement stmt, Method enclosingMethod, r var status = ConfirmTailCall(s.Tok, enclosingMethod, fce.TypeApplication_JustFunction, new List() { s.Lhs }, reportErrors); if (status == TailRecursionStatus.TailCallSpent) { tailCall = s; - fce.Args.Iter(ee => DisallowRecursiveCallsInExpressions(ee, enclosingMethod)); + fce.Args.ForEach(ee => DisallowRecursiveCallsInExpressions(ee, enclosingMethod)); } else { DisallowRecursiveCallsInExpressions(s.Lhs, enclosingMethod, reportErrors); DisallowRecursiveCallsInExpressions(eRhs.Expr, enclosingMethod, reportErrors); @@ -284,7 +284,7 @@ void DisallowRecursiveCallsInExpressions(Statement stmt, Method enclosingMethod, Contract.Requires(enclosingMethod != null); if (enclosingMethod.IsByMethod && reportErrors) { - stmt.SubExpressions.Iter(e => DisallowRecursiveCallsInExpressions(e, enclosingMethod)); + stmt.SubExpressions.ForEach(e => DisallowRecursiveCallsInExpressions(e, enclosingMethod)); } } @@ -303,7 +303,7 @@ void DisallowRecursiveCallsInExpressions(Expression expr, Method enclosingMethod if (expr is FunctionCallExpr fce && fce.Function.ByMethodDecl == enclosingMethod) { reporter.Error(MessageSource.Resolver, expr.tok, "a recursive call in this context is not recognized as a tail call"); } - expr.SubExpressions.Iter(ee => DisallowRecursiveCallsInExpressions(ee, enclosingMethod)); + expr.SubExpressions.ForEach(ee => DisallowRecursiveCallsInExpressions(ee, enclosingMethod)); } TailRecursionStatus ConfirmTailCall(IToken tok, Method method, List typeApplication_JustMember, List lhss, bool reportErrors) { diff --git a/Source/DafnyCore/Rewriters/PrecedenceLinter.cs b/Source/DafnyCore/Rewriters/PrecedenceLinter.cs index c55811c115b..8c13cc656fa 100644 --- a/Source/DafnyCore/Rewriters/PrecedenceLinter.cs +++ b/Source/DafnyCore/Rewriters/PrecedenceLinter.cs @@ -140,7 +140,7 @@ protected override bool VisitOneExpr(Expression expr, ref LeftMargin st) { return false; // indicate that we've already processed expr's subexpressions } else if (expr is QuantifierExpr quantifierExpr) { - Attributes.SubExpressions(quantifierExpr.Attributes).Iter(VisitIndependentComponent); + Attributes.SubExpressions(quantifierExpr.Attributes).ForEach(VisitIndependentComponent); if (quantifierExpr.Range != null) { VisitIndependentComponent(quantifierExpr.Range); } @@ -150,14 +150,14 @@ protected override bool VisitOneExpr(Expression expr, ref LeftMargin st) { return false; // indicate that we've already processed expr's subexpressions } else if (expr is LetExpr letExpr) { - Attributes.SubExpressions(letExpr.Attributes).Iter(VisitIndependentComponent); - letExpr.RHSs.Iter(VisitIndependentComponent); + Attributes.SubExpressions(letExpr.Attributes).ForEach(VisitIndependentComponent); + letExpr.RHSs.ForEach(VisitIndependentComponent); VisitRhsComponent(expr.tok, letExpr.Body, "body of let-expression"); return false; // indicate that we've already processed expr's subexpressions } else if (expr is OldExpr or FreshExpr or UnchangedExpr or DatatypeValue or DisplayExpression or MapDisplayExpr) { // In these expressions, all subexpressions are contained in parentheses, so there's no risk of precedence confusion - expr.SubExpressions.Iter(VisitIndependentComponent); + expr.SubExpressions.ForEach(VisitIndependentComponent); return false; // indicate that we've already processed expr's subexpressions } else if (expr is FunctionCallExpr functionCallExpr) { @@ -181,7 +181,7 @@ protected override bool VisitOneExpr(Expression expr, ref LeftMargin st) { } else if (expr is NestedMatchExpr nestedMatchExpr) { // Handle each case like the "else" of an if-then-else - Attributes.SubExpressions(nestedMatchExpr.Attributes).Iter(VisitIndependentComponent); + Attributes.SubExpressions(nestedMatchExpr.Attributes).ForEach(VisitIndependentComponent); VisitIndependentComponent(nestedMatchExpr.Source); var n = nestedMatchExpr.Cases.Count; for (var i = 0; i < n; i++) { diff --git a/Source/DafnyCore/Rewriters/PrintEffectEnforcement.cs b/Source/DafnyCore/Rewriters/PrintEffectEnforcement.cs index b2dd4b31e2e..d3b3c214952 100644 --- a/Source/DafnyCore/Rewriters/PrintEffectEnforcement.cs +++ b/Source/DafnyCore/Rewriters/PrintEffectEnforcement.cs @@ -20,7 +20,7 @@ internal override void PostDecreasesResolve(ModuleDefinition m) { var hasPrintAttribute = HasPrintAttribute(iter.Attributes); if (!hasPrintAttribute && iter.Body != null) { if (Reporter.Options.EnforcePrintEffects) { - iter.Body.Body.Iter(stmt => CheckNoPrintEffects(stmt, iter)); + iter.Body.Body.ForEach(stmt => CheckNoPrintEffects(stmt, iter)); } } } else if (decl is TopLevelDeclWithMembers cl) { @@ -31,7 +31,7 @@ internal override void PostDecreasesResolve(ModuleDefinition m) { ReportError(ErrorId.rw_print_attribute_forbidden_on_functions, member.tok, ":print attribute is not allowed on functions"); } if (f.ByMethodDecl != null && Reporter.Options.EnforcePrintEffects) { - f.ByMethodDecl.Body.Body.Iter(stmt => CheckNoPrintEffects(stmt, f.ByMethodDecl)); + f.ByMethodDecl.Body.Body.ForEach(stmt => CheckNoPrintEffects(stmt, f.ByMethodDecl)); } } else if (member is Method method) { if (hasPrintAttribute) { @@ -43,7 +43,7 @@ internal override void PostDecreasesResolve(ModuleDefinition m) { } } else if (!member.IsGhost && method.Body != null) { if (Reporter.Options.EnforcePrintEffects) { - method.Body.Body.Iter(stmt => CheckNoPrintEffects(stmt, method)); + method.Body.Body.ForEach(stmt => CheckNoPrintEffects(stmt, method)); } } } @@ -81,7 +81,7 @@ private void CheckNoPrintEffects(Statement stmt, IMethodCodeContext codeContext) } } } - stmt.SubStatements.Iter(s => CheckNoPrintEffects(s, codeContext)); + stmt.SubStatements.ForEach(s => CheckNoPrintEffects(s, codeContext)); } } } diff --git a/Source/DafnyCore/Triggers/QuantifiersCollection.cs b/Source/DafnyCore/Triggers/QuantifiersCollection.cs index 952a9b7d139..72fcfb1515e 100644 --- a/Source/DafnyCore/Triggers/QuantifiersCollection.cs +++ b/Source/DafnyCore/Triggers/QuantifiersCollection.cs @@ -151,7 +151,9 @@ bool SuppressMatchingLoops() { (candidate, loopingSubterms) => { looping.Add(candidate); loopingMatches = loopingSubterms.ToList(); - candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "\"" + Printer.ExprToString(reporter.Options, t.OriginalExpr) + "\"", ", "); + candidate.Annotation = "may loop with " + + String.Join(", ", + loopingSubterms.Select(t => "\"" + Printer.ExprToString(reporter.Options, t.OriginalExpr) + "\"")); }).ToList(); q.CouldSuppressLoops = safe.Count > 0; diff --git a/Source/DafnyCore/Triggers/TriggersCollector.cs b/Source/DafnyCore/Triggers/TriggersCollector.cs index af6c07dcc8c..adb3e7298ff 100644 --- a/Source/DafnyCore/Triggers/TriggersCollector.cs +++ b/Source/DafnyCore/Triggers/TriggersCollector.cs @@ -203,7 +203,7 @@ private TriggerAnnotation Annotate(Expression expr) { } if (annotation == null) { - expr.SubExpressions.Iter(e => Annotate(e)); + expr.SubExpressions.ForEach(e => Annotate(e)); if (IsPotentialTriggerCandidate(expr)) { annotation = AnnotatePotentialCandidate(expr); diff --git a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs index be1199c04d7..1ae0a8154c5 100644 --- a/Source/DafnyCore/Verifier/Translator.ClassMembers.cs +++ b/Source/DafnyCore/Verifier/Translator.ClassMembers.cs @@ -652,16 +652,16 @@ private void AddMethodImpl(Method m, Boogie.Procedure proc, bool wellformednessP builder.Add(Boogie.Cmd.SimpleAssign(m.tok, new Boogie.IdentifierExpr(m.tok, "$_reverifyPost", Boogie.Type.Bool), Boogie.Expr.False)); // register output parameters with definite-assignment trackers Contract.Assert(definiteAssignmentTrackers.Count == 0); - m.Outs.Iter(p => AddExistingDefiniteAssignmentTracker(p, m.IsGhost)); + m.Outs.ForEach(p => AddExistingDefiniteAssignmentTracker(p, m.IsGhost)); // translate the body TrStmt(m.Body, builder, localVariables, etran); - m.Outs.Iter(p => CheckDefiniteAssignmentReturn(m.Body.RangeToken.EndToken, p, builder)); + m.Outs.ForEach(p => CheckDefiniteAssignmentReturn(m.Body.RangeToken.EndToken, p, builder)); if (m is { FunctionFromWhichThisIsByMethodDecl: { ByMethodTok: { } } fun }) { AssumeCanCallForByMethodDecl(m, builder); } stmts = builder.Collect(m.Body.RangeToken.StartToken); // TODO should this be EndToken? the parameter name suggests it should be the closing curly // tear down definite-assignment trackers - m.Outs.Iter(RemoveDefiniteAssignmentTracker); + m.Outs.ForEach(RemoveDefiniteAssignmentTracker); Contract.Assert(definiteAssignmentTrackers.Count == 0); } else { diff --git a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs index 7fe73330e68..b287ca2c4f7 100644 --- a/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs +++ b/Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs @@ -593,7 +593,7 @@ void CheckWellformedWithResult(Expression expr, WFOptions wfOptions, Bpl.Expr re } // Cannot use the datatype's formals, so we substitute the inferred type args: var su = new Dictionary(); - foreach (var p in LinqExtender.Zip(dtv.Ctor.EnclosingDatatype.TypeArgs, dtv.InferredTypeArgs)) { + foreach (var p in Enumerable.Zip(dtv.Ctor.EnclosingDatatype.TypeArgs, dtv.InferredTypeArgs)) { su[p.Item1] = p.Item2; } Type ty = formal.Type.Subst(su); diff --git a/Source/DafnyCore/Verifier/Translator.TrStatement.cs b/Source/DafnyCore/Verifier/Translator.TrStatement.cs index 00e43a29613..4777812e316 100644 --- a/Source/DafnyCore/Verifier/Translator.TrStatement.cs +++ b/Source/DafnyCore/Verifier/Translator.TrStatement.cs @@ -56,7 +56,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List CheckDefiniteAssignmentReturn(stmt.Tok, p, builder)); + method.Outs.ForEach(p => CheckDefiniteAssignmentReturn(stmt.Tok, p, builder)); } if (codeContext is Method { FunctionFromWhichThisIsByMethodDecl: { ByMethodTok: { } } fun } method2) { @@ -267,7 +267,7 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List f == null); var localSurrogates = fields.ConvertAll(f => new Bpl.LocalVariable(f.tok, new TypedIdent(f.tok, SurrogateName(f), TrType(f.Type)))); locals.AddRange(localSurrogates); - fields.Iter(f => AddDefiniteAssignmentTrackerSurrogate(f, cl, locals, codeContext is Constructor && codeContext.IsGhost)); + fields.ForEach(f => AddDefiniteAssignmentTrackerSurrogate(f, cl, locals, codeContext is Constructor && codeContext.IsGhost)); Contract.Assert(!inBodyInitContext); inBodyInitContext = true; @@ -277,8 +277,8 @@ private void TrStmt(Statement stmt, BoogieStmtListBuilder builder, List CheckDefiniteAssignmentSurrogate(s.SeparatorTok ?? s.RangeToken.EndToken, f, true, builder)); - fields.Iter(RemoveDefiniteAssignmentTrackerSurrogate); + fields.ForEach(f => CheckDefiniteAssignmentSurrogate(s.SeparatorTok ?? s.RangeToken.EndToken, f, true, builder)); + fields.ForEach(RemoveDefiniteAssignmentTrackerSurrogate); var th = new ThisExpr(cl); var bplThis = (Bpl.IdentifierExpr)etran.TrExpr(th); SelectAllocateObject(tok, bplThis, th.Type, false, builder, etran); diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs index 731b373b350..7ccd19b54ac 100644 --- a/Source/DafnyCore/Verifier/Translator.cs +++ b/Source/DafnyCore/Verifier/Translator.cs @@ -821,12 +821,12 @@ private Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { if (InsertChecksums) { foreach (var impl in sink.Implementations) { - if (impl.FindStringAttribute("checksum") == null) { + if (impl.FindAttribute("checksum") == null) { impl.AddAttribute("checksum", "stable"); } } foreach (var func in sink.Functions) { - if (func.FindStringAttribute("checksum") == null) { + if (func.FindAttribute("checksum") == null) { func.AddAttribute("checksum", "stable"); } } @@ -3362,15 +3362,15 @@ void RemoveDefiniteAssignmentTrackers(List ss, int prevDefAssTrackerC if (vdecl.Update is AssignOrReturnStmt ars) { foreach (var sx in ars.ResolvedStatements) { if (sx is VarDeclStmt vdecl2) { - vdecl2.Locals.Iter(RemoveDefiniteAssignmentTracker); + vdecl2.Locals.ForEach(RemoveDefiniteAssignmentTracker); } } } - vdecl.Locals.Iter(RemoveDefiniteAssignmentTracker); + vdecl.Locals.ForEach(RemoveDefiniteAssignmentTracker); } else if (s is AssignOrReturnStmt ars) { foreach (var sx in ars.ResolvedStatements) { if (sx is VarDeclStmt vdecl2) { - vdecl2.Locals.Iter(RemoveDefiniteAssignmentTracker); + vdecl2.Locals.ForEach(RemoveDefiniteAssignmentTracker); } } } @@ -6938,7 +6938,7 @@ private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, Me outParams.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.AssignUniqueName(currentDeclaration.IdGenerator), varType, wh), false)); } // tear down definite-assignment trackers - m.Outs.Iter(RemoveDefiniteAssignmentTracker); + m.Outs.ForEach(RemoveDefiniteAssignmentTracker); Contract.Assert(definiteAssignmentTrackers.Count == 0); if (kind == MethodTranslationKind.Implementation) { @@ -10591,7 +10591,7 @@ private bool CanSafelyInline(FunctionCallExpr fexp, Function f) { } visitor.Visit(body); } - return LinqExtender.Zip(f.Formals, fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2)); + return Enumerable.Zip(f.Formals, fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2)); } // Using an empty set of old expressions is ok here; the only uses of the triggersCollector will be to check for trigger killers. @@ -10717,8 +10717,8 @@ bool TrSplitNeedsTokenAdjustment(Expression expr) { // No expression introduces a type variable static void ComputeFreeTypeVariables(Expression expr, ISet fvs) { ComputeFreeTypeVariables(expr.Type, fvs); - expr.ComponentTypes.Iter(ty => ComputeFreeTypeVariables((Type)ty, fvs)); - expr.SubExpressions.Iter(ee => ComputeFreeTypeVariables(ee, fvs)); + expr.ComponentTypes.ForEach(ty => ComputeFreeTypeVariables((Type)ty, fvs)); + expr.SubExpressions.ForEach(ee => ComputeFreeTypeVariables(ee, fvs)); } static void ComputeFreeTypeVariables(Type ty, ISet fvs) { @@ -10728,7 +10728,7 @@ static void ComputeFreeTypeVariables(Type ty, ISet fvs) { Contract.Assert(ty.TypeArgs.Count == 0); fvs.Add(tp); } else { - ty.NormalizeExpandKeepConstraints().TypeArgs.Iter(tt => ComputeFreeTypeVariables(tt, fvs)); + ty.NormalizeExpandKeepConstraints().TypeArgs.ForEach(tt => ComputeFreeTypeVariables(tt, fvs)); } } @@ -10737,7 +10737,7 @@ static void ComputeFreeTypeVariables_All(Type ty, ISet fvs) { if (ty.IsTypeParameter) { fvs.Add(ty.AsTypeParameter); } - ty.NormalizeExpandKeepConstraints().TypeArgs.Iter(tt => ComputeFreeTypeVariables_All(tt, fvs)); + ty.NormalizeExpandKeepConstraints().TypeArgs.ForEach(tt => ComputeFreeTypeVariables_All(tt, fvs)); } public bool UsesHeap(Expression expr) { @@ -10847,7 +10847,7 @@ static Bpl.Expr BplForallTrim(IEnumerable> va return body; } for (var tt = trg; tt != null; tt = tt.Next) { - tt.Tr.Iter(ee => vis.Visit(ee)); + tt.Tr.ForEach(ee => vis.Visit(ee)); } var args = new List(); diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index b12cc09a587..414f9e04418 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -5,6 +5,7 @@ using System.IO; using System.Text; using System.Collections.Generic; +using System.Linq; using System.Runtime.Serialization; using System.Runtime.Serialization.Json; using Microsoft.Boogie; @@ -29,7 +30,7 @@ internal static void EOM(string header, Exception ex, string subHeader = "") { if (aggregate == null) { EOM(header, subHeader + ex.Message); } else { - EOM(header, subHeader + aggregate.InnerExceptions.MapConcat(exn => exn.Message, ", ")); + EOM(header, subHeader + String.Join(", ", aggregate.InnerExceptions.Select(e => e.Message))); } } } diff --git a/Source/DafnyTestGeneration/ProgramModifier.cs b/Source/DafnyTestGeneration/ProgramModifier.cs index 6c15a5869b6..fb9b47669eb 100644 --- a/Source/DafnyTestGeneration/ProgramModifier.cs +++ b/Source/DafnyTestGeneration/ProgramModifier.cs @@ -132,7 +132,7 @@ private static AssumeCmd GetAssumePrintCmd( string separator = " | ") { // first insert separators between the things being printed var toPrint = new List(); - data.Iter(obj => toPrint.AddRange(new List { obj, separator })); + data.ForEach(obj => toPrint.AddRange(new List { obj, separator })); if (toPrint.Count() != 0) { toPrint.RemoveAt(toPrint.Count() - 1); } @@ -256,7 +256,7 @@ private class CallGraph : ReadOnlyVisitor { public CallGraph(DafnyInfo info, Program program) { this.info = info; procedureNames = new(); - program.Procedures.Iter(p => procedureNames.Add(p.Name)); + program.Procedures.ForEach(p => procedureNames.Add(p.Name)); VisitProgram(program); } @@ -525,11 +525,11 @@ public override Program VisitProgram(Program node) { node = new RemoveFunctionsFromShortCircuitRewriter(modifier, options).VisitProgram(node); currProgram = node; functionMap = new(); - node.Functions.Iter(i => functionMap[i.Name] = i); + node.Functions.ForEach(i => functionMap[i.Name] = i); node.TopLevelDeclarations .OfType() .Where(i => modifier.ImplementationIsToBeTested(i)) - .Iter(i => VisitImplementation(i)); + .ForEach(i => VisitImplementation(i)); return Utils.DeepCloneResolvedProgram(node, options); } @@ -658,7 +658,7 @@ public override Cmd VisitAssumeCmd(AssumeCmd node) { new List { toBeAssigned }, new List { funcCall }); currAssignCmd = cmd; - funcCall.Args.Iter(e => VisitExpr(e)); + funcCall.Args.ForEach(e => VisitExpr(e)); currAssignCmd = null; commandsToInsert?.Add((cmd, node)); return node; @@ -689,13 +689,13 @@ public override Program VisitProgram(Program node) { functionMap = new(); procedureMap = new(); implementationMap = new(); - node.Implementations.Iter(i => implementationMap[i.Name] = i); - node.Functions.Iter(i => functionMap[i.Name] = i); - node.Procedures.Iter(i => procedureMap[i.Name] = i); + node.Implementations.ForEach(i => implementationMap[i.Name] = i); + node.Functions.ForEach(i => functionMap[i.Name] = i); + node.Procedures.ForEach(i => procedureMap[i.Name] = i); node.TopLevelDeclarations .OfType() .Where(i => modifier.ImplementationIsToBeTested(i)) - .Iter(i => VisitImplementation(i)); + .ForEach(i => VisitImplementation(i)); node.Resolve(options); return node; } diff --git a/Source/DafnyTestGeneration/Utils.cs b/Source/DafnyTestGeneration/Utils.cs index f68e4116153..b3a22617d9c 100644 --- a/Source/DafnyTestGeneration/Utils.cs +++ b/Source/DafnyTestGeneration/Utils.cs @@ -144,7 +144,7 @@ private static void AddByMethod(TopLevelDecl d) { AddByMethod(topLevelDecl); } } else if (d is TopLevelDeclWithMembers withMembers) { - withMembers.Members.OfType().Iter(AddByMethod); + withMembers.Members.OfType().ForEach(AddByMethod); } } diff --git a/customBoogie.patch b/customBoogie.patch index ceab354ade0..722366631fb 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + From 15bf0c5bb2479177c89c7d2c61091c444b49b88c Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 21 Jul 2023 15:19:52 -0700 Subject: [PATCH 5/6] Bump to Boogie 3.0.0 --- Source/DafnyCore/DafnyCore.csproj | 2 +- customBoogie.patch | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/DafnyCore.csproj b/Source/DafnyCore/DafnyCore.csproj index 6ca50785589..49ad7566759 100644 --- a/Source/DafnyCore/DafnyCore.csproj +++ b/Source/DafnyCore/DafnyCore.csproj @@ -32,7 +32,7 @@ - + diff --git a/customBoogie.patch b/customBoogie.patch index 722366631fb..22f8535f3ea 100644 --- a/customBoogie.patch +++ b/customBoogie.patch @@ -61,7 +61,7 @@ index 4a8b2f89b..a308be9bf 100644 -- +- + From a5a4338ac19c161fa63716354a0f1d01552c9f3a Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Fri, 21 Jul 2023 15:31:09 -0700 Subject: [PATCH 6/6] Update Options.txt --- docs/DafnyRef/Options.txt | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/docs/DafnyRef/Options.txt b/docs/DafnyRef/Options.txt index e5ce095472f..243812f716e 100644 --- a/docs/DafnyRef/Options.txt +++ b/docs/DafnyRef/Options.txt @@ -515,6 +515,8 @@ Usage: dafny [ option ... ] [ filename ... ] unroll loops, following up to n back edges (and then some) /soundLoopUnrolling sound loop unrolling + /doModSetAnalysis + automatically infer modifies clauses /printModel: 0 (default) - do not print Z3's error model 1 - print Z3's error model @@ -656,8 +658,6 @@ Usage: dafny [ option ... ] [ filename ... ] /smokeTimeout: Timeout, in seconds, for a single theorem prover invocation during smoke test, defaults to 10. - /causalImplies - Translate Boogie's A ==> B into prover's A ==> A && B. /typeEncoding: Encoding of types when generating VC of a polymorphic program: m = monomorphic (default) @@ -698,6 +698,13 @@ Usage: dafny [ option ... ] [ filename ... ] This option is implemented by renaming variables and reordering declarations in the input, and by setting solver options that have similar effects. + /trackVerificationCoverage + Track and report which program elements labeled with an + `{:id ...}` attribute were necessary to complete verification. + Assumptions, assertions, requires clauses, ensures clauses, + assignments, and calls can be labeled for inclusion in this + report. This generalizes and replaces the previous + (undocumented) `/printNecessaryAssertions` option. ---- Verification-condition splitting --------------------------------------