The GoblintCil.stmt datatype includes fields for intraprocedural control-flow information: the predecessor and successor statements of the current statement. This information is not computed by default. If you want to use the control-flow graph, or any of the extensions in this section that require it, you have to explicitly ask CIL to compute the CFG using one of these two methods:
The best way to compute the CFG is with the CFG module. Just invoke Cfg.computeFileCFG on your file. The Cfg API describes the rest of actions you can take with this module, including computing the CFG for one function at a time, or printing the CFG in dot form.
CIL can reduce high-level C control-flow constructs like switch and continue to lower-level gotos. This completely eliminates some possible classes of statements from the program and may make the result easier to analyze (e.g., it simplifies data-flow analysis).
You can invoke this transformation on the command line with --domakeCFG or programatically with GoblintCil.prepareCFG. After calling Cil.prepareCFG, you can use GoblintCil.computeCFGInfo to compute the CFG information and find the successor and predecessor of each statement.
For a concrete example, you can see how cilly --domakeCFG transforms the following code (note the fall-through in case 1):
int foo (int predicate) {
int x = 0;
switch (predicate) {
case 0: return 111;
case 1: x = x + 1;
case 2: return (x+3);
case 3: break;
default: return 222;
}
return 333;
}
See the CIL output for this code fragment
The Dataflow module (click for the ocamldoc) contains a parameterized framework for forward and backward data flow analyses. You provide the transfer functions and this module does the analysis. You must compute control-flow information (Section 7.1) before invoking the Dataflow module.
The module Dominators contains the computation of immediate dominators. It uses the Dataflow module.
The module ptranal.ml contains two interprocedural points-to analyses for CIL: Olf and Golf. Olf is the default. (Switching from olf.ml to golf.ml requires a change in Ptranal and a recompiling cilly.)
The analyses have the following characteristics:
The analysis itself is factored into two components: Ptranal, which walks over the CIL file and generates constraints, and Olf or Golf, which solve the constraints. The analysis is invoked with the function Ptranal.analyze_file: Cil.file -> unit. This function builds the points-to graph for the CIL file and stores it internally. There is currently no facility for clearing internal state, so Ptranal.analyze_file should only be called once.
The constructed points-to graph supports several kinds of queries, including alias queries (may two expressions be aliased?) and points-to queries (to what set of locations may an expression point?).
The main interface with the alias analysis is as follows:
The precision of the analysis can be customized by changing the values of several flags:
In practice, the best precision/efficiency tradeoff is achieved by setting
Ptranal.no_sub = false Ptranal.analyze_mono = true Ptranal.smart_aliases = false
These are the default values of the flags.
There are also a few flags that can be used to inspect or serialize the results of the analysis.
If Ptranal.analyze_mono and Ptranal.no_sub are both true, this output is sufficient to reconstruct the points-to graph. One nice feature is that there is a pretty printer for recursive types, so the print routine does not loop.
The reachingdefs.ml module uses the dataflow framework and CFG information to calculate the definitions that reach each statement. After computing the CFG (Section 7.1) and calling computeRDs on a function declaration, ReachingDef.stmtStartData will contain a mapping from statement IDs to data about which definitions reach each statement. In particular, it is a mapping from statement IDs to a triple the first two members of which are used internally. The third member is a mapping from variable IDs to Sets of integer options. If the set contains Some(i), then the definition of that variable with ID i reaches that statement. If the set contains None, then there is a path to that statement on which there is no definition of that variable. Also, if the variable ID is unmapped at a statement, then no definition of that variable reaches that statement.
To summarize, reachingdefs.ml has the following interface:
The availexps.ml module uses the dataflow framework and CFG information to calculate something similar to a traditional available expressions analysis. After computeAEs is called following a CFG calculation (Section 7.1), AvailableExps.stmtStartData will contain a mapping from statement IDs to data about what expressions are available at that statement. The data for each statement is a mapping for each variable ID to the whole expression available at that point(in the traditional sense) which the variable was last defined to be. So, this differs from a traditional available expressions analysis in that only whole expressions from a variable definition are considered rather than all expressions.
The interface is as follows:
The liveness.ml module uses the dataflow framework and CFG information to calculate which variables are live at each program point. After computeLiveness is called following a CFG calculation (Section 7.1), LiveFlow.stmtStartData will contain a mapping for each statement ID to a set of varinfos for varialbes live at that program point.
The interface is as follows:
Also included in this module is a command line interface that will cause liveness data to be printed to standard out for a particular function or label.
The module deadcodeelim.ml uses the reaching definitions analysis to eliminate assignment instructions whose results are not used. The interface is as follows: