Implement {:nowarn}, clarify some messages, and add a few tests

2 files changed, 25 insertions, 12 deletions

diff --git a/Source/Dafny/Triggers/QuantifiersCollection.cs b/Source/Dafny/Triggers/QuantifiersCollection.cs
index 50458ab7..f72dab7f 100644
--- a/Source/Dafny/Triggers/QuantifiersCollection.cs
+++ b/Source/Dafny/Triggers/QuantifiersCollection.cs
@@ -117,7 +117,7 @@ namespace Microsoft.Dafny.Triggers {
           (candidate, loopingSubterms) => !loopingSubterms.Any(),

           (candidate, loopingSubterms) => {

             looping.Add(candidate);

-            candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "{" + Printer.ExprToString(t.OriginalExpr) + "}", ", ");

+            candidate.Annotation = "may loop with " + loopingSubterms.MapConcat(t => "\"" + Printer.ExprToString(t.OriginalExpr) + "\"", ", ");

           }).ToList();

 

         q.CouldSuppressLoops = safe.Count > 0;

@@ -145,12 +145,14 @@ namespace Microsoft.Dafny.Triggers {
       var errorLevel = ErrorLevel.Info;

       var msg = new StringBuilder();

       var indent = addHeader ? "  " : "";

+      bool suppressWarnings = Attributes.Contains(q.quantifier.Attributes, "nowarn");

 

-      if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: matchingloop, split and autotriggers attributes are passed down to Boogie

-        msg.AppendFormat("Not generating triggers for {{{0}}}.", Printer.ExprToString(q.quantifier.Term)).AppendLine(); 

+      if (!TriggerUtils.NeedsAutoTriggers(q.quantifier)) { // NOTE: split and autotriggers attributes are passed down to Boogie

+        var extraMsg = TriggerUtils.WantsAutoTriggers(q.quantifier) ? "" : " Note that {:autotriggers false} can cause instabilities. Consider using {:nowarn}, {:matchingloop} (not great either), or a manual trigger instead.";

+        msg.AppendFormat("Not generating triggers for \"{0}\".{1}", Printer.ExprToString(q.quantifier.Term), extraMsg).AppendLine(); 

       } else {

         if (addHeader) {

-          msg.AppendFormat("For expression {{{0}}}:", Printer.ExprToString(q.quantifier.Term)).AppendLine();

+          msg.AppendFormat("For expression \"{0}\":", Printer.ExprToString(q.quantifier.Term)).AppendLine();

         }

 

         foreach (var candidate in q.Candidates) {

@@ -161,20 +163,26 @@ namespace Microsoft.Dafny.Triggers {
         AddTriggersToMessage("Rejected triggers:", q.RejectedCandidates, msg, indent, true);

 

 #if QUANTIFIER_WARNINGS

-        string WARN = indent + (DafnyOptions.O.UnicodeOutput ? "⚠ " : "(!) ");

+        var WARN_TAG = DafnyOptions.O.UnicodeOutput ? "⚠ " : "/!\\ ";

+        var WARN_TAG_OVERRIDE = suppressWarnings ? "(Suppressed warning) " : WARN_TAG;

+        var WARN_LEVEL = suppressWarnings ? ErrorLevel.Info : ErrorLevel.Warning;

+        var WARN = indent + WARN_TAG_OVERRIDE;

         if (!q.CandidateTerms.Any()) {

-          errorLevel = ErrorLevel.Warning;

+          errorLevel = WARN_LEVEL;

           msg.Append(WARN).AppendLine("No terms found to trigger on.");

         } else if (!q.Candidates.Any()) {

-          errorLevel = ErrorLevel.Warning;

+          errorLevel = WARN_LEVEL;

           msg.Append(WARN).AppendLine("No trigger covering all quantified variables found.");

         } else if (!q.CouldSuppressLoops && !q.AllowsLoops) {

-          errorLevel = ErrorLevel.Warning;

+          errorLevel = WARN_LEVEL;

           msg.Append(WARN).AppendLine("Suppressing loops would leave this expression without triggers.");

+        } else if (suppressWarnings) {

+          errorLevel = ErrorLevel.Warning;

+          msg.Append(indent).Append(WARN_TAG).AppendLine("There is no warning here to suppress.");

         }

 #endif

       }

-      

+

       if (msg.Length > 0) {

         var msgStr = msg.ToString().TrimEnd("\r\n ".ToCharArray());

         reporter.Message(MessageSource.Rewriter, errorLevel, q.quantifier.tok, msgStr);

diff --git a/Source/Dafny/Triggers/TriggerUtils.cs b/Source/Dafny/Triggers/TriggerUtils.cs
index efa1f167..c16a3e44 100644
--- a/Source/Dafny/Triggers/TriggerUtils.cs
+++ b/Source/Dafny/Triggers/TriggerUtils.cs
@@ -183,14 +183,19 @@ namespace Microsoft.Dafny.Triggers {
 

     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

+      // This is different from nowarn: it won't remove loops at all, even if another trigger is available.

       return Attributes.Contains(quantifier.Attributes, "matchingloop");

     }

 

-    internal static bool NeedsAutoTriggers(QuantifierExpr quantifier) {

+    internal static bool WantsAutoTriggers(QuantifierExpr quantifier) {

       Contract.Requires(quantifier.SplitQuantifier == null); // Don't call this on a quantifier with a Split clause: it's not a real quantifier

       bool wantsAutoTriggers = true;

-      return !Attributes.Contains(quantifier.Attributes, "trigger") && 

-        (!Attributes.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers);

+      return !Attributes.ContainsBool(quantifier.Attributes, "autotriggers", ref wantsAutoTriggers) || wantsAutoTriggers;

+    }

+

+    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 !Attributes.Contains(quantifier.Attributes, "trigger") && WantsAutoTriggers(quantifier);

     }

 

     internal static BinaryExpr.ResolvedOpcode RemoveNotInBinaryExprIn(BinaryExpr.ResolvedOpcode opcode) {