fix: Select alternative default calc operator more carefully

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