Use native byte/char arrays in Go

Source/DafnyCore/AST/Expressions/ComprehensionExpr.cs

@@ -1,7 +1,9 @@
 using System;
 using System.Collections.Generic;
 using System.Diagnostics.Contracts;
+using System.Numerics;
 using System.Linq;
+using JetBrains.Annotations;
 
 namespace Microsoft.Dafny;
 
@@ -89,13 +91,32 @@ public static BoundedPool GetBest(List<BoundedPool> bounds, PoolVirtues required
       BoundedPool best = null;
       foreach (var bound in bounds) {
         if ((bound.Virtues & requiredVirtues) == requiredVirtues) {
-          if (best == null || bound.Preference() > best.Preference()) {
+          if (best is IntBoundedPool ibp0 && bound is IntBoundedPool ibp1) {
+            best = new IntBoundedPool(
+              ChooseBestIntegerBound(ibp0.LowerBound, ibp1.LowerBound, true),
+              ChooseBestIntegerBound(ibp0.UpperBound, ibp1.UpperBound, false));
+          } else if (best == null || bound.Preference() > best.Preference()) {
             best = bound;
           }
         }
       }
       return best;
     }
+
+    [CanBeNull]
+    static Expression ChooseBestIntegerBound([CanBeNull] Expression a, [CanBeNull] Expression b, bool pickMax) {
+      if (a == null || b == null) {
+        return a ?? b;
+      }
+
+      if (Expression.IsIntLiteral(Expression.StripParensAndCasts(a), out var aa) &&
+          Expression.IsIntLiteral(Expression.StripParensAndCasts(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"
+    }
+
     public static List<VT> MissingBounds<VT>(List<VT> vars, List<BoundedPool> bounds, PoolVirtues requiredVirtues = PoolVirtues.None) where VT : IVariable {
       Contract.Requires(vars != null);
       Contract.Requires(bounds == null || vars.Count == bounds.Count);

Source/DafnyCore/AST/Expressions/Expressions.cs

@@ -15,7 +15,7 @@ void ObjectInvariant() {
     Contract.Invariant(tok != null);
   }
 
-  [Pure]
+  [System.Diagnostics.Contracts.Pure]
   public bool WasResolved() {
     return Type != null;
   }
@@ -343,30 +343,30 @@ public static Expression CreateIncrement(Expression e, int n) {
   /// <summary>
   /// Create a resolved expression of the form "e - n"
   /// </summary>
-  public static Expression CreateDecrement(Expression e, int n) {
+  public static Expression CreateDecrement(Expression e, int n, Type ty = null) {
     Contract.Requires(e != null);
     Contract.Requires(e.Type.IsNumericBased(Type.NumericPersuasion.Int));
     Contract.Requires(0 <= n);
     Contract.Ensures(Contract.Result<Expression>() != null);
     if (n == 0) {
       return e;
     }
-    var nn = CreateIntLiteral(e.tok, n);
+    var nn = CreateIntLiteral(e.tok, n, ty);
     return CreateSubtract(e, nn);
   }
 
   /// <summary>
   /// Create a resolved expression of the form "n"
   /// </summary>
-  public static Expression CreateIntLiteral(IToken tok, int n) {
+  public static Expression CreateIntLiteral(IToken tok, int n, Type ty = null) {
     Contract.Requires(tok != null);
     Contract.Requires(n != int.MinValue);
     if (0 <= n) {
       var nn = new LiteralExpr(tok, n);
-      nn.Type = Type.Int;
+      nn.Type = ty ?? Type.Int;
       return nn;
     } else {
-      return CreateDecrement(CreateIntLiteral(tok, 0), -n);
+      return CreateDecrement(CreateIntLiteral(tok, 0, ty), -n, ty);
     }
   }
 
@@ -427,6 +427,22 @@ public static Expression StripParens(Expression expr) {
     }
   }
 
+  /// <summary>
+  /// Returns "expr", but with all outer layers of parentheses and casts removed.
+  /// This method can be called before resolution.
+  /// </summary>
+  public static Expression StripParensAndCasts(Expression expr) {
+    while (true) {
+      if (expr is ParensExpression parens) {
+        expr = parens.E;
+      } else if (expr is ConversionExpr cast) {
+        expr = cast.E;
+      } else {
+        return expr;
+      }
+    }
+  }
+
   public static ThisExpr AsThis(Expression expr) {
     Contract.Requires(expr != null);
     return StripParens(expr) as ThisExpr;
@@ -449,6 +465,26 @@ public static bool IsBoolLiteral(Expression expr, out bool value) {
     }
   }
 
+  /// <summary>
+  /// If "expr" denotes an integer literal "x", then return "true" and set "value" to "x".
+  /// Otherwise, return "false" (and the value of "value" should not be used by the caller).
+  /// This method can be called before resolution.
+  /// </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) {
+      value = new BigInteger(x);
+      return true;
+    } else if (e != null && e.Value is BigInteger xx) {
+      value = xx;
+      return true;
+    } else {
+      value = BigInteger.Zero; // to please compiler
+      return false;
+    }
+  }
+
   /// <summary>
   /// Returns "true" if "expr" denotes the empty set (for "iset", "set", or "multiset").
   /// This method can be called before resolution.
@@ -801,7 +837,7 @@ public class LiteralExpr : Expression {
   /// </summary>
   public readonly object Value;
 
-  [Pure]
+  [System.Diagnostics.Contracts.Pure]
   public static bool IsTrue(Expression e) {
     Contract.Requires(e != null);
     return Expression.IsBoolLiteral(e, out var value) && value;
@@ -1129,7 +1165,7 @@ public override Type ReplaceTypeArguments(List<Type> arguments) {
     }
   }
   public class ResolverType_Module : ResolverType {
-    [Pure]
+    [System.Diagnostics.Contracts.Pure]
     public override string TypeName(ModuleDefinition context, bool parseAble) {
       Contract.Assert(parseAble == false);
       return "#module";
@@ -1139,7 +1175,7 @@ public override bool Equals(Type that, bool keepConstraints = false) {
     }
   }
   public class ResolverType_Type : ResolverType {
-    [Pure]
+    [System.Diagnostics.Contracts.Pure]
     public override string TypeName(ModuleDefinition context, bool parseAble) {
       Contract.Assert(parseAble == false);
       return "#type";

Source/DafnyCore/AST/Printer.cs

@@ -1835,11 +1835,9 @@ void PrintRhs(AssignmentRhs rhs) {
           if (ShowType(t.EType)) {
             PrintType(t.EType);
           }
-          var dim0 = t.ArrayDimensions[0] as LiteralExpr;
           if (DafnyOptions.O.DafnyPrintResolvedFile == null &&
-            t.InitDisplay != null &&
-            t.ArrayDimensions.Count == 1 && dim0.Value is BigInteger &&
-            (BigInteger)dim0.Value == new BigInteger(t.InitDisplay.Count)) {
+            t.InitDisplay != null && t.ArrayDimensions.Count == 1 &&
+            AutoGeneratedToken.Is(t.ArrayDimensions[0].tok)) {
             // elide the size
             wr.Write("[]");
           } else {

Source/DafnyCore/Compilers/Compiler-Csharp.cs

@@ -1475,6 +1475,7 @@ internal override string TypeName(Type type, ConcreteSyntaxTree wr, IToken tok,
     // To improve readability
     private static bool CharIsRune => UnicodeCharEnabled;
     private static string CharTypeName => UnicodeCharEnabled ? "Dafny.Rune" : "char";
+    private static string CharTypeDescriptorName => DafnyHelpersClass + (UnicodeCharEnabled ? ".RUNE" : ".CHAR");
 
     private void ConvertFromChar(Expression e, ConcreteSyntaxTree wr, bool inLetExprBody, ConcreteSyntaxTree wStmts) {
       if (e.Type.IsCharType && UnicodeCharEnabled) {
@@ -1529,7 +1530,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
       if (xType is BoolType) {
         return "false";
       } else if (xType is CharType) {
-        return CharType.DefaultValueAsString;
+        return UnicodeCharEnabled ? $"new {CharTypeName}({CharType.DefaultValueAsString})" : CharType.DefaultValueAsString;
       } else if (xType is IntType || xType is BigOrdinalType) {
         return "BigInteger.Zero";
       } else if (xType is RealType) {
@@ -1650,7 +1651,7 @@ protected override string TypeDescriptor(Type type, ConcreteSyntaxTree wr, IToke
       if (type is BoolType) {
         return "Dafny.Helpers.BOOL";
       } else if (type is CharType) {
-        return "Dafny.Helpers.CHAR";
+        return CharTypeDescriptorName;
       } else if (type is IntType || type is BigOrdinalType) {
         return "Dafny.Helpers.INT";
       } else if (type is RealType) {
@@ -1930,8 +1931,9 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
       return startWr;
     }
 
-    protected override ConcreteSyntaxTree CreateForLoop(string indexVar, string bound, ConcreteSyntaxTree wr) {
-      return wr.NewNamedBlock("for (var {0} = 0; {0} < {1}; {0}++)", indexVar, bound);
+    protected override ConcreteSyntaxTree CreateForLoop(string indexVar, string bound, ConcreteSyntaxTree wr, string start = null) {
+      start = start ?? "0";
+      return wr.NewNamedBlock("for (var {0} = {2}; {0} < {1}; {0}++)", indexVar, bound, start);
     }
 
     protected override ConcreteSyntaxTree CreateDoublingForLoop(string indexVar, int start, ConcreteSyntaxTree wr) {
@@ -2000,37 +2002,30 @@ protected override void EmitNew(Type type, IToken tok, CallStmt initCall /*?*/,
       arguments.Write(ConstructorArguments(initCall, wStmts, ctor, sep));
     }
 
-    // if checkRange is false, msg is ignored
-    // if checkRange is true and msg is null and the value is out of range, a generic message is emitted
-    // if checkRange is true and msg is not null and the value is out of range, msg is emitted in the error message
-    protected void TrExprAsInt(Expression expr, ConcreteSyntaxTree wr, bool inLetExprBody, ConcreteSyntaxTree wStmts,
-        bool checkRange = false, string msg = null) {
-      wr.Write($"{GetHelperModuleName()}.ToIntChecked(");
-      TrExpr(expr, wr, inLetExprBody, wStmts);
-      if (checkRange) {
-        wr.Write(msg == null ? ", null" : $", \"{msg}\")");
-      }
-    }
-
-    protected override void EmitNewArray(Type elmtType, IToken tok, List<Expression> dimensions,
-        bool mustInitialize, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
-      var wrs = EmitNewArray(elmtType, tok, dimensions.Count, mustInitialize, wr);
+    protected override void EmitNewArray(Type elementType, IToken tok, List<string> dimensions,
+        bool mustInitialize, [CanBeNull] string exampleElement, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      var wrs = EmitNewArray(elementType, tok, dimensions.Count, mustInitialize, wr);
       for (var i = 0; i < wrs.Count; i++) {
-        TrExprAsInt(dimensions[i], wrs[i], inLetExprBody: false, wStmts, true, "C# arrays may not be larger than the max 32-bit integer");
+        wrs[i].Write(dimensions[i]);
       }
     }
 
     private List<ConcreteSyntaxTree> EmitNewArray(Type elmtType, IToken tok, int dimCount, bool mustInitialize, ConcreteSyntaxTree wr) {
+      ConcreteSyntaxTree EmitSizeCheckWrapper(ConcreteSyntaxTree w) {
+        w.Write($"{DafnyHelpersClass}.ToIntChecked(");
+        var wSize = w.Fork();
+        w.Write(", \"array size exceeds memory limit\")");
+        return wSize;
+      }
+
       var wrs = new List<ConcreteSyntaxTree>();
       if (!mustInitialize || HasSimpleZeroInitializer(elmtType)) {
         TypeName_SplitArrayName(elmtType, wr, tok, out string typeNameSansBrackets, out string brackets);
         wr.Write("new {0}", typeNameSansBrackets);
         string prefix = "[";
         for (var d = 0; d < dimCount; d++) {
-          wr.Write($"{prefix}{DafnyHelpersClass}.ToIntChecked(");
-          var w = wr.Fork();
-          wrs.Add(w);
-          wr.Write(",\"C# array size must not be larger than max 32-bit int\")");
+          wr.Write(prefix);
+          wrs.Add(EmitSizeCheckWrapper(wr));
           prefix = ", ";
         }
         wr.Write("]{0}", brackets);
@@ -2040,8 +2035,7 @@ private List<ConcreteSyntaxTree> EmitNewArray(Type elmtType, IToken tok, int dim
         inParens.Write(DefaultValue(elmtType, inParens, tok, true));
         for (var d = 0; d < dimCount; d++) {
           inParens.Write(", ");
-          var w = inParens.Fork();
-          wrs.Add(w);
+          wrs.Add(EmitSizeCheckWrapper(inParens));
         }
       }
       return wrs;
@@ -2109,9 +2103,10 @@ 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) {
-        string nativeName = null, literalSuffix = null;
-        bool needsCastAfterArithmetic = false;
-        GetNativeInfo(AsNativeType(e.Type).Sel, out nativeName, out literalSuffix, out needsCastAfterArithmetic);
+        GetNativeInfo(AsNativeType(e.Type).Sel, out var nativeName, out var literalSuffix, out var needsCastAfterArithmetic);
+        if (needsCastAfterArithmetic) {
+          wr = wr.Write($"({nativeName})").ForkInParens();
+        }
         wr.Write((BigInteger)e.Value + literalSuffix);
       } else if (e.Value is BigInteger bigInteger) {
         EmitIntegerLiteral(bigInteger, wr);
@@ -2159,9 +2154,8 @@ protected override void EmitStringLiteral(string str, bool isVerbatim, ConcreteS
 
     protected override ConcreteSyntaxTree EmitBitvectorTruncation(BitvectorType bvType, bool surroundByUnchecked, ConcreteSyntaxTree wr) {
       string nativeName = null, literalSuffix = null;
-      bool needsCastAfterArithmetic = false;
       if (bvType.NativeType != null) {
-        GetNativeInfo(bvType.NativeType.Sel, out nativeName, out literalSuffix, out needsCastAfterArithmetic);
+        GetNativeInfo(bvType.NativeType.Sel, out nativeName, out literalSuffix, out var needsCastAfterArithmetic);
       }
 
       // --- Before
@@ -2597,7 +2591,7 @@ protected override ConcreteSyntaxTree EmitArraySelect(List<Expression> indices,
       return w;
     }
 
-    protected override void EmitExprAsInt(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+    protected override void EmitExprAsNativeInt(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
       TrParenExpr("(int)", expr, wr, inLetExprBody, wStmts);
     }
 
@@ -2710,7 +2704,7 @@ private void EmitSeqConstructionExprFromLambda(Expression lengthExpr, BoundVar b
         ixVar, TypeName(indexType, wrLoopBody, body.tok), intIxVar);
       var wrArrName = EmitArrayUpdate(new List<string> { ixVar }, body, wrLoopBody);
       wrArrName.Write(arrVar);
-      wrLoopBody.WriteLine(";");
+      EndStmt(wrLoopBody);
 
       wrLamBody.WriteLine("return {0}<{1}>.FromArray({2});", DafnySeqClass, TypeName(body.Type, wr, body.tok), arrVar);
     }

Source/DafnyCore/Compilers/Compiler-cpp.cs

@@ -1346,8 +1346,9 @@ protected override ConcreteSyntaxTree EmitForStmt(IToken tok, IVariable loopInde
       throw new UnsupportedFeatureException(tok, Feature.ForLoops, "for loops have not yet been implemented");
     }
 
-    protected override ConcreteSyntaxTree CreateForLoop(string indexVar, string bound, ConcreteSyntaxTree wr) {
-      return wr.NewNamedBlock("for (auto {0} = 0; {0} < {1}; {0}++)", indexVar, bound);
+    protected override ConcreteSyntaxTree CreateForLoop(string indexVar, string bound, ConcreteSyntaxTree wr, string start = null) {
+      start = start ?? "0";
+      return wr.NewNamedBlock("for (auto {0} = {2}; {0} < {1}; {0}++)", indexVar, bound, start);
     }
 
     protected override ConcreteSyntaxTree CreateDoublingForLoop(string indexVar, int start, ConcreteSyntaxTree wr) {
@@ -1439,15 +1440,13 @@ protected override void EmitNew(Type type, IToken tok, CallStmt initCall /*?*/,
       }
     }
 
-    protected override void EmitNewArray(Type elmtType, IToken tok, List<Expression> dimensions,
-        bool mustInitialize, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
-      var initValue = mustInitialize ? DefaultValue(elmtType, wr, tok) : null;
+    protected override void EmitNewArray(Type elementType, IToken tok, List<string> dimensions,
+        bool mustInitialize, [CanBeNull] string exampleElement, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+      var initValue = mustInitialize ? DefaultValue(elementType, wr, tok) : null;
       // TODO: Handle initValue
       if (dimensions.Count == 1) {
         // handle the common case of 1-dimensional arrays separately
-        wr.Write("DafnyArray<{0}>::New(", TypeName(elmtType, wr, tok));
-        TrExpr(dimensions[0], wr, false, wStmts);
-        wr.Write(")");
+        wr.Write($"DafnyArray<{TypeName(elementType, wr, tok)}>::New({dimensions[0]})");
       } else {
         throw new UnsupportedFeatureException(tok, Feature.MultiDimensionalArrays);
       }
@@ -1855,11 +1854,7 @@ protected override ConcreteSyntaxTree EmitArraySelect(List<Expression> indices,
       return w;
     }
 
-    protected override string ArrayIndexToInt(string arrayIndex, Type fromType) {
-      return arrayIndex;
-    }
-
-    protected override void EmitExprAsInt(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
+    protected override void EmitExprAsNativeInt(Expression expr, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
       TrParenExpr(expr, wr, inLetExprBody, wStmts);
       if (AsNativeType(expr.Type) == null) {
         wr.Write(".toNumber()");