Module CtrlDpds

module CtrlDpds: sig .. end

Lexical successors

Internal information about control dependencies

val dkey : Log.category

Lexical successors

module Lexical_successors: sig .. end

Compute a graph which provide the lexical successor of each statement s, ie.

Postdominators (with infine path extension)

module PdgPostdom: sig .. end

This backward dataflow implements a variant of postdominators that verify the property P enunciated in bts 963: a statement postdominates itself if and only it is within the main path of a syntactically infinite loop.

Compute information needed for control dependencies

type t = Lexical_successors.t * PdgPostdom.t

val compute : Cil_types.kernel_function ->
       Lexical_successors.t * PdgPostdom.t

Compute some information on the function in order to be able to compute the control dependencies later on

val pd_b_but_not_a : PdgPostdom.t ->
       Cil_types.stmt -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t

Compute the PDB(A,B) set used in the control dependencies algorithm. Roughly speaking, it gives

({B} U postdom(B))-postdom(A)

. It means that if S is in the result, it postdominates B but not A. As B is usually a successor of A, it means that S is reached if the B-branch is chosen, but not necessary for the other branches. Then, S should depend on A. (see the document to know more about the applied algorithm)

Control dependencies

val get_if_controled_stmts : 'a * PdgPostdom.t -> Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t

Compute the list of the statements that should have a control dependency on the given IF statement.
Returns the statements which are depending on the condition.

= U (PDB (if, succs(if))

(see the document to know more about the applied algorithm).

val jump_controled_stmts : PdgPostdom.t ->
       Cil_types.stmt ->
       Cil_types.stmt -> Cil_datatype.Stmt.Hptset.elt -> Cil_datatype.Stmt.Hptset.t

val get_jump_controled_stmts : Lexical_successors.t * PdgPostdom.t ->
       Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t

let's find the statements which are depending on the jump statement (goto, break, continue) =

PDB(jump,lex_suc) U (PDB(lex_suc,label) - lex_suc)

(see the document to know more about the applied algorithm).

Compute the list of the statements that should have a control dependency on the given jump statement. This statement can be a goto of course, but also a break, a continue, or even a loop because CIL transformations make them of the form

while(true) body;

which is equivalent to

L : body ; goto L;

val get_loop_controled_stmts : Lexical_successors.t * PdgPostdom.t ->
       Cil_types.stmt -> Cil_datatype.Stmt.Hptset.t

Try to process while(1) S; LS: as L: S; goto L; LS: