Skip to content
New issue

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

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

Already on GitHub? Sign in to your account

Read clauses on methods #30

Draft
wants to merge 59 commits into
base: master
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
59 commits
Select commit Hold shift + click to select a range
1bf4616
First step, adding to parser and Method model
robin-aws Sep 16, 2021
6cf7685
Split TheFrame into ReadsFrame and ModifiesFrame
robin-aws Sep 17, 2021
e29db85
Just enough to support the first test case
robin-aws Sep 17, 2021
6fa7f62
Set default of "reads *" for methods
robin-aws Sep 17, 2021
c538c2b
Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…
robin-aws Aug 4, 2023
12c9933
Partial fixes to bad merge
robin-aws Aug 4, 2023
41ee604
Remove zombie files from merge
robin-aws Aug 4, 2023
57d9919
More fixes
robin-aws Aug 4, 2023
dbb4ce0
Another batch of error fixes
robin-aws Aug 4, 2023
9ce3f2a
Finally builds
robin-aws Aug 4, 2023
905f103
Fix test
robin-aws Aug 4, 2023
bbeefdb
Address missing resolution etc.
robin-aws Aug 4, 2023
7f77f7c
Clean up WFOptions
robin-aws Aug 4, 2023
11d4a0d
Partially get test working
robin-aws Aug 4, 2023
20118e6
Missing cloning case
robin-aws Aug 14, 2023
f249adb
Default to reads *
robin-aws Aug 15, 2023
b2b266c
Tweaks
robin-aws Aug 15, 2023
e53422e
Fix iterators (different kind of reads frame)
robin-aws Aug 17, 2023
f1b1657
Avoid reads checks when reads clause is * (not working yet?)
robin-aws Aug 17, 2023
b2b3189
Test todos
robin-aws Aug 17, 2023
46f9367
Fixing check for wildcard, adding etran.WithReads/ModifiesClause()
robin-aws Aug 17, 2023
e94bc0f
Fix null readsFrame bug
robin-aws Aug 17, 2023
e0afd4a
Do reads checks on function by method bodies too
robin-aws Aug 17, 2023
f6dad35
Clean up test file
robin-aws Aug 17, 2023
267acae
Updates to documentation
robin-aws Aug 18, 2023
7518121
Whitespace
robin-aws Aug 18, 2023
4f4ace4
Apply reads clause to other clauses, {:concurrent} checks for empty f…
robin-aws Aug 19, 2023
22d8d4d
Typo fixes, more testing
robin-aws Aug 19, 2023
998b100
Add WithDelayedReadsChecks
robin-aws Aug 19, 2023
37fa445
Fix default values
robin-aws Aug 20, 2023
0a82760
Add ReadsCheckDelayer and apply it to other cases as well
robin-aws Aug 21, 2023
f7be5ed
Several missing calls to Method.Reads, beef up test cases
robin-aws Aug 21, 2023
1a0d6be
Whoops, dropping delayed reads checks statements
robin-aws Aug 21, 2023
38cdbf5
Subclassing and method call checks
robin-aws Aug 21, 2023
a00fc44
Enable reads checks on statements outside of method contexts
robin-aws Aug 22, 2023
0a54826
Trying out defaulting to `reads {}` on ghost methods
robin-aws Aug 22, 2023
22a4867
Lemmas instead of ghost methods
robin-aws Aug 23, 2023
347563e
No reads or checking on lemmas, more LHS fixes, more tests
robin-aws Aug 25, 2023
af497ec
update TODOs
robin-aws Aug 25, 2023
275e56d
Add option to enable, most testing (and reorganize old file tests)
robin-aws Aug 25, 2023
1386c43
More tests
robin-aws Aug 25, 2023
1cb1175
Cloning another test file
robin-aws Aug 25, 2023
0254121
Remaining tests
robin-aws Aug 25, 2023
82a160e
Whitespace and todos
robin-aws Aug 25, 2023
d376bf8
Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…
robin-aws Aug 25, 2023
ee39edc
Fix function-by-method handling, update test
robin-aws Aug 26, 2023
85f9db2
PR feedback (more to come)
robin-aws Aug 29, 2023
71b0a2f
Merge duplicated code into AddMethodOverrideFrameSubsetChk
robin-aws Aug 29, 2023
5993220
More feedback (especially fixing {:concurrent} w.r.t. default reads!)
robin-aws Aug 29, 2023
96dde55
Address TODO about method specs referring to the set of allocated obj…
robin-aws Aug 29, 2023
b484dae
Mark test inconsistent with function version as expected for now
robin-aws Aug 29, 2023
1f8b12c
Couple of TODOs, remove extraneous code from AddMethodOverrideFrameSu…
robin-aws Aug 30, 2023
79d541a
Update expect files
robin-aws Aug 30, 2023
f16064a
Add “Do” to “WithDelayedReadsChecks”
robin-aws Aug 30, 2023
e27efe4
Reorder {:concurrent} checks
robin-aws Aug 30, 2023
3cdf36e
Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…
robin-aws Aug 30, 2023
0acef7f
Whitespace
robin-aws Aug 30, 2023
5fcf4a3
Fix reference manual (options and attribute section numbering)
robin-aws Aug 30, 2023
33ac004
Merge branch 'master' of https://github.com/dafny-lang/dafny into rea…
robin-aws Aug 30, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Do reads checks on function by method bodies too
  • Loading branch information
robin-aws committed Aug 17, 2023
commit e0afd4a4b43b0c9fff473855c293edbcdd4e0b2c
12 changes: 11 additions & 1 deletion Source/DafnyCore/Resolver/ModuleResolver.cs
Original file line number Diff line number Diff line change
@@ -792,9 +792,19 @@ public static void RegisterByMethod(Function f, TopLevelDeclWithMembers cl) {
new ActualBindings(f.Formals.ConvertAll(Expression.CreateIdentExpr)).ArgumentBindings,
tok);
var post = new AttributedExpression(new BinaryExpr(tok, BinaryExpr.Opcode.Eq, r, fn));
// If f.Reads is empty, replace it with an explicit `reads {}` so that we don't replace that
// with the default `reads *` for methods later.
// TODO: We could also have a flag similar to InferredDecreases to distinguish between
// "not given" and "explicitly empty"
var reads = f.Reads;
if (!reads.Any()) {
reads = new List<FrameExpression>();
var emptySet = new SetDisplayExpr(tok, true, new List<Expression>());
reads.Add(new FrameExpression(tok, emptySet, null));
}
var method = new Method(f.RangeToken, f.NameNode, f.HasStaticKeyword, false, f.TypeArgs,
f.Formals, new List<Formal>() { resultVar },
f.Req, new List<FrameExpression>(), new Specification<FrameExpression>(new List<FrameExpression>(), null), new List<AttributedExpression>() { post }, f.Decreases,
f.Req, reads, new Specification<FrameExpression>(new List<FrameExpression>(), null), new List<AttributedExpression>() { post }, f.Decreases,
f.ByMethodBody, f.Attributes, null, true);
Contract.Assert(f.ByMethodDecl == null);
method.InheritVisibility(f);
10 changes: 9 additions & 1 deletion Source/DafnyCore/Rewriters/ExpectContracts.cs
Original file line number Diff line number Diff line change
@@ -204,9 +204,17 @@ private static void RegisterResolvedByMethod(Function f, TopLevelDeclWithMembers
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
// with the default `reads *` for methods later.
var reads = f.Reads;
if (!reads.Any()) {
reads = new List<FrameExpression>();
var emptySet = new SetDisplayExpr(tok, true, new List<Expression>());
reads.Add(new FrameExpression(tok, emptySet, null));
}
var method = new Method(f.RangeToken, f.NameNode, f.HasStaticKeyword, false, f.TypeArgs,
f.Formals, new List<Formal>() { resultVar },
f.Req, new List<FrameExpression>(), new Specification<FrameExpression>(new List<FrameExpression>(), null), new List<AttributedExpression>() { post }, f.Decreases,
f.Req, reads, new Specification<FrameExpression>(new List<FrameExpression>(), null), new List<AttributedExpression>() { post }, f.Decreases,
f.ByMethodBody, f.Attributes, null, true);
Contract.Assert(f.ByMethodDecl == null);
method.InheritVisibility(f);
11 changes: 7 additions & 4 deletions Test/git-issues/github-issue-reads-on-methods.dfy
Original file line number Diff line number Diff line change
@@ -72,12 +72,15 @@ method MemoizedSquare(x: int, cache: ExternalMutableMap<int, int>) returns (xSqu
}
}

function Foo(b: Box): int {
b.x
function Always42(b: Box): int {
42
} by method {
var x := b.x; // Should be error
var result := 42;
result := result + b.x; // Error: insufficient reads clause to read field
result := result - b.x;
return 42;
}

// TODO:
// * iterators (would like to align semantics)
// * stress test well-formedness of reads clauses (e.g. when depending on method preconditions)
// * Double check refinement
3 changes: 2 additions & 1 deletion Test/git-issues/github-issue-reads-on-methods.dfy.expect
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
github-issue-reads-on-methods.dfy(36,9): Error: insufficient reads clause to read field
github-issue-reads-on-methods.dfy(79,23): Error: insufficient reads clause to read field

Dafny program verifier finished with 8 verified, 1 error
Dafny program verifier finished with 8 verified, 2 errors