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 Base.Comparable.S with type t := t
val comparator : (t, comparator_witness) Base__.Comparator.comparator
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_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.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.
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.
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 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
.
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
.
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 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.
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.
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"
.
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.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.
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
.
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.
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 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
.
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
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
.
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)).
has_roles t roles v
is true if v
has all the roles
in t
.
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
.
val endianness : t -> endianness
endianness target
describes the byte order.
Describes how multibyte words are stored in the main memory.
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.
module Options : sig ... end
An extensible set of the target options.