Skip to content
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.

Sign up for GitHub

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

fix: Use the right >/</>=/<= comparison operators for bitvectors in JS #2716

Merged
merged 4 commits into from
Sep 20, 2022
Merged

fix: Use the right >/</>=/<= comparison operators for bitvectors in JS #2716

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
447f888
fix: Use the right >/</>=/<= comparison operators for bitvectors in JS
cpitclaudel Sep 8, 2022
0421f12
fix: Use the right comparison operators for ordinals in Go
cpitclaudel Sep 20, 2022
e929451
Merge remote-tracking branch 'origin/master' into cpitclaudel_fix-2672
cpitclaudel Sep 20, 2022
be66cdf
Work around a C++ compiler bug (#2773)
cpitclaudel Sep 20, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions RELEASE_NOTES.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@
- feat: Generate warning when 'old' has no effect (https://github.com/dafny-lang/dafny/pull/2610)
- fix: Missing related position in failing precondition (https://github.com/dafny-lang/dafny/pull/2658)
- fix: No more IDE crashing on the elephant operator (https://github.com/dafny-lang/dafny/pull/2668)
- fix: Use the right comparison operators for bitvectors in Javascript (https://github.com/dafny-lang/dafny/pull/2716)
- fix: Retain non-method-body block statements when cloning abstract signatures (https://github.com/dafny-lang/dafny/pull/2731)
- fix: Correctly substitute variables introduced by a binding guard (https://github.com/dafny-lang/dafny/pull/2745)

Expand Down
2 changes: 1 addition & 1 deletion Source/DafnyCore/Compilers/Compiler-go.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2905,7 +2905,7 @@ private bool IsDirectlyComparable(Type t) {
}

private bool IsOrderedByCmp(Type t) {
return t.IsIntegerType || t.IsRealType || (t.IsBitVectorType && t.AsBitVectorType.NativeType == null) || (t.AsNewtype is NewtypeDecl nt && nt.NativeType == null);
return t.IsIntegerType || t.IsRealType || t.IsBigOrdinalType || (t.IsBitVectorType && t.AsBitVectorType.NativeType == null) || (t.AsNewtype is NewtypeDecl nt && nt.NativeType == null);
}

private bool IsComparedByEquals(Type t) {
Expand Down
40 changes: 30 additions & 10 deletions Source/DafnyCore/Compilers/Compiler-js.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1923,6 +1923,18 @@ bool IsDirectlyComparable(Type t) {
return t.IsBoolType || t.IsCharType || AsNativeType(t) != null || t.IsRefType;
}

bool IsRepresentedAsBigNumber(Type t) {
if (AsNativeType(t) != null) {
return false;
} else if (t.AsBitVectorType is { } bvt) {
return bvt.NativeType == null;
} else {
return t.IsNumericBased(Type.NumericPersuasion.Int)
|| t.IsBitVectorType
|| t.IsBigOrdinalType;
}
}

protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
Expression e0, Expression e1, IToken tok, Type resultType,
out string opString,
Expand Down Expand Up @@ -2017,38 +2029,46 @@ protected override void CompileBinOp(BinaryExpr.ResolvedOpcode op,
}

case BinaryExpr.ResolvedOpcode.Lt:
if (e0.Type.IsNumericBased() && AsNativeType(e0.Type) == null) {
if (AsNativeType(e0.Type) != null) {
opString = "<";
} else if (IsRepresentedAsBigNumber(e0.Type) || e0.Type.IsNumericBased(Type.NumericPersuasion.Real)) {
callString = "isLessThan";
} else {
opString = "<";
Contract.Assert(false); throw new cce.UnreachableException();
}
break;
case BinaryExpr.ResolvedOpcode.Le:
if (e0.Type.IsNumericBased(Type.NumericPersuasion.Int) && AsNativeType(e0.Type) == null) {
if (AsNativeType(e0.Type) != null) {
opString = "<=";
} else if (IsRepresentedAsBigNumber(e0.Type)) {
callString = "isLessThanOrEqualTo";
} else if (e0.Type.IsNumericBased(Type.NumericPersuasion.Real) && AsNativeType(e0.Type) == null) {
} else if (e0.Type.IsNumericBased(Type.NumericPersuasion.Real)) {
callString = "isAtMost";
} else {
opString = "<=";
Contract.Assert(false); throw new cce.UnreachableException();
}
break;
case BinaryExpr.ResolvedOpcode.Ge:
if (e0.Type.IsNumericBased(Type.NumericPersuasion.Int) && AsNativeType(e0.Type) == null) {
if (AsNativeType(e0.Type) != null) {
opString = ">=";
} else if (IsRepresentedAsBigNumber(e0.Type)) {
callString = "isLessThanOrEqualTo";
reverseArguments = true;
} else if (e0.Type.IsNumericBased(Type.NumericPersuasion.Real) && AsNativeType(e0.Type) == null) {
} else if (e0.Type.IsNumericBased(Type.NumericPersuasion.Real)) {
callString = "isAtMost";
reverseArguments = true;
} else {
opString = ">=";
Contract.Assert(false); throw new cce.UnreachableException();
}
break;
case BinaryExpr.ResolvedOpcode.Gt:
if (e0.Type.IsNumericBased() && AsNativeType(e0.Type) == null) {
if (AsNativeType(e0.Type) != null) {
opString = ">";
} else if (IsRepresentedAsBigNumber(e0.Type) || e0.Type.IsNumericBased(Type.NumericPersuasion.Real)) {
callString = "isLessThan";
reverseArguments = true;
} else {
opString = ">";
Contract.Assert(false); throw new cce.UnreachableException();
}
break;
case BinaryExpr.ResolvedOpcode.LeftShift:
Expand Down
100 changes: 100 additions & 0 deletions Test/git-issues/git-issue-2672.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:cs "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:js "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:go "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:java "%s" >> "%t"
// RUN: %dafny /noVerify /compile:4 /compileTarget:py "%s" >> "%t"
// RUN: %diff "%s.expect" "%t"
Comment on lines +1 to +7
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you use %testDafnyForEachCompiler %s instead? :)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you remind me how to generate the output with that flag?

Copy link
Member

@robin-aws robin-aws Sep 8, 2022 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It should just be a single copy of the program's output, not including the "Dafny program verifier ..." line. So in this case just:

true true true true true true true true true
false false false false false false false false false
false false false false false false false false false
true true true true true true true true true
true true true true true true true true true
false false false false false false false false false
true true true
false false false

It occurs to me that having a flag on the TestDafny tool to generate the expect file would be super handy, let me know see if I can add that. :)

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! Unfortunately it doesn't correctly detect unsupported features, so it fails on this example; I've reported the error at #2718 , and I'm currently preparing a PR. We can update this test file once that PR is merged, but I don't think we need to block on it.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure we should add the output generation to TestDafny, btw, since it's needed for all lit tests (not just for for-each-compiler). Maybe we could update runTest.py to recognize that case in addition to the usual diff-based ones.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think both makes sense. Since LIT tests can be more complicated than just piping to a single *.expect file, runTest.py can't realistically generate the "expected output" for an arbitrary LIT test (nor would this make sense as a feature on the xUnit-based LIT test runner either). I say we update it to recognize %testDafnyForEachCompiler but have it delegate generating the output file to TestDafny.

Part of the reason I'd prefer that is I'd also find it useful to install testdafny as a local dotnet tool and run it in this mode on arbitrary source files as part of development.


newtype sreal = r: real | r > -4 as real
newtype sint = r: int | r > -4 as int
newtype ssreal = r: sreal | r > -3 as sreal
newtype ssint = r: sint | r > -3 as sint

method Print(b: bool, end: string)
// Print boolean `b` as `true` or `false`, then print `end`. This is needed
// by C++ due to BUG(https://github.com/dafny-lang/dafny/issues/2773).
{
if b {
print "true";
} else {
print "false";
}
print end;
}

method Main() {
Print(24 as real <= 1507 as real, " ");
Print(24 as sreal <= 1507 as sreal, " ");
Print(24 as ssreal <= 1507 as ssreal, " ");
Print(24 as int <= 1507 as int, " ");
Print(24 as sint <= 1507 as sint, " ");
Print(24 as ssint <= 1507 as ssint, " ");
Print(24 as bv16 <= 1507 as bv16, " ");
Print(24 as bv232 <= 1507 as bv232, " ");
Print(24 as char <= 1507 as char, " ");
Print(24 as ORDINAL <= 1507 as ORDINAL, "\n");

Print(24 as real == 1507 as real, " ");
Print(24 as sreal == 1507 as sreal, " ");
Print(24 as ssreal == 1507 as ssreal, " ");
Print(24 as int == 1507 as int, " ");
Print(24 as sint == 1507 as sint, " ");
Print(24 as ssint == 1507 as ssint, " ");
Print(24 as bv16 == 1507 as bv16, " ");
Print(24 as bv232 == 1507 as bv232, " ");
Print(24 as char == 1507 as char, " ");
Print(24 as ORDINAL == 1507 as ORDINAL, "\n");

Print(24 as real >= 1507 as real, " ");
Print(24 as sreal >= 1507 as sreal, " ");
Print(24 as ssreal >= 1507 as ssreal, " ");
Print(24 as int >= 1507 as int, " ");
Print(24 as sint >= 1507 as sint, " ");
Print(24 as ssint >= 1507 as ssint, " ");
Print(24 as bv16 >= 1507 as bv16, " ");
Print(24 as bv232 >= 1507 as bv232, " ");
Print(24 as char >= 1507 as char, " ");
Print(24 as ORDINAL >= 1507 as ORDINAL, "\n");

Print(24 as real < 1507 as real, " ");
Print(24 as sreal < 1507 as sreal, " ");
Print(24 as ssreal < 1507 as ssreal, " ");
Print(24 as int < 1507 as int, " ");
Print(24 as sint < 1507 as sint, " ");
Print(24 as ssint < 1507 as ssint, " ");
Print(24 as bv16 < 1507 as bv16, " ");
Print(24 as bv232 < 1507 as bv232, " ");
Print(24 as char < 1507 as char, " ");
Print(24 as ORDINAL < 1507 as ORDINAL, "\n");

Print(24 as real != 1507 as real, " ");
Print(24 as sreal != 1507 as sreal, " ");
Print(24 as ssreal != 1507 as ssreal, " ");
Print(24 as int != 1507 as int, " ");
Print(24 as sint != 1507 as sint, " ");
Print(24 as ssint != 1507 as ssint, " ");
Print(24 as bv16 != 1507 as bv16, " ");
Print(24 as bv232 != 1507 as bv232, " ");
Print(24 as char != 1507 as char, " ");
Print(24 as ORDINAL != 1507 as ORDINAL, "\n");

Print(24 as real > 1507 as real, " ");
Print(24 as sreal > 1507 as sreal, " ");
Print(24 as ssreal > 1507 as ssreal, " ");
Print(24 as int > 1507 as int, " ");
Print(24 as sint > 1507 as sint, " ");
Print(24 as ssint > 1507 as ssint, " ");
Print(24 as bv16 > 1507 as bv16, " ");
Print(24 as bv232 > 1507 as bv232, " ");
Print(24 as char > 1507 as char, " ");
Print(24 as ORDINAL > 1507 as ORDINAL, "\n");

Print(0 as bv0 <= 0 as bv0, " ");
Print(0 as bv0 == 0 as bv0, " ");
Print(0 as bv0 >= 0 as bv0, "\n");

Print(0 as bv0 < 0 as bv0, " ");
Print(0 as bv0 != 0 as bv0, " ");
Print(0 as bv0 > 0 as bv0, "\n");
}
52 changes: 52 additions & 0 deletions Test/git-issues/git-issue-2672.dfy.expect
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@

Dafny program verifier finished with 5 verified, 0 errors

Dafny program verifier did not attempt verification
true true true true true true true true true true
false false false false false false false false false false
false false false false false false false false false false
true true true true true true true true true true
true true true true true true true true true true
false false false false false false false false false false
true true true
false false false

Dafny program verifier did not attempt verification
true true true true true true true true true true
false false false false false false false false false false
false false false false false false false false false false
true true true true true true true true true true
true true true true true true true true true true
false false false false false false false false false false
true true true
false false false

Dafny program verifier did not attempt verification
true true true true true true true true true true
false false false false false false false false false false
false false false false false false false false false false
true true true true true true true true true true
true true true true true true true true true true
false false false false false false false false false false
true true true
false false false

Dafny program verifier did not attempt verification
true true true true true true true true true true
false false false false false false false false false false
false false false false false false false false false false
true true true true true true true true true true
true true true true true true true true true true
false false false false false false false false false false
true true true
false false false

Dafny program verifier did not attempt verification
true true true true true true true true true true
false false false false false false false false false false
false false false false false false false false false false
true true true true true true true true true true
true true true true true true true true true true
false false false false false false false false false false
true true true
false false false