module Cil2cfg:sig
..end
abstract type of a cfg
val dkey : Log.category
val debug : ('a, Format.formatter, unit) Pervasives.format -> 'a
val debug2 : ('a, Format.formatter, unit) Pervasives.format -> 'a
type
block_type =
| |
Bstmt of |
| |
Bthen of |
| |
Belse of |
| |
Bloop of |
| |
Bfct |
Be careful that only Bstmt are real Block statements
type
call_type =
| |
Dynamic of |
| |
Static of |
val pp_call_type : Format.formatter -> call_type -> unit
type
node_type =
| |
Vstart |
|||
| |
Vend |
|||
| |
Vexit |
|||
| |
VfctIn |
|||
| |
VfctOut |
|||
| |
VblkIn of |
|||
| |
VblkOut of |
|||
| |
Vstmt of |
|||
| |
Vcall of |
|||
| |
Vtest of |
(* |
bool=true for In and false for Out
| *) |
| |
Vswitch of |
|||
| |
Vloop of |
(* |
boolean is is_natural. None means the node has not been detected
as a loop
boolean is is_natural. None means the node has not been
detected as a loop. | *) |
| |
Vloop2 of |
type
node_info = {
|
kind : |
|
mutable reachable : |
typenode =
node_info
val node_type : node_info -> node_type
val bkind_stmt : block_type -> Cil_types.stmt option
val _bkind_sid : block_type -> int
typenode_id =
int * int
val node_type_id : node_type -> node_id
val node_id : node_info -> node_id
val pp_bkind : Format.formatter -> block_type -> unit
val pp_node_type : Format.formatter -> node_type -> unit
val same_node : node_info -> node_info -> bool
module VL:sig
..end
val pp_node : Format.formatter -> node_info -> unit
val start_stmt_of_node : node_info -> Cil_types.stmt option
val node_stmt_opt : node_info -> Cil_types.stmt option
val node_stmt_exn : node_info -> Cil_types.stmt
type
edge_type =
| |
Enone |
(* |
normal edge
| *) |
| |
Ethen |
(* |
then branch : edge source is a Vtest
| *) |
| |
Eelse |
(* |
else branch : edge source is a Vtest
| *) |
| |
Eback |
(* |
back edge to a loop : the edge destination is a Vloop
| *) |
| |
EbackThen |
(* |
Eback + Ethen
| *) |
| |
EbackElse |
(* |
Eback + Eelse
| *) |
| |
Ecase of |
(* |
switch branch : edge source is a Vswitch.
Ecase [] for default case
| *) |
| |
Enext |
(* |
not really a edge : gives the next node of a complex stmt
| *) |
module EL:sig
..end
module PMAP:
module MyGraph:Graph.Blocks.Make
(
PMAP
)
module CFG:sig
..end
module Eset:FCSet.Make
(
CFG.E
)
module Nset:FCSet.Make
(
CFG.V
)
module Ntbl:Hashtbl.Make
(
CFG.V
)
type
t = {
|
kernel_function : |
|
graph : |
|
spec_only : |
|
stmt_node : |
|
unreachables : |
|
loop_nodes : |
|
mutable loop_cpt : |
abstract type of a cfg
val new_cfg_env : bool -> Cil_types.kernel_function -> t
val cfg_kf : t -> Cil_types.kernel_function
val cfg_graph : t -> CFG.t
val cfg_spec_only : t -> bool
true
is this CFG is degenerated (no code available)val unreachable_nodes : t -> node_type list
typeedge =
CFG.E.t
val edge_type : CFG.E.t -> edge_type
val edge_src : CFG.E.t -> CFG.E.vertex
val edge_dst : CFG.E.t -> CFG.E.vertex
val pp_edge : Format.formatter -> CFG.E.t -> unit
val is_back_edge : CFG.E.t -> bool
val is_next_edge : CFG.E.t -> bool
val pred_e : t -> CFG.vertex -> CFG.E.t list
val succ_e : t -> CFG.vertex -> CFG.E.t list
typeedge_key =
int * int * int * int
val edge_key : CFG.E.t -> edge_key
val same_edge : CFG.E.t -> CFG.E.t -> bool
Enext
edgesval iter_nodes : (CFG.vertex -> unit) -> t -> unit
val fold_nodes : (CFG.vertex -> 'a -> 'a) -> t -> 'a -> 'a
val iter_edges : (CFG.E.t -> unit) -> t -> unit
val iter_succ : (CFG.E.vertex -> unit) -> t -> CFG.vertex -> unit
val fold_succ : (CFG.E.vertex -> 'a -> 'a) ->
t -> CFG.vertex -> 'a -> 'a
val fold_pred : (CFG.E.vertex -> 'a -> 'a) ->
t -> CFG.vertex -> 'a -> 'a
val _iter_succ_e : (CFG.E.t -> unit) -> t -> CFG.vertex -> unit
val iter_pred_e : (CFG.E.t -> unit) -> t -> CFG.vertex -> unit
val fold_pred_e : (CFG.E.t -> 'a -> 'a) -> t -> CFG.vertex -> 'a -> 'a
val fold_succ_e : (CFG.E.t -> 'a -> 'a) -> t -> CFG.vertex -> 'a -> 'a
val cfg_start : t -> CFG.V.t
val start_edge : t -> CFG.E.t
exception Found of node
val _find_stmt_node : t -> Cil_types.stmt -> node
val get_test_edges : t -> CFG.vertex -> CFG.E.t * CFG.E.t
similar to succ_e g v
but tests the branch to return (then-edge, else-edge)
Raises Invalid_argument
if the node is not a test.
val get_switch_edges : t ->
CFG.vertex ->
(Cil_types.exp list * CFG.E.t) list * CFG.E.t
succ_e g v
but give the switch cases and the default edgeval get_call_out_edges : t -> CFG.vertex -> CFG.E.t * CFG.E.t
succ_e g v
but gives the edge to VcallOut first and the edge to Vexit second.val get_edge_labels : CFG.E.t -> Clabels.c_label list
val next_edge : t -> CFG.vertex -> CFG.E.t
val node_after : t -> CFG.vertex -> CFG.E.vertex
Not_found
when the node after has been removed (unreachable)val get_pre_edges : t -> CFG.vertex -> CFG.E.t list
val get_post_edges : t -> CFG.vertex -> CFG.E.t list
val get_exit_edges : t -> CFG.V.t -> CFG.E.t list
e
that goes to the Vexit
node inside the statement
begining at node n
val add_edges_before : t ->
CFG.V.t -> Eset.t -> CFG.E.t -> Eset.t
val get_internal_edges : t -> CFG.vertex -> CFG.E.t list * Eset.t
e
of the statement node n
postcondition
and the set of edges that are inside the statement (e
excluded).
For instance, for a single statement node, e
is succ_e n
,
and the set is empty. For a test node, e
are the last edges of the 2
branches, and the set contains all the edges between n
and the e
edges.
val get_edge_next_stmt : t -> CFG.E.t -> Cil_types.stmt option
val get_post_logic_label : t -> CFG.vertex -> Cil_types.logic_label option
val blocks_closed_by_edge : t -> CFG.E.t -> Cil_types.block list
val has_exit : t -> bool
module type HEsig =sig
..end
module HE:
val add_node : t -> node_type -> CFG.V.t
val change_node_kind : t -> CFG.vertex -> node_type -> CFG.V.t
val add_edge : t ->
CFG.E.vertex -> edge_type -> CFG.E.vertex -> unit
val remove_edge : t -> CFG.E.t -> unit
val insert_loop_node : t -> CFG.vertex -> node_type -> CFG.V.t
val init_cfg : bool ->
Cil_types.kernel_function -> t * CFG.V.t * CFG.V.t
val get_node : t -> node_type -> CFG.V.t
val setup_preconditions_proxies : Cil_types.exp -> unit
e_kf
, when possibleval get_call_type : Cil_types.exp -> call_type
val get_stmt_node : t -> Cil_types.stmt -> CFG.V.t
cfg_stmt
. It is important that the created node
is the same than while the 'normal' processing ! That is why
this pattern matching might seem redondant with the other one.val cfg_stmts : t -> Cil_types.stmt list -> CFG.V.t -> CFG.V.t
stmts
, connect the last one with next
,
and return the node of the first stmt.val cfg_block : t ->
block_type ->
Cil_types.block -> CFG.E.vertex -> CFG.V.t
val cfg_switch : t ->
Cil_types.stmt ->
Cil_types.exp ->
Cil_types.block ->
Cil_types.stmt list -> CFG.E.vertex -> CFG.V.t
val cfg_stmt : t -> Cil_types.stmt -> CFG.V.t -> CFG.V.t
val clean_graph : t -> t
Below, we use an algorithm from the paper :
"A New Algorithm for Identifying Loops in Decompilation"
of Tao Wei, Jian Mao, Wei Zou, and Yu Chen,
to gather information about the loops in the builted CFG.
module type WeiMaoZouChenInput =sig
..end
module WeiMaoZouChen:
module LoopInfo:sig
..end
module Mloop:WeiMaoZouChen
(
LoopInfo
)
module HEloop:HE
(
sig
typet =
Cil2cfg.Nset.t
end
)
val set_back_edge : CFG.E.t -> unit
val mark_loops : LoopInfo.graph -> t
val loop_nodes : t -> node list
val strange_loops : t -> node list
mark_loops
). Must be empty in the mode
-wp-no-invariants
. (see also very_strange_loops
)val very_strange_loops : t -> node list
mark_loops
). At the moment, we are not able to handle those
loops.val cfg_from_definition : Kernel_function.t -> Cil_types.fundec -> t
val cfg_from_proto : Cil_types.kernel_function -> t
module Printer:
typepp_edge_fun =
Format.formatter -> edge -> unit
val export : file:string ->
?pp_edge_fun:(Format.formatter -> CFG.E.t -> unit) ->
t -> unit
val create : Kernel_function.t -> t
module KfCfg:Kernel_function.Make_Table
(
Datatype.Make
(
sig
include Datatype.Undefinedtypett =
Cil2cfg.t
typet =
tt
val name :string
val mem_project :(Project_skeleton.t -> bool) -> 'a -> bool
val reprs :t list
val equal :t -> t -> bool
val hash :t -> int
val compare :t -> t -> int
end
)
)
(
sig
val name :string
val dependencies :State.t list
val size :int
end
)
val get : KfCfg.key -> KfCfg.data
Log.FeatureRequest
for non natural loops and 'exception' stmts.