Use native byte/char arrays in Go

[RustanLeino]

This PR does three things to improve performance of Go code that uses arrays:

• For nonempty arrays where the target representation of elements uses uint8 or rune, the underlying Array uses a []uint8 or []rune array, respectively, instead of the default []any.
• For 1-dimensional arrays, the index is passed directly to the ArrayGet/ArraySet method in the Dafny runtime, rather than using a var-args version of those methods.
• When the static type of the array operations reveals that the underlying representation is uint8 or rune, then special versions of ArrayGet/ArraySet are called where the argument/return is a uint8 or rune, respectively, rather than the default versions, which use an any (that is, interface{}) as the argument/return.

Unlike the current compilation to Java, which introduces type descriptors for all types in order to specialize arrays, this PR uses existing type descriptors or the initialization elements provided by the program. The one case where the type cannot be recovered for specialization is for 0-length arrays, which this PR represents with an underlying nil array. It seems the design in this PR can be adapted to Java or JavaScript as well.

The performance improvements are as follows. The program run is included below, and the Go measurements were repeated 6 times (each varying less than 0.2s from the numbers shown here).

target features	time
C#	31.4s
Go with specialized arrays and no boxing across Set/Get	27.4s
Go with specialized arrays, but still using boxes across Set/Get	31.8s
Go with arrays of any	103.6s
Go with arrays of any and using var-args even for 1-dim arrays	179.1s

newtype byte = x | 0 <= x < 256
newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000

method MM<X>(x: X) returns (r: X) { r := x; }

method Main() {
  for i := 0 to 10_000 {
    var a := GenerateArray();
    a := CopyArray(a);
    var s := SumArray(a);
    expect s == 0;
  }
  print "done\n";
}

method GenerateArray() returns (b: array<byte>)
  ensures b.Length == 256_000
{
  b := new byte[256_000];
  for i: int32 := 0 to 256_000 {
    b[i] := (i % 256) as byte;
  }
}

method CopyArray(a: array<byte>) returns (b: array<byte>)
  requires a.Length == 256_000
  ensures b.Length == 256_000
{
  b := new byte[256_000];
  for i: int32 := 0 to 256_000 {
    b[i] := a[i];
  }
}

method SumArray(a: array<byte>) returns (sb: byte)
  requires a.Length == 256_000
{
  var s: int32 := 0;
  for i: int32 := 0 to 256_000
    invariant 0 <= s < 256
  {
    s := s + a[i] as int32;
    if 256 <= s {
      s := s - 256;
    }
  }
  sb := s as byte;
}

Other fixes along the way

As part of writing tests for the new functionality, I detected and fixed various other infelicities as well:

• fix: In Java, cast to non-box type after let
• fix: In JavaScript, compare arrays by comparing their references, not their elements (issue Array comparison causes JavaScript run-time crash #3207)
• fix: In C#, add some necessary casts
• In Go, improved implementation of array comparisons
• In Go, fixes array comparisons (to be reference equality, not equality of elements) (Go incorrectly compares array values by contents, instead of by reference #2708)
• fix: In Java, fix enumerations of long Java values (which previously ended up truncating numbers to ints)
• fix: In Java, don't confuse a Dafny-defined type Long with Java's java.lang.Long (and similar for other integer types) (reported as Emitted Java converts long to int and loses precision #3204)
• fix: In Python, don't share inner arrays, which was previously done when arrays have 3 or more dimensions
• Across the target languages, pass BigInteger as array sizes and use native integers for array indices
• Pretty printing: Elide the array size in new only when the input program does (this uses AutoGeneratedToken, as in other places)
• When there are several IntBoundedPools, try a little harder to pick the best bounds. Alas, there are still simple cases where the target code ends up enumerating all 32-bit integers, for example. To improve the target code further, we need to make use of the partial-evaluation of expressions, which exists elsewhere in the Dafny implementation, and/or make use of run-time Min and Max routines.

Fixes #3204
Fixes #2708
Fixes #3207

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[robin-aws]

Just to update: I've been working on fixing the remaining issues with the new Test/unicodechars/comp/Arrays.dfy test case - I have them mostly fixed on a branch but there's still some non-trivial work to coerce Java functions correctly in the same style Go already does.

[robin-aws]

The Java fixes are rather involved so I'm going to move them to a separate PR, and just merge this one with Java disabled in the new Test/unicodechars/comp/Arrays.dfy test case for now.

@fabiomadge would you mind giving my two commits (6835539 and bcd2f04) a sanity check before I merge this? Rustan asked me to add whatever was necessary to complete this while he was on vacation, but I don't want to use that to sneak code in without review. :)

[fabiomadge]

Did you try doing this without circumventing the TypeHelperName?

[robin-aws]

I did at first and found the code generation was a lot messier.

[fabiomadge]

Are you sure that this changes the semantics?

[robin-aws]

Yup. Before Seq("a", isStr=None) + Seq("b", isStr=None) would become the same as Seq("ab", isStr=False), which would still go through the inference and decide it was a string, which we don't want.

[fabiomadge]

>>> (None and None) == None
True
>>> (None and None) == False
False

[robin-aws]

Ah you're right, self.isStr = None is all that needed to change. I added this at the same time and never tested it without. :) Thanks!

[fabiomadge]

I was certain to have made this remark elsewhere, but can't find it, so: Can you overload + and - instead?

[robin-aws]

Ah true, I can do that. For the record I don't care much about the usability of CodePoint though, since I only expect compiled Dafny code to reference it.

[robin-aws]

It did end up simplifying the code generation logic a little though, which I DO care about :) , so thanks!

[fabiomadge]

The Python changes look ok to me.