bap-std 2.3.0 · OCaml Package

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

val apply : t -> string list -> unit Bap_knowledge.knowledge

apply analysis is the computation performed by the analysis.

val find : ?package:string -> string -> t option

find ?package string searches the analysis with the given name in the registry.

val name : info -> Bap_knowledge.Knowledge.Name.t

name info is the analysis unique name.

val desc : info -> string

desc info is the short description of the analysis

val grammar : info -> grammar

grammar info is the description of the rule grammar.

val register : 
  ?desc:string ->
  ?package:string ->
  string ->
  ('a, unit Bap_knowledge.knowledge) args ->
  'a ->
  unit

register ?desc ?package name comp registers the knowledge computation as an analysis. The package:name pair should be unique.

val registered : unit -> info list

information about currently registered analyses

val args : 'a arg -> ('a -> 'b, 'b) args

args x a unary signature.

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.

val ($) : ('a, 'b -> 'c) args -> 'b arg -> ('a, 'c) args

args $ arg appends arg to args.

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

'r = Bitvec.t -> 'c
'a = string -> 'r = string -> Bitvec.t -> 'c

Therefore the type of args string $ bitvec is

('a,'c) args = (string -> Bitvec.t -> 'c,'c) args

Grammar Rules

Terminals

val empty : unit arg

empty no arguments.

The syntax is an empty string and the signature is a unary function that takes an argument of type unit.

val string : string arg

string a string argument.

The syntax is a string of characters that does not include whitespaces.

val bitvec : Bitvec.t arg

bitvec a bitvector.

The syntax is described in the Bitvec.of_string and is a non-negative binary, octal, hexadecimal, or decimal numeral.

val program : Bap_core_theory.Theory.Label.t arg

program a program label.

The syntax is a textual representation of the knowledge base symbol (Knowledge.Symbol). Unqualified names are read in the current package.

Examples, 0x88f0 or bin/arm-linux-gnueabi-echo:0x88f0.

val unit : Bap_core_theory.Theory.Unit.t arg

unit a program unit.

The syntax is a textual representation of the knowledge base symbol (Knowledge.Symbol). Unqualified names are read in the current package.

Examples, file:/bin/ls or my-unit.

val argument : 
  ?desc:string ->
  parse:
    (fail:(string -> _ Bap_knowledge.knowledge) ->
      string ->
      'a Bap_knowledge.knowledge) ->
  string ->
  'a arg

argument ~parse name defines a new terminal.

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.

Non-terminals

val optional : 'a arg -> 'a option arg

optional x an optional argument x.

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"]

val keyword : string -> 'a arg -> 'a option arg

keyword s x an optional keyworded argument x.

The syntax of args xs $ keyword s x is

<xs> [:<s> <x>]

, 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.

Example, the grammar of

  args @@
  keyword "foo" string $
  keyword "bar" bitvec
}],

recognizes the following strings,

  - [""]
  - [":foo hello"]
  - [":bar 0x42"]
  - [":foo hello :bar 0x42"]
  - [":bar 0x42 :foo hello"]

val flag : string -> bool arg

flag x a keyword x without arguments.

The syntax of args xs $ flag s is

<xs> [:<s>]

, 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.

val rest : 'a arg -> 'a list arg

rest x a zero or more x arguments.

The syntax of args xs $ rest x is

<xs> [<x>]...

, 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

module Grammar : sig ... end

Abstract Grammar descriptions.

package bap-std

Grammar Rules

Terminals

Non-terminals