From 6027c65707f6098bec2e373b738d80b96cbc0a15 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Sat, 29 Oct 2011 16:59:46 -0700 Subject: Dafny induction: * implemented induction tactic for result-less, non-mutating ghost methods * refine heuristics for determining if a variables is usefully passed to a recursive function * disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy) * added command-line flags /induction and /inductionHeuristic (everything is on by default) --- Source/Dafny/Compiler.cs | 10 +- Source/Dafny/Dafny.atg | 1 + Source/Dafny/DafnyAst.cs | 19 +- Source/Dafny/Parser.cs | 1 + Source/Dafny/Resolver.cs | 53 ++++- Source/Dafny/Translator.cs | 555 +++++++++++++++++++++++++++++++++++---------- 6 files changed, 494 insertions(+), 145 deletions(-) (limited to 'Source/Dafny') diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 9938d30a..61b0398f 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -959,13 +959,9 @@ namespace Microsoft.Dafny { // ingredients.Add(new L-Tuple( LHS0(w,x,y,z), LHS1(w,x,y,z), ..., RHS(w,x,y,z) )); // } Indent(indent + n * IndentAmount); - wr.Write("if ("); - if (s.Range == null) { - wr.Write("true"); - } else { - TrExpr(s.Range); - } - wr.WriteLine(") {"); + wr.Write("if "); + TrParenExpr(s.Range); + wr.WriteLine(" {"); Indent(indent + (n + 1) * IndentAmount); wr.Write("{0}.Add(new System.Tuple<{1}>(", ingredients, tupleTypeArgs); diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 9de1421b..fa857aad 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -922,6 +922,7 @@ ParallelStmt "parallel" (. x = t; .) "(" QuantifierDomain + (. if (range == null) { range = new LiteralExpr(x, true); } .) ")" { (. isFree = false; .) [ "free" (. isFree = true; .) diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 88862483..bf8eb6b0 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1040,6 +1040,19 @@ namespace Microsoft.Dafny { } } + /// + /// A "ThisSurrogate" is used during translation time to make the treatment of the receiver more similar to + /// the treatment of other in-parameters. + /// + public class ThisSurrogate : Formal + { + public ThisSurrogate(IToken tok, Type type) + : base(tok, "this", type, true, false) { + Contract.Requires(tok != null); + Contract.Requires(type != null); + } + } + public class BoundVar : NonglobalVariable { public override bool IsMutable { get { @@ -2009,7 +2022,6 @@ namespace Microsoft.Dafny { : base(tok) { // represents the Dafny literal "null" Contract.Requires(tok != null); this.Value = null; - } public LiteralExpr(IToken tok, BigInteger n) @@ -2018,7 +2030,6 @@ namespace Microsoft.Dafny { Contract.Requires(0 <= n.Sign); this.Value = n; - } public LiteralExpr(IToken tok, int n) :base(tok){ @@ -2297,7 +2308,9 @@ namespace Microsoft.Dafny { public override IEnumerable SubExpressions { get { - yield return Receiver; + if (!Function.IsStatic) { + yield return Receiver; + } foreach (var e in Args) { yield return e; } diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 57f4c46e..2fc50c37 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1233,6 +1233,7 @@ List/*!*/ decreases) { x = t; Expect(33); QuantifierDomain(out bvars, out attrs, out range); + if (range == null) { range = new LiteralExpr(x, true); } Expect(34); while (la.kind == 29 || la.kind == 31) { isFree = false; diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 5d806aa9..a4d99bd0 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -785,8 +785,36 @@ namespace Microsoft.Dafny { ResolveAttributes(m.Attributes, false); // ... continue resolving specification + bool twoState = true; + if (m.Mod.Count == 0 && m.Outs.Count == 0) { + // In this special case, the current translation of parallel Call statements would be unsound. + // The reason is that the parallel Call statement does not advance the heap, so there had better + // not be any way to say that the post-heap is definitely different than the pre-heap. For example, + // the following program, is permitted, would unsoundly verify: + // ghost static method M(y: int) + // ensures exists o: object :: o != null && fresh(o); + // { + // var p := new object; + // } + // method Main() { + // parallel (x) { M(x); } + // assert false; + // } + // In fact, here is another method M that together with Main above would yield unsound verification: + // class C { ghost var data: int; } + // ghost static method M(y: int) + // ensures exists c: C :: c != null && c.data != old(c.data); + // { + // var c := new C; + // c.data := c.data + 1; + // } + // So, it seems best just to disallow two-state postconditions in these cases. Perhaps the error + // message will not explain enough of the reasons for this restriction, but the restriction does + // not seem to rule out any useful programs. + twoState = false; + } foreach (MaybeFreeExpression e in m.Ens) { - ResolveExpression(e.E, true); + ResolveExpression(e.E, twoState); Contract.Assert(e.E.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(e.E.Type, Type.Bool)) { Error(e.E, "Postcondition must be a boolean (got {0})", e.E.Type); @@ -1490,15 +1518,13 @@ namespace Microsoft.Dafny { } ResolveType(v.tok, v.Type); } - if (s.Range != null) { - ResolveExpression(s.Range, true); - Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression - if (!UnifyTypes(s.Range.Type, Type.Bool)) { - Error(stmt, "range restriction in parallel statement must be of type bool (instead got {0})", s.Range.Type); - } + ResolveExpression(s.Range, true); + Contract.Assert(s.Range.Type != null); // follows from postcondition of ResolveExpression + if (!UnifyTypes(s.Range.Type, Type.Bool)) { + Error(stmt, "range restriction in parallel statement must be of type bool (instead got {0})", s.Range.Type); } foreach (var ens in s.Ens) { - ResolveExpression(ens.E, true); + ResolveExpression(ens.E, false); // Note, two-state features are not allowed (see the resolution of method postconditions in this file, and see the X_ examples in Test/dafny0/ParallelResolveErrors.dfy) Contract.Assert(ens.E.Type != null); // follows from postcondition of ResolveExpression if (!UnifyTypes(ens.E.Type, Type.Bool)) { Error(ens.E, "ensures condition is expected to be of type {0}, but is {1}", Type.Bool, ens.E.Type); @@ -1546,7 +1572,11 @@ namespace Microsoft.Dafny { s.Kind = ParallelStmt.ParBodyKind.Call; } else { s.Kind = ParallelStmt.ParBodyKind.Proof; - Warning(s.Tok, "the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause"); + if (s.Body is BlockStmt && ((BlockStmt)s.Body).Body.Count == 0) { + // an empty statement, so don't produce any warning + } else { + Warning(s.Tok, "the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause"); + } } } CheckParallelBodyRestrictions(s.Body, s.Kind == ParallelStmt.ParBodyKind.Assign); @@ -3248,13 +3278,14 @@ namespace Microsoft.Dafny { /// /// Tries to find a bounded pool for each of the bound variables "bvars" of "expr". If this process /// fails, then "null" is returned and the bound variables for which the process fails are added to "missingBounds". - /// Requires "e" to be successfully resolved. + /// Requires "expr" to be successfully resolved. /// List DiscoverBounds(IToken tok, List bvars, Expression expr, bool polarity, List missingBounds) { Contract.Requires(tok != null); Contract.Requires(bvars != null); Contract.Requires(missingBounds != null); - Contract.Requires(expr.Type != null); // a sanity check (but not a complete proof) that "e" has been resolved + Contract.Requires(expr != null); + Contract.Requires(expr.Type != null); // a sanity check (but not a complete proof) that "expr" has been resolved Contract.Ensures( (Contract.Result>() != null && Contract.Result>().Count == bvars.Count && diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 61f3dad3..a6198625 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -479,6 +479,22 @@ namespace Microsoft.Dafny { i++; } } + + // Add: + // function $IsA#Dt(d: DatatypeType): bool { + // Dt.Ctor0?(d) || Dt.Ctor1?(d) || ... + // } + var cases_dBv = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, "d", predef.DatatypeType), true); + var cases_dId = new Bpl.IdentifierExpr(dt.tok, cases_dBv.Name, predef.DatatypeType); + Bpl.Expr cases_body = null; + foreach (DatatypeCtor ctor in dt.Ctors) { + var disj = FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, cases_dId); + cases_body = cases_body == null ? disj : Bpl.Expr.Or(cases_body, disj); + } + var cases_resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false); + var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.Name, new Bpl.VariableSeq(cases_dBv), cases_resType); + cases_fn.Body = cases_body; + sink.TopLevelDeclarations.Add(cases_fn); } void CreateBoundVariables(List/*!*/ formals, out Bpl.VariableSeq/*!*/ bvs, out List/*!*/ args) @@ -1022,8 +1038,124 @@ namespace Microsoft.Dafny { ExpressionTranslator etran = new ExpressionTranslator(this, predef, m.tok); Bpl.VariableSeq localVariables = new Bpl.VariableSeq(); GenerateImplPrelude(m, inParams, outParams, builder, localVariables); + Bpl.StmtList stmts; if (!wellformednessProc) { + if (3 <= CommandLineOptions.Clo.DafnyInduction && m.IsGhost && m.Mod.Count == 0 && m.Outs.Count == 0) { + var posts = new List(); + m.Ens.ForEach(mfe => posts.Add(mfe.E)); + var allIns = new List(); + 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' ]]; + // parallel (this', y' | Pre(this', x, y') && VF(this', x, y') << VF(this, x, y)) { + // this'.M(x, y'); + // } + // Generate bound variables for the parallel 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.Name, Bpl.Type.Bool)); + var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.UniqueName, TrType(inFormal.Type)); + builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new Bpl.ExprSeq(f)))); + } + } + + var parBoundVars = new List(); + Expression receiverReplacement = null; + var substMap = new Dictionary(); + 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); // 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(); + 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 recursiveCall = new CallStmt(m.tok, new List(), recursiveCallReceiver, m.Name, recursiveCallArgs); + recursiveCall.Method = m; // 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 = DafnyAnd(parRange, neqNull); + } + foreach (var pre in m.Req) { + if (!pre.IsFree) { + parRange = DafnyAnd(parRange, Substitute(pre.E, receiverReplacement, substMap)); + } + } + // construct an expression (generator) for: VF' << VF + ExpressionConverter decrCheck = delegate(Dictionary decrSubstMap) { + var decrToks = new List(); + var decrTypes = new List(); + var decrCallee = new List(); + var decrCaller = new List(); + bool decrInferred; // we don't actually care + foreach (var ee in MethodDecreasesWithDefault(m, out decrInferred)) { + decrToks.Add(ee.tok); + decrTypes.Add(ee.Type); + decrCaller.Add(etran.TrExpr(ee)); + Expression es = Substitute(ee, receiverReplacement, substMap); + es = Substitute(es, null, decrSubstMap); + decrCallee.Add(etran.TrExpr(es)); + } + return DecreasesCheck(decrToks, decrTypes, decrCallee, decrCaller, etran, null, null, false, true); + }; + +#if VERIFY_CORRECTNESS_OF_TRANSLATION_PARALLEL_RANGE + var definedness = new Bpl.StmtListBuilder(); + var exporter = new Bpl.StmtListBuilder(); + TrParallelCall(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 + TrParallelCall(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 stmts = TrStmt2StmtList(builder, m.Body, localVariables, etran); @@ -1555,6 +1687,7 @@ namespace Microsoft.Dafny { Expression precond = Substitute(p, e.Receiver, substMap); r = BplAnd(r, etran.TrExpr(precond)); } + // TODO: if this is a recursive call, also conjoin the well-ordering predicate return r; } else if (expr is DatatypeValue) { DatatypeValue dtv = (DatatypeValue)expr; @@ -1788,6 +1921,23 @@ namespace Microsoft.Dafny { return total; } + Expression DafnyAnd(Expression a, Expression b) { + Contract.Requires(a != null); + Contract.Requires(b != null); + Contract.Ensures(Contract.Result() != null); + + if (LiteralExpr.IsTrue(a)) { + return b; + } else if (LiteralExpr.IsTrue(b)) { + return a; + } else { + BinaryExpr and = new BinaryExpr(a.tok, BinaryExpr.Opcode.And, a, b); + and.ResolvedOp = BinaryExpr.ResolvedOpcode.And; // resolve here + and.Type = Type.Bool; // resolve here + return and; + } + } + Bpl.Expr BplAnd(Bpl.Expr a, Bpl.Expr b) { Contract.Requires(a != null); Contract.Requires(b != null); @@ -2282,10 +2432,7 @@ namespace Microsoft.Dafny { if (prefix == null) { prefix = guardConjunct; } else { - BinaryExpr and = new BinaryExpr(tok, BinaryExpr.Opcode.And, prefix, guardConjunct); - and.ResolvedOp = BinaryExpr.ResolvedOpcode.And; // resolve here - and.Type = Type.Bool; // resolve here - prefix = and; + prefix = DafnyAnd(prefix, guardConjunct); } } } @@ -2353,6 +2500,20 @@ namespace Microsoft.Dafny { } } + void CloneVariableAsBoundVar(IToken tok, IVariable iv, string prefix, out BoundVar bv, out IdentifierExpr ie) { + Contract.Requires(tok != null); + Contract.Requires(iv != null); + Contract.Requires(prefix != null); + Contract.Ensures(Contract.ValueAtReturn(out bv) != null); + Contract.Ensures(Contract.ValueAtReturn(out ie) != null); + + bv = new BoundVar(tok, prefix + otherTmpVarCount, iv.Type); + otherTmpVarCount++; // use this counter, but for a Dafny name (the idea being that the number and the initial "_" in the name might avoid name conflicts) + ie = new IdentifierExpr(tok, bv.Name); + ie.Var = bv; // resolve here + ie.Type = bv.Type; // resolve here + } + Bpl.Constant GetClass(TopLevelDecl cl) { Contract.Requires(cl != null); @@ -3208,7 +3369,7 @@ namespace Microsoft.Dafny { var s0 = (CallStmt)s.S0; var definedness = new Bpl.StmtListBuilder(); var exporter = new Bpl.StmtListBuilder(); - TrParallelCall(s, s0, definedness, exporter, locals, etran); + TrParallelCall(s.Tok, s.BoundVars, s.Range, null, s0, definedness, exporter, locals, etran); // All done, so put the two pieces together builder.Add(new Bpl.IfCmd(s.Tok, null, definedness.Collect(s.Tok), null, exporter.Collect(s.Tok))); builder.Add(CaptureState(stmt.Tok)); @@ -3347,11 +3508,9 @@ namespace Microsoft.Dafny { // } var substMap = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran); - if (s.Range != null) { - Expression range = Substitute(s.Range, null, substMap); - TrStmt_CheckWellformed(range, definedness, locals, etran, false); - definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(range))); - } + Expression range = Substitute(s.Range, null, substMap); + TrStmt_CheckWellformed(range, definedness, locals, etran, false); + definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(range))); var lhs = Substitute(s0.Lhs.Resolved, null, substMap); TrStmt_CheckWellformed(lhs, definedness, locals, etran, false); @@ -3378,10 +3537,8 @@ namespace Microsoft.Dafny { // check for duplicate LHSs var substMapPrime = SetupBoundVarsAsLocals(s.BoundVars, definedness, locals, etran); var lhsPrime = Substitute(s0.Lhs.Resolved, null, substMapPrime); - if (s.Range != null) { - Expression range = Substitute(s.Range, null, substMapPrime); - definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range))); - } + range = Substitute(s.Range, null, substMapPrime); + definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range))); // assume !(x == x' && y == y'); Bpl.Expr eqs = Bpl.Expr.True; foreach (var bv in s.BoundVars) { @@ -3421,9 +3578,7 @@ namespace Microsoft.Dafny { Bpl.Expr oldHeapOF = ExpressionTranslator.ReadHeap(s.Tok, prevHeap, o, f); Bpl.VariableSeq xBvars = new Bpl.VariableSeq(); var xBody = etran.TrBoundVariables(s.BoundVars, xBvars); - if (s.Range != null) { - xBody = BplAnd(xBody, prevEtran.TrExpr(s.Range)); - } + xBody = BplAnd(xBody, prevEtran.TrExpr(s.Range)); Bpl.Expr xObj, xField; GetObjFieldDetails(s0.Lhs.Resolved, prevEtran, out xObj, out xField); xBody = BplAnd(xBody, Bpl.Expr.Eq(o, xObj)); @@ -3438,9 +3593,7 @@ namespace Microsoft.Dafny { // $Heap[ Object(x,y)[$Heap:=oldHeap], Field(x,y)[$Heap:=oldHeap] ] == G[$Heap:=oldHeap] )); xBvars = new Bpl.VariableSeq(); Bpl.Expr xAnte = etran.TrBoundVariables(s.BoundVars, xBvars); - if (s.Range != null) { - xAnte = BplAnd(xAnte, prevEtran.TrExpr(s.Range)); - } + xAnte = BplAnd(xAnte, prevEtran.TrExpr(s.Range)); var rhs = ((ExprRhs)s0.Rhs).Expr; var g = prevEtran.TrExpr(rhs); GetObjFieldDetails(s0.Lhs.Resolved, prevEtran, out xObj, out xField); @@ -3459,7 +3612,20 @@ namespace Microsoft.Dafny { } } - void TrParallelCall(ParallelStmt s, CallStmt s0, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) { + delegate Bpl.Expr ExpressionConverter(Dictionary substMap); + + void TrParallelCall(IToken tok, List boundVars, Expression range, ExpressionConverter additionalRange, CallStmt s0, + Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) { + Contract.Requires(tok != null); + Contract.Requires(boundVars != null); + Contract.Requires(range != null); + // additionalRange is allowed to be null + Contract.Requires(s0 != null); + // definedness is allowed to be null + Contract.Requires(exporter != null); + Contract.Requires(locals != null); + Contract.Requires(etran != null); + // Translate: // parallel (x,y | Range(x,y)) { // E(x,y) . M( Args(x,y) ); @@ -3470,58 +3636,64 @@ namespace Microsoft.Dafny { // havoc x,y; // CheckWellformed( Range ); // assume Range(x,y); + // assume additionalRange; // Tr( Call ); // assume false; // } else { - // assume (forall x,y :: Range(x,y) ==> Post( E(x,y), Args(x,y) )); + // assume (forall x,y :: Range(x,y) && additionalRange ==> Post( E(x,y), Args(x,y) )); // } // where Post(this,args) is the postcondition of method M. - // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals - // here (rather than a TrBoundVariables). However, there is currently no way to apply - // a substMap to a statement (in particular, to s.Body), so that doesn't work here. - Bpl.VariableSeq bvars = new Bpl.VariableSeq(); - var ante = etran.TrBoundVariables(s.BoundVars, bvars, true); - locals.AddRange(bvars); - var havocIds = new Bpl.IdentifierExprSeq(); - foreach (Bpl.Variable bv in bvars) { - havocIds.Add(new Bpl.IdentifierExpr(s.Tok, bv)); - } - definedness.Add(new Bpl.HavocCmd(s.Tok, havocIds)); - definedness.Add(new Bpl.AssumeCmd(s.Tok, ante)); - if (s.Range != null) { - TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false); - definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range))); - } + if (definedness != null) { + // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals + // here (rather than a TrBoundVariables). However, there is currently no way to apply + // a substMap to a statement (in particular, to s.Body), so that doesn't work here. + Bpl.VariableSeq bvars = new Bpl.VariableSeq(); + var ante = etran.TrBoundVariables(boundVars, bvars, true); + locals.AddRange(bvars); + var havocIds = new Bpl.IdentifierExprSeq(); + foreach (Bpl.Variable bv in bvars) { + havocIds.Add(new Bpl.IdentifierExpr(tok, bv)); + } + definedness.Add(new Bpl.HavocCmd(tok, havocIds)); + definedness.Add(new Bpl.AssumeCmd(tok, ante)); + TrStmt_CheckWellformed(range, definedness, locals, etran, false); + definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range))); + if (additionalRange != null) { + var es = additionalRange(new Dictionary()); + definedness.Add(new Bpl.AssumeCmd(es.tok, es)); + } - TrStmt(s0, definedness, locals, etran); + TrStmt(s0, definedness, locals, etran); - definedness.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False)); + definedness.Add(new Bpl.AssumeCmd(tok, Bpl.Expr.False)); + } // Now for the other branch, where the postcondition of the call is exported. + { + var bvars = new Bpl.VariableSeq(); + Dictionary substMap; + var ante = etran.TrBoundVariablesRename(boundVars, bvars, out substMap); + ante = BplAnd(ante, etran.TrExpr(Substitute(range, null, substMap))); + if (additionalRange != null) { + ante = BplAnd(ante, additionalRange(substMap)); + } - bvars = new Bpl.VariableSeq(); - Dictionary substMap; - ante = etran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap); - if (s.Range != null) { - var range = Substitute(s.Range, null, substMap); - ante = BplAnd(ante, etran.TrExpr(range)); - } + var argsSubstMap = new Dictionary(); // maps formal arguments to actuals + Contract.Assert(s0.Method.Ins.Count == s0.Args.Count); + for (int i = 0; i < s0.Method.Ins.Count; i++) { + argsSubstMap.Add(s0.Method.Ins[i], s0.Args[i]); + } + Bpl.Expr post = Bpl.Expr.True; + foreach (var ens in s0.Method.Ens) { + var p = Substitute(ens.E, s0.Receiver, argsSubstMap); // substitute the call's actuals for the method's formals + p = Substitute(p, null, substMap); // substitute the renamed bound variables for the declared ones + post = BplAnd(post, etran.TrExpr(p)); + } - var argsSubstMap = new Dictionary(); // maps formal arguments to actuals - Contract.Assert(s0.Method.Ins.Count == s0.Args.Count); - for (int i = 0; i < s0.Method.Ins.Count; i++) { - argsSubstMap.Add(s0.Method.Ins[i], s0.Args[i]); + Bpl.Expr qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post)); + exporter.Add(new Bpl.AssumeCmd(tok, qq)); } - Bpl.Expr post = Bpl.Expr.True; - foreach (var ens in s0.Method.Ens) { - var p = Substitute(ens.E, s0.Receiver, argsSubstMap); // substitute the call's actuals for the method's formals - p = Substitute(p, null, substMap); // substitute the renamed bound variables for the declared ones - post = BplAnd(post, etran.TrExpr(p)); - } - - Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, bvars, Bpl.Expr.Imp(ante, post)); - exporter.Add(new Bpl.AssumeCmd(s.Tok, qq)); } void TrParallelProof(ParallelStmt s, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, Bpl.VariableSeq locals, ExpressionTranslator etran) { @@ -3557,10 +3729,8 @@ namespace Microsoft.Dafny { } definedness.Add(new Bpl.HavocCmd(s.Tok, havocIds)); definedness.Add(new Bpl.AssumeCmd(s.Tok, ante)); - if (s.Range != null) { - TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false); - definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range))); - } + TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false); + definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range))); TrStmt(s.Body, definedness, locals, etran); @@ -3584,11 +3754,8 @@ namespace Microsoft.Dafny { bvars = new Bpl.VariableSeq(); Dictionary substMap; ante = etran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap); - if (s.Range != null) { - var range = Substitute(s.Range, null, substMap); - TrStmt_CheckWellformed(range, definedness, locals, etran, false); - ante = BplAnd(ante, etran.TrExpr(range)); - } + var range = Substitute(s.Range, null, substMap); + ante = BplAnd(ante, etran.TrExpr(range)); Bpl.Expr post = Bpl.Expr.True; foreach (var ens in s.Ens) { @@ -4148,7 +4315,7 @@ namespace Microsoft.Dafny { Contract.Requires(etran != null); Contract.Requires(predef != null); Contract.Requires(types.Count == ee0.Count && ee0.Count == ee1.Count); - Contract.Requires((builder != null) == (suffixMsg != null)); + Contract.Requires(builder == null || suffixMsg != null); Contract.Ensures(Contract.Result() != null); int N = types.Count; @@ -6268,7 +6435,7 @@ namespace Microsoft.Dafny { } else if ((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) { var e = (QuantifierExpr)expr; var inductionVariables = ApplyInduction(e); - if (inductionVariables.Count != 0) { + if (2 <= CommandLineOptions.Clo.DafnyInduction && 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 @@ -6360,12 +6527,30 @@ namespace Microsoft.Dafny { } } - List ApplyInduction(QuantifierExpr e) + List ApplyInduction(QuantifierExpr e) { + return ApplyInduction(e.BoundVars, e.Attributes, new List() { e.LogicalBody() }, + delegate(System.IO.TextWriter wr) { new Printer(Console.Out).PrintExpression(e); }); + } + + delegate void TracePrinter(System.IO.TextWriter wr); + + /// + /// 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". + /// + List ApplyInduction(List boundVars, Attributes attributes, List searchExprs, TracePrinter tracePrinter) where VarType : class, IVariable { - Contract.Requires(e != null); - Contract.Ensures(Contract.Result>() != null); + Contract.Requires(boundVars != null); + Contract.Requires(searchExprs != null); + Contract.Requires(tracePrinter != null); + Contract.Ensures(Contract.Result>() != null); + + if (CommandLineOptions.Clo.DafnyInduction == 0) { + return new List(); // don't apply induction + } - for (var a = e.Attributes; a != null; a = a.Prev) { + for (var a = attributes; a != null; a = a.Prev) { if (a.Name == "induction") { // Here are the supported forms of the :induction attribute. // :induction -- apply induction to all bound variables @@ -6382,26 +6567,44 @@ namespace Microsoft.Dafny { if (arg != null && arg.Value is bool && !(bool)arg.Value) { if (CommandLineOptions.Clo.Trace) { Console.Write("Suppressing automatic induction for: "); - new Printer(Console.Out).PrintExpression(e); + tracePrinter(Console.Out); Console.WriteLine(); } - return new List(); + return new List(); } } // Handle {:induction L} if (a.Args.Count != 0) { - var L = new List(); + // check that all attribute arguments refer to bound variables; otherwise, go to default_form + var argsAsVars = new List(); foreach (var arg in a.Args) { - var id = arg.E.Resolved as IdentifierExpr; - var bv = id == null ? null : id.Var as BoundVar; - if (bv != null && e.BoundVars.Contains(bv)) { - // add to L, but don't add duplicates - if (!L.Contains(bv)) { - L.Add(bv); + var theArg = arg.E.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; } - } else { - goto USE_DEFAULT_FORM; + } + // 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(); + foreach (var bv in boundVars) { + if (argsAsVars.Contains(bv)) { + L.Add(bv); } } if (CommandLineOptions.Clo.Trace) { @@ -6411,7 +6614,7 @@ namespace Microsoft.Dafny { sep = ", "; } Console.Write(" of: "); - new Printer(Console.Out).PrintExpression(e); + tracePrinter(Console.Out); Console.WriteLine(); } return L; @@ -6421,20 +6624,24 @@ namespace Microsoft.Dafny { // 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: "); - new Printer(Console.Out).PrintExpression(e); + tracePrinter(Console.Out); Console.WriteLine(); } - return e.BoundVars; + return boundVars; } } + if (CommandLineOptions.Clo.DafnyInduction < 2) { + return new List(); // don't apply induction + } + // consider automatically applying induction - var inductionVariables = new List(); - foreach (var n in e.BoundVars) { - if (!n.Type.IsTypeParameter && VarOccursInArgumentToRecursiveFunction(e.LogicalBody(), n, null)) { + var inductionVariables = new List(); + 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); - new Printer(Console.Out).PrintExpression(e); + tracePrinter(Console.Out); Console.WriteLine(); } inductionVariables.Add(n); @@ -6447,57 +6654,136 @@ namespace Microsoft.Dafny { /// /// Returns 'true' iff /// there is a subexpression of 'expr' of the form 'F(...n...)' where 'F' is a recursive function - /// and 'n' appears in an "elevated" subexpression of some argument to 'F', + /// and 'n' appears in an "elevated" subexpression of some decreases-contributing argument to 'F', + /// "elevated" essentially means "top-level or top-level under a + or -". + /// Variations, where a higher number means a more discriminating (and, consequently, + /// more complicated) heuristic: + /// * DafnyInductionHeuristic==0: always return 'true' no matter what + /// * DafnyInductionHeuristic==1: replace "elevated" by "any", and look at all arguments to 'F' + /// * DafnyInductionHeuristic==2: look at all arguments to 'F' + /// * DafnyInductionHeuristic==3: as stated above + /// Parameter 'n' is allowed to be a ThisSurrogate. + /// + bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n) { + switch (CommandLineOptions.Clo.DafnyInductionHeuristic) { + case 0: return true; + case 1: return VarOccursInArgumentToRecursiveFunction(expr, n, n); + default: return VarOccursInArgumentToRecursiveFunction(expr, n, null); + } + } + + /// + /// Returns 'true' iff + /// there is a subexpression of 'expr' of the form 'F(...n...)' where 'F' is a recursive function + /// and 'n' appears in an "elevated" subexpression of some decreases-contributing argument to 'F', /// or /// 'p' is non-null and 'p' appears in an "elevated" subexpression of 'expr'. + /// Variations: + /// * DafnyInductionHeuristic LESS 2: replace "elevated" by "any" + /// * DafnyInductionHeuristic LESS 3: look at all arguments to 'F' /// Requires that 'p' is either 'null' of 'n'. + /// Parameters 'n' and 'p' are allowed to be a ThisSurrogate. /// - static bool VarOccursInArgumentToRecursiveFunction(Expression expr, BoundVar n, BoundVar p) { + bool VarOccursInArgumentToRecursiveFunction(Expression expr, IVariable n, IVariable p) { Contract.Requires(expr != null); Contract.Requires(n != null); + Contract.Requires(p == null || p == n); + + var pForNotElevated = CommandLineOptions.Clo.DafnyInductionHeuristic < 2 ? p : null; - if (expr is LiteralExpr || expr is WildcardExpr || expr is ThisExpr || expr is BoogieWrapper) { + if (expr is LiteralExpr || expr is WildcardExpr || expr is BoogieWrapper) { return false; + } else if (expr is ThisExpr) { + return p is ThisSurrogate; } else if (expr is IdentifierExpr) { var e = (IdentifierExpr)expr; return p != null && e.Var == p; } else if (expr is DisplayExpression) { var e = (DisplayExpression)expr; - return e.Elements.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, null)); // subexpressions are not "elevated" + return e.Elements.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, pForNotElevated)); // subexpressions are not "elevated" } else if (expr is FieldSelectExpr) { var e = (FieldSelectExpr)expr; - return VarOccursInArgumentToRecursiveFunction(e.Obj, n, null); // subexpressions are not "elevated" + return VarOccursInArgumentToRecursiveFunction(e.Obj, n, pForNotElevated); // subexpressions are not "elevated" } else if (expr is SeqSelectExpr) { var e = (SeqSelectExpr)expr; - p = e.SelectOne ? null : p; - return VarOccursInArgumentToRecursiveFunction(e.Seq, n, null) || // this subexpression is not "elevated" - (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, p)) || // this one is, if the SeqSelectExpr denotes a range - (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, p)); // ditto + var q = e.SelectOne ? pForNotElevated : p; + return VarOccursInArgumentToRecursiveFunction(e.Seq, n, pForNotElevated) || // this subexpression is not "elevated" + (e.E0 != null && VarOccursInArgumentToRecursiveFunction(e.E0, n, q)) || // this one is, if the SeqSelectExpr denotes a range + (e.E1 != null && VarOccursInArgumentToRecursiveFunction(e.E1, n, q)); // ditto } else if (expr is SeqUpdateExpr) { var e = (SeqUpdateExpr)expr; return VarOccursInArgumentToRecursiveFunction(e.Seq, n, p) || // this subexpression is "elevated" - VarOccursInArgumentToRecursiveFunction(e.Index, n, null) || // but this one - VarOccursInArgumentToRecursiveFunction(e.Value, n, null); // and this one are not + VarOccursInArgumentToRecursiveFunction(e.Index, n, pForNotElevated) || // but this one + VarOccursInArgumentToRecursiveFunction(e.Value, n, pForNotElevated); // and this one are not } else if (expr is MultiSelectExpr) { var e = (MultiSelectExpr)expr; // subexpressions are not "elevated" - return VarOccursInArgumentToRecursiveFunction(e.Array, n, null) || - e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, null)); + return VarOccursInArgumentToRecursiveFunction(e.Array, n, pForNotElevated) || + e.Indices.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, pForNotElevated)); } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; // For recursive functions: arguments are "elevated" // For non-recursive function: arguments are "elevated" if the call is - if (e.Function.IsRecursive) { - p = n; + var rec = e.Function.IsRecursive; + bool inferredDecreases; // we don't actually care + var decr = FunctionDecreasesWithDefault(e.Function, out inferredDecreases); + bool variantArgument; + if (CommandLineOptions.Clo.DafnyInductionHeuristic < 3) { + 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 ? n : p)) { + return true; + } +#if DEBUG_TRACE + if (rec && !variantArgument) { + // rec is true, but variantArgument is not. So, we passed in "p" whereas under the previous approach, we would have passed in "n". + if (n != p) { + // We can now say more precisely: we passed in "null", whereas the previous approach would have passed in "n" + if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, n)) { + // Moreover, passing in "null" instead of "n" actually made a difference here + Console.WriteLine("DEBUG: rec is true but variantArgument is not (this), and it made a difference"); + } + } + } +#endif + 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 (CommandLineOptions.Clo.DafnyInductionHeuristic < 3) { + variantArgument = rec; + } else { + // The argument position is considered to be "variant" if the function is recursive and the argument participates + // in the effective decreases clause of the function. The argument participates if it's a free variable + // of a term in the explicit decreases clause. + variantArgument = rec && decr.Exists(ee => ContainsFreeVariable(ee, false, f)); + } + if (VarOccursInArgumentToRecursiveFunction(exp, n, variantArgument ? n : p)) { + return true; + } +#if DEBUG_TRACE + if (rec && !variantArgument) { + // rec is true, but variantArgument is not. So, we passed in "p" whereas under the previous approach, we would have passed in "n". + if (n != p) { + // We can now say more precisely: we passed in "null", whereas the previous approach would have passed in "n" + if (VarOccursInArgumentToRecursiveFunction(e.Receiver, n, n)) { + // Moreover, passing in "null" instead of "n" actually made a difference here + Console.WriteLine("DEBUG: rec is true but variantArgument is not ({0}), and it made a difference", f.Name); + } + } + } +#endif } - return VarOccursInArgumentToRecursiveFunction(e.Receiver, n, p) || - e.Args.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, p)); + return false; } else if (expr is DatatypeValue) { var e = (DatatypeValue)expr; - if (!n.Type.IsDatatype) { - p = null; - } - return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, p)); + var q = n.Type.IsDatatype ? p : pForNotElevated; + return e.Arguments.Exists(exp => VarOccursInArgumentToRecursiveFunction(exp, n, q)); } else if (expr is OldExpr) { var e = (OldExpr)expr; return VarOccursInArgumentToRecursiveFunction(e.E, n, p); @@ -6506,16 +6792,17 @@ namespace Microsoft.Dafny { return VarOccursInArgumentToRecursiveFunction(e.E, n, p); } else if (expr is FreshExpr) { var e = (FreshExpr)expr; - return VarOccursInArgumentToRecursiveFunction(e.E, n, null); + return VarOccursInArgumentToRecursiveFunction(e.E, n, pForNotElevated); } else if (expr is AllocatedExpr) { var e = (AllocatedExpr)expr; - return VarOccursInArgumentToRecursiveFunction(e.E, n, null); + return VarOccursInArgumentToRecursiveFunction(e.E, n, pForNotElevated); } else if (expr is UnaryExpr) { var e = (UnaryExpr)expr; // arguments to both Not and SeqLength are "elevated" return VarOccursInArgumentToRecursiveFunction(e.E, n, p); } else if (expr is BinaryExpr) { var e = (BinaryExpr)expr; + IVariable q; switch (e.ResolvedOp) { case BinaryExpr.ResolvedOpcode.Add: case BinaryExpr.ResolvedOpcode.Sub: @@ -6527,22 +6814,23 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.SetDifference: case BinaryExpr.ResolvedOpcode.Concat: // these operators have "elevated" arguments + q = p; break; default: // whereas all other binary operators do not - p = null; + q = pForNotElevated; break; } - return VarOccursInArgumentToRecursiveFunction(e.E0, n, p) || - VarOccursInArgumentToRecursiveFunction(e.E1, n, p); + return VarOccursInArgumentToRecursiveFunction(e.E0, n, q) || + VarOccursInArgumentToRecursiveFunction(e.E1, n, q); } else if (expr is ComprehensionExpr) { var e = (ComprehensionExpr)expr; - return (e.Range != null && VarOccursInArgumentToRecursiveFunction(e.Range, n, null)) || - VarOccursInArgumentToRecursiveFunction(e.Term, n, null); + return (e.Range != null && VarOccursInArgumentToRecursiveFunction(e.Range, n, pForNotElevated)) || + VarOccursInArgumentToRecursiveFunction(e.Term, n, pForNotElevated); } else if (expr is ITEExpr) { var e = (ITEExpr)expr; - return VarOccursInArgumentToRecursiveFunction(e.Test, n, null) || // test is not "elevated" - VarOccursInArgumentToRecursiveFunction(e.Thn, n, p) || // but the two branches are + return VarOccursInArgumentToRecursiveFunction(e.Test, n, pForNotElevated) || // test is not "elevated" + VarOccursInArgumentToRecursiveFunction(e.Thn, n, p) || // but the two branches are VarOccursInArgumentToRecursiveFunction(e.Els, n, p); } else if (expr is ConcreteSyntaxExpression) { var e = (ConcreteSyntaxExpression)expr; @@ -6593,7 +6881,26 @@ namespace Microsoft.Dafny { } } - static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary/*!*/ substMap) { + static bool ContainsFreeVariable(Expression expr, bool lookForReceiver, IVariable v) { + Contract.Requires(expr != null); + Contract.Requires(lookForReceiver || v != null); + + if (expr is ThisExpr) { + return lookForReceiver; + } else if (expr is IdentifierExpr) { + IdentifierExpr e = (IdentifierExpr)expr; + return e.Var == v; + } else { + foreach (var ee in expr.SubExpressions) { + if (ContainsFreeVariable(ee, lookForReceiver, v)) { + return true; + } + } + return false; + } + } + + static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary/*!*/ substMap) { Contract.Requires(expr != null); Contract.Requires(cce.NonNullDictionaryAndValues(substMap)); Contract.Ensures(Contract.Result() != null); -- cgit v1.2.3