4.14 Working with Incorrect Data

We have seen how Poke type definitions very often include constraint expressions reflecting the integrity of the data stored in these types.

Consider for example the following abbreviated description of the header of an ELF file:

type Elf64_Ehdr =
  struct
  {
    struct
    {
      byte[4] ei_mag = [0x7fUB, 'E', 'L', 'F'];
      byte ei_class;
      [...]
    } e_ident;

    Elf_Half e_type;
    Elf_Half e_machine;
    Elf_Word e_version = EV_CURRENT;
    [...]
    Elf_Half e_shstrndx : e_shnum == 0 || e_shstrndx < e_shnum;
  };

There are three constraint expressions in the definition above:

• The constraint expression in the field ei_mag makes sure that a right magic number begins the header.
• The constraint expression in e_version checks that the ELF version is the current version.
• The constraint expression in e_shstrndx checks that the index stored in the field doesn’t overflow the section header table of the file.

Every time we construct or map an Elf64_Ehdr value the constraint expressions are checked. In case any of the constraints are not satisfied we get a “constraint violation exception”. This is useful to realize that we are facing invalid data (when mapping) or that we are trying to build an invalid ELF header (when constructing.)

However, the exception avoids the completion of the mapping or construction operation. Sometimes this is inconvenient:

• When we are given invalid data that we want to explore or fix. Imagine for example a programmer investigating a possible assembler or linker bug that results in an invalid ELF file.
• When we are discovering or inferring the structure of some data: we suspect at some point there may be something that is similar to an ELF header.
• When we want to create invalid data. Suppose for example a programmer who is building a test case for the linker, that requires a corrupted ELF file.

The way poke provides support for these situation is using the concept of map strictness. Suppose we map an ELF header in some IO space:

(poke) load elf
(poke) var ehdr = Elf64_Ehdr @ 0#B

The mapping operator @ performs a strict mapping. This means that constraint expressions are evaluated and the operation is interrupted if any constraint fails, as described above. Also, this means the integrity will be checked when the data is modified:

(poke) ehdr.e_version = 666
unhandled constraint violation exception

So the mapping operator generates “strict” values. We can check the strictness of a mapped value using the 'strict attribute:

(poke) ehdr'strict
1

If we know that we are facing corrupted data, or if we want to corrupt the ELF header, we perform a non-strict mapping using a variant of the mapping operator:

(poke) var ehdr_ns = Elf64_Ehdr @! 0#B
(poke) ehdr_ns'strict
0

When mapping is performend in non-strict mode, the constraint expressions are still executed, but their resulting value is discarded. The constraint expressions are executed regardless of strictness because it is fairly common for them to include side-effects that have a calculated impact in subsequent operations, such as for example setting the endianness or some other global state.

We can now corrupt the header in the example above:

(poke) ehdr_ns.e_version = 666