Module Eval

module Eval: sig .. end
Types and functions related to evaluations. Heavily used by abstract values and domains, evaluation of expressions, transfer functions of instructions and the dataflow analysis.


Types and functions related to evaluations. Heavily used by abstract values and domains, evaluation of expressions, transfer functions of instructions and the dataflow analysis.

Types and functions related to evaluations. Heavily used by abstract values and domains, evaluation of expressions, transfer functions of instructions and the dataflow analysis.

Lattice structure


include Bottom.Type
type 'a or_top = [ `Top | `Value of 'a ] 
For some functions, the special value top (denoting no information) is managed separately.

Types for the evaluations


type 't with_alarms = 't * Alarmset.t 
A type and a set of alarms.
type 't evaluated = 't or_bottom with_alarms 
Most forward evaluation functions return the set of alarms resulting from the operations, and a result which can be `Bottom, if the evaluation fails, or the expected value.
val (>>=) : 'a evaluated -> ('a -> 'b evaluated) -> 'b evaluated
This monad propagates the `Bottom value if needed, and join the alarms of each evaluation.
val (>>=.) : 'a evaluated -> ('a -> 'b or_bottom) -> 'b evaluated
Use this monad of the following function returns no alarms.
val (>>=:) : 'a evaluated -> ('a -> 'b) -> 'b evaluated
Use this monad if the following function returns a simple value.
type 'a reduced = [ `Bottom | `Unreduced | `Value of 'a ] 
Most backward evaluation function returns `Bottom if the reduction leads to an invalid state, `Unreduced if no reduction can be performed, or the reduced value.

Context for the evaluation of abstract value operators.
type unop_context = Cil_types.exp * Cil_types.exp 
Evaluation of unary operator: unop e1 = e2.
type binop_context = Cil_types.exp * Cil_types.exp * Cil_types.exp * Cil_types.typ 
Evaluation of binary operator: e1 binop e2 = e3.
type index_context = Cil_types.exp * Cil_types.offset * Cil_types.typ * Cil_types.exp option 
Evaluation of an index: index, remaining, typ pointed, array size expression

Cache for the evaluations



Cache for the evaluations



The evaluation of an expression stores in a cache the result of all intermediate computation. This cache is the outcome of the evaluation, and is used by abstract domains for transfer functions. It contains The evaluation queries the abstract domain the value of some sub-expressions.

The origin of an abstract value is then provided by the abstract domain, and kept in the cache. The origin is None if the value has been internally computed without calling the domain.

Also, a value provided by the domain may be reduced by the internal computation of the forward and backward evaluation. Such a reduction is tracked by the evaluator and reported to the domain, in the cache. States of reduction are:


type reductness = 
| Unreduced (*
No reduction.
*)
| Reduced (*
A reduction has been performed for this expression.
*)
| Created (*
The abstract value has been created.
*)
| Dull (*
Reduction is pointless for this expression.
*)
State of reduction of an abstract value.
type 'a flagged_value = {
   v : 'a;
   initialized : bool;
   escaping : bool;
}
Right values with 'undefined' and 'escaping addresses' flags.
type ('a, 'origin) record_val = {
   value : 'a or_bottom flagged_value; (*
The resulting abstract value
*)
   origin : 'origin option; (*
The origin of the abstract value
*)
   reductness : reductness; (*
The state of reduction.
*)
   val_alarms : Alarmset.t; (*
The emitted alarms during the evaluation.
*)
}
Data record associated to each evaluated expression.
type 'a record_loc = {
   loc : 'a; (*
The location of the left-value.
*)
   typ : Cil_types.typ; (*
*)
   loc_alarms : Alarmset.t; (*
The emitted alarms during the evaluation.
*)
}
Data record associated to each evaluated left-value.
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 Clear_Valuation: 
functor (Valuation : Valuation) -> sig .. end

Types of assignments


type 'loc left_value = {
   lval : Cil_types.lval;
   lloc : 'loc;
   ltyp : Cil_types.typ;
}
type 'value copied = 
| Determinate of 'value flagged_value (*
Determinates the right value before the copy: the copied value is initialized, and without escaping addresses.
*)
| Exact of 'value or_bottom flagged_value (*
Exact copy of the right value, with possible indeterminateness (then, the value can be bottom).
*)
Copy of values.
type 'value assigned = 
| Assign of 'value (*
Default assignment of a value.
*)
| Copy of Cil_types.lval * 'value copied (*
Used when the right expression of an assignment is a left value. Copy the location of the lvalue lval, that contains the value value copied. The copy can remove or not the possible indeterminateness of the value (according to the parameters of the analysis).
*)
Assigned values.
val value_assigned : 'value assigned -> 'value or_bottom

Interprocedural Analysis


type 'value argument = {
   formal : Cil_types.varinfo;
   concrete : Cil_types.exp;
   avalue : 'value assigned;
}
type 'value call = {
   kf : Cil_types.kernel_function;
   arguments : 'value argument list;
   rest : (Cil_types.exp * 'value assigned) list;
}
type ('state, 'summary, 'value) return = {
   post_state : 'state;
   returned_value : 'value or_bottom flagged_value option;
   summary : 'summary;
}
type ('state, 'summary, 'value) call_result = ('state, 'summary, 'value) return list or_bottom 
type 't init = 
| Default (*
The entry point is initialized to top, and all the others to bottom.
*)
| Continue of 't (*
The entry point is initialized to the current value, and all the others to bottom.
*)
| Custom of (Cil_types.stmt * 't) list (*
Custom association list for the initial values of statements. Other statements are initialized to bottom.
*)
Initialization of a dataflow analysis, by definig the initial value of each statement.
type ('state, 'summary, 'value) action = 
| Compute of 'state init * bool (*
Analyze the called function with the given initialization. If the summary of a previous analysis for this initialization has been cached, it will be used without re-computation. The second boolean indicates whether the result must be cached.
*)
| Recall of 'state init (*
Do not run the analysis of the function, but use the summary for this initialization if it exists. Otherwise, default_call is called.
*)
| Result of ('state, 'summary, 'value) call_result * Value_types.cacheable (*
Direct computation of the result.
*)
Action to perform on a call site.
exception InvalidCall