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.

Sign up for GitHub

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

Jump to bottom

Old read clauses on methods (diff against original branch point) #31

Draft
wants to merge 4 commits into
base: read-clauses-on-methods-old-baseline
Choose a base branch
from
Draft

Old read clauses on methods (diff against original branch point) #31

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 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
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
45 changes: 31 additions & 14 deletions Source/Dafny/AST/DafnyAst.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6446,6 +6446,7 @@ public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext {
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;
Expand Down Expand Up @@ -6493,7 +6494,9 @@ public Method(IToken tok, string 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,
Expand All @@ -6505,12 +6508,14 @@ public Method(IToken tok, string 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;
Expand Down Expand Up @@ -6599,12 +6604,14 @@ public Lemma(IToken tok, string 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(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
}
}

Expand All @@ -6615,12 +6622,13 @@ public TwoStateLemma(IToken tok, string 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(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(typeArgs != null);
Expand Down Expand Up @@ -6660,12 +6668,14 @@ public List<Statement> BodyProper { // second part of Body's statements
public Constructor(IToken tok, string name,
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(tok, name, false, false, typeArgs, ins, new List<Formal>(), req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(tok, name, false, false, typeArgs, ins, new List<Formal>(), req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Expand All @@ -6692,9 +6702,10 @@ public class PrefixLemma : Method {
public readonly ExtremeLemma ExtremeLemma;
public PrefixLemma(IToken tok, string 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, List<FrameExpression> reads, Specification<FrameExpression> mod,
List<AttributedExpression> ens, Specification<Expression> decreases,
BlockStmt body, Attributes attributes, ExtremeLemma extremeLemma)
: base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, null) {
: base(tok, 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);
Expand All @@ -6716,12 +6727,14 @@ public ExtremeLemma(IToken tok, string 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(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(tok, name, hasStaticKeyword, true, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Expand All @@ -6742,12 +6755,14 @@ public LeastLemma(IToken tok, string 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(tok, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(tok, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Expand All @@ -6767,12 +6782,14 @@ public GreatestLemma(IToken tok, string 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(tok, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, mod, ens, decreases, body, attributes, signatureEllipsis) {
: base(tok, name, hasStaticKeyword, typeOfK, typeArgs, ins, outs, req, reads, mod, ens, decreases, body, attributes, signatureEllipsis) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
Contract.Requires(cce.NonNullElements(typeArgs));
Expand Down
13 changes: 7 additions & 6 deletions Source/Dafny/Cloner.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -790,6 +790,7 @@ public virtual Method CloneMethod(Method m) {
var tps = m.TypeArgs.ConvertAll(CloneTypeParam);
var ins = m.Ins.ConvertAll(CloneFormal);
var req = m.Req.ConvertAll(CloneAttributedExpr);
var reads = m.Reads.ConvertAll(CloneFrameExpr);
var mod = CloneSpecFrameExpr(m.Mod);
var decreases = CloneSpecExpr(m.Decreases);

Expand All @@ -799,23 +800,23 @@ public virtual Method CloneMethod(Method m) {

if (m is Constructor) {
return new Constructor(Tok(m.tok), m.Name, tps, ins,
req, mod, ens, decreases, (DividedBlockStmt)body, CloneAttributes(m.Attributes), null);
req, reads, mod, ens, decreases, (DividedBlockStmt)body, CloneAttributes(m.Attributes), null);
} else if (m is LeastLemma) {
return new LeastLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, ((LeastLemma)m).TypeOfK, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
req, reads, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
} else if (m is GreatestLemma) {
return new GreatestLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, ((GreatestLemma)m).TypeOfK, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
req, reads, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
} else if (m is Lemma) {
return new Lemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
req, reads, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
} else if (m is TwoStateLemma) {
var two = (TwoStateLemma)m;
return new TwoStateLemma(Tok(m.tok), m.Name, m.HasStaticKeyword, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
req, reads, mod, ens, decreases, body, CloneAttributes(m.Attributes), null);
} else {
return new Method(Tok(m.tok), m.Name, m.HasStaticKeyword, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),
req, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m.IsByMethod);
req, reads, mod, ens, decreases, body, CloneAttributes(m.Attributes), null, m.IsByMethod);
}
}

Expand Down
21 changes: 12 additions & 9 deletions Source/Dafny/Dafny.atg
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1667,6 +1667,7 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
List<Formal/*!*/> ins = new List<Formal/*!*/>();
List<Formal/*!*/> outs = new List<Formal/*!*/>();
List<AttributedExpression/*!*/> req = new List<AttributedExpression/*!*/>();
List<FrameExpression/*!*/> reads = new List<FrameExpression/*!*/>();
List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();
List<AttributedExpression/*!*/> ens = new List<AttributedExpression/*!*/>();
List<Expression/*!*/> dec = new List<Expression/*!*/>();
Expand Down Expand Up @@ -1736,7 +1737,7 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
| ellipsis (. signatureEllipsis = t; .)
)
MethodSpec<dmod.IsGhost || isLemma || isTwoStateLemma || isLeastLemma || isGreatestLemma,
req, mod, ens, dec, ref decAttrs, ref modAttrs, caption, isConstructor>
req, reads, mod, ens, dec, ref decAttrs, ref modAttrs, caption, isConstructor>
[ IF(isConstructor)
(. DividedBlockStmt dividedBody; .)
DividedBlockStmt<out dividedBody, out bodyStart, out bodyEnd>
Expand All @@ -1746,23 +1747,23 @@ MethodDecl<DeclModifierData dmod, bool allowConstructor, out Method/*!*/ m>
(. IToken tok = id;
if (isConstructor) {
m = new Constructor(tok, hasName ? id.val : "_ctor", typeArgs, ins,
req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), (DividedBlockStmt)body, attrs, signatureEllipsis);
req, reads, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), (DividedBlockStmt)body, attrs, signatureEllipsis);
} else if (isLeastLemma) {
m = new LeastLemma(tok, id.val, dmod.IsStatic, kType, typeArgs, ins, outs,
req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
req, reads, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
} else if (isGreatestLemma) {
m = new GreatestLemma(tok, id.val, dmod.IsStatic, kType, typeArgs, ins, outs,
req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
req, reads, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
} else if (isLemma) {
m = new Lemma(tok, id.val, dmod.IsStatic, typeArgs, ins, outs,
req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
req, reads, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
} else if (isTwoStateLemma) {
m = new TwoStateLemma(tok, id.val, dmod.IsStatic, typeArgs, ins, outs,
req, new Specification<FrameExpression>(mod, modAttrs),
req, reads, new Specification<FrameExpression>(mod, modAttrs),
ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
} else {
m = new Method(tok, id.val, dmod.IsStatic, dmod.IsGhost, typeArgs, ins, outs,
req, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
req, reads, new Specification<FrameExpression>(mod, modAttrs), ens, new Specification<Expression>(dec, decAttrs), body, attrs, signatureEllipsis);
}
m.BodyStartTok = bodyStart;
m.BodyEndTok = bodyEnd;
Expand Down Expand Up @@ -1852,15 +1853,17 @@ InvariantClause<. List<AttributedExpression> invariants.> =
.

/*------------------------------------------------------------------------*/
MethodSpec<.bool isGhost, List<AttributedExpression> req, List<FrameExpression> mod, List<AttributedExpression> ens,
MethodSpec<.bool isGhost, List<AttributedExpression> req, List<FrameExpression> reads, List<FrameExpression> mod, List<AttributedExpression> ens,
List<Expression> decreases, ref Attributes decAttrs, ref Attributes modAttrs, string caption, bool performThisDeprecatedCheck.>
= (. Contract.Requires(cce.NonNullElements(req));
Contract.Requires(cce.NonNullElements(reads));
Contract.Requires(cce.NonNullElements(mod));
Contract.Requires(cce.NonNullElements(ens));
Contract.Requires(cce.NonNullElements(decreases));
.)
SYNC
{ ModifiesClause<ref mod, ref modAttrs, false, performThisDeprecatedCheck>
{ ReadsClause<reads, false, false, true>
| ModifiesClause<ref mod, ref modAttrs, false, performThisDeprecatedCheck>
| RequiresClause<req, true>
| EnsuresClause<ens, false>
| DecreasesClause<decreases, ref decAttrs, !isGhost, false>
Expand Down
Loading