# Module `Theory.Alias`

A simple DSL for describing registers aliasing rules.

CPU architectures commonly give names to registers parts or, contrary, give names to a concatenation of registers. For example, in x86 it is possible to address the second byte of the `RAX` register using the `AH` register. Or, in AVR, the `Y` register is refers to the concatenation of `R19` and `R18` registers.

Such kind of relationships between the CPU registers could be described using a system of equations of the form,

```         Rn = Ri * ... * Rj
...
Rm = Rj * ... * Rk```

In this system, the same register can occur on the left and right-hand sides multiple times. The system is solved for the set of basis registers, `b1;...;bN` so that each register that occurs in the system but which is not a basis register can be expressed in terms of the basis registers.

For example, given the following system,

``````def r25r24 [reg 25; reg r24];
def w [reg r25r24];
def w [reg whi; reg wlo];``````

And assuming that `r25` and `r24` are basis registers, it will be inferred that the `r25r24` and `w` are both concatenations of `r25` and `r24` and that `whi` and `wlo` are synonyms for `r25` and `r24`, correspondingly. This information is available via the `Target.unalias` function that will express an alias register in terms of corresponding basis registers, see `Origin` for more information.

The set of basis registers is defined from the register roles using a simple rule that all registers that are not `alias` are basis registers, therefore it is necessary to mark alias registers as such, otherwise the system of equations will not have a solution.

In a well-formed system of equations each alias is uniquely defined in terms of a basis register.

• since 2.4.0
`type t = alias`
`type 'a part`
`val def : 'a Bitv.t Var.t -> 'b part list -> t`

`def x parts` defines `x` as a concatenation of `parts`.

All elements of `parts` must have the same size `n` and the size of `x` should be equal to `n * List.length parts`. If this doesn't hold then the aliasing definition will fail.

The left-most position of the list of `parts` correspond to the most-significant parts (the high part) of the base register `x`.

Example,

``````[
def rax [unk; reg eax];
def eax [unk; reg ax];
def ax [reg ah; reg al]
]``````
`val reg : 'a Bitv.t Var.t -> 'a part`

`reg x` defines `x` as a part.

`val unk : 'a part`

`unk` defines an unnamed part of the register.