-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Compiled code has useless duplicate membership test #5465
Labels
area: performance
Performance issues
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Comments
MikaelMayer
added
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
area: performance
Performance issues
labels
May 20, 2024
MikaelMayer
added a commit
that referenced
this issue
Jun 8, 2024
### Description Let's consider the following code: ```dafny newtype UX = x: int | 129 <= x < 256 method Main() { var u8toInt := map[1 as u8 := 1, 2 as u8 := 2]; var IntToU8 := map k <- u8toInt :: u8toInt[k] := k; } ``` in every backend, for `IntToU8 `it is generating code lilke ``` c = MapCollectionBuilder() for k in u8toInt if k is u8 { if u8toInt contains k { col.Add(u8toInt[k], k) } } } k.build() ``` I already filed an issue that the ["contains" test is redundant](#5465) when we are already iterating over the collection. But here there is another test that is redundant: The membership test to the newtype. Indeed, contrary to subset types which can be erased, newtype conversions must be explicit. So we cannot iterate over a newtype different than the newtype obtain like we do for subset types. Moreover, the test of being a newtype involves a conversion from a U8 (how the newtype is encoded) to a DafnyInt because otherwise we would not be able to compare it with the number "256" which is out of the range. So this test is not only redundant, it actually adds computation that is not necessary. ### How has this been tested? All existing tests should pass. <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>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Labels
area: performance
Performance issues
kind: enhancement
Enhancements, feature requests, etc. These are NOT bugs, but ways we can improve Dafny
part: code-generation
Support for transpiling Dafny to another language. If relevant, add a `lang:` tag
Consider the following code:
In all compilers, the compilation of the forall expression is done in two ways:
However, by construction, in many cases the bounded pool arise from one of the range check, so the range check is useless.
For example, let's consider the C# case (but all other languages have the same issue)
C#
Performance slowdown:
!((Dafny.Sequence<BigInteger>.Concat(_0_a, _0_a)).Contains(_1_x))
is always false by construction.I'm reporting this because I'm working on the Dafny-to-Rust code generator, and since performance of the generated code is a requirement, this one thing is something we'll need to cover.
The text was updated successfully, but these errors were encountered: