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.

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.


  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.