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 four categories:

The functor Domain_builder.Complete automatically builds some of the functions required by the Abstract_domain.S signature. However, these functions can also be redefined in the domain to achieve better precision or performance.

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

Finally, a new domain can be registered in the Eva engine via Abstractions.register. See abstractions.mli for more details.

module type Lattice = sig .. end

Lattice structure of a domain.

type evaluation_context = {
   root : bool; (*

Is the queried expression the "root" expression being evaluated, or is it a sub-expression?

*)
   subdivision : int; (*

Maximum number of subdivisions for the current evaluation. See Subdivided_evaluation for more details.

*)
   subdivided : bool; (*

Is the current evaluation a subdivision of the complete evaluation?

*)
}

Context from the engine evaluation about a domain query.

module type Queries = sig .. end

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

type ('value, 'location, 'origin) valuation = {
   find : Cil_types.exp -> ('value, 'origin) Eval.record_val Eval.or_top; (*

Finds the value computed for an expression. The returned record also contains the origin provided by the domain for the given expression, the alarms emitted by its evaluation and whether its value has been reduced. Returns `Top if the expression has not been evaluated.

*)
   fold : 'a.
(Cil_types.exp -> ('value, 'origin) Eval.record_val -> 'a -> 'a) ->
'a -> 'a
;
(*

fold f a computes (f eN rN ... (f e1 r1 a)...), where e1 ... eN are the evaluated (sub)expressions and r1 ... rN are the computed records for each of these expressions. The record of an expression contains its value, reduction status, origin and alarms.

*)
   find_loc : Cil_types.lval -> 'location Eval.record_loc Eval.or_top; (*

Finds the location computed for an lvalue. The returned record also contains the lvalue type and the alarms emitted by its evaluation. Returns `Top if the lvalue has not been evaluated.

*)
}

Results of an evaluation: the results of all intermediate calculation (the value of each (sub)expression and the location of each lvalue) are available to the domain. As the evaluation results into a mapping from exp to record_val and from lval to record_loc, we define as Abstract_domain.valuation the classic functions to retrieve information from a map.

module type Transfer = sig .. end

Transfer function of the domain.

type 'state logic_environment = {
   states : Cil_types.logic_label -> 'state; (*

The logic can refer to the states at other points of the program using labels. states associates a state (which can be top) to each label.

*)
   result : Cil_types.varinfo option; (*

result contains the variable corresponding to \result. It is None when \result is meaningless.

*)
}

Environment for the logical evaluation of predicates.

type variable_kind = 
| Global (*

Global variable.

*)
| Formal of Cil_types.kernel_function (*

Formal parameter of a function.

*)
| Local of Cil_types.kernel_function (*

Local variable of a function.

*)
| Result of Cil_types.kernel_function (*

Special variable storing the return value of a call. Assigned at the end of the called function, and used at the call site. Also used to model the ACSL \result construct.

*)
type init_value = 
| Zero
| Top

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

module type Reuse = sig .. end

MemExec is a global cache for the complete analysis of functions.

module type S = sig .. end

Signature for the abstract domains of the analysis.

type 't key = 't Structure.Key_Domain.key 
module type Leaf = sig .. end

Signature for a leaf module of a domain.