package bap-core-theory

  1. Overview
  2. Docs

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].


Innovation. Community. Security.