Module type Dataflow.BackwardsTransfer

module type BackwardsTransfer = sig .. end

Interface to provide for a backward dataflow analysis.

val name : string

For debugging purposes, the name of the analysis

val debug : bool Pervasives.ref

Whether to turn on debugging

type t

The type of the data we compute for each block start. In many presentations of backwards data flow analysis we maintain the data at the block end. This is not easy to do with JVML because a block has many exceptional ends. So we maintain the data for the statement start.

val pretty : Format.formatter -> t -> unit

Pretty-print the state

val funcExitData : t

The data at function exit. Used for statements with no successors. This is usually bottom, since we'll also use doStmt on Return statements.

val combineStmtStartData : Cil_types.stmt ->
       old:t ->
       t -> t option

When the analysis reaches the start of a block, combine the old data with the one we have just computed. Return None if the combination is the same as the old data, otherwise return the combination. In the latter case, the predecessors of the statement are put on the working list.

val combineSuccessors : t ->
       t -> t

Take the data from two successors and combine it

val doStmt : Cil_types.stmt -> t Dataflow.action

The (backwards) transfer function for a branch. The

(Cil.CurrentLoc.get
      ())

is set before calling this. If it returns None, then we have some default handling. Otherwise, the returned data is the data before the branch (not considering the exception handlers)

val doInstr : Cil_types.stmt ->
       Cil_types.instr ->
       t -> t Dataflow.action

The (backwards) transfer function for an instruction. The (Cil.CurrentLoc.get ()) is set before calling this. If it returns None, then we have some default handling. Otherwise, the returned data is the data before the branch (not considering the exception handlers)

val filterStmt : Cil_types.stmt -> Cil_types.stmt -> bool

Whether to put this predecessor block in the worklist. We give the predecessor and the block whose predecessor we are (and whose data has changed)

val stmt_can_reach : Cil_types.stmt -> Cil_types.stmt -> bool

Must return true if ther is a path in the control-flow graph of the function from the first statement to the second. Used to choose a "good" node in the worklist.

Suggested use is let stmt_can_reach = Stmts_graph.stmt_can_reach kf, where kf is the kernel_function being analyzed; let stmt_can_reach _ _ = true is also correct, albeit less efficient
Since Oxygen-20120901

module StmtStartData: Dataflow.StmtStartData  with type data = t

For each block id, the data at the start.