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()");