-
Notifications
You must be signed in to change notification settings - Fork 259
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
Feat: {:only}
attribute for members
#4075
Changes from 6 commits
b57f52a
eb93921
61a650e
a3f6420
0547fc3
e26a10a
f61809f
a2db7e8
e78e3ec
c3da8a3
5839315
fc678c1
ca1d3df
f7bf31e
b5a9a96
902a374
5f6595f
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change | ||||
---|---|---|---|---|---|---|
|
@@ -103,10 +103,18 @@ public static AssumptionDescription NoBody(bool isGhost) { | |||||
allowedInLibraries: false); | ||||||
} | ||||||
|
||||||
public static AssumptionDescription AssertOnly = new( | ||||||
public static readonly AssumptionDescription AssertOnly = new( | ||||||
issue: "Assertion has explicit temporary [{:only}] attribute.", | ||||||
mitigation: "Remove the [{:only}] attribute", | ||||||
mitigationIETF: "Must remove the [{:only}] attribute", | ||||||
mitigation: "Remove the [{:only}] attribute.", | ||||||
mitigationIETF: "Must remove the [{:only}] attribute.", | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
That's the standard IETF way of writing obligatory requirements. |
||||||
isExplicit: true, | ||||||
allowedInLibraries: false | ||||||
); | ||||||
|
||||||
public static readonly AssumptionDescription MemberOnly = new( | ||||||
issue: "Member has explicit temporary [{:only}] attribute.", | ||||||
mitigation: "Remove the [{:only}] attribute.", | ||||||
mitigationIETF: "Must remove the [{:only}] attribute.", | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||
isExplicit: true, | ||||||
allowedInLibraries: false | ||||||
); | ||||||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -3252,6 +3252,14 @@ void ResolveClassMemberBodies(TopLevelDeclWithMembers cl) { | |
currentClass = cl; | ||
foreach (MemberDecl member in cl.Members) { | ||
Contract.Assert(VisibleInScope(member)); | ||
if (Attributes.Find(member.Attributes, "only") is UserSuppliedAttributes attribute) { | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This could use There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Implemented. |
||
reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_assumes_other.ToString(), attribute.RangeToken.ToToken(), | ||
"Members with {:only} temporarily disable the verification of other members in the entire file"); | ||
if (attribute.Args.Count >= 1) { | ||
reporter.Warning(MessageSource.Verifier, ResolutionErrors.ErrorId.r_member_only_has_no_before_after.ToString(), attribute.Args[0].RangeToken.ToToken(), | ||
"{:only} on members does not support arguments"); | ||
} | ||
} | ||
if (member is Field) { | ||
var resolutionContext = new ResolutionContext(new NoContext(currentClass.EnclosingModuleDefinition), false); | ||
scope.PushMarker(); | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -30,6 +30,7 @@ namespace Microsoft.Dafny { | |
public partial class Translator { | ||
private DafnyOptions options; | ||
public const string NameSeparator = "$$"; | ||
private bool filterOnlyMembers; | ||
|
||
ErrorReporter reporter; | ||
// TODO(wuestholz): Enable this once Dafny's recommended Z3 version includes changeset 0592e765744497a089c42021990740f303901e67. | ||
|
@@ -792,23 +793,36 @@ private Bpl.Program DoTranslation(Program p, ModuleDefinition forModule) { | |
mods.Remove(forModule); | ||
mods.Insert(0, forModule); | ||
|
||
foreach (ModuleDefinition m in mods) { | ||
foreach (TopLevelDecl d in m.TopLevelDecls.FindAll(VisibleInScope)) { | ||
currentDeclaration = d; | ||
if (d is AbstractTypeDecl) { | ||
var dd = (AbstractTypeDecl)d; | ||
AddTypeDecl(dd); | ||
AddClassMembers(dd, true, true); | ||
} else if (d is ModuleDecl) { | ||
// submodules have already been added as a top level module, ignore this. | ||
} else if (d is RevealableTypeDecl) { | ||
AddTypeDecl((RevealableTypeDecl)d); | ||
} else { | ||
Contract.Assert(false); | ||
} | ||
|
||
var visibleTopLevelDecls = | ||
mods.SelectMany(m => m.TopLevelDecls.FindAll(VisibleInScope)); | ||
|
||
if (visibleTopLevelDecls.Any( | ||
d => d is TopLevelDeclWithMembers memberContainer && | ||
memberContainer.Members.Any( | ||
member => | ||
Attributes.Contains(member.Attributes, "only") | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Could use |
||
))) { | ||
filterOnlyMembers = true; | ||
} | ||
|
||
foreach (TopLevelDecl d in visibleTopLevelDecls) { | ||
currentDeclaration = d; | ||
if (d is AbstractTypeDecl) { | ||
var dd = (AbstractTypeDecl)d; | ||
AddTypeDecl(dd); | ||
AddClassMembers(dd, true, true); | ||
} else if (d is ModuleDecl) { | ||
// submodules have already been added as a top level module, ignore this. | ||
} else if (d is RevealableTypeDecl) { | ||
AddTypeDecl((RevealableTypeDecl)d); | ||
} else { | ||
Contract.Assert(false); | ||
} | ||
} | ||
|
||
filterOnlyMembers = false; | ||
|
||
foreach (var c in tytagConstants.Values) { | ||
sink.AddTopLevelDeclaration(c); | ||
} | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -137,3 +137,7 @@ method AssertOnly() { | |
assert {:only} true; | ||
assert false; | ||
} | ||
|
||
method {:only} MethodOnly() { | ||
assert false; | ||
} |
Original file line number | Diff line number | Diff line change | ||||
---|---|---|---|---|---|---|
|
@@ -76,4 +76,8 @@ | |||||
|
||||||
### Member `AssertOnly` | ||||||
|
||||||
* Assertion has explicit temporary `{:only}` attribute. Must remove the `{:only}` attribute | ||||||
* Assertion has explicit temporary `{:only}` attribute. Must remove the `{:only}` attribute. | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
||||||
|
||||||
### Member `MethodOnly` | ||||||
|
||||||
* Member has explicit temporary `{:only}` attribute. Must remove the `{:only}` attribute. | ||||||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
Suggested change
|
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
// RUN: %exits-with 4 %baredafny verify %args "%s" > "%t" | ||
// RUN: %diff "%s.expect" "%t" | ||
|
||
method {:only "wrongArgument"} TestReported() { | ||
assert false; // An error here | ||
} | ||
|
||
method TestNotReported() { | ||
assert false; | ||
} | ||
|
||
class A { | ||
method {:only} TestReported() { | ||
assert false; // An error here | ||
} | ||
|
||
method TestNotReported() { | ||
assert false; | ||
} | ||
} | ||
|
||
module B { | ||
method {:only} TestReported() { | ||
assert false; // An error here | ||
} | ||
|
||
method TestNotReported() { | ||
assert false; | ||
} | ||
} |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
git-issue-4074.dfy(23,9): Warning: Members with {:only} temporarily disable the verification of other members in the entire file | ||
git-issue-4074.dfy(13,9): Warning: Members with {:only} temporarily disable the verification of other members in the entire file | ||
git-issue-4074.dfy(4,7): Warning: Members with {:only} temporarily disable the verification of other members in the entire file | ||
git-issue-4074.dfy(4,14): Warning: {:only} on members does not support arguments | ||
git-issue-4074.dfy(24,11): Error: assertion might not hold | ||
git-issue-4074.dfy(14,11): Error: assertion might not hold | ||
git-issue-4074.dfy(5,9): Error: assertion might not hold | ||
|
||
Dafny program verifier finished with 0 verified, 3 errors |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It's a little unfortunate to have this implemented twice, once on members and once on statements, but it might be worse to lift it up to arbitrary AST nodes, so perhaps it's reasonable to keep it this way.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, until we have mix-ins :-)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Actually with extensions we have mixins. Let me refactor it.