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/TriggerExtensions.cs | 489 +++++++++++++++++++++++++++++ 1 file changed, 489 insertions(+) create mode 100644 Source/Dafny/Triggers/TriggerExtensions.cs (limited to 'Source/Dafny/Triggers/TriggerExtensions.cs') diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs new file mode 100644 index 00000000..7bebe1ac --- /dev/null +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -0,0 +1,489 @@ +#define THROW_UNSUPPORTED_COMPARISONS + +using Microsoft.Dafny; +using System; +using System.Collections.Generic; +using System.Diagnostics.Contracts; +using System.Linq; +using System.Text; + +namespace Microsoft.Dafny.Triggers { + internal static class DeduplicateExtension { + public static List Deduplicate(this IEnumerable seq, Func eq) { + List deduplicated = new List(); + + foreach (var elem in seq) { + if (!deduplicated.Any(other => eq(elem, other))) { + deduplicated.Add(elem); + } + } + + return deduplicated; + } + } + + internal static class ExprExtensions { + internal static IEnumerable AllSubExpressions(this Expression expr, bool strict = false) { + foreach (var subexpr in expr.SubExpressions) { + foreach (var r_subexpr in AllSubExpressions(subexpr, false)) { + yield return r_subexpr; + } + yield return subexpr; + } + + if (expr is StmtExpr) { + foreach (var r_subexpr in AllSubExpressions(((StmtExpr)expr).S, false)) { + yield return r_subexpr; + } + } + + if (!strict) { + yield return expr; + } + } + + internal static IEnumerable AllSubExpressions(this Statement stmt, bool strict = false) { + foreach (var subexpr in stmt.SubExpressions) { + foreach (var r_subexpr in AllSubExpressions(subexpr, false)) { + yield return r_subexpr; + } + yield return subexpr; + } + + foreach (var substmt in stmt.SubStatements) { + foreach (var r_subexpr in AllSubExpressions(substmt, false)) { + yield return r_subexpr; + } + } + } + + internal static bool ExpressionEq(this Expression expr1, Expression expr2) { + expr1 = expr1.Resolved; + expr2 = expr2.Resolved; + + return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEq(e1, e2)); + } + + internal static bool ExpressionEqModuloVariableNames(this Expression expr1, Expression expr2) { + expr1 = expr1.Resolved; + expr2 = expr2.Resolved; + + if (expr1 is IdentifierExpr) { + return expr2 is IdentifierExpr; + } + + 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) { + expr = expr.Resolved; + trigger = trigger.Resolved; + + if (trigger is IdentifierExpr) { + var var = ((IdentifierExpr)trigger).Var; + + if (holes.Contains(var)) { + Expression existing_binding = null; + if (bindings.TryGetValue(var, out existing_binding)) { + return ExpressionEq(expr, existing_binding); + } else { + bindings[var] = expr; + return true; + } + } + } + + 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; + } + + internal static IEnumerable SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) { + return quantifier.Term.AllSubExpressions() + .Select(e => e.MatchAgainst(trigger, new HashSet(quantifier.BoundVars))) + .Where(e => e.HasValue).Select(e => e.Value); + } + + private static bool ShallowSameAttributes(Attributes attributes1, Attributes attributes2) { + return TriggerUtils.SameLists(attributes1.AsEnumerable(), attributes2.AsEnumerable(), ShallowSameSingleAttribute); + } + + private static bool ShallowSameSingleAttribute(Attributes arg1, Attributes arg2) { + return arg1.Name == arg2.Name; + } + + private static bool SameBoundVar(IVariable arg1, IVariable arg2) { + return arg1 == arg2 || + (arg1.Name == arg2.Name && + arg1.CompileName == arg2.CompileName && + arg1.DisplayName == arg2.DisplayName && + arg1.UniqueName == arg2.UniqueName && + arg1.IsGhost == arg2.IsGhost && + arg1.IsMutable == arg2.IsMutable); //FIXME compare types? + } + + /// + /// Compares two abstract syntax expressions, looking only at their direct members. Subexpressions and substatements are not compared. + /// + /// + internal static bool ShallowEq_Top(Expression expr1, Expression expr2) { + Contract.Requires(expr1 != null); + Contract.Requires(expr2 != null); + + // We never compare concrete expressions + Contract.Requires(!(expr1 is ConcreteSyntaxExpression)); + Contract.Requires(!(expr2 is ConcreteSyntaxExpression)); + + // CPC: Hey future editor: the following block of code is auto-generated. Just add your own cases at the end. + // This could be a visitor pattern, except I need to visit a pair of nodes. + // It could also be implemented in each individual class. I'd have a slight preference for that. + // This really just wants to use double dispatch. + if (expr1 is UnboxingCastExpr && expr2 is UnboxingCastExpr) { + return ShallowEq((UnboxingCastExpr)expr1, (UnboxingCastExpr)expr2); + } else if (expr1 is BoxingCastExpr && expr2 is BoxingCastExpr) { + return ShallowEq((BoxingCastExpr)expr1, (BoxingCastExpr)expr2); + } else if (expr1 is MatchExpr && expr2 is MatchExpr) { + return ShallowEq((MatchExpr)expr1, (MatchExpr)expr2); + } else if (expr1 is ITEExpr && expr2 is ITEExpr) { + return ShallowEq((ITEExpr)expr1, (ITEExpr)expr2); + } else if (expr1 is StmtExpr && expr2 is StmtExpr) { + return ShallowEq((StmtExpr)expr1, (StmtExpr)expr2); + } else if (expr1 is WildcardExpr && expr2 is WildcardExpr) { + return ShallowEq((WildcardExpr)expr1, (WildcardExpr)expr2); + } else if (expr1 is ComprehensionExpr && expr2 is ComprehensionExpr) { + return ShallowEq((ComprehensionExpr)expr1, (ComprehensionExpr)expr2); + } else if (expr1 is NamedExpr && expr2 is NamedExpr) { + return ShallowEq((NamedExpr)expr1, (NamedExpr)expr2); + } else if (expr1 is LetExpr && expr2 is LetExpr) { + return ShallowEq((LetExpr)expr1, (LetExpr)expr2); + } else if (expr1 is TernaryExpr && expr2 is TernaryExpr) { + return ShallowEq((TernaryExpr)expr1, (TernaryExpr)expr2); + } else if (expr1 is BinaryExpr && expr2 is BinaryExpr) { + return ShallowEq((BinaryExpr)expr1, (BinaryExpr)expr2); + } else if (expr1 is UnaryExpr && expr2 is UnaryExpr) { + return ShallowEq((UnaryExpr)expr1, (UnaryExpr)expr2); + } else if (expr1 is MultiSetFormingExpr && expr2 is MultiSetFormingExpr) { + return ShallowEq((MultiSetFormingExpr)expr1, (MultiSetFormingExpr)expr2); + } else if (expr1 is OldExpr && expr2 is OldExpr) { + return ShallowEq((OldExpr)expr1, (OldExpr)expr2); + } else if (expr1 is FunctionCallExpr && expr2 is FunctionCallExpr) { + return ShallowEq((FunctionCallExpr)expr1, (FunctionCallExpr)expr2); + } else if (expr1 is ApplyExpr && expr2 is ApplyExpr) { + return ShallowEq((ApplyExpr)expr1, (ApplyExpr)expr2); + } else if (expr1 is SeqUpdateExpr && expr2 is SeqUpdateExpr) { + return ShallowEq((SeqUpdateExpr)expr1, (SeqUpdateExpr)expr2); + } else if (expr1 is MultiSelectExpr && expr2 is MultiSelectExpr) { + return ShallowEq((MultiSelectExpr)expr1, (MultiSelectExpr)expr2); + } else if (expr1 is SeqSelectExpr && expr2 is SeqSelectExpr) { + return ShallowEq((SeqSelectExpr)expr1, (SeqSelectExpr)expr2); + } else if (expr1 is MemberSelectExpr && expr2 is MemberSelectExpr) { + return ShallowEq((MemberSelectExpr)expr1, (MemberSelectExpr)expr2); + } else if (expr1 is MapDisplayExpr && expr2 is MapDisplayExpr) { //Note: MapDisplayExpr is not a DisplayExpression + return ShallowEq((MapDisplayExpr)expr1, (MapDisplayExpr)expr2); + } else if (expr1 is DisplayExpression && expr2 is DisplayExpression) { + return ShallowEq((DisplayExpression)expr1, (DisplayExpression)expr2); + } else if (expr1 is IdentifierExpr && expr2 is IdentifierExpr) { + return ShallowEq((IdentifierExpr)expr1, (IdentifierExpr)expr2); + } else if (expr1 is ThisExpr && expr2 is ThisExpr) { + return ShallowEq((ThisExpr)expr1, (ThisExpr)expr2); + } else if (expr1 is DatatypeValue && expr2 is DatatypeValue) { + return ShallowEq((DatatypeValue)expr1, (DatatypeValue)expr2); + } else if (expr1 is LiteralExpr && expr2 is LiteralExpr) { + return ShallowEq((LiteralExpr)expr1, (LiteralExpr)expr2); + } else { + // If this assertion fail, then a new abstract AST node was probably introduced but not registered here. + Contract.Assert(expr1.GetType() != expr2.GetType()); + return false; + } + } + + private static bool ShallowEq(UnboxingCastExpr expr1, UnboxingCastExpr expr2) { + Contract.Requires(false); + throw new InvalidOperationException(); + } + + private static bool ShallowEq(BoxingCastExpr expr1, BoxingCastExpr expr2) { + return expr1.FromType == expr2.FromType && + expr1.ToType == expr2.ToType; + } + + private static bool ShallowEq(MatchExpr expr1, MatchExpr expr2) { + return true; + } + + private static bool ShallowEq(ITEExpr expr1, ITEExpr expr2) { + return true; + } + + private static bool ShallowEq(StmtExpr expr1, StmtExpr expr2) { +#if THROW_UNSUPPORTED_COMPARISONS + Contract.Assume(false); // This kind of expression never appears in a trigger + throw new NotImplementedException(); +#else + return expr1.S == expr2.S; +#endif + } + + private static bool ShallowEq(WildcardExpr expr1, WildcardExpr expr2) { + return true; + } + + private static bool ShallowEq(LambdaExpr expr1, LambdaExpr expr2) { +#if THROW_UNSUPPORTED_COMPARISONS + Contract.Assume(false); // This kind of expression never appears in a trigger + throw new NotImplementedException(); +#else + return false; +#endif + } + + private static bool ShallowEq(MapComprehension expr1, MapComprehension expr2) { + return expr1.Finite == expr2.Finite; + } + + private static bool ShallowEq(SetComprehension expr1, SetComprehension expr2) { + return expr1.TermIsImplicit == expr2.TermIsImplicit && //TODO + expr1.Finite == expr2.Finite; + } + + private static bool ShallowEq(ExistsExpr expr1, ExistsExpr expr2) { + return true; + } + + private static bool ShallowEq(ForallExpr expr1, ForallExpr expr2) { + return true; + } + + private static bool ShallowEq(QuantifierExpr expr1, QuantifierExpr expr2) { //FIXME are these TypeArgs still useful? + if (expr1.TypeArgs.Count != expr2.TypeArgs.Count || + !TriggerUtils.SameNullity(expr1.Range, expr2.Range)) { + return false; + } + + if (expr1 is ExistsExpr && expr2 is ExistsExpr) { + return ShallowEq((ExistsExpr)expr1, (ExistsExpr)expr2); + } else if (expr1 is ForallExpr && expr2 is ForallExpr) { + return ShallowEq((ForallExpr)expr1, (ForallExpr)expr2); + } else { + return false; + } + } + + private static bool ShallowEq(ComprehensionExpr expr1, ComprehensionExpr expr2) { + if (!TriggerUtils.SameLists(expr1.BoundVars, expr2.BoundVars, SameBoundVar) || + !ShallowSameAttributes(expr1.Attributes, expr2.Attributes) || + // Filled in during resolution: !SameLists(expr1.Bounds, expr2.Bounds, ReferenceCompare) || + // !SameLists(expr1.MissingBounds, expr2.MissingBounds, SameBoundVar) || + !TriggerUtils.SameNullity(expr1.Range, expr2.Range)) { //TODO Check + return false; + } + + if (expr1 is LambdaExpr && expr2 is LambdaExpr) { + return ShallowEq((LambdaExpr)expr1, (LambdaExpr)expr2); + } else if (expr1 is MapComprehension && expr2 is MapComprehension) { + return ShallowEq((MapComprehension)expr1, (MapComprehension)expr2); + } else if (expr1 is SetComprehension && expr2 is SetComprehension) { + return ShallowEq((SetComprehension)expr1, (SetComprehension)expr2); + } else if (expr1 is QuantifierExpr && expr2 is QuantifierExpr) { + return ShallowEq((QuantifierExpr)expr1, (QuantifierExpr)expr2); + } else { + return false; // ComprehensionExpr is abstract + } + } + + private static bool ShallowEq(NamedExpr expr1, NamedExpr expr2) { + return expr1.Name == expr2.Name && + TriggerUtils.SameNullity(expr1.Contract, expr2.Contract); + } + + private static bool ShallowEq(LetExpr expr1, LetExpr expr2) { + return expr1.Exact == expr2.Exact && + ShallowSameAttributes(expr1.Attributes, expr2.Attributes); + } + + private static bool ShallowEq(TernaryExpr expr1, TernaryExpr expr2) { + return expr1.Op == expr2.Op; + } + + private static bool ShallowEq(BinaryExpr expr1, BinaryExpr expr2) { + Contract.Requires(expr1.ResolvedOp != BinaryExpr.ResolvedOpcode.YetUndetermined); + Contract.Requires(expr2.ResolvedOp != BinaryExpr.ResolvedOpcode.YetUndetermined); + return expr1.ResolvedOp == expr2.ResolvedOp; + } + + private static bool ShallowEq(ConversionExpr expr1, ConversionExpr expr2) { + return expr1.Type == expr2.Type; //TODO equality on types? + } + + private static bool ShallowEq(UnaryOpExpr expr1, UnaryOpExpr expr2) { + return expr1.Op == expr2.Op; + } + + private static bool ShallowEq(UnaryExpr expr1, UnaryExpr expr2) { + if (expr1 is ConversionExpr && expr2 is ConversionExpr) { + return ShallowEq((ConversionExpr)expr1, (ConversionExpr)expr2); + } else if (expr1 is UnaryOpExpr && expr2 is UnaryOpExpr) { + return ShallowEq((UnaryOpExpr)expr1, (UnaryOpExpr)expr2); + } else { + return false; // UnaryExpr is abstract + } + } + + private static bool ShallowEq(MultiSetFormingExpr expr1, MultiSetFormingExpr expr2) { + return true; + } + + private static bool ShallowEq(OldExpr expr1, OldExpr expr2) { + return true; + } + + private static bool ShallowEq(FunctionCallExpr expr1, FunctionCallExpr expr2) { + return expr1.Name == expr2.Name && + expr1.CoCall == expr2.CoCall && //TODO + expr1.Function == expr2.Function; // TODO TypeArgumentSubstitutions? + } + + private static bool ShallowEq(ApplyExpr expr1, ApplyExpr expr2) { + return true; + } + + private static bool ShallowEq(SeqUpdateExpr expr1, SeqUpdateExpr expr2) { + Contract.Requires(expr1.ResolvedUpdateExpr != null && expr2.ResolvedUpdateExpr != null); + return true; + } + + private static bool ShallowEq(MultiSelectExpr expr1, MultiSelectExpr expr2) { + return true; + } + + private static bool ShallowEq(SeqSelectExpr expr1, SeqSelectExpr expr2) { + return expr1.SelectOne == expr2.SelectOne && + TriggerUtils.SameNullity(expr1.Seq, expr2.Seq) && + TriggerUtils.SameNullity(expr1.E0, expr2.E0) && + TriggerUtils.SameNullity(expr1.E1, expr2.E1); + } + + private static bool ShallowEq(MemberSelectExpr expr1, MemberSelectExpr expr2) { + return expr1.MemberName == expr2.MemberName && + expr1.Member == expr2.Member && + TriggerUtils.SameLists(expr1.TypeApplication, expr2.TypeApplication, Microsoft.Dafny.Type.Equals); + } + + private static bool ShallowEq(SeqDisplayExpr expr1, SeqDisplayExpr expr2) { + return true; + } + + private static bool ShallowEq(MapDisplayExpr expr1, MapDisplayExpr expr2) { + return expr1.Finite == expr2.Finite; + } + + private static bool ShallowEq(MultiSetDisplayExpr expr1, MultiSetDisplayExpr expr2) { + return true; + } + + private static bool ShallowEq(SetDisplayExpr expr1, SetDisplayExpr expr2) { + return expr1.Finite == expr2.Finite; + } + + private static bool ShallowEq(DisplayExpression expr1, DisplayExpression expr2) { + if (expr1 is SeqDisplayExpr && expr2 is SeqDisplayExpr) { + return ShallowEq((SeqDisplayExpr)expr1, (SeqDisplayExpr)expr2); + } else if (expr1 is MultiSetDisplayExpr && expr2 is MultiSetDisplayExpr) { + return ShallowEq((MultiSetDisplayExpr)expr1, (MultiSetDisplayExpr)expr2); + } else if (expr1 is SetDisplayExpr && expr2 is SetDisplayExpr) { + return ShallowEq((SetDisplayExpr)expr1, (SetDisplayExpr)expr2); + } else { + return false; + } + } + + private static bool ShallowEq(AutoGhostIdentifierExpr expr1, AutoGhostIdentifierExpr expr2) { + return true; + } + + private static bool ShallowEq(IdentifierExpr expr1, IdentifierExpr expr2) { + if (expr1.Name != expr2.Name || + expr1.Var != expr2.Var) { + return false; + } + + if (expr1 is AutoGhostIdentifierExpr && expr2 is AutoGhostIdentifierExpr) { + return ShallowEq((AutoGhostIdentifierExpr)expr1, (AutoGhostIdentifierExpr)expr2); + } else { + return true; + } + } + + private static bool ShallowEq(ImplicitThisExpr expr1, ImplicitThisExpr expr2) { + return true; + } + + private static bool ShallowEq(ThisExpr expr1, ThisExpr expr2) { + if (expr1 is ImplicitThisExpr && expr2 is ImplicitThisExpr) { + return ShallowEq((ImplicitThisExpr)expr1, (ImplicitThisExpr)expr2); + } else { + return (expr1.GetType() == expr2.GetType()); // LiteralExpr is not abstract + } + } + + private static bool ShallowEq(DatatypeValue expr1, DatatypeValue expr2) { + return // Implied by Ctor equality: expr1.DatatypeName == expr2.DatatypeName && + // Implied by Ctor equality: expr1.MemberName == expr2.MemberName && + expr1.Ctor == expr2.Ctor && + // Contextual information: expr1.IsCoCall == expr2.IsCoCall && + TriggerUtils.SameLists(expr1.InferredTypeArgs, expr2.InferredTypeArgs, Microsoft.Dafny.Type.Equals); + } + + private static bool ShallowEq(StringLiteralExpr expr1, StringLiteralExpr expr2) { + return true; + } + + private static bool ShallowEq(CharLiteralExpr expr1, CharLiteralExpr expr2) { + return true; + } + + private static bool ShallowEq(StaticReceiverExpr expr1, StaticReceiverExpr expr2) { + return true; + } + + private static bool ShallowEq(LiteralExpr expr1, LiteralExpr expr2) { + if (expr1.Value != expr2.Value) { + return false; + } + + if (expr1 is StringLiteralExpr && expr2 is StringLiteralExpr) { + return ShallowEq((StringLiteralExpr)expr1, (StringLiteralExpr)expr2); + } else if (expr1 is CharLiteralExpr && expr2 is CharLiteralExpr) { + return ShallowEq((CharLiteralExpr)expr1, (CharLiteralExpr)expr2); + } else if (expr1 is StaticReceiverExpr && expr2 is StaticReceiverExpr) { + return ShallowEq((StaticReceiverExpr)expr1, (StaticReceiverExpr)expr2); + } else { + return (expr1.GetType() == expr2.GetType()); // LiteralExpr is not abstract + } + } + } +} -- 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/TriggerExtensions.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/TriggerExtensions.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/TriggerExtensions.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 c311617de4641a4eef54a0ce1bc51574effa2756 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Wed, 19 Aug 2015 15:58:36 -0700 Subject: Fix the equality test for literal expressions (compare by value, not by reference to boxed value) --- Source/Dafny/Triggers/TriggerExtensions.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Source/Dafny/Triggers/TriggerExtensions.cs') diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index 0a0ad547..a49ed13a 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -477,7 +477,7 @@ namespace Microsoft.Dafny.Triggers { } private static bool ShallowEq(LiteralExpr expr1, LiteralExpr expr2) { - if (expr1.Value != expr2.Value) { + if (!TriggerUtils.SameNullity(expr1.Value, expr2.Value) || (expr1.Value != null && !expr1.Value.Equals(expr2.Value))) { return false; } -- 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/TriggerExtensions.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 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/TriggerExtensions.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 5b62a70205871f5f4d62db5247f11ac6c53fc57e Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Sat, 22 Aug 2015 15:39:50 -0700 Subject: Look at the full quantifier to find loops, not just the term. --- Source/Dafny/Triggers/TriggerExtensions.cs | 2 +- Test/triggers/loop-detection-looks-at-ranges-too.dfy | 14 ++++++++++++++ .../triggers/loop-detection-looks-at-ranges-too.dfy.expect | 6 ++++++ 3 files changed, 21 insertions(+), 1 deletion(-) create mode 100644 Test/triggers/loop-detection-looks-at-ranges-too.dfy create mode 100644 Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect (limited to 'Source/Dafny/Triggers/TriggerExtensions.cs') diff --git a/Source/Dafny/Triggers/TriggerExtensions.cs b/Source/Dafny/Triggers/TriggerExtensions.cs index 02deb92f..71414eee 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -121,7 +121,7 @@ namespace Microsoft.Dafny.Triggers { } internal static IEnumerable SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) { - return quantifier.Term.AllSubExpressions(true, false) //FIXME should loop detection actually pass true here? + return quantifier.AllSubExpressions(true, true) .Select(e => TriggerUtils.PrepareExprForInclusionInTrigger(e).MatchAgainst(trigger, quantifier.BoundVars, e)) .Where(e => e.HasValue).Select(e => e.Value); } diff --git a/Test/triggers/loop-detection-looks-at-ranges-too.dfy b/Test/triggers/loop-detection-looks-at-ranges-too.dfy new file mode 100644 index 00000000..7a99ea2d --- /dev/null +++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy @@ -0,0 +1,14 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This file checks that loops between the range and the term of a quantifier +// are properly detected. + +predicate P(x: int) + +method M(x: int) { + // This will be flagged as a loop even without looking at the range + assert true || forall x: int | P(x) :: P(x+1); + // This requires checking the range for looping terms + assert true || forall x: int | P(x+1) :: P(x); +} diff --git a/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect new file mode 100644 index 00000000..72482de5 --- /dev/null +++ b/Test/triggers/loop-detection-looks-at-ranges-too.dfy.expect @@ -0,0 +1,6 @@ +loop-detection-looks-at-ranges-too.dfy(11,17): Warning: Selected triggers: {P(x)} (loops with {P(x + 1)}) + (!) Suppressing loops would leave this expression without triggers. +loop-detection-looks-at-ranges-too.dfy(13,17): Warning: Selected triggers: {P(x)} (loops with {P(x + 1)}) + (!) Suppressing loops would leave this expression without triggers. + +Dafny program verifier finished with 3 verified, 0 errors -- cgit v1.2.3 From 7a993f6c87eaa82f383b1c5e7411f1878d4edf30 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 27 Aug 2015 16:10:25 -0700 Subject: Small fix: there is no loop in (forall x :: Q(x) && Q(0)) Again, spotted by Chris :) --- Source/Dafny/Triggers/QuantifiersCollection.cs | 4 +++- Source/Dafny/Triggers/TriggerExtensions.cs | 8 ++++---- Test/triggers/redundancy-detection-is-bidirectional.dfy | 2 +- 3 files changed, 8 insertions(+), 6 deletions(-) (limited to 'Source/Dafny/Triggers/TriggerExtensions.cs') diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs index 114d5f5d..b77afccb 100644 --- a/Source/Dafny/Triggers/QuantifiersCollection.cs +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -100,7 +100,9 @@ namespace Microsoft.Dafny.Triggers { // 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 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). // 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 71414eee..dccd996d 100644 --- a/Source/Dafny/Triggers/TriggerExtensions.cs +++ b/Source/Dafny/Triggers/TriggerExtensions.cs @@ -33,7 +33,7 @@ namespace Microsoft.Dafny.Triggers { internal bool CouldCauseLoops(List terms) { var expr = Expr; - return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNames(expr)); + return !terms.Any(term => term.Expr.ExpressionEqModuloVariableNamesAndConstants(expr)); } } @@ -79,15 +79,15 @@ namespace Microsoft.Dafny.Triggers { return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEq(e1, e2)); } - internal static bool ExpressionEqModuloVariableNames(this Expression expr1, Expression expr2) { + internal static bool ExpressionEqModuloVariableNamesAndConstants(this Expression expr1, Expression expr2) { expr1 = expr1.Resolved; expr2 = expr2.Resolved; if (expr1 is IdentifierExpr) { - return expr2 is IdentifierExpr; + return expr2 is IdentifierExpr || expr2 is LiteralExpr; } - return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNames(e1, e2)); + return ShallowEq_Top(expr1, expr2) && TriggerUtils.SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNamesAndConstants(e1, e2)); } internal static bool MatchesTrigger(this Expression expr, Expression trigger, ISet holes, Dictionary bindings) { diff --git a/Test/triggers/redundancy-detection-is-bidirectional.dfy b/Test/triggers/redundancy-detection-is-bidirectional.dfy index df1d78c3..06541b70 100644 --- a/Test/triggers/redundancy-detection-is-bidirectional.dfy +++ b/Test/triggers/redundancy-detection-is-bidirectional.dfy @@ -1,7 +1,7 @@ // 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 +// This test checks for tricky cases of redundancy suppression when building // triggers. predicate P(x: int, y: int) -- 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/TriggerExtensions.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