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 |
type 'a
control =
| |
Edges |
(* | control flow is only given by vertex edges. | *) |
||||||
| |
Loop of |
(* | start of a Loop stmt, with breaking vertex. | *) |
||||||
| |
If of |
(* | edges are guaranteed to be two guards `Then` else `Else` with the given condition and successor vertices. | *) |
||||||
| |
Switch of |
(* | 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 : |
|
mutable vertex_start_of : |
|
mutable vertex_info : |
|
mutable 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 : |
|
predicate : |
|
labels : |
|
property : |
}
type 'vertex
transition =
| |
Skip |
| |
Return of |
| |
Guard of |
| |
Prop of |
| |
Instr of |
| |
Enter of |
| |
Leave of |
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 : |
|
edge_kinstr : |
|
edge_transition : |
|
edge_loc : |
}
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
typegraph =
G.t
typewto =
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 : |
|
entry_point : |
|
return_point : |
|
stmt_table : |
}
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
typewto_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
v
is a component head or notval is_back_edge : Cil_types.kernel_function ->
vertex * vertex -> bool
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
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:
Forward dataflow analysis.
module BackwardAnalysis:
Backward dataflow analysis.