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

Are ByteArray.toInt64LE! and ByteArray.toInt64BE! reversed? #3657

Closed
1 task done
gleachkr opened this issue Mar 12, 2024 · 1 comment · Fixed by #3660
Closed
1 task done

Are ByteArray.toInt64LE! and ByteArray.toInt64BE! reversed? #3657

gleachkr opened this issue Mar 12, 2024 · 1 comment · Fixed by #3660
Labels
bug Something isn't working

Comments

@gleachkr
Copy link

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Check that your issue is not already filed.
    • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

I suspect that the little-endian and big-endian ByteArray functions have their names backwards. The little-endian function seems to convert a ByteArray to a UInt64 by taking the leftmost byte as most significant, and vice-versa.

Steps to Reproduce

It should be easy to check, but here's a minimal reproduction, showing how the current functions seem to get things wrong when reading an ELF binary. Requires a 64 bit ELF binary - I used /bin/true.

def test: IO Unit := do
  let bytes ← IO.FS.readBinFile ↑"/bin/true"
  if h : bytes.size > 256 then do
    IO.println bytes[0x5] -- e_ident[EI_DATA], 1 means little endian, 2 means bigendian
    let ph_off := bytes.extract 0x20 0x28 --program header offset in a 64 bit binary, should be 64.
    IO.println ph_off
    IO.println ph_off.toUInt64LE!
    IO.println ph_off.toUInt64BE!

#eval test 

Expected behavior:

I would expect the code above to show toUInt64LE! returning 64 for bytes [0x20,0x28) on a little-endian binary, and toUInt64BE! to give a 64 for that range on a big-endian binary.

Actual behavior:

Seems to be the reverse

Versions

4.7.0-rc1
Ubuntu 22.04.1

Additional Information

Impact

@gleachkr gleachkr added the bug Something isn't working label Mar 12, 2024
@gleachkr gleachkr changed the title Are ByteArray.toInt64LE! and ByteArray.toInt64LE! reversed? Are ByteArray.toInt64LE! and ByteArray.toInt64BE! reversed? Mar 12, 2024
@digama0
Copy link
Collaborator

digama0 commented Mar 12, 2024

Here's a simpler reproduction:

#eval (ByteArray.mk #[1,0,0,0,0,0,0,0]).toUInt64BE! -- 1
#eval (ByteArray.mk #[1,0,0,0,0,0,0,0]).toUInt64LE! -- 72057594037927936

A little endian array should have the least significant byte at index [0], meaning that #[1,0,0,0,0,0,0,0] encodes 1 in little endian.

digama0 added a commit to digama0/lean4 that referenced this issue Mar 12, 2024
github-merge-queue bot pushed a commit that referenced this issue Mar 28, 2024
fixes #3657

These functions are mostly not used by lean itself, but it does affect
two occurrences of `ByteArray.toUInt64LE! <$> IO.getRandomBytes 8` which
I left as is instead of switching them to use `toUInt64BE!` to preserve
behavior; but they are random bytes anyway seeded by the OS so it's
unlikely any use of them depending on particular values was sound to
begin with.

Co-authored-by: Scott Morrison <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants