chore: Improve code (#5042)

This PR consists only of minor code changes, like using more modern C#
constructions. (These particular changes were ones I came across as I
was working on other PRs, so they make no attempt at being exhaustive.)

Notes:
* The PR updates `.gitignore`
* There are lots of new calls to `Expression.CreateBoolLiteral`, which
creates a resolved boolean literal AST node. If I remember correctly,
one of those changes was actually a bug fix. I'm afraid I don't have the
test case in this PR, but it's somewhere in my upcoming PRs.
* In one place, I spotted a Rider warning that an enumeration was used
twice. I fixed that my adding a `.ToList()`.
* We don't really use `cce.NonNull` anymore, since Rider does some
static null checking. So, I removed some such wrapper that I thought
just cluttered up the code. (Historic note: Dafny was originally written
in Spec#, and then these had been `(!)` casts. When Spec# was at its end
of life, the Boogie and Dafny sources were converted to C#, at which
point these non-null casts were turned into the `cce.NonNull` wrappers.)
* A call to `Expression.IsIntLiteral` was assuming something about the
out-parameter when the method return `false`. I changed this to instead
look at the return value.

<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>

.gitignore

@@ -73,3 +73,9 @@ docs/dev/*.fix
 docs/dev/*.feat
 docs/dev/*.break
 
+Source/IntegrationTests/TestFiles/LitTests/LitTest/server/*.bvd
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/Inputs/wrappers3.doo
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/replaceables/complex/Build1
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/separate-verification/assumptions-lib
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/log.smt2
+/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/model

Source/DafnyCore/AST/Expressions/Comprehensions/ComprehensionExpr.cs

@@ -105,12 +105,13 @@ static Expression ChooseBestIntegerBound([CanBeNull] Expression a, [CanBeNull] E
  return a ?? b;
  }
 
- if (Expression.IsIntLiteral(Expression.StripParensAndCasts(a), out var aa) &&
- Expression.IsIntLiteral(Expression.StripParensAndCasts(b), out var bb)) {
+ if (Expression.IsIntLiteral(a, out var aa) && Expression.IsIntLiteral(b, out var bb)) {
  var x = pickMax ? BigInteger.Max(aa, bb) : BigInteger.Min(aa, bb);
  return new LiteralExpr(a.tok, x) { Type = a.Type };
  }
- return a; // we don't know how to determine which of "a" or "b" is better, so we'll just return "a"
+ // we don't know how to determine which of "a" or "b" is better, so we'll just return "a"
+ // (better would be to return an expression that computes to the minimum of "a" and "b")
+ return a;
  }
 
  public static List<VT> MissingBounds<VT>(List<VT> vars, List<BoundedPool> bounds, PoolVirtues requiredVirtues = PoolVirtues.None) where VT : IVariable {

Source/DafnyCore/AST/Expressions/Conditional/NestedMatchStmt.cs

@@ -20,7 +20,7 @@ private void InitializeAttributes() {
  foreach (var c in this.Cases) {
  if (!Attributes.Contains(c.Attributes, "split")) {
  List<Expression> args = new List<Expression>();
- args.Add(new LiteralExpr(c.Tok, splitMatch));
+ args.Add(Expression.CreateBoolLiteral(c.Tok, splitMatch));
  Attributes attrs = new Attributes("split", args, c.Attributes);
  c.Attributes = attrs;
  }

Source/DafnyCore/AST/Expressions/Expression.cs

@@ -418,8 +418,9 @@ public static Expression CreateNatLiteral(IToken tok, int n, Type ty) {
  /// </summary>
  public static LiteralExpr CreateBoolLiteral(IToken tok, bool b) {
  Contract.Requires(tok != null);
- var lit = new LiteralExpr(tok, b);
- lit.Type = Type.Bool; // resolve here
+ var lit = new LiteralExpr(tok, b) {
+ Type = Type.Bool
+ };
  return lit;
  }
 
@@ -429,8 +430,9 @@ public static LiteralExpr CreateBoolLiteral(IToken tok, bool b) {
  public static LiteralExpr CreateStringLiteral(IToken tok, string s) {
  Contract.Requires(tok != null);
  Contract.Requires(s != null);
- var lit = new StringLiteralExpr(tok, s, true);
- lit.Type = new SeqType(new CharType()); // resolve here
+ var lit = new StringLiteralExpr(tok, s, true) {
+ Type = new SeqType(new CharType())
+ };
  return lit;
  }
 
@@ -440,8 +442,7 @@ public static LiteralExpr CreateStringLiteral(IToken tok, string s) {
  /// </summary>
  public static Expression StripParens(Expression expr) {
  while (true) {
- var e = expr as ParensExpression;
- if (e == null) {
+ if (expr is not ParensExpression e) {
  return expr;
  }
  expr = e.E;
@@ -493,11 +494,11 @@ public static bool IsBoolLiteral(Expression expr, out bool value) {
  /// </summary>
  public static bool IsIntLiteral(Expression expr, out BigInteger value) {
  Contract.Requires(expr != null);
- var e = StripParens(expr) as LiteralExpr;
- if (e != null && e.Value is int x) {
+ var e = StripParensAndCasts(expr) as LiteralExpr;
+ if (e is { Value: int x }) {
  value = new BigInteger(x);
  return true;
- } else if (e != null && e.Value is BigInteger xx) {
+ } else if (e is { Value: BigInteger xx }) {
  value = xx;
  return true;
  } else {

Source/DafnyCore/AST/Expressions/Operators/BinaryExpr.cs

@@ -51,8 +51,8 @@ public enum ResolvedOpcode {
  Le,
  Ge,
  Gt,
- Add,
- Sub,
+ Add, // also used for char
+ Sub, // also used for char
  Mul,
  Div,
  Mod,

Source/DafnyCore/AST/Expressions/StmtExpr.cs

@@ -62,9 +62,9 @@ public Expression GetSConclusion() {
  var s = (CalcStmt)S;
  return s.Result;
  } else if (S is RevealStmt) {
- return new LiteralExpr(tok, true); // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :)
+ return CreateBoolLiteral(tok, true); // one could use the definition axiom or the referenced labeled assertions, but "true" is conservative and much simpler :)
  } else if (S is UpdateStmt) {
- return new LiteralExpr(tok, true); // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :)
+ return CreateBoolLiteral(tok, true); // one could use the postcondition of the method, suitably instantiated, but "true" is conservative and much simpler :)
  } else {
  Contract.Assert(false); throw new cce.UnreachableException(); // unexpected statement
  }

Source/DafnyCore/AST/Members/Function.cs

@@ -536,8 +536,7 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
  }
 
  if (autoRevealDepth > 0) {
- Expression reqExpr = new LiteralExpr(Tok, true);
- reqExpr.Type = Type.Bool;
+ Expression reqExpr = Expression.CreateBoolLiteral(Tok, true);
 
  var bodyExpr = Body;
 

Source/DafnyCore/AST/Members/Method.cs

@@ -450,9 +450,7 @@ public void AutoRevealDependencies(AutoRevealFunctionDependencies Rewriter, Dafn
  }
 
  if (autoRevealDepth > 0) {
- Expression reqExpr = new LiteralExpr(Tok, true) {
- Type = Type.Bool
- };
+ Expression reqExpr = Expression.CreateBoolLiteral(Tok, true);
 
  foreach (var revealStmt in addedReveals) {
  if (revealStmt.Depth <= autoRevealDepth) {

Source/DafnyCore/AST/Substituter.cs

@@ -519,7 +519,9 @@ public ComprehensionExpr.BoundedPool SubstituteBoundedPool(ComprehensionExpr.Bou
  return bound; // nothing to substitute
  } else if (bound is ComprehensionExpr.IntBoundedPool) {
  var b = (ComprehensionExpr.IntBoundedPool)bound;
- return new ComprehensionExpr.IntBoundedPool(b.LowerBound == null ? null : Substitute(b.LowerBound), b.UpperBound == null ? null : Substitute(b.UpperBound));
+ return new ComprehensionExpr.IntBoundedPool(
+ b.LowerBound == null ? null : Substitute(b.LowerBound),
+ b.UpperBound == null ? null : Substitute(b.UpperBound));
  } else if (bound is ComprehensionExpr.SetBoundedPool) {
  var b = (ComprehensionExpr.SetBoundedPool)bound;
  return new ComprehensionExpr.SetBoundedPool(Substitute(b.Set), b.BoundVariableType, b.CollectionElementType, b.IsFiniteCollection);

Source/DafnyCore/AST/TypeDeclarations/NewtypeDecl.cs

@@ -33,8 +33,7 @@ public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Ty
  this.NewSelfSynonym();
  }
  public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, BoundVar bv, Expression constraint,
- SubsetTypeDecl.WKind witnessKind, Expression witness, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining)
- : base(rangeToken, name, module, new List<TypeParameter>(), members, attributes, isRefining, parentTraits) {
+ SubsetTypeDecl.WKind witnessKind, Expression witness, List<Type> parentTraits, List<MemberDecl> members, Attributes attributes, bool isRefining) : base(rangeToken, name, module, new List<TypeParameter>(), members, attributes, isRefining, parentTraits) {
  Contract.Requires(rangeToken != null);
  Contract.Requires(name != null);
  Contract.Requires(module != null);
@@ -49,8 +48,7 @@ public NewtypeDecl(RangeToken rangeToken, Name name, ModuleDefinition module, Bo
  this.NewSelfSynonym();
  }
 
- /// <summary>
- /// Return .BaseType instantiated with "typeArgs", but only look at the part of .BaseType that is in scope.
+ /// <summary> /// Return .BaseType instantiated with "typeArgs", but only look at the part of .BaseType that is in scope.
  /// </summary>
  public Type RhsWithArgument(List<Type> typeArgs) {
  Contract.Requires(typeArgs != null);

Source/DafnyCore/AST/TypeDeclarations/SubsetTypeDecl.cs

@@ -12,7 +12,6 @@ public class SubsetTypeDecl : TypeSynonymDecl, RedirectingTypeDecl, ICanAutoReve
  public enum WKind { CompiledZero, Compiled, Ghost, OptOut, Special }
  public readonly WKind WitnessKind;
  public Expression/*?*/ Witness; // non-null iff WitnessKind is Compiled or Ghost
- [FilledInDuringResolution] public bool CheckedIfConstraintIsCompilable = false; // Set to true lazily by the Resolver when the Resolver fills in "ConstraintIsCompilable".
 
  [FilledInDuringResolution] bool RedirectingTypeDecl.ConstraintIsCompilable { get; set; }
 

Source/DafnyCore/AST/TypeDeclarations/TypeSynonymDeclBase.cs

@@ -67,7 +67,7 @@ public Type RhsWithArgumentIgnoringScope(List<Type> typeArgs) {
  Expression RedirectingTypeDecl.Constraint { get { return null; } }
 
  bool RedirectingTypeDecl.ConstraintIsCompilable {
- get => false;
+ get => throw new NotSupportedException();
  set => throw new NotSupportedException();
  }
 

Source/DafnyCore/AST/Types/Types.cs

@@ -94,8 +94,7 @@ public string TypeArgsToString(DafnyOptions options, ModuleDefinition/*?*/ conte
  public void AddFreeTypeParameters(ISet<TypeParameter> tps) {
  Contract.Requires(tps != null);
  var ty = this.NormalizeExpandKeepConstraints();
- var tp = ty.AsTypeParameter;
- if (tp != null) {
+ if (ty.AsTypeParameter is { } tp) {
  tps.Add(tp);
  }
  foreach (var ta in ty.TypeArgs) {
@@ -186,9 +185,7 @@ public Type NormalizeExpand(ExpandMode expandMode = ExpandMode.ExpandSynonymsAnd
 
  Type type = this;
  while (true) {
-
- var pt = type as TypeProxy;
- if (pt != null && pt.T != null) {
+ if (type is TypeProxy { T: not null } pt) {
  type = pt.T;
  continue;
  }
@@ -579,15 +576,13 @@ public UserDefinedType AsNonNullRefType {
  get {
  var t = this;
  while (true) {
- var udt = t.NormalizeExpandKeepConstraints() as UserDefinedType;
- if (udt == null) {
+ if (t.NormalizeExpandKeepConstraints() is not UserDefinedType udt) {
  return null;
  }
  if (udt.ResolvedClass is NonNullTypeDecl) {
  return udt;
  }
- var sst = udt.ResolvedClass as SubsetTypeDecl;
- if (sst != null) {
+ if (udt.ResolvedClass is SubsetTypeDecl sst) {
  t = sst.RhsWithArgument(udt.TypeArgs); // continue the search up the chain of subset types
  } else {
  return null;

Source/DafnyCore/CompileNestedMatch/MatchFlattener.cs

@@ -396,8 +396,7 @@ private CaseBody CompileHeadsContainingConstructor(MatchCompilationState mti, Ma
  }
 
  var args = new List<Expression>();
- var literalExpr = new LiteralExpr(mti.Tok, false);
- literalExpr.Type = Type.Bool;
+ var literalExpr = Expression.CreateBoolLiteral(mti.Tok, false);
  args.Add(literalExpr);
  c.Attributes = new Attributes("split", args, c.Attributes);
  }

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -2205,8 +2205,8 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
  }
  } else if (e is StringLiteralExpr str) {
  wr.Format($"{DafnySeqClass}<{CharTypeName}>.{CharMethodQualifier}FromString({StringLiteral(str)})");
- } else if (AsNativeType(e.Type) != null) {
- GetNativeInfo(AsNativeType(e.Type).Sel, out var nativeName, out var literalSuffix, out var needsCastAfterArithmetic);
+ } else if (AsNativeType(e.Type) is { } nativeType) {
+ GetNativeInfo(nativeType.Sel, out var nativeName, out var literalSuffix, out var needsCastAfterArithmetic);
  if (needsCastAfterArithmetic) {
  wr = wr.Write($"({nativeName})").ForkInParens();
  }
@@ -2290,11 +2290,11 @@ protected override ConcreteSyntaxTree EmitBitvectorTruncation(BitvectorType bvTy
 
  protected override void EmitRotate(Expression e0, Expression e1, bool isRotateLeft, ConcreteSyntaxTree wr,
  bool inLetExprBody, ConcreteSyntaxTree wStmts, FCE_Arg_Translator tr) {
- string nativeName = null, literalSuffix = null;
+ string nativeName = null;
  bool needsCast = false;
  var nativeType = AsNativeType(e0.Type);
  if (nativeType != null) {
- GetNativeInfo(nativeType.Sel, out nativeName, out literalSuffix, out needsCast);
+ GetNativeInfo(nativeType.Sel, out nativeName, out _, out needsCast);
  }
 
  // ( e0 op1 e1) | (e0 op2 (width - e1))
@@ -2308,7 +2308,7 @@ protected override void EmitRotate(Expression e0, Expression e1, bool isRotateLe
  EmitShift(e0, e1, isRotateLeft ? ">>" : "<<", !isRotateLeft, nativeType, false, wr.ForkInParens(), inLetExprBody, wStmts, tr);
  }
 
- void EmitShift(Expression e0, Expression e1, string op, bool truncate, NativeType nativeType /*?*/, bool firstOp,
+ private void EmitShift(Expression e0, Expression e1, string op, bool truncate, [CanBeNull] NativeType nativeType, bool firstOp,
  ConcreteSyntaxTree wr, bool inLetExprBody, ConcreteSyntaxTree wStmts, FCE_Arg_Translator tr) {
  var bv = e0.Type.AsBitVectorType;
  if (truncate) {

Source/DafnyCore/Compilers/Dafny/Compiler-dafny.cs

@@ -1885,7 +1885,6 @@ protected override void EmitDestructor(Action<ConcreteSyntaxTree> source, Formal
  }
  }
 
- protected override bool TargetLambdasRestrictedToExpressions => true;
  protected override ConcreteSyntaxTree CreateLambda(List<Type> inTypes, IToken tok, List<string> inNames,
  Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, bool untyped = false) {
  if (wr is BuilderSyntaxTree<ExprContainer> builder) {

Source/DafnyCore/Compilers/Java/Compiler-java.cs

@@ -1133,8 +1133,8 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) {
  wr.Write(UnicodeCharEnabled ? $"{DafnySeqClass}.asUnicodeString(" : $"{DafnySeqClass}.asString(");
  TrStringLiteral(str, wr);
  wr.Write(")");
- } else if (AsNativeType(e.Type) is NativeType nt) {
- EmitNativeIntegerLiteral((BigInteger)e.Value, nt, wr);
+ } else if (AsNativeType(e.Type) is { } nativeType) {
+ EmitNativeIntegerLiteral((BigInteger)e.Value, nativeType, wr);
  } else if (e.Value is BigInteger i) {
  if (i.IsZero) {
  wr.Write("java.math.BigInteger.ZERO");
@@ -1742,11 +1742,11 @@ protected override void EmitIndexCollectionUpdate(Expression source, Expression
 
  protected override void EmitRotate(Expression e0, Expression e1, bool isRotateLeft, ConcreteSyntaxTree wr,
  bool inLetExprBody, ConcreteSyntaxTree wStmts, FCE_Arg_Translator tr) {
- string nativeName = null, literalSuffix = null;
+ string nativeName = null;
  bool needsCast = false;
  var nativeType = AsNativeType(e0.Type);
  if (nativeType != null) {
- GetNativeInfo(nativeType.Sel, out nativeName, out literalSuffix, out needsCast);
+ GetNativeInfo(nativeType.Sel, out nativeName, out _, out needsCast);
  }
  var leftShift = nativeType == null ? ".shiftLeft" : "<<";
  var rightShift = nativeType == null ? ".shiftRight" : ">>>";
@@ -1770,7 +1770,7 @@ protected override void EmitRotate(Expression e0, Expression e1, bool isRotateLe
  }
  }
 
- void EmitShift(Expression e0, Expression e1, string op, bool truncate, NativeType nativeType /*?*/, bool firstOp,
+ private void EmitShift(Expression e0, Expression e1, string op, bool truncate, [CanBeNull] NativeType nativeType, bool firstOp,
  ConcreteSyntaxTree wr, bool inLetExprBody, ConcreteSyntaxTree wStmts, FCE_Arg_Translator tr) {
  var bv = e0.Type.AsBitVectorType;
  if (truncate) {

Source/DafnyCore/Compilers/Python/Compiler-python.cs

@@ -147,7 +147,7 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
  : "";
  var methodWriter = wr.NewBlockPy(header: $"class {IdProtect(name)}{baseClasses}:");
 
- var relevantTypeParameters = typeParameters.Where(NeedsTypeDescriptor);
+ var relevantTypeParameters = typeParameters.Where(NeedsTypeDescriptor).ToList();
  var args = relevantTypeParameters.Comma(tp => tp.GetCompileName(Options));
  if (!string.IsNullOrEmpty(args)) { args = $", {args}"; }
  var isNewtypeWithTraits = cls is NewtypeDecl { ParentTraits: { Count: > 0 } };
@@ -1404,7 +1404,6 @@ protected override void EmitDestructor(Action<ConcreteSyntaxTree> source, Formal
  }
  }
 
- protected override bool TargetLambdasRestrictedToExpressions => true;
  protected override ConcreteSyntaxTree CreateLambda(List<Type> inTypes, IToken tok, List<string> inNames,
  Type resultType, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts, bool untyped = false) {
  var functionName = ProtectedFreshId("_lambda");