package bap-core-theory

  1. Overview
  2. Docs
On This Page
  1. Properties

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

Properties

val addr : (program, Bitvec.t option) KB.slot

the address of the label.

val name : (program, string option) KB.slot

the linkage name of the 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.

val ivec : (program, int option) KB.slot

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.

val encoding : (program, language) KB.slot

the program encoding.

The language used to encode the program.

  • since 2.2.0

possible aliases under which the label might be known.

This may include versioned names, demangled names, etc.

val unit : (program, Unit.t option) KB.slot

a compilation unit (file/library/object) to which this label belongs

target label is the Unit.target of the label's unit.

val is_valid : (program, bool option) KB.slot

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.

val is_subroutine : (program, bool option) KB.slot

a link is subroutine if it is an entry point to a subroutine.

fresh a fresh label (a shortcut for KB.create cls).

  • since 2.4.0
val null : t

null is a shortcut for KB.null cls.

  • since 2.4.0
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.

  • since 2.2.0 the [package] parameter is added
  • since 2.2.0 the object is interned in the currently selected 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.

  • since 2.2.0 the [package] parameter is added
  • since 2.2.0 the object is interned in the currently selected 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.

  • since 2.2.0 the [package] parameter is added
  • since 2.2.0 the object is interned in the currently selected package
include Bap_knowledge.Knowledge.Object.S with type t := t
include Sexplib0.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
include Base.Comparisons.S with type t := t
include Base.Comparisons.Infix 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

compare t1 t2 returns 0 if t1 is equal to t2, a negative integer if t1 is less than t2, and a positive integer if t1 is greater than t2.

val min : t -> t -> t
val max : t -> t -> t
val ascending : t -> t -> int

ascending is identical to compare. descending x y = ascending y x. These are intended to be mnemonic when used like List.sort ~compare:ascending and List.sort ~cmp:descending, since they cause the list to be sorted in ascending or descending order, respectively.

val descending : t -> t -> int
val between : t -> low:t -> high:t -> bool

between t ~low ~high means low <= t <= high

val clamp_exn : t -> min:t -> max:t -> t

clamp_exn t ~min ~max returns t', the closest value to t such that between t' ~low:min ~high:max is true.

Raises if not (min <= max).

val clamp : t -> min:t -> max:t -> t Base.Or_error.t
include Base.Comparator.S with type t := t
type comparator_witness
include Core_kernel.Binable.S with type t := t
include Bin_prot.Binable.S_only_functions 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

This function only needs implementation if t exposed to be a polymorphic variant. Despite what the type reads, this does *not* produce a function after reading; instead it takes the constructor tag (int) before reading and reads the rest of the variant t afterwards.

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