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.
include Bottom.Type
type'a
or_top =[ `Top | `Value of 'a ]
For some functions, the special value top (denoting no information) is managed separately.
type'a
or_top_or_bottom =[ `Bottom | `Top | `Value of 'a ]
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 = {
|
operand : |
Context for the evaluation of an unary operator: contains the involved expressions needed to create the appropriate alarms.
Context for the evaluation of an unary operator: contains the involved expressions needed to create the appropriate alarms.
type
binop_context = {
|
left_operand : |
|
right_operand : |
|
binary_result : |
Context for the evaluation of a binary operator: contains the expressions of both operands and of the result, needed to create the appropriate alarms.
Context for the evaluation of a binary operator: contains the expressions of both operands and of the result, needed to create the appropriate alarms.
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 : |
|
initialized : |
|
escaping : |
Right values with 'undefined' and 'escaping addresses' flags.
module Flagged_Value:sig
..end
type ('a, 'origin)
record_val = {
|
value : |
(* | The resulting abstract value | *) |
|
origin : |
(* | The origin of the abstract value | *) |
|
reductness : |
(* | The state of reduction. | *) |
|
val_alarms : |
(* | The emitted alarms during the evaluation. | *) |
Data record associated to each evaluated expression.
type 'a
record_loc = {
|
loc : |
(* | The location of the left-value. | *) |
|
typ : |
(* | *) |
|
|
loc_alarms : |
(* | 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:
type 'loc
left_value = {
|
lval : |
|
lloc : |
|
ltyp : |
type 'value
assigned =
| |
Assign of |
(* | Default assignment of a value. | *) |
| |
Copy of |
(* | Copy of the location of the lvalue | *) |
Assigned values.
val value_assigned : 'value assigned -> 'value or_bottom
type 'value
argument = {
|
formal : |
(* | The formal argument of the called function. | *) |
|
concrete : |
(* | The concrete argument at the call site | *) |
|
avalue : |
(* | The value of the concrete argument. | *) |
Argument of a function call.
type 'value
call = {
|
kf : |
(* | The called function. | *) |
|
arguments : |
(* | The arguments of the call. | *) |
|
rest : |
(* | Extra-arguments. | *) |
|
return : |
(* | Fake varinfo to store the return value of the call. | *) |
|
recursive : |
A function call.
type 'state
call_action =
| |
Compute of |
(* | Analyze the called function, starting with the given state at the entry-point. If the summary of a previous analysis for this initialization has been cached, it will be used without re-computation. | *) |
| |
Result of |
(* | Direct computation of the result. | *) |
Action to perform on a call site.