Previous  Up  Next

Module Build

module Build: sig .. end
Build graphs (PDG) for the function (see module 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))
set of nodes of the graph 
val pretty_node : ?key:bool -> Format.formatter -> PdgTypes.Node.t -> unit
val is_variadic : Kernel_function.t -> bool
type arg_nodes = PdgTypes.Node.t list 
type pdg_build = {
   fct : Cil_types.kernel_function;
   mutable topinput : PdgTypes.Node.t option;
   mutable other_inputs : (PdgTypes.Node.t * PdgTypes.Dpd.td * Locations.Zone.t) list;
   graph : PdgTypes.G.t;
   states : Pdg_state.states;
   index : PdgTypes.Pdg.fi;
   ctrl_dpds : BoolNodeSet.t Cil_datatype.Stmt.Hashtbl.t; (*
The nodes to which each stmt control-depend on. The links will be added in the graph at the end.
*)
   decl_nodes : PdgTypes.Node.t Cil_datatype.Varinfo.Hashtbl.t; (*
map between declaration nodes and the variables to build the dependencies.
*)
}
type of the whole PDG representation during its building process
val create_pdg_build : Kernel_function.t -> pdg_build
create an empty build pdg for the function
val _pretty : Format.formatter -> pdg_build -> unit
val add_elem : pdg_build -> PdgIndex.Key.t -> PdgTypes.Node.t
add a node to the PDG, but if it is associated with a stmt, check before if it doesn't exist already (useful for loops).
Returns the (new or old) node.
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
add a dependency with the given label between the two nodes. Pre : the nodes have to be already in pdg.
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
add a dependency on the variable declaration. The kind of the dependency is address if the variable appears in a lvalue, data otherwise.
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 state
val add_ctrl_dpds : pdg_build -> unit
Process and clear 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
Add a PDG node for each formal argument, and add its dependencies to the corresponding argument node.
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
creates a node for lval : caller has to add dpds about the right part
val add_from : pdg_build ->
       PdgTypes.data_state ->
       PdgTypes.data_state ->
       Locations.Zone.t -> bool * Locations.Zone.t -> PdgTypes.data_state
val process_call_output : pdg_build ->
       PdgTypes.data_state ->
       PdgTypes.data_state ->
       Cil_types.stmt ->
       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
mix between process_call_ouput and process_asgn
val process_skip : pdg_build -> 'a -> Cil_types.stmt -> 'b option
for skip statement : we want to add a node in the PDG in ordrer to be able to store information (like marks) about this statement later on
val process_asm : pdg_build -> 'a -> Cil_types.stmt -> 'b option
for asm: similar to process_skip, except that we emit a warning
val 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
The control dependencies are stored : they will be added at the end by 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
Add a node for a stmt that is a jump. Add control dependencies from this node to the nodes which correspond to the stmt list. Also add dependencies for the jump to the label. Don't use for jumps with data dependencies : use 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
like 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
add a node corresponding to the returned value.
val process_other_inputs : pdg_build -> PdgTypes.data_state
part of 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
to call then the building process is over : add the control dependencies in the graph.
Returns the real PDG that will be used later on.
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
gives needed informations about lval : = location + exact + dependencies + declarations
val process_asgn : pdg_build ->
       PdgTypes.data_state ->
       Cil_types.stmt ->
       Cil_types.lval -> Cil_types.exp -> PdgTypes.data_state option
process assignment 
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
Add a PDG node and its dependencies for each explicit call argument.
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
Add nodes for the call outputs, and add the dependencies according to from_table. To avoid mixing inputs and outputs, 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
process call : 
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
Add a node in the PDG for the conditional statement, and register the statements that are control-dependent on it.
val process_jump_stmt : pdg_build -> CtrlDpds.t -> Cil_types.stmt -> unit
let's add a node for e jump statement (goto, break, continue) and find the statements which are depending on it. Returns are not handled here, but in Build.process_return.
val process_loop_stmt : pdg_build -> CtrlDpds.t -> Cil_types.stmt -> unit
Loop are processed like gotos because CIL transforms them into 
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) -> 
functor (Fenv : Dataflows.FUNCTION_ENV) -> 
functor (Param : sig


val current_pdg : pdg_build


val ctrl_dpds_infos : CtrlDpds.t
end) -> sig .. end
exception Value_State_Top
val compute_pdg_for_f : Kernel_function.t -> PdgTypes.Pdg.t
Compute and return the PDG for the given function
val degenerated : bool -> Kernel_function.t -> PdgTypes.Pdg.t
val compute_pdg : Kernel_function.t -> PdgTypes.Pdg.t