au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Dargent endianness annotations #373

Closed lukakerr closed 3 years ago

lukakerr commented 4 years ago

Implement endianness annotations for Dargent layouts. The new syntax is shown below:

type XY = { x: U32, y: U32 }
  layout
    record { x: 4B using LE
           , y: 4B at 4B using BE
           }

If no endianness annotation is specified, it defaults to the machine's endianness.

crizkallah commented 3 years ago

On Wed, Jul 15, 2020 at 4:58 PM CraigMcL notifications@github.com wrote:

@cmcl commented on this pull request.

In cogent/lib/cogent-endianness.h https://github.com/NICTA/cogent/pull/373#discussion_r454815428:

@@ -0,0 +1,54 @@ +#ifndef COGENT_ENDIANNESS_H +#define COGENT_ENDIANNESS_H + +const int ENDIANNESS_TEST = 1; +#define IS_BIG_ENDIAN ((char )&ENDIANNESS_TEST == 0) + +u16 swap_u16(u16 v) {

  • return (v << 8) | (v >> 8); +}
  • +u32 swap_u32(u32 v) {

GNU provides swapping functions (bswap_*) in the header file. Might it be a good idea to use these functions instead?

Implementing these ourselves will be better for verification.