Module Abstract_domain

module Abstract_domain: sig .. end

Abstract domains of the analysis.

An abstract domain is a collection of abstract states propagated through the control flow graph by a dataflow analysis. At a program point, they are abstractions of the set of possible concrete states that may arise during any execution of the program.

In EVA, different abstract domains may communicate through alarms, values and locations. Alarms report undesirable behaviors that may occur during an execution of the program. They are defined in Alarmset, while values and locations depend on the domain. Values are numerical and non-relational abstractions of the set of the possible values of expressions at a program point. Locations are similar abstractions for memory locations. The main values and locations used in the analyzer are respectively available in Main_values and Main_locations. Values and locations abstractions are extensible, should a domain requires new abstractions. Their signature are in Abstract_value.S and Abstract_location.S.

Lvalues and expressions are cooperatively evaluated into locations and values using all the information provided by all domains. These computed values and locations are then available for the domain transformers which model the action of statements on abstract states. However, a domain could ignore this mechanism; its values and locations should then be the unit type.

This file gathers the definition of the module types for an abstract domain.

The module type Abstract_domain.S requires all the functions to be implemented to define the abstract semantics of a domain, divided in three categories:

Abstract_domain.Lattice gives a semi-lattice structure to the abstract states;
Abstract_domain.Queries extracts information from a state, by giving a value to an expression.
Abstract_domain.Transfer are the transfer functions of the domain for assignments, assumptions and function calls. It is a functor from a Abstract_domain.Valuation module, which are maps containing all locations and values computed by the evaluation of the expressions involved in the considered statement.

The module type Abstract_domain.S_with_Structure is Abstract_domain.S, plus a special OCaml value describing the internal structure of the domain and identifying it. This structure enables automatic accessors to the domain when combined to others. See Structure for details. Abstract_domain.S_with_Structure is the interface to implement in order to introduce a now domain in EVA.

The module type Abstract_domain.Internal contains some other functionalities needed by the analyzer, but that can be automatically generated from the previous one. The functor Domain_builder.Complete produces an Abstract_domain.Internal module from a Abstract_domain.S_with_Structure one.

Abstract_domain.Internal modules can then be lifted on more general values and locations through Domain_lift.Make, and be combined through Domain_product.Make.

Finally, Abstract_domain.External is the type of the final modules built and used by EVA. It contains the generic accessors to specific domains, described in Abstract_domain.Interface.

module type Lattice = sig .. end

Lattice structure of a domain.

module type Queries = sig .. end

Extraction of information: queries for values or locations inferred by a domain about expressions and lvalues.

module type Valuation = sig .. end

Results of an evaluation: the results of all intermediate calculation (the value of each expression and the location of each lvalue) are cached in a map.

module type Transfer = sig .. end

Transfer function of the domain.

type 'state logic_environment = {

	`states : Cil_types.logic_label -> 'state;`	`(*`	`result` contains the variable corresponding to \result. It is None when \result is meaningless.	`*)`
	`result : Cil_types.varinfo option;`

}

Environment for the logical evaluation of predicates.

type init_value =

`\|`	`Zero`
`\|`	`Top`

Value for the initialization of variables. Can be either zero or top.

type init_kind =

`\|`	`Main_Formal`
`\|`	`Library_Global`
`\|`	`Spec_Return of Cil_types.kernel_function`

module type S = sig .. end

Signature for the abstract domains of the analysis.

type 'a key = 'a Structure.Key_Domain.k

Keys identify abstract domains through the type of their abstract values.

type 'a structure = 'a Structure.Key_Domain.structure =

`\|`	`Void : 'a0 structure`
`\|`	`Leaf : 'a1 key -> 'a1 structure`
`\|`	`Node : 'a2 structure * 'b structure -> ('a2 * 'b) structure`

Describes the internal structure of a domain. Used internally to automatically generate efficient accessors from a generic abstract domain, which may be a combination of several domains, to a specific one.

For a simple 'leaf' domain, the structure should be:

let key = Structure.Key_Domain.create_key "name_of_the_domain";;
      let structure = Leaf key;;

Then, the key should be exported by the domain, to allow the use of the functions defined in the Abstract_domain.Interface interface below.

A compound domain may use the Node constructor to provide a separate access to each of its parts.

A domain can also use the Void constructor to prevent access to itself.

module type S_with_Structure = sig .. end

Structure of a domain.

module type Interface = sig .. end

External interface of a domain, with accessors.

module type Store = sig .. end

Automatic storage of the states computed during the analysis.

module type Internal = sig .. end

Full implementation of domains.

module type External = sig .. end

Final interface of domains, as generated and used by EVA, with generic accessors for domains.