summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/DafnyAst.cs60
-rw-r--r--Source/Dafny/Printer.cs5
-rw-r--r--Source/Dafny/Resolver.cs121
-rw-r--r--Source/Dafny/Translator.cs248
-rw-r--r--Test/dafny0/Answer72
-rw-r--r--Test/dafny0/Iterators.dfy145
-rw-r--r--Test/dafny0/ResolutionErrors.dfy95
-rw-r--r--Test/dafny0/StatementExpressions.dfy58
-rw-r--r--Test/dafny0/runtest.bat2
9 files changed, 597 insertions, 209 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 21435f76..bfd9e633 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -977,8 +977,8 @@ namespace Microsoft.Dafny {
public ModuleDecl RefinementBaseRoot; // filled in early during resolution, corresponds to RefinementBaseName[0]
public ModuleDefinition RefinementBase; // filled in during resolution (null if no refinement base)
- public readonly List<TopLevelDecl/*!*/> TopLevelDecls = new List<TopLevelDecl/*!*/>(); // filled in by the parser; readonly after that
- public readonly Graph<MemberDecl/*!*/> CallGraph = new Graph<MemberDecl/*!*/>(); // filled in during resolution
+ public readonly List<TopLevelDecl> TopLevelDecls = new List<TopLevelDecl>(); // filled in by the parser; readonly after that
+ public readonly Graph<ICallable> CallGraph = new Graph<ICallable>(); // filled in during resolution
public int Height; // height in the topological sorting of modules; filled in during resolution
public readonly bool IsAbstract;
public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface)
@@ -1261,19 +1261,34 @@ namespace Microsoft.Dafny {
}
}
- public interface ICodeContext : ICallable
+ /// <summary>
+ /// An ICodeContext is a Function, Method, or IteratorDecl, or a NoContext.
+ /// </summary>
+ public interface ICodeContext
{
bool IsGhost { get; }
bool IsStatic { get; }
List<TypeParameter> TypeArgs { get; }
List<Formal> Ins { get ; }
- List<Formal> Outs { get; }
- Specification<FrameExpression> Modifies { get; }
- Specification<Expression> Decreases { get; }
ModuleDefinition EnclosingModule { get; } // to be called only after signature-resolution is complete
bool MustReverify { get; }
string FullSanitizedName { get; }
}
+ /// <summary>
+ /// An ICallable is a Function, Method, or IteratorDecl.
+ /// </summary>
+ public interface ICallable : ICodeContext
+ {
+ Specification<Expression> Decreases { get; }
+ }
+ /// <summary>
+ /// An IMethodCodeContext is a Method or IteratorDecl.
+ /// </summary>
+ public interface IMethodCodeContext : ICallable
+ {
+ List<Formal> Outs { get; }
+ Specification<FrameExpression> Modifies { get; }
+ }
/// <summary>
/// Applies when we are neither inside a method, nor iterator.
@@ -1289,15 +1304,13 @@ namespace Microsoft.Dafny {
bool ICodeContext.IsStatic { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
List<TypeParameter> ICodeContext.TypeArgs { get { return new List<TypeParameter>(); } }
List<Formal> ICodeContext.Ins { get { return new List<Formal>(); } }
- List<Formal> ICodeContext.Outs { get { return new List<Formal>(); } }
- Specification<FrameExpression> ICodeContext.Modifies { get { return new Specification<FrameExpression>(null, null); } }
- Specification<Expression> ICodeContext.Decreases { get { return new Specification<Expression>(null, null); } }
+ Specification<Expression> Decreases { get { return new Specification<Expression>(null, null); } }
ModuleDefinition ICodeContext.EnclosingModule { get { return Module; } }
bool ICodeContext.MustReverify { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
public string FullSanitizedName { get { Contract.Assume(false, "should not be called on NoContext"); throw new cce.UnreachableException(); } }
}
- public class IteratorDecl : ClassDecl, ICodeContext
+ public class IteratorDecl : ClassDecl, IMethodCodeContext
{
public readonly List<Formal> Ins;
public readonly List<Formal> Outs;
@@ -1364,18 +1377,13 @@ namespace Microsoft.Dafny {
bool ICodeContext.IsStatic { get { return true; } }
List<TypeParameter> ICodeContext.TypeArgs { get { return this.TypeArgs; } }
List<Formal> ICodeContext.Ins { get { return this.Ins; } }
- List<Formal> ICodeContext.Outs { get { return this.Outs; } }
- Specification<FrameExpression> ICodeContext.Modifies { get { return this.Modifies; } }
- Specification<Expression> ICodeContext.Decreases { get { return this.Decreases; } }
+ List<Formal> IMethodCodeContext.Outs { get { return this.Outs; } }
+ Specification<FrameExpression> IMethodCodeContext.Modifies { get { return this.Modifies; } }
+ Specification<Expression> ICallable.Decreases { get { return this.Decreases; } }
ModuleDefinition ICodeContext.EnclosingModule { get { return this.Module; } }
bool ICodeContext.MustReverify { get { return false; } }
}
- /// <summary>
- /// An "ICallable" is a function, method, or iterator.
- /// </summary>
- public interface ICallable { }
-
public abstract class MemberDecl : Declaration {
public readonly bool IsStatic;
public readonly bool IsGhost;
@@ -1854,6 +1862,14 @@ namespace Microsoft.Dafny {
this.Body = body;
this.SignatureIsOmitted = signatureOmitted;
}
+
+ bool ICodeContext.IsGhost { get { return this.IsGhost; } }
+ bool ICodeContext.IsStatic { get { return this.IsStatic; } }
+ List<TypeParameter> ICodeContext.TypeArgs { get { return this.TypeArgs; } }
+ List<Formal> ICodeContext.Ins { get { return this.Formals; } }
+ Specification<Expression> ICallable.Decreases { get { return this.Decreases; } }
+ ModuleDefinition ICodeContext.EnclosingModule { get { return this.EnclosingClass.Module; } }
+ bool ICodeContext.MustReverify { get { return false; } }
}
public class Predicate : Function
@@ -1929,7 +1945,7 @@ namespace Microsoft.Dafny {
}
}
- public class Method : MemberDecl, TypeParameter.ParentType, ICodeContext
+ public class Method : MemberDecl, TypeParameter.ParentType, IMethodCodeContext
{
public readonly bool SignatureIsOmitted;
public bool MustReverify;
@@ -1989,9 +2005,9 @@ namespace Microsoft.Dafny {
bool ICodeContext.IsStatic { get { return this.IsStatic; } }
List<TypeParameter> ICodeContext.TypeArgs { get { return this.TypeArgs; } }
List<Formal> ICodeContext.Ins { get { return this.Ins; } }
- List<Formal> ICodeContext.Outs { get { return this.Outs; } }
- Specification<FrameExpression> ICodeContext.Modifies { get { return Mod; } }
- Specification<Expression> ICodeContext.Decreases { get { return this.Decreases; } }
+ List<Formal> IMethodCodeContext.Outs { get { return this.Outs; } }
+ Specification<FrameExpression> IMethodCodeContext.Modifies { get { return Mod; } }
+ Specification<Expression> ICallable.Decreases { get { return this.Decreases; } }
ModuleDefinition ICodeContext.EnclosingModule {
get {
Contract.Assert(this.EnclosingClass != null); // this getter is supposed to be called only after signature-resolution is complete
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index a3122050..0a05e817 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1413,9 +1413,10 @@ namespace Microsoft.Dafny {
var e = (CalcExpr)expr;
bool parensNeeded = !isRightmost;
if (parensNeeded) { wr.Write("("); }
- PrintStatement(e.Guard, indent);
+ int ind = indent < 0 ? IndentAmount : indent; // if the expression was to be printed on one line, instead print the calc statement part at indentation IndentAmount (not pretty, but something)
+ PrintStatement(e.Guard, ind);
wr.WriteLine();
- Indent(indent);
+ Indent(ind);
PrintExpression(e.Body);
if (parensNeeded) { wr.Write(")"); }
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 22f7d95c..f04c17a6 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -584,7 +584,7 @@ namespace Microsoft.Dafny
}
// finally, add special variables to hold the components of the (explicit or implicit) decreases clause
bool inferredDecreases;
- var decr = Translator.MethodDecreasesWithDefault(iter, out inferredDecreases);
+ var decr = Translator.CallableDecreasesWithDefault(iter, null, out inferredDecreases);
if (inferredDecreases) {
iter.InferredDecreases = true;
Contract.Assert(iter.Decreases.Expressions.Count == 0);
@@ -1274,8 +1274,8 @@ namespace Microsoft.Dafny
if (fn.Body != null && module.CallGraph.GetSCCRepresentative(fn) == fn) {
bool dealsWithCodatatypes = false;
foreach (var m in module.CallGraph.GetSCC(fn)) {
- var f = (Function)m;
- if (f.ResultType.InvolvesCoDatatype) {
+ var f = m as Function;
+ if (f != null && f.ResultType.InvolvesCoDatatype) {
dealsWithCodatatypes = true;
break;
}
@@ -1283,11 +1283,13 @@ namespace Microsoft.Dafny
var coCandidates = new List<CoCallResolution.CoCallInfo>();
var hasIntraClusterCallsInDestructiveContexts = false;
foreach (var m in module.CallGraph.GetSCC(fn)) {
- var f = (Function)m;
- var checker = new CoCallResolution(f, dealsWithCodatatypes);
- checker.CheckCoCalls(f.Body);
- coCandidates.AddRange(checker.FinalCandidates);
- hasIntraClusterCallsInDestructiveContexts |= checker.HasIntraClusterCallsInDestructiveContexts;
+ if (m is Function) {
+ var f = (Function)m;
+ var checker = new CoCallResolution(f, dealsWithCodatatypes);
+ checker.CheckCoCalls(f.Body);
+ coCandidates.AddRange(checker.FinalCandidates);
+ hasIntraClusterCallsInDestructiveContexts |= checker.HasIntraClusterCallsInDestructiveContexts;
+ }
}
if (coCandidates.Count != 0) {
if (hasIntraClusterCallsInDestructiveContexts) {
@@ -2255,7 +2257,6 @@ namespace Microsoft.Dafny
}
ClassDecl currentClass;
- Function currentFunction;
readonly Scope<TypeParameter>/*!*/ allTypeParameters = new Scope<TypeParameter>();
readonly Scope<IVariable>/*!*/ scope = new Scope<IVariable>();
Scope<Statement>/*!*/ labeledStatements = new Scope<Statement>();
@@ -2677,42 +2678,39 @@ namespace Microsoft.Dafny
/// </summary>
void ResolveFunction(Function f) {
Contract.Requires(f != null);
- Contract.Requires(currentFunction == null);
- Contract.Ensures(currentFunction == null);
scope.PushMarker();
- currentFunction = f;
if (f.IsStatic) {
scope.AllowInstance = false;
}
foreach (Formal p in f.Formals) {
scope.Push(p.Name, p);
}
- ResolveAttributes(f.Attributes, false, new NoContext(currentClass.Module));
+ ResolveAttributes(f.Attributes, false, f);
foreach (Expression r in f.Req) {
- ResolveExpression(r, false, new NoContext(currentFunction.EnclosingClass.Module));
+ ResolveExpression(r, false, f);
Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(r.Type, Type.Bool)) {
Error(r, "Precondition must be a boolean (got {0})", r.Type);
}
}
foreach (FrameExpression fr in f.Reads) {
- ResolveFrameExpression(fr, "reads");
+ ResolveFrameExpression(fr, "reads", f);
}
foreach (Expression r in f.Ens) {
- ResolveExpression(r, false, new NoContext(currentClass.Module)); // since this is a function, the postcondition is still a one-state predicate
+ ResolveExpression(r, false, f); // since this is a function, the postcondition is still a one-state predicate
Contract.Assert(r.Type != null); // follows from postcondition of ResolveExpression
if (!UnifyTypes(r.Type, Type.Bool)) {
Error(r, "Postcondition must be a boolean (got {0})", r.Type);
}
}
foreach (Expression r in f.Decreases.Expressions) {
- ResolveExpression(r, false, new NoContext(currentClass.Module));
+ ResolveExpression(r, false, f);
// any type is fine
}
if (f.Body != null) {
var prevErrorCount = ErrorCount;
List<IVariable> matchVarContext = new List<IVariable>(f.Formals);
- ResolveExpression(f.Body, false, new NoContext(currentClass.Module), matchVarContext);
+ ResolveExpression(f.Body, false, f, matchVarContext);
if (!f.IsGhost) {
CheckIsNonGhost(f.Body);
}
@@ -2721,14 +2719,14 @@ namespace Microsoft.Dafny
Error(f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
}
}
- currentFunction = null;
scope.PopMarker();
}
- void ResolveFrameExpression(FrameExpression fe, string kind) {
+ void ResolveFrameExpression(FrameExpression fe, string kind, ICodeContext codeContext) {
Contract.Requires(fe != null);
- Contract.Requires(kind != null);
- ResolveExpression(fe.E, false, new NoContext(moduleInfo.ModuleDef));
+ Contract.Requires(kind != null);
+ Contract.Requires(codeContext != null);
+ ResolveExpression(fe.E, false, codeContext);
Type t = fe.E.Type;
Contract.Assert(t != null); // follows from postcondition of ResolveExpression
if (t is CollectionType) {
@@ -2810,7 +2808,7 @@ namespace Microsoft.Dafny
}
}
foreach (FrameExpression fe in m.Mod.Expressions) {
- ResolveFrameExpression(fe, "modifies");
+ ResolveFrameExpression(fe, "modifies", m);
if (m is Lemma) {
Error(fe.tok, "lemmas are not allowed to have modifies clauses");
} else if (m is CoMethod) {
@@ -2925,10 +2923,10 @@ namespace Microsoft.Dafny
}
}
foreach (FrameExpression fe in iter.Reads.Expressions) {
- ResolveFrameExpression(fe, "reads");
+ ResolveFrameExpression(fe, "reads", iter);
}
foreach (FrameExpression fe in iter.Modifies.Expressions) {
- ResolveFrameExpression(fe, "modifies");
+ ResolveFrameExpression(fe, "modifies", iter);
}
foreach (MaybeFreeExpression e in iter.Requires) {
ResolveExpression(e.E, false, iter);
@@ -3672,14 +3670,17 @@ namespace Microsoft.Dafny
}
var s = (ProduceStmt)stmt;
if (s.rhss != null) {
- if (codeContext.Outs.Count != s.rhss.Count)
- Error(s, "number of {2} parameters does not match declaration (found {0}, expected {1})", s.rhss.Count, codeContext.Outs.Count, kind);
+ var cmc = codeContext as IMethodCodeContext;
+ if (cmc == null) {
+ // an error has already been reported above
+ } else if (cmc.Outs.Count != s.rhss.Count)
+ Error(s, "number of {2} parameters does not match declaration (found {0}, expected {1})", s.rhss.Count, cmc.Outs.Count, kind);
else {
Contract.Assert(s.rhss.Count > 0);
// Create a hidden update statement using the out-parameter formals, resolve the RHS, and check that the RHS is good.
List<Expression> formals = new List<Expression>();
int i = 0;
- foreach (Formal f in codeContext.Outs) {
+ foreach (Formal f in cmc.Outs) {
Expression produceLhs;
if (stmt is ReturnStmt) {
var ident = new IdentifierExpr(f.tok, f.Name);
@@ -3919,7 +3920,7 @@ namespace Microsoft.Dafny
if (s.Mod.Expressions != null) {
foreach (FrameExpression fe in s.Mod.Expressions) {
- ResolveFrameExpression(fe, "modifies");
+ ResolveFrameExpression(fe, "modifies", codeContext);
}
}
s.IsGhost = bodyMustBeSpecOnly;
@@ -4224,6 +4225,7 @@ namespace Microsoft.Dafny
/// </summary>
private void ResolveUpdateStmt(UpdateStmt update, bool specContextOnly, ICodeContext codeContext, int errorCountBeforeCheckingLhs) {
Contract.Requires(update != null);
+ Contract.Requires(codeContext != null);
IToken firstEffectfulRhs = null;
CallRhs callRhs = null;
foreach (var rhs in update.Rhss) {
@@ -4326,6 +4328,7 @@ namespace Microsoft.Dafny
private void ResolveAssignSuchThatStmt(AssignSuchThatStmt s, bool specContextOnly, ICodeContext codeContext) {
Contract.Requires(s != null);
+ Contract.Requires(codeContext != null);
var varLhss = new List<IVariable>();
if (s.AssumeToken == null) {
@@ -4548,12 +4551,15 @@ namespace Microsoft.Dafny
ModuleDefinition callerModule = codeContext.EnclosingModule;
ModuleDefinition calleeModule = ((ICodeContext)callee).EnclosingModule;
if (callerModule == calleeModule) {
- // intra-module call; this is allowed; add edge in module's call graph
- var caller = codeContext is Method ? (Method)codeContext : ((IteratorDecl)codeContext).Member_MoveNext;
- callerModule.CallGraph.AddEdge(caller, callee);
- } else {
- //Contract.Assert(dependencies.Reaches(callerModule, calleeModule));
- //
+ // intra-module call; add edge in module's call graph
+ var caller = codeContext as ICallable;
+ if (caller == null) {
+ // don't add anything to the call graph after all
+ } else if (caller is IteratorDecl) {
+ callerModule.CallGraph.AddEdge(((IteratorDecl)caller).Member_MoveNext, callee);
+ } else {
+ callerModule.CallGraph.AddEdge(caller, callee);
+ }
}
}
}
@@ -4795,7 +4801,10 @@ namespace Microsoft.Dafny
}
} else if (stmt is WhileStmt) {
- WhileStmt s = (WhileStmt)stmt;
+ var s = (WhileStmt)stmt;
+ if (s.Mod.Expressions != null && s.Mod.Expressions.Count != 0) {
+ Error(s.Mod.Expressions[0].tok, "a while statement used inside a hint is not allowed to have a modifies clause");
+ }
CheckHintRestrictions(s.Body);
} else if (stmt is AlternativeLoopStmt) {
@@ -4842,12 +4851,10 @@ namespace Microsoft.Dafny
void CheckHintLhs(IToken tok, Expression lhs) {
var idExpr = lhs as IdentifierExpr;
- if (idExpr != null) {
- if (scope.ContainsDecl(idExpr.Var)) {
- Error(tok, "a hint is not allowed to update a variable declared outside the hint");
- }
- } else {
+ if (idExpr == null) {
Error(tok, "a hint is not allowed to update heap locations");
+ } else if (scope.ContainsDecl(idExpr.Var)) {
+ Error(tok, "a hint is not allowed to update a variable declared outside the hint");
}
}
@@ -5657,7 +5664,7 @@ namespace Microsoft.Dafny
if (missingBounds.Count != 0) {
// Report errors here about quantifications that depend on the allocation state.
var mb = missingBounds;
- if (currentFunction != null) {
+ if (codeContext is Function) {
mb = new List<BoundVar>(); // (who cares if we allocate another array; this happens only in the case of a resolution error anyhow)
foreach (var bv in missingBounds) {
if (bv.Type.IsRefType) {
@@ -5764,11 +5771,8 @@ namespace Microsoft.Dafny
ResolveStatement(e.Guard, twoState, codeContext);
ResolveExpression(e.Body, twoState, codeContext);
Contract.Assert(e.Body.Type != null); // follows from postcondition of ResolveExpression
- if (prevErrorCount == ErrorCount) {
- // Do not build AsAssumeExpression if there were errors, because e.Guard.Result might be null
- e.AsAssumeExpr = new AssumeExpr(e.tok, e.Guard.Result, e.Body);
- ResolveExpression(e.AsAssumeExpr, twoState, codeContext);
- }
+ e.AsAssumeExpr = new AssumeExpr(e.tok, prevErrorCount == ErrorCount ? e.Guard.Result : new LiteralExpr(e.tok, true), e.Body);
+ ResolveExpression(e.AsAssumeExpr, twoState, codeContext);
expr.Type = e.Body.Type;
} else if (expr is ITEExpr) {
@@ -6189,17 +6193,20 @@ namespace Microsoft.Dafny
}
// Resolution termination check
- if (currentFunction != null && currentFunction.EnclosingClass != null && function.EnclosingClass != null) {
- ModuleDefinition callerModule = currentFunction.EnclosingClass.Module;
- ModuleDefinition calleeModule = function.EnclosingClass.Module;
- if (callerModule == calleeModule) {
- // intra-module call; this is allowed; add edge in module's call graph
- callerModule.CallGraph.AddEdge(currentFunction, function);
- if (currentFunction == function) {
- currentFunction.IsRecursive = true; // self recursion (mutual recursion is determined elsewhere)
- }
+ ModuleDefinition callerModule = codeContext.EnclosingModule;
+ ModuleDefinition calleeModule = function.EnclosingClass.Module;
+ if (callerModule == calleeModule) {
+ // intra-module call; add edge in module's call graph
+ var caller = codeContext as ICallable;
+ if (caller == null) {
+ // don't add anything to the call graph after all
+ } else if (caller is IteratorDecl) {
+ callerModule.CallGraph.AddEdge(((IteratorDecl)codeContext).Member_MoveNext, function);
} else {
- //Contract.Assert(dependencies.Reaches(callerModule, calleeModule));
+ callerModule.CallGraph.AddEdge(caller, function);
+ if (caller == function) {
+ function.IsRecursive = true; // self recursion (mutual recursion is determined elsewhere)
+ }
}
}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index e6e0a7dd..a2fd8eef 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2204,7 +2204,7 @@ namespace Microsoft.Dafny {
}
ModuleDefinition currentModule = null; // the name of the module whose members are currently being translated
- ICodeContext codeContext = null; // the method/iterator whose implementation is currently being translated
+ ICallable codeContext = null; // the method/iterator whose implementation is currently being translated or the function whose specification is being checked for well-formedness
LocalVariable yieldCountVariable = null; // non-null when an iterator body is being translated
bool assertAsAssume = false; // generate assume statements instead of assert statements
int loopHeapVarCount = 0;
@@ -2391,7 +2391,7 @@ namespace Microsoft.Dafny {
var decrCallee = new List<Expr>();
var decrCaller = new List<Expr>();
bool decrInferred; // we don't actually care
- foreach (var ee in MethodDecreasesWithDefault(m, out decrInferred)) {
+ foreach (var ee in CallableDecreasesWithDefault(m, out decrInferred)) {
decrToks.Add(ee.tok);
decrTypes.Add(ee.Type);
decrCaller.Add(exprTran.TrExpr(ee));
@@ -2673,15 +2673,14 @@ namespace Microsoft.Dafny {
builder.Add(Bpl.Cmd.SimpleAssign(tok, new Bpl.IdentifierExpr(tok, frame), lambda));
}
- void CheckFrameSubset(IToken tok, List<FrameExpression/*!*/>/*!*/ calleeFrame,
+ void CheckFrameSubset(IToken tok, List<FrameExpression> calleeFrame,
Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/> substMap,
ExpressionTranslator/*!*/ etran, Bpl.StmtListBuilder/*!*/ builder, string errorMessage,
Bpl.QKeyValue kv)
{
Contract.Requires(tok != null);
- Contract.Requires(cce.NonNullElements(calleeFrame));
+ Contract.Requires(calleeFrame != null);
Contract.Requires((receiverReplacement == null) == (substMap == null));
- Contract.Requires(substMap == null || cce.NonNullDictionaryAndValues(substMap));
Contract.Requires(etran != null);
Contract.Requires(builder != null);
Contract.Requires(errorMessage != null);
@@ -2947,10 +2946,11 @@ namespace Microsoft.Dafny {
Contract.Requires(f != null);
Contract.Requires(sink != null && predef != null);
Contract.Requires(f.EnclosingClass != null);
- Contract.Requires(currentModule == null);
- Contract.Ensures(currentModule == null);
+ Contract.Requires(currentModule == null && codeContext == null);
+ Contract.Ensures(currentModule == null && codeContext == null);
currentModule = f.EnclosingClass.Module;
+ codeContext = f;
ExpressionTranslator etran = new ExpressionTranslator(this, predef, f.tok);
// parameters of the procedure
@@ -2971,11 +2971,13 @@ namespace Microsoft.Dafny {
// the procedure itself
var req = new List<Bpl.Requires>();
// free requires mh == ModuleContextHeight && fh == FunctionContextHeight;
- ModuleDefinition mod = f.EnclosingClass.Module;
+ ModuleDefinition module = f.EnclosingClass.Module;
Bpl.Expr context = Bpl.Expr.And(
- Bpl.Expr.Eq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),
- Bpl.Expr.Eq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()));
+ Bpl.Expr.Eq(Bpl.Expr.Literal(module.Height), etran.ModuleContextHeight()),
+ Bpl.Expr.Eq(Bpl.Expr.Literal(module.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()));
req.Add(Requires(f.tok, true, context, null, null));
+ // modifies $Heap, $Tick
+ var mod = new List<Bpl.IdentifierExpr> { (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr, etran.Tick() };
// check that postconditions hold
var ens = new List<Bpl.Ensures>();
foreach (Expression p in f.Ens) {
@@ -2989,7 +2991,7 @@ namespace Microsoft.Dafny {
}
}
Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullSanitizedName, typeParams, inParams, new List<Variable>(),
- req, new List<Bpl.IdentifierExpr>(), ens, etran.TrAttributes(f.Attributes, null));
+ req, mod, ens, etran.TrAttributes(f.Attributes, null));
sink.TopLevelDeclarations.Add(proc);
if (InsertChecksums)
@@ -3005,7 +3007,7 @@ namespace Microsoft.Dafny {
// check well-formedness of the preconditions (including termination, but no reads checks), and then
// assume each one of them
foreach (Expression p in f.Req) {
- CheckWellformed(p, new WFOptions(f, null, false), locals, builder, etran);
+ CheckWellformed(p, new WFOptions(null, false), locals, builder, etran);
builder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));
}
// check well-formedness of the reads clause
@@ -3013,7 +3015,7 @@ namespace Microsoft.Dafny {
// check well-formedness of the decreases clauses (including termination, but no reads checks)
foreach (Expression p in f.Decreases.Expressions)
{
- CheckWellformed(p, new WFOptions(f, null, false), locals, builder, etran);
+ CheckWellformed(p, new WFOptions(null, false), locals, builder, etran);
}
// Generate:
// if (*) {
@@ -3048,7 +3050,7 @@ namespace Microsoft.Dafny {
}
// Now for the ensures clauses
foreach (Expression p in f.Ens) {
- CheckWellformed(p, new WFOptions(f, f, false), locals, postCheckBuilder, etran);
+ CheckWellformed(p, new WFOptions(f, false), locals, postCheckBuilder, etran);
// assume the postcondition for the benefit of checking the remaining postconditions
postCheckBuilder.Add(new Bpl.AssumeCmd(p.tok, etran.TrExpr(p)));
}
@@ -3070,7 +3072,7 @@ namespace Microsoft.Dafny {
Bpl.Expr funcAppl = new Bpl.NAryExpr(f.tok, funcID, args);
DefineFrame(f.tok, f.Reads, bodyCheckBuilder, locals, null);
- CheckWellformedWithResult(f.Body, new WFOptions(f, null, true), funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);
+ CheckWellformedWithResult(f.Body, new WFOptions(null, true), funcAppl, f.ResultType, locals, bodyCheckBuilder, etran);
}
// Combine the two, letting the postcondition be checked on after the "bodyCheckBuilder" branch
postCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False));
@@ -3087,7 +3089,9 @@ namespace Microsoft.Dafny {
}
Contract.Assert(currentModule == f.EnclosingClass.Module);
+ Contract.Assert(codeContext == f);
currentModule = null;
+ codeContext = null;
}
Bpl.Expr CtorInvocation(MatchCase mc, ExpressionTranslator etran, List<Variable> locals, StmtListBuilder localTypeAssumptions) {
@@ -3440,8 +3444,6 @@ namespace Microsoft.Dafny {
/// <summary>
/// Instances of WFContext are used as an argument to CheckWellformed, supplying options for the
/// checks to be performed.
- /// If non-null, "Decr" gives the caller to be used for termination checks. If it is null, no
- /// termination checks are performed.
/// If "SelfCallsAllowance" is non-null, termination checks will be omitted for calls that look
/// like it. This is useful in function postconditions, where the result of the function is
/// syntactically given as what looks like a recursive call with the same arguments.
@@ -3450,13 +3452,11 @@ namespace Microsoft.Dafny {
/// </summary>
class WFOptions
{
- public readonly Function Decr;
public readonly Function SelfCallsAllowance;
public readonly bool DoReadsChecks;
public readonly Bpl.QKeyValue AssertKv;
public WFOptions() { }
- public WFOptions(Function decr, Function selfCallsAllowance, bool doReadsChecks) {
- Decr = decr;
+ public WFOptions(Function selfCallsAllowance, bool doReadsChecks) {
SelfCallsAllowance = selfCallsAllowance;
DoReadsChecks = doReadsChecks;
}
@@ -3566,7 +3566,7 @@ namespace Microsoft.Dafny {
builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "upper bound " + (e.E0 == null ? "" : "below lower bound or ") + "above length of " + (isSequence ? "sequence" : "array"), options.AssertKv));
}
}
- if (options.DoReadsChecks && cce.NonNull(e.Seq.Type).IsArrayType) {
+ if (options.DoReadsChecks && e.Seq.Type.IsArrayType) {
if (e.SelectOne) {
Contract.Assert(e.E0 != null);
Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, etran.TrExpr(e.E0));
@@ -3669,59 +3669,57 @@ namespace Microsoft.Dafny {
Expression precond = Substitute(p, e.Receiver, substMap);
builder.Add(Assert(expr.tok, etran.TrExpr(precond), "possible violation of function precondition", options.AssertKv));
}
+ if (options.DoReadsChecks) {
+ // check that the callee reads only what the caller is already allowed to read
+ CheckFrameSubset(expr.tok, e.Function.Reads, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function", options.AssertKv);
+ }
+
Bpl.Expr allowance = null;
- if (options.Decr != null || options.DoReadsChecks) {
- if (options.DoReadsChecks) {
- // check that the callee reads only what the caller is already allowed to read
- CheckFrameSubset(expr.tok, e.Function.Reads, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function", options.AssertKv);
- }
-
- if (options.Decr != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes && !(e.Function is CoPredicate)) {
- // check that the decreases measure goes down
- ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module;
- if (module == cce.NonNull(options.Decr.EnclosingClass).Module) {
- if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(options.Decr)) {
- bool contextDecrInferred, calleeDecrInferred;
- List<Expression> contextDecreases = FunctionDecreasesWithDefault(options.Decr, out contextDecrInferred);
- List<Expression> calleeDecreases = FunctionDecreasesWithDefault(e.Function, out calleeDecrInferred);
- if (e.Function == options.SelfCallsAllowance) {
- allowance = Bpl.Expr.True;
- if (!e.Function.IsStatic) {
- allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(e.Receiver), new Bpl.IdentifierExpr(e.tok, etran.This, predef.RefType)));
- }
- for (int i = 0; i < e.Args.Count; i++) {
- Expression ee = e.Args[i];
- Formal ff = e.Function.Formals[i];
- allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(ee), new Bpl.IdentifierExpr(e.tok, ff.AssignUniqueName(currentDeclaration), TrType(ff.Type))));
- }
+ if (codeContext != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes && !(e.Function is CoPredicate)) {
+ // check that the decreases measure goes down
+ ModuleDefinition module = cce.NonNull(e.Function.EnclosingClass).Module;
+ if (module == codeContext.EnclosingModule) {
+ if (module.CallGraph.GetSCCRepresentative(e.Function) == module.CallGraph.GetSCCRepresentative(codeContext)) {
+ bool contextDecrInferred, calleeDecrInferred;
+ List<Expression> contextDecreases = CallableDecreasesWithDefault(codeContext, out contextDecrInferred);
+ List<Expression> calleeDecreases = CallableDecreasesWithDefault(e.Function, out calleeDecrInferred);
+ if (e.Function == options.SelfCallsAllowance) {
+ allowance = Bpl.Expr.True;
+ if (!e.Function.IsStatic) {
+ allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(e.Receiver), new Bpl.IdentifierExpr(e.tok, etran.This, predef.RefType)));
}
- string hint;
- switch (e.CoCall) {
- case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects:
- hint = "note that only functions without side effects can be called co-recursively";
- break;
- case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition:
- hint = "note that only functions without any ensures clause can be called co-recursively";
- break;
- case FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded:
- hint = "note that the call is not sufficiently guarded to be used co-recursively";
- break;
- case FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsAreNotAllowedInThisContext:
- hint = "note that calls cannot be co-recursive in this context";
- break;
- case FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext:
- hint = "note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts";
- break;
- case FunctionCallExpr.CoCallResolution.No:
- hint = null;
- break;
- default:
- Contract.Assert(false); // unexpected CoCallResolution
- goto case FunctionCallExpr.CoCallResolution.No; // please the compiler
+ for (int i = 0; i < e.Args.Count; i++) {
+ Expression ee = e.Args[i];
+ Formal ff = e.Function.Formals[i];
+ allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(ee), new Bpl.IdentifierExpr(e.tok, ff.AssignUniqueName(currentDeclaration), TrType(ff.Type))));
}
- CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, allowance, e.Receiver, substMap, etran, etran, builder,
- contextDecrInferred, hint);
}
+ string hint;
+ switch (e.CoCall) {
+ case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects:
+ hint = "note that only functions without side effects can be called co-recursively";
+ break;
+ case FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasPostcondition:
+ hint = "note that only functions without any ensures clause can be called co-recursively";
+ break;
+ case FunctionCallExpr.CoCallResolution.NoBecauseIsNotGuarded:
+ hint = "note that the call is not sufficiently guarded to be used co-recursively";
+ break;
+ case FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsAreNotAllowedInThisContext:
+ hint = "note that calls cannot be co-recursive in this context";
+ break;
+ case FunctionCallExpr.CoCallResolution.NoBecauseRecursiveCallsInDestructiveContext:
+ hint = "note that a call can be co-recursive only if all intra-cluster calls are in non-destructive contexts";
+ break;
+ case FunctionCallExpr.CoCallResolution.No:
+ hint = null;
+ break;
+ default:
+ Contract.Assert(false); // unexpected CoCallResolution
+ goto case FunctionCallExpr.CoCallResolution.No; // please the compiler
+ }
+ CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, allowance, e.Receiver, substMap, etran, etran, builder,
+ contextDecrInferred, hint);
}
}
}
@@ -3895,10 +3893,7 @@ namespace Microsoft.Dafny {
} else if (expr is CalcExpr) {
var e = (CalcExpr)expr;
- // TrStmt needs a context so give it one:
- codeContext = new NoContext(this.currentModule);
TrStmt(e.Guard, builder, locals, etran);
- codeContext = null;
CheckWellformed(e.Body, options, locals, builder, etran);
} else if (expr is ITEExpr) {
@@ -3983,18 +3978,34 @@ namespace Microsoft.Dafny {
return !t.IsTypeParameter && !t.IsCoDatatype;
}
- public static List<Expression> MethodDecreasesWithDefault(ICodeContext m, out bool inferredDecreases) {
+ List<Expression> CallableDecreasesWithDefault(ICallable m, out bool inferredDecreases)
+ {
+ Contract.Requires(m != null);
+ if (m is Function) {
+ var f = (Function)m;
+ if (f.Reads.Count != 0) {
+ // start the default lexicographic tuple with the reads clause
+ return CallableDecreasesWithDefault(m, FrameToObjectSet(f.Reads), out inferredDecreases);
+ }
+ }
+ return CallableDecreasesWithDefault(m, null, out inferredDecreases);
+ }
+ public static List<Expression> CallableDecreasesWithDefault(ICallable m, Expression firstComponent, out bool inferredDecreases)
+ {
Contract.Requires(m != null);
inferredDecreases = false;
List<Expression> decr = m.Decreases.Expressions;
if (decr.Count == 0 || (m is PrefixMethod && decr.Count == 1)) {
decr = new List<Expression>();
+ if (firstComponent != null) {
+ decr.Add(firstComponent);
+ }
foreach (Formal p in m.Ins) {
if (IsOrdered(p.Type)) {
- IdentifierExpr ie = new IdentifierExpr(p.tok, p.Name);
+ var ie = new IdentifierExpr(p.tok, p.Name);
ie.Var = p; ie.Type = ie.Var.Type; // resolve it here
- decr.Add(ie); // use the method's first parameter instead
+ decr.Add(ie);
}
}
inferredDecreases = true;
@@ -4004,28 +4015,6 @@ namespace Microsoft.Dafny {
return decr;
}
- List<Expression> FunctionDecreasesWithDefault(Function f, out bool inferredDecreases) {
- Contract.Requires(f != null);
-
- inferredDecreases = false;
- List<Expression> decr = f.Decreases.Expressions;
- if (decr.Count == 0) {
- decr = new List<Expression>();
- if (f.Reads.Count != 0) {
- decr.Add(FrameToObjectSet(f.Reads)); // start the lexicographic tuple with the reads clause
- }
- foreach (Formal p in f.Formals) {
- if (IsOrdered(p.Type)) {
- IdentifierExpr ie = new IdentifierExpr(p.tok, p.AssignUniqueName(f));
- ie.Var = p; ie.Type = ie.Var.Type; // resolve it here
- decr.Add(ie);
- }
- }
- inferredDecreases = true; // use 'true' even if decr.Count==0, because this will trigger an error message that asks the user to consider supplying a decreases clause
- }
- return decr;
- }
-
List<Expression> LoopDecreasesWithDefault(IToken tok, Expression Guard, List<Expression> Decreases, out bool inferredDecreases) {
Contract.Requires(tok != null);
Contract.Requires(Decreases != null);
@@ -4540,6 +4529,10 @@ namespace Microsoft.Dafny {
}
private void AddMethodRefinementCheck(MethodCheck methodCheck) {
+ Contract.Requires(methodCheck != null);
+ Contract.Requires(methodCheck.Refined != null);
+ Contract.Requires(currentModule == null && codeContext == null);
+ Contract.Ensures(currentModule == null && codeContext == null);
// First, we generate the declaration of the procedure. This procedure has the same
// pre and post conditions as the refined method. The body implementation will be a call
@@ -4807,7 +4800,7 @@ namespace Microsoft.Dafny {
GenerateMethodParametersChoose(tok, m, kind, !m.IsStatic, true, true, etran, out inParams, out outParams);
}
- private void GenerateMethodParametersChoose(IToken tok, ICodeContext m, MethodTranslationKind kind, bool includeReceiver, bool includeInParams, bool includeOutParams,
+ private void GenerateMethodParametersChoose(IToken tok, IMethodCodeContext m, MethodTranslationKind kind, bool includeReceiver, bool includeInParams, bool includeOutParams,
ExpressionTranslator etran, out List<Variable> inParams, out List<Variable> outParams) {
inParams = new List<Variable>();
outParams = new List<Variable>();
@@ -6297,19 +6290,20 @@ namespace Microsoft.Dafny {
foreach (Expression e in theDecreases) {
TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true);
}
- // include boilerplate invariants
- foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, codeContext.Modifies.Expressions, s.IsGhost, etranPreLoop, etran, etran.Old))
- {
+ if (codeContext is IMethodCodeContext) {
+ var modifiesClause = ((IMethodCodeContext)codeContext).Modifies.Expressions;
+ // include boilerplate invariants
+ foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, modifiesClause, s.IsGhost, etranPreLoop, etran, etran.Old)) {
if (tri.IsFree) {
- invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));
- }
- else {
- Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant
- invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));
+ invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));
+ } else {
+ Contract.Assert(tri.ErrorMessage != null); // follows from BoilerplateTriple invariant
+ invariants.Add(Assert(s.Tok, tri.Expr, tri.ErrorMessage));
}
+ }
+ // add a free invariant which says that the heap hasn't changed outside of the modifies clause.
+ invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));
}
- // add a free invariant which says that the heap hasn't changed outside of the modifies clause.
- invariants.Add(new Bpl.AssumeCmd(s.Tok, FrameConditionUsingDefinedFrame(s.Tok, etranPreLoop, etran, updatedFrameEtran)));
// include a free invariant that says that all completed iterations so far have only decreased the termination metric
if (initDecr != null) {
@@ -6499,26 +6493,27 @@ namespace Microsoft.Dafny {
Contract.Requires(tok != null);
Contract.Requires(dafnyReceiver != null || bReceiver != null);
Contract.Requires(method != null);
- Contract.Requires(cce.NonNullElements(Args));
- Contract.Requires(cce.NonNullElements(Lhss));
- Contract.Requires(cce.NonNullElements(LhsTypes));
+ Contract.Requires(Args != null);
+ Contract.Requires(Lhss != null);
+ Contract.Requires(LhsTypes != null);
Contract.Requires(method.Outs.Count == Lhss.Count);
Contract.Requires(method.Outs.Count == LhsTypes.Count);
Contract.Requires(builder != null);
Contract.Requires(locals != null);
Contract.Requires(etran != null);
- // 'codeContext' can be a Method or an IteratorDecl. In case of the latter, the caller is really
- // the iterator's MoveNext method. Computer the caller here:
- Method caller = codeContext as Method ?? ((IteratorDecl)codeContext).Member_MoveNext;
// Figure out if the call is recursive or not, which will be used below to determine the need for a
// termination check and the need to include an implicit _k-1 argument.
bool isRecursiveCall = false;
// consult the call graph to figure out if this is a recursive call
var module = method.EnclosingClass.Module;
- if (module == currentModule) {
+ if (codeContext != null && module == currentModule) {
// Note, prefix methods are not recorded in the call graph, but their corresponding comethods are.
- Method cllr = caller is PrefixMethod ? ((PrefixMethod)caller).Co : caller;
+ // Similarly, an iterator is not recorded in the call graph, but its MoveNext method is.
+ ICallable cllr =
+ codeContext is PrefixMethod ? ((PrefixMethod)codeContext).Co :
+ codeContext is IteratorDecl ? ((IteratorDecl)codeContext).Member_MoveNext :
+ codeContext;
if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(cllr)) {
isRecursiveCall = true;
}
@@ -6541,7 +6536,7 @@ namespace Microsoft.Dafny {
// Translate receiver argument, if any
Expression receiver = bReceiver == null ? dafnyReceiver : new BoogieWrapper(bReceiver, dafnyReceiver.Type);
- List<Bpl.Expr> ins = new List<Bpl.Expr>();
+ var ins = new List<Bpl.Expr>();
if (!method.IsStatic) {
if (bReceiver == null && !(dafnyReceiver is ThisExpr)) {
CheckNonNull(dafnyReceiver.tok, dafnyReceiver, builder, etran, null);
@@ -6567,7 +6562,7 @@ namespace Microsoft.Dafny {
Bpl.Expr bActual;
if (i == 0 && method is CoMethod && isRecursiveCall) {
// Treat this call to M(args) as a call to the corresponding prefix method M#(_k - 1, args), so insert an argument here.
- var k = ((PrefixMethod)caller).K;
+ var k = ((PrefixMethod)codeContext).K;
bActual = Bpl.Expr.Sub(new Bpl.IdentifierExpr(k.tok, k.AssignUniqueName(currentDeclaration), Bpl.Type.Int), Bpl.Expr.Literal(1));
} else {
Expression actual;
@@ -6586,19 +6581,22 @@ namespace Microsoft.Dafny {
}
// Check modifies clause of a subcall is a subset of the current frame.
- CheckFrameSubset(tok, callee.Mod.Expressions, receiver, substMap, etran, builder, "call may violate context's modifies clause", null);
+ if (codeContext is IMethodCodeContext) {
+ CheckFrameSubset(tok, callee.Mod.Expressions, receiver, substMap, etran, builder, "call may violate context's modifies clause", null);
+ }
// Check termination
if (isRecursiveCall) {
+ Contract.Assert(codeContext != null);
bool contextDecrInferred, calleeDecrInferred;
- List<Expression> contextDecreases = MethodDecreasesWithDefault(caller, out contextDecrInferred);
- List<Expression> calleeDecreases = MethodDecreasesWithDefault(callee, out calleeDecrInferred);
+ List<Expression> contextDecreases = CallableDecreasesWithDefault(codeContext, out contextDecrInferred);
+ List<Expression> calleeDecreases = CallableDecreasesWithDefault(callee, out calleeDecrInferred);
CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, etran.Old, builder, contextDecrInferred, null);
}
// Create variables to hold the output parameters of the call, so that appropriate unboxes can be introduced.
- List<Bpl.IdentifierExpr> outs = new List<Bpl.IdentifierExpr>();
- List<Bpl.IdentifierExpr> tmpOuts = new List<Bpl.IdentifierExpr>();
+ var outs = new List<Bpl.IdentifierExpr>();
+ var tmpOuts = new List<Bpl.IdentifierExpr>();
for (int i = 0; i < Lhss.Count; i++) {
var bLhs = Lhss[i];
if (ExpressionTranslator.ModeledAsBoxType(callee.Outs[i].Type) && !ExpressionTranslator.ModeledAsBoxType(LhsTypes[i])) {
@@ -10292,7 +10290,7 @@ namespace Microsoft.Dafny {
// For non-recursive function: arguments are "prominent" if the call is
var rec = e.Function.IsRecursive && e.CoCall != FunctionCallExpr.CoCallResolution.Yes;
bool inferredDecreases; // we don't actually care
- var decr = FunctionDecreasesWithDefault(e.Function, out inferredDecreases);
+ var decr = CallableDecreasesWithDefault(e.Function, out inferredDecreases);
bool variantArgument;
if (DafnyOptions.O.InductionHeuristic < 6) {
variantArgument = rec;
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index f6c46bc6..c79d166a 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -366,6 +366,21 @@ ResolutionErrors.dfy(617,20): Error: only ghost methods can be called from this
ResolutionErrors.dfy(619,8): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(637,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.
ResolutionErrors.dfy(637,21): Error: the type of this expression is underspecified, but it cannot be an arbitrary type.
+ResolutionErrors.dfy(674,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(684,8): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(687,20): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(698,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(698,16): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(699,21): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(700,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(703,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(722,8): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(725,20): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(730,16): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+ResolutionErrors.dfy(730,16): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(731,21): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(732,8): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(735,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
ResolutionErrors.dfy(427,2): Error: More than one default constructor
ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts
@@ -439,7 +454,7 @@ ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specifi
ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(544,18): Error: unresolved identifier: w
ResolutionErrors.dfy(651,11): Error: lemmas are not allowed to have modifies clauses
-92 resolution/type errors detected in ResolutionErrors.dfy
+107 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -1161,6 +1176,20 @@ Execution trace:
Dafny program verifier finished with 40 verified, 6 errors
+-------------------- StatementExpressions.dfy --------------------
+StatementExpressions.dfy(52,11): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon6_Then
+ (0,0): anon8_Then
+StatementExpressions.dfy(56,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon6_Then
+ StatementExpressions.dfy(50,7): anon8_Else
+
+Dafny program verifier finished with 9 verified, 2 errors
+
-------------------- Coinductive.dfy --------------------
Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
@@ -1749,6 +1778,45 @@ IteratorResolution.dfy(137,9): Error: unresolved identifier: _decreases0
12 resolution/type errors detected in IteratorResolution.dfy
-------------------- Iterators.dfy --------------------
+Iterators.dfy(248,9): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Else
+Iterators.dfy(271,9): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Else
+Iterators.dfy(281,24): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+Iterators.dfy(293,9): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Else
+Iterators.dfy(314,9): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Else
+Iterators.dfy(323,24): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon0
+Iterators.dfy(340,9): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Else
+Iterators.dfy(350,24): Error: cannot prove termination; try supplying a decreases clause
+Execution trace:
+ (0,0): anon0
+Iterators.dfy(367,9): Error: failure to decrease termination measure
+Execution trace:
+ (0,0): anon0
+ (0,0): anon5_Else
+ (0,0): anon6_Else
Iterators.dfy(100,22): Error: assertion violation
Execution trace:
(0,0): anon0
@@ -1812,7 +1880,7 @@ Execution trace:
Iterators.dfy(222,3): anon18_Else
(0,0): anon19_Else
-Dafny program verifier finished with 38 verified, 11 errors
+Dafny program verifier finished with 65 verified, 20 errors
-------------------- RankPos.dfy --------------------
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
index e0c58867..f4d36762 100644
--- a/Test/dafny0/Iterators.dfy
+++ b/Test/dafny0/Iterators.dfy
@@ -233,3 +233,148 @@ method ClientOfNewReferences()
i := i - 1;
}
}
+
+// ------ recursive iterators --------------------------------------
+
+module ITER_A {
+ iterator RecursiveIterator(n: nat, r: RecIterCaller, good: bool)
+ requires r != null;
+ decreases n+2, 0;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1);
+ } else {
+ r.M(n + 1); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat)
+ decreases n+2;
+ {
+ var good;
+ var iter := new RecursiveIterator(n, this, good);
+ var more := iter.MoveNext();
+ }
+ }
+}
+module ITER_B {
+ iterator RecursiveIterator(n: nat, r: RecIterCaller, good: bool)
+ requires r != null;
+ decreases n;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1);
+ } else {
+ r.M(n + 1); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat)
+ decreases n;
+ {
+ var good;
+ var iter := new RecursiveIterator(n, this, good);
+ var more := iter.MoveNext(); // error: failure to decrease variant function
+ }
+ }
+}
+module ITER_C {
+ iterator RecursiveIterator(n: nat, r: RecIterCaller, good: bool)
+ requires r != null;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1);
+ } else {
+ r.M(n + 1); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat)
+ {
+ var good;
+ var iter := new RecursiveIterator(n, this, good);
+ var more := iter.MoveNext();
+ }
+ }
+}
+module ITER_D {
+ iterator RecursiveIterator(n: nat, r: RecIterCaller, good: bool)
+ requires r != null;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1, {});
+ } else {
+ r.M(n + 1, {}); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat, incomparable: set<int>)
+ {
+ var good;
+ var iter := new RecursiveIterator(n, this, good);
+ var more := iter.MoveNext(); // error: failure to decrease variant function
+ }
+ }
+}
+module ITER_E {
+ class Cell {
+ var data: nat;
+ }
+ iterator RecursiveIterator(cell: Cell, n: nat, r: RecIterCaller, good: bool)
+ requires cell != null && r != null;
+ modifies cell;
+ decreases if cell.data < 2 then n else n+n-n;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1);
+ } else {
+ r.M(n + 1); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat)
+ {
+ var good;
+ var cell := new Cell;
+ var iter := new RecursiveIterator(cell, n, this, good);
+ var more := iter.MoveNext(); // error: failure to decrease variant function
+ }
+ }
+}
+module ITER_F {
+ class Cell {
+ var data: nat;
+ }
+ iterator RecursiveIterator(cell: Cell, n: nat, r: RecIterCaller, good: bool)
+ requires cell != null && r != null;
+ modifies cell;
+ decreases if cell.data < 2 then n else n+n-n, 0;
+ {
+ if n == 0 {
+ } else if good {
+ r.M(n - 1);
+ } else {
+ r.M(n + 1); // error: may fail to terminate
+ }
+ }
+
+ class RecIterCaller {
+ method M(n: nat)
+ {
+ var good;
+ var cell := new Cell;
+ var iter := new RecursiveIterator(cell, n, this, good);
+ var more := iter.MoveNext();
+ }
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 92b4aa80..b96b0867 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -653,3 +653,98 @@ lemma MyLemma(x: int) returns (y: int)
{
y := x;
}
+
+// ------------------------- statements in expressions ------------------------------
+
+module StatementsInExpressions {
+ ghost method SideEffect()
+ modifies this;
+ {
+ }
+
+ method NonGhostMethod()
+ {
+ }
+
+ ghost method M()
+ modifies this;
+ {
+ calc {
+ 5;
+ { SideEffect(); } // error: cannot call method with side effects
+ 5;
+ }
+ }
+
+ function F(): int
+ {
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method
+ { var x := 8;
+ while x != 0
+ decreases *; // error: cannot use 'decreases *' in a ghost context
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop
+ {
+ x := x - 1;
+ }
+ }
+ 6;
+ }
+ 5
+ }
+
+ var MyField: int;
+ ghost var MyGhostField: int;
+
+ method N()
+ {
+ var y :=
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method
+ { var x := 8;
+ while x != 0
+ decreases *; // error: cannot use 'decreases *' in a ghost context
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { M(); } // error: cannot call (ghost) method with a modifies clause
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ 6;
+ }
+ 5;
+ }
+}
diff --git a/Test/dafny0/StatementExpressions.dfy b/Test/dafny0/StatementExpressions.dfy
new file mode 100644
index 00000000..9f33b282
--- /dev/null
+++ b/Test/dafny0/StatementExpressions.dfy
@@ -0,0 +1,58 @@
+ghost method M(n: nat) //returns (y: nat)
+{
+ var y := F(n, 0);
+}
+function F(n: nat, p: int): nat
+{
+ calc {
+ 100;
+ < { if n != 0 { M(n-1); } }
+ 102;
+ }
+ n
+}
+
+ghost method MM(n: nat) returns (y: nat)
+ decreases n, 0;
+{
+ if n != 0 {
+ y := FF(n-1);
+ }
+}
+function FF(n: nat): nat
+ decreases n, 1;
+{
+ calc {
+ 100;
+ < { var y := MM(n); }
+ 102;
+ }
+ n
+}
+
+ghost method P(n: nat)
+{
+ if n != 0 {
+ var y :=
+ calc {
+ 12;
+ { P(n-1); }
+ 12;
+ }
+ 100;
+ assert y == 100;
+ }
+}
+ghost method Q(n: nat)
+{
+ if n != 0 {
+ var y :=
+ calc {
+ 12;
+ { Q(n+1); } // error: cannot prove termination
+ 12;
+ }
+ 100;
+ assert y == 102; // error: assertion does not hold
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index b911625b..703f8a2c 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -16,7 +16,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy Definedness.dfy
ModulesCycle.dfy Modules0.dfy Modules1.dfy Modules2.dfy BadFunction.dfy
Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy ParallelResolveErrors.dfy Parallel.dfy
- TypeParameters.dfy Datatypes.dfy
+ TypeParameters.dfy Datatypes.dfy StatementExpressions.dfy
Coinductive.dfy Corecursion.dfy CoResolution.dfy
CoPrefix.dfy CoinductiveProofs.dfy
TypeAntecedents.dfy NoTypeArgs.dfy EqualityTypes.dfy SplitExpr.dfy
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-24 08:48:31 +0000