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, 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
.
type ('s, 'k) t = ('s, 'k) origin
the abstract representation of an aliased register origin.
reg origin
is the base register.
The returned value is never an alias itself, i.e., it is a base register.
is_alias origin
if the the base register has the same size and sort as the aliased register.
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.
lo origin
returns the inclusive upper bound of the origin register to which an alias belongs.
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].