package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Library
Module
Module type
Parameter
Class
Class type

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.

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct