Legend:
Library
Module
Module type
Parameter
Class
Class type
Knowledge base analyses.
A registry of the knowledge base computations that could be used for exploring and refining the facts stored in the knowledge base.
An analysis could be parameterized by an arbitrary number of arguments, e.g., to register a function print_subr that has type
tid -> string -> Bitvec.t -> unit knowledge
use the following code
let open Project.Analysis in
register ~package "subroutine"
(args @@ unit $ string $ bitvec)
print_subr
The registered analyses could be invoked directly, using the Analysis.apply function or via the analysis plugin that provides a REPL as well as an ability to call analysis from the command-line interface or from a script. To get the list of available analyses, run `bap analyze commands`.
type t
the type for analyses
type info
information about an analysis
type grammar
a description of the analysis application syntax
type'a arg
a description of an analysis argument
type('a, 'r) args
a signature of an analysis.
The 'r type denotes the return type of an analysis, which is always unit knowledge and the 'a type variable denotes the function type of the analysis, e.g., an analysis of type
tid -> Bitvec.t -> unit knowledge
will have the following args type
(tid -> Bitvec.t -> unit knowledge, unit knowledge) args
Creates a signature of a function that takes one argument. The type 'a of the argument and its syntax are represented by the value of type 'a arg.
Examples,
args empty
-- a function of type unit -> 'r
args string
-- a function of type string -> 'r.
Note, while the 'r type is kept as a variable it will be concretized to the unit knowledge when the function of this type will be registered using the register function.
If args denote a signature of a function with type x -> y and arg has type z, then args $ arg denote a signature of type x -> y -> z.
Example
args string $ bitvec $ program - denotes a function of type string -> Bitvec.t -> Theory.Label.t -> 'r.
A note on the type
The type of the $ makes a little bit more clear if we will consider the following example, args string $ bitvec, where
args string has type (string -> 'r,'r) args and
bitvec has type Bitvec.t arg.
The type of args string $ bitvec is computed by unifying string -> 'r with 'a and 'r with 'b -> 'c, where 'b is Bitvec.t. A syntactic unification gives us the following values for the variables 'r and 'a
The name denotes the name of the rule as it will appear in the grammar definition. The parse function defines the grammar, it is called as parse fail input where input is the value of type string. The parse function should either produce a value of type 'a if input is a valid representation or use fail error to indicate that it is invalid, where error is the error message.
The parse function is a knowledge computation so it can access the knowledge base to construct the value.
The syntax of args xs $ optional x is <xs> [<x>], where <x> denotes the syntax of the argument x, [] indicates that it can be omitted, and <xs> is the grammar of the signature xs. An optional argument should be the last argument in the signature, otherwise the resulting grammar will be ambiguous.
Example, the grammar of
args string $ optional bitvec
}],
recognizes the following strings,
- ["hello"]
- ["hello 0x42"]
, where <x> denotes the syntax of the argument x, [] indicates that it can be omitted, :<s> is the literal string ":<s>", where <s> is equal to s, and <xs> is the grammar of the signature xs. If a grammar includes several keyworded arguments they may follow in an arbitrary order.
, where [] indicates that it can be omitted, :s is the literal string ":<s>", where <s> is equal to s, and <xs> is the grammar of the signature xs. If a grammar includes several flags they may follow in an arbitrary order.
Example, the grammar of
args @@
flag "foo" $
flag "bar"
}],
recognizes the following strings,
- [""]
- [":foo hello"]
- [":bar 0x42"]
- [":foo hello :bar 0x42"]
- [":bar 0x42 :foo hello"]
- and so on.
, where []... indicates that an argument can be omitted or repeated an arbitrary number of times, <x> is syntax of the agument x, and <xs> is the grammar of the signature xs. The rest x argument should be the last argument in the signature, and any extensions of the resulting signature will lead to an ambiguous grammar.
Example, the grammar of
args string $ rest bitvec
}],
recognizes the following strings,
- ["hello"]
- ["hello 0x42"]
- ["hello 0x42 42"]
- and so on