fix: Select alternative default calc operator more carefully (#3963)

Fixes #3962


<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: Remy Willems <[email protected]>

Author: RustanLeino

Source/DafnyCore/AST/Statements/CalcStmt.cs

@@ -2,6 +2,7 @@
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using JetBrains.Annotations;
 
 namespace Microsoft.Dafny;
 
@@ -11,13 +12,13 @@ public abstract class CalcOp {
     /// Resulting operator "x op z" if "x this y" and "y other z".
     /// Returns null if this and other are incompatible.
     /// </summary>
-    [Pure]
+    [System.Diagnostics.Contracts.Pure]
     public abstract CalcOp ResultOp(CalcOp other);
 
     /// <summary>
     /// Returns an expression "line0 this line1".
     /// </summary>
-    [Pure]
+    [System.Diagnostics.Contracts.Pure]
     public abstract Expression StepExpr(Expression line0, Expression line1);
   }
 
@@ -32,7 +33,7 @@ void ObjectInvariant() {
     /// <summary>
     /// Is op a valid calculation operator?
     /// </summary>
-    [Pure]
+    [System.Diagnostics.Contracts.Pure]
     public static bool ValidOp(BinaryExpr.Opcode op) {
       return
         op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Neq
@@ -44,7 +45,7 @@ public static bool ValidOp(BinaryExpr.Opcode op) {
     /// <summary>
     /// Is op a valid operator only for Boolean lines?
     /// </summary>
-    [Pure]
+    [System.Diagnostics.Contracts.Pure]
     public static bool LogicOp(BinaryExpr.Opcode op) {
       return op == BinaryExpr.Opcode.Iff || op == BinaryExpr.Opcode.Imp || op == BinaryExpr.Opcode.Exp;
     }
@@ -84,7 +85,7 @@ private bool Subsumes(BinaryCalcOp other) {
     public override CalcOp ResultOp(CalcOp other) {
       if (other is BinaryCalcOp) {
         var o = (BinaryCalcOp)other;
-        if (this.Subsumes(o)) {
+        if (Subsumes(o)) {
           return this;
         } else if (o.Subsumes(this)) {
           return other;
@@ -153,6 +154,48 @@ public override string ToString() {
 
   }
 
+  /// <summary>
+  /// This method infers a default operator to be used between the steps.
+  /// Usually, we'd use == as the default operator.  However, if the calculation
+  /// begins or ends with a boolean literal, then we can do better by selecting ==>
+  /// or <==.  Also, if the calculation begins or ends with an empty set, then we can
+  /// do better by selecting <= or >=.
+  /// Note, these alternative operators are chosen only if they don't clash with something
+  /// supplied by the user.
+  /// If the rules come up with a good inferred default operator, then that default operator
+  /// is returned; otherwise, null is returned.
+  /// </summary>
+  [CanBeNull]
+  public CalcOp GetInferredDefaultOp() {
+    CalcOp alternativeOp = null;
+    if (Lines.Count == 0) {
+      return null;
+    }
+
+    if (Expression.IsBoolLiteral(Lines.First(), out var firstOperatorIsBoolLiteral)) {
+      alternativeOp = new BinaryCalcOp(firstOperatorIsBoolLiteral ? BinaryExpr.Opcode.Imp : BinaryExpr.Opcode.Exp);
+    } else if (Expression.IsBoolLiteral(Lines.Last(), out var lastOperatorIsBoolLiteral)) {
+      alternativeOp = new BinaryCalcOp(lastOperatorIsBoolLiteral ? BinaryExpr.Opcode.Exp : BinaryExpr.Opcode.Imp);
+    } else if (Expression.IsEmptySetOrMultiset(Lines.First())) {
+      alternativeOp = new BinaryCalcOp(BinaryExpr.Opcode.Ge);
+    } else if (Expression.IsEmptySetOrMultiset(Lines.Last())) {
+      alternativeOp = new BinaryCalcOp(BinaryExpr.Opcode.Le);
+    } else {
+      return null;
+    }
+
+    // Check that the alternative operator is compatible with anything supplied by the user.
+    var resultOp = alternativeOp;
+    foreach (var stepOp in StepOps.Where(stepOp => stepOp != null)) {
+      resultOp = resultOp.ResultOp(stepOp);
+      if (resultOp == null) {
+        // no go
+        return null;
+      }
+    }
+    return alternativeOp;
+  }
+
   public readonly List<Expression> Lines;    // Last line is dummy, in order to form a proper step with the dangling hint
   public readonly List<BlockStmt> Hints;     // Hints[i] comes after line i; block statement is used as a container for multiple sub-hints
   public readonly CalcOp UserSuppliedOp;     // may be null, if omitted by the user
@@ -189,13 +232,13 @@ public CalcStmt(RangeToken rangeToken, CalcOp userSuppliedOp, List<Expression> l
     Contract.Requires(cce.NonNullElements(hints));
     Contract.Requires(hints.Count == Math.Max(lines.Count - 1, 0));
     Contract.Requires(stepOps.Count == hints.Count);
-    this.UserSuppliedOp = userSuppliedOp;
-    this.Lines = lines;
-    this.Hints = hints;
+    UserSuppliedOp = userSuppliedOp;
+    Lines = lines;
+    Hints = hints;
     Steps = new List<Expression>();
-    this.StepOps = stepOps;
-    this.Result = null;
-    this.Attributes = attrs;
+    StepOps = stepOps;
+    Result = null;
+    Attributes = attrs;
   }
 
   public CalcStmt Clone(Cloner cloner) {
@@ -291,7 +334,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
     var inOrdinal = false;
     var innerCalcIndent = indentBefore + formatter.SpaceTab;
     var extraHintIndent = 0;
-    var ownedTokens = this.OwnedTokens;
+    var ownedTokens = OwnedTokens;
     // First phase: We get the alignment
     foreach (var token in ownedTokens) {
       if (formatter.SetIndentLabelTokens(token, indentBefore)) {
@@ -366,7 +409,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
       }
     }
 
-    foreach (var hint in this.Hints) {
+    foreach (var hint in Hints) {
       // This block
       if (hint.Tok.pos != hint.EndToken.pos) {
         foreach (var hintStep in hint.Body) {
@@ -375,7 +418,7 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
       }
     }
 
-    foreach (var expression in this.Lines) {
+    foreach (var expression in Lines) {
       formatter.SetIndentations(expression.StartToken, innerCalcIndent, innerCalcIndent, innerCalcIndent);
     }
 

Source/DafnyCore/Resolver/NameResolutionAndTypeInference.cs

@@ -4521,26 +4521,7 @@ public void ResolveStatement(Statement stmt, ResolutionContext resolutionContext
         if (s.UserSuppliedOp != null) {
           s.Op = s.UserSuppliedOp;
         } else {
-          // Usually, we'd use == as the default main operator.  However, if the calculation
-          // begins or ends with a boolean literal, then we can do better by selecting ==>
-          // or <==.  Also, if the calculation begins or ends with an empty set, then we can
-          // do better by selecting <= or >=.
-          if (s.Lines.Count == 0) {
-            s.Op = CalcStmt.DefaultOp;
-          } else {
-            bool b;
-            if (Expression.IsBoolLiteral(s.Lines.First(), out b)) {
-              s.Op = new CalcStmt.BinaryCalcOp(b ? BinaryExpr.Opcode.Imp : BinaryExpr.Opcode.Exp);
-            } else if (Expression.IsBoolLiteral(s.Lines.Last(), out b)) {
-              s.Op = new CalcStmt.BinaryCalcOp(b ? BinaryExpr.Opcode.Exp : BinaryExpr.Opcode.Imp);
-            } else if (Expression.IsEmptySetOrMultiset(s.Lines.First())) {
-              s.Op = new CalcStmt.BinaryCalcOp(BinaryExpr.Opcode.Ge);
-            } else if (Expression.IsEmptySetOrMultiset(s.Lines.Last())) {
-              s.Op = new CalcStmt.BinaryCalcOp(BinaryExpr.Opcode.Le);
-            } else {
-              s.Op = CalcStmt.DefaultOp;
-            }
-          }
+          s.Op = s.GetInferredDefaultOp() ?? CalcStmt.DefaultOp;
           reporter.Info(MessageSource.Resolver, s.Tok, s.Op.ToString());
         }
 

Test/git-issues/git-issue-3962.dfy

@@ -0,0 +1,25 @@
+// RUN: %exits-with 4 %dafny /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Issues(a: bool, s: set) {
+  // Each one of the following 8 calc statements used to cause a crash
+
+  if
+  case true =>
+    calc { a; <== false; }
+  case true =>
+    calc { true; <== a; }
+  case true =>
+    calc { a; ==> true; }
+  case true =>
+    calc { false; ==> a; }
+
+  case true =>
+    calc { s; >= ({}); }
+  case true =>
+    calc { s; > ({}); } // error: cannot prove calc step
+  case true =>
+    calc { {}; <= s; }
+  case true =>
+    calc { {}; < s; } // error: cannot prove calc step
+}

Test/git-issues/git-issue-3962.dfy.expect

@@ -0,0 +1,12 @@
+git-issue-3962.dfy(9,4): Info: ==
+git-issue-3962.dfy(11,4): Info: ==
+git-issue-3962.dfy(13,4): Info: ==
+git-issue-3962.dfy(15,4): Info: ==
+git-issue-3962.dfy(18,4): Info: ==
+git-issue-3962.dfy(20,4): Info: ==
+git-issue-3962.dfy(22,4): Info: ==
+git-issue-3962.dfy(24,4): Info: ==
+git-issue-3962.dfy(20,16): Error: the calculation step between the previous line and this line might not hold
+git-issue-3962.dfy(24,17): Error: the calculation step between the previous line and this line might not hold
+
+Dafny program verifier finished with 0 verified, 2 errors

docs/dev/news/3963.fix

@@ -0,0 +1 @@
+Select alternative default calc operator only if it doesn't clash with given step operators