chore: Enable dotnet_style_parentheses_in_other_binary_operators (#…

…1627)

add `dotnet_style_parentheses_in_other_binary_operators` as a warning and fix violations

.editorconfig

@@ -28,6 +28,9 @@ csharp_new_line_before_else = false
 csharp_prefer_braces = true:error
 dotnet_diagnostic.IDE0011.severity = error
 
+# Parentheses around logical operators
+dotnet_style_parentheses_in_other_binary_operators = always_for_clarity:error
+
 #### Naming rules
 
 ##### Private mutable fields

Source/Dafny/AST/DafnyAst.cs

@@ -7574,7 +7574,7 @@ void ObjectInvariant() {
  Contract.Invariant(Lhss != null);
  Contract.Invariant(
  Lhss.Count == 0 || // ":- MethodOrExpresion;" which returns void success or an error
- Lhss.Count == 1 && Lhss[0] != null // "y :- MethodOrExpression;"
+ (Lhss.Count == 1 && Lhss[0] != null) // "y :- MethodOrExpression;"
  );
  Contract.Invariant(Rhs != null);
  }
@@ -12499,7 +12499,7 @@ public class FrameExpression {
  [ContractInvariantMethod]
  void ObjectInvariant() {
  Contract.Invariant(E != null);
- Contract.Invariant(!(E is WildcardExpr) || FieldName == null && Field == null);
+ Contract.Invariant(!(E is WildcardExpr) || (FieldName == null && Field == null));
  }
 
  public readonly string FieldName;

Source/Dafny/AST/Printer.cs

@@ -921,7 +921,7 @@ private bool PrintModeSkipFunctionOrMethod(bool IsGhost, Attributes attributes,
 
  private bool PrintModeSkipGeneral(Bpl.IToken tok, string fileBeingPrinted) {
  return (printMode == DafnyOptions.PrintModes.NoIncludes || printMode == DafnyOptions.PrintModes.NoGhost)
- && (tok.filename != null && fileBeingPrinted != null && Path.GetFullPath(tok.filename) != fileBeingPrinted);
+ && tok.filename != null && fileBeingPrinted != null && Path.GetFullPath(tok.filename) != fileBeingPrinted;
  }
 
  public void PrintMethod(Method method, int indent, bool printSignatureOnly) {

Source/Dafny/Compilers/Compiler-Csharp.cs

@@ -811,7 +811,7 @@ public ClassWriter(CsharpCompiler compiler, ConcreteSyntaxTree instanceMemberWri
 
  public ConcreteSyntaxTree Writer(bool isStatic, bool createBody, MemberDecl/*?*/ member) {
  if (createBody) {
- if (isStatic || member?.EnclosingClass is TraitDecl && NeedsCustomReceiver(member)) {
+ if (isStatic || (member?.EnclosingClass is TraitDecl && NeedsCustomReceiver(member))) {
  return StaticMemberWriter;
  }
  }
@@ -1941,8 +1941,8 @@ protected override string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ memb
 
  protected override void EmitThis(ConcreteSyntaxTree wr) {
  var custom =
- enclosingMethod != null && enclosingMethod.IsTailRecursive ||
- enclosingFunction != null && enclosingFunction.IsTailRecursive ||
+ (enclosingMethod != null && enclosingMethod.IsTailRecursive) ||
+ (enclosingFunction != null && enclosingFunction.IsTailRecursive) ||
  thisContext is NewtypeDecl ||
  thisContext is TraitDecl;
  wr.Write(custom ? "_this" : "this");

Source/Dafny/Compilers/Compiler-go.cs

@@ -3230,7 +3230,7 @@ protected override void EmitTypeTest(string localName, Type fromType, Type toTyp
 
  private static bool EqualsUpToParameters(Type type1, Type type2) {
  // TODO Consider whether Type.SameHead should return true in this case
- return Type.SameHead(type1, type2) || type1.IsArrayType && type1.IsArrayType;
+ return Type.SameHead(type1, type2) || (type1.IsArrayType && type1.IsArrayType);
  }
 
  protected override ConcreteSyntaxTree EmitCoercionIfNecessary(Type/*?*/ from, Type/*?*/ to, Bpl.IToken tok, ConcreteSyntaxTree wr) {

Source/Dafny/Compilers/Compiler-java.cs

@@ -2481,7 +2481,7 @@ private string AddTypeDescriptorArgs(string fullCompileName, List<Type> typeArgs
 
  bool OutContainsParam(List<Formal> l, TypeParameter tp) {
  foreach (Formal f in l) {
- if (f.Type.IsTypeParameter && f.Type.AsTypeParameter.Equals(tp) || f.Type.AsCollectionType != null && f.Type.AsCollectionType.Arg.IsTypeParameter && f.Type.AsCollectionType.Arg.AsTypeParameter.Equals(tp)) {
+ if ((f.Type.IsTypeParameter && f.Type.AsTypeParameter.Equals(tp)) || (f.Type.AsCollectionType != null && f.Type.AsCollectionType.Arg.IsTypeParameter && f.Type.AsCollectionType.Arg.AsTypeParameter.Equals(tp))) {
  return true;
  }
  }

Source/Dafny/Compilers/Compiler.cs

@@ -1217,7 +1217,7 @@ public void Compile(Program program, ConcreteSyntaxTree wrx) {
  }
  var classIsExtern = false;
  if (include) {
- classIsExtern = !DafnyOptions.O.DisallowExterns && Attributes.Contains(cl.Attributes, "extern") || cl.IsDefaultClass && Attributes.Contains(cl.EnclosingModuleDefinition.Attributes, "extern");
+ classIsExtern = (!DafnyOptions.O.DisallowExterns && Attributes.Contains(cl.Attributes, "extern")) || (cl.IsDefaultClass && Attributes.Contains(cl.EnclosingModuleDefinition.Attributes, "extern"));
  if (classIsExtern && cl.Members.TrueForAll(member => member.IsGhost || Attributes.Contains(member.Attributes, "extern"))) {
  include = false;
  }
@@ -1745,7 +1745,7 @@ void CompileClassMembers(Program program, TopLevelDeclWithMembers c, IClassWrite
  } else if (f.IsGhost) {
  // nothing to compile, but we do check for assumes
  if (f.Body == null) {
- Contract.Assert(c is TraitDecl && !f.IsStatic || Attributes.Contains(f.Attributes, "extern"));
+ Contract.Assert((c is TraitDecl && !f.IsStatic) || Attributes.Contains(f.Attributes, "extern"));
  }
 
  if (Attributes.Contains(f.Attributes, "test")) {
@@ -3381,9 +3381,9 @@ private bool CanSequentializeForall(List<BoundVar> bvs, List<ComprehensionExpr.B
  return
  no1DArrayAccesses(sse.Seq, sse.E0, range, rhs) ||
 
- bvs.Count == 1 &&
+ (bvs.Count == 1 &&
  isVar(bvs[0], sse.E0) &&
- indexIsAlwaysVar(bvs[0], range, sse.Seq, rhs); // also covers sequence conversions
+ indexIsAlwaysVar(bvs[0], range, sse.Seq, rhs)); // also covers sequence conversions
  } else if (lhs is MultiSelectExpr mse) {
  return
  noMultiDArrayAccesses(mse.Array, range, rhs) &&
@@ -3395,9 +3395,9 @@ private bool CanSequentializeForall(List<BoundVar> bvs, List<ComprehensionExpr.B
  return
  noFieldAccesses(mse2.Member, mse2.Obj, range, rhs) ||
 
- bvs.Count == 1 &&
+ (bvs.Count == 1 &&
  isVar(bvs[0], mse2.Obj) &&
- accessedObjectIsAlwaysVar(mse2.Member, bvs[0], range, rhs);
+ accessedObjectIsAlwaysVar(mse2.Member, bvs[0], range, rhs));
  }
 
  bool noImpureFunctionCalls(params Expression[] exprs) {

Source/Dafny/Reporting.cs

@@ -193,7 +193,7 @@ private ConsoleColor ColorForLevel(ErrorLevel level) {
  }
 
  public override bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {
- if (base.Message(source, level, tok, msg) && (DafnyOptions.O != null && DafnyOptions.O.PrintTooltips || level != ErrorLevel.Info)) {
+ if (base.Message(source, level, tok, msg) && ((DafnyOptions.O != null && DafnyOptions.O.PrintTooltips) || level != ErrorLevel.Info)) {
  // Extra indent added to make it easier to distinguish multiline error messages for clients that rely on the CLI
  msg = msg.Replace(Environment.NewLine, Environment.NewLine + " ");
 

Source/Dafny/Resolver.cs

@@ -70,7 +70,7 @@ public static Thing Create(ModuleDefinition m, Thing a, Thing b, IEqualityCompar
  Contract.Requires(b != null);
  Contract.Requires(eq != null);
  Contract.Ensures(Contract.Result<Thing>() != null ||
- (Contract.ValueAtReturn(out s) != null || 2 <= Contract.ValueAtReturn(out s).Count));
+ Contract.ValueAtReturn(out s) != null || 2 <= Contract.ValueAtReturn(out s).Count);
  s = null;
  if (eq.Equals(a, b)) {
  return a;

Source/DafnyDriver/DafnyDriver.cs

@@ -478,7 +478,7 @@ public static bool Compile(string fileName, ReadOnlyCollection<string> otherFile
  WriteStatss(statss);
  if ((DafnyOptions.O.Compile && verified && !CommandLineOptions.Clo.UserConstrainedProcsToCheck) || DafnyOptions.O.ForceCompile) {
  compiled = CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, true);
- } else if (2 <= DafnyOptions.O.SpillTargetCode && verified && !CommandLineOptions.Clo.UserConstrainedProcsToCheck || 3 <= DafnyOptions.O.SpillTargetCode) {
+ } else if ((2 <= DafnyOptions.O.SpillTargetCode && verified && !CommandLineOptions.Clo.UserConstrainedProcsToCheck) || 3 <= DafnyOptions.O.SpillTargetCode) {
  compiled = CompileDafnyProgram(dafnyProgram, resultFileName, otherFileNames, false);
  }
  break;

Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs

@@ -390,10 +390,10 @@ private DafnyModelType ReconstructType(Model.Element typeElement) {
  return new DafnyModelType("?");
  }
  var tagName = GetTrueName(tagElement);
- if (tagName == null || tagName.Length < 10 && tagName != "TagSeq" &&
+ if (tagName == null || (tagName.Length < 10 && tagName != "TagSeq" &&
  tagName != "TagSet" &&
  tagName != "TagBitVector" &&
- tagName != "TagMap") {
+ tagName != "TagMap")) {
  return new DafnyModelType("?");
  }
  var typeArgs = Model.GetFunc("T" + tagName.Substring(3))?.

Source/DafnyTestGeneration.Test/Various.cs

@@ -201,25 +201,25 @@ decreases 3 - counter {
  m.DafnyInfo.IsStatic("Objects.List.IsACircleOfLessThanThree")));
  Assert.IsTrue(methods.All(m => m.ArgValues.Count == 1));
  Assert.IsTrue(methods.Exists(m =>
- m.Assignments.Count == 1 && m.Assignments[0] == ("v0", "next", "v0") &&
- m.ObjectsToMock.Count == 1 ||
- m.Assignments.Count == 2 && m.Assignments[1] == ("v0", "next", "v1") &&
+ (m.Assignments.Count == 1 && m.Assignments[0] == ("v0", "next", "v0") &&
+ m.ObjectsToMock.Count == 1) ||
+ (m.Assignments.Count == 2 && m.Assignments[1] == ("v0", "next", "v1") &&
  m.Assignments[0] == ("v1", "next", "v0") &&
- m.ObjectsToMock.Count == 2));
+ m.ObjectsToMock.Count == 2)));
  Assert.IsTrue(methods.Exists(m =>
- m.Assignments.Count > 2 && m.ObjectsToMock.Count > 2 &&
+ (m.Assignments.Count > 2 && m.ObjectsToMock.Count > 2 &&
  m.Assignments.Last() == ("v0", "next", "v1") &&
- m.Assignments[^2] == ("v1", "next", "v2") ||
- m.Assignments.Count == 2 && m.ObjectsToMock.Count == 2 &&
+ m.Assignments[^2] == ("v1", "next", "v2")) ||
+ (m.Assignments.Count == 2 && m.ObjectsToMock.Count == 2 &&
  m.Assignments[1] == ("v0", "next", "v1") &&
- m.Assignments[0] == ("v1", "next", "v1")));
+ m.Assignments[0] == ("v1", "next", "v1"))));
  Assert.IsTrue(methods.Exists(m =>
- m.Assignments.Count == 1 &&
+ (m.Assignments.Count == 1 &&
  m.Assignments[0] == ("v0", "next", "null") &&
- m.ObjectsToMock.Count == 1 ||
- m.Assignments.Count == 2 && m.Assignments[1] == ("v0", "next", "v1") &&
+ m.ObjectsToMock.Count == 1) ||
+ (m.Assignments.Count == 2 && m.Assignments[1] == ("v0", "next", "v1") &&
  m.Assignments[0] == ("v1", "next", "null") &&
- m.ObjectsToMock.Count == 2));
+ m.ObjectsToMock.Count == 2)));
  }
 
  [TestMethod]