Document address offset fixup and make it optional

[hanno-becker]

Background: Address offset fixup is an important feature to facilitate software pipelining as it allows the reordering of ldr/str instructions with increment operating on the same address register. Normally, SLOTHY would not allow such reordering because it breaks data dependencies, but commutativity relations such as ldr _, [x0]; str _, [x0], #imm == str _, [x0], #imm; ldr _, [x0, #-imm] makes it possible, assuming a suitable 'address offset fixup' -- hence the name.

Issue: While important, address offset fixup is still somewhat experimental and poorly documented. What's more, SLOTHY's selfcheck is not aware of it and cannot catch bugs it may still have. To facilitate debugging, address offset fixup should be behind a configuration option to begin with.

Acceptance criteria:

• SLOTHY supports a configuration option config.address_offset_fixup controlling the use of address offset fixup.
• Document what determines whether instructions can participate in address offset fixup.