From 1885f7d7d1fb9bd6ceb8220450dbb5d890501337 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Fri, 2 Oct 2015 15:26:56 -0700 Subject: Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/lemmas (this fixes an item from the wishlist). Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?). Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1]. --- Source/Dafny/Cloner.cs | 91 +++++++++++++++++++++++++++++++++++++------- Source/Dafny/DafnyOptions.cs | 27 +++++++++---- Source/Dafny/Resolver.cs | 16 +++++++- 3 files changed, 111 insertions(+), 23 deletions(-) (limited to 'Source') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index c94c697d..45d8a2c9 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -715,7 +715,7 @@ namespace Microsoft.Dafny { protected readonly Expression k; protected readonly ErrorReporter reporter; - readonly string suffix; + protected readonly string suffix; protected FixpointCloner(Expression k, ErrorReporter reporter) { Contract.Requires(k != null); @@ -724,6 +724,18 @@ namespace Microsoft.Dafny this.reporter = reporter; this.suffix = string.Format("#[{0}]", Printer.ExprToString(k)); } + protected Expression CloneCallAndAddK(FunctionCallExpr e) { + Contract.Requires(e != null); + var receiver = CloneExpr(e.Receiver); + var args = new List(); + args.Add(k); + foreach (var arg in e.Args) { + args.Add(CloneExpr(arg)); + } + var fexp = new FunctionCallExpr(Tok(e.tok), e.Name + "#", receiver, e.OpenParen, args); + reporter.Info(MessageSource.Cloner, e.tok, e.Name + suffix); + return fexp; + } } /// @@ -733,6 +745,7 @@ namespace Microsoft.Dafny /// precondition (resp. postcondition) of the inductive lemma's (resp. colemma's) corresponding prefix lemma. /// It is assumed that the source expression has been resolved. Note, the "k" given to the constructor /// is not cloned with each use; it is simply used as is. + /// The resulting expression needs to be resolved by the caller. /// class FixpointLemmaSpecificationSubstituter : FixpointCloner { @@ -756,15 +769,7 @@ namespace Microsoft.Dafny } else if (expr is FunctionCallExpr) { var e = (FunctionCallExpr)expr; if (friendlyCalls.Contains(e)) { - var receiver = CloneExpr(e.Receiver); - var args = new List(); - args.Add(k); - foreach (var arg in e.Args) { - args.Add(CloneExpr(arg)); - } - var fexp = new FunctionCallExpr(Tok(e.tok), e.Name + "#", receiver, e.OpenParen, args); - reporter.Info(MessageSource.Cloner, e.tok, e.Name); - return fexp; + return CloneCallAndAddK(e); } } else if (expr is BinaryExpr && isCoContext) { var e = (BinaryExpr)expr; @@ -774,7 +779,7 @@ namespace Microsoft.Dafny var B = CloneExpr(e.E1); var teq = new TernaryExpr(Tok(e.tok), op, k, A, B); var opString = op == TernaryExpr.Opcode.PrefixEqOp ? "==" : "!="; - reporter.Info(MessageSource.Cloner, e.tok, opString); + reporter.Info(MessageSource.Cloner, e.tok, opString + suffix); return teq; } } @@ -803,19 +808,77 @@ namespace Microsoft.Dafny } /// - /// The task of the FixpointLemmaBodyCloner is to fill in the implicit _k-1 arguments in recursive inductive/co-lemma calls. + /// The task of the FixpointLemmaBodyCloner is to fill in the implicit _k-1 arguments in recursive inductive/co-lemma calls + /// and in calls to the focal predicates. /// The source statement and the given "k" are assumed to have been resolved. /// class FixpointLemmaBodyCloner : FixpointCloner { readonly FixpointLemma context; - public FixpointLemmaBodyCloner(FixpointLemma context, Expression k, ErrorReporter reporter) + readonly ISet focalPredicates; + public FixpointLemmaBodyCloner(FixpointLemma context, Expression k, ISet focalPredicates, ErrorReporter reporter) : base(k, reporter) { Contract.Requires(context != null); Contract.Requires(k != null); Contract.Requires(reporter != null); this.context = context; + this.focalPredicates = focalPredicates; + } + public override Expression CloneExpr(Expression expr) { + if (DafnyOptions.O.RewriteFocalPredicates) { + if (expr is FunctionCallExpr) { + var e = (FunctionCallExpr)expr; +#if DEBUG_PRINT + if (e.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => e.Function.Name == p.Name + "#")) { + Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e)); + } +#endif + // Note, we don't actually ever get here, because all calls will have been parsed as ApplySuffix. + // However, if something changes in the future (for example, some rewrite that changing an ApplySuffix + // to its resolved FunctionCallExpr), then we do want this code, so with the hope of preventing + // some error in the future, this case is included. (Of course, it is currently completely untested!) + var f = e.Function as FixpointPredicate; + if (f != null && focalPredicates.Contains(f)) { +#if DEBUG_PRINT + var r = CloneCallAndAddK(e); + Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r)); + return r; +#else + return CloneCallAndAddK(e); +#endif + } + } else if (expr is ApplySuffix) { + var apply = (ApplySuffix)expr; + if (!apply.WasResolved()) { + // Since we're assuming the enclosing statement to have been resolved, this ApplySuffix must + // be part of an ExprRhs that actually designates a method call. Such an ApplySuffix does + // not get listed as being resolved, but its components (like its .Lhs) are resolved. + var mse = (MemberSelectExpr)apply.Lhs.Resolved; + Contract.Assume(mse.Member is Method); + } else { + var fce = apply.Resolved as FunctionCallExpr; + if (fce != null) { +#if DEBUG_PRINT + if (fce.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => fce.Function.Name == p.Name + "#")) { + Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce)); + } +#endif + var f = fce.Function as FixpointPredicate; + if (f != null && focalPredicates.Contains(f)) { +#if DEBUG_PRINT + var r = CloneCallAndAddK(fce); + Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r)); + return r; +#else + return CloneCallAndAddK(fce); +#endif + } + } + } + } + } + return base.CloneExpr(expr); } public override AssignmentRhs CloneRHS(AssignmentRhs rhs) { var r = rhs as ExprRhs; @@ -839,7 +902,7 @@ namespace Microsoft.Dafny apply.Args.ForEach(arg => args.Add(CloneExpr(arg))); var applyClone = new ApplySuffix(Tok(apply.tok), lhsClone, args); var c = new ExprRhs(applyClone); - reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name); + reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name + suffix); return c; } } diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 59d0eb2c..2d8756d2 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -65,11 +65,12 @@ namespace Microsoft.Dafny public bool AllowGlobals = false; public bool CountVerificationErrors = true; public bool Optimize = false; - public bool AutoTriggers = false; + public bool AutoTriggers = false; + public bool RewriteFocalPredicates = false; public bool PrintTooltips = false; public bool PrintStats = false; public bool PrintFunctionCallGraph = false; - public bool WarnShadowing = false; + public bool WarnShadowing = false; public bool IronDafny = #if ENABLE_IRONDAFNY true @@ -216,12 +217,20 @@ namespace Microsoft.Dafny case "printTooltips": PrintTooltips = true; - return true; + return true; + + case "autoTriggers": { + int autoTriggers = 0; + if (ps.GetNumericArgument(ref autoTriggers, 2)) { + AutoTriggers = autoTriggers == 1; + } + return true; + } - case "autoTriggers": { - int autoTriggers = 0; - if (ps.GetNumericArgument(ref autoTriggers, 2)) { - AutoTriggers = autoTriggers == 1; + case "rewriteFocalPredicates": { + int rewriteFocalPredicates = 0; + if (ps.GetNumericArgument(ref rewriteFocalPredicates, 2)) { + RewriteFocalPredicates = rewriteFocalPredicates == 1; } return true; } @@ -369,6 +378,10 @@ namespace Microsoft.Dafny 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers. 1 - Add a {:trigger} to each user-level quantifier. Existing annotations are preserved. + /rewriteFocalPredicates: + 0 (default) - Don't rewrite predicates in the body of prefix lemmas. + 1 - In the body of prefix lemmas, rewrite any use of a focal predicate + P to P#[_k-1]. /optimize Produce optimized C# code, meaning: - selects optimized C# prelude by passing /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 36464925..7a540722 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -1565,6 +1565,7 @@ namespace Microsoft.Dafny continue; // something went wrong during registration of the prefix lemma (probably a duplicated fixpoint-lemma name) } var k = prefixLemma.Ins[0]; + var focalPredicates = new HashSet(); if (com is CoLemma) { // compute the postconditions of the prefix lemma Contract.Assume(prefixLemma.Ens.Count == 0); // these are not supposed to have been filled in before @@ -1574,6 +1575,12 @@ namespace Microsoft.Dafny var subst = new FixpointLemmaSpecificationSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this.reporter, true); var post = subst.CloneExpr(p.E); prefixLemma.Ens.Add(new MaybeFreeExpression(post, p.IsFree)); + foreach (var e in coConclusions) { + var fce = e as FunctionCallExpr; + if (fce != null) { // the other possibility is that "e" is a BinaryExpr + focalPredicates.Add((CoPredicate)fce.Function); + } + } } } else { // compute the preconditions of the prefix lemma @@ -1584,13 +1591,18 @@ namespace Microsoft.Dafny var subst = new FixpointLemmaSpecificationSubstituter(antecedents, new IdentifierExpr(k.tok, k.Name), this.reporter, false); var pre = subst.CloneExpr(p.E); prefixLemma.Req.Add(new MaybeFreeExpression(pre, p.IsFree)); + foreach (var e in antecedents) { + var fce = (FunctionCallExpr)e; // we expect "antecedents" to contain only FunctionCallExpr's + focalPredicates.Add((InductivePredicate)fce.Function); + } } } + reporter.Info(MessageSource.Resolver, com.tok, string.Format("{0} specialized for {1}", com.PrefixLemma.Name, Util.Comma(focalPredicates, p => p.Name))); // Compute the statement body of the prefix lemma Contract.Assume(prefixLemma.Body == null); // this is not supposed to have been filled in before if (com.Body != null) { var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1)); - var subst = new FixpointLemmaBodyCloner(com, kMinusOne, this.reporter); + var subst = new FixpointLemmaBodyCloner(com, kMinusOne, focalPredicates, this.reporter); var mainBody = subst.CloneBlockStmt(com.Body); var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name)); var condBody = new IfStmt(com.BodyStartTok, mainBody.EndTok, kPositive, mainBody, null); @@ -3571,7 +3583,7 @@ namespace Microsoft.Dafny var substituter = new Translator.AlphaConverting_Substituter(cs.Receiver, argsSubstMap, new Dictionary(), new Translator(resolver.reporter)); foreach (var ens in cs.Method.Ens) { var p = substituter.Substitute(ens.E); // substitute the call's actuals for the method's formals - resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(p) + ";"); + resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(p)); } } } -- cgit v1.2.3