module Build:sig
..end
Build.BuildPdg
)
to represente the dependencies between instructions
in order to use it for slicing purposes.
A function is processed using a forward dataflow analysis
(see module Dataflow2
which is instanciated with the module
Build.Computer
below).
val dkey : Log.category
val debug : ('a, Format.formatter, unit) Pervasives.format -> 'a
val debug2 : ('a, Format.formatter, unit) Pervasives.format -> 'a
exception Err_Bot of string
module BoolNodeSet:FCSet.Make
(
Datatype.Pair
(
Datatype.Bool
)
(
PdgTypes.Node
)
)
val pretty_node : ?key:bool -> Format.formatter -> PdgTypes.Node.t -> unit
val is_variadic : Kernel_function.t -> bool
typearg_nodes =
PdgTypes.Node.t list
type
pdg_build = {
|
fct : |
|||
|
mutable topinput : |
|||
|
mutable other_inputs : |
|||
|
graph : |
|||
|
states : |
|||
|
index : |
|||
|
ctrl_dpds : |
(* | The nodes to which each stmt control-depend on. The links will be added in the graph at the end. | *) |
|
decl_nodes : |
(* | map between declaration nodes and the variables to build the dependencies. | *) |
val create_pdg_build : Kernel_function.t -> pdg_build
val _pretty : Format.formatter -> pdg_build -> unit
val add_elem : pdg_build -> PdgIndex.Key.t -> PdgTypes.Node.t
val decl_var : pdg_build -> Cil_datatype.Varinfo.Hashtbl.key -> PdgTypes.Node.t
val get_var_base : Locations.Zone.t -> Cil_types.varinfo option
val add_dpd_in_g : PdgTypes.G.t ->
PdgTypes.Node.t ->
PdgTypes.Dpd.td -> Locations.Zone.t option -> PdgTypes.Node.t -> unit
val add_z_dpd : pdg_build ->
PdgTypes.Node.t ->
PdgTypes.Dpd.td -> Locations.Zone.t option -> PdgTypes.Node.t -> unit
val add_ctrl_dpd : pdg_build -> PdgTypes.Node.t -> PdgTypes.Node.t -> unit
val add_decl_dpd : pdg_build ->
PdgTypes.Node.t -> PdgTypes.Dpd.td -> PdgTypes.Node.t -> unit
val add_decl_dpds : pdg_build ->
PdgTypes.Node.t -> PdgTypes.Dpd.td -> Cil_datatype.Varinfo.Set.t -> unit
val add_dpds : pdg_build ->
PdgTypes.Node.t ->
PdgTypes.Dpd.td -> PdgTypes.data_state -> Locations.Zone.t -> unit
add_dpds pdg v dpd_kind state loc
add 'dpd_kind' dependencies from node n to each element
which are stored for loc in stateval add_ctrl_dpds : pdg_build -> unit
pdg.ctrl_dpds
which contains a mapping between the
statements and the control dependencies that have to be added to the
statement nodes.
Because some jump nodes can vanish due to optimisations using the value
analysis, we can not rely on the transitivity of the dependencies.
So let's compute a transitive closure of the control dependencies.
The table gives : stmt -> ctrl dependency nodes of the statement.
So for each stmt, we have to find if some of its ctrl nodes
also have dependencies that have to be added to the stmt.
val process_declarations : pdg_build ->
formals:Cil_datatype.Varinfo.Hashtbl.key list ->
locals:Cil_datatype.Varinfo.Hashtbl.key list -> PdgTypes.data_state
val ctrl_call_node : pdg_build -> Cil_types.stmt -> PdgTypes.Node.t
val process_call_args : pdg_build ->
PdgTypes.data_state ->
Cil_types.stmt ->
(Locations.Zone.t * Cil_datatype.Varinfo.Set.t) list -> arg_nodes
val process_call_params : pdg_build ->
PdgTypes.data_state ->
Cil_types.stmt -> Kernel_function.t -> arg_nodes -> PdgTypes.data_state
val create_call_output_node : pdg_build ->
PdgTypes.data_state ->
Cil_types.stmt ->
PdgIndex.Key.t -> Locations.Zone.t -> Locations.Zone.t -> PdgTypes.Node.t
val create_lval_node : pdg_build ->
PdgTypes.data_state ->
PdgIndex.Key.t ->
l_loc:Locations.Zone.t ->
exact:bool ->
l_dpds:Locations.Zone.t ->
l_decl:Cil_datatype.Varinfo.Set.t -> PdgTypes.Node.t * PdgTypes.data_state
val add_from : pdg_build ->
PdgTypes.data_state ->
PdgTypes.data_state ->
Locations.Zone.t -> bool * Locations.Zone.t -> PdgTypes.data_state
val process_call_ouput : pdg_build ->
PdgTypes.data_state ->
PdgTypes.data_state ->
Cil_types.stmt ->
int ->
Locations.Zone.t ->
bool -> Locations.Zone.t -> Locations.Zone.t -> PdgTypes.data_state
val process_call_return : pdg_build ->
PdgTypes.data_state ->
PdgTypes.data_state ->
Cil_types.stmt ->
l_loc:Locations.Zone.t ->
exact:bool ->
l_dpds:Locations.Zone.t ->
l_decl:Cil_datatype.Varinfo.Set.t ->
r_dpds:Locations.Zone.t -> Locations.Zone.t -> PdgTypes.data_state
val process_skip : pdg_build -> 'a -> Cil_types.stmt -> 'b option
val process_asm : pdg_build -> 'a -> Cil_types.stmt -> 'b option
process_skip
, except that we emit a warningval add_label : pdg_build -> Cil_types.label -> Cil_types.stmt -> PdgTypes.Node.t
val process_stmt_labels : pdg_build -> Cil_types.stmt -> unit
val add_label_and_dpd : pdg_build ->
Cil_types.label -> Cil_types.stmt -> PdgTypes.Node.t -> unit
val add_dpd_goto_label : pdg_build -> PdgTypes.Node.t -> Cil_datatype.Stmt.t -> unit
val add_dpd_switch_cases : pdg_build -> PdgTypes.Node.t -> Cil_types.stmt list -> unit
val store_ctrl_dpds : pdg_build ->
PdgTypes.Node.t ->
((Cil_datatype.Stmt.Hashtbl.key -> unit) -> 'a -> 'b) ->
Datatype.Bool.t * 'a -> 'b
finalize_pdg
val mk_jump_node : pdg_build ->
Cil_types.stmt ->
Datatype.Bool.t * Cil_datatype.Stmt.Hptset.t -> PdgTypes.Node.t
val process_jump : pdg_build ->
Cil_types.stmt -> Datatype.Bool.t * Cil_datatype.Stmt.Hptset.t -> unit
process_jump_with_exp
instead !val process_jump_with_exp : pdg_build ->
Cil_types.stmt ->
Datatype.Bool.t * Cil_datatype.Stmt.Hptset.t ->
PdgTypes.data_state -> Locations.Zone.t -> Cil_datatype.Varinfo.Set.t -> unit
process_jump
but also add data dependencies on the datas and their
declarations. Use for conditional jumps and returns.val add_blk_ctrl_dpds : pdg_build ->
PdgIndex.Key.t -> Cil_datatype.Stmt.Hashtbl.key list -> unit
val process_block : pdg_build -> Cil_types.stmt -> Cil_types.block -> unit
val process_entry_point : pdg_build -> Cil_datatype.Stmt.Hashtbl.key list -> unit
val create_fun_output_node : pdg_build -> PdgTypes.data_state option -> Locations.Zone.t -> unit
val add_retres : pdg_build ->
PdgTypes.data_state ->
Cil_types.stmt ->
Locations.Zone.t -> Cil_datatype.Varinfo.Set.t -> PdgTypes.data_state
val process_other_inputs : pdg_build -> PdgTypes.data_state
finalize_pdg
: add missing inputs
and build a state with the new nodes to find them back when searching for
undefined zones.
(notice that now, they can overlap, for example we can have G and G.a)
And also deals with warning for uninitialized local variables.val finalize_pdg : pdg_build -> Function_Froms.froms option -> PdgTypes.Pdg.t
from_opt
: for undefined functions (declarations)val get_lval_infos : Cil_types.lval ->
Cil_types.stmt ->
Locations.Zone.t * bool * Locations.Zone.t * Cil_datatype.Varinfo.Set.t
lval
:
= location + exact + dependencies + declarationsval process_asgn : pdg_build ->
PdgTypes.data_state ->
Cil_types.stmt ->
Cil_types.lval -> Cil_types.exp -> PdgTypes.data_state option
lval = exp;Use the state at ki (before assign) and returns the new state (after assign).
val process_args : pdg_build ->
PdgTypes.data_state ->
Cil_types.stmt -> Cil_types.exp list -> arg_nodes
val call_ouputs : pdg_build ->
PdgTypes.data_state ->
PdgTypes.data_state ->
Cil_types.stmt ->
Cil_types.lval option ->
Function_Froms.froms -> Locations.Zone.t -> PdgTypes.data_state
in_state
is the input state
and new_state
the state to modify.
Process call outputs (including returned value)val process_call : pdg_build ->
PdgTypes.data_state ->
Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.exp -> Cil_types.exp list -> PdgTypes.data_state option
lvaloption = funcexp (argl);Use the state at ki (before the call) and returns the new state (after the call).
val process_condition : CtrlDpds.t ->
pdg_build ->
PdgTypes.data_state -> Cil_types.stmt -> Cil_types.exp -> unit
val process_jump_stmt : pdg_build -> CtrlDpds.t -> Cil_types.stmt -> unit
Build.process_return
.val process_loop_stmt : pdg_build -> CtrlDpds.t -> Cil_types.stmt -> unit
while(true) body;which is equivalent to
L : body ; goto L;There is a small difference because we have to detect the case where the
goto L;
would be unreachable (no real loop).
This is important because it might lead to infinite loop (see bst#787)val process_return : 'a ->
pdg_build ->
PdgTypes.data_state -> Cil_types.stmt -> Cil_types.exp option -> unit
return ret_exp;
is equivalent to out0 = ret_exp; goto END;
while a simple return;
is only a goto END;
.
Here, we assume that the Oneret analysis
was used, ie. that it is the only return of the function
and that it is the last statement. So, the goto
is not useful,
and the final state is stored to be used later on to compute the outputs.module Computer:functor (
Initial
:
sig
val initial :(Cil_types.stmt * PdgTypes.data_state) list
end
) ->
exception Value_State_Top
val compute_pdg_for_f : Kernel_function.t -> PdgTypes.Pdg.t
val degenerated : bool -> Kernel_function.t -> PdgTypes.Pdg.t
val compute_pdg : Kernel_function.t -> PdgTypes.Pdg.t