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.

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

JavaScript compiler: incorrect bignum comparison #2672

Closed
sorawee opened this issue Sep 1, 2022 · 1 comment · Fixed by #2716
Closed

JavaScript compiler: incorrect bignum comparison #2672

sorawee opened this issue Sep 1, 2022 · 1 comment · Fixed by #2716
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 lang: js Dafny's JavaScript transpiler and its runtime

Comments

@sorawee
Copy link
Contributor

sorawee commented Sep 1, 2022

Consider:

method Main() {
  print 24 as bv16 <= 1507 as bv16, "\n";
  assert 24 as bv16 <= 1507 as bv16;
}

This should print "true", which is what Go, Java, C#, and Python output. However, JavaScript prints "false".

@cpitclaudel cpitclaudel added logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) kind: bug Crashes, unsoundness, incorrect output, etc. If possible, add a `part:` label lang: js Dafny's JavaScript transpiler and its runtime labels Sep 1, 2022
@sorawee
Copy link
Contributor Author

sorawee commented Sep 1, 2022

Turns out this is about the comparison operator for bigintegers, not bitwise and. It should use .isLessThanOrEqualTo rather than <=.

@sorawee sorawee changed the title JavaScript compiler: incorrect bitwise and JavaScript compiler: incorrect bignum comparison Sep 1, 2022
@cpitclaudel cpitclaudel added during 4: bad execution of correct program A bug in the Dafny compiler that causes a correct Dafny program to execute incorrectly and removed logic An inconsistency in Dafny's logic (e.g. in the Boogie prelude) labels Sep 2, 2022
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
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 lang: js Dafny's JavaScript transpiler and its runtime
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants