feat: Read clauses on methods #4440

robin-aws · 2023-08-18T18:13:44Z

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/.

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

…d-clauses-on-methods # Conflicts: # Source/Dafny/AST/DafnyAst.cs # Source/Dafny/Cloner.cs # Source/Dafny/Resolver.cs # Source/Dafny/Rewriter.cs # Source/Dafny/Verifier/Translator.ExpressionTranslator.cs # Source/DafnyCore/Dafny.atg # Source/DafnyCore/Rewriters/RefinementTransformer.cs # Source/DafnyCore/Verifier/Translator.TrStatement.cs # Source/DafnyCore/Verifier/Translator.cs

…rames

…d-clauses-on-methods # Conflicts: # Source/DafnyCore/AST/Members/Method.cs # Source/DafnyCore/Resolver/ModuleResolver.cs # Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs

keyboardDrummer

~~Whoa, so few changes are needed. Nice!~~

keyboardDrummer · 2023-08-28T11:00:05Z

Source/DafnyCore/AST/Members/Method.cs

@@ -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;


Seems to be some duplication between Function and Method that this PR increases, that we could reduce some time.

Agreed, but I couldn't see an easy way without a fair bit of refactoring.

keyboardDrummer · 2023-08-28T11:03:41Z

Source/DafnyCore/DafnyOptions.cs

+
+      RegisterLegacyUi(CommonOptionBag.ReadsClausesOnMethods, ParseBoolean, "Language feature selection", "readsClausesOnMethods", @"
+0 (default) - Reads clauses on methods are forbidden.
+1 - Reads clauses on methods are permitted.".TrimStart(), defaultValue: false);


This is good, but it might be nice to also mention the reads * default, since the value/verbosity ratio is high.

Yes I agree on that

Good call, I added this to the new CLI help string too.

keyboardDrummer · 2023-08-28T11:07:27Z

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -792,9 +792,25 @@ public partial class ModuleResolver {
        new ActualBindings(f.Formals.ConvertAll(Expression.CreateIdentExpr)).ArgumentBindings,
        tok);
      var post = new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq, r, fn));
+      List<FrameExpression> reads;
+      if (Options.Get(CommonOptionBag.ReadsClausesOnMethods)) {


I think this code becomes obsolete by assigning the default reads * during parsing

That would make it hard/impossible to reject explicit reads clauses if the option is not turned on though, since you couldn't distinguish between code that explicitly includes reads *.

Wouldn't you reject that code as part of parsing as well ?

On revisiting this, yes, I think I could have assigned the default during parsing instead (with the same conditionals to avoiding doing that on lemmas etc.) I was wary of that at the time since I didn't see any other examples of adding default elements at parse time, and didn't want to risk more cases of errors that pointed to tokens that didn't exist in the original program, although in this particular case I don't think that's possible (since reads * can't cause errors AFAICT).

keyboardDrummer · 2023-08-28T11:26:41Z

Source/DafnyCore/Rewriters/ExpectContracts.cs

@@ -204,9 +204,17 @@ public class ExpectContracts : IRewriter {
    var post = new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq, r, fn) {
      Type = Type.Bool
    });
+    // If f.Reads is empty, replace it with an explicit `reads {}` so that we don't replace that


I think this code becomes obsolete by assigning the default reads * during parsing

keyboardDrummer · 2023-08-28T11:29:17Z

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

+      Boogie.LocalVariable frame = new Boogie.LocalVariable(tok, new Boogie.TypedIdent(tok, null ?? traitFrame.Name, traitFrame.Type));
+      localVariables.Add(frame);
+      // $_Frame := (lambda<alpha> $o: ref, $f: Field alpha :: $o != null && $Heap[$o,alloc] ==> ($o,$f) in Reads-Clause);
+      Boogie.TypeVariable alpha = new Boogie.TypeVariable(tok, "alpha");


Why so little use of var ?

Again copied without cleaning up, will do if it makes sense (prefer to merge these two instead)

keyboardDrummer · 2023-08-28T11:29:53Z

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

-              var desc = new PODesc.IsAllocated("default value", "in the two-state lemma's previous state");
-              builder.Add(Assert(e.tok, wh, desc));
+        // check well-formedness of any default-value expressions (before assuming preconditions)
+        readsCheckDelayer.WithDelayedReadsChecks(true, wfo => {


AFAIK the prefix With is commonly used for pure methods, while this seems to be a side-effecting one. I suggest replacing With with Add.

Good observation, it makes sense

Fair point, although I do want to get across the idea of "execute this with this additional context/before and after effect". Perhaps RunWithDelayedReadsChecks (or is there a more idiomatic verb for executing an Action<...>?)

Went with "DoWith.." :)

keyboardDrummer · 2023-08-28T11:33:23Z

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -1334,7 +1370,58 @@ public partial class Translator {
      builder.Add(Assert(original.Tok, decrChk, new PODesc.TraitDecreases(original.WhatKind)));
    }

-    private void AddMethodOverrideSubsetChk(Method m, BoogieStmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables,
+    // TODO: Worth sharing code between this and AddMethodOverrideModifiesSubsetChk?


keyboardDrummer · 2023-08-28T11:33:52Z

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

+    private void AddMethodOverrideReadsSubsetChk(Method m, BoogieStmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables,
+      Dictionary<IVariable, Expression> substMap,
+      Dictionary<TypeParameter, Type> typeMap) {
+      //getting framePrime


I don't understand this comment.

keyboardDrummer · 2023-08-28T11:35:49Z

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -1334,7 +1370,58 @@ public partial class Translator {
      builder.Add(Assert(original.Tok, decrChk, new PODesc.TraitDecreases(original.WhatKind)));
    }

-    private void AddMethodOverrideSubsetChk(Method m, BoogieStmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables,
+    // TODO: Worth sharing code between this and AddMethodOverrideModifiesSubsetChk?
+    private void AddMethodOverrideReadsSubsetChk(Method m, BoogieStmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables,


m => subject/target/method

keyboardDrummer · 2023-08-28T11:37:53Z

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

@@ -1334,7 +1370,58 @@ public partial class Translator {
      builder.Add(Assert(original.Tok, decrChk, new PODesc.TraitDecreases(original.WhatKind)));
    }

-    private void AddMethodOverrideSubsetChk(Method m, BoogieStmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables,
+    // TODO: Worth sharing code between this and AddMethodOverrideModifiesSubsetChk?
+    private void AddMethodOverrideReadsSubsetChk(Method m, BoogieStmtListBuilder builder, ExpressionTranslator etran, List<Variable> localVariables,


Could you clean up the code in the method AddMethodOverrideReadsSubsetChk a bit? It shows up as new in this PR but I see it was existing code.

Yup I'll first seem if I can merge the two, and either way clean them up.

MikaelMayer

Initial review, will continue later

Source/DafnyCore/AST/Members/Method.cs

MikaelMayer · 2023-08-28T19:19:05Z

Source/DafnyCore/DafnyOptions.cs

+
+      RegisterLegacyUi(CommonOptionBag.ReadsClausesOnMethods, ParseBoolean, "Language feature selection", "readsClausesOnMethods", @"
+0 (default) - Reads clauses on methods are forbidden.
+1 - Reads clauses on methods are permitted.".TrimStart(), defaultValue: false);


Yes I agree on that

Source/DafnyCore/Verifier/ProofObligationDescription.cs

MikaelMayer · 2023-08-28T19:24:41Z

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

-              var desc = new PODesc.IsAllocated("default value", "in the two-state lemma's previous state");
-              builder.Add(Assert(e.tok, wh, desc));
+        // check well-formedness of any default-value expressions (before assuming preconditions)
+        readsCheckDelayer.WithDelayedReadsChecks(true, wfo => {


Good observation, it makes sense

Source/DafnyCore/Verifier/Translator.ClassMembers.cs

MikaelMayer

I think that after my comments it's ready for approval!
Good job.

Source/DafnyCore/Verifier/Translator.cs

docs/DafnyRef/Specifications.md

Source/DafnyDriver/DafnyDoc.cs

Source/DafnyCore/Dafny.atg

Test/dafny0/ConcurrentAttribute.dfy

Test/dafny0/ConcurrentAttribute.dfy.expect

Test/dafny0/ReadsOnMethods-Resolution.dfy.expect

…ects

…bsetChk

…d-clauses-on-methods # Conflicts: # Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs # Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs

…d-clauses-on-methods

MikaelMayer · 2023-08-30T16:51:27Z

Test/dafny0/ConcurrentAttribute.dfy.expect

+ConcurrentAttribute.dfy(30,25): Error: reads clause could not be proved to be empty ({:concurrent} restriction)
+ConcurrentAttribute.dfy(48,23): Error: reads clause could not be proved to be empty ({:concurrent} restriction)
+ConcurrentAttribute.dfy(51,23): Error: reads clause could not be proved to be empty ({:concurrent} restriction)
+ConcurrentAttribute.dfy(55,23): Error: reads clause could not be proved to be empty ({:concurrent} restriction)


I see that you recently deleted {:concurrent} checks from the auditor and various places within the last 13 commits, however, you still have issues mentioning it. Can you please explain?

Ah which issues, I'm not sure I follow? I intended to delete all the references to {:concurrent} in the auditor context since I removed that case and have replaced it with verification obligations instead, but I could have missed some.

MikaelMayer

As far as I'm concerned and desired this feature, this is all I need for now, thank you very much!

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>

robin-aws added 30 commits September 16, 2021 16:01

First step, adding to parser and Method model

1bf4616

Split TheFrame into ReadsFrame and ModifiesFrame

6cf7685

Just enough to support the first test case

e29db85

Set default of "reads *" for methods

6fa7f62

Partial fixes to bad merge

12c9933

Remove zombie files from merge

41ee604

More fixes

57d9919

Another batch of error fixes

dbb4ce0

Finally builds

9ce3f2a

Fix test

905f103

Address missing resolution etc.

bbeefdb

Clean up WFOptions

7f77f7c

Partially get test working

11d4a0d

Missing cloning case

20118e6

Default to reads *

f249adb

Tweaks

b2b266c

Fix iterators (different kind of reads frame)

e53422e

Avoid reads checks when reads clause is * (not working yet?)

f1b1657

Test todos

b2b3189

Fixing check for wildcard, adding etran.WithReads/ModifiesClause()

46f9367

Fix null readsFrame bug

e94bc0f

Do reads checks on function by method bodies too

e0afd4a

Clean up test file

f6dad35

Updates to documentation

267acae

Whitespace

7518121

Apply reads clause to other clauses, {:concurrent} checks for empty f…

4f4ace4

…rames

Typo fixes, more testing

22d8d4d

Add WithDelayedReadsChecks

998b100

Fix default values

37fa445

Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…

d376bf8

…d-clauses-on-methods # Conflicts: # Source/DafnyCore/AST/Members/Method.cs # Source/DafnyCore/Resolver/ModuleResolver.cs # Source/DafnyCore/Rewriters/OpaqueMemberRewriter.cs

robin-aws changed the title ~~feat: Read clauses on methods (WIP)~~ feat: Read clauses on methods Aug 25, 2023

robin-aws marked this pull request as ready for review August 25, 2023 23:22

robin-aws requested review from MikaelMayer and RustanLeino August 25, 2023 23:28

Fix function-by-method handling, update test

ee39edc

keyboardDrummer previously approved these changes Aug 28, 2023

View reviewed changes

keyboardDrummer reviewed Aug 28, 2023

View reviewed changes

MikaelMayer reviewed Aug 28, 2023

View reviewed changes

MikaelMayer requested changes Aug 29, 2023

View reviewed changes

robin-aws added 6 commits August 29, 2023 11:29

PR feedback (more to come)

85f9db2

Merge duplicated code into AddMethodOverrideFrameSubsetChk

71b0a2f

More feedback (especially fixing {:concurrent} w.r.t. default reads!)

5993220

Address TODO about method specs referring to the set of allocated obj…

96dde55

…ects

Mark test inconsistent with function version as expected for now

b484dae

Couple of TODOs, remove extraneous code from AddMethodOverrideFrameSu…

1f8b12c

…bsetChk

robin-aws dismissed keyboardDrummer’s stale review via 1f8b12c August 30, 2023 00:09

robin-aws added 7 commits August 29, 2023 20:26

Update expect files

79d541a

Add “Do” to “WithDelayedReadsChecks”

f16064a

Reorder {:concurrent} checks

e27efe4

Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…

3cdf36e

…d-clauses-on-methods # Conflicts: # Source/DafnyCore/Resolver/PreType/UnderspecificationDetector.cs # Source/DafnyCore/Verifier/Translator.ExpressionWellformed.cs

Whitespace

0acef7f

Fix reference manual (options and attribute section numbering)

5fcf4a3

Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…

33ac004

…d-clauses-on-methods

MikaelMayer reviewed Aug 30, 2023

View reviewed changes

MikaelMayer approved these changes Aug 30, 2023

View reviewed changes

robin-aws merged commit 0d9d4e9 into dafny-lang:master Aug 30, 2023
18 checks passed

robin-aws mentioned this pull request Aug 30, 2023

Concurrency-safe history mechanism proposal (POC) smithy-lang/smithy-dafny#286

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Read clauses on methods #4440

feat: Read clauses on methods #4440

robin-aws commented Aug 18, 2023 •

edited

Loading

keyboardDrummer left a comment •

edited

Loading

keyboardDrummer Aug 28, 2023

robin-aws Aug 29, 2023

keyboardDrummer Aug 28, 2023

MikaelMayer Aug 28, 2023

robin-aws Aug 29, 2023

keyboardDrummer Aug 28, 2023

robin-aws Aug 29, 2023

keyboardDrummer Aug 30, 2023

robin-aws Sep 6, 2023

keyboardDrummer Aug 28, 2023

keyboardDrummer Aug 28, 2023

robin-aws Aug 29, 2023

keyboardDrummer Aug 28, 2023

MikaelMayer Aug 28, 2023

robin-aws Aug 29, 2023

robin-aws Aug 30, 2023

keyboardDrummer Aug 28, 2023

keyboardDrummer Aug 28, 2023

keyboardDrummer Aug 28, 2023

keyboardDrummer Aug 28, 2023

robin-aws Aug 29, 2023

MikaelMayer left a comment

MikaelMayer Aug 28, 2023

MikaelMayer Aug 28, 2023

MikaelMayer left a comment

MikaelMayer Aug 30, 2023

robin-aws Aug 30, 2023

MikaelMayer left a comment

feat: Read clauses on methods #4440

feat: Read clauses on methods #4440

Conversation

robin-aws commented Aug 18, 2023 • edited Loading

keyboardDrummer left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

robin-aws commented Aug 18, 2023 •

edited

Loading

keyboardDrummer left a comment •

edited

Loading