3. CIL Plugins

The CIL Plugins/Modules found in the src/ directory perform static analysis and transformation of C files. The modules perform Control Flow Graph analysis to identify segments that can be extracted and also extract those segments. This is the largest part of the tool.

You can read more about CIL plugins in general here:

• C Intermediate Language
• CIL Plugin Skeleton

Finding Segments

The file findLoops.ml finds and records the segments of the program that can be extracted. We do so by finding "local loops" in the program. The loop is said to be local if its entry point is its exit point (or is followed immediately by, depending on how the CFG is defined).

The program first finds all the loops (nested or otherwise) and then tests each loop for locality. It is important to note that finding cycles using DFS may or may not yield all the loops if some loops are nested. We, therefore, use Tarjan's algorithm to find strongly connected components first. Each strongly connected component will contain the outermost loop and all of its children. We then remove the root to break the loop and perform Tarjan's recursively to identify all the nested loops.

The loops are labelled by sid of their root (see CIL documentation), which is later used for extraction. The sid is only guaranteed to be unique per function by CIL. This is a notable limitation, meaning that all helper functions containing nested elements should be inlined to avoid collisions. The tool does not enforce this. This can be resolved relatively easily in the future by storing the sid-s per function instead of per program.

goto is fully supported for this functionality.

This plugin can be used in two ways:

• Just printing the cycles
• Using in extract (see Extracting Segments section below)

To just print the cycles, you need to compile and run with countCFGnested.ml. See the Makefile for details.

Extracting Segments

This plugin relies on findLoops.ml described in the section above. tututil.ml from Zachary Anderson's CIL template is also used.

The file/CIL feature extractMLC.ml extracts the bodies of local cycles into separate functions. There is currently no support for Arrays, and dynamic memory was not tested. Pointers are generally supported, the extraction will only pass pointers into the extracted function when necessary, otherwise, a copy will be passed.

The extraction process is performed recursively until all the bodies are extracted, non-local loops are left as is. This is because non-local loops cannot be extracted.

goto is not supported as the root of a loop, but is supported as an exit or otherwise inside the loop body.

The program will print the original line of code and the parent of each extracted function. This output is used by the verification tool.

To run this plugin, compile and run extractMLC, see the Makefile for details.

Utils

findFuncs.ml is a utility used by the verification tool to get specified information about the functions in the program.

The requested command is passed via an environment variable (this is because cilly does not support passing custom command-line arguments to plugins)

The command must be set to the FIND_COMMAND environment variable. The available commands are

• GET_ASSERT_FUNCS prints all functions with CBMC's CPROVER calls
• GET_ALL_FUNCS prints all functions
• GET_PARENTS prints the caller of each function. If two functions call the same function, there will be a print per each caller.
• GET_FUNC Prints the desired function. Requires FUN_NAME to be set with the function name. For debugging purposes only.

To run this plugin, compile and run findFuncs, see the make file for details.