htole64

[dinosaure]

From #29, a question still exists where ocaml-freestanding does not provide htole64 or more generally, <inttypes.h> & these functions. From the extraction point-of-view, 2 problems appear:

• PRIu64 is not defined (only used to debug) (eg. mirage/ocaml-freestanding#60)
• htole64 is not defined and we must update <inttypes.h> to <stdint.h>

The first problem can be fixed with gcc -DPRIu64=... but it's a hack. The second problem is solved by mirage-crypto (eg. src/native/bitfn.h which defines such functions).

1) From my perspective, even if it's a duplicate, we should be able to define by ourselves such functions into hacl (but it can be error-prone).

2) An other solution is to extend ocaml-freestanding to provide such macro/function and help by this way mirage-crypto and hacl. However. as it's explained into mirage/ocaml-freestanding#60, it's not really the proper way.

Should we choose 1) or 2) ?

/cc @hannesm /cc @mato

[hannesm]

@dinosaure thanks for opening this issue as a new one. I think the PRIu is dealt with in this repository (not sure whether this is "appropriate" and "sustainable", but I'd be keen to first get an update story for the imported C code before figuring out what to do there.

For htole64 and le64toh, while reading the source here (src/kremlib.h) I can spot there are already definitions thereof, but they are guarded in a long ifdef chain. I'd suggest we do as follows (for the freestanding build at least, I have not looked into the xen build):

• not define linux
• include <endian.h> (to get the __BYTE_ORDER definition)
• end up in the

  /* ... generic little-endian fallback code */
  #elif defined(__BYTE_ORDER__) && __BYTE_ORDER__ == __ORDER_LITTLE_ENDIAN__

  case (or, on big endian, in the case before).

thus: no modification of ocaml-freestanding needed; no dependency onto mirage-crypto needed. :)

[hannesm]

(I can try to figure out a PR for the approach outlined above during this week)

[hannesm]

it turns out to be a bit more complicated:

• solo5 on BSD copies various headers to solo5../crt (amongst them sys/endian.h)
• solo5 on Linux copies only the cc -print-file-name=include directory (with lots of intrinsics, they are not present on *BSD)
• ocaml-freestanding provides a different set of headers (e.g. endian.h)

now, a cross-build of hacl excutes (amongst other things):

$ (cd _build/default/freestanding && /usr/home/hannes/.opam/4.10.0/bin/ocamlc.opt -g -I /usr/home/hannes/.opam/4.10.0/lib/ocaml-freestanding -ccopt -I/usr/home/hannes/.opam/4.10.0/lib/pkgconfig/../../include/ocaml-freestanding -ccopt -ffreestanding -ccopt -fstack-protector-strong -ccopt -nostdlibinc -ccopt -isystem -ccopt /usr/home/hannes/.opam/4.10.0/lib/pkgconfig/../../include/solo5-bindings-hvt/crt -ccopt -I/usr/home/hannes/.opam/4.10.0/lib/pkgconfig/../../include/solo5-bindings-hvt/solo5 -ccopt -g -o Hacl_Curve25519.o Hacl_Curve25519.c)

which (for reasons unknown to me) evaluates the #elif defined(__FreeBSD__) to true, and using this way includes (the copied) sys/endian.h that defines the right symbols.

On Linux, the #if defined(__linux__) is true, and #include <endian.h> entails the inclusion of ocaml-freestanding endian.h, which is not very complete (i.e. missing the le64toh definitions etc.).

I guess I have some questions @mato:

• why does #if defined(__FreeBSD__) evaluate to true? and how can we stop doing this (I believe we instead would like to have a specific #if defined(__freestanding__) cases in our supportive C code)?
• EDIT: cc -dM -E - < /dev/null contains that __FreeBSD__ is defined... (and passing -undef to the C compiler would remove all the pre-defined macros...)
• in solo5, should we copy less system headers (or alternatively do the same for a linux host (looking at configure.sh)? I'm pretty sure I'm responsible for copying them...
• instead should ocaml-freestanding provide an endian.h (that is not specified by posix, but from man(3) endian on a linux host, the set of functions is rather small (and useful). this would as well allow us in mirage-crypto to remove some cargo-culted copied code.

[mato]

why does #if defined(FreeBSD) evaluate to true?

Because we're appropriating the host toolchain, and it always defines that.

have a specific #if defined(freestanding) cases

Defining __freestanding__ is a good idea (at the ocaml-freestanding layer), as you propose in https://github.com/mirage/ocaml-freestanding/pull/73. However, it won't make __FreeBSD__ go away.

and passing -undef to the C compiler would remove all the pre-defined macros

Where is -undef documented? I didn't know about that. However, it's not a great solution as it'll probably undefine various things we do want such as __<arch>__.

in solo5, should we copy less system headers (or alternatively do the same for a linux host (looking at configure.sh)?

Yes, I merged that PR. Not sure why endian.h was in there, it's a bug.

instead should ocaml-freestanding provide an endian.h

Yes, ocaml-freestanding can provide the needed functions in its own endian.h, as proposed in https://github.com/mirage/ocaml-freestanding/pull/73. I'll comment on the specifics there.

[hannesm]

@mato

Defining freestanding is a good idea (at the ocaml-freestanding layer), as you propose in mirage/ocaml-freestanding#73. However, it won't make FreeBSD go away.

Yes, I'm aware of that (so the #ifdef .. #elif #endif chain first needs to check for __freestanding__) ;)

Where is -undef documented?

from man(1) gcc:

-undef
    Do not predefine any system-specific or GCC-specific macros. The standard predefined macros remain defined.

However, it's not a great solution as it'll probably undefine various things we do want such as __<arch>__.

yes, indeed. I came to the same conclusion.

$ cc -undef -dM -E - < /dev/null 
#define __STDC_HOSTED__ 1
#define __STDC_UTF_16__ 1
#define __STDC_UTF_32__ 1
#define __STDC_VERSION__ 201112L
#define __STDC__ 1

Thanks for your answer and cleanups.

[mato]

Yes, I'm aware of that (so the #ifdef .. #elif #endif chain first needs to check for freestanding) ;)

Yeah, that's probably the best option. We could also manually pass -UFreeBSD and suchlike, but I'd prefer to avoid that (maintenance nightmare, pollutes CFLAGS, etc.)

[dinosaure]

Still open for me, I need to check by hands but I will able to do that next week - however, consider it as solved.

[hannesm]

ocaml-freestanding since 0.6.0 now provides (a) inttypes.h and (b) endian.h, with the "missing" functionality for hacl. I just released hacl 0.1.1 with the mirage cross-compilation runes. Closing this issue, please comment / reopen if there's something remaining to be done for you.