Module Project.Analysis

the type for analyses

information about an analysis

a description of the analysis application syntax

a description of an analysis argument

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

apply analysis is the computation performed by the analysis.

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

name info is the analysis unique name.

desc info is the short description of the analysis

grammar info is the description of the rule grammar.

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

information about currently registered analyses

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.

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

empty no arguments.

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

string a string argument.

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

bitvec a bitvector.

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

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.

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.

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.

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

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

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.

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

Abstract Grammar descriptions.