bap-core-theory 2.1.0 · OCaml Package

The Core Theory.

type cls

The class index for all Core Theories.

type theory = cls KB.obj

A theory instance. To create a new theory instance use the instance function. To manifest a theory into an OCaml module, use the require function.

type t = theory

Theory.t is theory.

module Value : sig ... end

The denotation of expression.

module Effect : sig ... end

The denotation of statements.

type 'a value = 'a Value.t

type 'a effect = 'a Effect.t

module Bool : sig ... end

The sort for boolean values.

module Bitv : sig ... end

Sorts of bitvectors

module Mem : sig ... end

Sorts of memories.

module Float : sig ... end

Sorts for floating point numbers.

module Rmode : sig ... end

Rounding modes.

type 'a pure = 'a value Bap_knowledge.knowledge

type 'a eff = 'a effect Bap_knowledge.knowledge

type ('r, 's) format = ('r, 's) Float.format

module Var : sig ... end

Variables.

type data = Effect.Sort.data

type ctrl = Effect.Sort.ctrl

type word = Bitvec.t

a concrete representation of words in the Core Theory.

type 'a var = 'a Var.t

a concrete representation of variables.

type program

a class index for class of programs.

type label = program KB.Object.t

label is an object of the program class.

module Program : sig ... end

The denotation of programs.

module Label : sig ... end

A program label.

type bool = Bool.t pure

a boolean terms

type 'a bitv = 'a Bitv.t pure

a bitvector term

type ('a, 'b) mem = ('a, 'b) Mem.t pure

a memory term

type 'f float = 'f Float.t pure

a floating point term

type rmode = Rmode.t pure

a rounding mode term

module type Init = sig ... end

The initial theory.

module type Bool = sig ... end

The theory of booleans.

module type Bitv = sig ... end

The theory of bitvectors.

module type Memory = sig ... end

The theory of memories.

module type Effect = sig ... end

The theory of effects.

module type Minimal = sig ... end

The Minimal theory.

module type Basic = sig ... end

The Basic theory of bitvector machines.

module type Fbasic = sig ... end

The Basic Theory of Floating Points.

module type Float = sig ... end

The theory of floating point numbers modulo transcendental functions.

module type Trans = sig ... end

The Theory of Transcendental Functions.

module type Core = sig ... end

The Core Theory signature.

type core = (module Core)

a type abbreviation for the core theory module type.

module Basic : sig ... end

The Basic Theory.

module Empty : Core

The empty theory.

val declare : 
  ?desc:string ->
  ?extends:string list ->
  ?context:string list ->
  ?provides:string list ->
  ?package:string ->
  name:string ->
  (module Core) Bap_knowledge.knowledge ->
  unit

declare name s that structure s as an instance of the Core Theory.

The qualified with the package name shall be unique, otherwise the declaration fails.

The extends list shall contain all theories that are included in the structure s (except the Empty theory, which is the base theory of all core theories, so there is no need to add it). Failure to list a theory in the extends list will prevent optimization during theory instantiation and may lead to less efficient theories (when the same denotation is computed twice) or even conflicts, when the extension overrides the extended theory.

parameter context
defines a context in which a theory is applicable. The declared theory could be only instantiated if the context, provided during the instantiation, contains all features specified in the context argument.

parameter provides
is a set of semantic tags that describe capabilities provided by the theory. The fully qualified name of the theory is automatically provided.

val instance : 
  ?context:string list ->
  ?requires:string list ->
  unit ->
  theory Bap_knowledge.knowledge

instance () creates an instance of the Core Theory.

The instance is built from all theories that match the context specified by the features list and provide features specified by the requires list. If any theory is subsumed by other theory, then it is excluded.

If no instances satisfy this requirement than the empty theory is returned. If only one theory satisfies the requirement, then it is returned. If many theories match, then a join of all theories is computed, stored in the knowledge base, and the resulting theory is returned.

To manifest a theory into an structure, use the require function.

parameter features
is a set of features that define the context, only those theories that have a context that is a subset of provided will be instantiated.

parameter requires
is a set of semantic features that are required. Defaults to the set of all possible features, i.e., if unspecified, then all instances applicable to the context will be loaded.

val require : theory -> (module Core) Bap_knowledge.knowledge

require theory manifests the theory as an OCaml structure.

It is only possible to create an instance of theory using the instance function. For example, the following will create an theory that is a join all currently declared theories (which are not specific to any context),

Theory.(instance>=>require) () -> fun (module Core) ->

To a create an instance for a specific context and requirements,

Theory.instance ()
  ~context:["arm-gnueabi"; "arm"]
  ~require:["bil"; "stack-frame-analysis"] >>=
Theory.require >>= fun (module Core) ->

Finally, to manifest a theory with a specific name, specify the name of the theory in the list of requirements.

Theory.instance ~requires:["bap.std:bil"] () >>=
Theory.require >>= fun (module Core) ->

module IEEE754 : sig ... end

Sorts implementing IEEE754 formats.

module Parser : sig ... end

Generates parsers of untyped ASTs into type Core Theory terms.

module Documentation : sig ... end

Documents all declared theories.

package bap-core-theory