fix: Select alternative default calc operator more carefully

Fixes #3962

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;
  }
@@ -153,6 +154,49 @@ 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() {
+ CalcStmt.CalcOp alternativeOp = null;
+ if (Lines.Count == 0) {
+ return null;
+ }
+
+ bool b;
+ if (Expression.IsBoolLiteral(Lines.First(), out b)) {
+ alternativeOp = new CalcStmt.BinaryCalcOp(b ? BinaryExpr.Opcode.Imp : BinaryExpr.Opcode.Exp);
+ } else if (Expression.IsBoolLiteral(Lines.Last(), out b)) {
+ alternativeOp = new CalcStmt.BinaryCalcOp(b ? BinaryExpr.Opcode.Exp : BinaryExpr.Opcode.Imp);
+ } else if (Expression.IsEmptySetOrMultiset(Lines.First())) {
+ alternativeOp = new CalcStmt.BinaryCalcOp(BinaryExpr.Opcode.Ge);
+ } else if (Expression.IsEmptySetOrMultiset(Lines.Last())) {
+ alternativeOp = new CalcStmt.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

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