Bap_core_theory.Theory
The Core Theory.
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 label = program KB.Object.t
label is an object of the program class.
a description of the register aliasing.
See Alias
.
a description of the origin of an aliased register.
See Origin
.
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.
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.
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.
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.
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
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.
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.