Module Bap_core_theory.Theory

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

type target

The target execution system.

  • since 2.2.0
type endianness

The ordering of the bytes.

  • since 2.2.0
type system

The operating system.

  • since 2.2.0
type abi

The application binary interface.

  • since 2.2.0
type fabi

The floating-point ABI.

  • since 2.2.0
type filetype

The file type.

  • since 2.2.0
type compiler

source to code transformer.

  • since 2.2.0
type language

the name of the code encoding.

  • since 2.2.0
type role

a target-specific role of a variable or other entity.

  • since 2.3.0
type alias

a description of the register aliasing.

See Alias.

  • since 2.4.0
type ('a, 'k) origin

a description of the origin of an aliased register.

See Origin.

  • since 2.4.0
module Semantics : sig ... end

The semantics of programs.

module Program : sig ... end

The denotation of programs.

module Source : sig ... end

The source code artifact of a compilation unit.

module Target : sig ... end

Description of the execution target.

module Unit : sig ... end

A unit of code.

module Label : sig ... end

A program label.

module Enum = KB.Enum
module Alias : sig ... end

A simple DSL for describing registers aliasing rules.

module Origin : sig ... end

The description of the origin of an aliased register.

module Role : sig ... end

A target-specific role of program entities.

module Language : sig ... end

The source code language.

module Endianness : sig ... end

Defines how multibyte words are stored in the memory.

module System : sig ... end

The Operating System.

module Abi : sig ... end

The Application Binary Interface name.

module Fabi : sig ... end

The Application Floating-point Binary Interface name.

module Filetype : sig ... end

The file type that is used to pack the unit.

module Compiler : sig ... end

Information about the compiler.

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 () returns the current or creates a new instance of the core theory.

If no parameters of the instance function were specialized and there is an instance of the current theory then this instance is returned.

Otherwise, the instance is built from all theories that match the context specified by the context 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 then 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. The current function is equivalent to the composition instance >=> require, use this function, if you want to use the current theory.

  • parameter context

    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.

  • since 2.4.0 respects the currently set theory.
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, but see also current.

For example, the following will create an theory that is a join all currently declared theories (which are not specific to any context),

let* (module CT) = Theory.(instance>=>require) () in

where let* comes from KB.Let.

To 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) ->
val current : (module Core) Bap_knowledge.knowledge

current returns the current core theory structure.

This function is the same as instance >=> require.

If there is no current theory set in the contex (via the with_current function) then a new structure is created, otherwise returns the current selected theory.

An example of usage,

let add x y =
  let* (module CT) = current in
  CT.add x y
  • since 2.4.0
val with_current : theory -> (unit -> 'a Bap_knowledge.knowledge) -> 'a Bap_knowledge.knowledge

with_current t f sets t as the current theory in the scope of f.

Evaluates compuation f in the theory of t. After f is evaluated the current theory is restored. This function could be safely called recursively, i.e., in a scope of another call to with_current. Effectively, with_current, which uses KB.Context.with_var underneath the hood, creates a dynamic scope for the theory variable.

  • since 2.4.0
module Pass : sig ... end

Core Theory Transformations.

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.