Frama-C:
Plug-ins:
Libraries:

Frama-C API - Eval

type lval = Eva_ast.lval
type lhost = Eva_ast.lhost
type exp = Eva_ast.exp

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 module type of Frama_c_kernel.Lattice_bounds
type 'a or_bottom = [
  1. | `Value of 'a
  2. | `Bottom
]
type 'a or_top = [
  1. | `Value of 'a
  2. | `Top
]
type 'a or_top_bottom = [
  1. | `Value of 'a
  2. | `Bottom
  3. | `Top
]
module Bottom : sig ... end
module Top : sig ... end
module TopBottom : sig ... end
include module type of Bottom.Operators
val (>>-) : 'a Bottom.t -> ('a -> 'b Bottom.t) -> 'b Bottom.t
val (let*) : 'a Bottom.t -> ('a -> 'b Bottom.t) -> 'b Bottom.t
val (and*) : 'a Bottom.t -> 'b Bottom.t -> ('a * 'b) Bottom.t
val (>>-:) : 'a Bottom.t -> ('a -> 'b) -> 'b Bottom.t
val (let+) : 'a Bottom.t -> ('a -> 'b) -> 'b Bottom.t
val (and+) : 'a Bottom.t -> 'b Bottom.t -> ('a * 'b) Bottom.t

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.

module Evaluated : sig ... end
type 'a reduced = [
  1. | `Bottom
  2. | `Unreduced
  3. | `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.

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 abstract value of each sub-expression, as well as its origin (see below), its reduction (see below), and the alarms produced by its evaluation.
  • the abstract location of each lvalue of the expression, as well as its type, and the alarms produced by its dereference.

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:

  • Unreduced: the value provided by the domain could not be reduced;
  • Reduced: the value provided by the domain has been reduced;
  • Created: the domain has returned `Top for the given expression;
  • Dull: the domain was not queried for the given expression.
type reductness =
  1. | Unreduced
    (*

    No reduction.

    *)
  2. | Reduced
    (*

    A reduction has been performed for this expression.

    *)
  3. | Created
    (*

    The abstract value has been created.

    *)
  4. | Dull
    (*

    Reduction is pointless for this expression.

    *)

State of reduction of an abstract value.

type 'a flagged_value = {
  1. v : 'a or_bottom;
  2. initialized : bool;
  3. escaping : bool;
}

Right values with 'undefined' and 'escaping addresses' flags.

module Flagged_Value : sig ... end
type ('a, 'origin) record_val = {
  1. value : 'a flagged_value;
    (*

    The resulting abstract value

    *)
  2. origin : 'origin option;
    (*

    The origin of the abstract value

    *)
  3. reductness : reductness;
    (*

    The state of reduction.

    *)
  4. val_alarms : Alarmset.t;
    (*

    The emitted alarms during the evaluation.

    *)
}

Data record associated to each evaluated expression.

type 'a record_loc = {
  1. loc : 'a;
    (*

    The location of the left-value.

    *)
  2. 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 (Valuation : Valuation) : sig ... end

Types of assignments

type 'loc left_value = {
  1. lval : lval;
  2. lloc : 'loc;
}

Lvalue with its location and type.

type ('loc, 'value) assigned =
  1. | Assign of 'value
    (*

    Default assignment of a value.

    *)
  2. | Copy of 'loc left_value * 'value flagged_value
    (*

    Copy of the location of a lvalue, that contains the given flagged value. The value is copied exactly, with possible indeterminateness.

    *)

Assigned values.

val value_assigned : ('loc, 'value) assigned -> 'value or_bottom
type 'location location_or_address =
  1. | Location of 'location
  2. | Address of Frama_c_kernel.Cil_types.varinfo

The location of a logic dependency:

  • the memory location of <lval> for a clause "\from lval" (default case).
  • the address of x in case of a clause "\from &x". 
type 'location logic_dependency = {
  1. term : Frama_c_kernel.Cil_types.identified_term;
    (*

    The ACSL term of the dependency, expressed in a \from clause.

    *)
  2. direct : bool;
    (*

    Whether the dependency is direct (default case), or has been declared as "indirect", meaning that its value is only used in a conditional or to compute an address.

    *)
  3. location : 'location location_or_address;
    (*

    The memory location of the dependency.

    *)
}

The logic dependency of an ACSL assigns clause.

type 'location logic_assign =
  1. | Assigns of Frama_c_kernel.Cil_types.identified_term * 'location logic_dependency list
    (*

    assigns clause, with the dependencies of the \from clause. An empty list means \nothing.

    *)
  2. | Allocates of Frama_c_kernel.Cil_types.identified_term
  3. | Frees of Frama_c_kernel.Cil_types.identified_term

Interprocedural Analysis

type ('loc, 'value) argument = {
  1. formal : Frama_c_kernel.Cil_types.varinfo;
    (*

    The formal argument of the called function.

    *)
  2. concrete : exp;
    (*

    The concrete argument at the call site

    *)
  3. avalue : ('loc, 'value) assigned;
    (*

    The value of the concrete argument.

    *)
}

Argument of a function call.

type ('loc, 'value) call = {
  1. kf : Frama_c_kernel.Cil_types.kernel_function;
    (*

    The called function.

    *)
  2. callstack : Callstack.t;
    (*

    The current callstack (with this call on top).

    *)
  3. arguments : ('loc, 'value) argument list;
    (*

    The arguments of the call.

    *)
  4. rest : (exp * ('loc, 'value) assigned) list;
    (*

    Extra-arguments.

    *)
  5. return : Frama_c_kernel.Cil_types.varinfo option;
    (*

    Fake varinfo to store the return value of the call. Same varinfo for every call to a given function.

    *)
}

A function call.

val position_of_call : ('a, 'b) call -> Position.t

position_of_call call creates the global or local position from the call information call. If this is the entry point of the analysis (i.e. the callsite is Kglobal) then the position will be a root call. If there is a statement callsite then the position will be local.

type recursion = {
  1. depth : int;
    (*

    Depth of the recursive call, i.e. the number of previous call to the called function in the current callstack.

    *)
  2. substitution : (Frama_c_kernel.Cil_types.varinfo * Frama_c_kernel.Cil_types.varinfo) list;
    (*

    List of variables substitutions to be performed by the domains: for each pair, the first variable must be replaced by the second one in the domain state.

    *)
  3. base_substitution : Frama_c_kernel.Base.substitution;
    (*

    Same substitution as the previous field, for bases.

    *)
  4. withdrawal : Frama_c_kernel.Cil_types.varinfo list;
    (*

    List of variables to be temporary removed from the state at the start of a new recursive call (by the function start_call of the abstract domains), or to be put back in the state at the end of a recursive call (by the function finalize_call of the abstract domains).

    *)
  5. base_withdrawal : Frama_c_kernel.Base.Hptset.t;
    (*

    Same withdrawal as the previous field, for bases.

    *)
}

Information needed to interpret a recursive call. The local variables and formal parameters of different recursive calls should not be mixed up. Those of the current call must be temporary withdraw or replaced from the domain states before starting the new recursive call, and the inverse transformation must be made at the end of the call.

type cacheable =
  1. | Cacheable
    (*

    Functions whose result can be safely cached.

    *)
  2. | NoCache
    (*

    Functions whose result should not be cached, but for which the caller can still be cached. Typically, functions printing something during the analysis.

    *)
  3. | NoCacheCallers
    (*

    Functions for which neither the call, neither the callers, can be cached.

    *)

Can the results of a function call be cached with memexec?