kremlib.h: __int128 type not supported by Microsoft C compiler

[BarryBo]

"typedef __int128 FStar_UInt128_t, FStar_UInt128t;" doesn't compile. There is no support for generic 128-bit math. The _m128 type can be used to generate 128-bit MMX code though.

[msprotz]

The only toolchain that I've tested is clang & gcc (including mingw). I think @jkzinzindohoue has been using 128-bit integers to implement the faster algorithms for elliptic curves, so it seems like he does need this type.

Any suggestions if we want to support to the Microsoft toolchain? I assume that this is not going to be the only problem, since I'm using a bunch of C99 features (e.g. field initializers, fixed-width int macros)...

Actually, it seems like the 2013 version includes most of these, so int128 might be the only issue so far (see http://stackoverflow.com/questions/9610747/which-c99-features-are-available-in-the-ms-visual-studio-compiler)

[msprotz]

It seems like an #ifdef that uses _m128 if MSVC, __int128 otherwise would be good. Or perhaps a configure script or something along those lines.

[BarryBo]

VS2015 64-bit C compiler still doesn’t support it…

C:\Repos\Spartan>cl /c DafnyDefaultModule.c /I ..\kremlin\kremlib Microsoft (R) C/C++ Optimizing Compiler Version 19.00.24213.1 for x64 Copyright (C) Microsoft Corporation. All rights reserved.

DafnyDefaultModule.c ..\kremlin\kremlib\kremlib.h(15): error C4235: nonstandard extension used: '__int128' keyword not supported on this architecture

“long long” is 64-bit in the Microsoft compiler… an alias for “long”.

_m128 is not a drop-in replacement, as that datatype has very different operators than C integers. They represent SSE registers, so you have to emit explicit load and store code, and you’d have to implement your own 128-bit integer math on top, as they operate either on 128-bit bitfields, or pairs of 64-bit integers.

For the 128-it crypto code, the ultimate code-gen is most likely a pair of 64-bit values, both in registers and in memory, with explicit code to do carries and borrows between the two halves. It would probably be better for the EC code to do that explicit math itself, instead of depending on the C compiler’s nonstandard support.

Barry

From: Jonathan Protzenko [mailto:notifications@github.com] Sent: Monday, September 19, 2016 12:21 AM To: FStarLang/kremlin kremlin@noreply.github.com Cc: Barry Bond barrybo@microsoft.com; Author author@noreply.github.com Subject: Re: [FStarLang/kremlin] kremlib.h: __int128 type not supported by Microsoft C compiler (#2)

The only toolchain that I've tested is clang & gcc (including mingw). I think @jkzinzindohouehttps://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fgithub.com%2fjkzinzindohoue&data=02%7c01%7cbarrybo%40microsoft.com%7c35ea4f0fc33945b2ec2308d3e05d8a29%7c72f988bf86f141af91ab2d7cd011db47%7c1%7c0%7c636098664759892837&sdata=cMmtDSfN%2fLR0WBgGqz5KCtyUzGYGPv%2fh3KBTxcFCMAg%3d has been using 128-bit integers to implement the faster algorithms for elliptic curves, so it seems like he does need this type.

Any suggestions if we want to support to the Microsoft toolchain? I assume that this is not going to be the only problem, since I'm using a bunch of C99 features (e.g. field initializers, fixed-width int macros)...

Actually, it seems like the 2013 version includes most of these, so int128 might be the only issue so far (see http://stackoverflow.com/questions/9610747/which-c99-features-are-available-in-the-ms-visual-studio-compilerhttps://na01.safelinks.protection.outlook.com/?url=http%3a%2f%2fstackoverflow.com%2fquestions%2f9610747%2fwhich-c99-features-are-available-in-the-ms-visual-studio-compiler&data=02%7c01%7cbarrybo%40microsoft.com%7c35ea4f0fc33945b2ec2308d3e05d8a29%7c72f988bf86f141af91ab2d7cd011db47%7c1%7c0%7c636098664759892837&sdata=sSUdAMxf79bF3uidvk2Iu4JkqjPjMs0YQmmPLG99Mq0%3d)

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHubhttps://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fgithub.com%2fFStarLang%2fkremlin%2fissues%2f2%23issuecomment-247925554&data=02%7c01%7cbarrybo%40microsoft.com%7c35ea4f0fc33945b2ec2308d3e05d8a29%7c72f988bf86f141af91ab2d7cd011db47%7c1%7c0%7c636098664759902845&sdata=1c4siZB3CZRCY99CD6QpjVXdBUZnLPJcBw6m6zjtwMw%3d, or mute the threadhttps://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fgithub.com%2fnotifications%2funsubscribe-auth%2fAS0bncHhMnbFUdbOcMsfiEhqLr6RyUuaks5qrjfpgaJpZM4J69Uq&data=02%7c01%7cbarrybo%40microsoft.com%7c35ea4f0fc33945b2ec2308d3e05d8a29%7c72f988bf86f141af91ab2d7cd011db47%7c1%7c0%7c636098664759902845&sdata=ZMY%2fze9aV%2fDIA6WCm%2b76iuFf1nUTK7kSCDinJkqm%2bqM%3d.

[msprotz]

I agree that it's suboptimal. Let me chat with @jkzinzindohoue to figure out whether he truly needs it or whether he can get away with it once I support pairs.

[jkzinzindohoue]

I truly need it. These are not just pairs since they support all standard integer operations. I don't think it is reasonable to pay the cost of reimplementing everything and not benefit from clang and GCC's optimizations. Similarly I don't want to reimplement the curves on 64bits integers, there would be significant changes to the proof. Why not just disabling int128s and the curve compilation when using the MS compiler ?

[msprotz]

We can start having compiler-specific support libraries; Kremlin emits FStar_Int128_addition; the gcc/clang support library uses +; the msvc support library uses whatever textbook algorithm is used for 128-bit addition using two long longs.

[BarryBo]

Microsoft C compiler implements “long long” as 64-bit only. There is no 128-bit integer type in the compiler or runtime.

See https://msdn.microsoft.com/en-us/library/s3f49ktz.aspx

From: Jonathan Protzenko [mailto:notifications@github.com] Sent: Tuesday, September 20, 2016 6:56 AM To: FStarLang/kremlin kremlin@noreply.github.com Cc: Barry Bond barrybo@microsoft.com; Author author@noreply.github.com Subject: Re: [FStarLang/kremlin] kremlib.h: __int128 type not supported by Microsoft C compiler (#2)

We can start having compiler-specific support libraries; Kremlin emits FStar_Int128_addition; the gcc/clang support library uses +; the msvc support library uses whatever textbook algorithm is used for 128-bit addition using two long longs.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHubhttps://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fgithub.com%2fFStarLang%2fkremlin%2fissues%2f2%23issuecomment-248308389&data=02%7c01%7cbarrybo%40microsoft.com%7c3e1a70b8af3643f57ec208d3e161ad00%7c72f988bf86f141af91ab2d7cd011db47%7c1%7c0%7c636099782036626160&sdata=8mueZbm22Lt0U9sOsobfGLNZBo9hfNirKmLNJbraNTY%3d, or mute the threadhttps://na01.safelinks.protection.outlook.com/?url=https%3a%2f%2fgithub.com%2fnotifications%2funsubscribe-auth%2fAS0bnfspuU7_grSLywsEmP3H1HnT_Nbjks5qr-X7gaJpZM4J69Uq&data=02%7c01%7cbarrybo%40microsoft.com%7c3e1a70b8af3643f57ec208d3e161ad00%7c72f988bf86f141af91ab2d7cd011db47%7c1%7c0%7c636099782036626160&sdata=Q5QTW07thPco4sl3ewQgh21sIZk9JPYRONsJLPvXkEY%3d.

[msprotz]

Sorry, I meant implement uint128_t using a struct with two long longs, then implement arithmetic "by hand" based on that.

[msprotz]

3dda050 should work around the issue but we still need to determine what we intend to do if we want to support @jkzinzindohoue's code with MSVC

[msprotz]

@jkzinzindohoue just provided an implementation for int128s that works with Compcert and, mostly, the Microsoft C compiler.

[jkzinzindohoue]

To be precise, it provides an implementation for addition, subtraction and bitwise operators. I think they follow our constant time discipline (see custom128.c). There is also support to multiply two uint64 to get a uint128, and casts back and forth from uint64 to uint128. But no more (because I do not need more for now).