feat: Read clauses on methods (#4440)

Implements dafny-lang/rfcs#6.

This functionality is guarded by a new `--reads-clauses-on-methods`
option, even though it's almost completely backwards compatible: the
only wrinkle is function-by-methods, where valid code today might be
rejected when the reads clause of the function definition is applied to
the by-method body.

Note that "methods" here is interpreted as it is in the Dafny reference
manual and similar documentation: it includes constructors and ghost
methods, but NOT lemmas.

The `{:concurrent}` attribute, which previously only existed to generate
an auditor warning that Dafny could not verify this property, now
creates assertions that the `reads` and `modifies` clauses on the
function or method are empty.

The core implementation strategy is relatively straightforward: enabling
reads checks (via the `WFOptions` value) in the well-formedness check
for statements as well as expressions. The existing `$_Frame` variable
is now split into `$_ReadsFrame` and `$_ModifiesFrame`, since we now
need both at once in method contexts. To help make reads checks optional
based on the new option, and to optimize by not enabling them when in a
`reads *` context (the default for methods), the
`ExpressionTranslator.readsFrame` field may be null. I performed some
mild refactoring to make this cleaner but open to suggestion on further
improvements.

Documentation changes preview at https://robin-aws.github.io/dafny/.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore.Test/ClonerTest.cs

@@ -31,7 +31,7 @@ public void ClonerKeepsBodyStartTok() {
     var dummyDecl = new Method(rangeToken, new Name(rangeToken, "hello"),
       false, false, new List<TypeParameter>(), new List<Formal> { formal1, formal2 },
       new List<Formal>(), new List<AttributedExpression>(),
-      new Specification<FrameExpression>(new List<FrameExpression>(), null),
+      new List<FrameExpression>(), new Specification<FrameExpression>(new List<FrameExpression>(), null),
       new List<AttributedExpression>(), new Specification<Expression>(new List<Expression>(), null),
       new BlockStmt(rangeToken, new List<Statement>()), null, Token.NoToken, false);
 

Source/DafnyCore/AST/AstVisitor.cs

@@ -173,6 +173,8 @@ public virtual void VisitMethod(Method method) {
 
       method.Req.ForEach(aexpr => VisitAttributedExpression(aexpr, context));
 
+      method.Reads.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));
+
       VisitAttributes(method.Mod, method.EnclosingClass.EnclosingModuleDefinition);
       method.Mod.Expressions.ForEach(frameExpression => VisitTopLevelFrameExpression(frameExpression, context));
 

Source/DafnyCore/AST/BottomUpVisitor.cs

@@ -56,6 +56,7 @@ public void Visit(NewtypeDecl ntd) {
   }
   public void Visit(Method method) {
     Visit(method.Req);
+    Visit(method.Reads);
     Visit(method.Mod.Expressions);
     Visit(method.Ens);
     Visit(method.Decreases.Expressions);

Source/DafnyCore/AST/Members/Constructor.cs

@@ -37,12 +37,14 @@ public Constructor(RangeToken rangeToken, Name name,
     bool isGhost,
     List<TypeParameter> typeArgs,
     List<Formal> ins,
-    List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
+    List<AttributedExpression> req,
+    List<FrameExpression> reads,
+    [Captured] Specification<FrameExpression> mod,
     List<AttributedExpression> ens,
     Specification<Expression> decreases,
     DividedBlockStmt body,
     Attributes attributes, IToken signatureEllipsis)
-    : base(rangeToken, name, false, isGhost, typeArgs, ins, new List<Formal>(), req, mod, ens, decreases, body, attributes, signatureEllipsis) {
+    : base(rangeToken, name, false, isGhost, typeArgs, ins, new List<Formal>(), req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(cce.NonNullElements(typeArgs));

Source/DafnyCore/AST/Members/ExtremeLemma.cs

@@ -22,12 +22,14 @@ public ExtremeLemma(RangeToken rangeToken, Name name,
     bool hasStaticKeyword, ExtremePredicate.KType typeOfK,
     List<TypeParameter> typeArgs,
     List<Formal> ins, [Captured] List<Formal> outs,
-    List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
+    List<AttributedExpression> req,
+    List<FrameExpression> reads,
+    [Captured] Specification<FrameExpression> mod,
     List<AttributedExpression> ens,
     Specification<Expression> decreases,
     BlockStmt body,
     Attributes attributes, IToken signatureEllipsis)
-    : base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
+    : base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(cce.NonNullElements(typeArgs));
@@ -50,12 +52,14 @@ public LeastLemma(RangeToken rangeToken, Name name,
     bool hasStaticKeyword, ExtremePredicate.KType typeOfK,
     List<TypeParameter> typeArgs,
     List<Formal> ins, [Captured] List<Formal> outs,
-    List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
+    List<AttributedExpression> req,
+    List<FrameExpression> reads,
+    [Captured] Specification<FrameExpression> mod,
     List<AttributedExpression> ens,
     Specification<Expression> decreases,
     BlockStmt body,
     Attributes attributes, IToken signatureEllipsis)
-    : base(rangeToken, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
+    : base(rangeToken, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(cce.NonNullElements(typeArgs));
@@ -78,12 +82,14 @@ public GreatestLemma(RangeToken rangeToken, Name name,
     bool hasStaticKeyword, ExtremePredicate.KType typeOfK,
     List<TypeParameter> typeArgs,
     List<Formal> ins, [Captured] List<Formal> outs,
-    List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
+    List<AttributedExpression> req,
+    List<FrameExpression> reads,
+    [Captured] Specification<FrameExpression> mod,
     List<AttributedExpression> ens,
     Specification<Expression> decreases,
     BlockStmt body,
     Attributes attributes, IToken signatureEllipsis)
-    : base(rangeToken, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
+    : base(rangeToken, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(cce.NonNullElements(typeArgs));

Source/DafnyCore/AST/Members/Function.cs

@@ -52,10 +52,6 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
       yield return new Assumption(this, tok, AssumptionDescription.NoBody(IsGhost));
     }
 
-    if (Body is not null && HasConcurrentAttribute) {
-      yield return new Assumption(this, tok, AssumptionDescription.HasConcurrentAttribute);
-    }
-
     if (HasExternAttribute) {
       yield return new Assumption(this, tok, AssumptionDescription.ExternFunction);
       if (HasPostcondition && !HasAxiomAttribute) {

Source/DafnyCore/AST/Members/Lemma.cs

@@ -10,12 +10,14 @@ public Lemma(RangeToken rangeToken, Name name,
     bool hasStaticKeyword,
     [Captured] List<TypeParameter> typeArgs,
     [Captured] List<Formal> ins, [Captured] List<Formal> outs,
-    [Captured] List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
+    [Captured] List<AttributedExpression> req,
+    [Captured] List<FrameExpression> reads,
+    [Captured] Specification<FrameExpression> mod,
     [Captured] List<AttributedExpression> ens,
     [Captured] Specification<Expression> decreases,
     [Captured] BlockStmt body,
     Attributes attributes, IToken signatureEllipsis)
-    : base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
+    : base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
   }
 
   public Lemma(Cloner cloner, Lemma lemma) : base(cloner, lemma) {
@@ -33,12 +35,13 @@ public TwoStateLemma(RangeToken rangeToken, Name name,
     [Captured] List<TypeParameter> typeArgs,
     [Captured] List<Formal> ins, [Captured] List<Formal> outs,
     [Captured] List<AttributedExpression> req,
+    [Captured] List<FrameExpression> reads,
     [Captured] Specification<FrameExpression> mod,
     [Captured] List<AttributedExpression> ens,
     [Captured] Specification<Expression> decreases,
     [Captured] BlockStmt body,
     Attributes attributes, IToken signatureEllipsis)
-    : base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
+    : base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
     Contract.Requires(rangeToken != null);
     Contract.Requires(name != null);
     Contract.Requires(typeArgs != null);

Source/DafnyCore/AST/Members/Method.cs

@@ -5,11 +5,10 @@
 
 namespace Microsoft.Dafny;
 
-public class Method : MemberDecl, TypeParameter.ParentType,
-  IMethodCodeContext, ICanFormat, IHasDocstring, IHasSymbolChildren, ICanVerify {
+public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext, ICanFormat, IHasDocstring, IHasSymbolChildren, ICanVerify {
   public override IEnumerable<INode> Children => new Node[] { Body, Decreases }.Where(x => x != null).
     Concat(Ins).Concat(Outs).Concat<Node>(TypeArgs).
-    Concat(Req).Concat(Ens).Concat(Mod.Expressions);
+    Concat(Req).Concat(Ens).Concat(Reads).Concat(Mod.Expressions);
   public override IEnumerable<INode> PreResolveChildren => Children;
 
   public override string WhatKind => "method";
@@ -22,6 +21,7 @@ public class Method : MemberDecl, TypeParameter.ParentType,
   public readonly List<Formal> Ins;
   public readonly List<Formal> Outs;
   public readonly List<AttributedExpression> Req;
+  public readonly List<FrameExpression> Reads;
   public readonly Specification<FrameExpression> Mod;
   public readonly List<AttributedExpression> Ens;
   public readonly Specification<Expression> Decreases;
@@ -48,10 +48,6 @@ public override IEnumerable<Assumption> Assumptions(Declaration decl) {
       yield return new Assumption(this, tok, AssumptionDescription.NoBody(IsGhost));
     }
 
-    if (Body is not null && HasConcurrentAttribute) {
-      yield return new Assumption(this, tok, AssumptionDescription.HasConcurrentAttribute);
-    }
-
     if (HasExternAttribute && HasPostcondition && !HasAxiomAttribute) {
       yield return new Assumption(this, tok, AssumptionDescription.ExternWithPostcondition);
     }
@@ -79,6 +75,9 @@ public override IEnumerable<Expression> SubExpressions {
       foreach (var e in Req) {
         yield return e.E;
       }
+      foreach (var e in Reads) {
+        yield return e.E;
+      }
       foreach (var e in Mod.Expressions) {
         yield return e.E;
       }
@@ -97,6 +96,7 @@ void ObjectInvariant() {
     Contract.Invariant(cce.NonNullElements(Ins));
     Contract.Invariant(cce.NonNullElements(Outs));
     Contract.Invariant(cce.NonNullElements(Req));
+    Contract.Invariant(cce.NonNullElements(Reads));
     Contract.Invariant(Mod != null);
     Contract.Invariant(cce.NonNullElements(Ens));
     Contract.Invariant(Decreases != null);
@@ -110,6 +110,7 @@ public Method(Cloner cloner, Method original) : base(cloner, original) {
     }
 
     this.Req = original.Req.ConvertAll(cloner.CloneAttributedExpr);
+    this.Reads = original.Reads.ConvertAll(cloner.CloneFrameExpr);
     this.Mod = cloner.CloneSpecFrameExpr(original.Mod);
     this.Decreases = cloner.CloneSpecExpr(original.Decreases);
     this.Ens = original.Ens.ConvertAll(cloner.CloneAttributedExpr);
@@ -122,7 +123,9 @@ public Method(RangeToken rangeToken, Name name,
     bool hasStaticKeyword, bool isGhost,
     [Captured] List<TypeParameter> typeArgs,
     [Captured] List<Formal> ins, [Captured] List<Formal> outs,
-    [Captured] List<AttributedExpression> req, [Captured] Specification<FrameExpression> mod,
+    [Captured] List<AttributedExpression> req,
+    [Captured] List<FrameExpression> reads,
+    [Captured] Specification<FrameExpression> mod,
     [Captured] List<AttributedExpression> ens,
     [Captured] Specification<Expression> decreases,
     [Captured] BlockStmt body,
@@ -134,12 +137,14 @@ public Method(RangeToken rangeToken, Name name,
     Contract.Requires(cce.NonNullElements(ins));
     Contract.Requires(cce.NonNullElements(outs));
     Contract.Requires(cce.NonNullElements(req));
+    Contract.Requires(reads != null);
     Contract.Requires(mod != null);
     Contract.Requires(cce.NonNullElements(ens));
     Contract.Requires(decreases != null);
     this.TypeArgs = typeArgs;
     this.Ins = ins;
     this.Outs = outs;
+    this.Reads = reads;
     this.Req = req;
     this.Mod = mod;
     this.Ens = ens;
@@ -213,6 +218,10 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
       formatter.SetAttributedExpressionIndentation(req, indentBefore + formatter.SpaceTab);
     }
 
+    foreach (var read in Reads) {
+      formatter.SetFrameExpressionIndentation(read, indentBefore + formatter.SpaceTab);
+    }
+
     foreach (var mod in Mod.Expressions) {
       formatter.SetFrameExpressionIndentation(mod, indentBefore + formatter.SpaceTab);
     }
@@ -270,6 +279,27 @@ public void Resolve(ModuleResolver resolver) {
         resolver.ConstrainTypeExprBool(e.E, "Precondition must be a boolean (got {0})");
       }
 
+      var readsClausesOnMethodsEnabled = resolver.Options.Get(CommonOptionBag.ReadsClausesOnMethods);
+      // Set the default of `reads *` if reads clauses on methods is enabled and this isn't a lemma.
+      // Doing it before resolution is a bit easier than adding resolved frame expressions afterwards.
+      // Note that `reads *` is the right default for backwards-compatibility,
+      // but we may want to infer a sensible default like decreases clauses instead in the future.
+      if (readsClausesOnMethodsEnabled && !IsLemmaLike && !Reads.Any()) {
+        Reads.Add(new FrameExpression(tok, new WildcardExpr(tok), null));
+      }
+      foreach (FrameExpression fe in Reads) {
+        resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Reads, this);
+        if (IsLemmaLike) {
+          resolver.reporter.Error(MessageSource.Resolver, fe.tok, "{0}s are not allowed to have reads clauses (they are allowed to read all memory locations)",
+            WhatKind);
+        } else if (!readsClausesOnMethodsEnabled) {
+          resolver.reporter.Error(MessageSource.Resolver, fe.tok,
+            "reads clauses on methods are forbidden without the command-line flag `--reads-clauses-on-methods`");
+        } else if (IsGhost) {
+          resolver.DisallowNonGhostFieldSpecifiers(fe);
+        }
+      }
+
       resolver.ResolveAttributes(Mod, new ResolutionContext(this, false));
       foreach (FrameExpression fe in Mod.Expressions) {
         resolver.ResolveFrameExpressionTopLevel(fe, FrameExpressionUse.Modifies, this);

Source/DafnyCore/AST/Members/PrefixLemma.cs

@@ -14,9 +14,10 @@ public class PrefixLemma : Method {
   public readonly ExtremeLemma ExtremeLemma;
   public PrefixLemma(RangeToken rangeToken, Name name, bool hasStaticKeyword,
     List<TypeParameter> typeArgs, Formal k, List<Formal> ins, List<Formal> outs,
-    List<AttributedExpression> req, Specification<FrameExpression> mod, List<AttributedExpression> ens, Specification<Expression> decreases,
+    List<AttributedExpression> req, [Captured] List<FrameExpression> reads,
+    Specification<FrameExpression> mod, List<AttributedExpression> ens, Specification<Expression> decreases,
     BlockStmt body, Attributes attributes, ExtremeLemma extremeLemma)
-    : base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, null) {
+    : base(rangeToken, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, null) {
     Contract.Requires(k != null);
     Contract.Requires(ins != null && 1 <= ins.Count && ins[0] == k);
     Contract.Requires(extremeLemma != null);

Source/DafnyCore/AST/TopDownVisitor.cs

@@ -68,6 +68,7 @@ public void Visit(ICallable decl, State st) {
   public virtual void Visit(Method method, State st) {
     Visit(method.Ens, st);
     Visit(method.Req, st);
+    Visit(method.Reads, st);
     Visit(method.Mod.Expressions, st);
     Visit(method.Decreases.Expressions, st);
     if (method.Body != null) { Visit(method.Body, st); }

Source/DafnyCore/AST/TypeDeclarations/IteratorDecl.cs

@@ -421,6 +421,7 @@ public void Resolve(ModuleResolver resolver) {
     var init = new Constructor(rangeToken, new Name(NameNode.RangeToken, "_ctor"), false,
       new List<TypeParameter>(), Ins,
       new List<AttributedExpression>(),
+      new List<FrameExpression>(),
       new Specification<FrameExpression>(new List<FrameExpression>(), null),
       new List<AttributedExpression>(),
       new Specification<Expression>(new List<Expression>(), null),
@@ -440,6 +441,7 @@ public void Resolve(ModuleResolver resolver) {
       new List<TypeParameter>(),
       new List<Formal>(), new List<Formal>() { new Formal(tok, "more", Type.Bool, false, false, null) },
       new List<AttributedExpression>(),
+      new List<FrameExpression>(),
       new Specification<FrameExpression>(new List<FrameExpression>(), null),
       new List<AttributedExpression>(),
       new Specification<Expression>(new List<Expression>(), null),

Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs

@@ -245,7 +245,8 @@ public void RegisterMembers(ModuleResolver resolver, Dictionary<string, MemberDe
               : extremeLemma.Ens.ConvertAll(cloner.CloneAttributedExpr);
             extremeLemma.PrefixLemma = new PrefixLemma(extremeLemma.RangeToken, extraName, extremeLemma.HasStaticKeyword,
               extremeLemma.TypeArgs.ConvertAll(cloner.CloneTypeParam), k, formals, extremeLemma.Outs.ConvertAll(f => cloner.CloneFormal(f, false)),
-              req, cloner.CloneSpecFrameExpr(extremeLemma.Mod), ens,
+              req, extremeLemma.Reads.ConvertAll(cloner.CloneFrameExpr),
+              cloner.CloneSpecFrameExpr(extremeLemma.Mod), ens,
               new Specification<Expression>(decr, null),
               null, // Note, the body for the prefix method will be created once the call graph has been computed and the SCC for the greatest lemma is known
               cloner.CloneAttributes(extremeLemma.Attributes), extremeLemma);
@@ -255,7 +256,7 @@ public void RegisterMembers(ModuleResolver resolver, Dictionary<string, MemberDe
           extraMember.InheritVisibility(m, false);
           members.Add(extraName.Value, extraMember);
         } else if (m is Function f && f.ByMethodBody != null) {
-          ModuleResolver.RegisterByMethod(f, this);
+          resolver.RegisterByMethod(f, this);
         }
       } else if (m is Constructor && !((Constructor)m).HasName) {
         resolver.reporter.Error(MessageSource.Resolver, m, "More than one anonymous constructor");