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/TriggersCollector.cs | 256 +++++++++++++++++++++++++++++ 1 file changed, 256 insertions(+) create mode 100644 Source/Dafny/Triggers/TriggersCollector.cs (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs new file mode 100644 index 00000000..912a661c --- /dev/null +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -0,0 +1,256 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using Microsoft.Boogie; +using System.Diagnostics.Contracts; +using System.Diagnostics; + +namespace Microsoft.Dafny.Triggers { + struct TriggerCandidate { + internal Expression Expr { get; set; } + internal ISet Variables { get; set; } + + public override string ToString() { + return Printer.ExprToString(Expr); + } + } + + class MultiTriggerCandidate { + internal List terms { get; set; } + + internal MultiTriggerCandidate(List candidates) { + this.terms = candidates; + } + + internal bool MentionsAll(List vars) { + return vars.All(x => terms.Any(candidate => candidate.Variables.Contains(x))); + } + + public override string ToString() { + return String.Join(", ", terms); + } + + 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; + } + } + + class TriggerAnnotation { + internal bool IsTriggerKiller; + internal ISet Variables; + internal readonly List PrivateTerms; + internal readonly List ExportedTerms; + + internal TriggerAnnotation(bool IsTriggerKiller, IEnumerable Variables, + IEnumerable AllCandidates, IEnumerable PrivateCandidates = 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)); + } + + public override string ToString() { + StringBuilder sb = new StringBuilder(); + string indent = " {0}", nindent = "\n - {0}", subindent = "\n * {0}"; + + sb.AppendFormat(indent, IsTriggerKiller); + + sb.AppendFormat(nindent, "Variables:"); + foreach (var bv in Variables) { + sb.AppendFormat(subindent, bv.Name); + } + + sb.AppendFormat(nindent, "Exported candidates:"); + foreach (var candidate in ExportedTerms) { + sb.AppendFormat(subindent, candidate); + } + + if (PrivateTerms.Any()) { + sb.AppendFormat(nindent, "Private candidates:"); + foreach (var candidate in PrivateTerms) { + sb.AppendFormat(subindent, candidate); + } + } + + return sb.ToString(); + } + } + + public class TriggersCollector { + Dictionary cache; + + private static TriggersCollector instance = new TriggersCollector(); + + private TriggersCollector() { + this.cache = new Dictionary(); + } + + private T ReduceAnnotatedSubExpressions(Expression expr, T seed, Func map, Func reduce) { + return expr.SubExpressions.Select(e => map(Annotate(e))) + .Aggregate(seed, (acc, e) => reduce(acc, e)); + } + + private List CollectExportedCandidates(Expression expr) { + return ReduceAnnotatedSubExpressions>(expr, new List(), a => a.ExportedTerms, TriggerUtils.MergeAlterFirst); + } + + private ISet CollectVariables(Expression expr) { + return ReduceAnnotatedSubExpressions(expr, new HashSet(), a => a.Variables, TriggerUtils.MergeAlterFirst); + } + + private bool CollectIsKiller(Expression expr) { + 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 TriggerAnnotation Annotate(Expression expr) { + TriggerAnnotation cached; + if (cache.TryGetValue(expr, out cached)) { + return cached; + } + + expr.SubExpressions.Iter(e => Annotate(e)); + + TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort + if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MemberSelectExpr || expr is OldExpr || + (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) { + annotation = AnnotateQuantifier((QuantifierExpr)expr); + } else if (expr is LetExpr) { + annotation = AnnotateLetExpr((LetExpr)expr); + } else if (expr is IdentifierExpr) { + annotation = AnnotateIdentifier((IdentifierExpr)expr); + } else if (expr is ApplySuffix) { + annotation = AnnotateApplySuffix((ApplySuffix)expr); + } else if (expr is ConcreteSyntaxExpression || + expr is LiteralExpr || + expr is OldExpr || + expr is ThisExpr || + expr is BoxingCastExpr || + expr is DatatypeValue || + expr is SeqDisplayExpr) { //FIXME what abvout other display expressions? + annotation = AnnotateOther(expr, false); + } else { + annotation = AnnotateOther(expr, true); + } + + TriggerUtils.DebugTriggers("{0} ({1})\n{2}", Printer.ExprToString(expr), expr.GetType(), annotation); + cache[expr] = annotation; + return annotation; + } + + private BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) { + switch (opcode) { + case BinaryExpr.ResolvedOpcode.NotInMap: + return BinaryExpr.ResolvedOpcode.InMap; + case BinaryExpr.ResolvedOpcode.NotInSet: + return BinaryExpr.ResolvedOpcode.InSet; + case BinaryExpr.ResolvedOpcode.NotInSeq: + return BinaryExpr.ResolvedOpcode.InSeq; + case BinaryExpr.ResolvedOpcode.NotInMultiSet: + return BinaryExpr.ResolvedOpcode.InMultiSet; + } + + Contract.Assert(false); + throw new ArgumentException(); + } + + private Expression CleanupExpr(Expression expr, out bool isKiller) { + isKiller = false; + + if (!(expr is BinaryExpr)) { + return expr; + } + + var bexpr = expr as BinaryExpr; + + BinaryExpr new_expr = bexpr; + if (bexpr.Op == BinaryExpr.Opcode.NotIn) { + new_expr = new BinaryExpr(bexpr.tok, BinaryExpr.Opcode.In, bexpr.E0, bexpr.E1); + new_expr.ResolvedOp = RemoveNotInBinaryExprIn(bexpr.ResolvedOp); + new_expr.Type = bexpr.Type; + } + + Expression returned_expr = new_expr; + if (new_expr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) { + returned_expr = new SeqSelectExpr(new_expr.tok, true, new_expr.E1, new_expr.E0, null); + returned_expr.Type = bexpr.Type; + isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer + } + + return returned_expr; + } + + 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) }; + + List collected_candidates = 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); + } + + // 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); + } + + private TriggerAnnotation AnnotateApplySuffix(ApplySuffix expr) { + // This is a bit tricky. A funcall node is generally meaningful as a trigger candidate, + // but when it's part of an ApplySuffix the function call itself may not resolve properly + // when the second round of resolving is done after modules are duplicated. + // Thus first we annotate expr and create a trigger candidate, and then we remove the + // candidate matching its direct subexpression if needed. Note that function calls are not the + // 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)); + return annotation; + } + + private TriggerAnnotation AnnotateQuantifierOrLetExpr(Expression expr, IEnumerable boundVars) { + var candidates = CollectExportedCandidates(expr); + return new TriggerAnnotation(true, CollectVariables(expr), candidates, OnlyPrivateCandidates(candidates, boundVars)); + } + + private TriggerAnnotation AnnotateQuantifier(QuantifierExpr expr) { + return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars); + } + + private TriggerAnnotation AnnotateLetExpr(LetExpr expr) { + return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars); + } + + private TriggerAnnotation AnnotateIdentifier(IdentifierExpr expr) { + return new TriggerAnnotation(false, Enumerable.Repeat(expr.Var, 1), null); + } + + private TriggerAnnotation AnnotateOther(Expression expr, bool isTriggerKiller) { + return new TriggerAnnotation(isTriggerKiller || CollectIsKiller(expr), CollectVariables(expr), CollectExportedCandidates(expr)); + } + + // FIXME document that this will contain duplicates + internal static 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; + } + + internal static bool IsTriggerKiller(Expression expr) { + return instance.Annotate(expr).IsTriggerKiller; + } + } +} -- 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/TriggersCollector.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/TriggersCollector.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 108e634af783601c60555c2e8e75775c3b4041ed Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Tue, 18 Aug 2015 08:47:40 -0700 Subject: Small cleanups, fixes, and refactorings In particular, start detecting loops between terms that don't look like each other at the Dafny level, such as {a[x]} and {x in a} (when a is a multiset) --- Source/Dafny/DafnyPipeline.csproj | 2 +- Source/Dafny/Rewriter.cs | 2 +- Source/Dafny/Triggers/QuantifiersCollection.cs | 8 ++-- Source/Dafny/Triggers/QuantifiersCollector.cs | 33 +++++++++++++++ Source/Dafny/Triggers/TriggerExtensions.cs | 15 ++++--- Source/Dafny/Triggers/TriggerGenerator.cs | 32 --------------- Source/Dafny/Triggers/TriggerUtils.cs | 56 ++++++++++++++++++++++++- Source/Dafny/Triggers/TriggersCollector.cs | 57 ++++---------------------- 8 files changed, 111 insertions(+), 94 deletions(-) create mode 100644 Source/Dafny/Triggers/QuantifiersCollector.cs delete mode 100644 Source/Dafny/Triggers/TriggerGenerator.cs (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj index 5a824c36..13a1e53e 100644 --- a/Source/Dafny/DafnyPipeline.csproj +++ b/Source/Dafny/DafnyPipeline.csproj @@ -147,7 +147,7 @@ - + diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 2c00e203..b6409b96 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -44,7 +44,7 @@ namespace Microsoft.Dafny } internal override void PostCyclicityResolve(ModuleDefinition m) { - var finder = new Triggers.QuantifierCollectionsFinder(reporter); + var finder = new Triggers.QuantifierCollector(reporter); foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { if (decl is Function) { diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index cbc212d2..01bceeb7 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -17,7 +17,7 @@ namespace Microsoft.Dafny.Triggers { internal List Candidates; internal List RejectedCandidates; - internal bool AllowsLoops { get { return quantifier.Attributes.AsEnumerable().Any(a => a.Name == "loop"); } } + internal bool AllowsLoops { get { return TriggerUtils.AllowsMatchingLoops(quantifier); } } internal bool CouldSuppressLoops { get; set; } internal QuantifierWithTriggers(QuantifierExpr quantifier) { @@ -65,8 +65,8 @@ namespace Microsoft.Dafny.Triggers { var multiPool = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate).Select(candidates => new TriggerCandidate(candidates)).ToList(); foreach (var q in quantifiers) { - q.CandidateTerms = distinctPool; - q.Candidates = multiPool; + q.CandidateTerms = distinctPool; //Candidate terms are immutable: no copy needed + q.Candidates = multiPool.Select(candidate => new TriggerCandidate(candidate)).ToList(); } } @@ -116,7 +116,7 @@ namespace Microsoft.Dafny.Triggers { c => !loopingSubterms[c].Any(), c => { looping.Add(c); - c.Annotation = "loop with " + loopingSubterms[c].MapConcat(t => Printer.ExprToString(t.Expr), ", "); + c.Annotation = "loops with " + loopingSubterms[c].MapConcat(t => Printer.ExprToString(t.Expr), ", "); }).ToList(); q.CouldSuppressLoops = safe.Count > 0; diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs new file mode 100644 index 00000000..a43aae7a --- /dev/null +++ b/Source/Dafny/Triggers/QuantifiersCollector.cs @@ -0,0 +1,33 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using Microsoft.Boogie; +using System.Collections.ObjectModel; +using System.Diagnostics.Contracts; + +namespace Microsoft.Dafny.Triggers { //FIXME rename this file + internal class QuantifierCollector : TopDownVisitor { + readonly ErrorReporter reporter; + internal List quantifierCollections = new List(); + + public QuantifierCollector(ErrorReporter reporter) { + Contract.Requires(reporter != null); + this.reporter = reporter; + } + + protected override bool VisitOneExpr(Expression expr, ref object st) { + var quantifier = expr as QuantifierExpr; + if (quantifier != null) { + if (quantifier.SplitQuantifier != null) { + var collection = quantifier.SplitQuantifier.Select(q => q as QuantifierExpr).Where(q => q != null); + quantifierCollections.Add(new QuantifiersCollection(collection, reporter)); + return false; + } else { + quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter)); + } + } + return true; + } + } +} diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index 9fbc8a8a..0a0ad547 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -110,14 +110,18 @@ namespace Microsoft.Dafny.Triggers { return ShallowEq_Top(expr, trigger) && TriggerUtils.SameLists(expr.SubExpressions, trigger.SubExpressions, (e1, e2) => MatchesTrigger(e1, e2, holes, bindings)); } - private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, ISet holes) { + private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, IEnumerable holes) { var bindings = new Dictionary(); - return expr.MatchesTrigger(trigger, holes, bindings) ? new TriggerMatch { Expr = expr, Bindings = bindings } : (TriggerMatch?)null; + if (expr.MatchesTrigger(trigger, new HashSet(holes), bindings)) { + return new TriggerMatch { Expr = expr, Bindings = bindings }; + } else { + return null; + } } internal static IEnumerable SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) { return quantifier.Term.AllSubExpressions() - .Select(e => e.MatchAgainst(trigger, new HashSet(quantifier.BoundVars))) + .Select(e => TriggerUtils.CleanupExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars)) .Where(e => e.HasValue).Select(e => e.Value); } @@ -136,7 +140,8 @@ namespace Microsoft.Dafny.Triggers { arg1.DisplayName == arg2.DisplayName && arg1.UniqueName == arg2.UniqueName && arg1.IsGhost == arg2.IsGhost && - arg1.IsMutable == arg2.IsMutable); //FIXME compare types? + arg1.IsMutable == arg2.IsMutable && + ((arg1.Type == null && arg2.Type == null) || arg1.Type.Equals(arg2.Type))); } /// @@ -271,7 +276,7 @@ namespace Microsoft.Dafny.Triggers { return true; } - private static bool ShallowEq(QuantifierExpr expr1, QuantifierExpr expr2) { //FIXME are these TypeArgs still useful? + private static bool ShallowEq(QuantifierExpr expr1, QuantifierExpr expr2) { if (!TriggerUtils.SameNullity(expr1.SplitQuantifier, expr2.SplitQuantifier)) { return false; } diff --git a/Source/Dafny/Triggers/TriggerGenerator.cs b/Source/Dafny/Triggers/TriggerGenerator.cs deleted file mode 100644 index e218ad7b..00000000 --- a/Source/Dafny/Triggers/TriggerGenerator.cs +++ /dev/null @@ -1,32 +0,0 @@ -using System; -using System.Collections.Generic; -using System.Linq; -using System.Text; -using Microsoft.Boogie; -using System.Collections.ObjectModel; -using System.Diagnostics.Contracts; - -namespace Microsoft.Dafny.Triggers { //FIXME rename this file - internal class QuantifierCollectionsFinder : TopDownVisitor { - readonly ErrorReporter reporter; - internal List quantifierCollections = new List(); - - public QuantifierCollectionsFinder(ErrorReporter reporter) { - Contract.Requires(reporter != null); - this.reporter = reporter; - } - - protected override bool VisitOneExpr(Expression expr, ref object st) { - var quantifier = expr as QuantifierExpr; - if (quantifier != null) { - 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 6c6eede2..9ebcf846 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -100,9 +100,63 @@ namespace Microsoft.Dafny.Triggers { Console.Error.WriteLine(format, more); } + internal static bool AllowsMatchingLoops(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 Attributes.Contains(quantifier.Attributes, "matchingloop"); + } + 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"); + bool wantsAutoTriggers = true; + return !Attributes.Contains(quantifier.Attributes, "trigger") && + (!Attributes.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers); + } + + internal static BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) { + switch (opcode) { + case BinaryExpr.ResolvedOpcode.NotInMap: + return BinaryExpr.ResolvedOpcode.InMap; + case BinaryExpr.ResolvedOpcode.NotInSet: + return BinaryExpr.ResolvedOpcode.InSet; + case BinaryExpr.ResolvedOpcode.NotInSeq: + return BinaryExpr.ResolvedOpcode.InSeq; + case BinaryExpr.ResolvedOpcode.NotInMultiSet: + return BinaryExpr.ResolvedOpcode.InMultiSet; + } + + Contract.Assert(false); + throw new ArgumentException(); + } + + internal static Expression CleanupExprForInclusionInTrigger(Expression expr, out bool isKiller) { + isKiller = false; + + if (!(expr is BinaryExpr)) { + return expr; + } + + var bexpr = expr as BinaryExpr; + + BinaryExpr new_expr = bexpr; + if (bexpr.Op == BinaryExpr.Opcode.NotIn) { + new_expr = new BinaryExpr(bexpr.tok, BinaryExpr.Opcode.In, bexpr.E0, bexpr.E1); + new_expr.ResolvedOp = RemoveNotInBinaryExprIn(bexpr.ResolvedOp); + new_expr.Type = bexpr.Type; + } + + Expression returned_expr = new_expr; + if (new_expr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) { + returned_expr = new SeqSelectExpr(new_expr.tok, true, new_expr.E1, new_expr.E0, null); + returned_expr.Type = bexpr.Type; + isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer + } + + return returned_expr; + } + + internal static Expression CleanupExprForInclusionInTrigger(Expression expr) { + bool _; + return CleanupExprForInclusionInTrigger(expr, out _); } } } diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 9f721d9a..221a4255 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -9,10 +9,11 @@ using System.Diagnostics; namespace Microsoft.Dafny.Triggers { class TriggerTerm { internal Expression Expr { get; set; } + internal Expression OriginalExpr { get; set; } internal ISet Variables { get; set; } public override string ToString() { - return Printer.ExprToString(Expr); + return Printer.ExprToString(OriginalExpr); } internal static bool Eq(TriggerTerm t1, TriggerTerm t2) { @@ -28,16 +29,15 @@ namespace Microsoft.Dafny.Triggers { this.Terms = terms; } - public TriggerCandidate(TriggerCandidate mc, string annotation) { - this.Terms = mc.Terms; - this.Annotation = annotation; + public TriggerCandidate(TriggerCandidate candidate) { + this.Terms = candidate.Terms; } internal bool MentionsAll(List vars) { return vars.All(x => Terms.Any(term => term.Variables.Contains(x))); } - private string Repr { get { return Terms.MapConcat(t => Printer.ExprToString(t.Expr), ", "); } } + private string Repr { get { return String.Join(", ", Terms); } } public override string ToString() { return "{" + Repr + "}" + (String.IsNullOrWhiteSpace(Annotation) ? "" : " (" + Annotation + ")"); @@ -51,7 +51,6 @@ namespace Microsoft.Dafny.Triggers { 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); } @@ -166,52 +165,10 @@ namespace Microsoft.Dafny.Triggers { return annotation; } - private BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) { - switch (opcode) { - case BinaryExpr.ResolvedOpcode.NotInMap: - return BinaryExpr.ResolvedOpcode.InMap; - case BinaryExpr.ResolvedOpcode.NotInSet: - return BinaryExpr.ResolvedOpcode.InSet; - case BinaryExpr.ResolvedOpcode.NotInSeq: - return BinaryExpr.ResolvedOpcode.InSeq; - case BinaryExpr.ResolvedOpcode.NotInMultiSet: - return BinaryExpr.ResolvedOpcode.InMultiSet; - } - - Contract.Assert(false); - throw new ArgumentException(); - } - - private Expression CleanupExpr(Expression expr, out bool isKiller) { - isKiller = false; - - if (!(expr is BinaryExpr)) { - return expr; - } - - var bexpr = expr as BinaryExpr; - - BinaryExpr new_expr = bexpr; - if (bexpr.Op == BinaryExpr.Opcode.NotIn) { - new_expr = new BinaryExpr(bexpr.tok, BinaryExpr.Opcode.In, bexpr.E0, bexpr.E1); - new_expr.ResolvedOp = RemoveNotInBinaryExprIn(bexpr.ResolvedOp); - new_expr.Type = bexpr.Type; - } - - Expression returned_expr = new_expr; - if (new_expr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) { - returned_expr = new SeqSelectExpr(new_expr.tok, true, new_expr.E1, new_expr.E0, null); - returned_expr.Type = bexpr.Type; - isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer - } - - return returned_expr; - } - private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) { bool expr_is_killer = false; - var new_expr = CleanupExpr(expr, out expr_is_killer); - var new_term = new TriggerTerm { Expr = new_expr, Variables = CollectVariables(expr) }; + var new_expr = TriggerUtils.CleanupExprForInclusionInTrigger(expr, out expr_is_killer); + var new_term = new TriggerTerm { Expr = new_expr, OriginalExpr = expr, Variables = CollectVariables(expr) }; List collected_terms = CollectExportedCandidates(expr); var children_contain_killers = CollectIsKiller(expr); -- cgit v1.2.3 From 8b40a61b3e0dd5c8154cd2095a2fa813e0d7c9c5 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 15:48:32 -0700 Subject: Collect ApplyExpr nodes when looking for trigger candidates --- Source/Dafny/Triggers/TriggersCollector.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 221a4255..08d33af6 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -136,7 +136,7 @@ namespace Microsoft.Dafny.Triggers { expr.SubExpressions.Iter(e => Annotate(e)); TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort - if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MemberSelectExpr || expr is OldExpr || + if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MemberSelectExpr || expr is OldExpr || expr is ApplyExpr || (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); -- cgit v1.2.3 From dd4f127f36ec24fbcedaaae0e61e0894b2bf5e83 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 22:14:56 -0700 Subject: Print matches for triggers as they appear in the buffer Triggers themselves, however, are printed exactly as used. For example, a term (x !in s) yields a trigger (x in s). --- Source/Dafny/Triggers/QuantifiersCollection.cs | 2 +- Source/Dafny/Triggers/TriggerExtensions.cs | 7 ++++--- Source/Dafny/Triggers/TriggersCollector.cs | 8 ++++++-- 3 files changed, 11 insertions(+), 6 deletions(-) (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index a6340f10..49cd84df 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -118,7 +118,7 @@ namespace Microsoft.Dafny.Triggers { c => !loopingSubterms[c].Any(), c => { looping.Add(c); - c.Annotation = "loops with " + loopingSubterms[c].MapConcat(t => Printer.ExprToString(t.Expr), ", "); + c.Annotation = "loops with " + loopingSubterms[c].MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", "); }).ToList(); q.CouldSuppressLoops = safe.Count > 0; diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index a49ed13a..6c3f4ee7 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -24,6 +24,7 @@ namespace Microsoft.Dafny.Triggers { internal struct TriggerMatch { internal Expression Expr; + internal Expression OriginalExpr; internal Dictionary Bindings; internal static bool Eq(TriggerMatch t1, TriggerMatch t2) { @@ -110,10 +111,10 @@ namespace Microsoft.Dafny.Triggers { return ShallowEq_Top(expr, trigger) && TriggerUtils.SameLists(expr.SubExpressions, trigger.SubExpressions, (e1, e2) => MatchesTrigger(e1, e2, holes, bindings)); } - private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, IEnumerable holes) { + private static TriggerMatch? MatchAgainst(this Expression expr, Expression trigger, IEnumerable holes, Expression originalExpr) { var bindings = new Dictionary(); if (expr.MatchesTrigger(trigger, new HashSet(holes), bindings)) { - return new TriggerMatch { Expr = expr, Bindings = bindings }; + return new TriggerMatch { Expr = expr, OriginalExpr = originalExpr ?? expr, Bindings = bindings }; } else { return null; } @@ -121,7 +122,7 @@ namespace Microsoft.Dafny.Triggers { internal static IEnumerable SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) { return quantifier.Term.AllSubExpressions() - .Select(e => TriggerUtils.CleanupExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars)) + .Select(e => TriggerUtils.CleanupExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars, e)) .Where(e => e.HasValue).Select(e => e.Value); } diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 08d33af6..735baa01 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -13,7 +13,11 @@ namespace Microsoft.Dafny.Triggers { internal ISet Variables { get; set; } public override string ToString() { - return Printer.ExprToString(OriginalExpr); + return Printer.ExprToString(Expr); + // NOTE: Using OriginalExpr here could cause some confusion: + // for example, {a !in b} is a binary expression, yielding + // trigger {a in b}. Saying the trigger is a !in b would be + // rather misleading. } internal static bool Eq(TriggerTerm t1, TriggerTerm t2) { @@ -45,7 +49,7 @@ 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); + var matchingSubterms = this.MatchingSubterms(quantifier); return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms)); } -- cgit v1.2.3 From 5176621e39435ddda9293b8ad0968cf1d7639fb6 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 16:36:21 -0700 Subject: Implement the SelectTrigger method, removing redundant triggers. The idea is that we define an partial order on triggers (which may contain multiple terms), and find all the maximal elements. The algorithm as implemented is rather inefficient; in particular, is does not look at the structure of the graph of the relation (thus is does many redundant comparisons). See triggers/useless-triggers-are-removed.dfy for an example where such a filter is useful. --- Source/Dafny/Triggers/QuantifiersCollection.cs | 42 +++++++++++++--------- Source/Dafny/Triggers/TriggerUtils.cs | 11 +++--- Source/Dafny/Triggers/TriggersCollector.cs | 35 ++++++++++++++++-- Test/triggers/useless-triggers-are-removed.dfy | 25 +++++++++++++ .../useless-triggers-are-removed.dfy.expect | 17 +++++++++ 5 files changed, 106 insertions(+), 24 deletions(-) create mode 100644 Test/triggers/useless-triggers-are-removed.dfy create mode 100644 Test/triggers/useless-triggers-are-removed.dfy.expect (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index e2afa2ee..bfa90d81 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -7,7 +7,6 @@ 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. namespace Microsoft.Dafny.Triggers { @@ -28,7 +27,7 @@ namespace Microsoft.Dafny.Triggers { internal void TrimInvalidTriggers() { Contract.Requires(CandidateTerms != null); Contract.Requires(Candidates != null); - Candidates = TriggerUtils.Filter(Candidates, tr => tr.MentionsAll(quantifier.BoundVars), tr => { }).ToList(); + Candidates = TriggerUtils.Filter(Candidates, tr => tr, (tr, _) => tr.MentionsAll(quantifier.BoundVars), (tr, _) => { }).ToList(); } } @@ -60,7 +59,13 @@ namespace Microsoft.Dafny.Triggers { return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any(); } - //FIXME document that this assumes that the quantifiers live in the same context and share the same variables + /// + /// Collect triggers from the body of each quantifier, and share them + /// between all quantifiers. This method assumes that all quantifiers + /// actually come from the same context, and were the result of a split that + /// gave them all the same variables. + /// + /// void CollectAndShareTriggers(TriggersCollector triggersCollector) { var pool = quantifiers.SelectMany(q => triggersCollector.CollectTriggers(q.quantifier)); var distinctPool = pool.Deduplicate(TriggerTerm.Eq); @@ -79,13 +84,10 @@ namespace Microsoft.Dafny.Triggers { } void BuildDependenciesGraph() { - // FIXME: Think more about multi-quantifier dependencies - //class QuantifierDependency { - // QuantifierWithTriggers Cause; - // QuantifierWithTriggers Consequence; - // List Triggers; - // List MatchingTerm; - //} + // The problem of finding matching loops between multiple-triggers is hard; it + // seems to require one to track exponentially-sized dependencies between parts + // of triggers and quantifiers. For now, we only do single-quantifier loop + // detection } void SuppressMatchingLoops() { @@ -111,14 +113,14 @@ namespace Microsoft.Dafny.Triggers { 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 = "loops with " + loopingSubterms[c].MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", "); + candidate => candidate.LoopingSubterms(q.quantifier).ToList(), + (candidate, loopingSubterms) => !loopingSubterms.Any(), + (candidate, loopingSubterms) => { + looping.Add(candidate); + candidate.Annotation = "loops with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", "); }).ToList(); q.CouldSuppressLoops = safe.Count > 0; @@ -131,7 +133,15 @@ namespace Microsoft.Dafny.Triggers { } void SelectTriggers() { - //FIXME + foreach (var q in quantifiers) { //FIXME Check whether this makes verification faster + q.Candidates = TriggerUtils.Filter(q.Candidates, + candidate => q.Candidates.Where(candidate.IsStrongerThan).ToList(), + (candidate, weakerCandidates) => !weakerCandidates.Any(), + (candidate, weakerCandidates) => { + q.RejectedCandidates.Add(candidate); + candidate.Annotation = "stronger than " + String.Join(", ", weakerCandidates); + }).ToList(); + } } private void CommitOne(QuantifierWithTriggers q, bool addHeader) { diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index 9ebcf846..6f76464b 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -76,13 +76,14 @@ namespace Microsoft.Dafny.Triggers { return it1_has == it2_has && acc; } - internal static IEnumerable Filter(IEnumerable elements, Func predicate, Action reject) { + internal static IEnumerable Filter(IEnumerable elements, Func Converter, Func predicate, Action reject) { var positive = new List(); - foreach (var c in elements) { - if (predicate(c)) { - yield return c; + foreach (var elem in elements) { + var conv = Converter(elem); + if (predicate(elem, conv)) { + yield return elem; } else { - reject(c); + reject(elem, conv); } } } diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 735baa01..3b2853ed 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -20,6 +20,20 @@ namespace Microsoft.Dafny.Triggers { // rather misleading. } + internal enum TermComparison { + SameStrength = 0, Stronger = 1, NotStronger = -1 + } + + internal TermComparison CompareTo(TriggerTerm other) { + if (this == other) { + return TermComparison.SameStrength; + } else if (Expr.AllSubExpressions(true).Any(other.Expr.ExpressionEq)) { + return TermComparison.Stronger; + } else { + return TermComparison.NotStronger; + } + } + internal static bool Eq(TriggerTerm t1, TriggerTerm t2) { return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr); } @@ -41,7 +55,7 @@ namespace Microsoft.Dafny.Triggers { return vars.All(x => Terms.Any(term => term.Variables.Contains(x))); } - private string Repr { get { return String.Join(", ", Terms); } } + internal string Repr { get { return String.Join(", ", Terms); } } public override string ToString() { return "{" + Repr + "}" + (String.IsNullOrWhiteSpace(Annotation) ? "" : " (" + Annotation + ")"); @@ -58,8 +72,23 @@ namespace Microsoft.Dafny.Triggers { return Terms.SelectMany(term => quantifier.SubexpressionsMatchingTrigger(term.Expr)).Deduplicate(TriggerMatch.Eq); } - public String AsDafnyAttributeString() { - return "{:trigger " + Repr + "}"; + internal bool IsStrongerThan(TriggerCandidate that) { + if (this == that) { + return false; + } + + var hasStrictlyStrongerTerm = false; + foreach (var t in Terms) { + var comparison = that.Terms.Select(t.CompareTo).Max(); + + // All terms of `this` must be at least as strong as a term of `that` + if (comparison == TriggerTerm.TermComparison.NotStronger) { return false; } + + // Did we find a strictly stronger term? + hasStrictlyStrongerTerm = hasStrictlyStrongerTerm || comparison == TriggerTerm.TermComparison.Stronger; + } + + return hasStrictlyStrongerTerm; } } diff --git a/Test/triggers/useless-triggers-are-removed.dfy b/Test/triggers/useless-triggers-are-removed.dfy new file mode 100644 index 00000000..16458e41 --- /dev/null +++ b/Test/triggers/useless-triggers-are-removed.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /printTooltips /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This file ensures that Dafny does get rid of redundant triggers before +// annotating a quantifier, and that ths process does not interfere with cycle +// detection. + +function f(x: int): int +function g(x: int): int +function h(x: int): int + +method M() + // In the following, only f(x) is kept. Note that the subset enumeration was + // already smart enough to not build any trigger with multiple terms (it only + // built 5 candidates) + requires forall x: int :: f(x) + g(f(x)) + h(f(x)) + g(h(f(x))) + h(g(f(x))) == 0 + + // Loop detection still works fine: in the following example, the trigger is + // f(f(x)) + requires forall x: int :: f(x) == f(f(x)) + + // This works for multi-triggers, too: + requires forall x, y :: f(x) + g(f(y)) + g(y) + g(f(x)) == 0 +{ +} diff --git a/Test/triggers/useless-triggers-are-removed.dfy.expect b/Test/triggers/useless-triggers-are-removed.dfy.expect new file mode 100644 index 00000000..6c2c0a2b --- /dev/null +++ b/Test/triggers/useless-triggers-are-removed.dfy.expect @@ -0,0 +1,17 @@ +useless-triggers-are-removed.dfy(16,11): Info: Selected triggers: {f(x)} + Rejected triggers: + {h(g(f(x)))} (stronger than {g(f(x))}, {f(x)}) + {g(h(f(x)))} (stronger than {h(f(x))}, {f(x)}) + {h(f(x))} (stronger than {f(x)}) + {g(f(x))} (stronger than {f(x)}) +useless-triggers-are-removed.dfy(20,11): Info: Selected triggers: {f(f(x))} + Rejected triggers: {f(x)} (loops with {f(f(x))}) +useless-triggers-are-removed.dfy(23,11): Info: Selected triggers: + {g(f(x)), g(y)}, {f(y), f(x)} + Rejected triggers: + {g(y), f(x)} (loops with {g(f(y))}, {g(f(x))}) + {g(f(x)), g(f(y))} (stronger than {g(f(x)), f(y)}, {g(f(y)), f(x)}, {f(y), f(x)}) + {g(f(x)), f(y)} (stronger than {f(y), f(x)}) + {g(f(y)), f(x)} (stronger than {f(y), f(x)}) + +Dafny program verifier finished with 5 verified, 0 errors -- cgit v1.2.3 From e676ad0877d31cb73a1a6bb5aae677ac64593fd6 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 19:58:46 -0700 Subject: Cleanup a number of FIXMEs that I had left in the code --- Source/Dafny/DafnyAst.cs | 12 ++++++------ Source/Dafny/Resolver.cs | 6 +++--- Source/Dafny/Triggers/QuantifiersCollection.cs | 8 ++------ Source/Dafny/Triggers/TriggersCollector.cs | 6 ++++-- Source/DafnyServer/DafnyHelper.cs | 2 +- Source/DafnyServer/Server.cs | 9 +-------- Source/DafnyServer/Utilities.cs | 6 ++---- 7 files changed, 19 insertions(+), 30 deletions(-) (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 14a354c4..06f6d856 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -7769,7 +7769,7 @@ namespace Microsoft.Dafny { } else if (decl is Method) { Visit((Method)decl); } - //FIXME More? + //TODO More? } public void Visit(Method method) { Visit(method.Ens); @@ -7777,7 +7777,7 @@ namespace Microsoft.Dafny { Visit(method.Mod.Expressions); Visit(method.Decreases.Expressions); if (method.Body != null) { Visit(method.Body); } - //FIXME More? + //TODO More? } public void Visit(Function function) { Visit(function.Ens); @@ -7785,7 +7785,7 @@ namespace Microsoft.Dafny { Visit(function.Reads); Visit(function.Decreases.Expressions); if (function.Body != null) { Visit(function.Body); } - //FIXME More? + //TODO More? } protected virtual void VisitOneExpr(Expression expr) { Contract.Requires(expr != null); @@ -7842,7 +7842,7 @@ namespace Microsoft.Dafny { } else if (decl is Method) { Visit((Method)decl, st); } - //FIXME More? + //TODO More? } public void Visit(Method method, State st) { Visit(method.Ens, st); @@ -7850,7 +7850,7 @@ namespace Microsoft.Dafny { Visit(method.Mod.Expressions, st); Visit(method.Decreases.Expressions, st); if (method.Body != null) { Visit(method.Body, st); } - //FIXME More? + //TODO More? } public void Visit(Function function, State st) { Visit(function.Ens, st); @@ -7858,7 +7858,7 @@ namespace Microsoft.Dafny { Visit(function.Reads, st); Visit(function.Decreases.Expressions, st); if (function.Body != null) { Visit(function.Body, st); } - //FIXME More? + //TODO More? } /// /// Visit one expression proper. This method is invoked before it is invoked on the diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 2f2b5a54..e5fe7cf8 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -199,7 +199,7 @@ namespace Microsoft.Dafny public void ResolveProgram(Program prog) { Contract.Requires(prog != null); - var origErrorCount = reporter.Count(ErrorLevel.Error); //FIXME (Clement): This is used further below, but not in the >0 comparisons in the next few lines. Is that right? + var origErrorCount = reporter.Count(ErrorLevel.Error); //TODO: This is used further below, but not in the >0 comparisons in the next few lines. Is that right? var bindings = new ModuleBindings(null); var b = BindModuleNames(prog.DefaultModuleDef, bindings); bindings.BindName("_module", prog.DefaultModule, b); @@ -8301,7 +8301,7 @@ namespace Microsoft.Dafny receiver = new StaticReceiverExpr(expr.tok, (ClassDecl)member.EnclosingClass, true); } else { if (!scope.AllowInstance) { - reporter.Error(MessageSource.Resolver, expr.tok, "'this' is not allowed in a 'static' context"); //FIXME: Rephrase this + reporter.Error(MessageSource.Resolver, expr.tok, "'this' is not allowed in a 'static' context"); //TODO: Rephrase this // nevertheless, set "receiver" to a value so we can continue resolution } receiver = new ImplicitThisExpr(expr.tok); @@ -8604,7 +8604,7 @@ namespace Microsoft.Dafny Dictionary members; if (classMembers.TryGetValue(cd, out members) && members.TryGetValue(expr.SuffixName, out member)) { if (!member.IsStatic) { - reporter.Error(MessageSource.Resolver, expr.tok, "accessing member '{0}' requires an instance expression", expr.SuffixName); //FIXME Unify with similar error message + reporter.Error(MessageSource.Resolver, expr.tok, "accessing member '{0}' requires an instance expression", expr.SuffixName); //TODO Unify with similar error messages // nevertheless, continue creating an expression that approximates a correct one } var receiver = new StaticReceiverExpr(expr.tok, (UserDefinedType)ty.NormalizeExpand(), (ClassDecl)member.EnclosingClass, false); diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index bfa90d81..8e4c3261 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -7,8 +7,6 @@ using System.Text; using Microsoft.Boogie; using System.Diagnostics.Contracts; -//FIXME: When scoring, do not consider old(x) to be higher than x. - namespace Microsoft.Dafny.Triggers { class QuantifierWithTriggers { internal QuantifierExpr quantifier; @@ -149,16 +147,14 @@ namespace Microsoft.Dafny.Triggers { var msg = new StringBuilder(); var indent = addHeader ? " " : ""; - if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { //FIXME: matchingloop, split and autotriggers attributes are passed down to Boogie + if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: matchingloop, split and autotriggers attributes are passed down to Boogie msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); - // FIXME This shouldn't be printed for autoReqs. (see autoReq.dfy) - // FIXME typeQuantifier? } else { if (addHeader) { msg.AppendFormat("For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine(); } - foreach (var candidate in q.Candidates) { //FIXME make this _trigger instead of trigger + foreach (var candidate in q.Candidates) { q.quantifier.Attributes = new Attributes("trigger", candidate.Terms.Select(t => t.Expr).ToList(), q.quantifier.Attributes); } diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 3b2853ed..30f7b9e8 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -249,10 +249,12 @@ namespace Microsoft.Dafny.Triggers { return new TriggerAnnotation(isTriggerKiller || CollectIsKiller(expr), CollectVariables(expr), CollectExportedCandidates(expr)); } - // FIXME document that this will contain duplicates + /// + /// Collect terms in the body of the subexpressions of the argument that look like quantifiers. The results of this function can contain duplicate terms. + /// 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 + // NOTE: We could check for existing trigger attributes and return that instead return Annotate(quantifier).PrivateTerms; } diff --git a/Source/DafnyServer/DafnyHelper.cs b/Source/DafnyServer/DafnyHelper.cs index 952f71c5..3204fdb3 100644 --- a/Source/DafnyServer/DafnyHelper.cs +++ b/Source/DafnyServer/DafnyHelper.cs @@ -74,7 +74,7 @@ namespace Microsoft.Dafny { ExecutionEngine.CoalesceBlocks(boogieProgram); ExecutionEngine.Inline(boogieProgram); - //FIXME Could capture errors instead of printing them (pass a delegate instead of null) + //NOTE: We could capture errors instead of printing them (pass a delegate instead of null) switch (ExecutionEngine.InferAndVerify(boogieProgram, new PipelineStatistics(), "ServerProgram", null, DateTime.UtcNow.Ticks.ToString())) { case PipelineOutcome.Done: case PipelineOutcome.VerificationCompleted: diff --git a/Source/DafnyServer/Server.cs b/Source/DafnyServer/Server.cs index e524a9a3..77840007 100644 --- a/Source/DafnyServer/Server.cs +++ b/Source/DafnyServer/Server.cs @@ -32,9 +32,8 @@ namespace Microsoft.Dafny { private void SetupConsole() { var utf8 = new UTF8Encoding(false, true); + Console.InputEncoding = utf8; Console.OutputEncoding = utf8; - Console.OutputEncoding = utf8; - Console.CancelKeyPress += CancelKeyPress; } public Server() { @@ -43,12 +42,6 @@ namespace Microsoft.Dafny { SetupConsole(); } - void CancelKeyPress(object sender, ConsoleCancelEventArgs e) { - // e.Cancel = true; - // FIXME TerminateProver and RunningProverFromCommandLine - // Cancel the current verification? TerminateProver()? Or kill entirely? - } - bool EndOfPayload(out string line) { line = Console.ReadLine(); return line == null || line == Interaction.CLIENT_EOM_TAG; diff --git a/Source/DafnyServer/Utilities.cs b/Source/DafnyServer/Utilities.cs index d6654ac1..59b3abb9 100644 --- a/Source/DafnyServer/Utilities.cs +++ b/Source/DafnyServer/Utilities.cs @@ -45,13 +45,11 @@ namespace Microsoft.Dafny { internal static void ApplyArgs(string[] args) { Dafny.DafnyOptions.Install(new Dafny.DafnyOptions()); - Dafny.DafnyOptions.O.ProverKillTime = 10; + Dafny.DafnyOptions.O.ProverKillTime = 15; //This is just a default; it can be overriden if (CommandLineOptions.Clo.Parse(args)) { - // Dafny.DafnyOptions.O.ErrorTrace = 0; //FIXME - // Dafny.DafnyOptions.O.ModelViewFile = "-"; DafnyOptions.O.VerifySnapshots = 2; // Use caching - DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount - 1); //FIXME + DafnyOptions.O.VcsCores = Math.Max(1, System.Environment.ProcessorCount / 2); // Don't use too many cores DafnyOptions.O.PrintTooltips = true; // Dump tooptips (ErrorLevel.Info) to stdout DafnyOptions.O.UnicodeOutput = true; // Use pretty warning signs DafnyOptions.O.TraceProofObligations = true; // Show which method is being verified, but don't show duration of verification -- cgit v1.2.3 From b819c42e85eb8ac0968abeab9f3fa3420a5dd760 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 21 Aug 2015 09:40:17 -0700 Subject: Allow display expressions as trigger terms --- Source/Dafny/Triggers/TriggersCollector.cs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 30f7b9e8..167a6a1b 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -169,7 +169,7 @@ namespace Microsoft.Dafny.Triggers { expr.SubExpressions.Iter(e => Annotate(e)); TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort - if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MemberSelectExpr || expr is OldExpr || expr is ApplyExpr || + if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MemberSelectExpr || expr is OldExpr || expr is ApplyExpr || expr is DisplayExpression || (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); @@ -186,8 +186,7 @@ namespace Microsoft.Dafny.Triggers { expr is OldExpr || expr is ThisExpr || expr is BoxingCastExpr || - expr is DatatypeValue || - expr is SeqDisplayExpr) { //FIXME what abvout other display expressions? + expr is DatatypeValue) { annotation = AnnotateOther(expr, false); } else { annotation = AnnotateOther(expr, true); -- cgit v1.2.3 From ff05bb6936d433e7be5ded41233214c0517dc2d2 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 21 Aug 2015 19:13:56 -0700 Subject: Make `old` a special case for trigger generation. Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and old(f(x)). This has a number of implications; see the new tests files for more information. --- Source/Dafny/Rewriter.cs | 4 +- Source/Dafny/Triggers/QuantifiersCollector.cs | 17 +++++--- Source/Dafny/Triggers/TriggerExtensions.cs | 24 ++++++------ Source/Dafny/Triggers/TriggerUtils.cs | 45 +++++++++++++++------- Source/Dafny/Triggers/TriggersCollector.cs | 34 +++++++++++----- .../looping-is-hard-to-decide-modulo-equality.dfy | 32 +++++++++++++++ ...ng-is-hard-to-decide-modulo-equality.dfy.expect | 10 +++++ .../old-is-a-special-case-for-triggers.dfy | 32 +++++++++++++++ .../old-is-a-special-case-for-triggers.dfy.expect | 22 +++++++++++ 9 files changed, 178 insertions(+), 42 deletions(-) create mode 100644 Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy create mode 100644 Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect create mode 100644 Test/triggers/old-is-a-special-case-for-triggers.dfy create mode 100644 Test/triggers/old-is-a-special-case-for-triggers.dfy.expect (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index 230d9349..557eee93 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -47,10 +47,10 @@ namespace Microsoft.Dafny var finder = new Triggers.QuantifierCollector(reporter); foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { - finder.Visit(decl, null); + finder.Visit(decl, false); } - var triggersCollector = new Triggers.TriggersCollector(); + var triggersCollector = new Triggers.TriggersCollector(finder.exprsInOldContext); foreach (var quantifierCollection in finder.quantifierCollections) { quantifierCollection.ComputeTriggers(triggersCollector); quantifierCollection.CommitTriggers(); diff --git a/Source/Dafny/Triggers/QuantifiersCollector.cs b/Source/Dafny/Triggers/QuantifiersCollector.cs index b30cb6b1..3385f36e 100644 --- a/Source/Dafny/Triggers/QuantifiersCollector.cs +++ b/Source/Dafny/Triggers/QuantifiersCollector.cs @@ -6,18 +6,19 @@ using Microsoft.Boogie; using System.Collections.ObjectModel; using System.Diagnostics.Contracts; -namespace Microsoft.Dafny.Triggers { //FIXME rename this file - internal class QuantifierCollector : TopDownVisitor { +namespace Microsoft.Dafny.Triggers { + internal class QuantifierCollector : TopDownVisitor { readonly ErrorReporter reporter; - private HashSet quantifiers = new HashSet(); - internal List quantifierCollections = new List(); + private readonly HashSet quantifiers = new HashSet(); + internal readonly HashSet exprsInOldContext = new HashSet(); + internal readonly List quantifierCollections = new List(); public QuantifierCollector(ErrorReporter reporter) { Contract.Requires(reporter != null); this.reporter = reporter; } - protected override bool VisitOneExpr(Expression expr, ref object _) { + protected override bool VisitOneExpr(Expression expr, ref bool inOldContext) { var quantifier = expr as QuantifierExpr; if (quantifier != null && !quantifiers.Contains(quantifier)) { @@ -31,6 +32,12 @@ namespace Microsoft.Dafny.Triggers { //FIXME rename this file } } + if (expr is OldExpr) { + inOldContext = true; + } else if (inOldContext) { // FIXME be more restrctive on the type of stuff that we annotate + exprsInOldContext.Add(expr); + } + return true; } } diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index 6c3f4ee7..02deb92f 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -38,17 +38,18 @@ namespace Microsoft.Dafny.Triggers { } internal static class ExprExtensions { - internal static IEnumerable AllSubExpressions(this Expression expr, bool strict = false) { + internal static IEnumerable AllSubExpressions(this Expression expr, bool wrapOld, bool strict) { + bool isOld = expr is OldExpr; + foreach (var subexpr in expr.SubExpressions) { - foreach (var r_subexpr in AllSubExpressions(subexpr, false)) { - yield return r_subexpr; + foreach (var r_subexpr in AllSubExpressions(subexpr, wrapOld, false)) { + yield return TriggerUtils.MaybeWrapInOld(r_subexpr, isOld); } - yield return subexpr; } if (expr is StmtExpr) { - foreach (var r_subexpr in AllSubExpressions(((StmtExpr)expr).S, false)) { - yield return r_subexpr; + foreach (var r_subexpr in AllSubExpressions(((StmtExpr)expr).S, wrapOld, false)) { + yield return TriggerUtils.MaybeWrapInOld(r_subexpr, isOld); } } @@ -57,16 +58,15 @@ namespace Microsoft.Dafny.Triggers { } } - internal static IEnumerable AllSubExpressions(this Statement stmt, bool strict = false) { + internal static IEnumerable AllSubExpressions(this Statement stmt, bool wrapOld, bool strict) { foreach (var subexpr in stmt.SubExpressions) { - foreach (var r_subexpr in AllSubExpressions(subexpr, false)) { + foreach (var r_subexpr in AllSubExpressions(subexpr, wrapOld, false)) { yield return r_subexpr; } - yield return subexpr; } foreach (var substmt in stmt.SubStatements) { - foreach (var r_subexpr in AllSubExpressions(substmt, false)) { + foreach (var r_subexpr in AllSubExpressions(substmt, wrapOld, false)) { yield return r_subexpr; } } @@ -121,8 +121,8 @@ namespace Microsoft.Dafny.Triggers { } internal static IEnumerable SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) { - return quantifier.Term.AllSubExpressions() - .Select(e => TriggerUtils.CleanupExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars, e)) + return quantifier.Term.AllSubExpressions(true, false) //FIXME should loop detection actually pass true here? + .Select(e => TriggerUtils.PrepareExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars, e)) .Where(e => e.HasValue).Select(e => e.Value); } diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index 6f76464b..4fd139e2 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -129,35 +129,52 @@ namespace Microsoft.Dafny.Triggers { throw new ArgumentException(); } - internal static Expression CleanupExprForInclusionInTrigger(Expression expr, out bool isKiller) { + internal static Expression PrepareExprForInclusionInTrigger(Expression expr, out bool isKiller) { isKiller = false; - if (!(expr is BinaryExpr)) { - return expr; + var ret = expr; + if (ret is BinaryExpr) { + ret = PrepareInMultisetForInclusionInTrigger(PrepareNotInForInclusionInTrigger((BinaryExpr)ret), ref isKiller); } - var bexpr = expr as BinaryExpr; + return ret; + } - BinaryExpr new_expr = bexpr; + private static BinaryExpr PrepareNotInForInclusionInTrigger(BinaryExpr bexpr) { if (bexpr.Op == BinaryExpr.Opcode.NotIn) { - new_expr = new BinaryExpr(bexpr.tok, BinaryExpr.Opcode.In, bexpr.E0, bexpr.E1); + var new_expr = new BinaryExpr(bexpr.tok, BinaryExpr.Opcode.In, bexpr.E0, bexpr.E1); new_expr.ResolvedOp = RemoveNotInBinaryExprIn(bexpr.ResolvedOp); new_expr.Type = bexpr.Type; + return new_expr; + } else { + return bexpr; } + } - Expression returned_expr = new_expr; - if (new_expr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) { - returned_expr = new SeqSelectExpr(new_expr.tok, true, new_expr.E1, new_expr.E0, null); - returned_expr.Type = bexpr.Type; + private static Expression PrepareInMultisetForInclusionInTrigger(BinaryExpr bexpr, ref bool isKiller) { + if (bexpr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) { + var new_expr = new SeqSelectExpr(bexpr.tok, true, bexpr.E1, bexpr.E0, null); + new_expr.Type = bexpr.Type; isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer + return new_expr; + } else { + return bexpr; } - - return returned_expr; } - internal static Expression CleanupExprForInclusionInTrigger(Expression expr) { + internal static Expression PrepareExprForInclusionInTrigger(Expression expr) { bool _; - return CleanupExprForInclusionInTrigger(expr, out _); + return PrepareExprForInclusionInTrigger(expr, out _); + } + + internal static Expression MaybeWrapInOld(Expression expr, bool wrap) { + if (wrap && !(expr is NameSegment) && !(expr is IdentifierExpr)) { + var newExpr = new OldExpr(expr.tok, expr); + newExpr.Type = expr.Type; + return newExpr; + } else { + return expr; + } } } } diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 167a6a1b..11860404 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -27,7 +27,7 @@ namespace Microsoft.Dafny.Triggers { internal TermComparison CompareTo(TriggerTerm other) { if (this == other) { return TermComparison.SameStrength; - } else if (Expr.AllSubExpressions(true).Any(other.Expr.ExpressionEq)) { + } else if (Expr.AllSubExpressions(true, true).Any(other.Expr.ExpressionEq)) { return TermComparison.Stronger; } else { return TermComparison.NotStronger; @@ -92,7 +92,7 @@ namespace Microsoft.Dafny.Triggers { } } - class TriggerAnnotation { + internal class TriggerAnnotation { internal bool IsTriggerKiller; internal ISet Variables; internal readonly List PrivateTerms; @@ -132,11 +132,27 @@ namespace Microsoft.Dafny.Triggers { } } - public class TriggersCollector { - Dictionary cache; + internal class TriggerAnnotationsCache { + public readonly HashSet exprsInOldContext; + public readonly Dictionary annotations; - internal TriggersCollector() { - this.cache = new Dictionary(); + /// + /// For certain operations, the TriggersCollector class needs to know whether + /// an particular expression is under an old(...) wrapper. This is in particular + /// true for generating trigger terms (but it is not for checking wehter something + /// is a trigger killer, so passing an empty set here for that case would be fine. + /// + public TriggerAnnotationsCache(HashSet exprsInOldContext) { + this.exprsInOldContext = exprsInOldContext; + annotations = new Dictionary(); + } + } + + internal class TriggersCollector { + TriggerAnnotationsCache cache; + + internal TriggersCollector(HashSet exprsInOldContext) { + this.cache = new TriggerAnnotationsCache(exprsInOldContext); } private T ReduceAnnotatedSubExpressions(Expression expr, T seed, Func map, Func reduce) { @@ -162,7 +178,7 @@ namespace Microsoft.Dafny.Triggers { private TriggerAnnotation Annotate(Expression expr) { TriggerAnnotation cached; - if (cache.TryGetValue(expr, out cached)) { + if (cache.annotations.TryGetValue(expr, out cached)) { return cached; } @@ -193,13 +209,13 @@ namespace Microsoft.Dafny.Triggers { } TriggerUtils.DebugTriggers("{0} ({1})\n{2}", Printer.ExprToString(expr), expr.GetType(), annotation); - cache[expr] = annotation; + cache.annotations[expr] = annotation; return annotation; } private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) { bool expr_is_killer = false; - var new_expr = TriggerUtils.CleanupExprForInclusionInTrigger(expr, out expr_is_killer); + var new_expr = TriggerUtils.MaybeWrapInOld(TriggerUtils.PrepareExprForInclusionInTrigger(expr, out expr_is_killer), cache.exprsInOldContext.Contains(expr)); var new_term = new TriggerTerm { Expr = new_expr, OriginalExpr = expr, Variables = CollectVariables(expr) }; List collected_terms = CollectExportedCandidates(expr); diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy new file mode 100644 index 00000000..c54089f2 --- /dev/null +++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy @@ -0,0 +1,32 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This file shows cases where loops could hide behind equalities. In all three +// cases we behave the same; that is, we don't warn for loops that would only +// exist in the presence of an equality. The easiest way to understand the +// issue, I (CPC) feel, is to look at the old case: f(x) could very well loop +// with old(f(f(x))) if f(f(x)) did not change the heap at all. + +// This equality issue is generally undecidable. It could make sense to special +// case `old`, but KRML and CPC decided against it on 2015-08-21. Future +// experiences could cause a change of mind. + +class C { } +function f(c: C): C +function g(c: C): C +function h(c: C, i: int): C + +// With explicit arguments +method M0(i: int, j: int, sc: set) { + assert forall c | c in sc :: true || h(c, i) == h(h(c, j), j); +} + +// With implicit arguments (f and g respectively, to Apply) +method M1(f: int -> int, g: int -> int) { + assert forall x :: true || f(x) == g(f(x)); +} + +// With implicit arguments (the heap, to old) +method M2(sc: set) { + assert forall c | c in sc :: true || f(c) == old(f(f(c))); +} diff --git a/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect new file mode 100644 index 00000000..c0eebdba --- /dev/null +++ b/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy.expect @@ -0,0 +1,10 @@ +looping-is-hard-to-decide-modulo-equality.dfy(21,9): Info: Selected triggers: + {h(h(c, j), j)}, {h(c, i)}, {c in sc} + Rejected triggers: {h(c, j)} (loops with {h(h(c, j), j)}) +looping-is-hard-to-decide-modulo-equality.dfy(26,9): Info: Selected triggers: {f(x)} + Rejected triggers: {g(f(x))} (more specific than {f(x)}) +looping-is-hard-to-decide-modulo-equality.dfy(31,9): Info: Selected triggers: + {old(f(f(c)))}, {f(c)}, {c in sc} + Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))}) + +Dafny program verifier finished with 9 verified, 0 errors diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy b/Test/triggers/old-is-a-special-case-for-triggers.dfy new file mode 100644 index 00000000..4424e8d3 --- /dev/null +++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy @@ -0,0 +1,32 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This file ensures that `old()` receives the special treatment that it +// requires; that is, `old(f(x))` is not less liberal than `f(x)`, and +// old(f(f(x))) does not loop with f(x) (doesn't it?) + +class C { } +function f(c: C): C +function g(c: C): C +function h(c: C, i: int): C + +method M(sc: set) + // Ensure that old(c) does not get picked as a trigger + ensures forall c | c in sc :: true || c == old(f(c)) + + // This checks whether loop detection handles `old` expressions properly. + // In the first one f(c)/old(f(f(c))) is not reported as a loop. See + // looping-is-hard-to-decide-modulo-equalities.dfy for an explanation. + ensures forall c | c in sc :: true || f(c) == old(f(f(c))) + ensures forall c | c in sc :: true || old(f(f(c))) == old(g(f(c))) || old(f(g(c))) == g(f(c)) || f(g(c)) == g(f(c)) + + // These check that the final trigger filtering step doesn't get confused + // between old expressions and regular expressions. + ensures forall c | c in sc :: true || f(c) == old(g(f(c))) + ensures forall c | c in sc :: true || f(c) == old(f(c)) || old(g(f(c))) == g(f(c)) + + // WISH: A Dafny rewriter could cleanup expressions so that adding the + // expression forall c :: c == old(c) in a quantifier would cause a warning, + // instead of a trigger generation error as it does now. +{ +} diff --git a/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect new file mode 100644 index 00000000..23ec089d --- /dev/null +++ b/Test/triggers/old-is-a-special-case-for-triggers.dfy.expect @@ -0,0 +1,22 @@ +old-is-a-special-case-for-triggers.dfy(15,10): Info: Selected triggers: + {old(f(c))}, {c in sc} +old-is-a-special-case-for-triggers.dfy(20,10): Info: Selected triggers: + {old(f(f(c)))}, {f(c)}, {c in sc} + Rejected triggers: {old(f(c))} (loops with {old(f(f(c)))}) +old-is-a-special-case-for-triggers.dfy(21,10): Info: Selected triggers: + {f(g(c))}, {g(f(c))}, {old(f(g(c)))}, {old(g(f(c)))}, {old(f(f(c)))}, {c in sc} + Rejected triggers: + {g(c)} (loops with {g(f(c))}) + {f(c)} (loops with {f(g(c))}) + {old(g(c))} (loops with {old(g(f(c)))}) + {old(f(c))} (loops with {old(f(f(c)))}, {old(f(g(c)))}) +old-is-a-special-case-for-triggers.dfy(25,10): Info: Selected triggers: + {old(f(c))}, {f(c)}, {c in sc} + Rejected triggers: {old(g(f(c)))} (more specific than {old(f(c))}) +old-is-a-special-case-for-triggers.dfy(26,10): Info: Selected triggers: + {old(f(c))}, {f(c)}, {c in sc} + Rejected triggers: + {g(f(c))} (more specific than {f(c)}) + {old(g(f(c)))} (more specific than {old(f(c))}) + +Dafny program verifier finished with 5 verified, 0 errors -- cgit v1.2.3 From 1a0ef1ae83a88966a2d68e5eba5a70a215f28f3e Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sun, 23 Aug 2015 00:08:25 -0700 Subject: Allow MultiSelectExpr as quantifier heads --- Source/Dafny/Triggers/TriggersCollector.cs | 3 ++- Test/triggers/matrix-accesses-are-triggers.dfy | 9 +++++++++ Test/triggers/matrix-accesses-are-triggers.dfy.expect | 12 ++++++++++++ 3 files changed, 23 insertions(+), 1 deletion(-) create mode 100644 Test/triggers/matrix-accesses-are-triggers.dfy create mode 100644 Test/triggers/matrix-accesses-are-triggers.dfy.expect (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 11860404..69c47d90 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -185,7 +185,8 @@ namespace Microsoft.Dafny.Triggers { expr.SubExpressions.Iter(e => Annotate(e)); TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort - if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MemberSelectExpr || expr is OldExpr || expr is ApplyExpr || expr is DisplayExpression || + if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MultiSelectExpr || expr is MemberSelectExpr || + expr is OldExpr || expr is ApplyExpr || expr is DisplayExpression || (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); diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy b/Test/triggers/matrix-accesses-are-triggers.dfy new file mode 100644 index 00000000..630fab9d --- /dev/null +++ b/Test/triggers/matrix-accesses-are-triggers.dfy @@ -0,0 +1,9 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This file checks that multi-dimensional array accesses yield trigger candidates + +method M(m: array2) + requires m != null + requires forall i, j | 0 <= i < m.Length0 && 0 <= j < m.Length1 :: m[i, j] == m[j, i+1] { +} diff --git a/Test/triggers/matrix-accesses-are-triggers.dfy.expect b/Test/triggers/matrix-accesses-are-triggers.dfy.expect new file mode 100644 index 00000000..b9dd1d88 --- /dev/null +++ b/Test/triggers/matrix-accesses-are-triggers.dfy.expect @@ -0,0 +1,12 @@ +matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (loops with {m[j, i + 1]}) + (!) Suppressing loops would leave this expression without triggers. +matrix-accesses-are-triggers.dfy(8,81): Error: index 0 out of range +Execution trace: + (0,0): anon0 + (0,0): anon4_Then +matrix-accesses-are-triggers.dfy(8,86): Error: index 1 out of range +Execution trace: + (0,0): anon0 + (0,0): anon4_Then + +Dafny program verifier finished with 1 verified, 2 errors -- cgit v1.2.3 From c55cb226f4de90b080aa809d883d52c3386db063 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 26 Aug 2015 18:36:34 -0700 Subject: Improve the redundancy detection algorithm used while constructing sets of terms Based on an issue noted by Chris with redundancy removal resuls being dependent on the order of the terms. Interestingly, one of our tests already had an instance of that problem. Also fix the issue with nested quantifiers getting redundant triggers. --- Source/Dafny/DafnyAst.cs | 1 + Source/Dafny/Triggers/QuantifiersCollection.cs | 17 ++-- Source/Dafny/Triggers/TriggerUtils.cs | 100 ++++++++++++++++++--- Source/Dafny/Triggers/TriggersCollector.cs | 5 ++ .../function-applications-are-triggers.dfy.expect | 2 +- .../redundancy-detection-is-bidirectional.dfy | 29 ++++++ ...edundancy-detection-is-bidirectional.dfy.expect | 12 +++ 7 files changed, 143 insertions(+), 23 deletions(-) create mode 100644 Test/triggers/redundancy-detection-is-bidirectional.dfy create mode 100644 Test/triggers/redundancy-detection-is-bidirectional.dfy.expect (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index c7aae173..9bff2038 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2965,6 +2965,7 @@ namespace Microsoft.Dafny { } } + [DebuggerDisplay("Bound<{name}>")] public class BoundVar : NonglobalVariable { public override bool IsMutable { get { diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 6555b52a..114d5f5d 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -47,15 +47,9 @@ namespace Microsoft.Dafny.Triggers { 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. - // Note that this may still be an over-approximation, as in the following example: - // forall a, b :: forall x :: a[x] || b[x] > 0. - return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any(); + private bool SubsetGenerationPredicate(TriggerUtils.SetOfTerms terms, TriggerTerm additionalTerm) { + return true; // FIXME Remove this + //return additionalTerm.Variables.Where(v => v is BoundVar && !terms.Any(t => t.Variables.Contains(v))).Any(); } /// @@ -68,11 +62,10 @@ namespace Microsoft.Dafny.Triggers { 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) { - q.CandidateTerms = distinctPool; //Candidate terms are immutable: no copy needed - q.Candidates = multiPool.Select(candidate => new TriggerCandidate(candidate)).ToList(); + q.CandidateTerms = distinctPool; // The list of candidate terms is immutable + q.Candidates = TriggerUtils.AllNonEmptySubsets(distinctPool, SubsetGenerationPredicate, q.quantifier.BoundVars).Select(set => set.ToTriggerCandidate()).ToList(); } } diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs index 4fd139e2..efa1f167 100644 --- a/Source/Dafny/Triggers/TriggerUtils.cs +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -15,29 +15,109 @@ namespace Microsoft.Dafny.Triggers { return copy; } - internal static IEnumerable> AllSubsets(IList source, Func, T, bool> predicate, int offset) { + internal class SetOfTerms { + internal bool IsRedundant { get; private set; } + internal List Terms { get; set; } + + private ISet variables; + private Dictionary termOwningAUniqueVar; + private Dictionary> uniqueVarsOwnedByATerm; + + public int Count { get { return Terms.Count; } } + + private SetOfTerms() { } + + internal TriggerCandidate ToTriggerCandidate() { + return new TriggerCandidate(Terms); + } + + internal static SetOfTerms Empty() { + var newSet = new SetOfTerms(); + newSet.IsRedundant = false; + newSet.Terms = new List(); + newSet.variables = new HashSet(); + newSet.termOwningAUniqueVar = new Dictionary(); + newSet.uniqueVarsOwnedByATerm = new Dictionary>(); + return newSet; + } + + /// + /// 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. As it copies its + /// argument, this method updates various datastructures that allow it to + /// efficiently track ownership relations between formulae and bound variables, + /// and sets the IsRedundant flag of the returned set, allowing the caller to + /// discard that set of terms, and the ones that would have been built on top of + /// it, thus ensuring that the only sets of terms produced in the end are sets + /// of terms in which each element contributes (owns) at least one variable. + /// + /// Note that this is trickier than just checking every term for new variables; + /// indeed, a new term that does bring new variables in can make an existing + /// term redundant (see redundancy-detection-does-its-job-properly.dfy). + /// + internal SetOfTerms CopyWithAdd(TriggerTerm term, ISet relevantVariables) { + var copy = new SetOfTerms(); + copy.Terms = new List(Terms); + copy.variables = new HashSet(variables); + copy.termOwningAUniqueVar = new Dictionary(termOwningAUniqueVar); + copy.uniqueVarsOwnedByATerm = new Dictionary>(uniqueVarsOwnedByATerm); + + copy.Terms.Add(term); + + var varsInNewTerm = new HashSet(term.BoundVars); + varsInNewTerm.IntersectWith(relevantVariables); + + var ownedByNewTerm = new HashSet(); + + // Check #0: does this term bring anything new? + copy.IsRedundant = IsRedundant || varsInNewTerm.All(bv => copy.variables.Contains(bv)); + copy.variables.UnionWith(varsInNewTerm); + + // Check #1: does this term claiming ownership of all its variables cause another term to become useless? + foreach (var v in varsInNewTerm) { + TriggerTerm originalOwner; + if (copy.termOwningAUniqueVar.TryGetValue(v, out originalOwner)) { + var alsoOwnedByOriginalOwner = copy.uniqueVarsOwnedByATerm[originalOwner]; + alsoOwnedByOriginalOwner.Remove(v); + if (!alsoOwnedByOriginalOwner.Any()) { + copy.IsRedundant = true; + } + } else { + ownedByNewTerm.Add(v); + copy.termOwningAUniqueVar[v] = term; + } + } + + // Actually claim ownership + copy.uniqueVarsOwnedByATerm[term] = ownedByNewTerm; + + return copy; + } + } + + internal static IEnumerable AllSubsets(IList source, Func predicate, int offset, ISet relevantVariables) { if (offset >= source.Count) { - yield return new List(); + yield return SetOfTerms.Empty(); yield break; } - foreach (var subset in AllSubsets(source, predicate, offset + 1)) { - if (predicate(subset, source[offset])) { - yield return CopyAndAdd(subset, source[offset]); + foreach (var subset in AllSubsets(source, predicate, offset + 1, relevantVariables)) { + var newSet = subset.CopyWithAdd(source[offset], relevantVariables); + if (!newSet.IsRedundant && predicate(subset, source[offset])) { // Fixme remove the predicate? + yield return newSet; } - yield return new List(subset); + yield return subset; } } - internal static IEnumerable> AllNonEmptySubsets(IEnumerable source, Func, T, bool> predicate) { - List all = new List(source); - foreach (var subset in AllSubsets(all, predicate, 0)) { + internal static IEnumerable AllNonEmptySubsets(IList source, Func predicate, IEnumerable relevantVariables) { + foreach (var subset in AllSubsets(source, predicate, 0, new HashSet(relevantVariables))) { if (subset.Count > 0) { yield return subset; } } } - + internal static List MergeAlterFirst(List a, List b) { Contract.Requires(a != null); Contract.Requires(b != null); diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 69c47d90..d78bcb9e 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -11,6 +11,11 @@ namespace Microsoft.Dafny.Triggers { internal Expression Expr { get; set; } internal Expression OriginalExpr { get; set; } internal ISet Variables { get; set; } + internal IEnumerable BoundVars { + get { + return Variables.Select(v => v as BoundVar).Where(v => v != null); + } + } public override string ToString() { return Printer.ExprToString(Expr); diff --git a/Test/triggers/function-applications-are-triggers.dfy.expect b/Test/triggers/function-applications-are-triggers.dfy.expect index 7922e88d..501cfa51 100644 --- a/Test/triggers/function-applications-are-triggers.dfy.expect +++ b/Test/triggers/function-applications-are-triggers.dfy.expect @@ -8,6 +8,6 @@ function-applications-are-triggers.dfy(10,9): Info: For expression {P(f) ==> f(1 function-applications-are-triggers.dfy(11,9): Info: Selected triggers: {f(10)}, {f.requires(10)} function-applications-are-triggers.dfy(12,5): Info: Selected triggers: - {g(x), f(x)}, {g(x), f.requires(x)}, {g(x)}, {f(x)}, {g.requires(x), f.requires(x)}, {g.requires(x)}, {f.requires(x)} + {g(x)}, {f(x)}, {g.requires(x)}, {f.requires(x)} Dafny program verifier finished with 2 verified, 0 errors diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy new file mode 100644 index 00000000..df1d78c3 --- /dev/null +++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy @@ -0,0 +1,29 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This tests checks for tricky cases of redundancy suppression when building +// triggers. + +predicate P(x: int, y: int) +predicate Q(x: int) +predicate R(x: int) + +method M() { + // For this term, it is enough to order the terms by number of variables + assert forall x, y :: true || P(x, y) || Q(y) || R(x); + assert forall x, y :: true || Q(y) || P(x, y) || R(x); + assert forall x, y :: true || Q(y) || R(x) || P(x, y); +} + +predicate PP(x: int, y: int, z: int) +predicate QQ(x: int, y: int) +predicate RR(x: int, y: int) +predicate SS(x: int, y: int) + +method MM() { + // Not for this one, though + assert forall x, y, z, u, v, w :: true || PP(x, y, z) || QQ(x, u) || RR(y, v) || SS(z, w); + assert forall x, y, z, u, v, w :: true || QQ(x, u) || PP(x, y, z) || RR(y, v) || SS(z, w); + assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || PP(x, y, z) || SS(z, w); + assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || SS(z, w) || PP(x, y, z); +} diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect new file mode 100644 index 00000000..78c9e7ca --- /dev/null +++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy.expect @@ -0,0 +1,12 @@ +redundancy-detection-is-bidirectional.dfy(13,9): Info: Selected triggers: + {R(x), Q(y)}, {P(x, y)} +redundancy-detection-is-bidirectional.dfy(14,9): Info: Selected triggers: + {R(x), Q(y)}, {P(x, y)} +redundancy-detection-is-bidirectional.dfy(15,9): Info: Selected triggers: + {P(x, y)}, {R(x), Q(y)} +redundancy-detection-is-bidirectional.dfy(25,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)} +redundancy-detection-is-bidirectional.dfy(26,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)} +redundancy-detection-is-bidirectional.dfy(27,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)} +redundancy-detection-is-bidirectional.dfy(28,9): Info: Selected triggers: {SS(z, w), RR(y, v), QQ(x, u)} + +Dafny program verifier finished with 11 verified, 0 errors -- cgit v1.2.3 From 1e725f0c9382a3dd8be109d160581868c9567f61 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 21:25:06 -0700 Subject: Further relax the loop detection conditions Mismatches are now allowed up to expressions not involving any of the bound variables of the quantifier under inspection. --- Source/Dafny/Triggers/QuantifiersCollection.cs | 7 +++++-- Source/Dafny/Triggers/TriggerExtensions.cs | 23 +++++++++++++++++----- Source/Dafny/Triggers/TriggersCollector.cs | 3 ++- Test/triggers/loop-detection-is-not-too-strict.dfy | 21 +++++++++++++++++++- .../loop-detection-is-not-too-strict.dfy.expect | 17 ++++++++++++---- 5 files changed, 58 insertions(+), 13 deletions(-) (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index b77afccb..50458ab7 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -101,8 +101,11 @@ namespace Microsoft.Dafny.Triggers { // [∀ 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). - // The last thing that we ignore is matching variables against constants, - // to ensure that P(x) is not flagged as looping with P(0). + // In addition, we ignore cases where the only differences between a trigger + // and a trigger match are places where a variable is replaced with an + // expression whose free variables do not intersect that of the quantifier + // in which that expression is found. For examples of this behavious, see + // triggers/literals-do-not-cause-loops. // This ignoring logic is implemented by the CouldCauseLoops method. foreach (var q in quantifiers) { diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index dccd996d..d4a822a8 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -31,9 +31,15 @@ namespace Microsoft.Dafny.Triggers { return ExprExtensions.ExpressionEq(t1.Expr, t2.Expr); } - internal bool CouldCauseLoops(List terms) { + /// + /// This method checks whether this match could actually cause a loop, given a set of terms participating in a trigger; + /// to compute an answer, we match the Expr of this match against the Exprs of each of these term, allowing for harmless + /// variations. If any of these tests does match, this term likely won't cause a loop. + /// The boundVars list is useful to determine that forall x :: P(x) == P(y+z) does not loop. + /// + internal bool CouldCauseLoops(List terms, ISet boundVars) { var expr = Expr; - return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNamesAndConstants(expr)); + return !terms.Any(term => term.Expr.ExpressionEqModuloExpressionsNotInvolvingBoundVariables(expr, boundVars)); } } @@ -79,15 +85,22 @@ namespace Microsoft.Dafny.Triggers { return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEq(e1, e2)); } - internal static bool ExpressionEqModuloVariableNamesAndConstants(this Expression expr1, Expression expr2) { + internal static bool ExpressionEqModuloExpressionsNotInvolvingBoundVariables(this Expression expr1, Expression expr2, ISet boundVars) { expr1 = expr1.Resolved; expr2 = expr2.Resolved; if (expr1 is IdentifierExpr) { - return expr2 is IdentifierExpr || expr2 is LiteralExpr; + if (expr2 is IdentifierExpr) { + return true; + } else { + var freeInE2 = Translator.ComputeFreeVariables(expr2); + freeInE2.IntersectWith(boundVars); + return !freeInE2.Any(); + } } - return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNamesAndConstants(e1, e2)); + return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, + expr2.SubExpressions, (e1, e2) => ExpressionEqModuloExpressionsNotInvolvingBoundVariables(e1, e2, boundVars)); } internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet holes, Dictionary bindings) { diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index d78bcb9e..cc3b1978 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -69,7 +69,8 @@ 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 = this.MatchingSubterms(quantifier); - return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms)); + var boundVars = new HashSet(quantifier.BoundVars); + return matchingSubterms.Where(tm => tm.CouldCauseLoops(Terms, boundVars)); } internal List MatchingSubterms(QuantifierExpr quantifier) { diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy b/Test/triggers/loop-detection-is-not-too-strict.dfy index a5a30c81..81f764ad 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy @@ -7,8 +7,9 @@ // equal to that trigger, as long as the only differences are variable predicate P(x: int, y: int) +predicate Q(x: int) -method Test() { +method Test(z: int) { // P(x, y) and P(y, x) might look like they would cause a loop. Since they // only differ by their variables, though, they won't raise flags. assume forall x: int, y: int :: P(x, y) == P(y, x); @@ -18,4 +19,22 @@ method Test() { // Contrast with the following: assume forall x: int, y: int :: P(x, y) == P(x, y+1); + + // The following examples were made legal after an exchange where Chris + // pointed examples in the IronClad sources where things like this were + // incorrectly flagged. + assert forall x :: true || Q(x) || Q(0); + assert forall x :: true || Q(x) || Q(z); + assert forall x :: true || P(x, 1) || P(x, z); + + // Support for the following was added following a discussion with Rustan; in + // the second one the expression `if z > 1 then z else 3 * z + 1` is not + // directly a constant expression, but it does not involve x, so it's ok: + assert forall x :: true || Q(x) || Q(0+1); + assert forall x :: true || Q(x) || Q(if z > 1 then z else 3 * z + 1); + // Sanity check: + assert forall x :: true || Q(x) || Q(if z > 1 then x else 3 * z + 1); + + // WISH: It might also be good to zeta-reduce before loop detection. + assert forall x :: true || Q(x) || (var xx := x+1; Q(xx)); } diff --git a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect index 6f5ed3d7..705c2a8c 100644 --- a/Test/triggers/loop-detection-is-not-too-strict.dfy.expect +++ b/Test/triggers/loop-detection-is-not-too-strict.dfy.expect @@ -1,8 +1,17 @@ -loop-detection-is-not-too-strict.dfy(14,9): Info: Selected triggers: +loop-detection-is-not-too-strict.dfy(15,9): Info: Selected triggers: {P(y, x)}, {P(x, y)} -loop-detection-is-not-too-strict.dfy(17,9): Info: Selected triggers: +loop-detection-is-not-too-strict.dfy(18,9): Info: Selected triggers: {P(y, x)}, {P(x, y)} -loop-detection-is-not-too-strict.dfy(20,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)}) +loop-detection-is-not-too-strict.dfy(21,9): Warning: Selected triggers: {P(x, y)} (may loop with {P(x, y + 1)}) (!) Suppressing loops would leave this expression without triggers. +loop-detection-is-not-too-strict.dfy(26,9): Info: Selected triggers: {Q(x)} +loop-detection-is-not-too-strict.dfy(27,9): Info: Selected triggers: {Q(x)} +loop-detection-is-not-too-strict.dfy(28,9): Info: Selected triggers: + {P(x, z)}, {P(x, 1)} +loop-detection-is-not-too-strict.dfy(33,9): Info: Selected triggers: {Q(x)} +loop-detection-is-not-too-strict.dfy(34,9): Info: Selected triggers: {Q(x)} +loop-detection-is-not-too-strict.dfy(36,9): Warning: Selected triggers: {Q(x)} (may loop with {Q(if z > 1 then x else 3 * z + 1)}) + (!) Suppressing loops would leave this expression without triggers. +loop-detection-is-not-too-strict.dfy(39,9): Info: Selected triggers: {Q(x)} -Dafny program verifier finished with 3 verified, 0 errors +Dafny program verifier finished with 4 verified, 0 errors -- cgit v1.2.3 From 6f2504ad3b3046dbf58a3fd2c52325d3b2009428 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 20:51:43 -0700 Subject: Tiny cleanup in TriggersCollector --- Source/Dafny/Triggers/TriggersCollector.cs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index cc3b1978..c25f65b9 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -191,8 +191,13 @@ namespace Microsoft.Dafny.Triggers { expr.SubExpressions.Iter(e => Annotate(e)); TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort - if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MultiSelectExpr || expr is MemberSelectExpr || - expr is OldExpr || expr is ApplyExpr || expr is DisplayExpression || + if (expr is FunctionCallExpr || + expr is SeqSelectExpr || + expr is MultiSelectExpr || + expr is MemberSelectExpr || + expr is OldExpr || + expr is ApplyExpr || + expr is DisplayExpression || (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); -- cgit v1.2.3 From 23067608f2d8855abd64982cabfe7f0c7f8e4f5a Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 6 Nov 2015 13:51:08 -0800 Subject: Fix issue 99. When annotate a quantifier expr that has a SplitQuantifier, we need exclude the private terms (the ones that includes the quantifier expr's bv) from it exported terms. --- Source/Dafny/Triggers/TriggersCollector.cs | 4 ++-- Test/dafny4/Bug99.dfy | 11 +++++++++++ Test/dafny4/Bug99.dfy.expect | 2 ++ 3 files changed, 15 insertions(+), 2 deletions(-) create mode 100644 Test/dafny4/Bug99.dfy create mode 100644 Test/dafny4/Bug99.dfy.expect (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index c25f65b9..698ea3b5 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -201,8 +201,8 @@ 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 && ((QuantifierExpr)expr).SplitQuantifier == null) { - annotation = AnnotateQuantifier((QuantifierExpr)expr); + } else if (expr is QuantifierExpr) { + annotation = AnnotateQuantifier((QuantifierExpr)expr); } else if (expr is LetExpr) { annotation = AnnotateLetExpr((LetExpr)expr); } else if (expr is IdentifierExpr) { diff --git a/Test/dafny4/Bug99.dfy b/Test/dafny4/Bug99.dfy new file mode 100644 index 00000000..3f95ce9f --- /dev/null +++ b/Test/dafny4/Bug99.dfy @@ -0,0 +1,11 @@ +// RUN: %dafny /autoTriggers:1 /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +predicate P(e:int, p:int) { true } +predicate Q(i:int, t:int) + +lemma Tester(x:int) +{ + assert forall i :: Q(i, x) ==> (forall p {:trigger P(i, p)} :: P(i, p)); + +} diff --git a/Test/dafny4/Bug99.dfy.expect b/Test/dafny4/Bug99.dfy.expect new file mode 100644 index 00000000..73ba063c --- /dev/null +++ b/Test/dafny4/Bug99.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 4 verified, 0 errors -- cgit v1.2.3 From 18a231edf04437a0748d542d3114ed79899aa363 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Tue, 8 Dec 2015 15:15:21 -0800 Subject: Fix issue 114. Do not export private terms for ComprehensionExpr in trigger collectors. --- Source/Dafny/Triggers/TriggersCollector.cs | 7 +++++++ Test/dafny4/Bug114.dfy | 10 ++++++++++ Test/dafny4/Bug114.dfy.expect | 7 +++++++ 3 files changed, 24 insertions(+) create mode 100644 Test/dafny4/Bug114.dfy create mode 100644 Test/dafny4/Bug114.dfy.expect (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index 698ea3b5..f96d3e4c 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -209,6 +209,8 @@ namespace Microsoft.Dafny.Triggers { annotation = AnnotateIdentifier((IdentifierExpr)expr); } else if (expr is ApplySuffix) { annotation = AnnotateApplySuffix((ApplySuffix)expr); + } else if (expr is ComprehensionExpr) { + annotation = AnnotateComprehensionExpr((ComprehensionExpr)expr); } else if (expr is ConcreteSyntaxExpression || expr is LiteralExpr || expr is OldExpr || @@ -272,6 +274,11 @@ namespace Microsoft.Dafny.Triggers { return new TriggerAnnotation(false, Enumerable.Repeat(expr.Var, 1), null); } + private TriggerAnnotation AnnotateComprehensionExpr(ComprehensionExpr expr) { + var terms = CollectExportedCandidates(expr); + return new TriggerAnnotation(true, CollectVariables(expr), terms, OnlyPrivateCandidates(terms, expr.BoundVars)); + } + private TriggerAnnotation AnnotateOther(Expression expr, bool isTriggerKiller) { return new TriggerAnnotation(isTriggerKiller || CollectIsKiller(expr), CollectVariables(expr), CollectExportedCandidates(expr)); } diff --git a/Test/dafny4/Bug114.dfy b/Test/dafny4/Bug114.dfy new file mode 100644 index 00000000..1c0f0109 --- /dev/null +++ b/Test/dafny4/Bug114.dfy @@ -0,0 +1,10 @@ +// RUN: %dafny /compile:0 /autoTriggers:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function f1(d:int):map +function f2(y:int, d:int):int + +method M(m:map, d:int, x2:int) +{ + assert forall d :: f1(d) == (map x | x in m :: f2(x, d)); +} \ No newline at end of file diff --git a/Test/dafny4/Bug114.dfy.expect b/Test/dafny4/Bug114.dfy.expect new file mode 100644 index 00000000..8e671f90 --- /dev/null +++ b/Test/dafny4/Bug114.dfy.expect @@ -0,0 +1,7 @@ +Bug114.dfy(9,9): Error: assertion violation +Execution trace: + (0,0): anon0 + (0,0): anon3_Then + (0,0): anon2 + +Dafny program verifier finished with 3 verified, 1 error -- cgit v1.2.3 From e9c589851d913a6566c421c87483dc7e94519f91 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Mon, 8 Feb 2016 12:28:25 -0800 Subject: Fix issue 124. Consider math operators that later turned into function calls as candidates for triggers. --- Source/Dafny/Triggers/TriggersCollector.cs | 26 ++++++++++++++++++++++++++ Test/dafny4/Bug124.dfy | 14 ++++++++++++++ Test/dafny4/Bug124.dfy.expect | 2 ++ 3 files changed, 42 insertions(+) create mode 100644 Test/dafny4/Bug124.dfy create mode 100644 Test/dafny4/Bug124.dfy.expect (limited to 'Source/Dafny/Triggers/TriggersCollector.cs') diff --git a/Source/Dafny/Triggers/TriggersCollector.cs b/Source/Dafny/Triggers/TriggersCollector.cs index f96d3e4c..4204cc29 100644 --- a/Source/Dafny/Triggers/TriggersCollector.cs +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -198,6 +198,7 @@ namespace Microsoft.Dafny.Triggers { expr is OldExpr || expr is ApplyExpr || expr is DisplayExpression || + TranslateToFunctionCall(expr) || (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); @@ -227,6 +228,31 @@ namespace Microsoft.Dafny.Triggers { return annotation; } + // math operations can be turned into a Boogie-level function as in the + // case with /noNLarith. + public bool TranslateToFunctionCall(Expression expr) { + if (!(expr is BinaryExpr)) { + return false; + } + BinaryExpr e = (BinaryExpr) expr; + bool isReal = e.E0.Type.IsNumericBased(Type.NumericPersuation.Real); + switch (e.ResolvedOp) { + case BinaryExpr.ResolvedOpcode.Lt: + case BinaryExpr.ResolvedOpcode.Le: + case BinaryExpr.ResolvedOpcode.Ge: + case BinaryExpr.ResolvedOpcode.Gt: + case BinaryExpr.ResolvedOpcode.Add: + case BinaryExpr.ResolvedOpcode.Sub: + case BinaryExpr.ResolvedOpcode.Mul: + case BinaryExpr.ResolvedOpcode.Div: + case BinaryExpr.ResolvedOpcode.Mod: + if (!isReal && DafnyOptions.O.DisableNLarith) { + return true; + } + break; + } + return false; + } private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) { bool expr_is_killer = false; var new_expr = TriggerUtils.MaybeWrapInOld(TriggerUtils.PrepareExprForInclusionInTrigger(expr, out expr_is_killer), cache.exprsInOldContext.Contains(expr)); diff --git a/Test/dafny4/Bug124.dfy b/Test/dafny4/Bug124.dfy new file mode 100644 index 00000000..60f26a00 --- /dev/null +++ b/Test/dafny4/Bug124.dfy @@ -0,0 +1,14 @@ +// RUN: %dafny /compile:0 /autoTriggers:1 /noNLarith "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function power(n:nat, e:nat) : int + +lemma lemma_power() + ensures forall n:nat, e:nat :: 0 <= n * e && power(n, e) == 5; +{ + forall n:nat, e:nat + ensures 0 <= n * e && power(n, e) == 5; + { + assume false; + } +} \ No newline at end of file diff --git a/Test/dafny4/Bug124.dfy.expect b/Test/dafny4/Bug124.dfy.expect new file mode 100644 index 00000000..52595bf9 --- /dev/null +++ b/Test/dafny4/Bug124.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 3 verified, 0 errors -- cgit v1.2.3