Frama-C:
Plug-ins:
Libraries:

Frama-C API - Interpreted_automata

An interpreted automaton is a convenient formalization of programs for abstract interpretation. It is a control flow graph where states are control point and edges are transitions. It keeps track of conditions on which a transition can be taken (guards) as well as actions which are computed when a transition is taken. It can then be interpreted w.r.t. the operational semantics to reproduce the behavior of the program or w.r.t. to the collection semantics to compute a set of reachable states.

This intermediate representation abstracts almost completely the notion of statement in CIL. Edges are either CIL expressions for guards, CIL instructions for actions or a return Edge. Thus, it saves the higher abstraction layers from interpreting CIL statements and from attaching guards to statement successors.

type info =
  1. | NoneInfo
  2. | LoopHead of int
type 'a control =
  1. | Edges
    (*

    control flow is only given by vertex edges.

    *)
  2. | Loop of 'a
    (*

    start of a Loop stmt, with breaking vertex.

    *)
  3. | If of {
    1. cond : Cil_types.exp;
    2. vthen : 'a;
    3. velse : 'a;
    }
    (*

    edges are guaranteed to be two guards `Then` else `Else` with the given condition and successor vertices.

    *)
  4. | Switch of {
    1. value : Cil_types.exp;
    2. cases : (Cil_types.exp * 'a) list;
    3. default : 'a;
    }
    (*

    edges are guaranteed to be issued from a `switch()` statement with the given cases and default vertices.

    *)

Control flow informations for outgoing edges, if any.

Vertices are control points. When a vertice is the *start* of a statement, this statement is kept in vertex_start_of. Currently, this statement is kept for two reasons: to know when callbacks should be called and when annotations should be read.

type vertex = private {
  1. vertex_kf : Cil_types.kernel_function;
  2. vertex_key : int;
  3. mutable vertex_start_of : Cil_types.stmt option;
  4. mutable vertex_info : info;
  5. mutable vertex_control : vertex control;
}
type assert_kind =
  1. | Invariant
  2. | Assert
  3. | Check
  4. | Assume
type 'vertex labels = 'vertex Cil_datatype.Logic_label.Map.t

Maps binding the labels from an annotation to the vertices they refer to in the graph.

type 'vertex annotation = {
  1. kind : assert_kind;
  2. predicate : Cil_types.identified_predicate;
  3. labels : 'vertex labels;
  4. property : Property.t;
}
type 'vertex transition =
  1. | Skip
  2. | Return of Cil_types.exp option * Cil_types.stmt
  3. | Guard of Cil_types.exp * guard_kind * Cil_types.stmt
  4. | Prop of 'vertex annotation * Cil_types.stmt
  5. | Instr of Cil_types.instr * Cil_types.stmt
  6. | Enter of Cil_types.block
  7. | Leave of Cil_types.block

Each transition can either be a skip (do nothing), a return, a guard represented by a Cil expression, a Cil instruction, an ACSL annotation or entering/leaving a block. The edge is annotated with the statement from which the transition has been generated. This is currently used to choose alarms locations.

and guard_kind =
  1. | Then
  2. | Else
type 'vertex edge = private {
  1. edge_kf : Cil_types.kernel_function;
  2. edge_key : int;
  3. edge_kinstr : Cil_types.kinstr;
  4. edge_transition : 'vertex transition;
  5. edge_loc : Cil_types.location;
}
module G : Graph.Sig.I with type V.t = vertex and type E.t = vertex * vertex edge * vertex and type V.label = vertex and type E.label = vertex edge
type graph = G.t

Weak Topological Order is given by a list (in topological order) of components of the graph, which are themselves WTOs

Datatype for vertices

Datatype for edges

An interpreted automaton for a given function is a graph whose edges are guards and commands and always containing two special nodes which are the entry point and the return point of the function. It also comes with a table linking Cil statements to their starting and ending vertex

type automaton = {
  1. graph : graph;
  2. entry_point : vertex;
  3. return_point : vertex;
  4. stmt_table : (vertex * vertex) Cil_datatype.Stmt.Hashtbl.t;
}
module Automaton : Datatype.S with type t = automaton

Datatype for automata

module WTO : sig ... end

Datatype for WTOs

val get_automaton : Cil_types.kernel_function -> automaton

Get the automaton for the given kernel_function without annotations

Get the wto for the automaton of the given kernel_function

val exit_strategy : graph -> vertex Wto.component -> wto

Extract an exit strategy from a component, i.e. a sub-wto where all vertices lead outside the wto without passing through the head.

type 'a labeling = [
  1. | `Stmt
  2. | `Vertex
  3. | `Both
  4. | `Custom of Stdlib.Format.formatter -> 'a -> unit
]
val output_to_dot : Stdlib.out_channel -> ?labeling:vertex labeling -> ?wto:wto -> automaton -> unit

Output the automaton in dot format

type wto_index = vertex list

the position of a statement in a wto given as the list of component heads

module WTOIndex : Datatype.S with type t = wto_index

Datatype for wto_index

val get_wto_index : Cil_types.kernel_function -> vertex -> wto_index
  • returns

    the wto_index for a statement

val wto_index_diff : wto_index -> wto_index -> vertex list * vertex list
  • returns

    the components left and the components entered when going from one index to another

val get_wto_index_diff : Cil_types.kernel_function -> vertex -> vertex -> vertex list * vertex list
  • returns

    the components left and the components entered when going from one vertex to another

val is_wto_head : Cil_types.kernel_function -> vertex -> bool
  • returns

    wether v is a component head or not

val is_back_edge : Cil_types.kernel_function -> (vertex * vertex) -> bool
  • returns

    wether v1,v2 is a back edge of a loop, i.e. if the vertex v1 is a wto head of any component where v2 is included. This assumes that (v1,v2) is actually an edge present in the control flow graph.

module Compute : sig ... end

This module defines the previous functions without memoization

module UnrollUnnatural : sig ... end

Could enter a loop only by head nodes

Generic versions of the algorithms on dataflow graphs

module Algorithms (G : Graph.Sig.G) : sig ... end
module Dot (V : sig ... end) (E : sig ... end) (G : Graph.Sig.G with type V.t = V.t and type E.t = V.t * E.t * V.t) : sig ... end

Dataflow computation: simple data-flow analysis using interpreted automata. See tests/misc/interpreted_automata_dataflow.ml for a complete example using this dataflow computation.

type 'a widening =
  1. | Fixpoint
    (*

    The analysis of the loop has reached a fixpoint.

    *)
  2. | Widening of 'a
    (*

    The analysis of the loop has not reached a fixpoint yet, and must continue through a new iteration with the given state, widened if termination requires it.

    *)
module type Domain = sig ... end

Input domain for a simple dataflow analysis.

module type DataflowAnalysis = sig ... end

Simple dataflow analysis

Forward dataflow analysis. The domain must provide a forward transfer function that computes the state after a transition from the state before.

Backward dataflow analysis. The domain must provide a backward transfer function that computes the state before a transition from the state after.