module Abstract_domain:sig
..end
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:
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. They are used when evaluating expressions.Abstract_domain.Transfer
are the transfer functions of the domain for assignments,
assumptions and function calls. These functions use the values and
locations computed by the evaluation of the expressions involved in
a given statement. These values and locations are made available through
a Abstract_domain.valuation
record.Mem_exec
cache.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.
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 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, External
is the type of the final modules built and used by Eva.
It contains the generic accessors to specific domains, described in
Interface
.
module type Lattice =sig
..end
module type Queries =sig
..end
type ('value, 'location, 'origin)
valuation = {
|
find : |
(* |
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 : |
(* | 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 : |
(* |
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.
| *) |
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
type 'state
logic_environment = {
|
states : |
(* | result contains the variable corresponding to \result. It is None when
\result is meaningless. | *) |
|
result : |
type
variable_kind =
| |
Global |
(* |
Global variable.
| *) |
| |
Formal of |
(* |
Formal parameter of a function.
| *) |
| |
Local of |
(* |
Local variable of a function.
| *) |
| |
Result of |
(* |
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 |
module type Reuse =sig
..end
module type S =sig
..end
module type Store =sig
..end
module type Internal =sig
..end
type't
key ='t Structure.Key_Domain.key
module type Leaf =sig
..end