From 674e30357980e1192ac532f4bd16c529cedc7fdc Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 10:51:44 -0700 Subject: Draft out a more advanced version of trigger generation This new version will include a cleaner pipeline, and trigger splitting. --- Source/Dafny/Triggers/QuantifierSplitter.cs | 66 +++++++++++++++++++++++++++++ 1 file changed, 66 insertions(+) create mode 100644 Source/Dafny/Triggers/QuantifierSplitter.cs (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs new file mode 100644 index 00000000..e83feebb --- /dev/null +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -0,0 +1,66 @@ +using Microsoft.Boogie; +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; + +namespace Microsoft.Dafny.Triggers { + class QuantifierSplitter : BottomUpVisitor { + internal enum Quantifier { Forall, Exists } + + internal static IEnumerable BreakQuantifier(Expression expr, Quantifier quantifier) { + expr = expr.Resolved; + var binary = expr as BinaryExpr; + + if (binary == null) { + yield return expr; + yield break; + } + + var e0 = binary.E0; + var e1 = binary.E1; + + if ((quantifier == Quantifier.Forall && binary.Op == BinaryExpr.Opcode.And) || + (quantifier == Quantifier.Exists && binary.Op == BinaryExpr.Opcode.Or)) { + foreach (var e in BreakQuantifier(e0, quantifier)) { yield return e; } + foreach (var e in BreakQuantifier(e1, quantifier)) { yield return e; } + } else if (binary.Op == BinaryExpr.Opcode.Imp) { + if (quantifier == Quantifier.Forall) { + foreach (var e in BreakImplication(e0, e1, quantifier, expr.tok)) { yield return e; } + } else { + yield return new UnaryOpExpr(e1.tok, UnaryOpExpr.Opcode.Not, e1); // FIXME should be broken further + foreach (var e in BreakQuantifier(e1, quantifier)) { yield return e; } + } + } else { + yield return expr; + } + } + + internal static IEnumerable BreakImplication(Expression ante, Expression post, Quantifier quantifier, IToken tok) { // FIXME: should work for exists and && + foreach (var small_post in BreakQuantifier(post, quantifier)) { + var bin_post = small_post as BinaryExpr; + if (bin_post == null || bin_post.Op != BinaryExpr.Opcode.Imp) { + yield return new BinaryExpr(tok, BinaryExpr.Opcode.Imp, ante, small_post); + } else { // bin_post is an implication + var large_ante = new BinaryExpr(ante.tok, BinaryExpr.Opcode.And, ante, bin_post.E0); + foreach (var imp in BreakImplication(large_ante, bin_post.E1, quantifier, tok)) { + yield return imp; + } + } + } + } + + protected override void VisitOneExpr(Expression expr) { //FIXME: This doesn't save the rewritten quantifier + var forall = expr as ForallExpr; + var exists = expr as ExistsExpr; + + if (forall != null && TriggerUtils.NeedsAutoTriggers(forall)) { + var rew = BreakQuantifier(forall.LogicalBody(), Quantifier.Forall); + //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| ")); + } else if (exists != null && TriggerUtils.NeedsAutoTriggers(exists)) { + var rew = BreakQuantifier(exists.LogicalBody(), Quantifier.Exists); + //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| ")); + } + } + } +} -- cgit v1.2.3 From 22a997192baf246bd86031f319aac154c2ec05cb Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 14 Aug 2015 10:05:37 -0700 Subject: Implement self-loop detection Implementing loop detection between multiple triggers is much harder, as it seems to require walking an exponentially sized graph. Self-loop detection is still a net gain compared to the current situation: we used to not detect loops in large quantifiers; not we break these apart, suppress the loops where we can in the smaller parts, and report the ones that we can't suppress. It could be that the broken-up quantifiers are mutually recursive, but these cases would have already led to a loop in the past. --- Source/Dafny/Translator.cs | 4 +- Source/Dafny/Triggers/QuantifierSplitter.cs | 97 +++++++++------ Source/Dafny/Triggers/QuantifiersCollection.cs | 165 +++++++++++++++++++------ Source/Dafny/Triggers/TriggerExtensions.cs | 37 +++--- Source/Dafny/Triggers/TriggerUtils.cs | 23 +++- Source/Dafny/Triggers/TriggersCollector.cs | 102 ++++++++------- 6 files changed, 275 insertions(+), 153 deletions(-) (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index b5d89abd..14fca463 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -13107,8 +13107,10 @@ namespace Microsoft.Dafny { return f.Formals.Zip(fexp.Args).All(formal_concrete => CanSafelySubstitute(visitor.TriggerVariables, formal_concrete.Item1, formal_concrete.Item2)); } + Triggers.TriggersCollector triggersCollector = new Triggers.TriggersCollector(); + private bool CanSafelySubstitute(ISet protectedVariables, IVariable variable, Expression substitution) { - return !(protectedVariables.Contains(variable) && Dafny.Triggers.TriggersCollector.IsTriggerKiller(substitution)); + return !(protectedVariables.Contains(variable) && triggersCollector.IsTriggerKiller(substitution)); } private class VariablesCollector: BottomUpVisitor { diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index e83feebb..33be0da2 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -6,59 +6,76 @@ using System.Text; namespace Microsoft.Dafny.Triggers { class QuantifierSplitter : BottomUpVisitor { - internal enum Quantifier { Forall, Exists } + private static BinaryExpr.Opcode FlipOpcode(BinaryExpr.Opcode opCode) { + if (opCode == BinaryExpr.Opcode.And) { + return BinaryExpr.Opcode.Or; + } else if (opCode == BinaryExpr.Opcode.Or) { + return BinaryExpr.Opcode.And; + } else { + throw new ArgumentException(); + } + } + + // NOTE: If we wanted to split quantifiers as far as possible, it would be + // enough to put the formulas in DNF (for foralls) or CNF (for exists). + // Unfortunately, this would cause ill-behaved quantifiers to produce + // exponentially many smaller quantifiers. - internal static IEnumerable BreakQuantifier(Expression expr, Quantifier quantifier) { + internal static IEnumerable SplitExpr(Expression expr, BinaryExpr.Opcode separator) { expr = expr.Resolved; + var unary = expr as UnaryOpExpr; var binary = expr as BinaryExpr; - if (binary == null) { - yield return expr; - yield break; + if (unary != null && unary.Op == UnaryOpExpr.Opcode.Not) { + foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, e); } + } else if (binary != null && binary.Op == separator) { + foreach (var e in SplitExpr(binary.E0, separator)) { yield return e; } + foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; } + } else if (binary != null && binary.Op == BinaryExpr.Opcode.Imp && separator == BinaryExpr.Opcode.Or) { + foreach (var e in SplitExpr(new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, binary.E0), separator)) { yield return e; } + foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; } } + } - var e0 = binary.E0; - var e1 = binary.E1; - - if ((quantifier == Quantifier.Forall && binary.Op == BinaryExpr.Opcode.And) || - (quantifier == Quantifier.Exists && binary.Op == BinaryExpr.Opcode.Or)) { - foreach (var e in BreakQuantifier(e0, quantifier)) { yield return e; } - foreach (var e in BreakQuantifier(e1, quantifier)) { yield return e; } - } else if (binary.Op == BinaryExpr.Opcode.Imp) { - if (quantifier == Quantifier.Forall) { - foreach (var e in BreakImplication(e0, e1, quantifier, expr.tok)) { yield return e; } - } else { - yield return new UnaryOpExpr(e1.tok, UnaryOpExpr.Opcode.Not, e1); // FIXME should be broken further - foreach (var e in BreakQuantifier(e1, quantifier)) { yield return e; } - } - } else { - yield return expr; + internal static IEnumerable SplitAndStich(BinaryExpr pair, BinaryExpr.Opcode separator) { + foreach (var e1 in SplitExpr(pair.E1, separator)) { + yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1); } } - internal static IEnumerable BreakImplication(Expression ante, Expression post, Quantifier quantifier, IToken tok) { // FIXME: should work for exists and && - foreach (var small_post in BreakQuantifier(post, quantifier)) { - var bin_post = small_post as BinaryExpr; - if (bin_post == null || bin_post.Op != BinaryExpr.Opcode.Imp) { - yield return new BinaryExpr(tok, BinaryExpr.Opcode.Imp, ante, small_post); - } else { // bin_post is an implication - var large_ante = new BinaryExpr(ante.tok, BinaryExpr.Opcode.And, ante, bin_post.E0); - foreach (var imp in BreakImplication(large_ante, bin_post.E1, quantifier, tok)) { - yield return imp; - } + internal static IEnumerable SplitQuantifier(QuantifierExpr quantifier) { + var body = quantifier.LogicalBody(); + var binary = body as BinaryExpr; + + if (quantifier is ForallExpr) { + IEnumerable stream; + if (binary != null && (binary.Op == BinaryExpr.Opcode.Imp || binary.Op == BinaryExpr.Opcode.Or)) { + stream = SplitAndStich(binary, BinaryExpr.Opcode.And); + } else { + stream = SplitExpr(body, BinaryExpr.Opcode.And); + } + foreach (var e in stream) { + yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes); + } + } else if (quantifier is ExistsExpr) { + IEnumerable stream; + if (binary != null && binary.Op == BinaryExpr.Opcode.And) { + stream = SplitAndStich(binary, BinaryExpr.Opcode.Or); + } else { + stream = SplitExpr(body, BinaryExpr.Opcode.Or); } + foreach (var e in stream) { + yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes); + } + } else { + yield return quantifier; } } - + protected override void VisitOneExpr(Expression expr) { //FIXME: This doesn't save the rewritten quantifier - var forall = expr as ForallExpr; - var exists = expr as ExistsExpr; - - if (forall != null && TriggerUtils.NeedsAutoTriggers(forall)) { - var rew = BreakQuantifier(forall.LogicalBody(), Quantifier.Forall); - //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| ")); - } else if (exists != null && TriggerUtils.NeedsAutoTriggers(exists)) { - var rew = BreakQuantifier(exists.LogicalBody(), Quantifier.Exists); + var quantifier = expr as QuantifierExpr; + if (quantifier != null) { + var rew = SplitQuantifier(quantifier); //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| ")); } } diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 3cbe3bd9..828e0e18 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -1,7 +1,11 @@ -using System; +#define QUANTIFIER_WARNINGS + +using System; using System.Collections.Generic; using System.Linq; using System.Text; +using Microsoft.Boogie; +using System.Diagnostics.Contracts; //FIXME Generated triggers should be _triggers //FIXME: When scoring, do not consider old(x) to be higher than x. @@ -9,18 +13,23 @@ using System.Text; namespace Microsoft.Dafny.Triggers { class QuantifierWithTriggers { internal QuantifierExpr quantifier; - internal List triggers; + internal List CandidateTerms; + internal List Candidates; + internal List RejectedCandidates; + + internal bool AllowsLoops { get { return quantifier.Attributes.AsEnumerable().Any(a => a.Name == "loop"); } } + internal bool CouldSuppressLoops { get; set; } internal QuantifierWithTriggers(QuantifierExpr quantifier) { this.quantifier = quantifier; - this.triggers = null; + this.RejectedCandidates = new List(); } internal void TrimInvalidTriggers() { - triggers = triggers.Where(tr => tr.MentionsAll(quantifier.BoundVars)).ToList(); + Contract.Requires(CandidateTerms != null); + Contract.Requires(Candidates != null); + Candidates = TriggerUtils.Filter(Candidates, tr => tr.MentionsAll(quantifier.BoundVars), tr => { }).ToList(); } - - public bool QuantifierAlreadyHadTriggers { get { return !TriggerUtils.NeedsAutoTriggers(quantifier); } } } class QuantifiersCollection { @@ -32,26 +41,32 @@ namespace Microsoft.Dafny.Triggers { this.quantifiers = quantifiers.Select(q => new QuantifierWithTriggers(q)).ToList(); } - void ComputeTriggers() { - CollectAndShareTriggers(); + internal void ComputeTriggers(TriggersCollector triggersCollector) { + CollectAndShareTriggers(triggersCollector); TrimInvalidTriggers(); BuildDependenciesGraph(); SuppressMatchingLoops(); SelectTriggers(); } + + private bool SubsetGenerationPredicate(List terms, TriggerTerm additionalTerm) { + // Simple formulas like [P0(i) && P1(i) && P2(i) && P3(i) && P4(i)] yield very + // large numbers of multi-triggers, most of which are useless. This filter + // restricts subsets of terms so that we only generate sets of terms where each + // element contributes at least one variable. In the example above, we'll only + // get 5 triggers. + return additionalTerm.Variables.Where(v => !terms.Any(t => t.Variables.Contains(v))).Any(); + } - void CollectAndShareTriggers() { - var pool = quantifiers.SelectMany(q => TriggersCollector.CollectTriggers(q.quantifier)); - var distinctPool = pool.Deduplicate((x, y) => ExprExtensions.ExpressionEq(x.Expr, y.Expr)); - var multiPool = TriggerUtils.AllNonEmptySubsets(distinctPool).Select(candidates => new MultiTriggerCandidate(candidates)).ToList(); + //FIXME document that this assumes that the quantifiers live in the same context and share the same variables + void CollectAndShareTriggers(TriggersCollector triggersCollector) { + var pool = quantifiers.SelectMany(q => triggersCollector.CollectTriggers(q.quantifier)); + var distinctPool = pool.Deduplicate(TriggerTerm.Eq); + var multiPool = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate).Select(candidates => new TriggerCandidate(candidates)).ToList(); foreach (var q in quantifiers) { - if (q.QuantifierAlreadyHadTriggers) { - reporter.Info(MessageSource.Resolver, q.quantifier.tok, "Not generating triggers for this quantifier."); //FIXME: no_trigger is passed down to Boogie - return; - } else { - q.triggers = multiPool; - } + q.CandidateTerms = distinctPool; + q.Candidates = multiPool; } } @@ -62,43 +77,111 @@ namespace Microsoft.Dafny.Triggers { } void BuildDependenciesGraph() { - //FIXME + // FIXME: Think more about multi-quantifier dependencies + //class QuantifierDependency { + // QuantifierWithTriggers Cause; + // QuantifierWithTriggers Consequence; + // List Triggers; + // List MatchingTerm; + //} } void SuppressMatchingLoops() { - //FIXME + // NOTE: This only looks for self-loops; that is, loops involving a single + // quantifier. + + // For a given quantifier q, we introduce a triggering relation between trigger + // candidates by writing t1 → t2 if instantiating q from t1 introduces a ground + // term that matches t2. Then, we notice that this relation is transitive, since + // all triggers yield the same set of terms. This means that any matching loop + // t1 → ... → t1 can be reduced to a self-loop t1 → t1. Detecting such + // self-loops is then only a matter of finding terms in the body of the + // quantifier that match a given trigger. + + // Of course, each trigger that actually appears in the body of the quantifier + // yields a trivial self-loop (e.g. P(i) in [∀ i {P(i)} ⋅ P(i)]), so we + // ignore this type of loops. In fact, we ignore any term in the body of the + // quantifier that matches one of the terms of the trigger (this ensures that + // [∀ x {f(x), f(f(x))} ⋅ f(x) = f(f(x))] is not a loop). And we even + // ignore terms that almost match a trigger term, modulo a single variable + // (this ensures that [∀ x y {a(x, y)} ⋅ a(x, y) == a(y, x)] is not a loop). + // This ignoring logic is implemented by the CouldCauseLoops method. + + foreach (var q in quantifiers) { + var looping = new List(); + var loopingSubterms = q.Candidates.ToDictionary(candidate => candidate, candidate => candidate.LoopingSubterms(q.quantifier).ToList()); + + var safe = TriggerUtils.Filter( + q.Candidates, + c => !loopingSubterms[c].Any(), + c => { + looping.Add(c); + c.Annotation = "loop with " + loopingSubterms[c].MapConcat(t => Printer.ExprToString(t.Expr), ", "); + }).ToList(); + + q.CouldSuppressLoops = safe.Count > 0; + + if (!q.AllowsLoops && q.CouldSuppressLoops) { + q.Candidates = safe; + q.RejectedCandidates.AddRange(looping); + } + } } void SelectTriggers() { //FIXME } - private void CommitOne(QuantifierWithTriggers q) { - foreach (var multiCandidate in q.triggers) { //TODO: error message for when no triggers found - q.quantifier.Attributes = new Attributes("trigger", multiCandidate.terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); - } - - - //TriggerUtils.DebugTriggers(" Final results:\n{0}", PickMultiTriggers(quantifier)); + private void CommitOne(QuantifierWithTriggers q, object conjunctId) { + var errorLevel = ErrorLevel.Info; + var msg = new StringBuilder(); + var indent = conjunctId != null ? " " : " "; + var header = conjunctId != null ? String.Format(" For conjunct {0}:{1}", conjunctId, Environment.NewLine) : ""; + + if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: no_trigger is passed down to Boogie + msg.Append(indent).AppendLine("Not generating triggers for this quantifier."); + } else { + foreach (var candidate in q.Candidates) { + q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); + } - //var multi_candidates = PickMultiTriggers(quantifier); + if (q.Candidates.Any()) { + msg.Append(indent).AppendLine("Selected triggers:"); + foreach (var mc in q.Candidates) { + msg.Append(indent).Append(" ").AppendLine(mc.ToString()); + } + } - //if (multi_candidates.RejectedMultiCandidates.Any()) { - // var tooltip = TriggerUtils.JoinStringsWithHeader("Rejected: ", multi_candidates.RejectedMultiCandidates.Where(candidate => candidate.Tags != null) - // .Select(candidate => candidate.AsDafnyAttributeString(true, true))); - // reporter.Info(ErrorSource.Resolver, quantifier.tok, tooltip, quantifier.tok.val.Length); - //} + if (q.RejectedCandidates.Any()) { + msg.Append(indent).AppendLine("Rejected triggers:"); + foreach (var mc in q.RejectedCandidates) { + msg.Append(indent).Append(" ").AppendLine(mc.ToString()); + } + } - //if (multi_candidates.FinalMultiCandidates.Any()) { - // var tooltip = JoinStringsWithHeader("Triggers: ", multi_candidates.FinalMultiCandidates.Select(multi_candidate => multi_candidate.AsDafnyAttributeString())); - // reporter.Info(ErrorSource.Resolver, quantifier.tok, tooltip, quantifier.tok.val.Length); - //} +#if QUANTIFIER_WARNINGS + if (!q.CandidateTerms.Any()) { + errorLevel = ErrorLevel.Warning; + msg.Append(indent).AppendLine("No terms found to trigger on."); + } else if (!q.Candidates.Any()) { + errorLevel = ErrorLevel.Warning; + msg.Append(indent).AppendLine("No trigger covering all quantified variables found."); + } else if (!q.CouldSuppressLoops) { + errorLevel = ErrorLevel.Warning; + msg.Append(indent).AppendLine("Suppressing loops would leave this quantifier without triggers."); + } +#endif + } - //string warning = multi_candidates.Warning(); - //if (warning != null) { - // // FIXME reenable Resolver.Warning(quantifier.tok, warning); - //} + if (msg.Length > 0) { + reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, header + msg.ToString()); + } } + internal void CommitTriggers() { + foreach (var q in quantifiers) { + CommitOne(q, quantifiers.Count > 1 ? q.quantifier : null); + } + } } } diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index 7bebe1ac..da43abcc 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -22,6 +22,20 @@ namespace Microsoft.Dafny.Triggers { } } + internal struct TriggerMatch { + internal Expression Expr; + internal Dictionary Bindings; + + internal static bool Eq(TriggerMatch t1, TriggerMatch t2) { + return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr); + } + + internal bool CouldCauseLoops(List terms) { + var expr = Expr; + return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNames(expr)); + } + } + internal static class ExprExtensions { internal static IEnumerable AllSubExpressions(this Expression expr, bool strict = false) { foreach (var subexpr in expr.SubExpressions) { @@ -75,7 +89,7 @@ namespace Microsoft.Dafny.Triggers { return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNames(e1, e2)); } - private static bool MatchesTrigger(this Expression expr, Expression trigger, ISet holes, Dictionary bindings) { + internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet holes, Dictionary bindings) { expr = expr.Resolved; trigger = trigger.Resolved; @@ -96,27 +110,6 @@ namespace Microsoft.Dafny.Triggers { return ShallowEq_Top(expr, trigger) && TriggerUtils.SameLists(expr.SubExpressions, trigger.SubExpressions, (e1, e2) => MatchesTrigger(e1, e2, holes, bindings)); } - internal struct TriggerMatch { - internal Expression Expr; - internal Dictionary Bindings; - - internal bool CouldCauseLoops(IEnumerable candidates) { - // A match for a trigger in the body of a quantifier can be a problem if - // it yields to a matching loop: for example, f(x) is a bad trigger in - // forall x, y :: f(x) = f(f(x)) - // In general, any such match can lead to a loop, but two special cases - // will only lead to a finite number of instantiations: - // 1. The match equals one of the triggers in the set of triggers under - // consideration. For example, { f(x) } a bad trigger above, but the - // pair { f(x), f(f(x)) } is fine (instantiating won't yield new - // matches) - // 2. The match only differs from one of these triggers by variable - // names. This is a superset of the previous case. - var expr = Expr; - return !candidates.Any(c => c.Expr.ExpressionEqModuloVariableNames(expr)); - } - } - private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, ISet holes) { var bindings = new Dictionary(); return expr.MatchesTrigger(trigger, holes, bindings) ? new TriggerMatch { Expr = expr, Bindings = bindings } : (TriggerMatch?)null; diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index 5a118a2f..dedbcbb1 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -15,21 +15,23 @@ namespace Microsoft.Dafny.Triggers { return copy; } - internal static IEnumerable> AllSubsets(IList source, int offset) { + internal static IEnumerable> AllSubsets(IList source, Func, T, bool> predicate, int offset) { if (offset >= source.Count) { yield return new List(); yield break; } - foreach (var subset in AllSubsets(source, offset + 1)) { - yield return CopyAndAdd(subset, source[offset]); + foreach (var subset in AllSubsets(source, predicate, offset + 1)) { + if (predicate(subset, source[offset])) { + yield return CopyAndAdd(subset, source[offset]); + } yield return new List(subset); } } - internal static IEnumerable> AllNonEmptySubsets(IEnumerable source) { + internal static IEnumerable> AllNonEmptySubsets(IEnumerable source, Func, T, bool> predicate) { List all = new List(source); - foreach (var subset in AllSubsets(all, 0)) { + foreach (var subset in AllSubsets(all, predicate, 0)) { if (subset.Count > 0) { yield return subset; } @@ -74,6 +76,17 @@ namespace Microsoft.Dafny.Triggers { return it1_has == it2_has && acc; } + internal static IEnumerable Filter(IEnumerable elements, Func predicate, Action reject) { + var positive = new List(); + foreach (var c in elements) { + if (predicate(c)) { + yield return c; + } else { + reject(c); + } + } + } + internal static bool SameNullity(T x1, T x2) where T : class { return (x1 == null) == (x2 == null); } diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 912a661c..e1f8a013 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -7,52 +7,68 @@ using System.Diagnostics.Contracts; using System.Diagnostics; namespace Microsoft.Dafny.Triggers { - struct TriggerCandidate { + class TriggerTerm { internal Expression Expr { get; set; } internal ISet Variables { get; set; } public override string ToString() { return Printer.ExprToString(Expr); } + + internal static bool Eq(TriggerTerm t1, TriggerTerm t2) { + return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr); + } } - class MultiTriggerCandidate { - internal List terms { get; set; } + class TriggerCandidate { + internal List Terms { get; set; } + internal string Annotation { get; set; } + + internal TriggerCandidate(List terms) { + this.Terms = terms; + } - internal MultiTriggerCandidate(List candidates) { - this.terms = candidates; + public TriggerCandidate(TriggerCandidate mc, string annotation) { + this.Terms = mc.Terms; + this.Annotation = annotation; } internal bool MentionsAll(List vars) { - return vars.All(x => terms.Any(candidate => candidate.Variables.Contains(x))); + return vars.All(x => Terms.Any(term => term.Variables.Contains(x))); } + private string Repr { get { return Terms.MapConcat(t => Printer.ExprToString(t.Expr), ", "); } } + public override string ToString() { - return String.Join(", ", terms); + return "{" + Repr + "}" + (String.IsNullOrWhiteSpace(Annotation) ? "" : " (" + Annotation + ")"); } - public String AsDafnyAttributeString(bool wrap = true, bool includeTags = false) { - var repr = terms.MapConcat(t => Printer.ExprToString(t.Expr), ", "); - if (wrap) { - repr = "{:trigger " + repr + "}"; - } - return repr; + internal IEnumerable LoopingSubterms(QuantifierExpr quantifier) { + var matchingSubterms = MatchingSubterms(quantifier); + return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms)); + } + + internal List MatchingSubterms(QuantifierExpr quantifier) { + //FIXME this will miss rewritten expressions (CleanupExpr). Should introduce an OriginalExpr to compare against. + return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq); + } + + public String AsDafnyAttributeString() { + return "{:trigger " + Repr + "}"; } } class TriggerAnnotation { internal bool IsTriggerKiller; internal ISet Variables; - internal readonly List PrivateTerms; - internal readonly List ExportedTerms; + internal readonly List PrivateTerms; + internal readonly List ExportedTerms; - internal TriggerAnnotation(bool IsTriggerKiller, IEnumerable Variables, - IEnumerable AllCandidates, IEnumerable PrivateCandidates = null) { + internal TriggerAnnotation(bool IsTriggerKiller, IEnumerable Variables, IEnumerable AllTerms, IEnumerable PrivateTerms = null) { this.IsTriggerKiller = IsTriggerKiller; this.Variables = new HashSet(Variables); - - this.PrivateTerms = new List(PrivateCandidates == null ? Enumerable.Empty() : PrivateCandidates); - this.ExportedTerms = new List(AllCandidates == null ? Enumerable.Empty() : AllCandidates.Except(this.PrivateTerms)); + this.PrivateTerms = new List(PrivateTerms == null ? Enumerable.Empty() : PrivateTerms); + this.ExportedTerms = new List(AllTerms == null ? Enumerable.Empty() : AllTerms.Except(this.PrivateTerms)); } public override string ToString() { @@ -66,15 +82,15 @@ namespace Microsoft.Dafny.Triggers { sb.AppendFormat(subindent, bv.Name); } - sb.AppendFormat(nindent, "Exported candidates:"); - foreach (var candidate in ExportedTerms) { - sb.AppendFormat(subindent, candidate); + sb.AppendFormat(nindent, "Exported terms:"); + foreach (var term in ExportedTerms) { + sb.AppendFormat(subindent, term); } if (PrivateTerms.Any()) { - sb.AppendFormat(nindent, "Private candidates:"); - foreach (var candidate in PrivateTerms) { - sb.AppendFormat(subindent, candidate); + sb.AppendFormat(nindent, "Private terms:"); + foreach (var term in PrivateTerms) { + sb.AppendFormat(subindent, term); } } @@ -85,9 +101,7 @@ namespace Microsoft.Dafny.Triggers { public class TriggersCollector { Dictionary cache; - private static TriggersCollector instance = new TriggersCollector(); - - private TriggersCollector() { + internal TriggersCollector() { this.cache = new Dictionary(); } @@ -96,8 +110,8 @@ namespace Microsoft.Dafny.Triggers { .Aggregate(seed, (acc, e) => reduce(acc, e)); } - private List CollectExportedCandidates(Expression expr) { - return ReduceAnnotatedSubExpressions>(expr, new List(), a => a.ExportedTerms, TriggerUtils.MergeAlterFirst); + private List CollectExportedCandidates(Expression expr) { + return ReduceAnnotatedSubExpressions>(expr, new List(), a => a.ExportedTerms, TriggerUtils.MergeAlterFirst); } private ISet CollectVariables(Expression expr) { @@ -108,8 +122,8 @@ namespace Microsoft.Dafny.Triggers { return ReduceAnnotatedSubExpressions(expr, false, a => a.IsTriggerKiller, (a, b) => a || b); } - private IEnumerable OnlyPrivateCandidates(List candidates, IEnumerable privateVars) { - return candidates.Where(c => privateVars.Intersect(c.Variables).Any()); //TODO Check perf + private IEnumerable OnlyPrivateCandidates(List terms, IEnumerable privateVars) { + return terms.Where(c => privateVars.Intersect(c.Variables).Any()); //TODO Check perf } private TriggerAnnotation Annotate(Expression expr) { @@ -195,18 +209,18 @@ namespace Microsoft.Dafny.Triggers { private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) { bool expr_is_killer = false; var new_expr = CleanupExpr(expr, out expr_is_killer); - var new_candidate = new TriggerCandidate { Expr = new_expr, Variables = CollectVariables(expr) }; + var new_term = new TriggerTerm { Expr = new_expr, Variables = CollectVariables(expr) }; - List collected_candidates = CollectExportedCandidates(expr); + List collected_terms = CollectExportedCandidates(expr); var children_contain_killers = CollectIsKiller(expr); if (!children_contain_killers) { // Add only if the children are not killers; the head has been cleaned up into non-killer form - collected_candidates.Add(new_candidate); + collected_terms.Add(new_term); } // This new node is a killer if its children were killers, or if it's non-cleaned-up head is a killer - return new TriggerAnnotation(children_contain_killers || expr_is_killer, new_candidate.Variables, collected_candidates); + return new TriggerAnnotation(children_contain_killers || expr_is_killer, new_term.Variables, collected_terms); } private TriggerAnnotation AnnotateApplySuffix(ApplySuffix expr) { @@ -218,13 +232,13 @@ namespace Microsoft.Dafny.Triggers { // only possible child here; there can be DatatypeValue nodes, for example (see vstte2012/Combinators.dfy). var annotation = AnnotatePotentialCandidate(expr); // Comparing by reference is fine here. Using sets could yield a small speedup - annotation.ExportedTerms.RemoveAll(candidate => expr.SubExpressions.Contains(candidate.Expr)); + annotation.ExportedTerms.RemoveAll(term => expr.SubExpressions.Contains(term.Expr)); return annotation; } private TriggerAnnotation AnnotateQuantifierOrLetExpr(Expression expr, IEnumerable boundVars) { - var candidates = CollectExportedCandidates(expr); - return new TriggerAnnotation(true, CollectVariables(expr), candidates, OnlyPrivateCandidates(candidates, boundVars)); + var terms = CollectExportedCandidates(expr); + return new TriggerAnnotation(true, CollectVariables(expr), terms, OnlyPrivateCandidates(terms, boundVars)); } private TriggerAnnotation AnnotateQuantifier(QuantifierExpr expr) { @@ -244,13 +258,13 @@ namespace Microsoft.Dafny.Triggers { } // FIXME document that this will contain duplicates - internal static List CollectTriggers(QuantifierExpr quantifier) { + internal List CollectTriggers(QuantifierExpr quantifier) { // TODO could check for existing triggers and return that instead, but that require a bit of work to extract the expressions - return instance.Annotate(quantifier).PrivateTerms; + return Annotate(quantifier).PrivateTerms; } - internal static bool IsTriggerKiller(Expression expr) { - return instance.Annotate(expr).IsTriggerKiller; + internal bool IsTriggerKiller(Expression expr) { + return Annotate(expr).IsTriggerKiller; } } } -- cgit v1.2.3 From a07b43ac03b38d4af575d1a1df48339ad228751a Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 14 Aug 2015 17:38:08 -0700 Subject: Start committing split quantifiers This requires rewriting the parts of the AST that contain these quantifiers. We unfortunately don't have facilities to do such rewrites at the moment (and there are loops in the AST, so it would be hard to write such a facility). As a workaround, this commit introduces a field in quantifier expressions, SplitQuantifiers. Code that manipulate triggers is expected to look for this field, and ignore the other fields if that one is found. --- Source/Dafny/Cloner.cs | 10 ++- Source/Dafny/Compiler.cs | 6 ++ Source/Dafny/DafnyAst.cs | 54 +++++++++++- Source/Dafny/Printer.cs | 7 ++ Source/Dafny/Resolver.cs | 16 +++- Source/Dafny/Rewriter.cs | 4 +- Source/Dafny/Translator.cs | 125 +++++++++++++++++----------- Source/Dafny/Triggers/QuantifierSplitter.cs | 26 ++++-- Source/Dafny/Triggers/TriggerExtensions.cs | 8 ++ Source/Dafny/Triggers/TriggerGenerator.cs | 10 ++- Source/Dafny/Triggers/TriggerUtils.cs | 1 + Source/Dafny/Triggers/TriggersCollector.cs | 5 +- 12 files changed, 203 insertions(+), 69 deletions(-) (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 323abc70..961d4d14 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -4,6 +4,7 @@ using System.Collections.Generic; using System.Numerics; using System.Diagnostics.Contracts; using IToken = Microsoft.Boogie.IToken; +using System.Linq; namespace Microsoft.Dafny { @@ -373,13 +374,18 @@ namespace Microsoft.Dafny if (e is QuantifierExpr) { var q = (QuantifierExpr)e; var tvs = q.TypeArgs.ConvertAll(CloneTypeParam); + QuantifierExpr cloned; if (e is ForallExpr) { - return new ForallExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); + cloned = new ForallExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); } else if (e is ExistsExpr) { - return new ExistsExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); + cloned = new ExistsExpr(tk, tvs, bvs, range, term, CloneAttributes(e.Attributes)); } else { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected quantifier expression } + if (q.SplitQuantifier != null) { //TODO CLEMENT TRIGGERS: Should we clone the quantifier as a quantifier in this case? Or should we just replace entirely? + cloned.SplitQuantifier = q.SplitQuantifier.Select(CloneExpr).ToList(); + } + return cloned; } else if (e is MapComprehension) { return new MapComprehension(tk, ((MapComprehension)e).Finite, bvs, range, term, CloneAttributes(e.Attributes)); } else if (e is LambdaExpr) { diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 4fdd34f6..d19d2bed 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -2816,6 +2816,12 @@ namespace Microsoft.Dafny { } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; + + if (e.SplitQuantifier != null) { //TODO CLEMENT TRIGGERS: Do we compile a split quantifier in its original form, or in its split form? + TrExpr(e.SplitQuantifierExpression); + return; + } + Contract.Assert(e.Bounds != null); // for non-ghost quantifiers, the resolver would have insisted on finding bounds var n = e.BoundVars.Count; Contract.Assert(e.Bounds.Count == n); diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index efe94c66..05548f38 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -1555,7 +1555,7 @@ namespace Microsoft.Dafny { // BUGBUG: The following line is a workaround to tell the verifier that 'value' is not of an Immutable type. // A proper solution would be to be able to express that in the program (in a specification or attribute) or // to be able to declare 'parent' as [PeerOrImmutable]. - Contract.Requires(value is TopLevelDecl || value is Function || value is Method || value is DatatypeCtor || value is QuantifierExpr); + Contract.Requires(value is TopLevelDecl || value is Function || value is Method || value is DatatypeCtor || (value is QuantifierExpr && ((QuantifierExpr)value).SplitQuantifier == null)); //modifies parent; parent = value; } @@ -6552,6 +6552,15 @@ namespace Microsoft.Dafny { } } + /// + /// Returns a resolved binary expression + /// + public BinaryExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) + : this(tok, BinaryExpr.ResolvedOp2SyntacticOp(rop), e0, e1) { + ResolvedOp = rop; + Type = Type.Bool; + } + public override IEnumerable SubExpressions { get { yield return E0; @@ -6770,6 +6779,8 @@ namespace Microsoft.Dafny { public List TypeArgs; private static int currentQuantId = -1; + protected abstract BinaryExpr.ResolvedOpcode SplitResolvedOp { get; } + static int FreshQuantId() { return System.Threading.Interlocked.Increment(ref currentQuantId); } @@ -6800,10 +6811,47 @@ namespace Microsoft.Dafny { this.TypeArgs = tvars; this.UniqueId = FreshQuantId(); } + + private Expression SplitQuantifierToExpression() { + Contract.Requires(SplitQuantifier != null && SplitQuantifier.Any()); + Expression accumulator = SplitQuantifier[0]; + for (int tid = 1; tid < SplitQuantifier.Count; tid++) { + var newAcc = new BinaryExpr(Term.tok, SplitResolvedOp, accumulator, SplitQuantifier[tid]); + accumulator = newAcc; + } + return accumulator; + } + + private List _SplitQuantifier; + public List SplitQuantifier { + get { + return _SplitQuantifier; + } + set { + _SplitQuantifier = value; + SplitQuantifierExpression = SplitQuantifierToExpression(); + } + } + + internal Expression SplitQuantifierExpression { get; private set; } + public abstract Expression LogicalBody(); + + public override IEnumerable SubExpressions { + get { + if (SplitQuantifier == null) { + return base.SubExpressions; + } else { + return SplitQuantifier; + } + } + } } public class ForallExpr : QuantifierExpr { + protected override BinaryExpr.Opcode SplitOp { get { return BinaryExpr.Opcode.And; } } + protected override BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.And; } } + public ForallExpr(IToken tok, List bvars, Expression range, Expression term, Attributes attrs) : this(tok, new List(), bvars, range, term, attrs) { Contract.Requires(cce.NonNullElements(bvars)); @@ -6817,6 +6865,7 @@ namespace Microsoft.Dafny { Contract.Requires(term != null); } public override Expression LogicalBody() { + Contract.Assert(SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier if (Range == null) { return Term; } @@ -6828,6 +6877,9 @@ namespace Microsoft.Dafny { } public class ExistsExpr : QuantifierExpr { + protected override BinaryExpr.Opcode SplitOp { get { return BinaryExpr.Opcode.Or; } } + protected override BinaryExpr.ResolvedOpcode SplitResolvedOp { get { return BinaryExpr.ResolvedOpcode.Or; } } + public ExistsExpr(IToken tok, List bvars, Expression range, Expression term, Attributes attrs) : this(tok, new List(), bvars, range, term, attrs) { Contract.Requires(cce.NonNullElements(bvars)); diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 1c7508eb..43b69bbb 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -1729,6 +1729,13 @@ namespace Microsoft.Dafny { } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; + + if (e.SplitQuantifier != null) { + // CLEMENT TODO TRIGGERS: Should (do) we have a setting to print the original forms instead of rewritten forms? + PrintExpr(e.SplitQuantifierExpression, contextBindingStrength, fragileContext, isRightmost, isFollowedBySemicolon, indent, resolv_count); + return; + } + bool parensNeeded = !isRightmost; if (parensNeeded) { wr.Write("("); } wr.Write(e is ForallExpr ? "forall" : "exists"); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 7bf085f9..e1c3c63b 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -305,7 +305,7 @@ namespace Microsoft.Dafny Contract.Assert(!useCompileSignatures); useCompileSignatures = true; // set Resolver-global flag to indicate that Signatures should be followed to their CompiledSignature var oldErrorsOnly = reporter.ErrorsOnly; - reporter.ErrorsOnly = true; // turn off warning reporting for the clone + reporter.ErrorsOnly = true; // turn off warning reporter for the clone var nw = new Cloner().CloneModuleDefinition(m, m.CompileName + "_Compile"); var compileSig = RegisterTopLevelDecls(nw, true); compileSig.Refines = refinementTransformer.RefinedSig; @@ -338,7 +338,7 @@ namespace Microsoft.Dafny if (refinementTransformer.CheckIsRefinement(compileSig, p)) { abs.Signature.CompileSignature = compileSig; } else { - reporter.Error(MessageSource.Resolver, + reporter.Error(MessageSource.Resolver, abs.CompilePath[0], "module " + Util.Comma(".", abs.CompilePath, x => x.val) + " must be a refinement of " + Util.Comma(".", abs.Path, x => x.val)); @@ -2438,6 +2438,7 @@ namespace Microsoft.Dafny return false; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; + Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution var cpos = IsCoContext ? cp : Invert(cp); if ((cpos == CallingPosition.Positive && e is ExistsExpr) || (cpos == CallingPosition.Negative && e is ForallExpr)) { if (e.MissingBounds != null && e.MissingBounds.Count != 0) { @@ -6962,7 +6963,7 @@ namespace Microsoft.Dafny reporter.Error(MessageSource.Resolver, expr, "'this' is not allowed in a 'static' context"); } if (currentClass != null) { - expr.Type = GetThisType(expr.tok, currentClass); // do this regardless of scope.AllowInstance, for better error reporting + expr.Type = GetThisType(expr.tok, currentClass); // do this regardless of scope.AllowInstance, for better error reporter } } else if (expr is IdentifierExpr) { @@ -7605,6 +7606,7 @@ namespace Microsoft.Dafny e.Type = e.Body.Type; } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; + Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution int prevErrorCount = reporter.Count(ErrorLevel.Error); bool _val = true; bool typeQuantifier = Attributes.ContainsBool(e.Attributes, "typeQuantifier", ref _val) && _val; @@ -9177,6 +9179,7 @@ namespace Microsoft.Dafny return; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; + Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution if (e.MissingBounds != null) { foreach (var bv in e.MissingBounds) { reporter.Error(MessageSource.Resolver, expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name); @@ -9774,10 +9777,13 @@ namespace Microsoft.Dafny if (expr is IdentifierExpr) { var e = (IdentifierExpr)expr; + return new HashSet() { e.Var }; } else if (expr is QuantifierExpr) { var e = (QuantifierExpr)expr; + Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution + var s = FreeVariables(e.LogicalBody()); foreach (var bv in e.BoundVars) { s.Remove(bv); @@ -10139,7 +10145,9 @@ namespace Microsoft.Dafny } else if (expr is NamedExpr) { return moduleInfo.IsGhost ? false : UsesSpecFeatures(((NamedExpr)expr).Body); } else if (expr is ComprehensionExpr) { - if (expr is QuantifierExpr && ((QuantifierExpr)expr).Bounds == null) { + var q = expr as QuantifierExpr; + Contract.Assert(q == null || q.SplitQuantifier == null); // No split quantifiers during resolution + if (q != null && q.Bounds == null) { return true; // the quantifier cannot be compiled if the resolver found no bounds } return Contract.Exists(expr.SubExpressions, se => UsesSpecFeatures(se)); diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 0798510a..2c00e203 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -43,9 +43,9 @@ namespace Microsoft.Dafny Contract.Requires(reporter != null); } - internal override void PostResolve(ModuleDefinition m) { + internal override void PostCyclicityResolve(ModuleDefinition m) { var finder = new Triggers.QuantifierCollectionsFinder(reporter); - + foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { if (decl is Function) { var function = (Function)decl; diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 14fca463..f0b7f276 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4465,6 +4465,11 @@ namespace Microsoft.Dafny { var e = (ComprehensionExpr)expr; var canCall = CanCallAssumption(e.Term, etran); var q = e as QuantifierExpr; + + if (q != null && q.SplitQuantifier != null) { + return CanCallAssumption(q.SplitQuantifierExpression, etran); + } + var tyvars = MkTyParamBinders(q != null ? q.TypeArgs : new List()); if (e.Range != null) { canCall = BplAnd(CanCallAssumption(e.Range, etran), BplImp(etran.TrExpr(e.Range), canCall)); @@ -4758,6 +4763,12 @@ namespace Microsoft.Dafny { // If the quantifier is universal, then continue as: // assume (\forall x :: body(x)); // Create local variables corresponding to the type arguments: + + if (e.SplitQuantifier != null) { + CheckWellformedAndAssume(e.SplitQuantifierExpression, options, locals, builder, etran); + return; + } + var typeArgumentCopies = Map(e.TypeArgs, tp => e.Refresh(tp, CurrentIdGenerator)); var typeMap = Util.Dict(e.TypeArgs, Map(typeArgumentCopies, tp => (Type)new UserDefinedType(tp))); var newLocals = Map(typeArgumentCopies, tp => new Bpl.LocalVariable(tp.tok, new TypedIdent(tp.tok, nameTypeParam(tp), predef.Ty))); @@ -5293,6 +5304,10 @@ namespace Microsoft.Dafny { var q = e as QuantifierExpr; var lam = e as LambdaExpr; + if (q != null && q.SplitQuantifier != null) { + CheckWellformedWithResult(q.SplitQuantifierExpression, options, result, resultType, locals, builder, etran); + } + var typeMap = new Dictionary(); var copies = new List(); if (q != null) { @@ -11534,56 +11549,60 @@ namespace Microsoft.Dafny { return TrExpr(((NamedExpr)expr).Body); } else if (expr is QuantifierExpr) { QuantifierExpr e = (QuantifierExpr)expr; - List tyvars = translator.MkTyParamBinders(e.TypeArgs); - List bvars = new List(); - - var initEtran = this; - var bodyEtran = this; - bool _scratch = true; - Bpl.Expr antecedent = Bpl.Expr.True; - - if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) { - // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body - var ly = BplBoundVar(e.Refresh("q$ly#", translator.CurrentIdGenerator), predef.LayerType, bvars); - bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(translator, 1, ly), new FuelSetting(translator, 1, ly), modifiesFrame, stripLits); - } - if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) { - var h = BplBoundVar(e.Refresh("q$heap#", translator.CurrentIdGenerator), predef.HeapType, bvars); - bodyEtran = new ExpressionTranslator(bodyEtran, h); - antecedent = BplAnd(new List { - antecedent, - translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h), - translator.HeapSameOrSucc(initEtran.HeapExpr, h) - }); - } + if (e.SplitQuantifier != null) { + return TrExpr(e.SplitQuantifierExpression); + } else { + List tyvars = translator.MkTyParamBinders(e.TypeArgs); + List bvars = new List(); + + var initEtran = this; + var bodyEtran = this; + bool _scratch = true; + + Bpl.Expr antecedent = Bpl.Expr.True; + + if (Attributes.ContainsBool(e.Attributes, "layerQuantifier", ref _scratch)) { + // If this is a layer quantifier, quantify over layers here, and use $LS(ly) layers in the translation of the body + var ly = BplBoundVar(e.Refresh("q$ly#", translator.CurrentIdGenerator), predef.LayerType, bvars); + bodyEtran = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, new FuelSetting(translator, 1, ly), new FuelSetting(translator, 1, ly), modifiesFrame, stripLits); + } + if (Attributes.ContainsBool(e.Attributes, "heapQuantifier", ref _scratch)) { + var h = BplBoundVar(e.Refresh("q$heap#", translator.CurrentIdGenerator), predef.HeapType, bvars); + bodyEtran = new ExpressionTranslator(bodyEtran, h); + antecedent = BplAnd(new List { + antecedent, + translator.FunctionCall(e.tok, BuiltinFunction.IsGoodHeap, null, h), + translator.HeapSameOrSucc(initEtran.HeapExpr, h) + }); + } - antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars)); + antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars)); - Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); - Bpl.Trigger tr = null; - var argsEtran = bodyEtran.WithNoLits(); - foreach (var aa in e.Attributes.AsEnumerable()) { - if (aa.Name == "trigger") { - List tt = new List(); - foreach (var arg in aa.Args) { - tt.Add(argsEtran.TrExpr(arg)); + Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); + Bpl.Trigger tr = null; + var argsEtran = bodyEtran.WithNoLits(); + foreach (var aa in e.Attributes.AsEnumerable()) { + if (aa.Name == "trigger") { + List tt = new List(); + foreach (var arg in aa.Args) { + tt.Add(argsEtran.TrExpr(arg)); + } + tr = new Bpl.Trigger(expr.tok, true, tt, tr); } - tr = new Bpl.Trigger(expr.tok, true, tt, tr); } - } - if (e.Range != null) { - antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range)); - } - Bpl.Expr body = bodyEtran.TrExpr(e.Term); + if (e.Range != null) { + antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range)); + } + Bpl.Expr body = bodyEtran.TrExpr(e.Term); - if (e is ForallExpr) { - return new Bpl.ForallExpr(expr.tok, new List(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body)); - } else { - Contract.Assert(e is ExistsExpr); - return new Bpl.ExistsExpr(expr.tok, new List(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.And(antecedent, body)); + if (e is ForallExpr) { + return new Bpl.ForallExpr(expr.tok, new List(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.Imp(antecedent, body)); + } else { + Contract.Assert(e is ExistsExpr); + return new Bpl.ExistsExpr(expr.tok, new List(), Concat(tyvars, bvars), kv, tr, Bpl.Expr.And(antecedent, body)); + } } - } else if (expr is SetComprehension) { var e = (SetComprehension)expr; // Translate "set xs | R :: T" into "lambda y: BoxType :: (exists xs :: CorrectType(xs) && R && y==Box(T))". @@ -12966,9 +12985,11 @@ namespace Microsoft.Dafny { } } + } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier != null) { + return TrSplitExpr(((QuantifierExpr)expr).SplitQuantifierExpression, splits, position, heightLimit, apply_induction, etran); } else if (((position && expr is ForallExpr) || (!position && expr is ExistsExpr)) - /* NB: only for type arg less quantifiers for now: */ - && ((QuantifierExpr)expr).TypeArgs.Count == 0) { + /* 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) { @@ -13138,8 +13159,11 @@ namespace Microsoft.Dafny { protected override void VisitOneExpr(Expression expr) { if (expr is QuantifierExpr) { - foreach (var trigger in (expr as QuantifierExpr).Attributes.AsEnumerable().Where(a => a.Name == "trigger").SelectMany(a => a.Args)) { - collector.Visit(trigger); + var e = (QuantifierExpr)expr; + if (e.SplitQuantifier == null) { + foreach (var trigger in (expr as QuantifierExpr).Attributes.AsEnumerable().Where(a => a.Name == "trigger").SelectMany(a => a.Args)) { + collector.Visit(trigger); + } } } } @@ -13173,6 +13197,7 @@ namespace Microsoft.Dafny { } List ApplyInduction(QuantifierExpr e) { + Contract.Requires(e.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier Contract.Requires(e.TypeArgs.Count == 0); return ApplyInduction(e.BoundVars, e.Attributes, new List() { e.LogicalBody() }, delegate(System.IO.TextWriter wr) { new Printer(wr).PrintExpression(e, true); }); @@ -13946,6 +13971,12 @@ namespace Microsoft.Dafny { var e = (ComprehensionExpr)expr; // For quantifiers and setComprehesion we want to make sure that we don't introduce name clashes with // the enclosing scopes. + + var q = e as QuantifierExpr; + if (q != null && q.SplitQuantifier != null) { + return Substitute(q.SplitQuantifierExpression); + } + var newBoundVars = CreateBoundVarSubstitutions(e.BoundVars, expr is ForallExpr || expr is ExistsExpr || expr is SetComprehension); Expression newRange = e.Range == null ? null : Substitute(e.Range); Expression newTerm = Substitute(e.Term); diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index 33be0da2..80381f0a 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -21,30 +21,37 @@ namespace Microsoft.Dafny.Triggers { // Unfortunately, this would cause ill-behaved quantifiers to produce // exponentially many smaller quantifiers. + private static UnaryOpExpr Not(Expression expr) { + var not = new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type }; + return not; + } + internal static IEnumerable SplitExpr(Expression expr, BinaryExpr.Opcode separator) { expr = expr.Resolved; var unary = expr as UnaryOpExpr; var binary = expr as BinaryExpr; if (unary != null && unary.Op == UnaryOpExpr.Opcode.Not) { - foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, e); } + foreach (var e in SplitExpr(unary.E, FlipOpcode(separator))) { yield return Not(e); } } else if (binary != null && binary.Op == separator) { foreach (var e in SplitExpr(binary.E0, separator)) { yield return e; } foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; } } else if (binary != null && binary.Op == BinaryExpr.Opcode.Imp && separator == BinaryExpr.Opcode.Or) { - foreach (var e in SplitExpr(new UnaryOpExpr(unary.tok, UnaryOpExpr.Opcode.Not, binary.E0), separator)) { yield return e; } + foreach (var e in SplitExpr(Not(binary.E0), separator)) { yield return e; } foreach (var e in SplitExpr(binary.E1, separator)) { yield return e; } + } else { + yield return expr; } } internal static IEnumerable SplitAndStich(BinaryExpr pair, BinaryExpr.Opcode separator) { - foreach (var e1 in SplitExpr(pair.E1, separator)) { - yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1); + foreach (var e1 in SplitExpr(pair.E1, separator)) { + yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1) { ResolvedOp = pair.ResolvedOp, Type = pair.Type }; } } internal static IEnumerable SplitQuantifier(QuantifierExpr quantifier) { - var body = quantifier.LogicalBody(); + var body = quantifier.Term; var binary = body as BinaryExpr; if (quantifier is ForallExpr) { @@ -55,7 +62,7 @@ namespace Microsoft.Dafny.Triggers { stream = SplitExpr(body, BinaryExpr.Opcode.And); } foreach (var e in stream) { - yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes); + yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type }; } } else if (quantifier is ExistsExpr) { IEnumerable stream; @@ -65,17 +72,18 @@ namespace Microsoft.Dafny.Triggers { stream = SplitExpr(body, BinaryExpr.Opcode.Or); } foreach (var e in stream) { - yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, quantifier.Term, quantifier.Attributes); + yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type }; } } else { yield return quantifier; } } - protected override void VisitOneExpr(Expression expr) { //FIXME: This doesn't save the rewritten quantifier + protected override void VisitOneExpr(Expression expr) { var quantifier = expr as QuantifierExpr; if (quantifier != null) { - var rew = SplitQuantifier(quantifier); + var split = SplitQuantifier(quantifier).ToList(); + quantifier.SplitQuantifier = split; //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| ")); } } diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index da43abcc..9fbc8a8a 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -272,6 +272,14 @@ namespace Microsoft.Dafny.Triggers { } private static bool ShallowEq(QuantifierExpr expr1, QuantifierExpr expr2) { //FIXME are these TypeArgs still useful? + if (!TriggerUtils.SameNullity(expr1.SplitQuantifier, expr2.SplitQuantifier)) { + return false; + } + + if (expr1.SplitQuantifier != null && expr2.SplitQuantifier != null) { + return ShallowEq_Top(expr1.SplitQuantifierExpression, expr2.SplitQuantifierExpression); + } + if (expr1.TypeArgs.Count != expr2.TypeArgs.Count || !TriggerUtils.SameNullity(expr1.Range, expr2.Range)) { return false; diff --git a/Source/Dafny/Triggers/TriggerGenerator.cs b/Source/Dafny/Triggers/TriggerGenerator.cs index de4b212b..e218ad7b 100644 --- a/Source/Dafny/Triggers/TriggerGenerator.cs +++ b/Source/Dafny/Triggers/TriggerGenerator.cs @@ -19,9 +19,13 @@ namespace Microsoft.Dafny.Triggers { //FIXME rename this file protected override bool VisitOneExpr(Expression expr, ref object st) { var quantifier = expr as QuantifierExpr; if (quantifier != null) { - quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter)); - } //FIXME handle the case of groups of quantifiers resulting from a split - + if (quantifier.SplitQuantifier != null) { + var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null); + quantifierCollections.Add(new QuantifiersCollection(collection, reporter)); + } else { + quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter)); + } + } return true; } } diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index dedbcbb1..6c6eede2 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -101,6 +101,7 @@ namespace Microsoft.Dafny.Triggers { } internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) { + Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier return quantifier.Attributes.AsEnumerable().All(aa => aa.Name != "trigger" && aa.Name != "no_trigger"); } } diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index e1f8a013..9f721d9a 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -44,11 +44,13 @@ namespace Microsoft.Dafny.Triggers { } internal IEnumerable LoopingSubterms(QuantifierExpr quantifier) { + Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier var matchingSubterms = MatchingSubterms(quantifier); return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms)); } internal List MatchingSubterms(QuantifierExpr quantifier) { + Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier //FIXME this will miss rewritten expressions (CleanupExpr). Should introduce an OriginalExpr to compare against. return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq); } @@ -139,7 +141,7 @@ namespace Microsoft.Dafny.Triggers { (expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944 (expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) { annotation = AnnotatePotentialCandidate(expr); - } else if (expr is QuantifierExpr) { + } else if (expr is QuantifierExpr && ((QuantifierExpr)expr).SplitQuantifier == null) { annotation = AnnotateQuantifier((QuantifierExpr)expr); } else if (expr is LetExpr) { annotation = AnnotateLetExpr((LetExpr)expr); @@ -259,6 +261,7 @@ namespace Microsoft.Dafny.Triggers { // FIXME document that this will contain duplicates internal List CollectTriggers(QuantifierExpr quantifier) { + Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier // TODO could check for existing triggers and return that instead, but that require a bit of work to extract the expressions return Annotate(quantifier).PrivateTerms; } -- cgit v1.2.3 From 6891a07f8213448bb483e434f66f552370fe9d66 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 18 Aug 2015 08:49:19 -0700 Subject: Use nested tokens in the quantifier splitter This allows it to report the source of the error, giving better feedback to the user about which precondition to a function failed to hold, for example. --- Source/Dafny/Triggers/QuantifierSplitter.cs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index 80381f0a..4b223856 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -19,7 +19,9 @@ namespace Microsoft.Dafny.Triggers { // NOTE: If we wanted to split quantifiers as far as possible, it would be // enough to put the formulas in DNF (for foralls) or CNF (for exists). // Unfortunately, this would cause ill-behaved quantifiers to produce - // exponentially many smaller quantifiers. + // exponentially many smaller quantifiers. Thus we only do one step of + // distributing, which takes care of the usual precondition case: + // forall x :: P(x) ==> (Q(x) && R(x)) private static UnaryOpExpr Not(Expression expr) { var not = new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type }; @@ -62,7 +64,8 @@ namespace Microsoft.Dafny.Triggers { stream = SplitExpr(body, BinaryExpr.Opcode.And); } foreach (var e in stream) { - yield return new ForallExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type }; + var tok = new NestedToken(quantifier.tok, e.tok); + yield return new ForallExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type }; } } else if (quantifier is ExistsExpr) { IEnumerable stream; @@ -72,13 +75,14 @@ namespace Microsoft.Dafny.Triggers { stream = SplitExpr(body, BinaryExpr.Opcode.Or); } foreach (var e in stream) { - yield return new ExistsExpr(quantifier.tok, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type }; + var tok = new NestedToken(quantifier.tok, e.tok); + yield return new ExistsExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type }; } } else { yield return quantifier; } } - + protected override void VisitOneExpr(Expression expr) { var quantifier = expr as QuantifierExpr; if (quantifier != null) { -- cgit v1.2.3 From e3fff39c37ed68cf718eab84613e3bbb02858653 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 10:01:50 -0700 Subject: Allow users to disable quantifier splitting by with a {:split false} attribute --- Source/Dafny/Triggers/QuantifierSplitter.cs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index 4b223856..c50bc9c6 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -85,10 +85,12 @@ namespace Microsoft.Dafny.Triggers { protected override void VisitOneExpr(Expression expr) { var quantifier = expr as QuantifierExpr; - if (quantifier != null) { - var split = SplitQuantifier(quantifier).ToList(); - quantifier.SplitQuantifier = split; - //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| ")); + if (quantifier != null && quantifier.SplitQuantifier == null) { + bool splitAttr = true; + if (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) { + var split = SplitQuantifier(quantifier).ToList(); + quantifier.SplitQuantifier = split; + } } } } -- cgit v1.2.3 From e0dbb8af7290beb81350acd0088866c0ca54acb8 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 00:09:36 -0700 Subject: Improve error reporting for split quantifiers --- Source/Dafny/Triggers/QuantifierSplitter.cs | 3 +- Test/triggers/splitting-picks-the-right-tokens.dfy | 24 ++++++++++++++ .../splitting-picks-the-right-tokens.dfy.expect | 38 ++++++++++++++++++++++ 3 files changed, 64 insertions(+), 1 deletion(-) create mode 100644 Test/triggers/splitting-picks-the-right-tokens.dfy create mode 100644 Test/triggers/splitting-picks-the-right-tokens.dfy.expect (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index c50bc9c6..ae76b780 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -48,7 +48,8 @@ namespace Microsoft.Dafny.Triggers { internal static IEnumerable SplitAndStich(BinaryExpr pair, BinaryExpr.Opcode separator) { foreach (var e1 in SplitExpr(pair.E1, separator)) { - yield return new BinaryExpr(pair.tok, pair.Op, pair.E0, e1) { ResolvedOp = pair.ResolvedOp, Type = pair.Type }; + // Notice the token. This makes triggers/splitting-picks-the-right-tokens.dfy possible + yield return new BinaryExpr(e1.tok, pair.Op, pair.E0, e1) { ResolvedOp = pair.ResolvedOp, Type = pair.Type }; } } diff --git a/Test/triggers/splitting-picks-the-right-tokens.dfy b/Test/triggers/splitting-picks-the-right-tokens.dfy new file mode 100644 index 00000000..76065eca --- /dev/null +++ b/Test/triggers/splitting-picks-the-right-tokens.dfy @@ -0,0 +1,24 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This file ensures that trigger splitting picks the right tokens + +function Id(i: int): int { i } + +method MSuchThat() + requires forall x | x > 0 :: Id(x) > 1 && x > 2 && x > -1 { } + +method MImplies() + // The bodies of the two terms that are produced here are both + // BinaryExpressions(==>); the token they use, however, is that of the RHS + // terms of these implications; otherwise, error messages would get stacked on + // the ==> sign + requires forall x :: x > 0 ==> Id(x) > 1 && x > 2 && x > -1 { } + +method M() { + if * { + MImplies(); + } else { + MSuchThat(); + } +} diff --git a/Test/triggers/splitting-picks-the-right-tokens.dfy.expect b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect new file mode 100644 index 00000000..af274e75 --- /dev/null +++ b/Test/triggers/splitting-picks-the-right-tokens.dfy.expect @@ -0,0 +1,38 @@ +splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {Id(x) > 1}: + Selected triggers: {Id(x)} +splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {x > 2}: + Selected triggers: {Id(x)} +splitting-picks-the-right-tokens.dfy(9,11): Info: For expression {x > -1}: + Selected triggers: {Id(x)} +splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> Id(x) > 1}: + Selected triggers: {Id(x)} +splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> x > 2}: + Selected triggers: {Id(x)} +splitting-picks-the-right-tokens.dfy(16,11): Info: For expression {x > 0 ==> x > -1}: + Selected triggers: {Id(x)} +splitting-picks-the-right-tokens.dfy(20,12): Error BP5002: A precondition for this call might not hold. +splitting-picks-the-right-tokens.dfy(16,11): Related location: This is the precondition that might not hold. +splitting-picks-the-right-tokens.dfy(16,48): Related location +Execution trace: + (0,0): anon0 + (0,0): anon3_Then +splitting-picks-the-right-tokens.dfy(20,12): Error BP5002: A precondition for this call might not hold. +splitting-picks-the-right-tokens.dfy(16,11): Related location: This is the precondition that might not hold. +splitting-picks-the-right-tokens.dfy(16,39): Related location +Execution trace: + (0,0): anon0 + (0,0): anon3_Then +splitting-picks-the-right-tokens.dfy(22,13): Error BP5002: A precondition for this call might not hold. +splitting-picks-the-right-tokens.dfy(9,11): Related location: This is the precondition that might not hold. +splitting-picks-the-right-tokens.dfy(9,46): Related location +Execution trace: + (0,0): anon0 + (0,0): anon3_Else +splitting-picks-the-right-tokens.dfy(22,13): Error BP5002: A precondition for this call might not hold. +splitting-picks-the-right-tokens.dfy(9,11): Related location: This is the precondition that might not hold. +splitting-picks-the-right-tokens.dfy(9,37): Related location +Execution trace: + (0,0): anon0 + (0,0): anon3_Else + +Dafny program verifier finished with 6 verified, 4 errors -- cgit v1.2.3 From be66434c97446d311aada9aec42fdbc8eba26ea8 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 00:11:00 -0700 Subject: Shallow-copy quantifier attributes when splitting --- Source/Dafny/Triggers/QuantifierSplitter.cs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index ae76b780..83059f8d 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -66,7 +66,7 @@ namespace Microsoft.Dafny.Triggers { } foreach (var e in stream) { var tok = new NestedToken(quantifier.tok, e.tok); - yield return new ForallExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type }; + yield return new ForallExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type }; } } else if (quantifier is ExistsExpr) { IEnumerable stream; @@ -77,7 +77,7 @@ namespace Microsoft.Dafny.Triggers { } foreach (var e in stream) { var tok = new NestedToken(quantifier.tok, e.tok); - yield return new ExistsExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, quantifier.Attributes) { Type = quantifier.Type }; + yield return new ExistsExpr(tok, quantifier.TypeArgs, quantifier.BoundVars, quantifier.Range, e, CopyAttributes(quantifier.Attributes)) { Type = quantifier.Type }; } } else { yield return quantifier; -- cgit v1.2.3 From dc08d67a27ffeb26889a56daa573ccc56daa1c0d Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 00:12:04 -0700 Subject: Make quantifier splitting a two step process This fixes a bug that affected Monad.dfy --- Source/Dafny/DafnyAst.cs | 2 +- Source/Dafny/Rewriter.cs | 1 + Source/Dafny/Triggers/QuantifierSplitter.cs | 42 ++++++++++++++++++++++++----- Test/triggers/regression-tests.dfy | 20 ++++++++++++++ Test/triggers/regression-tests.dfy.expect | 3 +++ 5 files changed, 60 insertions(+), 8 deletions(-) create mode 100644 Test/triggers/regression-tests.dfy create mode 100644 Test/triggers/regression-tests.dfy.expect (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index c4ea0a5a..c7aae173 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4796,7 +4796,7 @@ namespace Microsoft.Dafny { } public override IEnumerable SubExpressions { - get { + get { // FIXME: This can return duplicates; this could confuse BottomUpVisitors that modify the AST in place foreach (var e in base.SubExpressions) { yield return e; } foreach (var e in Attributes.SubExpressions(Attributes)) { yield return e; } diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 557eee93..9bc24c30 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -68,6 +68,7 @@ namespace Microsoft.Dafny foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { splitter.Visit(decl); } + splitter.Commit(); } } diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index 83059f8d..865aa33e 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -1,11 +1,19 @@ using Microsoft.Boogie; using System; using System.Collections.Generic; +using System.Diagnostics.Contracts; using System.Linq; using System.Text; namespace Microsoft.Dafny.Triggers { class QuantifierSplitter : BottomUpVisitor { + /// This cache was introduced because some statements (notably calc) return the same SubExpression multiple times. + /// This ended up causing an inconsistent situation when the calc statement's subexpressions contained the same quantifier + /// twice: on the first pass that quantifier got its SplitQuantifiers generated, and on the the second pass these + /// split quantifiers got re-split, creating a situation where the direct children of a split quantifier were + /// also split quantifiers. + private Dictionary> splits = new Dictionary>(); + private static BinaryExpr.Opcode FlipOpcode(BinaryExpr.Opcode opCode) { if (opCode == BinaryExpr.Opcode.And) { return BinaryExpr.Opcode.Or; @@ -24,8 +32,15 @@ namespace Microsoft.Dafny.Triggers { // forall x :: P(x) ==> (Q(x) && R(x)) private static UnaryOpExpr Not(Expression expr) { - var not = new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type }; - return not; + return new UnaryOpExpr(expr.tok, UnaryOpExpr.Opcode.Not, expr) { Type = expr.Type }; + } + + private static Attributes CopyAttributes(Attributes source) { + if (source == null) { + return null; + } else { + return new Attributes(source.Name, source.Args, CopyAttributes(source.Prev)); + } } internal static IEnumerable SplitExpr(Expression expr, BinaryExpr.Opcode separator) { @@ -83,16 +98,29 @@ namespace Microsoft.Dafny.Triggers { yield return quantifier; } } + + private static bool AllowsSplitting(QuantifierExpr quantifier) { + bool splitAttr = true; + return !Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr; + } protected override void VisitOneExpr(Expression expr) { var quantifier = expr as QuantifierExpr; - if (quantifier != null && quantifier.SplitQuantifier == null) { - bool splitAttr = true; - if (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) { - var split = SplitQuantifier(quantifier).ToList(); - quantifier.SplitQuantifier = split; + if (quantifier != null) { + Contract.Assert(quantifier.SplitQuantifier == null); + if (!splits.ContainsKey(quantifier) && AllowsSplitting(quantifier)) { + splits[quantifier] = SplitQuantifier(quantifier).ToList(); } } } + + /// + /// See comments above definition of splits for reason why this method exists + /// + internal void Commit() { + foreach (var quantifier in splits.Keys) { + quantifier.SplitQuantifier = splits[quantifier]; + } + } } } diff --git a/Test/triggers/regression-tests.dfy b/Test/triggers/regression-tests.dfy new file mode 100644 index 00000000..263e424a --- /dev/null +++ b/Test/triggers/regression-tests.dfy @@ -0,0 +1,20 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This tests checks that quantifier splitting is resilient to the fact that +// certain statements (like calc) can return duplicate subexpressions. This was +// once a problem, because a quantifier that got returned twice would get split +// on the first pass over it, and would have its nely created children re-split +// on the second pass. This created a split quantifier whose children were split +// quantifiers, which violated an invariant of spliit quantifiers. + +abstract module Base { } + +module Blah refines Base { + lemma A() { + calc { + forall b :: b; + } + } +} + diff --git a/Test/triggers/regression-tests.dfy.expect b/Test/triggers/regression-tests.dfy.expect new file mode 100644 index 00000000..a03810fb --- /dev/null +++ b/Test/triggers/regression-tests.dfy.expect @@ -0,0 +1,3 @@ +regression-tests.dfy(16,5): Warning: (!) No terms found to trigger on. + +Dafny program verifier finished with 2 verified, 0 errors -- cgit v1.2.3 From b8fad094ad74180ca16670bebe602737d856b5da Mon Sep 17 00:00:00 2001 From: qunyanm Date: Wed, 25 Nov 2015 10:27:02 -0800 Subject: Fix issue 103. Emit the quantifiers for ForallStmt before AutoTrigger so that the auto-triggers can be computed for ForallStmt. --- Source/Dafny/Cloner.cs | 4 +- Source/Dafny/DafnyAst.cs | 1 + Source/Dafny/Printer.cs | 15 +- Source/Dafny/Resolver.cs | 1 + Source/Dafny/Rewriter.cs | 273 +++++++++++++++++++++ Source/Dafny/Translator.cs | 340 +++++++------------------- Source/Dafny/Triggers/QuantifierSplitter.cs | 12 + Source/Dafny/Triggers/QuantifiersCollector.cs | 13 + Test/dafny0/SmallTests.dfy.expect | 1 + Test/dafny4/Bug103.dfy | 20 ++ Test/dafny4/Bug103.dfy.expect | 2 + 11 files changed, 424 insertions(+), 258 deletions(-) create mode 100644 Test/dafny4/Bug103.dfy create mode 100644 Test/dafny4/Bug103.dfy.expect (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index 1a6dfecb..6b3b0caa 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -552,7 +552,9 @@ namespace Microsoft.Dafny } else if (stmt is ForallStmt) { var s = (ForallStmt)stmt; r = new ForallStmt(Tok(s.Tok), Tok(s.EndTok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body)); - + if (s.ForallExpressions != null) { + ((ForallStmt)r).ForallExpressions = s.ForallExpressions.ConvertAll(CloneExpr); + } } else if (stmt is CalcStmt) { var s = (CalcStmt)stmt; // calc statements have the unusual property that the last line is duplicated. If that is the case (which diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 847617aa..4c1e2bd7 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -4693,6 +4693,7 @@ namespace Microsoft.Dafny { public readonly Expression Range; public readonly List Ens; public readonly Statement Body; + public List ForallExpressions; // fill in by rewriter. public List Bounds; // initialized and filled in by resolver // invariant: if successfully resolved, Bounds.Count == BoundVars.Count; diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 145e82e7..0a25b941 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -841,11 +841,22 @@ namespace Microsoft.Dafny { wr.Write("}"); } else if (stmt is ForallStmt) { - var s = (ForallStmt)stmt; + var s = (ForallStmt)stmt; + Attributes attributes = s.Attributes; + if (attributes == null && s.ForallExpressions != null) { + foreach (Expression expr in s.ForallExpressions) { + ForallExpr e = (ForallExpr)expr; + while (e != null && attributes == null) { + attributes = e.Attributes; + e = (ForallExpr)e.SplitQuantifierExpression; + } + if (attributes != null) { break; } + } + } wr.Write("forall"); if (s.BoundVars.Count != 0) { wr.Write(" "); - PrintQuantifierDomain(s.BoundVars, s.Attributes, s.Range); + PrintQuantifierDomain(s.BoundVars, attributes, s.Range); } if (s.Ens.Count == 0) { wr.Write(" "); diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 315b823a..eff7d97d 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -235,6 +235,7 @@ namespace Microsoft.Dafny rewriters.Add(new AutoReqFunctionRewriter(this.reporter, opaqueRewriter)); rewriters.Add(opaqueRewriter); rewriters.Add(new TimeLimitRewriter(reporter)); + rewriters.Add(new ForallStmtRewriter(reporter)); if (DafnyOptions.O.AutoTriggers) { rewriters.Add(new QuantifierSplittingRewriter(reporter)); diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 39c8f667..802b1918 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -72,6 +72,279 @@ namespace Microsoft.Dafny } } + // write out the quantifier for ForallStmt + public class ForallStmtRewriter : IRewriter + { + public ForallStmtRewriter(ErrorReporter reporter) : base(reporter) { + Contract.Requires(reporter != null); + } + + internal override void PostResolve(ModuleDefinition m) { + var forallvisiter = new ForAllStmtVisitor(); + foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { + forallvisiter.Visit(decl, true); + } + } + + internal class ForAllStmtVisitor : TopDownVisitor + { + protected override bool VisitOneStmt(Statement stmt, ref bool st) { + Contract.Requires(stmt != null); + if (stmt is ForallStmt) { + ForallStmt s = (ForallStmt)stmt; + if (s.Kind == ForallStmt.ParBodyKind.Proof) { + Expression term = s.Ens.Count != 0 ? s.Ens[0].E : new LiteralExpr(s.Tok, true); + for (int i = 1; i < s.Ens.Count; i++) { + term = new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.And, term, s.Ens[i].E); + } + List exprList = new List(); + ForallExpr expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, term, s.Attributes); + expr.Type = Type.Bool; // resolve here + exprList.Add(expr); + s.ForallExpressions = exprList; + } else if (s.Kind == ForallStmt.ParBodyKind.Assign) { + if (s.BoundVars.Count != 0) { + var s0 = (AssignStmt)s.S0; + if (s0.Rhs is ExprRhs) { + List exprList = new List(); + Expression Fi = null; + Func lhsBuilder = null; + var lhs = s0.Lhs.Resolved; + var i = s.BoundVars[0]; + if (s.BoundVars.Count == 1) { + //var lhsContext = null; + // Detect the following cases: + // 0: forall i | R(i) { F(i).f := E(i); } + // 1: forall i | R(i) { A[F(i)] := E(i); } + // 2: forall i | R(i) { F(i)[N] := E(i); } + if (lhs is MemberSelectExpr) { + var ll = (MemberSelectExpr)lhs; + Fi = ll.Obj; + lhsBuilder = e => { var l = new MemberSelectExpr(ll.tok, e, ll.MemberName); l.Member = ll.Member; l.Type = ll.Type; return l; }; + } else if (lhs is SeqSelectExpr) { + var ll = (SeqSelectExpr)lhs; + Contract.Assert(ll.SelectOne); + if (!Translator.ContainsFreeVariable(ll.Seq, false, i)) { + Fi = ll.E0; + lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, ll.Seq, e, null); l.Type = ll.Type; return l; }; + } else if (!Translator.ContainsFreeVariable(ll.E0, false, i)) { + Fi = ll.Seq; + lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, e, ll.E0, null); l.Type = ll.Type; return l; }; + } + } + } + var rhs = ((ExprRhs)s0.Rhs).Expr; + bool usedInversion = false; + if (Fi != null) { + var j = new BoundVar(i.tok, i.Name + "#inv", Fi.Type); + var jj = Expression.CreateIdentExpr(j); + var jList = new List() { j }; + var vals = InvertExpression(i, j, s.Range, Fi); +#if DEBUG_PRINT + Console.WriteLine("DEBUG: Trying to invert:"); + Console.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi)); + if (vals == null) { + Console.WriteLine("DEBUG: Can't"); + } else { + Console.WriteLine("DEBUG: The inverse is the disjunction of the following:"); + foreach (var val in vals) { + Console.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name); + } + } +#endif + if (vals != null) { + foreach (var val in vals) { + lhs = lhsBuilder(jj); + Attributes attributes = new Attributes("trigger", new List() { lhs }, s.Attributes); + var expr = new ForallExpr(s.Tok, jList, val.Range, new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.EqCommon, lhs, Substitute(rhs, i, val.FInverse)), attributes); + expr.Type = Type.Bool; //resolve here + exprList.Add(expr); + } + usedInversion = true; + } + } + if (!usedInversion) { + var expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.EqCommon, lhs, rhs), s.Attributes); + expr.Type = Type.Bool; // resolve here + exprList.Add(expr); + } + s.ForallExpressions = exprList; + } + } + } else if (s.Kind == ForallStmt.ParBodyKind.Call) { + var s0 = (CallStmt)s.S0; + Expression term = s0.Method.Ens.Count != 0 ? s0.Method.Ens[0].E : new LiteralExpr(s.Tok, true); + for (int i = 1; i < s0.Method.Ens.Count; i++) { + term = new BinaryExpr(s.Tok, BinaryExpr.ResolvedOpcode.And, term, s0.Method.Ens[i].E); + } + List exprList = new List(); + ForallExpr expr = new ForallExpr(s.Tok, s.BoundVars, s.Range, term, s.Attributes); + expr.Type = Type.Bool; // resolve here + exprList.Add(expr); + } else { + Contract.Assert(false); // unexpected kind + } + } + return true; //visit the sub-parts with the same "st" + } + + internal class ForallStmtTranslationValues + { + public readonly Expression Range; + public readonly Expression FInverse; + public ForallStmtTranslationValues(Expression range, Expression fInverse) { + Contract.Requires(range != null); + Contract.Requires(fInverse != null); + Range = range; + FInverse = fInverse; + } + public ForallStmtTranslationValues Subst(IVariable j, Expression e) { + Contract.Requires(j != null); + Contract.Requires(e != null); + Dictionary typeMap = new Dictionary(); + var substMap = new Dictionary(); + substMap.Add(j, e); + Translator.Substituter sub = new Translator.Substituter(null, substMap, typeMap, null); + var v = new ForallStmtTranslationValues(sub.Substitute(Range), sub.Substitute(FInverse)); + return v; + } + } + + /// + /// Find piecewise inverse of F under R. More precisely, find lists of expressions P and F-1 + /// such that + /// R(i) && j == F(i) + /// holds iff the disjunction of the following predicates holds: + /// P_0(j) && F-1_0(j) == i + /// ... + /// P_{n-1}(j) && F-1_{n-1}(j) == i + /// If no such disjunction is found, return null. + /// If such a disjunction is found, return for each disjunct: + /// * The predicate P_k(j), which is an expression that may have free occurrences of j (but no free occurrences of i) + /// * The expression F-1_k(j), which also may have free occurrences of j but not of i + /// + private List InvertExpression(BoundVar i, BoundVar j, Expression R, Expression F) { + Contract.Requires(i != null); + Contract.Requires(j != null); + Contract.Requires(R != null); + Contract.Requires(F != null); + var vals = new List(InvertExpressionIter(i, j, R, F)); + if (vals.Count == 0) { + return null; + } else { + return vals; + } + } + /// + /// See InvertExpression. + /// + private IEnumerable InvertExpressionIter(BoundVar i, BoundVar j, Expression R, Expression F) { + Contract.Requires(i != null); + Contract.Requires(j != null); + Contract.Requires(R != null); + Contract.Requires(F != null); + F = F.Resolved; + if (!Translator.ContainsFreeVariable(F, false, i)) { + // We're looking at R(i) && j == K. + // We cannot invert j == K, but if we're lucky, R(i) contains a conjunct i==G. + Expression r = Expression.CreateBoolLiteral(R.tok, true); + Expression G = null; + foreach (var c in Expression.Conjuncts(R)) { + if (G == null && c is BinaryExpr) { + var bin = (BinaryExpr)c; + if (BinaryExpr.IsEqualityOp(bin.ResolvedOp)) { + var id = bin.E0.Resolved as IdentifierExpr; + if (id != null && id.Var == i) { + G = bin.E1; + continue; + } + id = bin.E1.Resolved as IdentifierExpr; + if (id != null && id.Var == i) { + G = bin.E0; + continue; + } + } + } + r = Expression.CreateAnd(r, c); + } + if (G != null) { + var jIsK = Expression.CreateEq(Expression.CreateIdentExpr(j), F, j.Type); + var rr = Substitute(r, i, G); + yield return new ForallStmtTranslationValues(Expression.CreateAnd(rr, jIsK), G); + } + } else if (F is IdentifierExpr) { + var e = (IdentifierExpr)F; + if (e.Var == i) { + // We're looking at R(i) && j == i, which is particularly easy to invert: R(j) && j == i + var jj = Expression.CreateIdentExpr(j); + yield return new ForallStmtTranslationValues(Substitute(R, i, jj), jj); + } + } else if (F is BinaryExpr) { + var bin = (BinaryExpr)F; + if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) { + if (!Translator.ContainsFreeVariable(bin.E1, false, i)) { + // We're looking at: R(i) && j == f(i) + K. + // By a recursive call, we'll ask to invert: R(i) && j' == f(i). + // For each P_0(j') && f-1_0(j') == i we get back, we yield: + // P_0(j - K) && f-1_0(j - K) == i + var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E1); + foreach (var val in InvertExpression(i, j, R, bin.E0)) { + yield return val.Subst(j, jMinusK); + } + } else if (!Translator.ContainsFreeVariable(bin.E0, false, i)) { + // We're looking at: R(i) && j == K + f(i) + // Do as in previous case, but with operands reversed. + var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E0); + foreach (var val in InvertExpression(i, j, R, bin.E1)) { + yield return val.Subst(j, jMinusK); + } + } + } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) { + if (!Translator.ContainsFreeVariable(bin.E1, false, i)) { + // We're looking at: R(i) && j == f(i) - K + // Recurse on f(i) and then replace j := j + K + var jPlusK = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E1); + foreach (var val in InvertExpression(i, j, R, bin.E0)) { + yield return val.Subst(j, jPlusK); + } + } else if (!Translator.ContainsFreeVariable(bin.E0, false, i)) { + // We're looking at: R(i) && j == K - f(i) + // Recurse on f(i) and then replace j := K - j + var kMinusJ = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E0); + foreach (var val in InvertExpression(i, j, R, bin.E1)) { + yield return val.Subst(j, kMinusJ); + } + } + } + } else if (F is ITEExpr) { + var ife = (ITEExpr)F; + // We're looking at R(i) && j == if A(i) then B(i) else C(i), which is equivalent to the disjunction of: + // R(i) && A(i) && j == B(i) + // R(i) && !A(i) && j == C(i) + // We recurse on each one, yielding the results + var r = Expression.CreateAnd(R, ife.Test); + var valsThen = InvertExpression(i, j, r, ife.Thn); + if (valsThen != null) { + r = Expression.CreateAnd(R, Expression.CreateNot(ife.tok, ife.Test)); + var valsElse = InvertExpression(i, j, r, ife.Els); + if (valsElse != null) { + foreach (var val in valsThen) { yield return val; } + foreach (var val in valsElse) { yield return val; } + } + } + } + } + + Expression Substitute(Expression expr, IVariable v, Expression e) { + Dictionary substMap = new Dictionary(); + Dictionary typeMap = new Dictionary(); + substMap.Add(v, e); + Translator.Substituter sub = new Translator.Substituter(null, substMap, typeMap, null); + return sub.Substitute(expr); + } + } + } + /// /// AutoContracts is an experimental feature that will fill much of the dynamic-frames boilerplate /// into a class. From the user's perspective, what needs to be done is simply: diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 8e8c3c19..37408aa1 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -2860,11 +2860,11 @@ namespace Microsoft.Dafny { #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); + TrForallStmtCall(m.tok, parBoundVars, parRange, decrCheck, null, 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, null, recursiveCall, null, builder, localVariables, etran); #endif } // translate the body of the method @@ -7413,7 +7413,7 @@ namespace Microsoft.Dafny { var s0 = (CallStmt)s.S0; var definedness = new Bpl.StmtListBuilder(); var exporter = new Bpl.StmtListBuilder(); - TrForallStmtCall(s.Tok, s.BoundVars, s.Range, null, s0, definedness, exporter, locals, etran); + TrForallStmtCall(s.Tok, s.BoundVars, s.Range, null, s.ForallExpressions, 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)); @@ -8038,65 +8038,16 @@ namespace Microsoft.Dafny { Bpl.Expr qq = new Bpl.ForallExpr(s.Tok, new List { alpha }, new List { oVar, fVar }, null, tr, body); updater.Add(new Bpl.AssumeCmd(s.Tok, qq)); - if (s0.Rhs is ExprRhs) { - Expression Fi = null; - Func lhsBuilder = null; - lhs = s0.Lhs.Resolved; - var i = s.BoundVars[0]; - if (s.BoundVars.Count == 1) { - //var lhsContext = null; - // Detect the following cases: - // 0: forall i | R(i) { F(i).f := E(i); } - // 1: forall i | R(i) { A[F(i)] := E(i); } - // 2: forall i | R(i) { F(i)[N] := E(i); } - if (lhs is MemberSelectExpr) { - var ll = (MemberSelectExpr)lhs; - Fi = ll.Obj; - lhsBuilder = e => { var l = new MemberSelectExpr(ll.tok, e, ll.MemberName); l.Member = ll.Member; l.Type = ll.Type; return l; }; - } else if (lhs is SeqSelectExpr) { - var ll = (SeqSelectExpr)lhs; - Contract.Assert(ll.SelectOne); - if (!ContainsFreeVariable(ll.Seq, false, i)) { - Fi = ll.E0; - lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, ll.Seq, e, null); l.Type = ll.Type; return l; }; - } else if (!ContainsFreeVariable(ll.E0, false, i)) { - Fi = ll.Seq; - lhsBuilder = e => { var l = new SeqSelectExpr(ll.tok, true, e, ll.E0, null); l.Type = ll.Type; return l; }; - } - } - } - var rhs = ((ExprRhs)s0.Rhs).Expr; - bool usedInversion = false; - if (Fi != null) { - var j = new BoundVar(i.tok, i.Name + "#inv", Fi.Type); - var jj = Expression.CreateIdentExpr(j); - var jList = new List() { j }; - var vals = InvertExpression(i, j, s.Range, Fi); -#if DEBUG_PRINT - Console.WriteLine("DEBUG: Trying to invert:"); - Console.WriteLine("DEBUG: " + Printer.ExprToString(s.Range) + " && " + j.Name + " == " + Printer.ExprToString(Fi)); - if (vals == null) { - Console.WriteLine("DEBUG: Can't"); - } else { - Console.WriteLine("DEBUG: The inverse is the disjunction of the following:"); - foreach (var val in vals) { - Console.WriteLine("DEBUG: " + Printer.ExprToString(val.Range) + " && " + Printer.ExprToString(val.FInverse) + " == " + i.Name); - } - } -#endif - if (vals != null) { - foreach (var val in vals) { - qq = TrForall_NewValueAssumption(s.Tok, jList, val.Range, lhsBuilder(jj), Substitute(rhs, i, val.FInverse), true, etran, prevEtran); - updater.Add(new Bpl.AssumeCmd(s.Tok, qq)); - } - usedInversion = true; - } - } - if (!usedInversion) { - qq = TrForall_NewValueAssumption(s.Tok, s.BoundVars, s.Range, lhs, rhs, false, etran, prevEtran); + if (s.ForallExpressions != null) { + foreach (ForallExpr expr in s.ForallExpressions) { + BinaryExpr term = (BinaryExpr)expr.Term; + Contract.Assert(term != null); + var e0 = Substitute(((BinaryExpr)term).E0.Resolved, null, substMap); + var e1 = Substitute(((BinaryExpr)term).E1, null, substMap); + qq = TrForall_NewValueAssumption(expr.tok, expr.BoundVars, expr.Range, e0, e1, expr.Attributes, etran, prevEtran); updater.Add(new Bpl.AssumeCmd(s.Tok, qq)); } - } + } } /// @@ -8110,7 +8061,7 @@ namespace Microsoft.Dafny { /// G is rhs /// If lhsAsTrigger is true, then use the LHS of the equality above as the trigger; otherwise, don't specify any trigger. /// - private Bpl.Expr TrForall_NewValueAssumption(IToken tok, List boundVars, Expression range, Expression lhs, Expression rhs, bool lhsAsTrigger, ExpressionTranslator etran, ExpressionTranslator prevEtran) { + private Bpl.Expr TrForall_NewValueAssumption(IToken tok, List boundVars, Expression range, Expression lhs, Expression rhs, Attributes attributes, ExpressionTranslator etran, ExpressionTranslator prevEtran) { Contract.Requires(tok != null); Contract.Requires(boundVars != null); Contract.Requires(range != null); @@ -8130,159 +8081,27 @@ namespace Microsoft.Dafny { Type lhsType = lhs is MemberSelectExpr ? ((MemberSelectExpr)lhs).Type : null; g = CondApplyBox(rhs.tok, g, rhs.Type, lhsType); - Trigger tr = lhsAsTrigger ? new Trigger(tok, true, new List() { xHeapOF }) : null; - return new Bpl.ForallExpr(tok, xBvars, tr, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g))); - } - - class ForallStmtTranslationValues - { - public readonly Expression Range; - public readonly Expression FInverse; - public ForallStmtTranslationValues(Expression range, Expression fInverse) { - Contract.Requires(range != null); - Contract.Requires(fInverse != null); - Range = range; - FInverse = fInverse; - } - public ForallStmtTranslationValues Subst(IVariable j, Expression e, Translator translator) { - Contract.Requires(j != null); - Contract.Requires(e != null); - Contract.Requires(translator != null); - var substMap = new Dictionary(); - substMap.Add(j, e); - var v = new ForallStmtTranslationValues(translator.Substitute(Range, null, substMap), translator.Substitute(FInverse, null, substMap)); - return v; - } - } - - /// - /// Find piecewise inverse of F under R. More precisely, find lists of expressions P and F-1 - /// such that - /// R(i) && j == F(i) - /// holds iff the disjunction of the following predicates holds: - /// P_0(j) && F-1_0(j) == i - /// ... - /// P_{n-1}(j) && F-1_{n-1}(j) == i - /// If no such disjunction is found, return null. - /// If such a disjunction is found, return for each disjunct: - /// * The predicate P_k(j), which is an expression that may have free occurrences of j (but no free occurrences of i) - /// * The expression F-1_k(j), which also may have free occurrences of j but not of i - /// - private List InvertExpression(BoundVar i, BoundVar j, Expression R, Expression F) { - Contract.Requires(i != null); - Contract.Requires(j != null); - Contract.Requires(R != null); - Contract.Requires(F != null); - var vals = new List(InvertExpressionIter(i, j, R, F)); - if (vals.Count == 0) { - return null; - } else { - return vals; - } - } - /// - /// See InvertExpression. - /// - private IEnumerable InvertExpressionIter(BoundVar i, BoundVar j, Expression R, Expression F) { - Contract.Requires(i != null); - Contract.Requires(j != null); - Contract.Requires(R != null); - Contract.Requires(F != null); - F = F.Resolved; - if (!ContainsFreeVariable(F, false, i)) { - // We're looking at R(i) && j == K. - // We cannot invert j == K, but if we're lucky, R(i) contains a conjunct i==G. - Expression r = Expression.CreateBoolLiteral(R.tok, true); - Expression G = null; - foreach (var c in Expression.Conjuncts(R)) { - if (G == null && c is BinaryExpr) { - var bin = (BinaryExpr)c; - if (BinaryExpr.IsEqualityOp(bin.ResolvedOp)) { - var id = bin.E0.Resolved as IdentifierExpr; - if (id != null && id.Var == i) { - G = bin.E1; - continue; - } - id = bin.E1.Resolved as IdentifierExpr; - if (id != null && id.Var == i) { - G = bin.E0; - continue; - } + Bpl.Trigger tr = null; + var argsEtran = etran.WithNoLits(); + foreach (var aa in attributes.AsEnumerable()) { + if (aa.Name == "trigger") { + List tt = new List(); + foreach (var arg in aa.Args) { + if (arg == lhs) { + tt.Add(xHeapOF); + } else { + tt.Add(argsEtran.TrExpr(arg)); } } - r = Expression.CreateAnd(r, c); - } - if (G != null) { - var jIsK = Expression.CreateEq(Expression.CreateIdentExpr(j), F, j.Type); - var rr = Substitute(r, i, G); - yield return new ForallStmtTranslationValues(Expression.CreateAnd(rr, jIsK), G); - } - } else if (F is IdentifierExpr) { - var e = (IdentifierExpr)F; - if (e.Var == i) { - // We're looking at R(i) && j == i, which is particularly easy to invert: R(j) && j == i - var jj = Expression.CreateIdentExpr(j); - yield return new ForallStmtTranslationValues(Substitute(R, i, jj), jj); - } - } else if (F is BinaryExpr) { - var bin = (BinaryExpr)F; - if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Add && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) { - if (!ContainsFreeVariable(bin.E1, false, i)) { - // We're looking at: R(i) && j == f(i) + K. - // By a recursive call, we'll ask to invert: R(i) && j' == f(i). - // For each P_0(j') && f-1_0(j') == i we get back, we yield: - // P_0(j - K) && f-1_0(j - K) == i - var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E1); - foreach (var val in InvertExpression(i, j, R, bin.E0)) { - yield return val.Subst(j, jMinusK, this); - } - } else if (!ContainsFreeVariable(bin.E0, false, i)) { - // We're looking at: R(i) && j == K + f(i) - // Do as in previous case, but with operands reversed. - var jMinusK = Expression.CreateSubtract(Expression.CreateIdentExpr(j), bin.E0); - foreach (var val in InvertExpression(i, j, R, bin.E1)) { - yield return val.Subst(j, jMinusK, this); - } - } - } else if (bin.ResolvedOp == BinaryExpr.ResolvedOpcode.Sub && (bin.E0.Type.IsIntegerType || bin.E0.Type.IsRealType)) { - if (!ContainsFreeVariable(bin.E1, false, i)) { - // We're looking at: R(i) && j == f(i) - K - // Recurse on f(i) and then replace j := j + K - var jPlusK = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E1); - foreach (var val in InvertExpression(i, j, R, bin.E0)) { - yield return val.Subst(j, jPlusK, this); - } - } else if (!ContainsFreeVariable(bin.E0, false, i)) { - // We're looking at: R(i) && j == K - f(i) - // Recurse on f(i) and then replace j := K - j - var kMinusJ = Expression.CreateAdd(Expression.CreateIdentExpr(j), bin.E0); - foreach (var val in InvertExpression(i, j, R, bin.E1)) { - yield return val.Subst(j, kMinusJ, this); - } - } - } - } else if (F is ITEExpr) { - var ife = (ITEExpr)F; - // We're looking at R(i) && j == if A(i) then B(i) else C(i), which is equivalent to the disjunction of: - // R(i) && A(i) && j == B(i) - // R(i) && !A(i) && j == C(i) - // We recurse on each one, yielding the results - var r = Expression.CreateAnd(R, ife.Test); - var valsThen = InvertExpression(i, j, r, ife.Thn); - if (valsThen != null) { - r = Expression.CreateAnd(R, Expression.CreateNot(ife.tok, ife.Test)); - var valsElse = InvertExpression(i, j, r, ife.Els); - if (valsElse != null) { - foreach (var val in valsThen) { yield return val; } - foreach (var val in valsElse) { yield return val; } - } + tr = new Bpl.Trigger(tok, true, tt, tr); } } + return new Bpl.ForallExpr(tok, xBvars, tr, Bpl.Expr.Imp(xAnte, Bpl.Expr.Eq(xHeapOF, g))); } delegate Bpl.Expr ExpressionConverter(Dictionary substMap, ExpressionTranslator etran); - void TrForallStmtCall(IToken tok, List boundVars, Expression range, ExpressionConverter additionalRange, CallStmt s0, + void TrForallStmtCall(IToken tok, List boundVars, Expression range, ExpressionConverter additionalRange, List forallExpressions, CallStmt s0, Bpl.StmtListBuilder definedness, Bpl.StmtListBuilder exporter, List locals, ExpressionTranslator etran) { Contract.Requires(tok != null); Contract.Requires(boundVars != null); @@ -8365,38 +8184,56 @@ namespace Microsoft.Dafny { RecordNewObjectsIn_New(tok, iter, initHeap, heapIdExpr, exporter, locals, etran); } - var bvars = new List(); - Dictionary substMap; - var ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap); - ante = BplAnd(ante, initEtran.TrExpr(Substitute(range, null, substMap))); - if (additionalRange != null) { - ante = BplAnd(ante, additionalRange(substMap, initEtran)); - } - // Note, in the following, we need to do a bit of a song and dance. The actual arguments of the // call should be translated using "initEtran", whereas the method postcondition should be translated // using "callEtran". To accomplish this, we translate the argument and then tuck the resulting // Boogie expressions into BoogieExprWrappers that are used in the DafnyExpr-to-DafnyExpr substitution. - // TODO - 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++) { - var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the renamed bound variables for the declared ones - argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type)); - } - var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type); - var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap); - Bpl.Expr post = Bpl.Expr.True; - foreach (var ens in s0.Method.Ens) { - var p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals - post = BplAnd(post, callEtran.TrExpr(p)); - } - - // TRIG (forall $ih#s0#0: Seq Box :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char))) - // TRIG (forall $ih#pat0#0: Seq Box, $ih#a0#0: Seq Box :: $Is($ih#pat0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#pat0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && $Is($ih#a0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#a0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && Seq#Length($ih#pat0#0) <= Seq#Length($ih#a0#0) && Seq#SameUntil($ih#pat0#0, $ih#a0#0, Seq#Length($ih#pat0#0)) && (Seq#Rank($ih#pat0#0) < Seq#Rank(pat#0) || (Seq#Rank($ih#pat0#0) == Seq#Rank(pat#0) && Seq#Rank($ih#a0#0) < Seq#Rank(a#0))) ==> _module.__default.IsRelaxedPrefixAux(_module._default.Same0$T, $LS($LZ), $Heap, $ih#pat0#0, $ih#a0#0, LitInt(1)))' - // TRIG (forall $ih#m0#0: DatatypeType, $ih#n0#0: DatatypeType :: $Is($ih#m0#0, Tclass._module.Nat()) && $IsAlloc($ih#m0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && $Is($ih#n0#0, Tclass._module.Nat()) && $IsAlloc($ih#n0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && Lit(true) && (DtRank($ih#m0#0) < DtRank(m#0) || (DtRank($ih#m0#0) == DtRank(m#0) && DtRank($ih#n0#0) < DtRank(n#0))) ==> _module.__default.mult($LS($LZ), $Heap, $ih#m0#0, _module.__default.plus($LS($LZ), $Heap, $ih#n0#0, $ih#n0#0)) == _module.__default.mult($LS($LZ), $Heap, _module.__default.plus($LS($LZ), $Heap, $ih#m0#0, $ih#m0#0), $ih#n0#0)) - Bpl.Expr qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post)); // SMART_TRIGGER - exporter.Add(new Bpl.AssumeCmd(tok, qq)); + // TODO + Bpl.Expr qq; + if (forallExpressions != null) { + var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap); + foreach (Expression expr in forallExpressions) { + Dictionary substMap = new Dictionary(); + var e = Substitute(expr, null, substMap, null); + var argsSubstMap = new Dictionary(); + Contract.Assert(s0.Method.Ins.Count == s0.Args.Count); + for (int i = 0; i < s0.Method.Ins.Count; i++) { + var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the renamed bound variables for the declared ones + argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type)); + } + var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type); + var p = Substitute(e, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals + qq = callEtran.TrExpr(p, initEtran); + exporter.Add(new Bpl.AssumeCmd(tok, qq)); + } + } else { + var bvars = new List(); + Dictionary substMap; + var ante = initEtran.TrBoundVariablesRename(boundVars, bvars, out substMap); + 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++) { + var arg = Substitute(s0.Args[i], null, substMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the renamed bound variables for the declared ones + argsSubstMap.Add(s0.Method.Ins[i], new BoogieWrapper(initEtran.TrExpr(arg), s0.Args[i].Type)); + } + var callEtran = new ExpressionTranslator(this, predef, etran.HeapExpr, initHeap); + ante = BplAnd(ante, initEtran.TrExpr(Substitute(range, null, substMap))); + if (additionalRange != null) { + ante = BplAnd(ante, additionalRange(substMap, initEtran)); + } + var receiver = new BoogieWrapper(initEtran.TrExpr(Substitute(s0.Receiver, null, substMap, s0.MethodSelect.TypeArgumentSubstitutions())), s0.Receiver.Type); + Bpl.Expr post = Bpl.Expr.True; + foreach (var ens in s0.Method.Ens) { + var p = Substitute(ens.E, receiver, argsSubstMap, s0.MethodSelect.TypeArgumentSubstitutions()); // substitute the call's actuals for the method's formals + post = BplAnd(post, callEtran.TrExpr(p)); + } + + // TRIG (forall $ih#s0#0: Seq Box :: $Is($ih#s0#0, TSeq(TChar)) && $IsAlloc($ih#s0#0, TSeq(TChar), $initHeapForallStmt#0) && Seq#Length($ih#s0#0) != 0 && Seq#Rank($ih#s0#0) < Seq#Rank(s#0) ==> (forall i#2: int :: true ==> LitInt(0) <= i#2 && i#2 < Seq#Length($ih#s0#0) ==> char#ToInt(_module.CharChar.MinChar($LS($LZ), $Heap, this, $ih#s0#0)) <= char#ToInt($Unbox(Seq#Index($ih#s0#0, i#2)): char))) + // TRIG (forall $ih#pat0#0: Seq Box, $ih#a0#0: Seq Box :: $Is($ih#pat0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#pat0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && $Is($ih#a0#0, TSeq(_module._default.Same0$T)) && $IsAlloc($ih#a0#0, TSeq(_module._default.Same0$T), $initHeapForallStmt#0) && Seq#Length($ih#pat0#0) <= Seq#Length($ih#a0#0) && Seq#SameUntil($ih#pat0#0, $ih#a0#0, Seq#Length($ih#pat0#0)) && (Seq#Rank($ih#pat0#0) < Seq#Rank(pat#0) || (Seq#Rank($ih#pat0#0) == Seq#Rank(pat#0) && Seq#Rank($ih#a0#0) < Seq#Rank(a#0))) ==> _module.__default.IsRelaxedPrefixAux(_module._default.Same0$T, $LS($LZ), $Heap, $ih#pat0#0, $ih#a0#0, LitInt(1)))' + // TRIG (forall $ih#m0#0: DatatypeType, $ih#n0#0: DatatypeType :: $Is($ih#m0#0, Tclass._module.Nat()) && $IsAlloc($ih#m0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && $Is($ih#n0#0, Tclass._module.Nat()) && $IsAlloc($ih#n0#0, Tclass._module.Nat(), $initHeapForallStmt#0) && Lit(true) && (DtRank($ih#m0#0) < DtRank(m#0) || (DtRank($ih#m0#0) == DtRank(m#0) && DtRank($ih#n0#0) < DtRank(n#0))) ==> _module.__default.mult($LS($LZ), $Heap, $ih#m0#0, _module.__default.plus($LS($LZ), $Heap, $ih#n0#0, $ih#n0#0)) == _module.__default.mult($LS($LZ), $Heap, _module.__default.plus($LS($LZ), $Heap, $ih#m0#0, $ih#m0#0), $ih#n0#0)) + qq = new Bpl.ForallExpr(tok, bvars, Bpl.Expr.Imp(ante, post)); // SMART_TRIGGER + exporter.Add(new Bpl.AssumeCmd(tok, qq)); + } } } @@ -8501,24 +8338,14 @@ namespace Microsoft.Dafny { } } - var bvars = new List(); - Dictionary substMap; - var ante = initEtran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap); - var range = Substitute(s.Range, null, substMap); - ante = BplAnd(ante, initEtran.TrExpr(range)); - - Bpl.Expr post = Bpl.Expr.True; - foreach (var ens in s.Ens) { - var p = Substitute(ens.E, null, substMap); - post = BplAnd(post, etran.TrExpr(p)); - } - - Bpl.Expr qq = Bpl.Expr.Imp(ante, post); - if (bvars.Count != 0) { - var triggers = TrTrigger(etran, s.Attributes, s.Tok, substMap); - qq = new Bpl.ForallExpr(s.Tok, bvars, triggers, qq); + Dictionary substMap = new Dictionary(); + var p = Substitute(s.ForallExpressions[0], null, substMap); + Bpl.Expr qq = etran.TrExpr(p, initEtran); + if (s.BoundVars.Count != 0) { + exporter.Add(new Bpl.AssumeCmd(s.Tok, qq)); + } else { + exporter.Add(new Bpl.AssumeCmd(s.Tok, ((Bpl.ForallExpr)qq).Body)); } - exporter.Add(new Bpl.AssumeCmd(s.Tok, qq)); } private string GetObjFieldDetails(Expression lhs, ExpressionTranslator etran, out Bpl.Expr obj, out Bpl.Expr F) { @@ -10868,7 +10695,10 @@ namespace Microsoft.Dafny { /// filled in, but it is really necessary for anything that may show up in a Boogie assert, since that location may /// then show up in an error message). /// - public Bpl.Expr TrExpr(Expression expr) + public Bpl.Expr TrExpr(Expression expr) { + return TrExpr(expr, null); + } + public Bpl.Expr TrExpr(Expression expr, ExpressionTranslator etran) { Contract.Requires(expr != null); Contract.Requires(predef != null); @@ -11683,7 +11513,7 @@ namespace Microsoft.Dafny { List tyvars = translator.MkTyParamBinders(e.TypeArgs); List bvars = new List(); - var initEtran = this; + var initEtran = (etran == null) ? this : etran; var bodyEtran = this; bool _scratch = true; @@ -11704,7 +11534,7 @@ namespace Microsoft.Dafny { }); } - antecedent = BplAnd(antecedent, bodyEtran.TrBoundVariables(e.BoundVars, bvars)); + antecedent = BplAnd(antecedent, initEtran.TrBoundVariables(e.BoundVars, bvars)); Bpl.QKeyValue kv = TrAttributes(e.Attributes, "trigger"); Bpl.Trigger tr = null; @@ -11719,7 +11549,7 @@ namespace Microsoft.Dafny { } } if (e.Range != null) { - antecedent = BplAnd(antecedent, bodyEtran.TrExpr(e.Range)); + antecedent = BplAnd(antecedent, initEtran.TrExpr(e.Range)); } Bpl.Expr body = bodyEtran.TrExpr(e.Term); diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index 865aa33e..e46b64fb 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -114,6 +114,18 @@ namespace Microsoft.Dafny.Triggers { } } + protected override void VisitOneStmt(Statement stmt) { + Contract.Requires(stmt != null); + if (stmt is ForallStmt) { + ForallStmt s = (ForallStmt)stmt; + if (s.ForallExpressions != null) { + foreach (Expression expr in s.ForallExpressions) { + VisitOneExpr(expr); + } + } + } + } + /// /// See comments above definition of splits for reason why this method exists /// diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs index 1f37dcfa..789e7614 100644 --- a/Source/Dafny/Triggers/QuantifiersCollector.cs +++ b/Source/Dafny/Triggers/QuantifiersCollector.cs @@ -40,5 +40,18 @@ namespace Microsoft.Dafny.Triggers { return true; } + + protected override bool VisitOneStmt(Statement stmt, ref bool st) { + Contract.Requires(stmt != null); + if (stmt is ForallStmt) { + ForallStmt s = (ForallStmt)stmt; + if (s.ForallExpressions != null) { + foreach (Expression expr in s.ForallExpressions) { + VisitOneExpr(expr, ref st); + } + } + } + return true; + } } } diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect index 4bd12096..6161c3dd 100644 --- a/Test/dafny0/SmallTests.dfy.expect +++ b/Test/dafny0/SmallTests.dfy.expect @@ -1,3 +1,4 @@ +SmallTests.dfy(507,4): Warning: /!\ No trigger covering all quantified variables found. SmallTests.dfy(34,10): Error: index out of range Execution trace: (0,0): anon0 diff --git a/Test/dafny4/Bug103.dfy b/Test/dafny4/Bug103.dfy new file mode 100644 index 00000000..559a361c --- /dev/null +++ b/Test/dafny4/Bug103.dfy @@ -0,0 +1,20 @@ +// RUN: %dafny /compile:0 /autoTriggers:1 /print:"%t.print" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +predicate IsLessThanSuccesor(i:int) +{ + i < i + 1 +} + +lemma LemmaWithoutTriggerOnForallStatement() +{ + forall i + ensures IsLessThanSuccesor(i); + { + } +} + + + + + diff --git a/Test/dafny4/Bug103.dfy.expect b/Test/dafny4/Bug103.dfy.expect new file mode 100644 index 00000000..52595bf9 --- /dev/null +++ b/Test/dafny4/Bug103.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 3 verified, 0 errors -- cgit v1.2.3 From 4c81e90e18b1d142c50453470fe9647693ef8de4 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 6 Jan 2016 19:00:18 -0800 Subject: Removed Contract.Requires from method overrides (preconditions of overrides are inherited from the overridden method and Code Contracts will copy those preconditions to make sure the right run-time checking happens; when Code Contracts finds preconditions on overrides, it emits warnings). --- Source/Dafny/Rewriter.cs | 1 - Source/Dafny/Triggers/QuantifierSplitter.cs | 1 - Source/Dafny/Triggers/QuantifiersCollector.cs | 1 - 3 files changed, 3 deletions(-) (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 13b16066..2e18c4e6 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -89,7 +89,6 @@ namespace Microsoft.Dafny internal class ForAllStmtVisitor : TopDownVisitor { protected override bool VisitOneStmt(Statement stmt, ref bool st) { - Contract.Requires(stmt != null); if (stmt is ForallStmt) { ForallStmt s = (ForallStmt)stmt; if (s.Kind == ForallStmt.ParBodyKind.Proof) { diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index e46b64fb..d0b2b430 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -115,7 +115,6 @@ namespace Microsoft.Dafny.Triggers { } protected override void VisitOneStmt(Statement stmt) { - Contract.Requires(stmt != null); if (stmt is ForallStmt) { ForallStmt s = (ForallStmt)stmt; if (s.ForallExpressions != null) { diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs index 789e7614..b887435b 100644 --- a/Source/Dafny/Triggers/QuantifiersCollector.cs +++ b/Source/Dafny/Triggers/QuantifiersCollector.cs @@ -42,7 +42,6 @@ namespace Microsoft.Dafny.Triggers { } protected override bool VisitOneStmt(Statement stmt, ref bool st) { - Contract.Requires(stmt != null); if (stmt is ForallStmt) { ForallStmt s = (ForallStmt)stmt; if (s.ForallExpressions != null) { -- cgit v1.2.3 From 436966ef61a3e4330bbe705d0d0319fcde5f3099 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 25 Jan 2016 11:30:02 -0800 Subject: Fix issue 121. Don't split QuantifierExpr that are empty. --- Source/Dafny/Triggers/QuantifierSplitter.cs | 5 +++-- Test/dafny4/Bug121.dfy | 18 ++++++++++++++++++ Test/dafny4/Bug121.dfy.expect | 2 ++ 3 files changed, 23 insertions(+), 2 deletions(-) create mode 100644 Test/dafny4/Bug121.dfy create mode 100644 Test/dafny4/Bug121.dfy.expect (limited to 'Source/Dafny/Triggers/QuantifierSplitter.cs') diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs index d0b2b430..b039a402 100644 --- a/Source/Dafny/Triggers/QuantifierSplitter.cs +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -100,8 +100,9 @@ namespace Microsoft.Dafny.Triggers { } private static bool AllowsSplitting(QuantifierExpr quantifier) { - bool splitAttr = true; - return !Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr; + // allow split if attributes doesn't contains "split" or it is "split: true" and it is not an empty QuantifierExpr (boundvar.count>0) + bool splitAttr = true; + return (!Attributes.ContainsBool(quantifier.Attributes, "split", ref splitAttr) || splitAttr) && (quantifier.BoundVars.Count > 0); } protected override void VisitOneExpr(Expression expr) { diff --git a/Test/dafny4/Bug121.dfy b/Test/dafny4/Bug121.dfy new file mode 100644 index 00000000..13798fa8 --- /dev/null +++ b/Test/dafny4/Bug121.dfy @@ -0,0 +1,18 @@ +// RUN: %dafny /compile:0 /autoTriggers:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +method Try (a:int, b:int, c:int) +{ + forall + ensures a * c == a * c; + ensures b * c == b * c; + { + } +} + + + + + + + diff --git a/Test/dafny4/Bug121.dfy.expect b/Test/dafny4/Bug121.dfy.expect new file mode 100644 index 00000000..069e7767 --- /dev/null +++ b/Test/dafny4/Bug121.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 2 verified, 0 errors -- cgit v1.2.3