diff options
| author |  leino <unknown> | 2015-08-11 19:07:42 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-08-11 19:07:42 -0700 |
| commit | 3bf4b44b821dca5017017e99502f263e636d5e84 (patch) | |
| tree | b9a2f6d58de3e17db6a49b5177dbd49a9cc9fdfe /Source/Dafny | |
| parent | 2a921fb2a765d91bba47901144845b0102edbcbb (diff) | |
Moved discovery of induction variables into a Rewriter.
Generate warnings for malformed :induction arguments.
Removed the functionality that allowed induction on 'this'.
Diffstat (limited to 'Source/Dafny')
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 8 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 1 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 343 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 513 |
5 files changed, 466 insertions, 401 deletions
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 66cf639f..2eea5717 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -312,7 +312,7 @@ namespace Microsoft.Dafny 2 - apply induction as requested (by attributes) and also
for heuristically chosen quantifiers
3 (default) - apply induction as requested, and for
- heuristically chosen quantifiers and ghost methods
+ heuristically chosen quantifiers and lemmas
/inductionHeuristic:<n>
0 - least discriminating induction heuristic (that is, lean
toward applying induction more often)
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 1fa90e41..7a93a140 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -109,11 +109,11 @@ namespace Microsoft.Dafny { }
}
- public static string OneAttributeToString(Attributes a) {
+ public static string OneAttributeToString(Attributes a, string nameSubstitution = null) {
Contract.Requires(a != null);
using (var wr = new System.IO.StringWriter()) {
var pr = new Printer(wr);
- pr.PrintOneAttribute(a);
+ pr.PrintOneAttribute(a, nameSubstitution);
return ToStringWithoutNewline(wr);
}
}
@@ -441,9 +441,9 @@ namespace Microsoft.Dafny { PrintOneAttribute(a);
}
}
- public void PrintOneAttribute(Attributes a) {
+ public void PrintOneAttribute(Attributes a, string nameSubstitution = null) {
Contract.Requires(a != null);
- wr.Write(" {{:{0}", a.Name);
+ wr.Write(" {{:{0}", nameSubstitution ?? a.Name);
if (a.Args != null) {
PrintAttributeArgs(a.Args, false);
}
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a58d6e6c..75d171ac 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -322,6 +322,7 @@ namespace Microsoft.Dafny if (DafnyOptions.O.AutoTriggers) {
rewriters.Add(new TriggersRewriter(this));
}
+ rewriters.Add(new InductionRewriter(this));
systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule, false);
prog.CompileModules.Add(prog.BuiltIns.SystemModule);
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 4223fb7f..ffd808c5 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -1266,6 +1266,347 @@ namespace Microsoft.Dafny return new AutoGeneratedToken(tok);
}
}
-}
+ // ===========================================================================================
+
+ public class InductionRewriter : IRewriter
+ {
+ Resolver Resolver;
+ internal InductionRewriter(Resolver resolver) {
+ Contract.Requires(resolver != null);
+ this.Resolver = resolver;
+ }
+ public void PreResolve(ModuleDefinition m) {
+ }
+ public void PostResolve(ModuleDefinition m) {
+ }
+ public void PostCyclicityResolve(ModuleDefinition m) {
+ if (DafnyOptions.O.Induction == 0) {
+ // Don't bother inferring :induction attributes. This will also have the effect of not warning about malformed :induction attributes
+ } else {
+ foreach (var decl in m.TopLevelDecls) {
+ if (decl is ClassDecl) {
+ var cl = (ClassDecl)decl;
+ foreach (var member in cl.Members) {
+ if (member is FixpointLemma) {
+ var method = (FixpointLemma)member;
+ ProcessMethodExpressions(method);
+ ComputeLemmaInduction(method.PrefixLemma);
+ ProcessMethodExpressions(method.PrefixLemma);
+ } else if (member is Method) {
+ var method = (Method)member;
+ ComputeLemmaInduction(method);
+ ProcessMethodExpressions(method);
+ } else if (member is FixpointPredicate) {
+ var function = (FixpointPredicate)member;
+ ProcessFunctionExpressions(function);
+ ProcessFunctionExpressions(function.PrefixPredicate);
+ } else if (member is Function) {
+ var function = (Function)member;
+ ProcessFunctionExpressions(function);
+ }
+ }
+ } else if (decl is NewtypeDecl) {
+ var nt = (NewtypeDecl)decl;
+ if (nt.Constraint != null) {
+ var visitor = new Induction_Visitor(this);
+ visitor.Visit(nt.Constraint);
+ }
+ }
+ }
+ }
+ }
+ void ProcessMethodExpressions(Method method) {
+ Contract.Requires(method != null);
+ var visitor = new Induction_Visitor(this);
+ method.Req.ForEach(mfe => visitor.Visit(mfe.E));
+ method.Ens.ForEach(mfe => visitor.Visit(mfe.E));
+ if (method.Body != null) {
+ visitor.Visit(method.Body);
+ }
+ }
+ void ProcessFunctionExpressions(Function function) {
+ Contract.Requires(function != null);
+ var visitor = new Induction_Visitor(this);
+ function.Req.ForEach(visitor.Visit);
+ function.Ens.ForEach(visitor.Visit);
+ if (function.Body != null) {
+ visitor.Visit(function.Body);
+ }
+ }
+ void ComputeLemmaInduction(Method method) {
+ Contract.Requires(method != null);
+ if (method.IsGhost && method.Mod.Expressions.Count == 0 && method.Outs.Count == 0 && !(method is FixpointLemma)) {
+ var posts = new List<Expression>();
+ method.Ens.ForEach(mfe => posts.Add(mfe.E));
+ ComputeInductionVariables(method.tok, method.Ins, posts, ref method.Attributes);
+ }
+ }
+ void ComputeInductionVariables<VarType>(IToken tok, List<VarType> boundVars, List<Expression> searchExprs, ref Attributes attributes) where VarType : class, IVariable {
+ Contract.Requires(tok != null);
+ Contract.Requires(boundVars != null);
+ Contract.Requires(searchExprs != null);
+ Contract.Requires(DafnyOptions.O.Induction != 0);
+ bool forLemma = boundVars is List<Formal>;
+
+ var args = Attributes.FindExpressions(attributes, "induction"); // we only look at the first one we find, since it overrides any other ones
+ if (args == null) {
+ if (DafnyOptions.O.Induction < 2) {
+ // No explicit induction variables and we're asked not to infer anything, so we're done
+ return;
+ } else if (DafnyOptions.O.Induction == 2 && forLemma) {
+ // We're asked to infer induction variables only for quantifiers, not for lemmas
+ return;
+ }
+ // GO INFER below (only select boundVars)
+ } else if (args.Count == 0) {
+ // {:induction} is treated the same as {:induction true}, which says to automatically infer induction variables
+ // GO INFER below (all boundVars)
+ } else if (args.Count == 1 && args[0] is LiteralExpr && ((LiteralExpr)args[0]).Value is bool) {
+ // {:induction false} or {:induction true}
+ if (!(bool)((LiteralExpr)args[0]).Value) {
+ // we're told not to infer anything
+ return;
+ }
+ // GO INFER below (all boundVars)
+ } else {
+ // Here, we're expecting the arguments to {:induction args} to be a sublist of "boundVars".
+ var goodArguments = new List<Expression>();
+ var i = 0;
+ foreach (var arg in args) {
+ var ie = arg.Resolved as IdentifierExpr;
+ if (ie != null) {
+ var j = boundVars.FindIndex(i, v => v == ie.Var);
+ if (i <= j) {
+ goodArguments.Add(ie);
+ i = j;
+ continue;
+ }
+ if (0 <= boundVars.FindIndex(v => v == ie.Var)) {
+ Resolver.Warning(arg.tok, "{0}s given as :induction arguments must be given in the same order as in the {1}; ignoring attribute",
+ forLemma ? "lemma parameter" : "bound variable", forLemma ? "lemma" : "quantifier");
+ return;
+ }
+ }
+ Resolver.Warning(arg.tok, "invalid :induction attribute argument; expected {0}{1}; ignoring attribute",
+ i == 0 ? "'false' or 'true' or " : "",
+ forLemma ? "lemma parameter" : "bound variable");
+ return;
+ }
+ // The argument list was legal, so let's use it for the _induction attribute
+ attributes = new Attributes("_induction", goodArguments, attributes);
+ return;
+ }
+
+ // Okay, here we go, coming up with good induction setting for the given situation
+ var inductionVariables = new List<Expression>();
+ foreach (IVariable n in boundVars) {
+ if (!n.Type.IsTypeParameter && (args != null || searchExprs.Exists(expr => VarOccursInArgumentToRecursiveFunction(expr, n)))) {
+ inductionVariables.Add(new IdentifierExpr(n));
+ }
+ }
+ if (inductionVariables.Count != 0) {
+ // We found something usable, so let's record that in an attribute
+ attributes = new Attributes("_induction", inductionVariables, attributes);
+ // And since we're inferring something, let's also report that in a hover text.
+ var s = Printer.OneAttributeToString(attributes, "induction");
+ Resolver.ReportAdditionalInformation(tok, s, s.Length);
+ }
+ }
+ class Induction_Visitor : BottomUpVisitor
+ {
+ readonly InductionRewriter IndRewriter;
+ public Induction_Visitor(InductionRewriter inductionRewriter) {
+ Contract.Requires(inductionRewriter != null);
+ IndRewriter = inductionRewriter;
+ }
+ protected override void VisitOneExpr(Expression expr) {
+ var q = expr as QuantifierExpr;
+ if (q != null) {
+ IndRewriter.ComputeInductionVariables(q.tok, q.BoundVars, new List<Expression>() { q.LogicalBody() }, ref q.Attributes);
+ }
+ }
+ void VisitInductionStmt(Statement stmt) {
+ Contract.Requires(stmt != null);
+ // visit a selection of subexpressions
+ if (stmt is AssertStmt) {
+ var s = (AssertStmt)stmt;
+ Visit(s.Expr);
+ }
+ // recursively visit all substatements
+ foreach (var s in stmt.SubStatements) {
+ VisitInductionStmt(s);
+ }
+ }
+ }
+
+ /// <summary>
+ /// Returns 'true' iff by looking at 'expr' the Induction Heuristic determines that induction should be applied to 'n'.
+ /// More precisely:
+ /// DafnyInductionHeuristic Return 'true'
+ /// ----------------------- -------------
+ /// 0 always
+ /// 1 if 'n' occurs as any subexpression (of 'expr')
+ /// 2 if 'n' occurs as any subexpression of any index argument of an array/sequence select expression or any argument to a recursive function
+ /// 3 if 'n' occurs as a prominent subexpression of any index argument of an array/sequence select expression or any argument to a recursive function
+ /// 4 if 'n' occurs as any subexpression of any argument to a recursive function
+ /// 5 if 'n' occurs as a prominent subexpression of any argument to a recursive function
+ /// 6 if 'n' occurs as a prominent subexpression of any decreases-influencing argument to a recursive function
+ /// Parameter 'n' is allowed to be a ThisSurrogate.
+ /// </summary>
+ public static bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) {
+ switch (DafnyOptions.O.InductionHeuristic) {
+ case 0: return true;
+ case 1: return Translator.ContainsFreeVariable(expr, false, n);
+ default: return VarOccursInArgumentToRecursiveFunction(expr, n, false);
+ }
+ }
+
+ /// <summary>
+ /// Worker routine for VarOccursInArgumentToRecursiveFunction(expr,n), where the additional parameter 'exprIsProminent' says whether or
+ /// not 'expr' has prominent status in its context.
+ /// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2).
+ /// Parameter 'n' is allowed to be a ThisSurrogate.
+ /// </summary>
+ static bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, bool exprIsProminent) {
+ Contract.Requires(expr != null);
+ Contract.Requires(n != null);
+
+ // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.
+ var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;
+
+ if (expr is ThisExpr) {
+ return exprIsProminent && n is ThisSurrogate;
+ } else if (expr is IdentifierExpr) {
+ var e = (IdentifierExpr)expr;
+ return exprIsProminent && e.Var == n;
+ } else if (expr is SeqSelectExpr) {
+ var e = (SeqSelectExpr)expr;
+ var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;
+ return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) || // this subexpression does not acquire "prominent" status
+ (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) || // this one does (unless arrays/sequences are excluded)
+ (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q)); // ditto
+ } else if (expr is MultiSelectExpr) {
+ var e = (MultiSelectExpr)expr;
+ var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;
+ return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) ||
+ e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));
+ } else if (expr is FunctionCallExpr) {
+ var e = (FunctionCallExpr)expr;
+ // For recursive functions: arguments are "prominent"
+ // For non-recursive function: arguments are "prominent" if the call is
+ var rec = e.Function.IsRecursive && e.CoCall != FunctionCallExpr.CoCallResolution.Yes;
+ var decr = e.Function.Decreases.Expressions;
+ bool variantArgument;
+ if (DafnyOptions.O.InductionHeuristic < 6) {
+ variantArgument = rec;
+ } else {
+ // The receiver is considered to be "variant" if the function is recursive and the receiver participates
+ // in the effective decreases clause of the function. The receiver participates if it's a free variable
+ // of a term in the explicit decreases clause.
+ variantArgument = rec && decr.Exists(ee => Translator.ContainsFreeVariable(ee, true, null));
+ }
+ if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, variantArgument || subExprIsProminent)) {
+ return true;
+ }
+ Contract.Assert(e.Function.Formals.Count == e.Args.Count);
+ for (int i = 0; i < e.Function.Formals.Count; i++) {
+ var f = e.Function.Formals[i];
+ var exp = e.Args[i];
+ if (DafnyOptions.O.InductionHeuristic < 6) {
+ variantArgument = rec;
+ } else if (rec) {
+ // The argument position is considered to be "variant" if the function is recursive and...
+ // ... it has something to do with why the callee is well-founded, which happens when...
+ if (f is ImplicitFormal) {
+ // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix lemma, or
+ variantArgument = true;
+ } else if (decr.Exists(ee => Translator.ContainsFreeVariable(ee, false, f))) {
+ // ... it participates in the effective decreases clause of the function, which happens when it is
+ // a free variable of a term in the explicit decreases clause, or
+ variantArgument = true;
+ } else {
+ // ... the callee is a prefix predicate.
+ variantArgument = true;
+ }
+ }
+ if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument || subExprIsProminent)) {
+ return true;
+ }
+ }
+ return false;
+ } else if (expr is TernaryExpr) {
+ var e = (TernaryExpr)expr;
+ switch (e.Op) {
+ case TernaryExpr.Opcode.PrefixEqOp:
+ case TernaryExpr.Opcode.PrefixNeqOp:
+ return VarOccursInArgumentToRecursiveFunction(e.E0, n, true) ||
+ VarOccursInArgumentToRecursiveFunction(e.E1, n, subExprIsProminent) ||
+ VarOccursInArgumentToRecursiveFunction(e.E2, n, subExprIsProminent);
+ default:
+ Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression
+ }
+ } else if (expr is DatatypeValue) {
+ var e = (DatatypeValue)expr;
+ var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent; // prominent status continues, if we're looking for a variable whose type is a datatype
+ return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));
+ } else if (expr is UnaryExpr) {
+ var e = (UnaryExpr)expr;
+ // both Not and SeqLength preserve prominence
+ return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent);
+ } else if (expr is BinaryExpr) {
+ var e = (BinaryExpr)expr;
+ bool q;
+ switch (e.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.Add:
+ case BinaryExpr.ResolvedOpcode.Sub:
+ case BinaryExpr.ResolvedOpcode.Mul:
+ case BinaryExpr.ResolvedOpcode.Div:
+ case BinaryExpr.ResolvedOpcode.Mod:
+ case BinaryExpr.ResolvedOpcode.Union:
+ case BinaryExpr.ResolvedOpcode.Intersection:
+ case BinaryExpr.ResolvedOpcode.SetDifference:
+ case BinaryExpr.ResolvedOpcode.Concat:
+ // these operators preserve prominence
+ q = exprIsProminent;
+ break;
+ default:
+ // whereas all other binary operators do not
+ q = subExprIsProminent;
+ break;
+ }
+ return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) ||
+ VarOccursInArgumentToRecursiveFunction(e.E1, n, q);
+ } else if (expr is StmtExpr) {
+ var e = (StmtExpr)expr;
+ // ignore the statement
+ return VarOccursInArgumentToRecursiveFunction(e.E, n);
+
+ } else if (expr is ITEExpr) {
+ var e = (ITEExpr)expr;
+ return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) || // test is not "prominent"
+ VarOccursInArgumentToRecursiveFunction(e.Thn, n, exprIsProminent) || // but the two branches are
+ VarOccursInArgumentToRecursiveFunction(e.Els, n, exprIsProminent);
+ } else if (expr is OldExpr ||
+ expr is ConcreteSyntaxExpression ||
+ expr is BoxingCastExpr ||
+ expr is UnboxingCastExpr) {
+ foreach (var exp in expr.SubExpressions) {
+ if (VarOccursInArgumentToRecursiveFunction(exp, n, exprIsProminent)) { // maintain prominence
+ return true;
+ }
+ }
+ return false;
+ } else {
+ // in all other cases, reset the prominence status and recurse on the subexpressions
+ foreach (var exp in expr.SubExpressions) {
+ if (VarOccursInArgumentToRecursiveFunction(exp, n, subExprIsProminent)) {
+ return true;
+ }
+ }
+ return false;
+ }
+ }
+ }
+}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index b8c4b8ec..cdfb1a32 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2756,126 +2756,117 @@ namespace Microsoft.Dafny { Bpl.StmtList stmts;
if (!wellformednessProc) {
- if (3 <= DafnyOptions.O.Induction && m.IsGhost && m.Mod.Expressions.Count == 0 && m.Outs.Count == 0 && !(m is FixpointLemma)) {
- var posts = new List<Expression>();
- m.Ens.ForEach(mfe => posts.Add(mfe.E));
- var allIns = new List<Formal>();
- if (!m.IsStatic) {
- allIns.Add(new ThisSurrogate(m.tok, Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass)));
- }
- allIns.AddRange(m.Ins);
- var inductionVars = ApplyInduction(allIns, m.Attributes, posts, delegate(System.IO.TextWriter wr) { wr.Write(m.FullName); });
- if (inductionVars.Count != 0) {
- // Let the parameters be this,x,y of the method M and suppose ApplyInduction returns this,y.
- // Also, let Pre be the precondition and VF be the decreases clause.
- // Then, insert into the method body what amounts to:
- // assume case-analysis-on-parameter[[ y' ]];
- // forall (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) {
- // this'.M(x, y');
- // }
- // Generate bound variables for the forall statement, and a substitution for the Pre and VF
-
- // assume case-analysis-on-parameter[[ y' ]];
- foreach (var inFormal in m.Ins) {
- var dt = inFormal.Type.AsDatatype;
- if (dt != null) {
- var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullSanitizedName, Bpl.Type.Bool));
- var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.AssignUniqueName(m.IdGenerator), TrType(inFormal.Type));
- builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new List<Bpl.Expr> { f })));
- }
- }
-
- var parBoundVars = new List<BoundVar>();
- Expression receiverReplacement = null;
- var substMap = new Dictionary<IVariable, Expression>();
- foreach (var iv in inductionVars) {
- BoundVar bv;
- IdentifierExpr ie;
- CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out ie);
- parBoundVars.Add(bv);
- if (iv is ThisSurrogate) {
- Contract.Assert(receiverReplacement == null && substMap.Count == 0); // the receiver comes first, if at all
- receiverReplacement = ie;
- } else {
- substMap.Add(iv, ie);
- }
+ var inductionVars = ApplyInduction(m.Ins, m.Attributes);
+ if (inductionVars.Count != 0) {
+ // Let the parameters be this,x,y of the method M and suppose ApplyInduction returns y.
+ // Also, let Pre be the precondition and VF be the decreases clause.
+ // Then, insert into the method body what amounts to:
+ // assume case-analysis-on-parameter[[ y' ]];
+ // forall (y' | Pre(this, x, y') && VF(this, x, y') << VF(this, x, y)) {
+ // this.M(x, y');
+ // }
+ // Generate bound variables for the forall statement, and a substitution for the Pre and VF
+
+ // assume case-analysis-on-parameter[[ y' ]];
+ foreach (var inFormal in m.Ins) {
+ var dt = inFormal.Type.AsDatatype;
+ if (dt != null) {
+ var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullSanitizedName, Bpl.Type.Bool));
+ var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.AssignUniqueName(m.IdGenerator), TrType(inFormal.Type));
+ builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new List<Bpl.Expr> { f })));
+ }
+ }
+
+ var parBoundVars = new List<BoundVar>();
+ Expression receiverReplacement = null;
+ var substMap = new Dictionary<IVariable, Expression>();
+ foreach (var iv in inductionVars) {
+ BoundVar bv;
+ IdentifierExpr ie;
+ CloneVariableAsBoundVar(iv.tok, iv, "$ih#" + iv.Name, out bv, out ie);
+ parBoundVars.Add(bv);
+ if (iv is ThisSurrogate) {
+ Contract.Assert(receiverReplacement == null && substMap.Count == 0); // the receiver comes first, if at all
+ receiverReplacement = ie;
+ } else {
+ substMap.Add(iv, ie);
}
+ }
- // Generate a CallStmt for the recursive call
- Expression recursiveCallReceiver;
- if (receiverReplacement != null) {
- recursiveCallReceiver = receiverReplacement;
- } else if (m.IsStatic) {
- recursiveCallReceiver = new StaticReceiverExpr(m.tok, (ClassDecl)m.EnclosingClass, true); // this also resolves it
+ // Generate a CallStmt for the recursive call
+ Expression recursiveCallReceiver;
+ if (receiverReplacement != null) {
+ recursiveCallReceiver = receiverReplacement;
+ } else if (m.IsStatic) {
+ recursiveCallReceiver = new StaticReceiverExpr(m.tok, (ClassDecl)m.EnclosingClass, true); // this also resolves it
+ } else {
+ recursiveCallReceiver = new ImplicitThisExpr(m.tok);
+ recursiveCallReceiver.Type = Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass); // resolve here
+ }
+ var recursiveCallArgs = new List<Expression>();
+ foreach (var inFormal in m.Ins) {
+ Expression inE;
+ if (substMap.TryGetValue(inFormal, out inE)) {
+ recursiveCallArgs.Add(inE);
} else {
- recursiveCallReceiver = new ImplicitThisExpr(m.tok);
- recursiveCallReceiver.Type = Resolver.GetThisType(m.tok, (ClassDecl)m.EnclosingClass); // resolve here
- }
- var recursiveCallArgs = new List<Expression>();
- foreach (var inFormal in m.Ins) {
- Expression inE;
- if (substMap.TryGetValue(inFormal, out inE)) {
- recursiveCallArgs.Add(inE);
- } else {
- var ie = new IdentifierExpr(inFormal.tok, inFormal.Name);
- ie.Var = inFormal; // resolve here
- ie.Type = inFormal.Type; // resolve here
- recursiveCallArgs.Add(ie);
- }
- }
- var methodSel = new MemberSelectExpr(m.tok, recursiveCallReceiver, m.Name);
- methodSel.Member = m; // resolve here
- methodSel.TypeApplication = new List<Type>();
- methodSel.TypeApplication.AddRange(recursiveCallReceiver.Type.TypeArgs);
- m.TypeArgs.ForEach(tp => methodSel.TypeApplication.Add(new UserDefinedType(tp)));
- methodSel.Type = new InferredTypeProxy(); // this is the last step in resolving 'methodSel'
- var recursiveCall = new CallStmt(m.tok, m.tok, new List<Expression>(), methodSel, recursiveCallArgs);
- recursiveCall.IsGhost = m.IsGhost; // resolve here
-
- Expression parRange = new LiteralExpr(m.tok, true);
- parRange.Type = Type.Bool; // resolve here
- if (receiverReplacement != null) {
- // add "this' != null" to the range
- var nil = new LiteralExpr(receiverReplacement.tok);
- nil.Type = receiverReplacement.Type; // resolve here
- var neqNull = new BinaryExpr(receiverReplacement.tok, BinaryExpr.Opcode.Neq, receiverReplacement, nil);
- neqNull.ResolvedOp = BinaryExpr.ResolvedOpcode.NeqCommon; // resolve here
- neqNull.Type = Type.Bool; // resolve here
- parRange = Expression.CreateAnd(parRange, neqNull);
- }
- foreach (var pre in m.Req) {
- if (!pre.IsFree) {
- parRange = Expression.CreateAnd(parRange, Substitute(pre.E, receiverReplacement, substMap));
- }
- }
- // construct an expression (generator) for: VF' << VF
- ExpressionConverter decrCheck = delegate(Dictionary<IVariable, Expression> decrSubstMap, ExpressionTranslator exprTran) {
- var decrToks = new List<IToken>();
- var decrTypes = new List<Type>();
- var decrCallee = new List<Expr>();
- var decrCaller = new List<Expr>();
- foreach (var ee in m.Decreases.Expressions) {
- decrToks.Add(ee.tok);
- decrTypes.Add(ee.Type.NormalizeExpand());
- decrCaller.Add(exprTran.TrExpr(ee));
- Expression es = Substitute(ee, receiverReplacement, substMap);
- es = Substitute(es, null, decrSubstMap);
- decrCallee.Add(exprTran.TrExpr(es));
- }
- return DecreasesCheck(decrToks, decrTypes, decrTypes, decrCallee, decrCaller, null, null, false, true);
- };
+ var ie = new IdentifierExpr(inFormal.tok, inFormal.Name);
+ ie.Var = inFormal; // resolve here
+ ie.Type = inFormal.Type; // resolve here
+ recursiveCallArgs.Add(ie);
+ }
+ }
+ var methodSel = new MemberSelectExpr(m.tok, recursiveCallReceiver, m.Name);
+ methodSel.Member = m; // resolve here
+ methodSel.TypeApplication = new List<Type>();
+ methodSel.TypeApplication.AddRange(recursiveCallReceiver.Type.TypeArgs);
+ m.TypeArgs.ForEach(tp => methodSel.TypeApplication.Add(new UserDefinedType(tp)));
+ methodSel.Type = new InferredTypeProxy(); // this is the last step in resolving 'methodSel'
+ var recursiveCall = new CallStmt(m.tok, m.tok, new List<Expression>(), methodSel, recursiveCallArgs);
+ recursiveCall.IsGhost = m.IsGhost; // resolve here
+
+ Expression parRange = new LiteralExpr(m.tok, true);
+ parRange.Type = Type.Bool; // resolve here
+ if (receiverReplacement != null) {
+ // add "this' != null" to the range
+ var nil = new LiteralExpr(receiverReplacement.tok);
+ nil.Type = receiverReplacement.Type; // resolve here
+ var neqNull = new BinaryExpr(receiverReplacement.tok, BinaryExpr.Opcode.Neq, receiverReplacement, nil);
+ neqNull.ResolvedOp = BinaryExpr.ResolvedOpcode.NeqCommon; // resolve here
+ neqNull.Type = Type.Bool; // resolve here
+ parRange = Expression.CreateAnd(parRange, neqNull);
+ }
+ foreach (var pre in m.Req) {
+ if (!pre.IsFree) {
+ parRange = Expression.CreateAnd(parRange, Substitute(pre.E, receiverReplacement, substMap));
+ }
+ }
+ // construct an expression (generator) for: VF' << VF
+ ExpressionConverter decrCheck = delegate(Dictionary<IVariable, Expression> decrSubstMap, ExpressionTranslator exprTran) {
+ var decrToks = new List<IToken>();
+ var decrTypes = new List<Type>();
+ var decrCallee = new List<Expr>();
+ var decrCaller = new List<Expr>();
+ foreach (var ee in m.Decreases.Expressions) {
+ decrToks.Add(ee.tok);
+ decrTypes.Add(ee.Type.NormalizeExpand());
+ decrCaller.Add(exprTran.TrExpr(ee));
+ Expression es = Substitute(ee, receiverReplacement, substMap);
+ es = Substitute(es, null, decrSubstMap);
+ decrCallee.Add(exprTran.TrExpr(es));
+ }
+ return DecreasesCheck(decrToks, decrTypes, decrTypes, decrCallee, decrCaller, null, null, false, true);
+ };
#if VERIFY_CORRECTNESS_OF_TRANSLATION_FORALL_STATEMENT_RANGE
- var definedness = new Bpl.StmtListBuilder();
- var exporter = new Bpl.StmtListBuilder();
- TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);
- // All done, so put the two pieces together
- builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
+ var definedness = new Bpl.StmtListBuilder();
+ var exporter = new Bpl.StmtListBuilder();
+ TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, definedness, exporter, localVariables, etran);
+ // All done, so put the two pieces together
+ builder.Add(new Bpl.IfCmd(m.tok, null, definedness.Collect(m.tok), null, exporter.Collect(m.tok)));
#else
- TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);
+ TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, recursiveCall, null, builder, localVariables, etran);
#endif
- }
}
// translate the body of the method
Contract.Assert(m.Body != null); // follows from method precondition and the if guard
@@ -12965,8 +12956,8 @@ namespace Microsoft.Dafny { /* NB: only for type arg less quantifiers for now: */
&& ((QuantifierExpr)expr).TypeArgs.Count == 0) {
var e = (QuantifierExpr)expr;
- var inductionVariables = ApplyInduction(e);
- if (apply_induction && 2 <= DafnyOptions.O.Induction && inductionVariables.Count != 0) {
+ var inductionVariables = ApplyInduction(e.BoundVars, e.Attributes);
+ if (apply_induction && inductionVariables.Count != 0) {
// From the given quantifier (forall n :: P(n)), generate the seemingly weaker proof obligation
// (forall n :: (forall k :: k < n ==> P(k)) ==> P(n))
// For an existential (exists n :: P(n)), it is
@@ -13165,297 +13156,29 @@ namespace Microsoft.Dafny { return RefinementToken.IsInherited(expr.tok, currentModule) && (codeContext == null || !codeContext.MustReverify) && RefinementTransformer.ContainsChange(expr, currentModule);
}
- List<BoundVar> ApplyInduction(QuantifierExpr e) {
- Contract.Requires(e.TypeArgs.Count == 0);
- return ApplyInduction(e.BoundVars, e.Attributes, new List<Expression>() { e.LogicalBody() },
- delegate(System.IO.TextWriter wr) { new Printer(wr).PrintExpression(e, true); });
- }
-
- delegate void TracePrinter(System.IO.TextWriter wr);
-
/// <summary>
/// Return a subset of "boundVars" (in the order giving in "boundVars") to which to apply induction to,
- /// according to :induction attributes in "attributes" and heuristically interesting subexpressions of
- /// "searchExprs".
+ /// according to :_induction attribute in "attributes".
/// </summary>
- List<VarType> ApplyInduction<VarType>(List<VarType> boundVars, Attributes attributes, List<Expression> searchExprs, TracePrinter tracePrinter) where VarType : class, IVariable
+ List<VarType> ApplyInduction<VarType>(List<VarType> boundVars, Attributes attributes) where VarType : class, IVariable
{
Contract.Requires(boundVars != null);
- Contract.Requires(searchExprs != null);
- Contract.Requires(tracePrinter != null);
Contract.Ensures(Contract.Result<List<VarType>>() != null);
- if (DafnyOptions.O.Induction == 0) {
+ var args = Attributes.FindExpressions(attributes, "_induction");
+ if (args == null) {
return new List<VarType>(); // don't apply induction
}
- foreach (var a in attributes.AsEnumerable()) {
- if (a.Name == "induction") {
- // Here are the supported forms of the :induction attribute.
- // :induction -- apply induction to all bound variables
- // :induction false -- suppress induction, that is, don't apply it to any bound variable
- // :induction L where L is a list consisting entirely of bound variables:
- // -- apply induction to the specified bound variables
- // :induction X where X is anything else
- // -- treat the same as {:induction}, that is, apply induction to all
- // bound variables
-
- // Handle {:induction false}
- if (a.Args.Count == 1) {
- var arg = a.Args[0] as LiteralExpr;
- if (arg != null && arg.Value is bool && !(bool)arg.Value) {
- if (CommandLineOptions.Clo.Trace) {
- Console.Write("Suppressing automatic induction for: ");
- tracePrinter(Console.Out);
- Console.WriteLine();
- }
- return new List<VarType>();
- }
- }
-
- // Handle {:induction L}
- if (a.Args.Count != 0) {
- // check that all attribute arguments refer to bound variables; otherwise, go to default_form
- var argsAsVars = new List<VarType>();
- foreach (var arg in a.Args) {
- var theArg = arg.Resolved;
- if (theArg is ThisExpr) {
- foreach (var bv in boundVars) {
- if (bv is ThisSurrogate) {
- argsAsVars.Add(bv);
- goto TRY_NEXT_ATTRIBUTE_ARGUMENT;
- }
- }
- } else if (theArg is IdentifierExpr) {
- var id = (IdentifierExpr)theArg;
- var bv = id.Var as VarType;
- if (bv != null && boundVars.Contains(bv)) {
- argsAsVars.Add(bv);
- goto TRY_NEXT_ATTRIBUTE_ARGUMENT;
- }
- }
- // the attribute argument was not one of the possible induction variables
- goto USE_DEFAULT_FORM;
- TRY_NEXT_ATTRIBUTE_ARGUMENT:
- ;
- }
- // so, all attribute arguments are variables; add them to L in the order of the bound variables (not necessarily the order in the attribute)
- var L = new List<VarType>();
- foreach (var bv in boundVars) {
- if (argsAsVars.Contains(bv)) {
- L.Add(bv);
- }
- }
- if (CommandLineOptions.Clo.Trace) {
- string sep = "Applying requested induction on ";
- foreach (var bv in L) {
- Console.Write("{0}{1}", sep, bv.Name);
- sep = ", ";
- }
- Console.Write(" of: ");
- tracePrinter(Console.Out);
- Console.WriteLine();
- }
- return L;
- USE_DEFAULT_FORM: ;
- }
-
- // We have the {:induction} case, or something to be treated in the same way
- if (CommandLineOptions.Clo.Trace) {
- Console.Write("Applying requested induction on all bound variables of: ");
- tracePrinter(Console.Out);
- Console.WriteLine();
- }
- return boundVars;
- }
- }
-
- if (DafnyOptions.O.Induction < 2) {
- return new List<VarType>(); // don't apply induction
- }
-
- // consider automatically applying induction
- var inductionVariables = new List<VarType>();
- foreach (var n in boundVars) {
- if (!n.Type.IsTypeParameter && searchExprs.Exists(expr => VarOccursInArgumentToRecursiveFunction(expr, n))) {
- if (CommandLineOptions.Clo.Trace) {
- Console.Write("Applying automatic induction on variable '{0}' of: ", n.Name);
- tracePrinter(Console.Out);
- Console.WriteLine();
- }
- inductionVariables.Add(n);
- }
- }
-
- return inductionVariables;
- }
-
- /// <summary>
- /// Returns 'true' iff by looking at 'expr' the Induction Heuristic determines that induction should be applied to 'n'.
- /// More precisely:
- /// DafnyInductionHeuristic Return 'true'
- /// ----------------------- -------------
- /// 0 always
- /// 1 if 'n' occurs as any subexpression (of 'expr')
- /// 2 if 'n' occurs as any subexpression of any index argument of an array/sequence select expression or any argument to a recursive function
- /// 3 if 'n' occurs as a prominent subexpression of any index argument of an array/sequence select expression or any argument to a recursive function
- /// 4 if 'n' occurs as any subexpression of any argument to a recursive function
- /// 5 if 'n' occurs as a prominent subexpression of any argument to a recursive function
- /// 6 if 'n' occurs as a prominent subexpression of any decreases-influencing argument to a recursive function
- /// Parameter 'n' is allowed to be a ThisSurrogate.
- /// </summary>
- bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) {
- switch (DafnyOptions.O.InductionHeuristic) {
- case 0: return true;
- case 1: return ContainsFreeVariable(expr, false, n);
- default: return VarOccursInArgumentToRecursiveFunction(expr, n, false);
- }
- }
-
- /// <summary>
- /// Worker routine for VarOccursInArgumentToRecursiveFunction(expr,n), where the additional parameter 'exprIsProminent' says whether or
- /// not 'expr' has prominent status in its context.
- /// DafnyInductionHeuristic cases 0 and 1 are assumed to be handled elsewhere (i.e., a precondition of this method is DafnyInductionHeuristic is at least 2).
- /// Parameter 'n' is allowed to be a ThisSurrogate.
- /// </summary>
- bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, bool exprIsProminent) {
- Contract.Requires(expr != null);
- Contract.Requires(n != null);
-
- // The following variable is what gets passed down to recursive calls if the subexpression does not itself acquire prominent status.
- var subExprIsProminent = DafnyOptions.O.InductionHeuristic == 2 || DafnyOptions.O.InductionHeuristic == 4 ? /*once prominent, always prominent*/exprIsProminent : /*reset the prominent status*/false;
-
- if (expr is ThisExpr) {
- return exprIsProminent && n is ThisSurrogate;
- } else if (expr is IdentifierExpr) {
- var e = (IdentifierExpr)expr;
- return exprIsProminent && e.Var == n;
- } else if (expr is SeqSelectExpr) {
- var e = (SeqSelectExpr)expr;
- var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;
- return VarOccursInArgumentToRecursiveFunction(e.Seq, n, subExprIsProminent) || // this subexpression does not acquire "prominent" status
- (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) || // this one does (unless arrays/sequences are excluded)
- (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q)); // ditto
- } else if (expr is MultiSelectExpr) {
- var e = (MultiSelectExpr)expr;
- var q = DafnyOptions.O.InductionHeuristic < 4 || subExprIsProminent;
- return VarOccursInArgumentToRecursiveFunction(e.Array, n, subExprIsProminent) ||
- e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));
- } else if (expr is FunctionCallExpr) {
- var e = (FunctionCallExpr)expr;
- // For recursive functions: arguments are "prominent"
- // For non-recursive function: arguments are "prominent" if the call is
- var rec = e.Function.IsRecursive && e.CoCall != FunctionCallExpr.CoCallResolution.Yes;
- var decr = e.Function.Decreases.Expressions;
- bool variantArgument;
- if (DafnyOptions.O.InductionHeuristic < 6) {
- variantArgument = rec;
- } else {
- // The receiver is considered to be "variant" if the function is recursive and the receiver participates
- // in the effective decreases clause of the function. The receiver participates if it's a free variable
- // of a term in the explicit decreases clause.
- variantArgument = rec && decr.Exists(ee => ContainsFreeVariable(ee, true, null));
- }
- if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, variantArgument || subExprIsProminent)) {
- return true;
- }
- Contract.Assert(e.Function.Formals.Count == e.Args.Count);
- for (int i = 0; i < e.Function.Formals.Count; i++) {
- var f = e.Function.Formals[i];
- var exp = e.Args[i];
- if (DafnyOptions.O.InductionHeuristic < 6) {
- variantArgument = rec;
- } else if (rec) {
- // The argument position is considered to be "variant" if the function is recursive and...
- // ... it has something to do with why the callee is well-founded, which happens when...
- if (f is ImplicitFormal) {
- // ... it is the argument is the implicit _k parameter, which is always first in the effective decreases clause of a prefix lemma, or
- variantArgument = true;
- } else if (decr.Exists(ee => ContainsFreeVariable(ee, false, f))) {
- // ... it participates in the effective decreases clause of the function, which happens when it is
- // a free variable of a term in the explicit decreases clause, or
- variantArgument = true;
- } else {
- // ... the callee is a prefix predicate.
- variantArgument = true;
- }
- }
- if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument || subExprIsProminent)) {
- return true;
- }
- }
- return false;
- } else if (expr is TernaryExpr) {
- var e = (TernaryExpr)expr;
- switch (e.Op) {
- case TernaryExpr.Opcode.PrefixEqOp:
- case TernaryExpr.Opcode.PrefixNeqOp:
- return VarOccursInArgumentToRecursiveFunction(e.E0, n, true) ||
- VarOccursInArgumentToRecursiveFunction(e.E1, n, subExprIsProminent) ||
- VarOccursInArgumentToRecursiveFunction(e.E2, n, subExprIsProminent);
- default:
- Contract.Assert(false); throw new cce.UnreachableException(); // unexpected ternary expression
- }
- } else if (expr is DatatypeValue) {
- var e = (DatatypeValue)expr;
- var q = n.Type.IsDatatype ? exprIsProminent : subExprIsProminent; // prominent status continues, if we're looking for a variable whose type is a datatype
- return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q));
- } else if (expr is UnaryExpr) {
- var e = (UnaryExpr)expr;
- // both Not and SeqLength preserve prominence
- return VarOccursInArgumentToRecursiveFunction(e.E, n, exprIsProminent);
- } else if (expr is BinaryExpr) {
- var e = (BinaryExpr)expr;
- bool q;
- switch (e.ResolvedOp) {
- case BinaryExpr.ResolvedOpcode.Add:
- case BinaryExpr.ResolvedOpcode.Sub:
- case BinaryExpr.ResolvedOpcode.Mul:
- case BinaryExpr.ResolvedOpcode.Div:
- case BinaryExpr.ResolvedOpcode.Mod:
- case BinaryExpr.ResolvedOpcode.Union:
- case BinaryExpr.ResolvedOpcode.Intersection:
- case BinaryExpr.ResolvedOpcode.SetDifference:
- case BinaryExpr.ResolvedOpcode.Concat:
- // these operators preserve prominence
- q = exprIsProminent;
- break;
- default:
- // whereas all other binary operators do not
- q = subExprIsProminent;
- break;
- }
- return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) ||
- VarOccursInArgumentToRecursiveFunction(e.E1, n, q);
- } else if (expr is StmtExpr) {
- var e = (StmtExpr)expr;
- // ignore the statement
- return VarOccursInArgumentToRecursiveFunction(e.E, n);
-
- } else if (expr is ITEExpr) {
- var e = (ITEExpr)expr;
- return VarOccursInArgumentToRecursiveFunction(e.Test, n, subExprIsProminent) || // test is not "prominent"
- VarOccursInArgumentToRecursiveFunction(e.Thn, n, exprIsProminent) || // but the two branches are
- VarOccursInArgumentToRecursiveFunction(e.Els, n, exprIsProminent);
- } else if (expr is OldExpr ||
- expr is ConcreteSyntaxExpression ||
- expr is BoxingCastExpr ||
- expr is UnboxingCastExpr) {
- foreach (var exp in expr.SubExpressions) {
- if (VarOccursInArgumentToRecursiveFunction(exp, n, exprIsProminent)) { // maintain prominence
- return true;
- }
- }
- return false;
- } else {
- // in all other cases, reset the prominence status and recurse on the subexpressions
- foreach (var exp in expr.SubExpressions) {
- if (VarOccursInArgumentToRecursiveFunction(exp, n, subExprIsProminent)) {
- return true;
- }
- }
- return false;
+ var argsAsVars = new List<VarType>();
+ foreach (var arg in args) {
+ // We expect each "arg" to be an IdentifierExpr among "boundVars"
+ var id = (IdentifierExpr)arg;
+ var bv = (VarType)id.Var;
+ Contract.Assume(boundVars.Contains(bv));
+ argsAsVars.Add(bv);
}
+ return argsAsVars;
}
IEnumerable<Bpl.Expr> InductionCases(Type ty, Bpl.Expr expr, ExpressionTranslator etran) {
@@ -13502,7 +13225,7 @@ namespace Microsoft.Dafny { /// Parameter 'v' is allowed to be a ThisSurrogate, in which case the method return true iff 'this'
/// occurs in 'expr'.
/// </summary>
- static bool ContainsFreeVariable(Expression expr, bool lookForReceiver, IVariable v) {
+ public static bool ContainsFreeVariable(Expression expr, bool lookForReceiver, IVariable v) {
Contract.Requires(expr != null);
Contract.Requires(lookForReceiver || v != null);
|