Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update to Boogie 3.0.0 #4209

Merged
merged 6 commits into from
Jul 21, 2023
Merged

Update to Boogie 3.0.0 #4209

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
0069a9d
Further reduce resource use of AppendOptimized
atomb Jul 18, 2023
01419b9
Revert "Further reduce resource use of AppendOptimized"
atomb Jul 18, 2023
88ec45d
Use correct old locations
atomb Jul 18, 2023
93c04f7
Update to Boogie 2.16.9
atomb Jun 21, 2023
15bf0c5
Bump to Boogie 3.0.0
atomb Jul 21, 2023
a5a4338
Update Options.txt
atomb Jul 21, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 21 additions & 21 deletions Source/DafnyCore/AST/AstVisitor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -57,7 +57,7 @@ protected virtual void VisitOneDeclaration(TopLevelDecl decl) {
}

if (decl is TopLevelDeclWithMembers cl) {
cl.Members.Iter(VisitMember);
cl.Members.ForEach(VisitMember);
}
}

Expand All @@ -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);
Expand Down Expand Up @@ -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);
Expand All @@ -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);
Expand All @@ -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) {
Expand Down Expand Up @@ -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);
}
Expand Down Expand Up @@ -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);
}
Expand Down
36 changes: 18 additions & 18 deletions Source/DafnyCore/AST/DafnyAst.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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) {
Expand Down Expand Up @@ -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;
Expand All @@ -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) {
Expand All @@ -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
Expand All @@ -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);
Expand All @@ -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) {
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/AST/Expressions/Expression.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/AST/Modules/ScopeCloner.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Compilers/Python/Compiler-python.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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__");
Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Dafny.atg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
.)
}
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/DafnyCore.csproj
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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>

Expand Down
4 changes: 2 additions & 2 deletions Source/DafnyCore/Generic/Node.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -328,7 +328,7 @@ void UpdateStartEndTokRecursive(Node node) {
}
}

PreResolveChildren.Iter(UpdateStartEndTokRecursive);
PreResolveChildren.ForEach(UpdateStartEndTokRecursive);

if (FormatTokens != null) {
foreach (var token in FormatTokens) {
Expand Down Expand Up @@ -360,4 +360,4 @@ protected RangeNode(Cloner cloner, RangeNode original) {
protected RangeNode(RangeToken rangeToken) {
RangeToken = rangeToken;
}
}
}
6 changes: 3 additions & 3 deletions Source/DafnyCore/Generic/Util.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand Down Expand Up @@ -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();
}
Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Resolver/Abstemious.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,6 @@ private void CheckDestructsAreAbstemiousCompliant(Expression expr) {
CheckDestructsAreAbstemiousCompliant(e.E);
return;
}
expr.SubExpressions.Iter(CheckDestructsAreAbstemiousCompliant);
expr.SubExpressions.ForEach(CheckDestructsAreAbstemiousCompliant);
}
}
4 changes: 2 additions & 2 deletions Source/DafnyCore/Resolver/BoundsDiscovery.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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;
}
Expand Down
16 changes: 8 additions & 8 deletions Source/DafnyCore/Resolver/CheckDividedConstructorInit_Visitor.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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); // (***)
}
Expand Down Expand Up @@ -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);
Expand Down
Loading
Loading