Skip to content

Fix build on s390x; related to #166 - #173

Merged
msprotz merged 2 commits into
FStarLang:masterfrom
ueno:wip/dueno/uint128-s390x
Apr 23, 2020
Merged

Fix build on s390x; related to #166#173
msprotz merged 2 commits into
FStarLang:masterfrom
ueno:wip/dueno/uint128-s390x

Conversation

@ueno

@ueno ueno commented Mar 4, 2020

Copy link
Copy Markdown
Contributor

@msftclas

msftclas commented Mar 4, 2020

Copy link
Copy Markdown

CLA assistant check
All CLA requirements met.

@franziskuskiefer franziskuskiefer left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Thanks!

Comment thread include/kremlin/internal/types.h
@beurdouche

Copy link
Copy Markdown
Member

I suggest we do, I suspect these macros are breaking the Firefox build that I am debugging right now, so regrouping them would be useful...

@msprotz

msprotz commented Mar 4, 2020

Copy link
Copy Markdown
Contributor

This piece of code is a little hairy because the _gcc file that's included a little further down the file is defining functions in the non-gcc case.

I would suggest cleaning things up to make sure the _gcc.h uint128 implementation only includes implementations that rely on int128, and moving the end of the file (the one after /* Verified uint128 implementation. */) to a separate file, e.g. fstar_uint128_struct_endianness.h, which would contain hand-written implementations of the load128/store128 functions, in the case that the uint128 implementation is from _Verified.h

That way, the series of tests can be identical for type definitions and inclusion of headers, and then you can easily have:

#define IS_MSVC64 defined(_MSC_VER) && defined(_M_X64) && !defined(__clang__)
#define HAS_INT128 (defined(__x86_64__) || defined(__x86_64) || defined(__aarch64__) || \
      (defined(__powerpc64__) && defined(__LITTLE_ENDIAN__))) || (defined(_MSC_VER) && defined(__clang__))

then the tests become easier:

#if !defined(KRML_VERIFIED_UINT128) && IS_MSVC64
#  include <emmintrin.h>
typedef __m128i FStar_UInt128_uint128;
#elif !defined(KRML_VERIFIED_UINT128) && HAS_UINT128
typedef unsigned __int128 FStar_UInt128_uint128;
#else
typedef struct FStar_UInt128_uint128_s {
  uint64_t low;
  uint64_t high;
} FStar_UInt128_uint128;
#endif

#if !defined(KRML_VERIFIED_UINT128) && HAS_INT128
#include "fstar_uint128_gcc64.h"
#elif !defined(KRML_VERIFIED_UINT128) && IS_MSVC64
#include "fstar_uint128_msvc.h"
#else 
#include "FStar_UInt128_Verified.h"
#include "fstar_uint128_struct_endianness.h"
#endif

thoughts?

@beurdouche

Copy link
Copy Markdown
Member

I think I like that.

ueno added a commit to ueno/kremlin that referenced this pull request Mar 5, 2020
@ueno
ueno force-pushed the wip/dueno/uint128-s390x branch from 9b76290 to ce9fc98 Compare March 5, 2020 10:48
@ueno

ueno commented Mar 5, 2020

Copy link
Copy Markdown
Contributor Author

Thank you for the suggestion; although I haven't tested it yet, it might be something like this?

@franziskuskiefer franziskuskiefer left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

I didn't check all the details, but lgtm.

Comment thread include/kremlin/internal/types.h Outdated
Comment thread include/kremlin/internal/types.h Outdated
ueno added a commit to ueno/kremlin that referenced this pull request Mar 5, 2020
@ueno
ueno force-pushed the wip/dueno/uint128-s390x branch from ce9fc98 to 1953590 Compare March 5, 2020 14:30
Comment thread include/kremlin/internal/types.h Outdated
defined(__aarch64__) || \
(defined(__powerpc64__) && defined(__LITTLE_ENDIAN__)) || \
defined(__s390x__)) || \
(defined(_MSC_VER) && defined(__clang__)))

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

could this last check be true in a hypothetical 32-bit build on windows with clang?

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

which would then not have int128

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

I've added a !defined(_M_X64) check here; would it be sufficient?

Comment thread kremlib/c/fstar_uint128_struct_endianness.h Outdated
Comment thread kremlib/c/fstar_uint128_struct_endianness.h Outdated
@msprotz

msprotz commented Mar 6, 2020

Copy link
Copy Markdown
Contributor

this generally looks good -- our CI system has a bug so I'll have to push this to a branch on the fstarlang/kremlin repo, it looks like builds aren't succeeding for external forks

can you sign the CLA?

thanks!!

@ueno
ueno force-pushed the wip/dueno/uint128-s390x branch from 1953590 to 08b8318 Compare March 6, 2020 17:17
@ueno

ueno commented Mar 10, 2020

Copy link
Copy Markdown
Contributor Author

Thanks for the review; I've signed the CLA a while ago.

@msprotz

msprotz commented Mar 10, 2020

Copy link
Copy Markdown
Contributor

thanks -- for some reason the CLA bot was complaining earlier

@beurdouche is there any chance you could give this a go at Mozilla to make sure it doesn't break any of your platforms? that way we can anticipate rather than break you next time you pull this code

@msprotz

msprotz commented Apr 6, 2020

Copy link
Copy Markdown
Contributor

ping @beurdouche or @glandium would this fix the Firefox build on various platforms that Debian packages? I'm happy to merge this, I would just like a sanity check that this fixes the build issue

@glandium

glandium commented Apr 8, 2020

Copy link
Copy Markdown

It fixes building NSS on Debian s390x. I haven't checked other architectures.

@msprotz

msprotz commented Apr 8, 2020

Copy link
Copy Markdown
Contributor

Thanks Mike. I guess I'll just try to merge this and see what happens, unless you know how to run a candidate build for other Debian-supported platforms (I am no Debian developer so I have no clue).

@FlyGoat

FlyGoat commented Apr 19, 2020

Copy link
Copy Markdown

https://buildd.debian.org/status/package.php?p=nss&suite=sid
It fails on mips64el & riscv64 as well, should we add these two architectures to the if defined?

for MIPS64 it should be

(defined(__mips__) && defined(__LP64__))

for riscv64:

(defined(__riscv) && __riscv_xlen == 64)

I have access to mips64el machine so if you need any test please call me.

Thanks.

msprotz pushed a commit that referenced this pull request Apr 21, 2020
@msprotz

msprotz commented Apr 21, 2020

Copy link
Copy Markdown
Contributor

I've pushed a working version of this PR based on @ueno's sketch (there were multiple issues, including a non-terminated #ifdef along with a #define defining some defined(...) which clang helpfully let me know is UB).

I also integrated @FlyGoat's suggestions for the other two platforms. This is on branch protz_feature_detection of kremlin.

@FlyGoat can you let me know if this fixes the build? I've also consolidated the ifdefs so that even if we think the platform doesn't support uint128, we always fallback to the verified (albeit, slow) implementation of uint128 using a pair of uint64. For some reason, this was not done before -- I'm hoping this makes the header more resilient and "always working".

Meanwhile, I'm running some Everest regression to make sure this doesn't break anything either, including in our compilation path with MSVC.

Thanks everyone for the feedback and suggestions, much appreciated.

@msprotz

msprotz commented Apr 22, 2020

Copy link
Copy Markdown
Contributor

Everest CI came back green so I'm intending to merge protz_feature_detection at the end of the week.

@FlyGoat

FlyGoat commented Apr 23, 2020

Copy link
Copy Markdown

Can confirm it works on MIPS64EL.
Thanks!

@msprotz
msprotz merged commit b1d43e5 into FStarLang:master Apr 23, 2020
@msprotz

msprotz commented Apr 23, 2020

Copy link
Copy Markdown
Contributor

Wonderful, thanks for the help debugging!

Comment on lines +53 to +57
#define HAS_INT128 ((defined(__x86_64__) || defined(__x86_64) || \
defined(__aarch64__) || \
(defined(__powerpc64__) && defined(__LITTLE_ENDIAN__)) || \
defined(__s390x__)) || \
(defined(_MSC_VER) && !defined(_M_X64) && defined(__clang__)))

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Note that __SIZEOF_INT128__ could be used to automatically add support to the platforms that aren't explicitly listed here but have compiler support for __int128.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

thanks, I've added that too in c332229

@beurdouche

Copy link
Copy Markdown
Member

This is now in NSS master (should be in 3.53). Thanks all !
mozilla/nss@1840833

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

7 participants