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.
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 |
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 ; |
}
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 = {
}
type 'vertex
transition =
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 =
val pretty_transition : vertex transition
Pretty_utils.formatter
type 'vertex
edge = private {
}
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
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 = {
}
module Automaton: Datatype.S
with type t = automaton
Datatype for automata
module WTO: sig
.. end
val get_automaton : Cil_types.kernel_function -> automaton
Get the interpreted automaton for the given kernel_function without annotations
Get the wto for the automaton of the given kernel_function
val get_wto : Cil_types.kernel_function -> 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 exit_strategy : graph ->
vertex Wto.component -> wto
Output the automaton in dot format
val output_to_dot : Pervasives.out_channel ->
?number:[ `Stmt | `Vertex ] ->
?wto:wto -> automaton -> unit
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
the components left and the components entered when going from
one index to another
val wto_index_diff : wto_index ->
wto_index ->
vertex list * vertex list
Returns the components left and the components entered when going from
one vertex to another
val get_wto_index_diff : Cil_types.kernel_function ->
vertex ->
vertex ->
vertex list * vertex list
Returns wether v
is a component head or not
val is_wto_head : Cil_types.kernel_function -> 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.
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.
This is mostly intended as an example for using interpreted automata;
see also tests/misc/interpreted_automata_dataflow.ml for a complete example
using this dataflow.
module type Domain = sig
.. end
Input domain for a simple dataflow analysis.
module Dataflow:
Builds a simple dataflow analysis over an input domain.