AWS benchmarks relaying on htonl and friends but spec is not provided - what is their spec?

[zvonimir]

For example, see here: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/aws-c-common/aws_byte_cursor_read_be64_harness.i#L3966

There are more benchmarks that seem to rely on these functions without providing a body (spec) for them:
https://linux.die.net/man/3/htonl

The fact that body is not provided leads to bugs in those benchmarks.

Now, they are POSIX, but their implementation is platform-specific (depends on how ints are represented).
So what should we use as their spec?

[PhilippWendler]

What exactly is the question? htonl is defined to convert from the host byte order to the network byte order. The host byte order is the one that is used for storing ints in memory internally. Network byte order is most significant byte first (MSB).

[zvonimir]

What is the host byte order prescribed by SVCOMP?
I searched through the rules and I couldn't find that anywhere. Thanks!

[PhilippWendler]

The same that is used by the verifier for storing (unsigned) ints in memory?

I agree that SV-COMP does not define which byte order verifiers should assume in general, addressing this question would be part of #1125. Probably most participants assume x86 byte order, or maybe some verifiers even check whether the program fulfills the property under all possible byte orders.

But for htonl etc. the situation seems clear, whatever the verifier assumes as byte order in memory must match what it uses as host byte order for these functions.

[zvonimir]

Yep. So I should assume x86 byte order and that should probably be fine. Ok, thanks!

[mchalupa]

Well, there is still the issue here that the functions are POSIX functions, not GNU nor ANSI C, so these should be defined in the benchmarks (the same had to be done with all the POSIX functions in busybox benchmarks)

[zvonimir]

Actually, I vaguely remember that POSIX functions have to be defined by verifiers as well, the same as standard C library functions. I could be wrong, but that is how I remember discussions around this from previous years.

[mchalupa]

I am pretty sure that rules specify the benchmarks to be in GNU C and that is why we defined all the POSIX functions in BusyBox: #394, #525, #542. For the C standard function, it is true (as those are included in GNU C).