fix: Don't use "/" and "%" for non-native int-based newtypes #2416
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
* `Source/Dafny/Compilers/Compiler-Csharp.cs` (`CompileBinOp`): Factor out the code to check for native division. * `Source/Dafny/Compilers/Compiler-java.cs` (`CompileBinOp`): Same. * `Source/Dafny/Compilers/SinglePassCompiler.cs`: (`NeedsEuclideanDivision`): New function; use `IsNumericBased` instead of `IsIntegerType` to properly handle `newtype`s. Closes #2367.
RustanLeino
requested changes
Jul 22, 2022
Comment on lines
+435
to
+438
| print var n: NewType := (-4) / (-2); n, "\n"; | ||
| print var n: NewType := ( 4) / (-2); n, "\n"; | ||
| print var n: NewType := (-4) / ( 2); n, "\n"; | ||
| print var n: NewType := ( 4) / ( 2); n, "\n"; |
There was a problem hiding this comment.
Note, these compilation would have been correct even before this PR, because the modulus is 0. (The new file git-issues-2367.dfy covers ones that failed, but only for C# and Java.) Here are some additional tests I suggest you add in this compilation test file:
// Some runtimes (like the one for C#) has three implementations
// of Euclidean div/mod: one for `int`, one for `long`, and one
// for `BigInteger`.
const TWO_15: int := 0x0_8000
const TWO_63: int := 0x0_8000_0000_0000_0000
const TWO_127: int := 0x0_8000_0000_0000_0000_0000_0000_0000_0000
// I0, I1, I2, and I3 use the BigInteger versions
type I0 = int
newtype I1 = int
newtype I2 = x: int | true
newtype I3 = x | -TWO_127 <= x < TWO_127
// I4 uses the int version
newtype I4 = x | -TWO_15 <= x < TWO_15
// I5 uses the long version
newtype I5 = x | -TWO_63 <= x < TWO_63
method M0() {
var neg: I0, pos: I0;
neg, pos := -6, 6;
// div
var a := neg / (-4); assert a == 2;
var b := pos / (-4); assert b == -1;
var c := neg / ( 4); assert c == -2;
var d := pos / ( 4); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (-4) / (-2); assert a == 2;
b := ( 4) / (-2); assert b == -2;
c := (-4) / ( 2); assert c == -2;
d := ( 4) / ( 2); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := 101 / (-3); assert a == -33;
b := 100 / (-3); assert b == -33;
c := 99 / (-3); assert c == -33;
d := 98 / (-3); assert d == -32;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) / 3; assert a == -34;
b := (-100) / 3; assert b == -34;
c := ( -99) / 3; assert c == -33;
d := ( -98) / 3; assert d == -33;
print a, " ", b, " ", c, " ", d, " ";
// mod
a := (-101) % (-3); assert a == 1;
b := (-100) % (-3); assert b == 2;
c := ( -99) % (-3); assert c == 0;
d := ( -98) % (-3); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := ( 101) % (-3); assert a == 2;
b := ( 100) % (-3); assert b == 1;
c := ( 99) % (-3); assert c == 0;
d := ( 98) % (-3); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) % 3; assert a == 1;
b := (-100) % 3; assert b == 2;
c := ( -99) % 3; assert c == 0;
d := ( -98) % 3; assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (101) % 3; assert a == 2;
b := (100) % 3; assert b == 1;
c := ( 99) % 3; assert c == 0;
d := ( 98) % 3; assert d == 2;
print a, " ", b, " ", c, " ", d, "\n";
}
method M1() {
var neg: I1, pos: I1;
neg, pos := -6, 6;
// div
var a := neg / (-4); assert a == 2;
var b := pos / (-4); assert b == -1;
var c := neg / ( 4); assert c == -2;
var d := pos / ( 4); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (-4) / (-2); assert a == 2;
b := ( 4) / (-2); assert b == -2;
c := (-4) / ( 2); assert c == -2;
d := ( 4) / ( 2); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := 101 / (-3); assert a == -33;
b := 100 / (-3); assert b == -33;
c := 99 / (-3); assert c == -33;
d := 98 / (-3); assert d == -32;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) / 3; assert a == -34;
b := (-100) / 3; assert b == -34;
c := ( -99) / 3; assert c == -33;
d := ( -98) / 3; assert d == -33;
print a, " ", b, " ", c, " ", d, " ";
// mod
a := (-101) % (-3); assert a == 1;
b := (-100) % (-3); assert b == 2;
c := ( -99) % (-3); assert c == 0;
d := ( -98) % (-3); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := ( 101) % (-3); assert a == 2;
b := ( 100) % (-3); assert b == 1;
c := ( 99) % (-3); assert c == 0;
d := ( 98) % (-3); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) % 3; assert a == 1;
b := (-100) % 3; assert b == 2;
c := ( -99) % 3; assert c == 0;
d := ( -98) % 3; assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (101) % 3; assert a == 2;
b := (100) % 3; assert b == 1;
c := ( 99) % 3; assert c == 0;
d := ( 98) % 3; assert d == 2;
print a, " ", b, " ", c, " ", d, "\n";
}
method M2() {
var neg: I2, pos: I2;
neg, pos := -6, 6;
// div
var a := neg / (-4); assert a == 2;
var b := pos / (-4); assert b == -1;
var c := neg / ( 4); assert c == -2;
var d := pos / ( 4); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (-4) / (-2); assert a == 2;
b := ( 4) / (-2); assert b == -2;
c := (-4) / ( 2); assert c == -2;
d := ( 4) / ( 2); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := 101 / (-3); assert a == -33;
b := 100 / (-3); assert b == -33;
c := 99 / (-3); assert c == -33;
d := 98 / (-3); assert d == -32;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) / 3; assert a == -34;
b := (-100) / 3; assert b == -34;
c := ( -99) / 3; assert c == -33;
d := ( -98) / 3; assert d == -33;
print a, " ", b, " ", c, " ", d, " ";
// mod
a := (-101) % (-3); assert a == 1;
b := (-100) % (-3); assert b == 2;
c := ( -99) % (-3); assert c == 0;
d := ( -98) % (-3); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := ( 101) % (-3); assert a == 2;
b := ( 100) % (-3); assert b == 1;
c := ( 99) % (-3); assert c == 0;
d := ( 98) % (-3); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) % 3; assert a == 1;
b := (-100) % 3; assert b == 2;
c := ( -99) % 3; assert c == 0;
d := ( -98) % 3; assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (101) % 3; assert a == 2;
b := (100) % 3; assert b == 1;
c := ( 99) % 3; assert c == 0;
d := ( 98) % 3; assert d == 2;
print a, " ", b, " ", c, " ", d, "\n";
}
method M3() {
var neg: I3, pos: I3;
neg, pos := -6, 6;
// div
var a := neg / (-4); assert a == 2;
var b := pos / (-4); assert b == -1;
var c := neg / ( 4); assert c == -2;
var d := pos / ( 4); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (-4) / (-2); assert a == 2;
b := ( 4) / (-2); assert b == -2;
c := (-4) / ( 2); assert c == -2;
d := ( 4) / ( 2); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := 101 / (-3); assert a == -33;
b := 100 / (-3); assert b == -33;
c := 99 / (-3); assert c == -33;
d := 98 / (-3); assert d == -32;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) / 3; assert a == -34;
b := (-100) / 3; assert b == -34;
c := ( -99) / 3; assert c == -33;
d := ( -98) / 3; assert d == -33;
print a, " ", b, " ", c, " ", d, " ";
// mod
a := (-101) % (-3); assert a == 1;
b := (-100) % (-3); assert b == 2;
c := ( -99) % (-3); assert c == 0;
d := ( -98) % (-3); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := ( 101) % (-3); assert a == 2;
b := ( 100) % (-3); assert b == 1;
c := ( 99) % (-3); assert c == 0;
d := ( 98) % (-3); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) % 3; assert a == 1;
b := (-100) % 3; assert b == 2;
c := ( -99) % 3; assert c == 0;
d := ( -98) % 3; assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (101) % 3; assert a == 2;
b := (100) % 3; assert b == 1;
c := ( 99) % 3; assert c == 0;
d := ( 98) % 3; assert d == 2;
print a, " ", b, " ", c, " ", d, "\n";
}
method M4() {
var neg: I4, pos: I4;
neg, pos := -6, 6;
// div
var a := neg / (-4); assert a == 2;
var b := pos / (-4); assert b == -1;
var c := neg / ( 4); assert c == -2;
var d := pos / ( 4); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (-4) / (-2); assert a == 2;
b := ( 4) / (-2); assert b == -2;
c := (-4) / ( 2); assert c == -2;
d := ( 4) / ( 2); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := 101 / (-3); assert a == -33;
b := 100 / (-3); assert b == -33;
c := 99 / (-3); assert c == -33;
d := 98 / (-3); assert d == -32;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) / 3; assert a == -34;
b := (-100) / 3; assert b == -34;
c := ( -99) / 3; assert c == -33;
d := ( -98) / 3; assert d == -33;
print a, " ", b, " ", c, " ", d, " ";
// mod
a := (-101) % (-3); assert a == 1;
b := (-100) % (-3); assert b == 2;
c := ( -99) % (-3); assert c == 0;
d := ( -98) % (-3); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := ( 101) % (-3); assert a == 2;
b := ( 100) % (-3); assert b == 1;
c := ( 99) % (-3); assert c == 0;
d := ( 98) % (-3); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) % 3; assert a == 1;
b := (-100) % 3; assert b == 2;
c := ( -99) % 3; assert c == 0;
d := ( -98) % 3; assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (101) % 3; assert a == 2;
b := (100) % 3; assert b == 1;
c := ( 99) % 3; assert c == 0;
d := ( 98) % 3; assert d == 2;
print a, " ", b, " ", c, " ", d, "\n";
}
method M5() {
var neg: I5, pos: I5;
neg, pos := -6, 6;
// div
var a := neg / (-4); assert a == 2;
var b := pos / (-4); assert b == -1;
var c := neg / ( 4); assert c == -2;
var d := pos / ( 4); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (-4) / (-2); assert a == 2;
b := ( 4) / (-2); assert b == -2;
c := (-4) / ( 2); assert c == -2;
d := ( 4) / ( 2); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := 101 / (-3); assert a == -33;
b := 100 / (-3); assert b == -33;
c := 99 / (-3); assert c == -33;
d := 98 / (-3); assert d == -32;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) / 3; assert a == -34;
b := (-100) / 3; assert b == -34;
c := ( -99) / 3; assert c == -33;
d := ( -98) / 3; assert d == -33;
print a, " ", b, " ", c, " ", d, " ";
// mod
a := (-101) % (-3); assert a == 1;
b := (-100) % (-3); assert b == 2;
c := ( -99) % (-3); assert c == 0;
d := ( -98) % (-3); assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := ( 101) % (-3); assert a == 2;
b := ( 100) % (-3); assert b == 1;
c := ( 99) % (-3); assert c == 0;
d := ( 98) % (-3); assert d == 2;
print a, " ", b, " ", c, " ", d, " ";
a := (-101) % 3; assert a == 1;
b := (-100) % 3; assert b == 2;
c := ( -99) % 3; assert c == 0;
d := ( -98) % 3; assert d == 1;
print a, " ", b, " ", c, " ", d, " ";
a := (101) % 3; assert a == 2;
b := (100) % 3; assert b == 1;
c := ( 99) % 3; assert c == 0;
d := ( 98) % 3; assert d == 2;
print a, " ", b, " ", c, " ", d, "\n";
}
method Main() {
// This is expected to print six lines of:
// 2 -1 -2 1 2 -2 -2 2 -33 -33 -33 -32 -34 -34 -33 -33 1 2 0 1 2 1 0 2 1 2 0 1 2 1 0 2
M0();
M1();
M2();
M3();
M4();
M5();
}
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Source/Dafny/Compilers/Compiler-Csharp.cs(
CompileBinOp): Factor out the code to check for native division.Source/Dafny/Compilers/Compiler-java.cs(CompileBinOp): Same.Source/Dafny/Compilers/SinglePassCompiler.cs:(
NeedsEuclideanDivision): New function; useIsNumericBasedinstead ofIsIntegerTypeto properly handlenewtypes.Closes #2367.