summaryrefslogtreecommitdiff
path: root/Dafny
diff options
context:
space:
mode:
Diffstat (limited to 'Dafny')
-rw-r--r--Dafny/Cloner.cs59
-rw-r--r--Dafny/Compiler.cs170
-rw-r--r--Dafny/Dafny.atg42
-rw-r--r--Dafny/DafnyAst.cs40
-rw-r--r--Dafny/Parser.cs38
-rw-r--r--Dafny/Printer.cs18
-rw-r--r--Dafny/RefinementTransformer.cs34
-rw-r--r--Dafny/Resolver.cs214
-rw-r--r--Dafny/Translator.cs102
9 files changed, 540 insertions, 177 deletions
diff --git a/Dafny/Cloner.cs b/Dafny/Cloner.cs
index b1b8828a..6d99ce9b 100644
--- a/Dafny/Cloner.cs
+++ b/Dafny/Cloner.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Dafny
if (m is DefaultModuleDecl) {
nw = new DefaultModuleDecl();
} else {
- nw = new ModuleDefinition(Tok(m.tok), name, m.IsGhost, m.IsAbstract, m.RefinementBaseName, null, true);
+ nw = new ModuleDefinition(Tok(m.tok), name, m.IsGhost, m.IsAbstract, m.RefinementBaseName, CloneAttributes(m.Attributes), true);
}
foreach (var d in m.TopLevelDecls) {
nw.TopLevelDecls.Add(CloneDeclaration(d, nw));
@@ -29,18 +29,18 @@ namespace Microsoft.Dafny
if (d is ArbitraryTypeDecl) {
var dd = (ArbitraryTypeDecl)d;
- return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, null);
+ return new ArbitraryTypeDecl(Tok(dd.tok), dd.Name, m, dd.EqualitySupport, CloneAttributes(dd.Attributes));
} else if (d is IndDatatypeDecl) {
var dd = (IndDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var ctors = dd.Ctors.ConvertAll(CloneCtor);
- var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
+ var dt = new IndDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes));
return dt;
} else if (d is CoDatatypeDecl) {
var dd = (CoDatatypeDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var ctors = dd.Ctors.ConvertAll(CloneCtor);
- var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, null);
+ var dt = new CoDatatypeDecl(Tok(dd.tok), dd.Name, m, tps, ctors, CloneAttributes(dd.Attributes));
return dt;
} else if (d is ClassDecl) {
if (d is DefaultClassDecl) {
@@ -53,7 +53,7 @@ namespace Microsoft.Dafny
var dd = (ClassDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var mm = dd.Members.ConvertAll(CloneMember);
- var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, null);
+ var cl = new ClassDecl(Tok(dd.tok), dd.Name, m, tps, mm, CloneAttributes(dd.Attributes));
return cl;
}
} else if (d is ModuleDecl) {
@@ -84,7 +84,7 @@ namespace Microsoft.Dafny
}
public DatatypeCtor CloneCtor(DatatypeCtor ct) {
- return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), null);
+ return new DatatypeCtor(Tok(ct.tok), ct.Name, ct.Formals.ConvertAll(CloneFormal), CloneAttributes(ct.Attributes));
}
public TypeParameter CloneTypeParam(TypeParameter tp) {
@@ -93,8 +93,9 @@ namespace Microsoft.Dafny
public MemberDecl CloneMember(MemberDecl member) {
if (member is Field) {
+ Contract.Assert(!(member is SpecialField)); // we don't expect a SpecialField to be cloned (or do we?)
var f = (Field)member;
- return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), null);
+ return new Field(Tok(f.tok), f.Name, f.IsGhost, f.IsMutable, CloneType(f.Type), CloneAttributes(f.Attributes));
} else if (member is Function) {
var f = (Function)member;
return CloneFunction(f);
@@ -142,17 +143,24 @@ namespace Microsoft.Dafny
public Specification<Expression> CloneSpecExpr(Specification<Expression> spec) {
var ee = spec.Expressions == null ? null : spec.Expressions.ConvertAll(CloneExpr);
- return new Specification<Expression>(ee, null);
+ return new Specification<Expression>(ee, CloneAttributes(spec.Attributes));
}
public Specification<FrameExpression> CloneSpecFrameExpr(Specification<FrameExpression> frame) {
var ee = frame.Expressions == null ? null : frame.Expressions.ConvertAll(CloneFrameExpr);
- return new Specification<FrameExpression>(ee, null);
+ return new Specification<FrameExpression>(ee, CloneAttributes(frame.Attributes));
}
public FrameExpression CloneFrameExpr(FrameExpression frame) {
return new FrameExpression(Tok(frame.tok), CloneExpr(frame.E), frame.FieldName);
}
+ public Attributes CloneAttributes(Attributes attrs) {
+ if (attrs == null) {
+ return null;
+ } else {
+ return new Attributes(attrs.Name, attrs.Args.ConvertAll(CloneAttrArg), CloneAttributes(attrs.Prev));
+ }
+ }
public Attributes.Argument CloneAttrArg(Attributes.Argument aa) {
if (aa.E != null) {
return new Attributes.Argument(Tok(aa.Tok), CloneExpr(aa.E));
@@ -162,7 +170,9 @@ namespace Microsoft.Dafny
}
public MaybeFreeExpression CloneMayBeFreeExpr(MaybeFreeExpression expr) {
- return new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);
+ var mfe = new MaybeFreeExpression(CloneExpr(expr.E), expr.IsFree);
+ mfe.Attributes = CloneAttributes(expr.Attributes);
+ return mfe;
}
public virtual Expression CloneExpr(Expression expr) {
@@ -273,9 +283,9 @@ namespace Microsoft.Dafny
var range = CloneExpr(e.Range);
var term = CloneExpr(e.Term);
if (e is ForallExpr) {
- return new ForallExpr(tk, bvs, range, term, null);
+ return new ForallExpr(tk, bvs, range, term, CloneAttributes(e.Attributes));
} else if (e is ExistsExpr) {
- return new ExistsExpr(tk, bvs, range, term, null);
+ return new ExistsExpr(tk, bvs, range, term, CloneAttributes(e.Attributes));
} else if (e is MapComprehension) {
return new MapComprehension(tk, bvs, range, term);
} else {
@@ -319,21 +329,24 @@ namespace Microsoft.Dafny
}
public AssignmentRhs CloneRHS(AssignmentRhs rhs) {
+ AssignmentRhs c;
if (rhs is ExprRhs) {
var r = (ExprRhs)rhs;
- return new ExprRhs(CloneExpr(r.Expr));
+ c = new ExprRhs(CloneExpr(r.Expr));
} else if (rhs is HavocRhs) {
- return new HavocRhs(Tok(rhs.Tok));
+ c = new HavocRhs(Tok(rhs.Tok));
} else {
var r = (TypeRhs)rhs;
if (r.ArrayDimensions != null) {
- return new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.ArrayDimensions.ConvertAll(CloneExpr));
+ c = new TypeRhs(Tok(r.Tok), CloneType(r.EType), r.ArrayDimensions.ConvertAll(CloneExpr));
} else if (r.InitCall != null) {
- return new TypeRhs(Tok(r.Tok), CloneType(r.EType), (CallStmt)CloneStmt(r.InitCall));
+ c = new TypeRhs(Tok(r.Tok), CloneType(r.EType), (CallStmt)CloneStmt(r.InitCall));
} else {
- return new TypeRhs(Tok(r.Tok), CloneType(r.EType));
+ c = new TypeRhs(Tok(r.Tok), CloneType(r.EType));
}
}
+ c.Attributes = CloneAttributes(rhs.Attributes);
+ return c;
}
public BlockStmt CloneBlockStmt(BlockStmt stmt) {
@@ -432,6 +445,7 @@ namespace Microsoft.Dafny
// add labels to the cloned statement
AddStmtLabels(r, stmt.Labels);
+ r.Attributes = CloneAttributes(stmt.Attributes);
return r;
}
@@ -452,7 +466,6 @@ namespace Microsoft.Dafny
}
public Function CloneFunction(Function f) {
-
var tps = f.TypeArgs.ConvertAll(CloneTypeParam);
var formals = f.Formals.ConvertAll(CloneFormal);
var req = f.Req.ConvertAll(CloneExpr);
@@ -463,13 +476,13 @@ namespace Microsoft.Dafny
if (f is Predicate) {
return new Predicate(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, tps, f.OpenParen, formals,
- req, reads, ens, decreases, body, false, null, false);
+ req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, CloneAttributes(f.Attributes), false);
} else if (f is CoPredicate) {
return new CoPredicate(Tok(f.tok), f.Name, f.IsStatic, tps, f.OpenParen, formals,
- req, reads, ens, body, null, false);
+ req, reads, ens, body, CloneAttributes(f.Attributes), false);
} else {
return new Function(Tok(f.tok), f.Name, f.IsStatic, f.IsGhost, tps, f.OpenParen, formals, CloneType(f.ResultType),
- req, reads, ens, decreases, body, null, false);
+ req, reads, ens, decreases, body, CloneAttributes(f.Attributes), false);
}
}
@@ -487,10 +500,10 @@ namespace Microsoft.Dafny
var body = CloneBlockStmt(m.Body);
if (m is Constructor) {
return new Constructor(Tok(m.tok), m.Name, tps, ins,
- req, mod, ens, decreases, body, null, false);
+ req, mod, ens, decreases, body, CloneAttributes(m.Attributes), false);
} else {
return new Method(Tok(m.tok), m.Name, m.IsStatic, m.IsGhost, tps, ins, m.Outs.ConvertAll(CloneFormal),
- req, mod, ens, decreases, body, null, false);
+ req, mod, ens, decreases, body, CloneAttributes(m.Attributes), false);
}
}
public virtual IToken Tok(IToken tok) {
diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index 18721cf3..8715c047 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -25,6 +25,7 @@ namespace Microsoft.Dafny {
}
TextWriter wr;
+ Method enclosingMethod; // non-null when a method body is being translated
public int ErrorCount;
void Error(string msg, params object[] args) {
@@ -633,7 +634,17 @@ namespace Microsoft.Dafny {
if (m.Body == null) {
Error("Method {0} has no body", m.FullName);
} else {
+ if (m.IsTailRecursive) {
+ Indent(indent); wr.WriteLine("TAIL_CALL_START: ;");
+ if (!m.IsStatic) {
+ Indent(indent); wr.WriteLine("var _this = this;");
+ }
+ }
+ Contract.Assert(enclosingMethod == null);
+ enclosingMethod = m;
TrStmtList(m.Body.Body, indent);
+ Contract.Assert(enclosingMethod == m);
+ enclosingMethod = null;
}
Indent(indent); wr.WriteLine("}");
@@ -1408,66 +1419,125 @@ namespace Microsoft.Dafny {
Contract.Requires(s != null);
Contract.Assert(s.Method != null); // follows from the fact that stmt has been successfully resolved
- var lvalues = new List<string>();
- Contract.Assert(s.Lhs.Count == s.Method.Outs.Count);
- for (int i = 0; i < s.Method.Outs.Count; i++) {
- Formal p = s.Method.Outs[i];
- if (!p.IsGhost) {
- lvalues.Add(CreateLvalue(s.Lhs[i], indent));
+ if (s.Method == enclosingMethod && enclosingMethod.IsTailRecursive) {
+ // compile call as tail-recursive
+
+ // assign the actual in-parameters to temporary variables
+ var inTmps = new List<string>();
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ SpillLetVariableDecls(s.Args[i], indent);
+ }
}
- }
- var outTmps = new List<string>();
- for (int i = 0; i < s.Method.Outs.Count; i++) {
- Formal p = s.Method.Outs[i];
- if (!p.IsGhost) {
- string target = "_out" + tmpVarCount;
+ if (receiverReplacement != null) {
+ // TODO: What to do here? When does this happen, what does it mean?
+ } else if (!s.Method.IsStatic) {
+ SpillLetVariableDecls(s.Receiver, indent);
+
+ string inTmp = "_in" + tmpVarCount;
tmpVarCount++;
- outTmps.Add(target);
+ inTmps.Add(inTmp);
Indent(indent);
- wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type), target);
+ wr.Write("var {0} = ", inTmp);
+ TrExpr(s.Receiver);
+ wr.WriteLine(";");
}
- }
- Contract.Assert(lvalues.Count == outTmps.Count);
-
- for (int i = 0; i < s.Method.Ins.Count; i++) {
- Formal p = s.Method.Ins[i];
- if (!p.IsGhost) {
- SpillLetVariableDecls(s.Args[i], indent);
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ string inTmp = "_in" + tmpVarCount;
+ tmpVarCount++;
+ inTmps.Add(inTmp);
+ Indent(indent);
+ wr.Write("var {0} = ", inTmp);
+ TrExpr(s.Args[i]);
+ wr.WriteLine(";");
+ }
}
- }
- if (receiverReplacement != null) {
- Indent(indent);
- wr.Write("@" + receiverReplacement);
- } else if (s.Method.IsStatic) {
+ // Now, assign to the formals
+ int n = 0;
+ if (!s.Method.IsStatic) {
+ Indent(indent);
+ wr.WriteLine("_this = {0};", inTmps[n]);
+ n++;
+ }
+ foreach (var p in s.Method.Ins) {
+ if (!p.IsGhost) {
+ Indent(indent);
+ wr.WriteLine("{0} = {1};", p.CompileName, inTmps[n]);
+ n++;
+ }
+ }
+ Contract.Assert(n == inTmps.Count);
+ // finally, the jump back to the head of the method
Indent(indent);
- wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
+ wr.WriteLine("goto TAIL_CALL_START;");
+
} else {
- SpillLetVariableDecls(s.Receiver, indent);
- Indent(indent);
- TrParenExpr(s.Receiver);
- }
- wr.Write(".@{0}(", s.Method.CompileName);
+ // compile call as a regular call
+
+ var lvalues = new List<string>();
+ Contract.Assert(s.Lhs.Count == s.Method.Outs.Count);
+ for (int i = 0; i < s.Method.Outs.Count; i++) {
+ Formal p = s.Method.Outs[i];
+ if (!p.IsGhost) {
+ lvalues.Add(CreateLvalue(s.Lhs[i], indent));
+ }
+ }
+ var outTmps = new List<string>();
+ for (int i = 0; i < s.Method.Outs.Count; i++) {
+ Formal p = s.Method.Outs[i];
+ if (!p.IsGhost) {
+ string target = "_out" + tmpVarCount;
+ tmpVarCount++;
+ outTmps.Add(target);
+ Indent(indent);
+ wr.WriteLine("{0} {1};", TypeName(s.Lhs[i].Type), target);
+ }
+ }
+ Contract.Assert(lvalues.Count == outTmps.Count);
- string sep = "";
- for (int i = 0; i < s.Method.Ins.Count; i++) {
- Formal p = s.Method.Ins[i];
- if (!p.IsGhost) {
- wr.Write(sep);
- TrExpr(s.Args[i]);
- sep = ", ";
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ SpillLetVariableDecls(s.Args[i], indent);
+ }
}
- }
+ if (receiverReplacement != null) {
+ Indent(indent);
+ wr.Write("@" + receiverReplacement);
+ } else if (s.Method.IsStatic) {
+ Indent(indent);
+ wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
+ } else {
+ SpillLetVariableDecls(s.Receiver, indent);
+ Indent(indent);
+ TrParenExpr(s.Receiver);
+ }
+ wr.Write(".@{0}(", s.Method.CompileName);
- foreach (var outTmp in outTmps) {
- wr.Write("{0}out {1}", sep, outTmp);
- sep = ", ";
- }
- wr.WriteLine(");");
+ string sep = "";
+ for (int i = 0; i < s.Method.Ins.Count; i++) {
+ Formal p = s.Method.Ins[i];
+ if (!p.IsGhost) {
+ wr.Write(sep);
+ TrExpr(s.Args[i]);
+ sep = ", ";
+ }
+ }
- // assign to the actual LHSs
- for (int j = 0; j < lvalues.Count; j++) {
- Indent(indent);
- wr.WriteLine("{0} = {1};", lvalues[j], outTmps[j]);
+ foreach (var outTmp in outTmps) {
+ wr.Write("{0}out {1}", sep, outTmp);
+ sep = ", ";
+ }
+ wr.WriteLine(");");
+
+ // assign to the actual LHSs
+ for (int j = 0; j < lvalues.Count; j++) {
+ Indent(indent);
+ wr.WriteLine("{0} = {1};", lvalues[j], outTmps[j]);
+ }
}
}
@@ -1651,7 +1721,7 @@ namespace Microsoft.Dafny {
}
} else if (expr is ThisExpr) {
- wr.Write("this");
+ wr.Write(enclosingMethod != null && enclosingMethod.IsTailRecursive ? "_this" : "this");
} else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 50f6859e..74e32823 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -318,8 +318,8 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
(. if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }
.)
{ Attribute<ref attrs> }
- IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
- { "," IdentType<out id, out ty> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
+ IdentType<out id, out ty, false> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
+ { "," IdentType<out id, out ty, false> (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)
}
SYNC ";"
.
@@ -342,18 +342,18 @@ GIdentType<bool allowGhostKeyword, out IToken/*!*/ id, out Type/*!*/ ty, out boo
isGhost = false; .)
[ "ghost" (. if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); } .)
]
- IdentType<out id, out ty>
+ IdentType<out id, out ty, true>
.
-IdentType<out IToken/*!*/ id, out Type/*!*/ ty>
+IdentType<out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId>
= (.Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);.)
- NoUSIdent<out id>
+ WildIdent<out id, allowWildcardId>
":"
Type<out ty>
.
LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
= (. IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
- NoUSIdent<out id>
+ WildIdent<out id, true>
[ ":" Type<out ty> (. optType = ty; .)
]
(. var = new VarDecl(id, id.val, optType == null ? new InferredTypeProxy() : optType, isGhost); .)
@@ -361,7 +361,7 @@ LocalIdentTypeOptional<out VarDecl/*!*/ var, bool isGhost>
IdentTypeOptional<out BoundVar/*!*/ var>
= (. Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
.)
- NoUSIdent<out id>
+ WildIdent<out id, true>
[ ":" Type<out ty> (. optType = ty; .)
]
(. var = new BoundVar(id, id.val, optType == null ? new InferredTypeProxy() : optType); .)
@@ -399,10 +399,10 @@ GenericParameters<.List<TypeParameter/*!*/>/*!*/ typeArgs.>
TypeParameter.EqualitySupportValue eqSupport;
.)
"<"
- NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
+ NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
- { "," NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
+ { "," NoUSIdent<out id> (. eqSupport = TypeParameter.EqualitySupportValue.Unspecified; .)
[ "(" "==" ")" (. eqSupport = TypeParameter.EqualitySupportValue.Required; .)
] (. typeArgs.Add(new TypeParameter(id, id.val, eqSupport)); .)
}
@@ -487,7 +487,7 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
( "requires" Expression<out e> SYNC ";" (. req.Add(new MaybeFreeExpression(e, isFree)); .)
| "ensures" { IF(IsAttribute()) Attribute<ref ensAttrs> } Expression<out e> SYNC ";" (. ens.Add(new MaybeFreeExpression(e, isFree, ensAttrs)); .)
)
- | "decreases" { IF(IsAttribute()) Attribute<ref decAttrs> } DecreasesList<decreases, false> SYNC ";"
+ | "decreases" { IF(IsAttribute()) Attribute<ref decAttrs> } DecreasesList<decreases, true> SYNC ";"
)
.
Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals, out IToken openParen.>
@@ -660,7 +660,7 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
]
(. if (isPredicate) {
f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,
- reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);
+ reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureOmitted);
} else if (isCoPredicate) {
f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,
reqs, reads, ens, body, attrs, signatureOmitted);
@@ -1087,13 +1087,13 @@ Invariant<out MaybeFreeExpression/*!*/ invariant>
DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>
= (. Expression/*!*/ e; .)
PossiblyWildExpression<out e> (. if (!allowWildcard && e is WildcardExpr) {
- SemErr(e.tok, "'decreases *' is only allowed on loops");
+ SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");
} else {
decreases.Add(e);
}
.)
{ "," PossiblyWildExpression<out e> (. if (!allowWildcard && e is WildcardExpr) {
- SemErr(e.tok, "'decreases *' is only allowed on loops");
+ SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");
} else {
decreases.Add(e);
}
@@ -1775,12 +1775,26 @@ Ident<out IToken/*!*/ x>
NoUSIdent<out IToken/*!*/ x>
= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
ident (. x = t;
- if (x.val.Length > 0 && x.val.StartsWith("_")) {
+ if (x.val.StartsWith("_")) {
SemErr("cannot declare identifier beginning with underscore");
}
.)
.
+// Identifier, disallowing leading underscores, except possibly the "wildcard" identifier "_"
+WildIdent<out IToken/*!*/ x, bool allowWildcardId>
+= (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)
+ ident (. x = t;
+ if (x.val.StartsWith("_")) {
+ if (allowWildcardId && x.val.Length == 1) {
+ t.val = "_v" + anonymousIds++;
+ } else {
+ SemErr("cannot declare identifier beginning with underscore");
+ }
+ }
+ .)
+ .
+
Nat<out BigInteger n>
=
digits
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 2d6d353c..c8c61c55 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -909,7 +909,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(CallGraph != null);
}
- public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase, Attributes attributes, bool isBuiltinName)
+ public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase, Attributes attributes, bool isBuiltinName)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -1279,6 +1279,9 @@ namespace Microsoft.Dafny {
string/*!*/ Name {
get;
}
+ string/*!*/ DisplayName { // what the user thinks he wrote
+ get;
+ }
string/*!*/ UniqueName {
get;
}
@@ -1303,6 +1306,12 @@ namespace Microsoft.Dafny {
throw new NotImplementedException();
}
}
+ public string DisplayName {
+ get {
+ Contract.Ensures(Contract.Result<string>() != null);
+ throw new NotImplementedException();
+ }
+ }
public string UniqueName {
get {
Contract.Ensures(Contract.Result<string>() != null);
@@ -1350,6 +1359,9 @@ namespace Microsoft.Dafny {
return name;
}
}
+ public string/*!*/ DisplayName {
+ get { return VarDecl.DisplayNameHelper(this); }
+ }
readonly int varId = varIdCount++;
public string UniqueName {
get {
@@ -1546,14 +1558,20 @@ namespace Microsoft.Dafny {
public class Predicate : Function
{
- public readonly bool BodyIsExtended; // says that this predicate definition is a refinement extension of a predicate definition is a refining module
+ public enum BodyOriginKind
+ {
+ OriginalOrInherited, // this predicate definition is new (and the predicate may or may not have a body), or the predicate's body (whether or not it exists) is being inherited unmodified (from the previous refinement--it may be that the inherited body was itself an extension, for example)
+ DelayedDefinition, // this predicate declaration provides, for the first time, a body--the declaration refines a previously declared predicate, but the previous one had no body
+ Extension // this predicate extends the definition of a predicate with a body in a module being refined
+ }
+ public readonly BodyOriginKind BodyOrigin;
public Predicate(IToken tok, string name, bool isStatic, bool isGhost,
List<TypeParameter> typeArgs, IToken openParen, List<Formal> formals,
List<Expression> req, List<FrameExpression> reads, List<Expression> ens, Specification<Expression> decreases,
- Expression body, bool bodyIsExtended, Attributes attributes, bool signatureOmitted)
+ Expression body, BodyOriginKind bodyOrigin, Attributes attributes, bool signatureOmitted)
: base(tok, name, isStatic, isGhost, typeArgs, openParen, formals, new BoolType(), req, reads, ens, decreases, body, attributes, signatureOmitted) {
- Contract.Requires(!bodyIsExtended || body != null);
- BodyIsExtended = bodyIsExtended;
+ Contract.Requires(bodyOrigin == Predicate.BodyOriginKind.OriginalOrInherited || body != null);
+ BodyOrigin = bodyOrigin;
}
}
@@ -1582,6 +1600,7 @@ namespace Microsoft.Dafny {
public readonly List<MaybeFreeExpression/*!*/>/*!*/ Ens;
public readonly Specification<Expression>/*!*/ Decreases;
public BlockStmt Body; // Body is readonly after construction, except for any kind of rewrite that may take place around the time of resolution
+ public bool IsTailRecursive; // filled in during resolution
[ContractInvariantMethod]
void ObjectInvariant() {
@@ -2224,6 +2243,17 @@ namespace Microsoft.Dafny {
return name;
}
}
+ public static bool HasWildcardName(IVariable v) {
+ Contract.Requires(v != null);
+ return v.Name.StartsWith("_");
+ }
+ public static string DisplayNameHelper(IVariable v) {
+ Contract.Requires(v != null);
+ return HasWildcardName(v) ? "_" : v.Name;
+ }
+ public string/*!*/ DisplayName {
+ get { return DisplayNameHelper(this); }
+ }
readonly int varId = NonglobalVariable.varIdCount++;
public string/*!*/ UniqueName {
get {
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index c422a619..489a233e 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -450,7 +450,7 @@ bool IsAttribute() {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
Expect(1);
x = t;
- if (x.val.Length > 0 && x.val.StartsWith("_")) {
+ if (x.val.StartsWith("_")) {
SemErr("cannot declare identifier beginning with underscore");
}
@@ -515,11 +515,11 @@ bool IsAttribute() {
while (la.kind == 6) {
Attribute(ref attrs);
}
- IdentType(out id, out ty);
+ IdentType(out id, out ty, false);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
while (la.kind == 24) {
Get();
- IdentType(out id, out ty);
+ IdentType(out id, out ty, false);
mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs));
}
while (!(la.kind == 0 || la.kind == 14)) {SynErr(123); Get();}
@@ -633,7 +633,7 @@ bool IsAttribute() {
}
if (isPredicate) {
f = new Predicate(id, id.val, mmod.IsStatic, !isFunctionMethod, typeArgs, openParen, formals,
- reqs, reads, ens, new Specification<Expression>(decreases, null), body, false, attrs, signatureOmitted);
+ reqs, reads, ens, new Specification<Expression>(decreases, null), body, Predicate.BodyOriginKind.OriginalOrInherited, attrs, signatureOmitted);
} else if (isCoPredicate) {
f = new CoPredicate(id, id.val, mmod.IsStatic, typeArgs, openParen, formals,
reqs, reads, ens, body, attrs, signatureOmitted);
@@ -754,9 +754,9 @@ bool IsAttribute() {
Expect(28);
}
- void IdentType(out IToken/*!*/ id, out Type/*!*/ ty) {
+ void IdentType(out IToken/*!*/ id, out Type/*!*/ ty, bool allowWildcardId) {
Contract.Ensures(Contract.ValueAtReturn(out id) != null); Contract.Ensures(Contract.ValueAtReturn(out ty) != null);
- NoUSIdent(out id);
+ WildIdent(out id, allowWildcardId);
Expect(5);
Type(out ty);
}
@@ -769,7 +769,21 @@ bool IsAttribute() {
Get();
if (allowGhostKeyword) { isGhost = true; } else { SemErr(t, "formal cannot be declared 'ghost' in this context"); }
}
- IdentType(out id, out ty);
+ IdentType(out id, out ty, true);
+ }
+
+ void WildIdent(out IToken/*!*/ x, bool allowWildcardId) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ Expect(1);
+ x = t;
+ if (x.val.StartsWith("_")) {
+ if (allowWildcardId && x.val.Length == 1) {
+ t.val = "_v" + anonymousIds++;
+ } else {
+ SemErr("cannot declare identifier beginning with underscore");
+ }
+ }
+
}
void Type(out Type/*!*/ ty) {
@@ -780,7 +794,7 @@ bool IsAttribute() {
void LocalIdentTypeOptional(out VarDecl/*!*/ var, bool isGhost) {
IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
- NoUSIdent(out id);
+ WildIdent(out id, true);
if (la.kind == 5) {
Get();
Type(out ty);
@@ -792,7 +806,7 @@ bool IsAttribute() {
void IdentTypeOptional(out BoundVar/*!*/ var) {
Contract.Ensures(Contract.ValueAtReturn(out var)!=null); IToken/*!*/ id; Type/*!*/ ty; Type optType = null;
- NoUSIdent(out id);
+ WildIdent(out id, true);
if (la.kind == 5) {
Get();
Type(out ty);
@@ -966,7 +980,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
while (IsAttribute()) {
Attribute(ref decAttrs);
}
- DecreasesList(decreases, false);
+ DecreasesList(decreases, true);
while (!(la.kind == 0 || la.kind == 14)) {SynErr(137); Get();}
Expect(14);
} else SynErr(138);
@@ -1018,7 +1032,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Expression/*!*/ e;
PossiblyWildExpression(out e);
if (!allowWildcard && e is WildcardExpr) {
- SemErr(e.tok, "'decreases *' is only allowed on loops");
+ SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");
} else {
decreases.Add(e);
}
@@ -1027,7 +1041,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Get();
PossiblyWildExpression(out e);
if (!allowWildcard && e is WildcardExpr) {
- SemErr(e.tok, "'decreases *' is only allowed on loops");
+ SemErr(e.tok, "'decreases *' is only allowed on loops and tail-recursive methods");
} else {
decreases.Add(e);
}
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index 7a84f86e..24941ce1 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -329,7 +329,7 @@ namespace Microsoft.Dafny {
wr.Write("ghost ");
}
if (f.HasName) {
- wr.Write("{0}: ", f.Name);
+ wr.Write("{0}: ", f.DisplayName);
}
PrintType(f.Type);
}
@@ -483,7 +483,7 @@ namespace Microsoft.Dafny {
if (s.IsGhost) {
wr.Write("ghost ");
}
- wr.Write("var {0}", s.Name);
+ wr.Write("var {0}", s.DisplayName);
PrintType(": ", s.OptionalType);
wr.Write(";");
@@ -571,7 +571,7 @@ namespace Microsoft.Dafny {
if (mc.Arguments.Count != 0) {
string sep = "(";
foreach (BoundVar bv in mc.Arguments) {
- wr.Write("{0}{1}", sep, bv.Name);
+ wr.Write("{0}{1}", sep, bv.DisplayName);
sep = ", ";
}
wr.Write(")");
@@ -605,7 +605,7 @@ namespace Microsoft.Dafny {
wr.Write("var ");
string sep = "";
foreach (var lhs in s.Lhss) {
- wr.Write("{0}{1}", sep, lhs.Name);
+ wr.Write("{0}{1}", sep, lhs.DisplayName);
PrintType(": ", lhs.OptionalType);
sep = ", ";
}
@@ -803,7 +803,7 @@ namespace Microsoft.Dafny {
if (mc.Arguments.Count != 0) {
string sep = "(";
foreach (BoundVar bv in mc.Arguments) {
- wr.Write("{0}{1}", sep, bv.Name);
+ wr.Write("{0}{1}", sep, bv.DisplayName);
sep = ", ";
}
wr.Write(")");
@@ -1134,7 +1134,7 @@ namespace Microsoft.Dafny {
wr.Write("var ");
string sep = "";
foreach (var v in e.Vars) {
- wr.Write("{0}{1}", sep, v.Name);
+ wr.Write("{0}{1}", sep, v.DisplayName);
PrintType(": ", v.Type);
sep = ", ";
}
@@ -1174,7 +1174,7 @@ namespace Microsoft.Dafny {
wr.Write("set ");
string sep = "";
foreach (BoundVar bv in e.BoundVars) {
- wr.Write("{0}{1}", sep, bv.Name);
+ wr.Write("{0}{1}", sep, bv.DisplayName);
sep = ", ";
PrintType(": ", bv.Type);
}
@@ -1194,7 +1194,7 @@ namespace Microsoft.Dafny {
wr.Write("map ");
string sep = "";
foreach (BoundVar bv in e.BoundVars) {
- wr.Write("{0}{1}", sep, bv.Name);
+ wr.Write("{0}{1}", sep, bv.DisplayName);
sep = ", ";
PrintType(": ", bv.Type);
}
@@ -1263,7 +1263,7 @@ namespace Microsoft.Dafny {
Contract.Requires(boundVars != null);
string sep = "";
foreach (BoundVar bv in boundVars) {
- wr.Write("{0}{1}", sep, bv.Name);
+ wr.Write("{0}{1}", sep, bv.DisplayName);
PrintType(": ", bv.Type);
sep = ", ";
}
diff --git a/Dafny/RefinementTransformer.cs b/Dafny/RefinementTransformer.cs
index e0f12246..6af14b14 100644
--- a/Dafny/RefinementTransformer.cs
+++ b/Dafny/RefinementTransformer.cs
@@ -473,21 +473,26 @@ namespace Microsoft.Dafny
}
Expression body;
+ Predicate.BodyOriginKind bodyOrigin;
if (replacementBody != null) {
body = replacementBody;
+ bodyOrigin = Predicate.BodyOriginKind.DelayedDefinition;
} else if (moreBody != null) {
if (f.Body == null) {
body = moreBody;
+ bodyOrigin = Predicate.BodyOriginKind.DelayedDefinition;
} else {
body = new BinaryExpr(f.tok, BinaryExpr.Opcode.And, refinementCloner.CloneExpr(f.Body), moreBody);
+ bodyOrigin = Predicate.BodyOriginKind.Extension;
}
} else {
body = refinementCloner.CloneExpr(f.Body);
+ bodyOrigin = Predicate.BodyOriginKind.OriginalOrInherited;
}
if (f is Predicate) {
return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,
- req, reads, ens, decreases, body, moreBody != null, null, false);
+ req, reads, ens, decreases, body, bodyOrigin, null, false);
} else if (f is CoPredicate) {
return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,
req, reads, ens, body, null, false);
@@ -497,14 +502,14 @@ namespace Microsoft.Dafny
}
}
- Method CloneMethod(Method m, List<MaybeFreeExpression> moreEnsures, BlockStmt replacementBody) {
+ Method CloneMethod(Method m, List<MaybeFreeExpression> moreEnsures, Specification<Expression> decreases, BlockStmt replacementBody) {
Contract.Requires(m != null);
+ Contract.Requires(decreases != null);
var tps = m.TypeArgs.ConvertAll(refinementCloner.CloneTypeParam);
var ins = m.Ins.ConvertAll(refinementCloner.CloneFormal);
var req = m.Req.ConvertAll(refinementCloner.CloneMayBeFreeExpr);
var mod = refinementCloner.CloneSpecFrameExpr(m.Mod);
- var decreases = refinementCloner.CloneSpecExpr(m.Decreases);
List<MaybeFreeExpression> ens;
if (replacementBody != null)
@@ -592,10 +597,10 @@ namespace Microsoft.Dafny
Expression moreBody = null;
Expression replacementBody = null;
- if (isPredicate) {
- moreBody = f.Body;
- } else if (prevFunction.Body == null) {
+ if (prevFunction.Body == null) {
replacementBody = f.Body;
+ } else if (isPredicate) {
+ moreBody = f.Body;
} else if (f.Body != null) {
reporter.Error(nwMember, "a refining function is not allowed to extend/change the body");
}
@@ -614,10 +619,15 @@ namespace Microsoft.Dafny
if (m.Mod.Expressions.Count != 0) {
reporter.Error(m.Mod.Expressions[0].E.tok, "a refining method is not allowed to extend the modifies clause");
}
- if (m.Decreases.Expressions.Count != 0) {
- reporter.Error(m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported");
+ Specification<Expression> decreases;
+ if (Contract.Exists(prevMethod.Decreases.Expressions, e => e is WildcardExpr)) {
+ decreases = m.Decreases;
+ } else {
+ if (m.Decreases.Expressions.Count != 0) {
+ reporter.Error(m.Decreases.Expressions[0].tok, "decreases clause on refining method not supported, unless the refined method was specified with 'decreases *'");
+ }
+ decreases = refinementCloner.CloneSpecExpr(prevMethod.Decreases);
}
-
if (prevMethod.IsStatic != m.IsStatic) {
reporter.Error(m, "a method in a refining module cannot be changed from static to non-static or vice versa: {0}", m.Name);
}
@@ -644,7 +654,7 @@ namespace Microsoft.Dafny
replacementBody = MergeBlockStmt(replacementBody, prevMethod.Body);
}
}
- nw.Members[index] = CloneMethod(prevMethod, m.Ens, replacementBody);
+ nw.Members[index] = CloneMethod(prevMethod, m.Ens, decreases, replacementBody);
}
}
}
@@ -1263,7 +1273,7 @@ namespace Microsoft.Dafny
var e = (FunctionCallExpr)expr;
if (e.Function.EnclosingClass.Module == m) {
var p = e.Function as Predicate;
- if (p != null && p.BodyIsExtended) {
+ if (p != null && p.BodyOrigin == Predicate.BodyOriginKind.Extension) {
return true;
}
}
@@ -1283,7 +1293,7 @@ namespace Microsoft.Dafny
public RefinementCloner(ModuleDefinition m) {
moduleUnderConstruction = m;
}
- override public IToken Tok(IToken tok) {
+ public override IToken Tok(IToken tok) {
return new RefinementToken(tok, moduleUnderConstruction);
}
}
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index f3fe1bf5..53449979 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -705,7 +705,7 @@ namespace Microsoft.Dafny
if (f is Predicate) {
return new Predicate(tok, f.Name, f.IsStatic, isGhost, tps, f.OpenParen, formals,
- req, reads, ens, decreases, body, false, null, false);
+ req, reads, ens, decreases, body, Predicate.BodyOriginKind.OriginalOrInherited, null, false);
} else if (f is CoPredicate) {
return new CoPredicate(tok, f.Name, f.IsStatic, tps, f.OpenParen, formals,
req, reads, ens, body, null, false);
@@ -969,13 +969,41 @@ namespace Microsoft.Dafny
if (d is ClassDecl) {
foreach (var member in ((ClassDecl)d).Members) {
if (member is Method) {
- var m = ((Method)member);
- if (m.Body != null)
+ var m = (Method)member;
+ if (m.Body != null) {
CheckTypeInference(m.Body);
+ bool tail = true;
+ bool hasTailRecursionPreference = Attributes.ContainsBool(m.Attributes, "tailrecursion", ref tail);
+ if (hasTailRecursionPreference && !tail) {
+ // the user specifically requested no tail recursion, so do nothing else
+ } else if (hasTailRecursionPreference && tail && m.IsGhost) {
+ Error(m.tok, "tail recursion can be specified only for methods that will be compiled, not for ghost methods");
+ } else {
+ var module = m.EnclosingClass.Module;
+ var sccSize = module.CallGraph.GetSCCSize(m);
+ if (hasTailRecursionPreference && 2 <= sccSize) {
+ Error(m.tok, "sorry, tail-call optimizations are not supported for mutually recursive methods");
+ } else if (hasTailRecursionPreference || sccSize == 1) {
+ CallStmt tailCall = null;
+ var status = CheckTailRecursive(m.Body.Body, m, ref tailCall, hasTailRecursionPreference);
+ if (status != TailRecursionStatus.NotTailRecursive) {
+ m.IsTailRecursive = true;
+ }
+ }
+ }
+ }
+ if (!m.IsTailRecursive && m.Body != null && Contract.Exists(m.Decreases.Expressions, e => e is WildcardExpr)) {
+ Error(m.Decreases.Expressions[0].tok, "'decreases *' is allowed only on tail-recursive methods");
+ }
} else if (member is Function) {
var f = (Function)member;
- if (f.Body != null)
+ if (f.Body != null) {
CheckTypeInference(f.Body);
+ bool tail = true;
+ if (Attributes.ContainsBool(f.Attributes, "tailrecursion", ref tail) && tail) {
+ Error(f.tok, "sorry, tail-call functions are not supported");
+ }
+ }
}
}
}
@@ -1144,6 +1172,172 @@ namespace Microsoft.Dafny
}
}
+ enum TailRecursionStatus
+ {
+ NotTailRecursive, // contains code that makes the enclosing method body not tail recursive (in way that is supported)
+ CanBeFollowedByAnything, // the code just analyzed does not do any recursive calls
+ TailCallSpent, // the method body is tail recursive, provided that all code that follows it in the method body is ghost
+ }
+
+ /// <summary>
+ /// Checks if "stmts" can be considered tail recursive, and (provided "reportsError" is true) reports an error if not.
+ /// Note, the current implementation is rather conservative in its analysis; upon need, the
+ /// algorithm could be improved.
+ /// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method.
+ ///
+ /// The incoming value of "tailCall" is not used, but it's nevertheless a 'ref' parameter to allow the
+ /// body to return the incoming value or to omit assignments to it.
+ /// If the return value is CanBeFollowedByAnything, "tailCall" is unchanged.
+ /// If the return value is TailCallSpent, "tailCall" shows one of the calls where the tail call was spent. (Note,
+ /// there could be several if the statements have branches.)
+ /// If the return value is NoTailRecursive, "tailCall" could be anything. In this case, an error
+ /// message has been reported (provided "reportsErrors" is true).
+ /// </summary>
+ TailRecursionStatus CheckTailRecursive(List<Statement> stmts, Method enclosingMethod, ref CallStmt tailCall, bool reportErrors) {
+ Contract.Requires(stmts != null);
+ var status = TailRecursionStatus.CanBeFollowedByAnything;
+ foreach (var s in stmts) {
+ if (!s.IsGhost) {
+ if (s is ReturnStmt && ((ReturnStmt)s).hiddenUpdate == null) {
+ return status;
+ }
+ if (status == TailRecursionStatus.TailCallSpent) {
+ // a tail call cannot be followed by non-ghost code
+ if (reportErrors) {
+ Error(tailCall.Tok, "this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code");
+ }
+ return TailRecursionStatus.NotTailRecursive;
+ }
+ status = CheckTailRecursive(s, enclosingMethod, ref tailCall, reportErrors);
+ if (status == TailRecursionStatus.NotTailRecursive) {
+ return status;
+ }
+ }
+ }
+ return status;
+ }
+
+ /// <summary>
+ /// See CheckTailRecursive(List Statement, ...), including its description of "tailCall".
+ /// In the current implementation, "enclosingMethod" is not allowed to be a mutually recursive method.
+ /// </summary>
+ TailRecursionStatus CheckTailRecursive(Statement stmt, Method enclosingMethod, ref CallStmt tailCall, bool reportErrors) {
+ Contract.Requires(stmt != null && !stmt.IsGhost);
+ if (stmt is PrintStmt) {
+ } else if (stmt is BreakStmt) {
+ } else if (stmt is ReturnStmt) {
+ var s = (ReturnStmt)stmt;
+ if (s.hiddenUpdate != null) {
+ return CheckTailRecursive(s.hiddenUpdate, enclosingMethod, ref tailCall, reportErrors);
+ }
+ } else if (stmt is AssignStmt) {
+ } else if (stmt is VarDecl) {
+ } else if (stmt is CallStmt) {
+ var s = (CallStmt)stmt;
+ if (s.Method == enclosingMethod) {
+ // It's a recursive call. It can be considered a tail call only if the LHS of the call are the
+ // formal out-parameters of the method
+ for (int i = 0; i < s.Lhs.Count; i++) {
+ var formal = enclosingMethod.Outs[i];
+ if (!formal.IsGhost) {
+ var lhs = s.Lhs[i] as IdentifierExpr;
+ if (lhs != null && lhs.Var == formal) {
+ // all is good
+ } else {
+ if (reportErrors) {
+ Error(s.Tok, "the recursive call to '{0}' is not tail recursive because the actual out-parameter {1} is not the formal out-parameter '{2}'", s.Method.Name, i, formal.Name);
+ }
+ return TailRecursionStatus.NotTailRecursive;
+ }
+ }
+ }
+ tailCall = s;
+ return TailRecursionStatus.TailCallSpent;
+ }
+ } else if (stmt is BlockStmt) {
+ var s = (BlockStmt)stmt;
+ return CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);
+ } else if (stmt is IfStmt) {
+ var s = (IfStmt)stmt;
+ var stThen = CheckTailRecursive(s.Thn, enclosingMethod, ref tailCall, reportErrors);
+ if (stThen == TailRecursionStatus.NotTailRecursive) {
+ return stThen;
+ }
+ var stElse = s.Els == null ? TailRecursionStatus.CanBeFollowedByAnything : CheckTailRecursive(s.Els, enclosingMethod, ref tailCall, reportErrors);
+ if (stElse == TailRecursionStatus.NotTailRecursive) {
+ return stElse;
+ } else if (stThen == TailRecursionStatus.TailCallSpent || stElse == TailRecursionStatus.TailCallSpent) {
+ return TailRecursionStatus.TailCallSpent;
+ }
+ } else if (stmt is AlternativeStmt) {
+ var s = (AlternativeStmt)stmt;
+ var status = TailRecursionStatus.CanBeFollowedByAnything;
+ foreach (var alt in s.Alternatives) {
+ var st = CheckTailRecursive(alt.Body, enclosingMethod, ref tailCall, reportErrors);
+ if (st == TailRecursionStatus.NotTailRecursive) {
+ return st;
+ } else if (st == TailRecursionStatus.TailCallSpent) {
+ status = st;
+ }
+ }
+ return status;
+ } else if (stmt is WhileStmt) {
+ var s = (WhileStmt)stmt;
+ var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);
+ if (status != TailRecursionStatus.CanBeFollowedByAnything) {
+ if (status == TailRecursionStatus.NotTailRecursive) {
+ // an error has already been reported
+ } else if (reportErrors) {
+ Error(tailCall.Tok, "a recursive call inside a loop is not recognized as being a tail call");
+ }
+ return TailRecursionStatus.NotTailRecursive;
+ }
+ } else if (stmt is AlternativeLoopStmt) {
+ var s = (AlternativeLoopStmt)stmt;
+ foreach (var alt in s.Alternatives) {
+ var status = CheckTailRecursive(alt.Body, enclosingMethod, ref tailCall, reportErrors);
+ if (status != TailRecursionStatus.CanBeFollowedByAnything) {
+ if (status == TailRecursionStatus.NotTailRecursive) {
+ // an error has already been reported
+ } else if (reportErrors) {
+ Error(tailCall.Tok, "a recursive call inside a loop is not recognized as being a tail call");
+ }
+ return TailRecursionStatus.NotTailRecursive;
+ }
+ }
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+ var status = CheckTailRecursive(s.Body, enclosingMethod, ref tailCall, reportErrors);
+ if (status != TailRecursionStatus.CanBeFollowedByAnything) {
+ if (status == TailRecursionStatus.NotTailRecursive) {
+ // an error has already been reported
+ } else if (reportErrors) {
+ Error(tailCall.Tok, "a recursive call inside a parallel statement is not a tail call");
+ }
+ return TailRecursionStatus.NotTailRecursive;
+ }
+ } else if (stmt is MatchStmt) {
+ var s = (MatchStmt)stmt;
+ var status = TailRecursionStatus.CanBeFollowedByAnything;
+ foreach (var kase in s.Cases) {
+ var st = CheckTailRecursive(kase.Body, enclosingMethod, ref tailCall, reportErrors);
+ if (st == TailRecursionStatus.NotTailRecursive) {
+ return st;
+ } else if (st == TailRecursionStatus.TailCallSpent) {
+ status = st;
+ }
+ }
+ return status;
+ } else if (stmt is AssignSuchThatStmt) {
+ } else if (stmt is ConcreteSyntaxStatement) {
+ var s = (ConcreteSyntaxStatement)stmt;
+ return CheckTailRecursive(s.ResolvedStatements, enclosingMethod, ref tailCall, reportErrors);
+ } else {
+ Contract.Assert(false); // unexpected statement type
+ }
+ return TailRecursionStatus.CanBeFollowedByAnything;
+ }
+
enum CallingPosition { Positive, Negative, Neither }
static CallingPosition Invert(CallingPosition cp) {
@@ -2096,6 +2290,9 @@ namespace Microsoft.Dafny
foreach (Expression e in m.Decreases.Expressions) {
ResolveExpression(e, false);
// any type is fine
+ if (m.IsGhost && e is WildcardExpr) {
+ Error(e, "'decreases *' is not allowed on ghost methods");
+ }
}
// Add out-parameters to a new scope that will also include the outermost-level locals of the body
@@ -3184,6 +3381,7 @@ namespace Microsoft.Dafny
foreach (var a in s.ResolvedStatements) {
ResolveStatement(a, specContextOnly, method);
}
+ s.IsGhost = s.ResolvedStatements.TrueForAll(ss => ss.IsGhost);
}
bool ResolveAlternatives(List<GuardedAlternative> alternatives, bool specContextOnly, AlternativeLoopStmt loopToCatchBreaks, Method method) {
@@ -5007,7 +5205,7 @@ namespace Microsoft.Dafny
/// -- every IntBoundedPool returned has both a lower and an upper bound
/// -- no SuperSetBoundedPool is returned
/// If "returnAllBounds" is true, then:
- /// -- a variable may give rise to BoundedPool's
+ /// -- a variable may give rise to several BoundedPool's
/// -- IntBoundedPool bounds may have just one component
/// -- a non-null return value means that some bound were found for each variable (but, for example, perhaps one
/// variable only has lower bounds, no upper bounds)
@@ -5043,7 +5241,7 @@ namespace Microsoft.Dafny
Expression lowerBound = bv.Type is NatType ? new LiteralExpr(bv.tok, new BigInteger(0)) : null;
Expression upperBound = null;
bool foundBoundsForBv = false;
- if (lowerBound != null) {
+ if (returnAllBounds && lowerBound != null) {
bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));
lowerBound = null;
foundBoundsForBv = true;
@@ -5128,8 +5326,8 @@ namespace Microsoft.Dafny
}
if ((lowerBound != null && upperBound != null) ||
(returnAllBounds && (lowerBound != null || upperBound != null))) {
- // we have found two halves
- bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));
+ // we have found two halves (or, in the case of returnAllBounds, we have found some bound)
+ bounds.Add(new ComprehensionExpr.IntBoundedPool(lowerBound, upperBound));
lowerBound = null;
upperBound = null;
foundBoundsForBv = true;
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 9966b915..f2011b72 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -5042,6 +5042,11 @@ namespace Microsoft.Dafny {
// order where elements from different Dafny types are incomparable. Thus, as an optimization below, if two
// components from different types are compared, the answer is taken to be false.
+ if (Contract.Exists(calleeDecreases, e => e is WildcardExpr)) {
+ // no check needed
+ return;
+ }
+
int N = Math.Min(contextDecreases.Count, calleeDecreases.Count);
List<IToken> toks = new List<IToken>();
List<Type> types = new List<Type>();
@@ -7456,51 +7461,58 @@ namespace Microsoft.Dafny {
if (module == currentModule && functionHeight < heightLimit) {
if (f.Body != null && !(f.Body.Resolved is MatchExpr)) {
- // inline this body
- Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
- Contract.Assert(fexp.Args.Count == f.Formals.Count);
- for (int i = 0; i < f.Formals.Count; i++) {
- Formal p = f.Formals[i];
- Expression arg = fexp.Args[i];
- arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), p.Type);
- arg.Type = p.Type; // resolve here
- substMap.Add(p, arg);
- }
- Expression body = Substitute(f.Body, fexp.Receiver, substMap);
-
- // Produce, for a "body" split into b0, b1, b2:
- // free F#canCall(args) && F(args) && (b0 && b1 && b2)
- // checked F#canCall(args) ==> F(args) || b0
- // checked F#canCall(args) ==> F(args) || b1
- // checked F#canCall(args) ==> F(args) || b2
- // Note that "body" does not contain limited calls.
-
- // F#canCall(args)
- Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);
- ExprSeq args = etran.FunctionInvocationArguments(fexp);
- Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);
-
- // F(args)
- Bpl.Expr fargs = etran.TrExpr(fexp);
-
- // body
- Bpl.Expr trBody = etran.TrExpr(body);
- trBody = etran.CondApplyUnbox(trBody.tok, trBody, f.ResultType, expr.Type);
-
- // here goes the free piece:
- splits.Add(new SplitExprInfo(true, Bpl.Expr.Binary(trBody.tok, BinaryOperator.Opcode.And, canCall, BplAnd(fargs, trBody))));
-
- // recurse on body
- var ss = new List<SplitExprInfo>();
- TrSplitExpr(body, ss, position, functionHeight, etran);
- foreach (var s in ss) {
- var unboxedConjunct = etran.CondApplyUnbox(s.E.tok, s.E, f.ResultType, expr.Type);
- var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct);
- var p = Bpl.Expr.Binary(new NestedToken(fexp.tok, s.E.tok), BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);
- splits.Add(new SplitExprInfo(s.IsFree, p));
- }
+ if (RefinementToken.IsInherited(fexp.tok, currentModule) &&
+ f is Predicate && ((Predicate)f).BodyOrigin == Predicate.BodyOriginKind.DelayedDefinition &&
+ (currentMethod == null || !currentMethod.MustReverify)) {
+ // The function was inherited as body-less but is now given a body. Don't inline the body (since, apparently, everything
+ // that needed to be proved about the function was proved already in the previous module, even without the body definition).
+ } else {
+ // inline this body
+ Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();
+ Contract.Assert(fexp.Args.Count == f.Formals.Count);
+ for (int i = 0; i < f.Formals.Count; i++) {
+ Formal p = f.Formals[i];
+ Expression arg = fexp.Args[i];
+ arg = new BoxingCastExpr(arg, cce.NonNull(arg.Type), p.Type);
+ arg.Type = p.Type; // resolve here
+ substMap.Add(p, arg);
+ }
+ Expression body = Substitute(f.Body, fexp.Receiver, substMap);
+
+ // Produce, for a "body" split into b0, b1, b2:
+ // free F#canCall(args) && F(args) && (b0 && b1 && b2)
+ // checked F#canCall(args) ==> F(args) || b0
+ // checked F#canCall(args) ==> F(args) || b1
+ // checked F#canCall(args) ==> F(args) || b2
+ // Note that "body" does not contain limited calls.
+
+ // F#canCall(args)
+ Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);
+ ExprSeq args = etran.FunctionInvocationArguments(fexp);
+ Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);
+
+ // F(args)
+ Bpl.Expr fargs = etran.TrExpr(fexp);
+
+ // body
+ Bpl.Expr trBody = etran.TrExpr(body);
+ trBody = etran.CondApplyUnbox(trBody.tok, trBody, f.ResultType, expr.Type);
+
+ // here goes the free piece:
+ splits.Add(new SplitExprInfo(true, Bpl.Expr.Binary(trBody.tok, BinaryOperator.Opcode.And, canCall, BplAnd(fargs, trBody))));
+
+ // recurse on body
+ var ss = new List<SplitExprInfo>();
+ TrSplitExpr(body, ss, position, functionHeight, etran);
+ foreach (var s in ss) {
+ var unboxedConjunct = etran.CondApplyUnbox(s.E.tok, s.E, f.ResultType, expr.Type);
+ var bodyOrConjunct = Bpl.Expr.Or(fargs, unboxedConjunct);
+ var p = Bpl.Expr.Binary(new NestedToken(fexp.tok, s.E.tok), BinaryOperator.Opcode.Imp, canCall, bodyOrConjunct);
+ splits.Add(new SplitExprInfo(s.IsFree, p));
+ }
- return true;
+ return true;
+ }
}
}
}
@@ -7600,6 +7612,8 @@ namespace Microsoft.Dafny {
translatedExpression = etran.TrExpr(expr);
splitHappened = etran.Statistics_CustomLayerFunctionCount != 0; // return true if the LayerOffset(1) came into play
}
+ // TODO: Is the the following call to ContainsChange expensive? It's linear in the size of "expr", but we get here many times in TrSpliExpr, so wouldn't the total
+ // time in the size of the expression passed to the first TrSpliExpr be quadratic?
if (RefinementToken.IsInherited(expr.tok, currentModule) && (currentMethod == null || !currentMethod.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule)) {
// If "expr" contains a subexpression that has changed from the inherited expression, we'll destructively
// change the token of the translated expression to make it look like it's not inherited. This will cause "e" to
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 06:49:42 +0000