diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 10:51:44 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-19 10:51:44 -0700 |
| commit | 674e30357980e1192ac532f4bd16c529cedc7fdc (patch) | |
| tree | 583d3eca7e0d40bb4753f25d4dbb3069e3dea9b5 | |
| parent | 8a0df70ffb8d57d1bd210ce2e1c9522ba0967365 (diff) | |
Draft out a more advanced version of trigger generation
This new version will include a cleaner pipeline, and trigger splitting.
| -rw-r--r-- | Source/Dafny/DafnyPipeline.csproj | 7 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 46 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/TriggerGenerator.cs | 1064 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/QuantifierSplitter.cs | 66 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/QuantifiersCollection.cs | 104 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/TriggerExtensions.cs | 489 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/TriggerGenerator.cs | 28 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/TriggerUtils.cs | 94 | ||||
| -rw-r--r-- | Source/Dafny/Triggers/TriggersCollector.cs | 256 | ||||
| -rw-r--r-- | Test/dafny0/SeqFromArray.dfy.expect | 3 |
11 files changed, 1089 insertions, 1072 deletions
diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj index 626bb26a..5a824c36 100644 --- a/Source/Dafny/DafnyPipeline.csproj +++ b/Source/Dafny/DafnyPipeline.csproj @@ -144,7 +144,12 @@ <ItemGroup>
<Compile Include="Cloner.cs" />
<Compile Include="Reporting.cs" />
- <Compile Include="TriggerGenerator.cs" />
+ <Compile Include="Triggers\QuantifiersCollection.cs" />
+ <Compile Include="Triggers\QuantifierSplitter.cs" />
+ <Compile Include="Triggers\TriggerExtensions.cs" />
+ <Compile Include="Triggers\TriggerGenerator.cs" />
+ <Compile Include="Triggers\TriggersCollector.cs" />
+ <Compile Include="Triggers\TriggerUtils.cs" />
<Compile Include="Util.cs" />
<Compile Include="Compiler.cs" />
<Compile Include="BigIntegerParser.cs" />
diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs index cb71b80d..4e274189 100644 --- a/Source/Dafny/Rewriter.cs +++ b/Source/Dafny/Rewriter.cs @@ -39,22 +39,56 @@ namespace Microsoft.Dafny }
public class TriggerGeneratingRewriter : IRewriter {
+ Triggers.QuantifierCollectionsFinder finder;
+
internal TriggerGeneratingRewriter(ErrorReporter reporter) : base(reporter) {
Contract.Requires(reporter != null);
+ this.finder = new Triggers.QuantifierCollectionsFinder(reporter);
+ }
+
+ internal override void PostResolve(ModuleDefinition m) {
+ foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) { //CLEMENT
+ if (decl is Function) {
+ var function = (Function)decl;
+ finder.Visit(function.Ens, null);
+ finder.Visit(function.Req, null);
+ if (function.Body != null) {
+ finder.Visit(function.Body, null);
+ }
+ } else if (decl is Method) {
+ var method = (Method)decl;
+ finder.Visit(method.Ens, null);
+ finder.Visit(method.Req, null);
+ if (method.Body != null) {
+ finder.Visit(method.Body, null);
+ }
+ }
+ }
+ }
+ }
+
+ internal class QuantifierSplittingRewriter : IRewriter {
+ internal QuantifierSplittingRewriter(ErrorReporter reporter) : base(reporter) {
+ Contract.Requires(reporter != null);
}
internal override void PostResolve(ModuleDefinition m) {
+ var splitter = new Triggers.QuantifierSplitter();
foreach (var decl in ModuleDefinition.AllCallables(m.TopLevelDecls)) {
if (decl is Function) {
var function = (Function)decl;
- //TriggerGenerator.AddTriggers(function.Ens, Resolver);
- //TriggerGenerator.AddTriggers(function.Req, Resolver);
- //TriggerGenerator.AddTriggers(function.Body, Resolver);
+ splitter.Visit(function.Ens);
+ splitter.Visit(function.Req);
+ if (function.Body != null) {
+ splitter.Visit(function.Body);
+ }
} else if (decl is Method) {
var method = (Method)decl;
- //TriggerGenerator.AddTriggers(method.Ens, Resolver);
- //TriggerGenerator.AddTriggers(method.Req, Resolver);
- //TriggerGenerator.AddTriggers(method.Body, Resolver);
+ splitter.Visit(method.Ens);
+ splitter.Visit(method.Req);
+ if (method.Body != null) {
+ splitter.Visit(method.Body);
+ }
}
}
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 039aa56f..b5d89abd 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -12895,6 +12895,8 @@ namespace Microsoft.Dafny { // that needed to be proved about the function was proved already in the previous module, even without the body definition).
} else if (!FunctionBodyIsAvailable(f, currentModule)) {
// Don't inline opaque functions or foreign protected functions
+ } else if (Attributes.Contains(f.Attributes, "no_inline")) {
+ // User manually prevented inlining
} else if (CanSafelyInline(fexp, f)) {
// inline this body
var body = GetSubstitutedBody(fexp, f, false);
@@ -13106,7 +13108,7 @@ namespace Microsoft.Dafny { }
private bool CanSafelySubstitute(ISet<IVariable> protectedVariables, IVariable variable, Expression substitution) {
- return !(protectedVariables.Contains(variable) && TriggerGenerator.IsTriggerKiller(substitution));
+ return !(protectedVariables.Contains(variable) && Dafny.Triggers.TriggersCollector.IsTriggerKiller(substitution));
}
private class VariablesCollector: BottomUpVisitor {
diff --git a/Source/Dafny/TriggerGenerator.cs b/Source/Dafny/TriggerGenerator.cs deleted file mode 100644 index 04d96b01..00000000 --- a/Source/Dafny/TriggerGenerator.cs +++ /dev/null @@ -1,1064 +0,0 @@ -// #define DEBUG_AUTO_TRIGGERS
-#define THROW_UNSUPPORTED_COMPARISONS
-
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using Microsoft.Boogie;
-using System.Diagnostics.Contracts;
-using System.Text;
-using System.Diagnostics;
-
-//FIXME Generated triggers should be _triggers
-//FIXME: When scoring, do not consider old(x) to be higher than x.
-
-/* High level note: There are really two processes going on here. One is finding quantifiers;
- * the other is walking the subtree corresponding to each quantifier, and finding trigger candidates.
- * These two processes are interleaved, because we can look for trigger candidates as we look for
- * quantifiers. Since the visitor starts from the bottom of the tree, the recursive annotation
- * procedure never causes deep recursion; every call it makes hits the cache that has been built
- * during the visiting of lower level nodes.
- *
- * Note also that it wouldn't be enough to just use the recursive procedure: it doesn't visit
- * statements, for example.
- */
-
-namespace Microsoft.Dafny {
- class TriggerCandidate {
- internal Expression Expr;
- internal ISet<IVariable> Variables;
- internal List<ExprExtensions.TriggerMatch> MatchesInQuantifierBody;
-
- public override string ToString() {
- return Printer.ExprToString(Expr);
- }
- }
-
- class MultiTriggerCandidate {
- internal List<TriggerCandidate> Candidates;
- internal List<string> Tags;
- internal double Score;
-
- private List<ExprExtensions.TriggerMatch> potentialMatchingLoops;
- internal List<ExprExtensions.TriggerMatch> PotentialMatchingLoops {
- get {
- if (potentialMatchingLoops == null) {
- //FIXME could be optimized by looking at the bindings instead of doing full equality
- var candidates = Candidates.Deduplicate((x, y) => ExprExtensions.ExpressionEq(x.Expr, y.Expr));
- potentialMatchingLoops = candidates.SelectMany(candidate => candidate.MatchesInQuantifierBody)
- .Deduplicate((x, y) => ExprExtensions.ExpressionEq(x.Expr, y.Expr)).Where(tm => tm.CouldCauseLoops(candidates)).ToList();
- }
-
- return potentialMatchingLoops;
- }
- }
-
- internal MultiTriggerCandidate(List<TriggerCandidate> candidates) {
- Candidates = candidates;
- Tags = new List<string>();
- }
-
- internal bool MentionsAll(List<BoundVar> vars) {
- var candidates = Candidates;
- return vars.All(x => candidates.Any(candidate => candidate.Variables.Contains(x))); //TODO Perfs?
- }
-
- public override string ToString() {
- return String.Format("[{0:G2}] {1}", Score, String.Join(", ", Candidates));
- }
-
- public String AsDafnyAttributeString(bool wrap = true, bool includeTags = false) {
- var repr = Candidates.MapConcat(t => Printer.ExprToString(t.Expr), ", ");
- if (wrap) {
- repr = "{:trigger " + repr + "}";
- }
- if (includeTags && Tags != null) {
- repr += " (" + String.Join("; ", Tags) + ")";
- }
- return repr;
- }
- }
-
-
- class TriggerAnnotation {
- internal bool IsTriggerKiller;
- internal ISet<IVariable> Variables;
- internal readonly List<TriggerCandidate> PrivateCandidates;
- internal readonly List<TriggerCandidate> ExportedCandidates;
-
- internal TriggerAnnotation(bool IsTriggerKiller, IEnumerable<IVariable> Variables,
- IEnumerable<TriggerCandidate> AllCandidates, IEnumerable<TriggerCandidate> PrivateCandidates = null) {
- this.IsTriggerKiller = IsTriggerKiller;
- this.Variables = new HashSet<IVariable>(Variables);
-
- this.PrivateCandidates = new List<TriggerCandidate>(PrivateCandidates == null ? Enumerable.Empty<TriggerCandidate>() : PrivateCandidates);
- this.ExportedCandidates = new List<TriggerCandidate>(AllCandidates == null ? Enumerable.Empty<TriggerCandidate>() : AllCandidates.Except(this.PrivateCandidates));
- }
-
- public override string ToString() {
- StringBuilder sb = new StringBuilder();
- string indent = " {0}", nindent = "\n - {0}", subindent = "\n * {0}";
-
- sb.AppendFormat(indent, IsTriggerKiller);
-
- sb.AppendFormat(nindent, "Variables:");
- foreach (var bv in Variables) {
- sb.AppendFormat(subindent, bv.Name);
- }
-
- sb.AppendFormat(nindent, "Exported candidates:");
- foreach (var candidate in ExportedCandidates) {
- sb.AppendFormat(subindent, candidate);
- }
-
- if (PrivateCandidates.Any()) {
- sb.AppendFormat(nindent, "Private candidates:");
- foreach (var candidate in PrivateCandidates) {
- sb.AppendFormat(subindent, candidate);
- }
- }
-
- return sb.ToString();
- }
- }
-
- public class TriggerGenerator : BottomUpVisitor {
- List<QuantifierExpr> quantifiers;
- Dictionary<Expression, TriggerAnnotation> annotations;
-
- Action<IToken, string, int> AdditionalInformationReporter;
-
- private TriggerGenerator(Action<IToken, string, int> additionalInformationReporter) {
- Contract.Requires(additionalInformationReporter != null);
- this.quantifiers = new List<QuantifierExpr>();
- this.annotations = new Dictionary<Expression, TriggerAnnotation>();
- this.AdditionalInformationReporter = additionalInformationReporter;
- }
-
- private List<T> MergeAlterFirst<T>(List<T> a, List<T> b) {
- Contract.Requires(a != null);
- Contract.Requires(b != null);
- a.AddRange(b);
- return a;
- }
-
- private ISet<T> MergeAlterFirst<T>(ISet<T> a, ISet<T> b) {
- Contract.Requires(a != null);
- Contract.Requires(b != null);
- a.UnionWith(b);
- return a;
- }
-
- private T ReduceAnnotatedSubExpressions<T>(Expression expr, T seed, Func<TriggerAnnotation, T> map, Func<T, T, T> reduce) {
- return expr.SubExpressions.Select(e => map(Annotate(e)))
- .Aggregate(seed, (acc, e) => reduce(acc, e));
- }
-
- private List<TriggerCandidate> CollectExportedCandidates(Expression expr) {
- return ReduceAnnotatedSubExpressions<List<TriggerCandidate>>(expr, new List<TriggerCandidate>(), a => a.ExportedCandidates, MergeAlterFirst);
- }
-
- private ISet<IVariable> CollectVariables(Expression expr) {
- return ReduceAnnotatedSubExpressions(expr, new HashSet<IVariable>(), a => a.Variables, MergeAlterFirst);
- }
-
- private bool CollectIsKiller(Expression expr) {
- return ReduceAnnotatedSubExpressions(expr, false, a => a.IsTriggerKiller, (a, b) => a || b);
- }
-
- private IEnumerable<TriggerCandidate> OnlyPrivateCandidates(List<TriggerCandidate> candidates, IEnumerable<IVariable> privateVars) {
- return candidates.Where(c => privateVars.Intersect(c.Variables).Any()); //TODO Check perf
- }
-
- private TriggerAnnotation Annotate(Expression expr) {
- TriggerAnnotation cached;
- if (annotations.TryGetValue(expr, out cached)) {
- return cached;
- }
-
- expr.SubExpressions.Iter(e => Annotate(e)); //NOTE: These values are all cached
-
- TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort
- if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MemberSelectExpr || expr is OldExpr ||
- (expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh oesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944
- (expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) {
- annotation = AnnotatePotentialCandidate(expr);
- } else if (expr is QuantifierExpr) {
- annotation = AnnotateQuantifier((QuantifierExpr)expr);
- } else if (expr is LetExpr) {
- annotation = AnnotateLetExpr((LetExpr)expr);
- } else if (expr is IdentifierExpr) {
- annotation = AnnotateIdentifier((IdentifierExpr)expr);
- } else if (expr is ApplySuffix) {
- annotation = AnnotateApplySuffix((ApplySuffix)expr);
- } else if (expr is ConcreteSyntaxExpression ||
- expr is LiteralExpr ||
- expr is OldExpr ||
- expr is ThisExpr ||
- expr is BoxingCastExpr ||
- expr is DatatypeValue) {
- annotation = AnnotateOther(expr, false);
- } else {
- annotation = AnnotateOther(expr, true);
- }
-
- DebugTriggers("{0} ({1})\n{2}", Printer.ExprToString(expr), expr.GetType(), annotation);
- annotations[expr] = annotation;
- return annotation;
- }
-
- [Conditional("DEBUG_AUTO_TRIGGERS")]
- private static void DebugTriggers(string format, params object[] more) {
- Console.Error.WriteLine(format, more);
- }
-
- private BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) {
- switch(opcode) {
- case BinaryExpr.ResolvedOpcode.NotInMap:
- return BinaryExpr.ResolvedOpcode.InMap;
- case BinaryExpr.ResolvedOpcode.NotInSet:
- return BinaryExpr.ResolvedOpcode.InSet;
- case BinaryExpr.ResolvedOpcode.NotInSeq:
- return BinaryExpr.ResolvedOpcode.InSeq;
- case BinaryExpr.ResolvedOpcode.NotInMultiSet:
- return BinaryExpr.ResolvedOpcode.InMultiSet;
- }
-
- Contract.Assert(false);
- throw new ArgumentException();
- }
-
- private Expression CleanupExpr(Expression expr, out bool isKiller) {
- isKiller = false;
-
- if (!(expr is BinaryExpr)) {
- return expr;
- }
-
- var bexpr = expr as BinaryExpr;
-
- BinaryExpr new_expr = bexpr;
- if (bexpr.Op == BinaryExpr.Opcode.NotIn) {
- new_expr = new BinaryExpr(bexpr.tok, BinaryExpr.Opcode.In, bexpr.E0, bexpr.E1);
- new_expr.ResolvedOp = RemoveNotInBinaryExprIn(bexpr.ResolvedOp);
- new_expr.Type = bexpr.Type;
- }
-
- Expression returned_expr = new_expr;
- if (new_expr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) {
- returned_expr = new SeqSelectExpr(new_expr.tok, true, new_expr.E1, new_expr.E0, null);
- returned_expr.Type = bexpr.Type;
- isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer
- }
-
- return returned_expr;
- }
-
- private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) {
- bool expr_is_killer = false;
- var new_expr = CleanupExpr(expr, out expr_is_killer);
- var new_candidate = new TriggerCandidate { Expr = new_expr, Variables = CollectVariables(expr) };
-
- List<TriggerCandidate> collected_candidates = CollectExportedCandidates(expr);
- var children_contain_killers = CollectIsKiller(expr);
-
- if (!children_contain_killers) {
- // Add only if the children are not killers; the head has been cleaned up into non-killer form
- collected_candidates.Add(new_candidate);
- }
-
- // This new node is a killer if its children were killers, or if it's non-cleaned-up head is a killer
- return new TriggerAnnotation(children_contain_killers || expr_is_killer, new_candidate.Variables, collected_candidates);
- }
-
- private TriggerAnnotation AnnotateApplySuffix(ApplySuffix expr) {
- // This is a bit tricky. A funcall node is generally meaningful as a trigger candidate,
- // but when it's part of an ApplySuffix the function call itself may not resolve properly
- // when the second round of resolving is done after modules are duplicated.
- // Thus first we annotate expr and create a trigger candidate, and then we remove the
- // candidate matching its direct subexpression if needed. Not that function calls are not the
- // only possible child here; there can be DatatypeValue nodes, for example (see vstte2012/Combinators.dfy).
- var annotation = AnnotatePotentialCandidate(expr);
- // Comparing by reference is fine here. Using sets could yield a small speedup
- annotation.ExportedCandidates.RemoveAll(candidate => expr.SubExpressions.Contains(candidate.Expr));
- return annotation;
- }
-
- private TriggerAnnotation AnnotateQuantifierOrLetExpr(Expression expr, IEnumerable<BoundVar> boundVars) {
- var candidates = CollectExportedCandidates(expr);
- return new TriggerAnnotation(true, CollectVariables(expr), candidates, OnlyPrivateCandidates(candidates, boundVars));
- }
-
- private TriggerAnnotation AnnotateQuantifier(QuantifierExpr expr) {
- quantifiers.Add(expr);
- return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars);
- }
-
- private TriggerAnnotation AnnotateLetExpr(LetExpr expr) {
- return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars);
- }
-
- private TriggerAnnotation AnnotateIdentifier(IdentifierExpr expr) {
- return new TriggerAnnotation(false, Enumerable.Repeat(expr.Var, 1), null);
- }
-
- private TriggerAnnotation AnnotateOther(Expression expr, bool isTriggerKiller) {
- return new TriggerAnnotation(isTriggerKiller || CollectIsKiller(expr), CollectVariables(expr), CollectExportedCandidates(expr));
- }
-
- private static List<T> CopyAndAdd<T>(List<T> seq, T elem) {
- var copy = new List<T>(seq);
- copy.Add(elem);
- return copy;
- }
-
- private static IEnumerable<List<T>> AllSubsets<T>(IList<T> source, int offset) {
- if (offset >= source.Count) {
- yield return new List<T>();
- yield break;
- }
-
- foreach (var subset in AllSubsets<T>(source, offset + 1)) {
- yield return CopyAndAdd(subset, source[offset]);
- yield return new List<T>(subset);
- }
- }
-
- private static IEnumerable<List<T>> AllNonEmptySubsets<T>(IEnumerable<T> source) {
- List<T> all = new List<T>(source);
- foreach (var subset in AllSubsets(all, 0)) {
- if (subset.Count > 0) {
- yield return subset;
- }
- }
- }
-
- private static bool DefaultCandidateFilteringFunction(TriggerCandidate candidate, QuantifierExpr quantifier) {
- //FIXME this will miss rewritten expressions (CleanupExpr). Should introduce an OriginalExpr to compare.
- candidate.MatchesInQuantifierBody = quantifier.SubexpressionsMatchingTrigger(candidate.Expr).ToList();
- return true;
- }
-
- private static bool DefaultMultiCandidateFilteringFunction(MultiTriggerCandidate multiCandidate, QuantifierExpr quantifier) {
- var allowsLoops = quantifier.Attributes.AsEnumerable().Any(a => a.Name == "loop");
-
- if (!allowsLoops && multiCandidate.PotentialMatchingLoops.Any()) {
- multiCandidate.Tags.Add(String.Format("matching loop with {0}", multiCandidate.PotentialMatchingLoops.MapConcat(tm => Printer.ExprToString(tm.Expr), ", ")));
- }
- return multiCandidate.MentionsAll(quantifier.BoundVars) && (allowsLoops || !multiCandidate.PotentialMatchingLoops.Any());
- }
-
- private static double DefaultMultiCandidateScoringFunction(MultiTriggerCandidate multi_candidate) {
- return 1.0;
- }
-
- private static IEnumerable<MultiTriggerCandidate> DefaultMultiCandidateSelectionFunction(List<MultiTriggerCandidate> multi_candidates) {
- return multi_candidates;
- }
-
- // CLEMENT: Make these customizable
- internal Func<TriggerCandidate, QuantifierExpr, bool> CandidateFilteringFunction = DefaultCandidateFilteringFunction;
- internal Func<MultiTriggerCandidate, QuantifierExpr, bool> MultiCandidateFilteringFunction = DefaultMultiCandidateFilteringFunction;
- internal Func<MultiTriggerCandidate, double> MultiCandidateScoringFunction = DefaultMultiCandidateScoringFunction;
- internal Func<List<MultiTriggerCandidate>, IEnumerable<MultiTriggerCandidate>> MultiCandidateSelectionFunction = DefaultMultiCandidateSelectionFunction;
-
- struct MultiCandidatesCollection {
- internal List<TriggerCandidate> AllCandidates;
- internal List<TriggerCandidate> SelectedCandidates;
- internal List<TriggerCandidate> RejectedCandidates;
- internal List<MultiTriggerCandidate> SelectedMultiCandidates;
- internal List<MultiTriggerCandidate> RejectedMultiCandidates;
- internal List<MultiTriggerCandidate> FinalMultiCandidates;
-
- public MultiCandidatesCollection(QuantifierExpr quantifier,
- TriggerAnnotation annotation,
- Func<TriggerCandidate, QuantifierExpr, bool> CandidateFilteringFunction,
- Func<MultiTriggerCandidate, QuantifierExpr, bool> MultiCandidateFilteringFunction,
- Func<MultiTriggerCandidate, double> MultiCandidateScoringFunction,
- Func<List<MultiTriggerCandidate>, IEnumerable<MultiTriggerCandidate>> MultiCandidateSelectionFunction) {
-
- Contract.Requires(annotation != null);
- Contract.Requires(quantifier != null);
- Contract.Requires(CandidateFilteringFunction != null);
- Contract.Requires(MultiCandidateFilteringFunction != null);
- Contract.Requires(MultiCandidateScoringFunction != null);
- Contract.Requires(MultiCandidateSelectionFunction != null);
-
- AllCandidates = annotation.PrivateCandidates.Deduplicate((x, y) => ExprExtensions.ExpressionEq(x.Expr, y.Expr));
- Partition(AllCandidates,
- x => CandidateFilteringFunction(x, quantifier), out SelectedCandidates, out RejectedCandidates);
- Partition(AllNonEmptySubsets(SelectedCandidates).Select(s => new MultiTriggerCandidate(s)),
- x => MultiCandidateFilteringFunction(x, quantifier), out SelectedMultiCandidates, out RejectedMultiCandidates);
- SelectedMultiCandidates.Iter(x => x.Score = MultiCandidateScoringFunction(x));
- FinalMultiCandidates = MultiCandidateSelectionFunction(SelectedMultiCandidates).ToList();
- }
-
- private static void Partition<T>(IEnumerable<T> elements, Func<T, bool> predicate, out List<T> positive, out List<T> negative) {
- positive = new List<T>();
- negative = new List<T>();
- foreach (var c in elements) {
- (predicate(c) ? positive : negative).Add(c);
- }
- }
-
- internal string Warning() {
- if (AllCandidates.Count == 0) {
- return "No triggers found in the body of this quantifier.";
- } else if (SelectedCandidates.Count == 0) {
- return String.Format("No suitable triggers found. Candidate building blocks for a good trigger where [{0}], but none these terms passed the initial selection stage.", String.Join(", ", AllCandidates));
- } else if (SelectedMultiCandidates.Count == 0) {
- return String.Format("No suitable set of triggers found. Candidate building blocks for a good trigger where [{0}], but no subset of these terms passed the subset selection stage.", String.Join(", ", SelectedCandidates));
- } else if (FinalMultiCandidates.Count == 0) {
- return String.Format("No suitable set of triggers found. Candidates where [{0}], but none passed the final selection stage.", String.Join(", ", SelectedMultiCandidates));
- } else {
- return null;
- }
- }
-
- private void WriteIndented<T>(StringBuilder builder, string indent, IEnumerable<T> elements) {
- foreach (var element in elements) {
- builder.Append(indent).AppendLine(element.ToString());
- }
- }
-
- private void WriteListOfCandidates<T>(StringBuilder builder, string indent, IEnumerable<T> elements) {
- if (elements.Any()) {
- builder.AppendLine();
- WriteIndented(builder, indent, elements);
- } else {
- builder.AppendLine(" (None)");
- }
- }
-
- public override string ToString() {
- var repr = new StringBuilder();
- var indent = " ";
- repr.Append(" All:");
- WriteListOfCandidates(repr, indent, AllCandidates);
- repr.Append(" Selected1:");
- WriteListOfCandidates(repr, indent, SelectedCandidates);
- repr.Append(" PreFilter:");
- WriteListOfCandidates(repr, indent, AllNonEmptySubsets(AllCandidates).Select(c => String.Join(", ", c)));
- repr.Append(" SelectedMulti:");
- WriteListOfCandidates(repr, indent, SelectedMultiCandidates.Select(c => String.Join(", ", c)));
- repr.Append(" Final:");
- WriteListOfCandidates(repr, indent, FinalMultiCandidates);
- return repr.ToString();
- }
- }
-
- private MultiCandidatesCollection PickMultiTriggers(QuantifierExpr quantifier) {
- var annotation = Annotate(quantifier);
- DebugTriggers("Quantifier {0}:\n{1}", Printer.ExprToString(quantifier), annotation);
- return new MultiCandidatesCollection(quantifier, annotation, CandidateFilteringFunction, MultiCandidateFilteringFunction, MultiCandidateScoringFunction, MultiCandidateSelectionFunction);
- }
-
- private void AddTrigger(QuantifierExpr quantifier) {
- DebugTriggers(" Final results:\n{0}", PickMultiTriggers(quantifier));
-
- if (quantifier.Attributes.AsEnumerable().Any(aa => aa.Name == "trigger" || aa.Name == "no_trigger")) {
- DebugTriggers("Not generating triggers for {0}", Printer.ExprToString(quantifier)); //FIXME: no_trigger is passed down to Boogie
- return;
- }
-
- var multi_candidates = PickMultiTriggers(quantifier);
- foreach (var multi_candidate in multi_candidates.FinalMultiCandidates) { //TODO: error message for when no triggers found
- quantifier.Attributes = new Attributes("trigger", multi_candidate.Candidates.Select(t => t.Expr).ToList(), quantifier.Attributes);
- }
-
- if (multi_candidates.RejectedMultiCandidates.Any()) {
- var tooltip = JoinStringsWithHeader("Rejected: ", multi_candidates.RejectedMultiCandidates.Where(candidate => candidate.Tags != null)
- .Select(candidate => candidate.AsDafnyAttributeString(true, true)));
- AdditionalInformationReporter(quantifier.tok, tooltip, quantifier.tok.val.Length);
- }
-
- if (multi_candidates.FinalMultiCandidates.Any()) {
- var tooltip = JoinStringsWithHeader("Triggers: ", multi_candidates.FinalMultiCandidates.Select(multi_candidate => multi_candidate.AsDafnyAttributeString()));
- AdditionalInformationReporter(quantifier.tok, tooltip, quantifier.tok.val.Length);
- }
-
- string warning = multi_candidates.Warning();
- if (warning != null) {
- // FIXME reenable Resolver.Warning(quantifier.tok, warning);
- }
- }
-
- internal static bool IsTriggerKiller(Expression expr) {
- var annotation = new TriggerGenerator((x, y, z) => { }).Annotate(expr);
- return annotation.IsTriggerKiller;
- }
-
- private string JoinStringsWithHeader(string header, IEnumerable<string> lines) {
- return header + String.Join(Environment.NewLine + new String(' ', header.Length), lines);
- }
-
- private void AddTriggers_Internal() {
- foreach (var quantifier in quantifiers) {
- AddTrigger(quantifier);
- }
- }
-
- private void AddTriggers_Internal(Expression root) {
- Visit(root);
- AddTriggers_Internal();
- }
-
- private void AddTriggers_Internal(Statement root) {
- Visit(root);
- AddTriggers_Internal();
- }
-
- internal static void AddTriggers(Expression root, Resolver resolver) {
- if (root == null)
- return;
-
- DebugTriggers("== From {0} visiting expr: {1}", new StackFrame(1).GetMethod().Name, Printer.ExprToString(root));
- TriggerGenerator generator = new TriggerGenerator(null);
- generator.AddTriggers_Internal(root);
- }
-
- internal static void AddTriggers(Statement root, Resolver resolver) {
- if (root == null)
- return;
-
- DebugTriggers("== From {0} visiting statement: {1}", new StackFrame(1).GetMethod().Name, Printer.StatementToString(root));
- TriggerGenerator generator = new TriggerGenerator(null);
- generator.AddTriggers_Internal(root);
- }
-
- internal static void AddTriggers(IEnumerable<Expression> roots, Resolver resolver) {
- DebugTriggers("== From {0} visiting expressions: {1}", new StackFrame(1).GetMethod().Name,
- roots.MapConcat(Printer.ExprToString, ", "));
- foreach (var expr in roots) {
- AddTriggers(expr, resolver);
- }
- }
-
- internal static void AddTriggers(IEnumerable<MaybeFreeExpression> roots, Resolver resolver) {
- DebugTriggers("== From {0} visiting expressions: {1}", new StackFrame(1).GetMethod().Name,
- roots.MapConcat(root => Printer.ExprToString(root.E), ", "));
- foreach (var expr in roots) {
- AddTriggers(expr.E, resolver);
- }
- }
-
- protected override void VisitOneExpr(Expression expr) {
- Annotate(expr);
- }
- }
-
- internal static class DeduplicateExtension {
- public static List<T> Deduplicate<T>(this IEnumerable<T> seq, Func<T, T, bool> eq) {
- List<T> deduplicated = new List<T>();
-
- foreach (var elem in seq) {
- if (!deduplicated.Any(other => eq(elem, other))) {
- deduplicated.Add(elem);
- }
- }
-
- return deduplicated;
- }
- }
-
- static class ExprExtensions {
- static IEnumerable<Expression> 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;
- }
- }
-
- private static IEnumerable<Expression> 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 = GetResolved(expr1);
- expr2 = GetResolved(expr2);
-
- return ShallowEq_Top(expr1, expr2) && SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEq(e1, e2));
- }
-
- internal static bool ExpressionEqModuloVariableNames(this Expression expr1, Expression expr2) {
- expr1 = GetResolved(expr1);
- expr2 = GetResolved(expr2);
-
- if (expr1 is IdentifierExpr) {
- return expr2 is IdentifierExpr;
- }
-
- return ShallowEq_Top(expr1, expr2) && SameLists(expr1.SubExpressions, expr2.SubExpressions, (e1, e2) => ExpressionEqModuloVariableNames(e1, e2));
- }
-
- private static bool MatchesTrigger(this Expression expr, Expression trigger, ISet<BoundVar> holes, Dictionary<IVariable, Expression> bindings) {
- expr = GetResolved(expr);
- trigger = GetResolved(trigger);
-
- 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) && SameLists(expr.SubExpressions, trigger.SubExpressions, (e1, e2) => MatchesTrigger(e1, e2, holes, bindings));
- }
-
- internal struct TriggerMatch {
- internal Expression Expr;
- internal Dictionary<IVariable, Expression> Bindings;
-
- internal bool CouldCauseLoops(IEnumerable<TriggerCandidate> 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<BoundVar> holes) {
- var bindings = new Dictionary<IVariable, Expression>();
- return expr.MatchesTrigger(trigger, holes, bindings) ? new TriggerMatch { Expr = expr, Bindings = bindings } : (TriggerMatch?)null;
- }
-
- internal static IEnumerable<TriggerMatch> SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) {
- return quantifier.Term.AllSubExpressions()
- .Select(e => e.MatchAgainst(trigger, new HashSet<BoundVar>(quantifier.BoundVars)))
- .Where(e => e.HasValue).Select(e => e.Value);
- }
-
- private static bool SameLists<T>(IEnumerable<T> list1, IEnumerable<T> list2, Func<T, T, bool> comparer) {
- if (ReferenceEquals(list1, list2)) {
- return true;
- } else if ((list1 == null) != (list2 == null)) {
- return false;
- }
-
- var it1 = list1.GetEnumerator();
- var it2 = list2.GetEnumerator();
- bool it1_has, it2_has;
- bool acc = true;
-
- do {
- it1_has = it1.MoveNext();
- it2_has = it2.MoveNext();
-
- if (it1_has == true && it2_has == true) {
- acc = acc && comparer(it1.Current, it2.Current);
- }
- } while (it1_has && it2_has);
-
- return it1_has == it2_has && acc;
- }
-
- private static bool SameNullity<T>(T x1, T x2) where T : class {
- return (x1 == null) == (x2 == null);
- }
-
- private static bool ShallowSameAttributes(Attributes attributes1, Attributes attributes2) {
- return 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?
- }
-
- private static Expression GetResolved(Expression expr) {
- if (expr is ConcreteSyntaxExpression) {
- return ((ConcreteSyntaxExpression)expr).ResolvedExpression;
- }
- return expr;
- }
-
- /// <summary>
- /// Compares two abstract syntax expressions, looking only at their direct members. Subexpressions and substatements are not compared.
- /// </summary>
- /// <returns></returns>
- 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 expr1.OneShot == expr2.OneShot &&
- SameLists(expr1.Reads, expr2.Reads, SameFrameExpression);
-#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 ||
- !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 (!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) ||
- !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 &&
- 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 &&
- SameNullity(expr1.Seq, expr2.Seq) &&
- SameNullity(expr1.E0, expr2.E0) &&
- SameNullity(expr1.E1, expr2.E1);
- }
-
- private static bool ShallowEq(MemberSelectExpr expr1, MemberSelectExpr expr2) {
- return expr1.MemberName == expr2.MemberName &&
- expr1.Member == expr2.Member &&
- SameLists(expr1.TypeApplication, expr2.TypeApplication, 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 &&
- SameLists(expr1.InferredTypeArgs, expr2.InferredTypeArgs, 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
- }
- }
- }
-}
diff --git a/Source/Dafny/Triggers/QuantifierSplitter.cs b/Source/Dafny/Triggers/QuantifierSplitter.cs new file mode 100644 index 00000000..e83feebb --- /dev/null +++ b/Source/Dafny/Triggers/QuantifierSplitter.cs @@ -0,0 +1,66 @@ +using Microsoft.Boogie;
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+namespace Microsoft.Dafny.Triggers {
+ class QuantifierSplitter : BottomUpVisitor {
+ internal enum Quantifier { Forall, Exists }
+
+ internal static IEnumerable<Expression> BreakQuantifier(Expression expr, Quantifier quantifier) {
+ expr = expr.Resolved;
+ var binary = expr as BinaryExpr;
+
+ if (binary == null) {
+ yield return expr;
+ yield break;
+ }
+
+ var e0 = binary.E0;
+ var e1 = binary.E1;
+
+ if ((quantifier == Quantifier.Forall && binary.Op == BinaryExpr.Opcode.And) ||
+ (quantifier == Quantifier.Exists && binary.Op == BinaryExpr.Opcode.Or)) {
+ foreach (var e in BreakQuantifier(e0, quantifier)) { yield return e; }
+ foreach (var e in BreakQuantifier(e1, quantifier)) { yield return e; }
+ } else if (binary.Op == BinaryExpr.Opcode.Imp) {
+ if (quantifier == Quantifier.Forall) {
+ foreach (var e in BreakImplication(e0, e1, quantifier, expr.tok)) { yield return e; }
+ } else {
+ yield return new UnaryOpExpr(e1.tok, UnaryOpExpr.Opcode.Not, e1); // FIXME should be broken further
+ foreach (var e in BreakQuantifier(e1, quantifier)) { yield return e; }
+ }
+ } else {
+ yield return expr;
+ }
+ }
+
+ internal static IEnumerable<Expression> BreakImplication(Expression ante, Expression post, Quantifier quantifier, IToken tok) { // FIXME: should work for exists and &&
+ foreach (var small_post in BreakQuantifier(post, quantifier)) {
+ var bin_post = small_post as BinaryExpr;
+ if (bin_post == null || bin_post.Op != BinaryExpr.Opcode.Imp) {
+ yield return new BinaryExpr(tok, BinaryExpr.Opcode.Imp, ante, small_post);
+ } else { // bin_post is an implication
+ var large_ante = new BinaryExpr(ante.tok, BinaryExpr.Opcode.And, ante, bin_post.E0);
+ foreach (var imp in BreakImplication(large_ante, bin_post.E1, quantifier, tok)) {
+ yield return imp;
+ }
+ }
+ }
+ }
+
+ protected override void VisitOneExpr(Expression expr) { //FIXME: This doesn't save the rewritten quantifier
+ var forall = expr as ForallExpr;
+ var exists = expr as ExistsExpr;
+
+ if (forall != null && TriggerUtils.NeedsAutoTriggers(forall)) {
+ var rew = BreakQuantifier(forall.LogicalBody(), Quantifier.Forall);
+ //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| "));
+ } else if (exists != null && TriggerUtils.NeedsAutoTriggers(exists)) {
+ var rew = BreakQuantifier(exists.LogicalBody(), Quantifier.Exists);
+ //Console.WriteLine("!!! {0} => {1}", Printer.ExprToString(expr), rew.MapConcat(Printer.ExprToString, " ||| "));
+ }
+ }
+ }
+}
diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs new file mode 100644 index 00000000..3cbe3bd9 --- /dev/null +++ b/Source/Dafny/Triggers/QuantifiersCollection.cs @@ -0,0 +1,104 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+//FIXME Generated triggers should be _triggers
+//FIXME: When scoring, do not consider old(x) to be higher than x.
+
+namespace Microsoft.Dafny.Triggers {
+ class QuantifierWithTriggers {
+ internal QuantifierExpr quantifier;
+ internal List<MultiTriggerCandidate> triggers;
+
+ internal QuantifierWithTriggers(QuantifierExpr quantifier) {
+ this.quantifier = quantifier;
+ this.triggers = null;
+ }
+
+ internal void TrimInvalidTriggers() {
+ triggers = triggers.Where(tr => tr.MentionsAll(quantifier.BoundVars)).ToList();
+ }
+
+ public bool QuantifierAlreadyHadTriggers { get { return !TriggerUtils.NeedsAutoTriggers(quantifier); } }
+ }
+
+ class QuantifiersCollection {
+ readonly ErrorReporter reporter;
+ readonly List<QuantifierWithTriggers> quantifiers;
+
+ internal QuantifiersCollection(IEnumerable<QuantifierExpr> quantifiers, ErrorReporter reporter) {
+ this.reporter = reporter;
+ this.quantifiers = quantifiers.Select(q => new QuantifierWithTriggers(q)).ToList();
+ }
+
+ void ComputeTriggers() {
+ CollectAndShareTriggers();
+ TrimInvalidTriggers();
+ BuildDependenciesGraph();
+ SuppressMatchingLoops();
+ SelectTriggers();
+ }
+
+ 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();
+
+ 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;
+ }
+ }
+ }
+
+ private void TrimInvalidTriggers() {
+ foreach (var q in quantifiers) {
+ q.TrimInvalidTriggers();
+ }
+ }
+
+ void BuildDependenciesGraph() {
+ //FIXME
+ }
+
+ void SuppressMatchingLoops() {
+ //FIXME
+ }
+
+ 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));
+
+ //var multi_candidates = PickMultiTriggers(quantifier);
+
+ //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 (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);
+ //}
+
+ //string warning = multi_candidates.Warning();
+ //if (warning != null) {
+ // // FIXME reenable Resolver.Warning(quantifier.tok, warning);
+ //}
+ }
+
+ }
+}
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<T> Deduplicate<T>(this IEnumerable<T> seq, Func<T, T, bool> eq) {
+ List<T> deduplicated = new List<T>();
+
+ foreach (var elem in seq) {
+ if (!deduplicated.Any(other => eq(elem, other))) {
+ deduplicated.Add(elem);
+ }
+ }
+
+ return deduplicated;
+ }
+ }
+
+ internal static class ExprExtensions {
+ internal static IEnumerable<Expression> 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<Expression> 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<BoundVar> holes, Dictionary<IVariable, Expression> 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<IVariable, Expression> Bindings;
+
+ internal bool CouldCauseLoops(IEnumerable<TriggerCandidate> 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<BoundVar> holes) {
+ var bindings = new Dictionary<IVariable, Expression>();
+ return expr.MatchesTrigger(trigger, holes, bindings) ? new TriggerMatch { Expr = expr, Bindings = bindings } : (TriggerMatch?)null;
+ }
+
+ internal static IEnumerable<TriggerMatch> SubexpressionsMatchingTrigger(this QuantifierExpr quantifier, Expression trigger) {
+ return quantifier.Term.AllSubExpressions()
+ .Select(e => e.MatchAgainst(trigger, new HashSet<BoundVar>(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?
+ }
+
+ /// <summary>
+ /// Compares two abstract syntax expressions, looking only at their direct members. Subexpressions and substatements are not compared.
+ /// </summary>
+ /// <returns></returns>
+ 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
+ }
+ }
+ }
+}
diff --git a/Source/Dafny/Triggers/TriggerGenerator.cs b/Source/Dafny/Triggers/TriggerGenerator.cs new file mode 100644 index 00000000..de4b212b --- /dev/null +++ b/Source/Dafny/Triggers/TriggerGenerator.cs @@ -0,0 +1,28 @@ +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<object> {
+ readonly ErrorReporter reporter;
+ internal List<QuantifiersCollection> quantifierCollections = new List<QuantifiersCollection>();
+
+ 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) {
+ quantifierCollections.Add(new QuantifiersCollection(Enumerable.Repeat(quantifier, 1), reporter));
+ } //FIXME handle the case of groups of quantifiers resulting from a split
+
+ return true;
+ }
+ }
+}
diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs new file mode 100644 index 00000000..5a118a2f --- /dev/null +++ b/Source/Dafny/Triggers/TriggerUtils.cs @@ -0,0 +1,94 @@ +#define DEBUG_AUTO_TRIGGERS
+
+using System;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using System.Text;
+
+namespace Microsoft.Dafny.Triggers {
+ class TriggerUtils {
+ internal static List<T> CopyAndAdd<T>(List<T> seq, T elem) {
+ var copy = new List<T>(seq);
+ copy.Add(elem);
+ return copy;
+ }
+
+ internal static IEnumerable<List<T>> AllSubsets<T>(IList<T> source, int offset) {
+ if (offset >= source.Count) {
+ yield return new List<T>();
+ yield break;
+ }
+
+ foreach (var subset in AllSubsets<T>(source, offset + 1)) {
+ yield return CopyAndAdd(subset, source[offset]);
+ yield return new List<T>(subset);
+ }
+ }
+
+ internal static IEnumerable<List<T>> AllNonEmptySubsets<T>(IEnumerable<T> source) {
+ List<T> all = new List<T>(source);
+ foreach (var subset in AllSubsets(all, 0)) {
+ if (subset.Count > 0) {
+ yield return subset;
+ }
+ }
+ }
+
+ internal static List<T> MergeAlterFirst<T>(List<T> a, List<T> b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ a.AddRange(b);
+ return a;
+ }
+
+ internal static ISet<T> MergeAlterFirst<T>(ISet<T> a, ISet<T> b) {
+ Contract.Requires(a != null);
+ Contract.Requires(b != null);
+ a.UnionWith(b);
+ return a;
+ }
+
+ internal static bool SameLists<T>(IEnumerable<T> list1, IEnumerable<T> list2, Func<T, T, bool> comparer) {
+ if (ReferenceEquals(list1, list2)) {
+ return true;
+ } else if ((list1 == null) != (list2 == null)) {
+ return false;
+ }
+
+ var it1 = list1.GetEnumerator();
+ var it2 = list2.GetEnumerator();
+ bool it1_has, it2_has;
+ bool acc = true;
+
+ do {
+ it1_has = it1.MoveNext();
+ it2_has = it2.MoveNext();
+
+ if (it1_has == true && it2_has == true) {
+ acc = acc && comparer(it1.Current, it2.Current);
+ }
+ } while (it1_has && it2_has);
+
+ return it1_has == it2_has && acc;
+ }
+
+ internal static bool SameNullity<T>(T x1, T x2) where T : class {
+ return (x1 == null) == (x2 == null);
+ }
+
+ internal string JoinStringsWithHeader(string header, IEnumerable<string> lines) {
+ return header + String.Join(Environment.NewLine + new String(' ', header.Length), lines);
+ }
+
+ [Conditional("DEBUG_AUTO_TRIGGERS")]
+ internal static void DebugTriggers(string format, params object[] more) {
+ Console.Error.WriteLine(format, more);
+ }
+
+ internal static bool NeedsAutoTriggers(QuantifierExpr 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 new file mode 100644 index 00000000..912a661c --- /dev/null +++ b/Source/Dafny/Triggers/TriggersCollector.cs @@ -0,0 +1,256 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.Boogie;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+namespace Microsoft.Dafny.Triggers {
+ struct TriggerCandidate {
+ internal Expression Expr { get; set; }
+ internal ISet<IVariable> Variables { get; set; }
+
+ public override string ToString() {
+ return Printer.ExprToString(Expr);
+ }
+ }
+
+ class MultiTriggerCandidate {
+ internal List<TriggerCandidate> terms { get; set; }
+
+ internal MultiTriggerCandidate(List<TriggerCandidate> candidates) {
+ this.terms = candidates;
+ }
+
+ internal bool MentionsAll(List<BoundVar> vars) {
+ return vars.All(x => terms.Any(candidate => candidate.Variables.Contains(x)));
+ }
+
+ public override string ToString() {
+ return String.Join(", ", terms);
+ }
+
+ public String AsDafnyAttributeString(bool wrap = true, bool includeTags = false) {
+ var repr = terms.MapConcat(t => Printer.ExprToString(t.Expr), ", ");
+ if (wrap) {
+ repr = "{:trigger " + repr + "}";
+ }
+ return repr;
+ }
+ }
+
+ class TriggerAnnotation {
+ internal bool IsTriggerKiller;
+ internal ISet<IVariable> Variables;
+ internal readonly List<TriggerCandidate> PrivateTerms;
+ internal readonly List<TriggerCandidate> ExportedTerms;
+
+ internal TriggerAnnotation(bool IsTriggerKiller, IEnumerable<IVariable> Variables,
+ IEnumerable<TriggerCandidate> AllCandidates, IEnumerable<TriggerCandidate> PrivateCandidates = null) {
+ this.IsTriggerKiller = IsTriggerKiller;
+ this.Variables = new HashSet<IVariable>(Variables);
+
+ this.PrivateTerms = new List<TriggerCandidate>(PrivateCandidates == null ? Enumerable.Empty<TriggerCandidate>() : PrivateCandidates);
+ this.ExportedTerms = new List<TriggerCandidate>(AllCandidates == null ? Enumerable.Empty<TriggerCandidate>() : AllCandidates.Except(this.PrivateTerms));
+ }
+
+ public override string ToString() {
+ StringBuilder sb = new StringBuilder();
+ string indent = " {0}", nindent = "\n - {0}", subindent = "\n * {0}";
+
+ sb.AppendFormat(indent, IsTriggerKiller);
+
+ sb.AppendFormat(nindent, "Variables:");
+ foreach (var bv in Variables) {
+ sb.AppendFormat(subindent, bv.Name);
+ }
+
+ sb.AppendFormat(nindent, "Exported candidates:");
+ foreach (var candidate in ExportedTerms) {
+ sb.AppendFormat(subindent, candidate);
+ }
+
+ if (PrivateTerms.Any()) {
+ sb.AppendFormat(nindent, "Private candidates:");
+ foreach (var candidate in PrivateTerms) {
+ sb.AppendFormat(subindent, candidate);
+ }
+ }
+
+ return sb.ToString();
+ }
+ }
+
+ public class TriggersCollector {
+ Dictionary<Expression, TriggerAnnotation> cache;
+
+ private static TriggersCollector instance = new TriggersCollector();
+
+ private TriggersCollector() {
+ this.cache = new Dictionary<Expression, TriggerAnnotation>();
+ }
+
+ private T ReduceAnnotatedSubExpressions<T>(Expression expr, T seed, Func<TriggerAnnotation, T> map, Func<T, T, T> reduce) {
+ return expr.SubExpressions.Select(e => map(Annotate(e)))
+ .Aggregate(seed, (acc, e) => reduce(acc, e));
+ }
+
+ private List<TriggerCandidate> CollectExportedCandidates(Expression expr) {
+ return ReduceAnnotatedSubExpressions<List<TriggerCandidate>>(expr, new List<TriggerCandidate>(), a => a.ExportedTerms, TriggerUtils.MergeAlterFirst);
+ }
+
+ private ISet<IVariable> CollectVariables(Expression expr) {
+ return ReduceAnnotatedSubExpressions(expr, new HashSet<IVariable>(), a => a.Variables, TriggerUtils.MergeAlterFirst);
+ }
+
+ private bool CollectIsKiller(Expression expr) {
+ return ReduceAnnotatedSubExpressions(expr, false, a => a.IsTriggerKiller, (a, b) => a || b);
+ }
+
+ private IEnumerable<TriggerCandidate> OnlyPrivateCandidates(List<TriggerCandidate> candidates, IEnumerable<IVariable> privateVars) {
+ return candidates.Where(c => privateVars.Intersect(c.Variables).Any()); //TODO Check perf
+ }
+
+ private TriggerAnnotation Annotate(Expression expr) {
+ TriggerAnnotation cached;
+ if (cache.TryGetValue(expr, out cached)) {
+ return cached;
+ }
+
+ expr.SubExpressions.Iter(e => Annotate(e));
+
+ TriggerAnnotation annotation; // TODO: Using ApplySuffix fixes the unresolved members problem in GenericSort
+ if (expr is FunctionCallExpr || expr is SeqSelectExpr || expr is MemberSelectExpr || expr is OldExpr ||
+ (expr is UnaryOpExpr && (((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Cardinality)) || // FIXME || ((UnaryOpExpr)expr).Op == UnaryOpExpr.Opcode.Fresh doesn't work, as fresh is a pretty tricky predicate when it's not about datatypes. See translator.cs:10944
+ (expr is BinaryExpr && (((BinaryExpr)expr).Op == BinaryExpr.Opcode.NotIn || ((BinaryExpr)expr).Op == BinaryExpr.Opcode.In))) {
+ annotation = AnnotatePotentialCandidate(expr);
+ } else if (expr is QuantifierExpr) {
+ annotation = AnnotateQuantifier((QuantifierExpr)expr);
+ } else if (expr is LetExpr) {
+ annotation = AnnotateLetExpr((LetExpr)expr);
+ } else if (expr is IdentifierExpr) {
+ annotation = AnnotateIdentifier((IdentifierExpr)expr);
+ } else if (expr is ApplySuffix) {
+ annotation = AnnotateApplySuffix((ApplySuffix)expr);
+ } else if (expr is ConcreteSyntaxExpression ||
+ expr is LiteralExpr ||
+ expr is OldExpr ||
+ expr is ThisExpr ||
+ expr is BoxingCastExpr ||
+ expr is DatatypeValue ||
+ expr is SeqDisplayExpr) { //FIXME what abvout other display expressions?
+ annotation = AnnotateOther(expr, false);
+ } else {
+ annotation = AnnotateOther(expr, true);
+ }
+
+ TriggerUtils.DebugTriggers("{0} ({1})\n{2}", Printer.ExprToString(expr), expr.GetType(), annotation);
+ cache[expr] = annotation;
+ return annotation;
+ }
+
+ private BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) {
+ switch (opcode) {
+ case BinaryExpr.ResolvedOpcode.NotInMap:
+ return BinaryExpr.ResolvedOpcode.InMap;
+ case BinaryExpr.ResolvedOpcode.NotInSet:
+ return BinaryExpr.ResolvedOpcode.InSet;
+ case BinaryExpr.ResolvedOpcode.NotInSeq:
+ return BinaryExpr.ResolvedOpcode.InSeq;
+ case BinaryExpr.ResolvedOpcode.NotInMultiSet:
+ return BinaryExpr.ResolvedOpcode.InMultiSet;
+ }
+
+ Contract.Assert(false);
+ throw new ArgumentException();
+ }
+
+ private Expression CleanupExpr(Expression expr, out bool isKiller) {
+ isKiller = false;
+
+ if (!(expr is BinaryExpr)) {
+ return expr;
+ }
+
+ var bexpr = expr as BinaryExpr;
+
+ BinaryExpr new_expr = bexpr;
+ if (bexpr.Op == BinaryExpr.Opcode.NotIn) {
+ new_expr = new BinaryExpr(bexpr.tok, BinaryExpr.Opcode.In, bexpr.E0, bexpr.E1);
+ new_expr.ResolvedOp = RemoveNotInBinaryExprIn(bexpr.ResolvedOp);
+ new_expr.Type = bexpr.Type;
+ }
+
+ Expression returned_expr = new_expr;
+ if (new_expr.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) {
+ returned_expr = new SeqSelectExpr(new_expr.tok, true, new_expr.E1, new_expr.E0, null);
+ returned_expr.Type = bexpr.Type;
+ isKiller = true; // [a in s] becomes [s[a] > 0], which is a trigger killer
+ }
+
+ return returned_expr;
+ }
+
+ private TriggerAnnotation AnnotatePotentialCandidate(Expression expr) {
+ bool expr_is_killer = false;
+ var new_expr = CleanupExpr(expr, out expr_is_killer);
+ var new_candidate = new TriggerCandidate { Expr = new_expr, Variables = CollectVariables(expr) };
+
+ List<TriggerCandidate> collected_candidates = CollectExportedCandidates(expr);
+ var children_contain_killers = CollectIsKiller(expr);
+
+ if (!children_contain_killers) {
+ // Add only if the children are not killers; the head has been cleaned up into non-killer form
+ collected_candidates.Add(new_candidate);
+ }
+
+ // This new node is a killer if its children were killers, or if it's non-cleaned-up head is a killer
+ return new TriggerAnnotation(children_contain_killers || expr_is_killer, new_candidate.Variables, collected_candidates);
+ }
+
+ private TriggerAnnotation AnnotateApplySuffix(ApplySuffix expr) {
+ // This is a bit tricky. A funcall node is generally meaningful as a trigger candidate,
+ // but when it's part of an ApplySuffix the function call itself may not resolve properly
+ // when the second round of resolving is done after modules are duplicated.
+ // Thus first we annotate expr and create a trigger candidate, and then we remove the
+ // candidate matching its direct subexpression if needed. Note that function calls are not the
+ // only possible child here; there can be DatatypeValue nodes, for example (see vstte2012/Combinators.dfy).
+ var annotation = AnnotatePotentialCandidate(expr);
+ // Comparing by reference is fine here. Using sets could yield a small speedup
+ annotation.ExportedTerms.RemoveAll(candidate => expr.SubExpressions.Contains(candidate.Expr));
+ return annotation;
+ }
+
+ private TriggerAnnotation AnnotateQuantifierOrLetExpr(Expression expr, IEnumerable<BoundVar> boundVars) {
+ var candidates = CollectExportedCandidates(expr);
+ return new TriggerAnnotation(true, CollectVariables(expr), candidates, OnlyPrivateCandidates(candidates, boundVars));
+ }
+
+ private TriggerAnnotation AnnotateQuantifier(QuantifierExpr expr) {
+ return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars);
+ }
+
+ private TriggerAnnotation AnnotateLetExpr(LetExpr expr) {
+ return AnnotateQuantifierOrLetExpr(expr, expr.BoundVars);
+ }
+
+ private TriggerAnnotation AnnotateIdentifier(IdentifierExpr expr) {
+ return new TriggerAnnotation(false, Enumerable.Repeat(expr.Var, 1), null);
+ }
+
+ private TriggerAnnotation AnnotateOther(Expression expr, bool isTriggerKiller) {
+ return new TriggerAnnotation(isTriggerKiller || CollectIsKiller(expr), CollectVariables(expr), CollectExportedCandidates(expr));
+ }
+
+ // FIXME document that this will contain duplicates
+ internal static List<TriggerCandidate> CollectTriggers(QuantifierExpr quantifier) {
+ // TODO could check for existing triggers and return that instead, but that require a bit of work to extract the expressions
+ return instance.Annotate(quantifier).PrivateTerms;
+ }
+
+ internal static bool IsTriggerKiller(Expression expr) {
+ return instance.Annotate(expr).IsTriggerKiller;
+ }
+ }
+}
diff --git a/Test/dafny0/SeqFromArray.dfy.expect b/Test/dafny0/SeqFromArray.dfy.expect index af845d3e..5395e298 100644 --- a/Test/dafny0/SeqFromArray.dfy.expect +++ b/Test/dafny0/SeqFromArray.dfy.expect @@ -1,3 +1,6 @@ +SeqFromArray.dfy(56,13): Warning: (!) No terms found to trigger on.
+SeqFromArray.dfy(76,17): Warning: (!) No terms found to trigger on.
+SeqFromArray.dfy(82,17): Warning: (!) No terms found to trigger on.
Dafny program verifier finished with 10 verified, 0 errors
Program compiled successfully
|