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 vertex_info =
  1. | NoneInfo
  2. | LoopHead of {
    1. stmt : Cil_types.stmt;
    2. level : 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.

type vertex = private {
  1. vertex_kf : Cil_types.kernel_function;
  2. vertex_key : int;
  3. vertex_blocks : Cil_types.block list;
  4. mutable vertex_start_of : Cil_types.stmt option;
  5. mutable vertex_end_of : Cil_types.stmt list;
  6. mutable vertex_info : vertex_info;
  7. 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.G 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

type automaton = {
  1. graph : graph;
  2. entry_point : vertex;
  3. return_point : vertex;
  4. exit_points : vertex list;
  5. stmt_table : (vertex * vertex) Cil_datatype.Stmt.Hashtbl.t;
}

An interpreted automaton for a given function is a graph whose edges are guards and commands.

  • graph is the control flow graph
  • entry_point: each execution of the function starts at this vertex
  • return_point: return statements link to this vertex
  • exit_points: each call to a non-returning function (declared with the C attribute "noreturn") leads to a vertex from this list, with no successor
  • stmt_table: this table links statements to their starting and ending vertex
module Automaton : Datatype.S with type t = automaton

Datatype for automata

module WTO : Wto.S with type node = vertex

Datatype for WTOs

val build_automaton : annotations:bool -> Cil_types.kernel_function -> automaton

Build an interpreted automaton for the given kernel_function. If annotations is true, the automaton includes Prop transitions for assertions and loop invariants of the function body. Note that the automata construction may lead to the build of new Cil expressions which will be different at each call: you may need to memoize the results of this function.

val build_wto : ?pref:WTO.pref -> automaton -> wto

Build a wto for the given automaton. The pref function is a comparison function used to determine what is the best vertex to use as a Wto component head. See Wto.Make for more details.

val get_automaton : Cil_types.kernel_function -> automaton

Get the automaton for the given kernel_function. This is the memoized version of build_automaton ~annotations:false

val exit_strategy : automaton -> 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.

val output_to_dot : ?pp_vertex:vertex Pretty_utils.formatter -> ?pp_edge:vertex edge Pretty_utils.formatter -> ?wto:wto -> Stdlib.out_channel -> 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 : 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.

module type Graph = sig ... end

Generic control flow graphs

module MakeGraph (Vertex : Datatype.S_with_hashtbl) (Edge : Datatype.S) : Graph with type V.t = Vertex.t and type E.t = Vertex.t * Edge.t * Vertex.t and type V.label = Vertex.t and type E.label = Edge.t and module VTable = Vertex.Hashtbl

This functor can be used to build generic control flow graphs

module UnrollUnnatural : sig ... end

Control flow graphs where unnatural loops are modified such that all paths entering a loop enters it by its head.