Emitted Java converts long to int and loses precision #3204
Assignees
Labels
during 4: bad execution of correct program
A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly
kind: bug
Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label
Comments
RustanLeino
added
kind: bug
robin-aws
added a commit
that referenced
this issue
Jan 25, 2023
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 |
``` dafny
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 #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) (#2708)
* fix: In Java, fix enumerations of `long` Java values (which previously
ended up truncating numbers to `int`s)
* 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
#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 `IntBoundedPool`s, 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
<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>
Co-authored-by: Fabio Madge <fabio@madge.me>
Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
atomb
added a commit
to atomb/dafny
that referenced
this issue
Feb 1, 2023
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 |
``` dafny
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 dafny-lang#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) (dafny-lang#2708)
* fix: In Java, fix enumerations of `long` Java values (which previously
ended up truncating numbers to `int`s)
* 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
dafny-lang#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 `IntBoundedPool`s, 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 dafny-lang#3204
Fixes dafny-lang#2708
Fixes dafny-lang#3207
<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>
Co-authored-by: Fabio Madge <fabio@madge.me>
Co-authored-by: Robin Salkeld <salkeldr@amazon.com>
Co-authored-by: Aaron Tomb <aarotomb@amazon.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Dafny version
3.9.1
Code to produce this issue
Command to run and resulting output
What happened?
The Java compiler emits code that converts each candidate
PrettyLongnumber to a 32-bit int. This means that that none of them falls into the range mentioned by the set. Thus, it erroneously computed the empty set.What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: