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 '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_start_of
.
type vertex = private {
vertex_kf : Cil_types.kernel_function;
vertex_key : int;
vertex_blocks : Cil_types.block list;
mutable vertex_start_of : Cil_types.stmt option;
mutable vertex_end_of : Cil_types.stmt list;
mutable vertex_info : vertex_info;
mutable vertex_control : vertex control;
}
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 'vertex edge = private {
edge_kf : Cil_types.kernel_function;
edge_key : int;
edge_kinstr : Cil_types.kinstr;
edge_transition : 'vertex transition;
edge_loc : Cil_types.location;
}
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
type automaton = {
graph : graph;
entry_point : vertex;
return_point : vertex;
exit_points : vertex list;
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 graphentry_point
: each execution of the function starts at this vertexreturn_point
: return statements link to this vertexexit_points
: each call to a non-returning function (declared with the C attribute "noreturn") leads to a vertex from this list, with no successorstmt_table
: this table links statements to their starting and ending vertex
module Automaton : Datatype.S with type t = automaton
Datatype for automata
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.
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
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
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.
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 (D : Domain) : DataflowAnalysis with type state = D.t
Forward dataflow analysis. The domain must provide a forward transfer
function that computes the state after a transition from the state before.
module BackwardAnalysis (D : Domain) : DataflowAnalysis with type state = D.t
Backward dataflow analysis. The domain must provide a backward transfer
function that computes the state before a transition from the state after.