Module Theory.Target

Description of the execution target.

An abstract description of the system on which a program is intended to be run. The description precisely describes various architectual and microarchitectual details of the target system, and could be extended with further details either internally, by adding more fields (and functions to this module) or storing those options in Options.t; or externally, by maintaining finite mappings from Target.t to corresponding properties.

The Target.t has a lightweight immediate representation, which is portable across OCaml runtime and persistent across versions of BAP and OCaml.

type t = target

the abstract type representing the target.

This type is a unique identifier of the target, represented as KB.Name.t underneath the hood.

include Core_kernel.Bin_prot.Binable.S with type t := t
include Ppx_sexp_conv_lib.Sexpable.S with type t := t
val t_of_sexp : Sexplib0__.Sexp.t -> t
val sexp_of_t : t -> Sexplib0__.Sexp.t
include Base.Comparable.S with type t := t
val (>=) : t -> t -> bool
val (<=) : t -> t -> bool
val (=) : t -> t -> bool
val (>) : t -> t -> bool
val (<) : t -> t -> bool
val (<>) : t -> t -> bool
val equal : t -> t -> bool
val compare : t -> t -> int
val min : t -> t -> t
val max : t -> t -> t
val ascending : t -> t -> int
val descending : t -> t -> int
val between : t -> low:t -> high:t -> bool
val clamp_exn : t -> min:t -> max:t -> t
val clamp : t -> min:t -> max:t -> t Base__.Or_error.t
type comparator_witness
val comparator : (t, comparator_witness) Base__.Comparator.comparator
val validate_lbound : min:t Base__.Maybe_bound.t -> t Base__.Validate.check
val validate_ubound : max:t Base__.Maybe_bound.t -> t Base__.Validate.check
val validate_bound : min:t Base__.Maybe_bound.t -> max:t Base__.Maybe_bound.t -> t Base__.Validate.check
include Core_kernel.Binable.S with type t := t
val bin_size_t : t Bin_prot.Size.sizer
val bin_write_t : t Bin_prot.Write.writer
val bin_read_t : t Bin_prot.Read.reader
val __bin_read_t__ : (int -> t) Bin_prot.Read.reader
val bin_shape_t : Bin_prot.Shape.t
val bin_writer_t : t Bin_prot.Type_class.writer
val bin_reader_t : t Bin_prot.Type_class.reader
val bin_t : t Bin_prot.Type_class.t
include Core_kernel.Stringable.S with type t := t
val of_string : string -> t
val to_string : t -> string
include Core_kernel.Pretty_printer.S with type t := t
val pp : Base__.Formatter.t -> t -> unit
type options = (options_cls, unit) KB.cls KB.Value.t

The set of target-specific options.

and options_cls
val declare : ?parent:t -> ?bits:int -> ?byte:int -> ?data:(_, _) Mem.t Var.t -> ?code:(_, _) Mem.t Var.t -> ?data_alignment:int -> ?code_alignment:int -> ?vars:unit Var.t list -> ?regs:(role list * unit Var.t list) list -> ?aliasing:alias list -> ?endianness:endianness -> ?system:system -> ?abi:abi -> ?fabi:fabi -> ?filetype:filetype -> ?options:options -> ?nicknames:string list -> ?package:string -> string -> t

declare ?package name declares a new execution target.

The packaged name of the target must be unique and the target shall be declared during the module registration (commonly as a toplevel definition of a module that implements the target support package).

The newly declared target inherits all the parameters from the parent target unless they are explicitly overriden.

For the description of parameters see the corresponding accessor functions in this module.

If the target architecture has register aliases, i.e., registers that correspond to some parts of other registers, then they should be properly described with the aliasing parameter, using the Alias language, in which each register that has aliases is structurally defined in terms of its subparts.

  • since 2.3.0 has the [regs] optional parameter.
  • since 2.4.0 has the [aliasing] optional parameters.

register <variants> t generates and registers a list of targets.

For a list of possible target properties generate a set of unique targets and declare them. To generate a unique name the following scheme is used,

<name>-<system>-<abi><fabi>-<format>+<option>...v}

        where if a property is [:unknown] then it is not listed in
        the name (including the separator, if necessary).

        E.g.,
        {v
        arm-linux-gnueabihf-elf
        armv7-linux-gnueabihf+m3
val register : ?systems:system list -> ?abis:abi list -> ?fabis:fabi list -> ?filetypes:filetype list -> ?options:options list -> ?package:string -> t -> unit
val lookup : ?package:string -> string -> t option

lookup ?package name lookups a target with the given name.

If name is unqualified then it is qualified with the package (which itself defaults to "user"), otherwise the package parameter is ignored.

Returns None if the target with the given name wasn't declared.

val select : ?unique:bool -> ?strict:bool -> ?parent:t -> ?system:system -> ?abi:abi -> ?fabi:fabi -> ?filetype:filetype -> ?options:options -> unit -> t

select <reqs> () selects a target that matches requirements.

Selects the least specific target that belongs to parent and matches the specified requirements. If unique is true and there is no single match then raises an exception, otherwise returns the first in the family order match (i.e., the least specific of the matches).

If there are no matching targets returns parent if strict is false, otherwise fails with an exception.

The matching procedure uses the domain structure of the corresponding parameters. A target matches the constraint if all properties of the target matches the corresponding parameters. A property matches a parameter if the property is greater or equal (in the domain order) than the parameter.

See also filter.

  • parameter parent

    defaults to unknown

  • parameter unique

    defaults to false

  • parameter strict

    defaults to false

  • parameter system

    defaults to System.unknown

  • parameter abi

    defaults to Abi.unknown

  • parameter fabi

    defaults to Fabi.unknown

  • parameter options

    defaults to Options.empty

  • since 2.5.0
val filter : ?strict:bool -> ?parent:t -> ?system:system -> ?abi:abi -> ?fabi:fabi -> ?filetype:filetype -> ?options:options -> unit -> t list

filter <reqs> () selects targets that matches requirements.

Filters targets that belong to parent and match the specified requirements. The targets are returned in the family order, i.e., the least specific target is comming first. This is the same order in which family list targets.

The matching procedure uses the domain structure of the corresponding parameters. A target matches the constraint if all properties of the target matches the corresponding parameters. A property matches a parameter if the property is greater or equal (in the domain order) than the parameter.

See also select.

  • parameter parent

    defaults to unknown

  • parameter system

    defaults to System.unknown

  • parameter abi

    defaults to Abi.unknown

  • parameter fabi

    defaults to Fabi.unknown

  • parameter options

    defaults to Options.empty

  • since 2.5.0
val get : ?package:string -> string -> t

get ?package name returns the target with the given name.

If the target with the given name wasn't declared raises an exception.

See lookup for the details on the name and package parameters.

val read : ?package:string -> string -> t

read ?package name is a synonym for get ?package name.

Introduced for the consistency with the Enum.S interface.

val declared : unit -> t list

declared () is the list of declared targets. The order is unspecified, see also families. The list doesn't include the unknown target.

val unknown : t

unknown the unknown architecture.

The core-theory:unknown is the ancestor of all other architectures with all fields set to defaults as described in declare.

val is_unknown : t -> bool

is_unknown t is true if t is equal to unknown.

val name : t -> KB.Name.t

name target is the unique name of the target.

val nicknames : t -> Core_kernel.String.Caseless.Set.t

nicknames t is the set of the target nicknames.

Note that the set is using caseless comparison.

  • since 2.5.0
val matching : t -> string -> t option

matching t name the target that matches name.

matching t name is Some r where r is t or the closest ancestor of t such that r's name is equal to name or one of name is r's nicknames.

  • since 2.5.0
val matches : t -> string -> bool

matches t name when matchingtname is not None.

matching t name is true when name matches either the unqualified name of the target itsef or one of its ancestors; or if the name matches one of the target nicknames or the target parents nicknames.

E.g., matches target "mips".

  • before 2.5.0

    the nicknames of the ancestors weren't taken into account @after 2.5.0 uses the ancestors nicknames for matching

val order : t -> t -> KB.Order.partial

order t t' the order of t and t' in the target hierarchy.

  • order t t' is NC if t and t' are different and neither t is an ancestor of t' nor t' is an ancestor of t;
  • order t t' is LT if t is an ancestor of t';
  • order t t' is GT if t' is an ancestor of t;
  • order t t' is EQ if t and t' are equal.
val belongs : t -> t -> bool

belongs t t' iff order t t' is GT or EQ.

The belongs t predicate defines a family of targets that are derived from the target t, e.g., belongs arm defines a set of all ARM targets.

val parent : t -> t

parent t is the closest ancestor of t or unknown if t is unknown

val parents : t -> t list

parents t returns an ordered list of t's ancestors.

The closest ancestor comes first in the list and the last element of the list is unknown.

val family : t -> t list

family p an ordered list of targets s.t. each belongs to p.

The family members are ordered according to their hierarchy with p comming first.

val partition : t list -> t list list

partition targets partitions targets into families.

The partition is a list where each element is a list of family members with the family parent coming as the first member and all other members ordered in the ascending order of their hierarchy, i.e., for each p::fs in families () family p is p:fs. The families itself are partitioned by the lexical order of the unqualified names of the family parents.

val families : unit -> t list list

families () partitions all declared targets into families, i.e., it is partition @@ declared ().

val bits : t -> int

bits target is the bitness of the target architecture.

It is commonly the number of bits of the machine word in the given architecture and corresponds to the logical width of the data bus.

val byte : t -> int

byte target is the size of the target's byte.

val data_addr_size : t -> int

data_addr_size target is the number of bits in the data address.

The logical size of the data address, which is taken from the sort of the keys of the data memory variable.

val code_addr_size : t -> int

code_addr_size target the size of the program counter.

The size of the instruction address, which is taken from the sort of the keys of the data memory variable.

val data_alignment : t -> int

The required data addresses alignment in bits.

The target t requires that all data addresses are multiples of data_alignment t-bit words.

val code_alignment : t -> int

The required code addresses alignment in bits.

The target t requires that all code addresses are multiples of code_alignment t-bit words.

val data : t -> (unit, unit) Mem.t Var.t

data target the main memory variable.

val code : t -> (unit, unit) Mem.t Var.t

code target the code memory variable.

val vars : t -> Core_kernel.Set.M(Var.Top).t

vars target is the set of all registers and memories.

The set includes both general-purpose, floating-points, and status registers, as well variables that denote memories and other entities specific to the target. The set includes all variables that were passed to the target definition, through data, code, vars, and regs variables.

@see also regs.

val regs : ?exclude:role list -> ?roles:role list -> t -> Core_kernel.Set.M(Var.Top).t

regs ?exclude ?roles target returns a set of registers.

If the roles list is passed then narrows down the list to registers that have all the specified roles. If exclude is specified then excludes all registers that have those roles.

Example,

regs ~roles:[general; integer] ~exclude:[stack_pointer; frame_pointer
  • since 2.3.0
val reg : ?exclude:role list -> ?unique:bool -> t -> role -> unit Var.t option

reg target role returns a register with the given role.

Returns a register from a set of registers regs ~roles:[role] ?exlude t. If the set is not singleton and unique is true (defaults to false) returns None.

  • since 2.3.0
val var : t -> string -> unit Var.t option

var target name returns a target variable with the given name.

The variable is searched in all variables and registers provided in target declaration. The search is O(log(N)).

  • since 2.3.0
val has_roles : t -> role list -> 'a Var.t -> bool

has_roles t roles v is true if v has all the roles in t.

  • since 2.3.0
val unalias : t -> 'a Var.t -> ('b, unit) origin option

unalias v if v is an alias then returns its origin.

If v is defined in terms of other registers then the returned value denotes v in terms of the original register or registers. See Origin.

  • since 2.4.0
val endianness : t -> endianness

endianness target describes the byte order.

Describes how multibyte words are stored in the main memory.

val system : t -> system

system target the target operating system.

val abi : t -> abi

abi target the target application binary interface.

val fabi : t -> fabi

fabi target the target floating-point ABI.

val filetype : t -> filetype

filetype target the target executable file type.

val options : t -> options

options target the target-specific set of options.

val domain : t KB.domain

the domain type class for the targets.

Targets form a flat domain with unknown in the bottom.

val persistent : t KB.persistent

the persistence type class, derived from KB.Name.persistent

val hash : t -> int

hash t returns the target's hash.

  • since 2.5.0
module Options : sig ... end

An extensible set of the target options.