From 0d0928e0660c2c660da581cc2e7115f73a4b4207 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Mar 2022 19:12:43 -0800 Subject: [PATCH 01/14] Shift contents of test file --- Test/dafny0/AttributeChecks.dfy | 161 +++++++++++++------------ Test/dafny0/AttributeChecks.dfy.expect | 48 ++++---- 2 files changed, 105 insertions(+), 104 deletions(-) diff --git a/Test/dafny0/AttributeChecks.dfy b/Test/dafny0/AttributeChecks.dfy index ac015c04d21..ebf4e5f1b98 100644 --- a/Test/dafny0/AttributeChecks.dfy +++ b/Test/dafny0/AttributeChecks.dfy @@ -1,106 +1,107 @@ // RUN: %dafny /print:"%t.print" /dprint:- /compile:0 /env:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" -method If(n: int) returns (k: int) -{ - var i := 0; - if {:split true} i < n { - if {:split 1 + 0} true {} + + method If(n: int) returns (k: int) + { + var i := 0; + if {:split true} i < n { + if {:split 1 + 0} true {} + } + else if {:split false} i > n {} + else {:split true} {} } - else if {:split false} i > n {} - else {:split true} {} -} -method IfAlt(n: int) returns (k: int) -{ - var i := 0; - if {:split true} - case {:split 1 + true} i < n => // error: 1 + true is ill-typed - if {:split 1 + k} true {} - case {:split false} i > n => {} - return 2; -} + method IfAlt(n: int) returns (k: int) + { + var i := 0; + if {:split true} + case {:split 1 + true} i < n => // error: 1 + true is ill-typed + if {:split 1 + k} true {} + case {:split false} i > n => {} + return 2; + } -method While(n: int) returns (k: int) -{ - var f: int -> int := x => x; - var i := 0; - while {:split true} {:split true + k} i < n // error: true + k is ill-typed - invariant forall u :: f(u) == u + i + method While(n: int) returns (k: int) { + var f: int -> int := x => x; + var i := 0; + while {:split true} {:split true + k} i < n // error: true + k is ill-typed + invariant forall u :: f(u) == u + i + { + } + return 2; } - return 2; -} -method WhileAlt(n: int) returns (k: int) -{ - var i := 0; - var f: int -> int := x => x; - while {:split} - invariant forall u :: f(u) == u + i + method WhileAlt(n: int) returns (k: int) { - case {:split 1 + true} i < n => {} // error: 1 + true is ill-typed - case {:split false} i > n => return 2; + var i := 0; + var f: int -> int := x => x; + while {:split} + invariant forall u :: f(u) == u + i + { + case {:split 1 + true} i < n => {} // error: 1 + true is ill-typed + case {:split false} i > n => return 2; + } } -} -datatype List = Nil | Cons (hd:T, tl: List) -method Match(xs: List) returns (r: int) -{ - match {:split 1} xs { - case {:split false} Cons(y, z) => return y; - case {:split 1 + false} Nil => return 0; // error: 1 + false is ill-typed + datatype List = Nil | Cons (hd:T, tl: List) + method Match(xs: List) returns (r: int) + { + match {:split 1} xs { + case {:split false} Cons(y, z) => return y; + case {:split 1 + false} Nil => return 0; // error: 1 + false is ill-typed + } } -} -function method CaseExpr(r: List): List -{ - match r { - case Nil => Nil - case {:ignore 3 + true} Cons(h, Nil) => Nil // error: 3 + true is ill-typed - case {:ignore false} Cons(h, t) => CaseExpr(t) + function method CaseExpr(r: List): List + { + match r { + case Nil => Nil + case {:ignore 3 + true} Cons(h, Nil) => Nil // error: 3 + true is ill-typed + case {:ignore false} Cons(h, t) => CaseExpr(t) + } } -} -method Calc(x: int, y: int) -{ - calc {:split 1} {:split 1 + false} { // error: 1 + false is ill-typed - x + y; - { assume x == 0; } - y; + method Calc(x: int, y: int) + { + calc {:split 1} {:split 1 + false} { // error: 1 + false is ill-typed + x + y; + { assume x == 0; } + y; + } + assert x == 0; // OK: follows from x + y == y; } - assert x == 0; // OK: follows from x + y == y; -} -method ForAll(i: int, j: int, arr: array2) -{ - forall i , j {:split 1 + false} {:split i + j} | i in {-3, 4} && j in {1, 2} { // error: 1 + false is ill-typed - arr[i, j] := 0; + method ForAll(i: int, j: int, arr: array2) + { + forall i , j {:split 1 + false} {:split i + j} | i in {-3, 4} && j in {1, 2} { // error: 1 + false is ill-typed + arr[i, j] := 0; + } } -} -method AssertBy(x: int, y: int) -{ - assert {:split false + x} {:split} x == 6 by { // error: false + x is ill-typed - assume x == 6; - assume y == 8; + method AssertBy(x: int, y: int) + { + assert {:split false + x} {:split} x == 6 by { // error: false + x is ill-typed + assume x == 6; + assume y == 8; + } + assert {:split} y == 8; } - assert {:split} y == 8; -} -method For(lo: int, hi: int) returns (k: int) - requires lo <= hi -{ - var f: int -> int := x => x; - for {:split i} {:split true + k} i := lo to hi // error: true + k is ill-typed - invariant forall u :: f(u) == u + i + method For(lo: int, hi: int) returns (k: int) + requires lo <= hi { + var f: int -> int := x => x; + for {:split i} {:split true + k} i := lo to hi // error: true + k is ill-typed + invariant forall u :: f(u) == u + i + { + } + return 2; } - return 2; -} -datatype {:dt 0} {:dt false + 3} Datatype = // error: false + 3 is ill-typed - {:dt k} Blue | {:dt 50} Green // error: k is unknown + datatype {:dt 0} {:dt false + 3} Datatype = // error: false + 3 is ill-typed + {:dt k} Blue | {:dt 50} Green // error: k is unknown -datatype {:dt 0} {:dt false + 3} AnotherDatatype = // error: false + 3 is ill-typed - | {:dt 50} Blue | {:dt k} Green // error: k is unknown + datatype {:dt 0} {:dt false + 3} AnotherDatatype = // error: false + 3 is ill-typed + | {:dt 50} Blue | {:dt k} Green // error: k is unknown diff --git a/Test/dafny0/AttributeChecks.dfy.expect b/Test/dafny0/AttributeChecks.dfy.expect index 295a7fb6afe..833fcde5354 100644 --- a/Test/dafny0/AttributeChecks.dfy.expect +++ b/Test/dafny0/AttributeChecks.dfy.expect @@ -116,28 +116,28 @@ method For(lo: int, hi: int) returns (k: int) } return 2; } -AttributeChecks.dfy(103,7): Error: unresolved identifier: k -AttributeChecks.dfy(102,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(102,28): Error: type of right argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(106,25): Error: unresolved identifier: k -AttributeChecks.dfy(105,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(105,28): Error: type of right argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(18,17): Error: type of left argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(18,17): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(28,35): Error: type of right argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(28,35): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(42,19): Error: type of left argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(42,19): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(52,19): Error: type of left argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(52,19): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(60,20): Error: type of left argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(60,20): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(67,28): Error: type of left argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(67,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(77,25): Error: type of left argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(77,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(84,23): Error: type of right argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(84,23): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(95,30): Error: type of right argument to + (int) must agree with the result type (bool) -AttributeChecks.dfy(95,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(104,9): Error: unresolved identifier: k +AttributeChecks.dfy(103,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(103,30): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(107,27): Error: unresolved identifier: k +AttributeChecks.dfy(106,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(106,30): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(19,19): Error: type of left argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(19,19): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(29,37): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(29,37): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(43,21): Error: type of left argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(43,21): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(53,21): Error: type of left argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(53,21): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(61,22): Error: type of left argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(61,22): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(68,30): Error: type of left argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(68,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(78,27): Error: type of left argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(78,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(85,25): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(85,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(96,32): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(96,32): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) 24 resolution/type errors detected in AttributeChecks.dfy From 1819beb3a18472cb359475623f603a72f8de68af Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Mar 2022 19:14:28 -0800 Subject: [PATCH 02/14] Add enclosing module into test file --- Test/dafny0/AttributeChecks.dfy | 3 +- Test/dafny0/AttributeChecks.dfy.expect | 179 +++++++++++++------------ 2 files changed, 93 insertions(+), 89 deletions(-) diff --git a/Test/dafny0/AttributeChecks.dfy b/Test/dafny0/AttributeChecks.dfy index ebf4e5f1b98..0754c4e98b7 100644 --- a/Test/dafny0/AttributeChecks.dfy +++ b/Test/dafny0/AttributeChecks.dfy @@ -1,7 +1,7 @@ // RUN: %dafny /print:"%t.print" /dprint:- /compile:0 /env:0 "%s" > "%t" // RUN: %diff "%s.expect" "%t" - +module JustAboutEverything { method If(n: int) returns (k: int) { var i := 0; @@ -105,3 +105,4 @@ datatype {:dt 0} {:dt false + 3} AnotherDatatype = // error: false + 3 is ill-typed | {:dt 50} Blue | {:dt k} Green // error: k is unknown +} diff --git a/Test/dafny0/AttributeChecks.dfy.expect b/Test/dafny0/AttributeChecks.dfy.expect index 833fcde5354..cb4ebb222f5 100644 --- a/Test/dafny0/AttributeChecks.dfy.expect +++ b/Test/dafny0/AttributeChecks.dfy.expect @@ -1,120 +1,123 @@ // AttributeChecks.dfy -datatype List = Nil | Cons(hd: T, tl: List) -datatype {:dt 0} {:dt false + 3} Datatype = {:dt k} Blue | {:dt 50} Green +module JustAboutEverything { + datatype List = Nil | Cons(hd: T, tl: List) -datatype {:dt 0} {:dt false + 3} AnotherDatatype = {:dt 50} Blue | {:dt k} Green + datatype {:dt 0} {:dt false + 3} Datatype = {:dt k} Blue | {:dt 50} Green -method If(n: int) returns (k: int) -{ - var i := 0; - if {:split true} i < n { - if {:split 1 + 0} true { - } - } else if {:split false} i > n { - } else {:split true} { - } -} - -method IfAlt(n: int) returns (k: int) -{ - var i := 0; - if {:split true} - case {:split 1 + true} i < n => - if {:split 1 + k} true { - } - case {:split false} i > n => - { - } - return 2; -} + datatype {:dt 0} {:dt false + 3} AnotherDatatype = {:dt 50} Blue | {:dt k} Green -method While(n: int) returns (k: int) -{ - var f: int -> int := x => x; - var i := 0; - while {:split true} {:split true + k} i < n - invariant forall u :: f(u) == u + i + method If(n: int) returns (k: int) { + var i := 0; + if {:split true} i < n { + if {:split 1 + 0} true { + } + } else if {:split false} i > n { + } else {:split true} { + } } - return 2; -} -method WhileAlt(n: int) returns (k: int) -{ - var i := 0; - var f: int -> int := x => x; - while {:split} - invariant forall u :: f(u) == u + i + method IfAlt(n: int) returns (k: int) { + var i := 0; + if {:split true} case {:split 1 + true} i < n => - { + if {:split 1 + k} true { } case {:split false} i > n => + { + } return 2; } -} -method Match(xs: List) returns (r: int) -{ - match {:split 1} xs { - case {:split false} Cons(y, z) => - return y; - case {:split 1 + false} Nil => - return 0; + method While(n: int) returns (k: int) + { + var f: int -> int := x => x; + var i := 0; + while {:split true} {:split true + k} i < n + invariant forall u :: f(u) == u + i + { + } + return 2; } -} -function method CaseExpr(r: List): List -{ - match r { - case Nil => - Nil - case {:ignore 3 + true} Cons(h, Nil) => - Nil - case {:ignore false} Cons(h, t) => - CaseExpr(t) + method WhileAlt(n: int) returns (k: int) + { + var i := 0; + var f: int -> int := x => x; + while {:split} + invariant forall u :: f(u) == u + i + { + case {:split 1 + true} i < n => + { + } + case {:split false} i > n => + return 2; + } } -} -method Calc(x: int, y: int) -{ - calc {:split 1} {:split 1 + false} { - x + y; - { - assume x == 0; + method Match(xs: List) returns (r: int) + { + match {:split 1} xs { + case {:split false} Cons(y, z) => + return y; + case {:split 1 + false} Nil => + return 0; } - y; } - assert x == 0; -} -method ForAll(i: int, j: int, arr: array2) -{ - forall i, j {:split 1 + false} {:split i + j} | i in {-3, 4} && j in {1, 2} { - arr[i, j] := 0; + function method CaseExpr(r: List): List + { + match r { + case Nil => + Nil + case {:ignore 3 + true} Cons(h, Nil) => + Nil + case {:ignore false} Cons(h, t) => + CaseExpr(t) + } } -} -method AssertBy(x: int, y: int) -{ - assert {:split false + x} {:split} x == 6 by { - assume x == 6; - assume y == 8; + method Calc(x: int, y: int) + { + calc {:split 1} {:split 1 + false} { + x + y; + { + assume x == 0; + } + y; + } + assert x == 0; } - assert {:split} y == 8; -} -method For(lo: int, hi: int) returns (k: int) - requires lo <= hi -{ - var f: int -> int := x => x; - for {:split i} {:split true + k} i := lo to hi - invariant forall u :: f(u) == u + i + method ForAll(i: int, j: int, arr: array2) { + forall i, j {:split 1 + false} {:split i + j} | i in {-3, 4} && j in {1, 2} { + arr[i, j] := 0; + } + } + + method AssertBy(x: int, y: int) + { + assert {:split false + x} {:split} x == 6 by { + assume x == 6; + assume y == 8; + } + assert {:split} y == 8; + } + + method For(lo: int, hi: int) returns (k: int) + requires lo <= hi + { + var f: int -> int := x => x; + for {:split i} {:split true + k} i := lo to hi + invariant forall u :: f(u) == u + i + { + } + return 2; } - return 2; } AttributeChecks.dfy(104,9): Error: unresolved identifier: k AttributeChecks.dfy(103,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) From 46f9df8c472434f40783c5634d1618b5c82544ef Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Mar 2022 19:34:00 -0800 Subject: [PATCH 03/14] Mark five more classes as IAttributeBearingDeclaration --- Source/Dafny/AST/DafnyAst.cs | 10 +++++----- Source/Dafny/Resolver.cs | 22 +++++++++++----------- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index 7091900aa77..a91f66536c6 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -8042,7 +8042,7 @@ public override IEnumerable NonSpecificationSubExpressions { } } - public class GuardedAlternative { + public class GuardedAlternative : IAttributeBearingDeclaration { public readonly IToken Tok; public readonly bool IsBindingGuard; public readonly Expression Guard; @@ -12478,7 +12478,7 @@ public NestedMatchCase(IToken tok, ExtendedPattern pat) { } } - public class NestedMatchCaseExpr : NestedMatchCase { + public class NestedMatchCaseExpr : NestedMatchCase, IAttributeBearingDeclaration { public readonly Expression Body; public Attributes Attributes; @@ -12489,7 +12489,7 @@ public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Att } } - public class NestedMatchCaseStmt : NestedMatchCase { + public class NestedMatchCaseStmt : NestedMatchCase, IAttributeBearingDeclaration { public readonly List Body; public Attributes Attributes; public NestedMatchCaseStmt(IToken tok, ExtendedPattern pat, List body) : base(tok, pat) { @@ -12615,7 +12615,7 @@ public override IEnumerable SubExpressions { } } - public class AttributedExpression { + public class AttributedExpression : IAttributeBearingDeclaration { public readonly Expression E; public readonly AssertLabel/*?*/ Label; @@ -13035,7 +13035,7 @@ public ApplySuffix(IToken tok, IToken/*?*/ atLabel, Expression lhs, List where T : class { + public class Specification : IAttributeBearingDeclaration where T : class { public readonly List Expressions; [ContractInvariantMethod] diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index e01ad8064c8..374be4dfd9e 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -10139,7 +10139,7 @@ void ResolveFunction(Function f) { scope.PopMarker(); } } - ResolveAttributes(f.Decreases.Attributes, null, new ResolveOpts(f, f is TwoStateFunction)); + ResolveAttributes(f.Decreases.Attributes, f.Decreases, new ResolveOpts(f, f is TwoStateFunction)); foreach (Expression r in f.Decreases.Expressions) { ResolveExpression(r, new ResolveOpts(f, f is TwoStateFunction)); // any type is fine @@ -10281,13 +10281,13 @@ void ResolveMethod(Method m) { // Start resolving specification... foreach (AttributedExpression e in m.Req) { - ResolveAttributes(e.Attributes, null, new ResolveOpts(m, m is TwoStateLemma)); + ResolveAttributes(e.Attributes, e, new ResolveOpts(m, m is TwoStateLemma)); ResolveExpression(e.E, new ResolveOpts(m, m is TwoStateLemma)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Precondition must be a boolean (got {0})"); } - ResolveAttributes(m.Mod.Attributes, null, new ResolveOpts(m, false)); + ResolveAttributes(m.Mod.Attributes, m.Mod, new ResolveOpts(m, false)); foreach (FrameExpression fe in m.Mod.Expressions) { ResolveFrameExpression(fe, FrameExpressionUse.Modifies, m); if (m.IsLemmaLike) { @@ -10296,7 +10296,7 @@ void ResolveMethod(Method m) { DisallowNonGhostFieldSpecifiers(fe); } } - ResolveAttributes(m.Decreases.Attributes, null, new ResolveOpts(m, false)); + ResolveAttributes(m.Decreases.Attributes, m.Decreases, new ResolveOpts(m, false)); foreach (Expression e in m.Decreases.Expressions) { ResolveExpression(e, new ResolveOpts(m, m is TwoStateLemma)); // any type is fine @@ -10324,7 +10324,7 @@ void ResolveMethod(Method m) { // ... continue resolving specification foreach (AttributedExpression e in m.Ens) { - ResolveAttributes(e.Attributes, null, new ResolveOpts(m, true)); + ResolveAttributes(e.Attributes, e, new ResolveOpts(m, true)); ResolveExpression(e.E, new ResolveOpts(m, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Postcondition must be a boolean (got {0})"); @@ -11503,7 +11503,7 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) { } else if (stmt is ModifyStmt) { var s = (ModifyStmt)stmt; - ResolveAttributes(s.Mod.Attributes, null, new ResolveOpts(codeContext, true)); + ResolveAttributes(s.Mod.Attributes, s.Mod, new ResolveOpts(codeContext, true)); foreach (FrameExpression fe in s.Mod.Expressions) { ResolveFrameExpression(fe, FrameExpressionUse.Modifies, codeContext); } @@ -11617,7 +11617,7 @@ private void ResolveLoopSpecificationComponents(List invar Contract.Requires(codeContext != null); foreach (AttributedExpression inv in invariants) { - ResolveAttributes(inv.Attributes, null, new ResolveOpts(codeContext, true)); + ResolveAttributes(inv.Attributes, inv, new ResolveOpts(codeContext, true)); ResolveExpression(inv.E, new ResolveOpts(codeContext, true)); Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression if (fvs != null) { @@ -11638,7 +11638,7 @@ private void ResolveLoopSpecificationComponents(List invar // any type is fine } - ResolveAttributes(modifies.Attributes, null, new ResolveOpts(codeContext, true)); + ResolveAttributes(modifies.Attributes, modifies, new ResolveOpts(codeContext, true)); if (modifies.Expressions != null) { usesHeap = true; // bearing a modifies clause counts as using the heap foreach (FrameExpression fe in modifies.Expressions) { @@ -12722,7 +12722,7 @@ private void CheckLinearNestedMatchCase(Type type, NestedMatchCase mc, ResolveOp private void CheckLinearNestedMatchExpr(Type dtd, NestedMatchExpr me, ResolveOpts opts) { foreach (NestedMatchCaseExpr mc in me.Cases) { scope.PushMarker(); - ResolveAttributes(mc.Attributes, null, opts); + ResolveAttributes(mc.Attributes, mc, opts); CheckLinearNestedMatchCase(dtd, mc, opts); scope.PopMarker(); } @@ -12731,7 +12731,7 @@ private void CheckLinearNestedMatchExpr(Type dtd, NestedMatchExpr me, ResolveOpt private void CheckLinearNestedMatchStmt(Type dtd, NestedMatchStmt ms, ResolveOpts opts) { foreach (NestedMatchCaseStmt mc in ms.Cases) { scope.PushMarker(); - ResolveAttributes(mc.Attributes, null, opts); + ResolveAttributes(mc.Attributes, mc, opts); CheckLinearNestedMatchCase(dtd, mc, opts); scope.PopMarker(); } @@ -13381,7 +13381,7 @@ void ResolveAlternatives(List alternatives, AlternativeLoopS ScopePushAndReport(scope, v, "bound-variable"); } } - ResolveAttributes(alternative.Attributes, null, new ResolveOpts(codeContext, true)); + ResolveAttributes(alternative.Attributes, alternative, new ResolveOpts(codeContext, true)); foreach (Statement ss in alternative.Body) { ResolveStatementWithLabels(ss, codeContext); } From 6434e9454acb46c9f48c897d2acefafc496ecd8d Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Mar 2022 20:25:35 -0800 Subject: [PATCH 04/14] Remove parsed-and-ignored attributes on reads clauses --- Source/Dafny/Dafny.atg | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 287996afe4b..64c268347b3 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1831,10 +1831,8 @@ DecreasesClause<.List decreases, ref Attributes attrs, /*------------------------------------------------------------------------*/ ReadsClause<.List/*!*/ reads, bool allowLemma, bool allowLambda, bool allowWild.> -= "reads" (. Attributes attrs = null; - FrameExpression fe; - .) - { Attribute } += "reads" + (. FrameExpression fe; .) PossiblyWildFrameExpression (. reads.Add(fe); .) { "," PossiblyWildFrameExpression (. reads.Add(fe); .) } From b5c03a92f691ab005dadc907d8d18440d96fc9c0 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Mar 2022 21:44:42 -0800 Subject: [PATCH 05/14] Remove parsed-and-ignored attributes on lambda-expr requires --- Source/Dafny/Dafny.atg | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 64c268347b3..2d68a7988af 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -3997,8 +3997,7 @@ LambdaExpression // Coco says LambdaSpec is deletable. This is OK (it might be empty). LambdaSpec<.ref List reads, ref Expression req.> = { ReadsClause - | "requires" (. Attributes attrs = null; .) - { Attribute } (. Expression ee; .) + | "requires" (. Expression ee; .) Expression (. req = req == null ? ee : new BinaryExpr(req.tok, BinaryExpr.Opcode.And, req, ee); .) } . From 34aa423e26a6621de32fdb2b4d5985ddf35f8da0 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Mar 2022 20:49:52 -0800 Subject: [PATCH 06/14] =?UTF-8?q?fix:=20Don=E2=80=99t=20throw=20away=20par?= =?UTF-8?q?sed=20decreases=20attributes=20on=20functions?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Source/Dafny/Dafny.atg | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 2d68a7988af..544331b95ef 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -2132,6 +2132,7 @@ FunctionDecl List ens = new List(); List reads = new List(); List decreases; + Attributes decAttrs = null; Expression body = null; bool isPredicate = false; bool isLeastPredicate = false; bool isGreatestPredicate = false; IToken/*?*/ headToken = null; // used only for a basic "function" or "predicate" @@ -2257,7 +2258,7 @@ FunctionDecl ) (. decreases = isLeastPredicate || isGreatestPredicate ? null : new List(); .) - FunctionSpec + FunctionSpec (. IToken byMethodTok = null; BlockStmt byMethodBody = null; .) [ FunctionBody ] @@ -2398,15 +2399,15 @@ FunctionDecl if (isTwoState && isPredicate) { Contract.Assert(functionMethodToken == null && !dmod.IsGhost); f = new TwoStatePredicate(tok, id.val, dmod.IsStatic, typeArgs, formals, - reqs, reads, ens, new Specification(decreases, null), body, attrs, signatureEllipsis); + reqs, reads, ens, new Specification(decreases, decAttrs), body, attrs, signatureEllipsis); } else if (isTwoState) { Contract.Assert(functionMethodToken == null && !dmod.IsGhost); f = new TwoStateFunction(tok, id.val, dmod.IsStatic, typeArgs, formals, result, returnType, - reqs, reads, ens, new Specification(decreases, null), body, attrs, signatureEllipsis); + reqs, reads, ens, new Specification(decreases, decAttrs), body, attrs, signatureEllipsis); } else if (isPredicate) { Contract.Assert(functionMethodToken == null || !dmod.IsGhost); f = new Predicate(tok, id.val, dmod.IsStatic, isGhost, typeArgs, formals, - reqs, reads, ens, new Specification(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, + reqs, reads, ens, new Specification(decreases, decAttrs), body, Predicate.BodyOriginKind.OriginalOrInherited, byMethodTok, byMethodBody, attrs, signatureEllipsis); } else if (isLeastPredicate) { Contract.Assert(functionMethodToken == null && !dmod.IsGhost); @@ -2420,7 +2421,7 @@ FunctionDecl Contract.Assert(functionMethodToken == null || !dmod.IsGhost); f = new Function(tok, id.val, dmod.IsStatic, isGhost, typeArgs, formals, result, returnType, - reqs, reads, ens, new Specification(decreases, null), body, + reqs, reads, ens, new Specification(decreases, decAttrs), body, byMethodTok, byMethodBody, attrs, signatureEllipsis); } @@ -2435,11 +2436,10 @@ FunctionDecl . /*------------------------------------------------------------------------*/ -FunctionSpec<.List/*!*/ reqs, List/*!*/ reads, List/*!*/ ens, List decreases.> +FunctionSpec<.List reqs, List reads, List ens, List decreases, ref Attributes decAttrs.> = (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(decreases == null || cce.NonNullElements(decreases)); - Attributes attrs = null; .) SYNC { RequiresClause @@ -2450,7 +2450,7 @@ FunctionSpec<.List/*!*/ reqs, List(); } .) - DecreasesClause + DecreasesClause } . From 5ffdfd0203713a66fa603bf6387333955d84c639 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Mar 2022 21:32:05 -0800 Subject: [PATCH 07/14] fix: Resolve attributes on function/iterator specs * attributes on requires/ensures clauses for functions * attributes on all specification clauses for iterators --- Source/Dafny/Resolver.cs | 8 + Test/dafny0/AttributeChecks.dfy | 134 ++++++++++++++++ Test/dafny0/AttributeChecks.dfy.expect | 206 ++++++++++++++++++++++++- 3 files changed, 347 insertions(+), 1 deletion(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 374be4dfd9e..bda40acdf0b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -10118,6 +10118,7 @@ void ResolveFunction(Function f) { } ResolveParameterDefaultValues(f.Formals, f); foreach (AttributedExpression e in f.Req) { + ResolveAttributes(e.Attributes, e, new ResolveOpts(f, f is TwoStateFunction)); Expression r = e.E; ResolveExpression(r, new ResolveOpts(f, f is TwoStateFunction)); Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression @@ -10132,6 +10133,7 @@ void ResolveFunction(Function f) { scope.PushMarker(); scope.Push(f.Result.Name, f.Result); // function return only visible in post-conditions } + ResolveAttributes(e.Attributes, e, new ResolveOpts(f, f is TwoStateFunction)); ResolveExpression(r, new ResolveOpts(f, f is TwoStateFunction, false, true, false)); // since this is a function, the postcondition is still a one-state predicate, unless it's a two-state function Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(r, "Postcondition must be a boolean (got {0})"); @@ -10440,6 +10442,7 @@ void ResolveIterator(IteratorDecl iter) { // we start with the decreases clause, because the _decreases fields were only given type proxies before; we'll know // the types only after resolving the decreases clause (and it may be that some of resolution has already seen uses of // these fields; so, with no further ado, here we go + ResolveAttributes(iter.Decreases.Attributes, iter.Decreases, new ResolveOpts(iter, false)); Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count); for (int i = 0; i < iter.Decreases.Expressions.Count; i++) { var e = iter.Decreases.Expressions[i]; @@ -10452,10 +10455,12 @@ void ResolveIterator(IteratorDecl iter) { foreach (FrameExpression fe in iter.Reads.Expressions) { ResolveFrameExpression(fe, FrameExpressionUse.Reads, iter); } + ResolveAttributes(iter.Modifies.Attributes, iter.Modifies, new ResolveOpts(iter, false)); foreach (FrameExpression fe in iter.Modifies.Expressions) { ResolveFrameExpression(fe, FrameExpressionUse.Modifies, iter); } foreach (AttributedExpression e in iter.Requires) { + ResolveAttributes(e.Attributes, e, new ResolveOpts(iter, false)); ResolveExpression(e.E, new ResolveOpts(iter, false)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Precondition must be a boolean (got {0})"); @@ -10470,16 +10475,19 @@ void ResolveIterator(IteratorDecl iter) { Contract.Assert(scope.AllowInstance); foreach (AttributedExpression e in iter.YieldRequires) { + ResolveAttributes(e.Attributes, e, new ResolveOpts(iter, false)); ResolveExpression(e.E, new ResolveOpts(iter, false)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Yield precondition must be a boolean (got {0})"); } foreach (AttributedExpression e in iter.YieldEnsures) { + ResolveAttributes(e.Attributes, e, new ResolveOpts(iter, true)); ResolveExpression(e.E, new ResolveOpts(iter, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Yield postcondition must be a boolean (got {0})"); } foreach (AttributedExpression e in iter.Ensures) { + ResolveAttributes(e.Attributes, e, new ResolveOpts(iter, true)); ResolveExpression(e.E, new ResolveOpts(iter, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Postcondition must be a boolean (got {0})"); diff --git a/Test/dafny0/AttributeChecks.dfy b/Test/dafny0/AttributeChecks.dfy index 0754c4e98b7..8e0d058b1d9 100644 --- a/Test/dafny0/AttributeChecks.dfy +++ b/Test/dafny0/AttributeChecks.dfy @@ -105,4 +105,138 @@ module JustAboutEverything { datatype {:dt 0} {:dt false + 3} AnotherDatatype = // error: false + 3 is ill-typed | {:dt 50} Blue | {:dt k} Green // error: k is unknown + + function FAttr(x: int): int + requires {:myAttr false + 3} true // error: false + 3 is ill-typed + ensures {:myAttr false + 3} true // error: false + 3 is ill-typed + decreases {:myAttr false + 3} x // error: false + 3 is ill-typed + { + 10 + } + + function GAttr(x: int): int + requires {:myAttr old(3)} true // error: old is not allowed here + ensures {:myAttr old(3)} true // error: old is not allowed here + decreases {:myAttr old(3)} x // error: old is not allowed here + { + 10 + } + + function HAttr(x: int): (r: int) + requires {:myAttr x, r} true // error: r is not in scope here + ensures {:myAttr x, r} true + decreases {:myAttr x, r} x // error: r is not in scope here + { + 10 + } + + twostate function F2Attr(x: int): int + requires {:myAttr false + 3} true // error: false + 3 is ill-typed + ensures {:myAttr false + 3} true // error: false + 3 is ill-typed + decreases {:myAttr false + 3} x // error: false + 3 is ill-typed + { + 10 + } + + twostate function G2Attr(x: int): int + requires {:myAttr old(3)} true + ensures {:myAttr old(3)} true + decreases {:myAttr old(3)} x + { + 10 + } + + twostate function H2Attr(x: int): (r: int) + requires {:myAttr x, r} true // error: r is not in scope here + ensures {:myAttr x, r} true + decreases {:myAttr x, r} x // error: r is not in scope here + { + 10 + } + + method MAttr(x: int) returns (y: int) + requires {:myAttr false + 3} true // error: false + 3 is ill-typed + modifies {:myAttr false + 3} {} // error: false + 3 is ill-typed + ensures {:myAttr false + 3} true // error: false + 3 is ill-typed + decreases {:myAttr false + 3} x // error: false + 3 is ill-typed + { + } + + method NAttr(x: int) returns (y: int) + requires {:myAttr old(3)} true // error: old is not allowed here + modifies {:myAttr old(3)} {} // error: old is not allowed here + ensures {:myAttr old(3)} true + decreases {:myAttr old(3)} x // error: old is not allowed here + { + } + + method OAttr(x: int) returns (y: int) + requires {:myAttr x, y} true // error: y is not in scope here + modifies {:myAttr x, y} {} // error: y is not in scope here + ensures {:myAttr x, y} true + decreases {:myAttr x, y} x // error: y is not in scope here + { + } + + twostate lemma M2Attr(x: int) returns (y: int) + requires {:myAttr false + 3} true // error: false + 3 is ill-typed + modifies {:myAttr false + 3} {} // error (x2): false + 3 is ill-typed, and twostate lemma cannot have modifies clause + ensures {:myAttr false + 3} true // error: false + 3 is ill-typed + decreases {:myAttr false + 3} x // error: false + 3 is ill-typed + { + } + + twostate lemma N2Attr(x: int) returns (y: int) + requires {:myAttr old(3)} true + modifies {:myAttr old(3)} {} // error (x2): old is not allowed here, and twostate lemma cannot have modifies clause + ensures {:myAttr old(3)} true + decreases {:myAttr old(3)} x // error: old is not allowed here + { + } + + twostate lemma O2Attr(x: int) returns (y: int) + requires {:myAttr x, y} true // error: y is not in scope here + modifies {:myAttr x, y} {} // error (x2): y is not in scope here, and twostate lemma cannot have modifies clause + ensures {:myAttr x, y} true + decreases {:myAttr x, y} x // error: y is not in scope here + { + } + + iterator Iter(x: int) yields (y: int) + requires {:myAttr false + 3} true // error: false + 3 is ill-typed + yield requires {:myAttr false + 3} true // error: false + 3 is ill-typed + modifies {:myAttr false + 3} {} // error: false + 3 is ill-typed + yield ensures {:myAttr false + 3} true // error: false + 3 is ill-typed + ensures {:myAttr false + 3} true // error: false + 3 is ill-typed + decreases {:myAttr false + 3} x // error: false + 3 is ill-typed + { + } + + iterator Jter(x: int) yields (y: int) + requires {:myAttr old(3)} true // error: old is not allowed here + yield requires {:myAttr old(3)} true // error: old is not allowed here + modifies {:myAttr old(3)} {} // error: old is not allowed here + yield ensures {:myAttr old(3)} true + ensures {:myAttr old(3)} true + decreases {:myAttr old(3)} x // error: old is not allowed here + { + } + + iterator Kter(x: int) yields (y: int) + requires {:myAttr x, y, ys} true // error (x2): y and ys are not in scope here + yield requires {:myAttr x, y, ys} true // these are allowed (but it would be weird for anyone to use y and ys here) + modifies {:myAttr x, y, ys} {} // error (x2): y and ys are not in scope here + yield ensures {:myAttr x, y, ys} true + ensures {:myAttr x, y, ys} true + decreases {:myAttr x, y, ys} x // error (x2): y and ys are not in scope here + { + } +} + +module + {:myAttr false + 3} // error: false + 3 is ill-typed + {:myAttr old(3)} // error: old is not allowed here + {:myAttr k} // error: k is not in scope here + Modu +{ } diff --git a/Test/dafny0/AttributeChecks.dfy.expect b/Test/dafny0/AttributeChecks.dfy.expect index cb4ebb222f5..02ee574e9c2 100644 --- a/Test/dafny0/AttributeChecks.dfy.expect +++ b/Test/dafny0/AttributeChecks.dfy.expect @@ -8,6 +8,36 @@ module JustAboutEverything { datatype {:dt 0} {:dt false + 3} AnotherDatatype = {:dt 50} Blue | {:dt k} Green + iterator Iter(x: int) yields (y: int) + requires {:myAttr false + 3} true + modifies {:myAttr false + 3} {} + yield requires {:myAttr false + 3} true + yield ensures {:myAttr false + 3} true + ensures {:myAttr false + 3} true + decreases {:myAttr false + 3} x + { + } + + iterator Jter(x: int) yields (y: int) + requires {:myAttr old(3)} true + modifies {:myAttr old(3)} {} + yield requires {:myAttr old(3)} true + yield ensures {:myAttr old(3)} true + ensures {:myAttr old(3)} true + decreases {:myAttr old(3)} x + { + } + + iterator Kter(x: int) yields (y: int) + requires {:myAttr x, y, ys} true + modifies {:myAttr x, y, ys} {} + yield requires {:myAttr x, y, ys} true + yield ensures {:myAttr x, y, ys} true + ensures {:myAttr x, y, ys} true + decreases {:myAttr x, y, ys} x + { + } + method If(n: int) returns (k: int) { var i := 0; @@ -118,6 +148,105 @@ module JustAboutEverything { } return 2; } + + function FAttr(x: int): int + requires {:myAttr false + 3} true + ensures {:myAttr false + 3} true + decreases {:myAttr false + 3} x + { + 10 + } + + function GAttr(x: int): int + requires {:myAttr old(3)} true + ensures {:myAttr old(3)} true + decreases {:myAttr old(3)} x + { + 10 + } + + function HAttr(x: int): (r: int) + requires {:myAttr x, r} true + ensures {:myAttr x, r} true + decreases {:myAttr x, r} x + { + 10 + } + + twostate function F2Attr(x: int): int + requires {:myAttr false + 3} true + ensures {:myAttr false + 3} true + decreases {:myAttr false + 3} x + { + 10 + } + + twostate function G2Attr(x: int): int + requires {:myAttr old(3)} true + ensures {:myAttr old(3)} true + decreases {:myAttr old(3)} x + { + 10 + } + + twostate function H2Attr(x: int): (r: int) + requires {:myAttr x, r} true + ensures {:myAttr x, r} true + decreases {:myAttr x, r} x + { + 10 + } + + method MAttr(x: int) returns (y: int) + requires {:myAttr false + 3} true + modifies {:myAttr false + 3} {} + ensures {:myAttr false + 3} true + decreases {:myAttr false + 3} x + { + } + + method NAttr(x: int) returns (y: int) + requires {:myAttr old(3)} true + modifies {:myAttr old(3)} {} + ensures {:myAttr old(3)} true + decreases {:myAttr old(3)} x + { + } + + method OAttr(x: int) returns (y: int) + requires {:myAttr x, y} true + modifies {:myAttr x, y} {} + ensures {:myAttr x, y} true + decreases {:myAttr x, y} x + { + } + + twostate lemma M2Attr(x: int) returns (y: int) + requires {:myAttr false + 3} true + modifies {:myAttr false + 3} {} + ensures {:myAttr false + 3} true + decreases {:myAttr false + 3} x + { + } + + twostate lemma N2Attr(x: int) returns (y: int) + requires {:myAttr old(3)} true + modifies {:myAttr old(3)} {} + ensures {:myAttr old(3)} true + decreases {:myAttr old(3)} x + { + } + + twostate lemma O2Attr(x: int) returns (y: int) + requires {:myAttr x, y} true + modifies {:myAttr x, y} {} + ensures {:myAttr x, y} true + decreases {:myAttr x, y} x + { + } +} + +module {:myAttr false + 3} {:myAttr old(3)} {:myAttr k} Modu { } AttributeChecks.dfy(104,9): Error: unresolved identifier: k AttributeChecks.dfy(103,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) @@ -125,6 +254,28 @@ AttributeChecks.dfy(103,30): Error: type of right argument to + (int) must agree AttributeChecks.dfy(107,27): Error: unresolved identifier: k AttributeChecks.dfy(106,30): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) AttributeChecks.dfy(106,30): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(211,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(211,29): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(208,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(208,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(206,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(206,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(207,34): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(207,34): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(209,33): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(209,33): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(210,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(210,27): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(221,23): Error: old expressions are not allowed in this context +AttributeChecks.dfy(218,22): Error: old expressions are not allowed in this context +AttributeChecks.dfy(216,22): Error: old expressions are not allowed in this context +AttributeChecks.dfy(217,28): Error: old expressions are not allowed in this context +AttributeChecks.dfy(231,26): Error: unresolved identifier: y +AttributeChecks.dfy(231,29): Error: unresolved identifier: ys +AttributeChecks.dfy(228,25): Error: unresolved identifier: y +AttributeChecks.dfy(228,28): Error: unresolved identifier: ys +AttributeChecks.dfy(226,25): Error: unresolved identifier: y +AttributeChecks.dfy(226,28): Error: unresolved identifier: ys AttributeChecks.dfy(19,19): Error: type of left argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(19,19): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) AttributeChecks.dfy(29,37): Error: type of right argument to + (int) must agree with the result type (bool) @@ -143,4 +294,57 @@ AttributeChecks.dfy(85,25): Error: type of right argument to + (int) must agree AttributeChecks.dfy(85,25): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) AttributeChecks.dfy(96,32): Error: type of right argument to + (int) must agree with the result type (bool) AttributeChecks.dfy(96,32): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -24 resolution/type errors detected in AttributeChecks.dfy +AttributeChecks.dfy(110,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(110,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(111,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(111,27): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(112,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(112,29): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(118,22): Error: old expressions are not allowed in this context +AttributeChecks.dfy(119,21): Error: old expressions are not allowed in this context +AttributeChecks.dfy(120,23): Error: old expressions are not allowed in this context +AttributeChecks.dfy(126,25): Error: unresolved identifier: r +AttributeChecks.dfy(128,26): Error: unresolved identifier: r +AttributeChecks.dfy(134,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(134,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(135,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(135,27): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(136,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(136,29): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(150,25): Error: unresolved identifier: r +AttributeChecks.dfy(152,26): Error: unresolved identifier: r +AttributeChecks.dfy(158,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(158,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(159,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(159,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(161,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(161,29): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(160,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(160,27): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(166,22): Error: old expressions are not allowed in this context +AttributeChecks.dfy(167,22): Error: old expressions are not allowed in this context +AttributeChecks.dfy(169,23): Error: old expressions are not allowed in this context +AttributeChecks.dfy(174,25): Error: unresolved identifier: y +AttributeChecks.dfy(175,25): Error: unresolved identifier: y +AttributeChecks.dfy(177,26): Error: unresolved identifier: y +AttributeChecks.dfy(183,33): Error: twostate lemmas are not allowed to have modifies clauses +AttributeChecks.dfy(182,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(182,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(183,28): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(183,28): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(185,29): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(185,29): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(184,27): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(184,27): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(191,22): Error: old expressions are not allowed in this context +AttributeChecks.dfy(191,30): Error: twostate lemmas are not allowed to have modifies clauses +AttributeChecks.dfy(193,23): Error: old expressions are not allowed in this context +AttributeChecks.dfy(198,25): Error: unresolved identifier: y +AttributeChecks.dfy(199,25): Error: unresolved identifier: y +AttributeChecks.dfy(199,28): Error: twostate lemmas are not allowed to have modifies clauses +AttributeChecks.dfy(201,26): Error: unresolved identifier: y +AttributeChecks.dfy(239,11): Error: unresolved identifier: k +AttributeChecks.dfy(238,11): Error: old expressions are not allowed in this context +AttributeChecks.dfy(237,17): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(237,17): Error: type of right argument to + (int) must agree with the result type (bool) +99 resolution/type errors detected in AttributeChecks.dfy From 86c4fe605cb7fdd2b5d08437a6046c4d7560a403 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Mar 2022 21:43:50 -0800 Subject: [PATCH 08/14] Add test for attributes of modify statement --- Test/dafny0/AttributeChecks.dfy | 4 ++++ Test/dafny0/AttributeChecks.dfy.expect | 17 ++++++++++++----- 2 files changed, 16 insertions(+), 5 deletions(-) diff --git a/Test/dafny0/AttributeChecks.dfy b/Test/dafny0/AttributeChecks.dfy index 8e0d058b1d9..da68944c00b 100644 --- a/Test/dafny0/AttributeChecks.dfy +++ b/Test/dafny0/AttributeChecks.dfy @@ -231,6 +231,10 @@ module JustAboutEverything { decreases {:myAttr x, y, ys} x // error (x2): y and ys are not in scope here { } + + method ModifyStatement(s: set) { + modify {:myAttr false + 3} s; // error: false + 3 is ill-typed + } } module diff --git a/Test/dafny0/AttributeChecks.dfy.expect b/Test/dafny0/AttributeChecks.dfy.expect index 02ee574e9c2..d89d3ce5ef6 100644 --- a/Test/dafny0/AttributeChecks.dfy.expect +++ b/Test/dafny0/AttributeChecks.dfy.expect @@ -244,6 +244,11 @@ module JustAboutEverything { decreases {:myAttr x, y} x { } + + method ModifyStatement(s: set) + { + modify {:myAttr false + 3} s; + } } module {:myAttr false + 3} {:myAttr old(3)} {:myAttr k} Modu { @@ -343,8 +348,10 @@ AttributeChecks.dfy(198,25): Error: unresolved identifier: y AttributeChecks.dfy(199,25): Error: unresolved identifier: y AttributeChecks.dfy(199,28): Error: twostate lemmas are not allowed to have modifies clauses AttributeChecks.dfy(201,26): Error: unresolved identifier: y -AttributeChecks.dfy(239,11): Error: unresolved identifier: k -AttributeChecks.dfy(238,11): Error: old expressions are not allowed in this context -AttributeChecks.dfy(237,17): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) -AttributeChecks.dfy(237,17): Error: type of right argument to + (int) must agree with the result type (bool) -99 resolution/type errors detected in AttributeChecks.dfy +AttributeChecks.dfy(236,26): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(236,26): Error: type of right argument to + (int) must agree with the result type (bool) +AttributeChecks.dfy(243,11): Error: unresolved identifier: k +AttributeChecks.dfy(242,11): Error: old expressions are not allowed in this context +AttributeChecks.dfy(241,17): Error: type of + must be of a numeric type, a bitvector type, ORDINAL, char, a sequence type, or a set-like or map-like type (instead got bool) +AttributeChecks.dfy(241,17): Error: type of right argument to + (int) must agree with the result type (bool) +101 resolution/type errors detected in AttributeChecks.dfy From 9b3c7af98763cfb9645e993609dcb2dbf2dad61b Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Mar 2022 21:48:21 -0800 Subject: [PATCH 09/14] Update release notes --- RELEASE_NOTES.md | 1 + 1 file changed, 1 insertion(+) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index fa6a819c844..d7371de0619 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -8,6 +8,7 @@ - fix: export-reveals of function-by-method now allows the function body to be ghost (https://github.com/dafny-lang/dafny/pull/1855) - fix: Regain C# 7.3 compatibility of the compiled code. (https://github.com/dafny-lang/dafny/pull/1877) - fix: The error "assertion violation" is replaced by the better wording "assertion might not hold". This indicates better that the verifier is unable to prove the assertion. (https://github.com/dafny-lang/dafny/pull/1862) +- fix: Resolve expressions in attributes in all specifications of functions and iterators. (https://github.com/dafny-lang/dafny/pull/1898) # 3.4.2 From 4d72b2734c592dfaaef18563717066c4486dda43 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 11 Mar 2022 22:15:58 -0800 Subject: [PATCH 10/14] Update PR number in release notes --- RELEASE_NOTES.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index d7371de0619..2cdfa6e51fa 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -8,7 +8,7 @@ - fix: export-reveals of function-by-method now allows the function body to be ghost (https://github.com/dafny-lang/dafny/pull/1855) - fix: Regain C# 7.3 compatibility of the compiled code. (https://github.com/dafny-lang/dafny/pull/1877) - fix: The error "assertion violation" is replaced by the better wording "assertion might not hold". This indicates better that the verifier is unable to prove the assertion. (https://github.com/dafny-lang/dafny/pull/1862) -- fix: Resolve expressions in attributes in all specifications of functions and iterators. (https://github.com/dafny-lang/dafny/pull/1898) +- fix: Resolve expressions in attributes in all specifications of functions and iterators. (https://github.com/dafny-lang/dafny/pull/1900) # 3.4.2 From 7be02be9c915db622f0f216dbc833cbde26d3646 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 14 Mar 2022 14:59:53 -0700 Subject: [PATCH 11/14] Pass in IAttributeBearingDeclaration in one missing place --- Source/Dafny/Resolver.cs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index bda40acdf0b..c81eb5dc489 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -9928,6 +9928,7 @@ void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph invar ConstrainTypeExprBool(inv.E, "invariant is expected to be of type bool, but is {0}"); } - ResolveAttributes(decreases.Attributes, null, new ResolveOpts(codeContext, true)); + ResolveAttributes(decreases.Attributes, decreases, new ResolveOpts(codeContext, true)); foreach (Expression e in decreases.Expressions) { ResolveExpression(e, new ResolveOpts(codeContext, true)); if (e is WildcardExpr && !codeContext.AllowsNontermination) { From 8ef41a43461a53e81c2a31dee3194592c16dd250 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 14 Mar 2022 15:04:35 -0700 Subject: [PATCH 12/14] Add Attributes getter in IAttributeBearingDeclaration --- Source/Dafny/AST/DafnyAst.cs | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Source/Dafny/AST/DafnyAst.cs b/Source/Dafny/AST/DafnyAst.cs index a91f66536c6..27e0f6db150 100644 --- a/Source/Dafny/AST/DafnyAst.cs +++ b/Source/Dafny/AST/DafnyAst.cs @@ -395,6 +395,7 @@ public IEnumerable AllBoundVars { /// A class implementing this interface is one that can carry attributes. /// public interface IAttributeBearingDeclaration { + Attributes Attributes { get; } } public class Attributes { @@ -3459,6 +3460,7 @@ public bool IsExtern(out string/*?*/ qualification, out string/*?*/ name) { return false; } public Attributes Attributes; // readonly, except during class merging in the refinement transformations and when changed by Compiler.MarkCapitalizationConflict + Attributes IAttributeBearingDeclaration.Attributes => Attributes; public Declaration(IToken tok, string name, Attributes attributes, bool isRefining) { Contract.Requires(tok != null); @@ -3965,6 +3967,7 @@ public string FullName { string INamedRegion.Name { get { return Name; } } public ModuleDefinition EnclosingModule; // readonly, except can be changed by resolver for prefix-named modules when the real parent is discovered public readonly Attributes Attributes; + Attributes IAttributeBearingDeclaration.Attributes => Attributes; public ModuleQualifiedId RefinementQId; // full qualified ID of the refinement parent, null if no refinement base public bool SuccessfullyResolved; // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved @@ -7784,6 +7787,7 @@ public class LocalVariable : IVariable, IAttributeBearingDeclaration { public readonly IToken EndTok; // typically a terminating semi-colon or end-curly-brace readonly string name; public Attributes Attributes; + Attributes IAttributeBearingDeclaration.Attributes => Attributes; public bool IsGhost; [ContractInvariantMethod] void ObjectInvariant() { @@ -8048,6 +8052,8 @@ public class GuardedAlternative : IAttributeBearingDeclaration { public readonly Expression Guard; public readonly List Body; public Attributes Attributes; + Attributes IAttributeBearingDeclaration.Attributes => Attributes; + [ContractInvariantMethod] void ObjectInvariant() { Contract.Invariant(Tok != null); @@ -11253,6 +11259,7 @@ public class LetExpr : Expression, IAttributeBearingDeclaration, IBoundVarsBeari public readonly Expression Body; public readonly bool Exact; // Exact==true means a regular let expression; Exact==false means an assign-such-that expression public readonly Attributes Attributes; + Attributes IAttributeBearingDeclaration.Attributes => Attributes; public List Constraint_Bounds; // initialized and filled in by resolver; null for Exact=true and for when expression is in a ghost context // invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count; private Expression translationDesugaring; // filled in during translation, lazily; to be accessed only via Translation.LetDesugaring; always null when Exact==true @@ -11355,6 +11362,7 @@ void ObjectInvariant() { } public Attributes Attributes; + Attributes IAttributeBearingDeclaration.Attributes => Attributes; public abstract class BoundedPool { [Flags] @@ -12481,6 +12489,7 @@ public NestedMatchCase(IToken tok, ExtendedPattern pat) { public class NestedMatchCaseExpr : NestedMatchCase, IAttributeBearingDeclaration { public readonly Expression Body; public Attributes Attributes; + Attributes IAttributeBearingDeclaration.Attributes => Attributes; public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Attributes attrs) : base(tok, pat) { Contract.Requires(body != null); @@ -12492,6 +12501,7 @@ public NestedMatchCaseExpr(IToken tok, ExtendedPattern pat, Expression body, Att public class NestedMatchCaseStmt : NestedMatchCase, IAttributeBearingDeclaration { public readonly List Body; public Attributes Attributes; + Attributes IAttributeBearingDeclaration.Attributes => Attributes; public NestedMatchCaseStmt(IToken tok, ExtendedPattern pat, List body) : base(tok, pat) { Contract.Requires(body != null); this.Body = body; From a7cea9f46a0927fed8d49b804508912889f7f10c Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 14 Mar 2022 15:14:05 -0700 Subject: [PATCH 13/14] Remove redundant parameter to ResolveAttributes --- Source/Dafny/Resolver.cs | 84 ++++++++++++++++++++-------------------- 1 file changed, 42 insertions(+), 42 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index c81eb5dc489..e049cc38b0a 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1016,9 +1016,7 @@ private bool ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, bo int prevErrorCount = reporter.Count(ErrorLevel.Error); ResolveTopLevelDecls_Signatures(m, sig, m.TopLevelDecls, datatypeDependencies, codatatypeDependencies); Contract.Assert(AllTypeConstraints.Count == 0); // signature resolution does not add any type constraints - ResolveAttributes(m.Attributes, m, - new ResolveOpts(new NoContext(m.EnclosingModule), - false)); // Must follow ResolveTopLevelDecls_Signatures, in case attributes refer to members + ResolveAttributes(m, new ResolveOpts(new NoContext(m.EnclosingModule), false)); // Must follow ResolveTopLevelDecls_Signatures, in case attributes refer to members SolveAllTypeConstraints(); // solve any type constraints entailed by the attributes if (reporter.Count(ErrorLevel.Error) == prevErrorCount) { ResolveTopLevelDecls_Core(m.TopLevelDecls, datatypeDependencies, codatatypeDependencies, isAnExport); @@ -2658,7 +2656,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, TopLevelDecl d = topd is ClassDecl ? ((ClassDecl)topd).NonNullTypeDecl : topd; if (d is NewtypeDecl) { var dd = (NewtypeDecl)d; - ResolveAttributes(d.Attributes, d, new ResolveOpts(new NoContext(d.EnclosingModuleDefinition), false)); + ResolveAttributes(d, new ResolveOpts(new NoContext(d.EnclosingModuleDefinition), false)); // this check can be done only after it has been determined that the redirected types do not involve cycles AddXConstraint(dd.tok, "NumericType", dd.BaseType, "newtypes must be based on some numeric type (got {0})"); // type check the constraint, if any @@ -2686,7 +2684,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, allTypeParameters.PushMarker(); ResolveTypeParameters(d.TypeArgs, false, d); - ResolveAttributes(d.Attributes, d, new ResolveOpts(new NoContext(d.EnclosingModuleDefinition), false)); + ResolveAttributes(d, new ResolveOpts(new NoContext(d.EnclosingModuleDefinition), false)); // type check the constraint Contract.Assert(object.ReferenceEquals(dd.Var.Type, dd.Rhs)); // follows from SubsetTypeDecl invariant Contract.Assert(dd.Constraint != null); // follows from SubsetTypeDecl invariant @@ -2714,7 +2712,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, if (member is ConstantField) { var field = (ConstantField)member; var opts = new ResolveOpts(field, false); - ResolveAttributes(field.Attributes, field, opts); + ResolveAttributes(field, opts); // Resolve the value expression if (field.Rhs != null) { var ec = reporter.Count(ErrorLevel.Error); @@ -2782,7 +2780,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, } else { if (!(d is IteratorDecl)) { // Note, attributes of iterators are resolved by ResolvedIterator, after registering any names in the iterator signature - ResolveAttributes(d.Attributes, d, new ResolveOpts(new NoContext(d.EnclosingModuleDefinition), false)); + ResolveAttributes(d, new ResolveOpts(new NoContext(d.EnclosingModuleDefinition), false)); } if (d is IteratorDecl) { var iter = (IteratorDecl)d; @@ -2791,7 +2789,7 @@ public void ResolveTopLevelDecls_Core(List/*!*/ declarations, } else if (d is DatatypeDecl) { var dt = (DatatypeDecl)d; foreach (var ctor in dt.Ctors) { - ResolveAttributes(ctor.Attributes, ctor, new ResolveOpts(new NoContext(d.EnclosingModuleDefinition), false)); + ResolveAttributes(ctor, new ResolveOpts(new NoContext(d.EnclosingModuleDefinition), false)); foreach (var formal in ctor.Formals) { AddTypeDependencyEdges((ICallable)d, formal.Type); } @@ -9550,7 +9548,7 @@ void ResolveClassMemberBodies(TopLevelDeclWithMembers cl) { // don't do anything here, because const fields have already been resolved } else if (member is Field) { var opts = new ResolveOpts(new NoContext(currentClass.EnclosingModuleDefinition), false); - ResolveAttributes(member.Attributes, member, opts); + ResolveAttributes(member, opts); } else if (member is Function) { var f = (Function)member; var ec = reporter.Count(ErrorLevel.Error); @@ -9926,9 +9924,11 @@ void DetermineEqualitySupport(IndDatatypeDecl startingPoint, Graph fields were only given type proxies before; we'll know // the types only after resolving the decreases clause (and it may be that some of resolution has already seen uses of // these fields; so, with no further ado, here we go - ResolveAttributes(iter.Decreases.Attributes, iter.Decreases, new ResolveOpts(iter, false)); + ResolveAttributes(iter.Decreases, new ResolveOpts(iter, false)); Contract.Assert(iter.Decreases.Expressions.Count == iter.DecreasesFields.Count); for (int i = 0; i < iter.Decreases.Expressions.Count; i++) { var e = iter.Decreases.Expressions[i]; @@ -10456,12 +10456,12 @@ void ResolveIterator(IteratorDecl iter) { foreach (FrameExpression fe in iter.Reads.Expressions) { ResolveFrameExpression(fe, FrameExpressionUse.Reads, iter); } - ResolveAttributes(iter.Modifies.Attributes, iter.Modifies, new ResolveOpts(iter, false)); + ResolveAttributes(iter.Modifies, new ResolveOpts(iter, false)); foreach (FrameExpression fe in iter.Modifies.Expressions) { ResolveFrameExpression(fe, FrameExpressionUse.Modifies, iter); } foreach (AttributedExpression e in iter.Requires) { - ResolveAttributes(e.Attributes, e, new ResolveOpts(iter, false)); + ResolveAttributes(e, new ResolveOpts(iter, false)); ResolveExpression(e.E, new ResolveOpts(iter, false)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Precondition must be a boolean (got {0})"); @@ -10476,26 +10476,26 @@ void ResolveIterator(IteratorDecl iter) { Contract.Assert(scope.AllowInstance); foreach (AttributedExpression e in iter.YieldRequires) { - ResolveAttributes(e.Attributes, e, new ResolveOpts(iter, false)); + ResolveAttributes(e, new ResolveOpts(iter, false)); ResolveExpression(e.E, new ResolveOpts(iter, false)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Yield precondition must be a boolean (got {0})"); } foreach (AttributedExpression e in iter.YieldEnsures) { - ResolveAttributes(e.Attributes, e, new ResolveOpts(iter, true)); + ResolveAttributes(e, new ResolveOpts(iter, true)); ResolveExpression(e.E, new ResolveOpts(iter, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Yield postcondition must be a boolean (got {0})"); } foreach (AttributedExpression e in iter.Ensures) { - ResolveAttributes(e.Attributes, e, new ResolveOpts(iter, true)); + ResolveAttributes(e, new ResolveOpts(iter, true)); ResolveExpression(e.E, new ResolveOpts(iter, true)); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression ConstrainTypeExprBool(e.E, "Postcondition must be a boolean (got {0})"); } SolveAllTypeConstraints(); - ResolveAttributes(iter.Attributes, iter, new ResolveOpts(iter, false)); + ResolveAttributes(iter, new ResolveOpts(iter, false)); var postSpecErrorCount = reporter.Count(ErrorLevel.Error); @@ -10983,7 +10983,7 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) { Contract.Requires(stmt != null); Contract.Requires(codeContext != null); if (!(stmt is ForallStmt || stmt is ForLoopStmt)) { // "forall" and "for" statements do their own attribute resolution below - ResolveAttributes(stmt.Attributes, stmt, new ResolveOpts(codeContext, true)); + ResolveAttributes(stmt, new ResolveOpts(codeContext, true)); } if (stmt is PredicateStmt) { PredicateStmt s = (PredicateStmt)stmt; @@ -11197,7 +11197,7 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) { } // With the new locals in scope, it's now time to resolve the attributes on all the locals foreach (var local in s.Locals) { - ResolveAttributes(local.Attributes, local, new ResolveOpts(codeContext, true)); + ResolveAttributes(local, new ResolveOpts(codeContext, true)); } // Resolve the AssignSuchThatStmt, if any if (s.Update is AssignSuchThatStmt) { @@ -11382,7 +11382,7 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) { // Create a new scope, add the local to the scope, and resolve the attributes scope.PushMarker(); ScopePushAndReport(scope, loopIndex, "index-variable"); - ResolveAttributes(s.Attributes, s, new ResolveOpts(codeContext, true)); + ResolveAttributes(s, new ResolveOpts(codeContext, true)); } ResolveLoopSpecificationComponents(s.Invariants, s.Decreases, s.Mod, codeContext, fvs, ref usesHeap); @@ -11438,7 +11438,7 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) { } // Since the range and postconditions are more likely to infer the types of the bound variables, resolve them // first (above) and only then resolve the attributes (below). - ResolveAttributes(s.Attributes, s, new ResolveOpts(codeContext, true)); + ResolveAttributes(s, new ResolveOpts(codeContext, true)); if (s.Body != null) { // clear the labels for the duration of checking the body, because break statements are not allowed to leave a forall statement @@ -11512,7 +11512,7 @@ public void ResolveStatement(Statement stmt, ICodeContext codeContext) { } else if (stmt is ModifyStmt) { var s = (ModifyStmt)stmt; - ResolveAttributes(s.Mod.Attributes, s.Mod, new ResolveOpts(codeContext, true)); + ResolveAttributes(s.Mod, new ResolveOpts(codeContext, true)); foreach (FrameExpression fe in s.Mod.Expressions) { ResolveFrameExpression(fe, FrameExpressionUse.Modifies, codeContext); } @@ -11626,7 +11626,7 @@ private void ResolveLoopSpecificationComponents(List invar Contract.Requires(codeContext != null); foreach (AttributedExpression inv in invariants) { - ResolveAttributes(inv.Attributes, inv, new ResolveOpts(codeContext, true)); + ResolveAttributes(inv, new ResolveOpts(codeContext, true)); ResolveExpression(inv.E, new ResolveOpts(codeContext, true)); Contract.Assert(inv.E.Type != null); // follows from postcondition of ResolveExpression if (fvs != null) { @@ -11635,7 +11635,7 @@ private void ResolveLoopSpecificationComponents(List invar ConstrainTypeExprBool(inv.E, "invariant is expected to be of type bool, but is {0}"); } - ResolveAttributes(decreases.Attributes, decreases, new ResolveOpts(codeContext, true)); + ResolveAttributes(decreases, new ResolveOpts(codeContext, true)); foreach (Expression e in decreases.Expressions) { ResolveExpression(e, new ResolveOpts(codeContext, true)); if (e is WildcardExpr && !codeContext.AllowsNontermination) { @@ -11647,7 +11647,7 @@ private void ResolveLoopSpecificationComponents(List invar // any type is fine } - ResolveAttributes(modifies.Attributes, modifies, new ResolveOpts(codeContext, true)); + ResolveAttributes(modifies, new ResolveOpts(codeContext, true)); if (modifies.Expressions != null) { usesHeap = true; // bearing a modifies clause counts as using the heap foreach (FrameExpression fe in modifies.Expressions) { @@ -12731,7 +12731,7 @@ private void CheckLinearNestedMatchCase(Type type, NestedMatchCase mc, ResolveOp private void CheckLinearNestedMatchExpr(Type dtd, NestedMatchExpr me, ResolveOpts opts) { foreach (NestedMatchCaseExpr mc in me.Cases) { scope.PushMarker(); - ResolveAttributes(mc.Attributes, mc, opts); + ResolveAttributes(mc, opts); CheckLinearNestedMatchCase(dtd, mc, opts); scope.PopMarker(); } @@ -12740,7 +12740,7 @@ private void CheckLinearNestedMatchExpr(Type dtd, NestedMatchExpr me, ResolveOpt private void CheckLinearNestedMatchStmt(Type dtd, NestedMatchStmt ms, ResolveOpts opts) { foreach (NestedMatchCaseStmt mc in ms.Cases) { scope.PushMarker(); - ResolveAttributes(mc.Attributes, mc, opts); + ResolveAttributes(mc, opts); CheckLinearNestedMatchCase(dtd, mc, opts); scope.PopMarker(); } @@ -12936,7 +12936,7 @@ private void ResolveConcreteUpdateStmt(ConcreteUpdateStatement s, ICodeContext c } else { Contract.Assert(false); throw new cce.UnreachableException(); } - ResolveAttributes(s.Attributes, s, new ResolveOpts(codeContext, true)); + ResolveAttributes(s, new ResolveOpts(codeContext, true)); } /// /// Resolve the RHSs and entire UpdateStmt (LHSs should already have been checked by the caller). @@ -13390,7 +13390,7 @@ void ResolveAlternatives(List alternatives, AlternativeLoopS ScopePushAndReport(scope, v, "bound-variable"); } } - ResolveAttributes(alternative.Attributes, alternative, new ResolveOpts(codeContext, true)); + ResolveAttributes(alternative, new ResolveOpts(codeContext, true)); foreach (Statement ss in alternative.Body) { ResolveStatementWithLabels(ss, codeContext); } @@ -15168,7 +15168,7 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { } } ResolveExpression(e.Body, opts); - ResolveAttributes(e.Attributes, e, opts); + ResolveAttributes(e, opts); scope.PopMarker(); expr.Type = e.Body.Type; } else if (expr is LetOrFailExpr) { @@ -15204,7 +15204,7 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { ConstrainTypeExprBool(e.Term, "body of quantifier must be of type bool (instead got {0})"); // Since the body is more likely to infer the types of the bound variables, resolve it // first (above) and only then resolve the attributes (below). - ResolveAttributes(e.Attributes, e, opts); + ResolveAttributes(e, opts); scope.PopMarker(); allTypeParameters.PopMarker(); expr.Type = Type.Bool; @@ -15227,7 +15227,7 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { ResolveExpression(e.Term, opts); Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression - ResolveAttributes(e.Attributes, e, opts); + ResolveAttributes(e, opts); scope.PopMarker(); expr.Type = new SetType(e.Finite, e.Term.Type); @@ -15254,7 +15254,7 @@ public void ResolveExpressionX(Expression expr, ResolveOpts opts) { ResolveExpression(e.Term, opts); Contract.Assert(e.Term.Type != null); // follows from postcondition of ResolveExpression - ResolveAttributes(e.Attributes, e, opts); + ResolveAttributes(e, opts); scope.PopMarker(); expr.Type = new MapType(e.Finite, e.TermLeft != null ? e.TermLeft.Type : e.BoundVars[0].Type, e.Term.Type); From 257090bfa4c3e1675724b124d2aa94c05e248e1c Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Mon, 14 Mar 2022 15:24:11 -0700 Subject: [PATCH 14/14] chore: Simplify code --- Source/Dafny/Resolver.cs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 6d89fbec6e5..7058d28004a 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -9928,10 +9928,9 @@ void ResolveAttributes(IAttributeBearingDeclaration attributeHost, ResolveOpts o Contract.Requires(opts != null); Contract.Requires(attributeHost != null); - var attrs = attributeHost.Attributes; // order does not matter much for resolution, so resolve them in reverse order - foreach (var attr in attrs.AsEnumerable()) { - if (attributeHost != null && attr is UserSuppliedAttributes) { + foreach (var attr in attributeHost.Attributes.AsEnumerable()) { + if (attr is UserSuppliedAttributes) { var usa = (UserSuppliedAttributes)attr; usa.Recognized = IsRecognizedAttribute(usa, attributeHost); }