Theory.Label
A program label.
Labels are generalization of addresses and are use to uniquely identify a program location, even if this location is not having an address. Labels are Knowledge objects of the program
class, therefore they have the semantics property, accessible via the Program.Semantics.slot
.
type t = label
val possible_name : (program, string option KB.opinions) KB.slot
a possible (and opinionated) name.
Use this slot when the name of a program is not really known or when it is possible that other name providers will have a conflicting opinion.
the interrupt vector of the label.
Labels could also represent code in interrupt vector routines, therefore the might be referenced by a number, not by an address of a name.
the program encoding.
The language used to encode the program.
possible aliases under which the label might be known.
This may include versioned names, demangled names, etc.
a compilation unit (file/library/object) to which this label belongs
val target : label -> Target.t Bap_knowledge.knowledge
target label
is the Unit.target
of the label's unit
.
a link is valid if it references a valid program.
If a link references a memory location which is not executable, then it is not valid.
a link is subroutine if it is an entry point to a subroutine.
val fresh : t Bap_knowledge.knowledge
fresh
a fresh label (a shortcut for KB.create cls
).
val null : t
null
is a shortcut for KB.null cls
.
val for_addr : ?package:string -> Bitvec.t -> t Bap_knowledge.knowledge
for_addr x
generates a link to address x
.
It is guaranteed that every call for_addr ~package x
with the same arguments will return the same label.
The addr
property of the created object is set to x
.
If the package
parameter is not specified then the created object is interned in the currently selected package otherwise it is interned in the provided package
.
val for_name : ?package:string -> string -> t Bap_knowledge.knowledge
for_name x
generates a link to program with linkage name x
.
It is guaranteed that every call for_name ~package x
with the same arguments will return the same label, which is the same object as the Knowledge.Symbol.intern ?package name
.
The name
property of the created object is set to x
.
If the package
parameter is not specified then the created object is interned in the currently selected package otherwise it is interned in the provided package
.
val for_ivec : ?package:string -> int -> t Bap_knowledge.knowledge
for_ivec x
generates a link to an interrupt service number x
.
It is guaranteed that every call for_addr ~package x
with the same arguments will return the same label, which is the same object as the Knowledge.Symbol.intern ?package name
, where name
is sprintf "ivec-%x" x
.
The addr
property of the created object is set to x
.
If the package
parameter is not specified then the created object is interned in the currently selected package otherwise it is interned in the provided package
.
include Bap_knowledge.Knowledge.Object.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