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.

since 2.2.0

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 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 ->
  ?vars:unit Var.t 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.

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

Introduces 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 matches : t -> string -> bool

matches target name is true if 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. E.g., matches target "mips".

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 returns an ordered list of targets that belongs 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 : 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.

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

module Options : sig ... end

An extensible set of the target options.

package bap-core-theory

Module Theory.Target

Module `Theory.Target`