Next: Pinned Structs, Previous: Field Initializers, Up: Structs [Contents][Index]
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.
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.
Next: Pinned Structs, Previous: Field Initializers, Up: Structs [Contents][Index]