Module Interpreted_automata

module Interpreted_automata: sig .. end

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 = 
| NoneInfo
| LoopHead of int
type 'a control = 
| Edges (*

control flow is only given by vertex edges.

*)
| Loop of 'a (*

start of a Loop stmt, with breaking vertex.

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

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

*)
| Switch of {
   value : Cil_types.exp;
   cases : (Cil_types.exp * 'a) list;
   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_stmt. Currently, this statement is kept for two reasons: to know when callbacks should be called and when annotations should be read.

type vertex = private {
   vertex_key : int;
   mutable vertex_start_of : Cil_types.stmt option;
   mutable vertex_info : info;
   mutable vertex_control : vertex control;
}
type assert_kind = 
| Invariant
| Assert
| Check
| 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 = {
   kind : assert_kind;
   predicate : Cil_types.identified_predicate;
   labels : 'vertex labels;
   property : Property.t;
}
type 'vertex transition = 
| Skip
| Return of Cil_types.exp option * Cil_types.stmt
| Guard of Cil_types.exp * guard_kind * Cil_types.stmt
| Prop of 'vertex annotation * Cil_types.stmt
| Instr of Cil_types.instr * Cil_types.stmt
| Enter of Cil_types.block
| 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.

type guard_kind = 
| Then
| Else
val pretty_transition : vertex transition
Pretty_utils.formatter
type 'vertex edge = private {
   edge_key : int;
   edge_kinstr : Cil_types.kinstr;
   edge_transition : 'vertex transition;
   edge_loc : Cil_types.location;
}
val pretty_edge : vertex edge Pretty_utils.formatter
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 
type wto = vertex Wto.partition 

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

module Vertex: Datatype.S_with_collections  with type t = vertex

Datatype for vertices

module Edge: Datatype.S_with_collections  with type t = vertex edge

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 = {
   graph : graph;
   entry_point : vertex;
   return_point : vertex;
   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

val get_wto : Cil_types.kernel_function -> wto

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 = [ `Both | `Custom of Stdlib.Format.formatter -> 'a -> unit | `Stmt | `Vertex
]
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
val wto_index_diff : wto_index ->
wto_index ->
vertex list * vertex list
val get_wto_index_diff : Cil_types.kernel_function ->
vertex ->
vertex ->
vertex list * vertex list
val is_wto_head : Cil_types.kernel_function -> vertex -> bool
val is_back_edge : Cil_types.kernel_function ->
vertex * vertex -> bool
module Compute: sig .. end

This module defines the previous functions without memoization

module UnrollUnnatural: 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.

module type Domain = sig .. end

Input domain for a simple dataflow analysis.

module type DataflowAnalysis = sig .. end

Simple dataflow analysis

module ForwardAnalysis: 
functor (D : Domain-> DataflowAnalysis with type state = D.t

Forward dataflow analysis.

module BackwardAnalysis: 
functor (D : Domain-> DataflowAnalysis with type state = D.t

Backward dataflow analysis.