24.6.8 Field Labels ¶

In structs, each field is associated with an offset, which is relative to the beginning of the struct. This is the offset used when reading and writing the field from/to the IO space when mapping.

The offset is reset to zero bits at the beginning of the struct type, and it is increased by the size of the fields:

struct
{
                /* Offset: 0#b */
    uint<1> f1; /* Offset: 1#b */
    sint<7> f2; /* Offset: 1#B */
    int     f3; /* Offset: 5#B */
    Bar     f4; /* Offset: 23#B */
}

It is possible to specify an alternative offset for a field using a field label, using the following syntax:

 field_type field_name @ offset;

Which defines a label for the field field_name with value offset. Note that the label specifier shall appear after any constraint expression and initialization value if the field has these.

Consider for example an entry in an ELF symbol table. Each entry has a st_info field which is 64-bits long, that in turn can be interpreted as two fields st_bind and st_type.

The obvious solution is to encode st_info as a sub-struct that is integral, like this:

struct
{
  elf32_word st_name;
  struct uint<64>
  {
    uint<60> st_bind;
    uint<4> st_type;
  } st_info;
}

This makes the value of st_info easily accessible as an integral value. But we may prefer to use labels instead:

struct
{
  elf32_word st_name;
  elf64_word st_info;
  uint<60> st_bind @ 4#B;
  uint<4> st_type @ 4#B + 60#b;
}

The resulting struct has fields st_info, st_bind and st_type, with the last two overlapping the first.

Field labels are also useful in the rare cases where a variable part of a struct depends on some data that comes after it. This happens for example in the COFF “line number” structures, which are defined like this in C:

struct external_lineno
{
  union
  {
    char l_symndx[4]; /* function name symbol index, iff l_lnno == 0*/
    char l_paddr[4];  /* (physical) address of line number */
  } l_addr;

  char l_lnno[L_LNNO_SIZE]; /* line number  */
};

i.e. the l_addr field is to be interpreted as an index in a table or as a physical address depending on the value of l_lnno.

This is one way to denote the above data structure using Poke struct labels:

type COFF_LINENO_32 =
  struct
  {
    uint<32> l_lnno  4#B; /* Line number.  */

    union
    {
      uint<32> l_symndx : l_lnno == 0;
      offset<uint<32>,B> l_paddr;
    } l_addr  0#B;
  };

Note how the l_lnno field is stored after l_addr even if they appear in reverse order in the struct definition. This allows us to refer to l_nno in the constraints for the union fields.