# Module `Theory.Origin`

The description of the origin of an aliased register.

When a register is defined in terms of other registers, `Origin.t` describes the relationship between an aliased register and its origin register or registers.

The `('s,'k) Origin.t` data type is parameterized with two type variables. The `'s` type variable denotes the width of the origin register(s) and `'k` denotes the kind of relationship between the alias and its origin.

Currently, we recognize two kinds of relationships. The `sub` kind defines the alias as a subset of the origin register, i.e., a contiguous sequnce of bits that are fully enclosed in the origin register. The `sup` kind defines an alias as a superset of a number of origin registers, i.e., it is a contiguous sequence of bits formed as a concatenation of the origin registers.

More kinds of relationships could be added later.

#### Example of a subset relation

Example, given the aliasing definition,

``````[
def rax [unk; reg eax];
def eax [unk; reg ax];
def ax [ah; al];
]``````

the `unalias ah` will retun the `origin` of `sub`-kind, so that `reg origin` is `rax`, `hi origin` is `15` and `lo origin` is `8`.

• since 2.4.0
`type ('s, 'k) t = ('s, 'k) origin`

the abstract representation of an aliased register origin.

`type sub`

the type index of the sub-registers

`type sup`

the type index for the super-registers

`val cast_sub : ('a, unit) t -> ('a, sub) t option`

`cast_sub origin` recovers the kind of the origin.

`val cast_sup : ('a, unit) t -> ('a, sup) t option`

`cast_sup origin` recovers the kind of the origin.

`val reg : ('a, sub) t -> 'a Bitv.t Var.t`

`reg origin` is the base register.

The returned value is never an alias itself, i.e., it is a base register.

`val is_alias : ('a, sub) t -> bool`

`is_alias origin` if the the base register has the same size and sort as the aliased register.

`val hi : ('a, sub) t -> int`

`hi origin` the inclusive upper bound. When an alias is a subset of the `origin` register, `hi origin` is the most significant bit of the alias register.

`val lo : ('a, sub) t -> int`

`lo origin` returns the inclusive upper bound of the origin register to which an alias belongs.

`val regs : ('a, sup) t -> 'a Bitv.t Var.t list`

`regs origin` returns an ordered list of constituent registers.

The registers are sorted in the big endian order, i.e., the first element of the list corresponds to the most significant part of the base register. This is the same order, in which the aliasing was specified, e.g., if the aliasing was defined as, ```def x [reg hix; reg lox], then [regs] will return [hix; lox].```