Unitgraph to SIBGraph Converter

From JETI FMICS Wiki
Jump to: navigation, search

soot2jabc – A tool to create control flow graphs from Java classes

From the Soot website:

"Soot is a Java optimization framework. It provides four intermediate representations for analyzing and transforming Java bytecode. [...] Soot can be used as a stand alone tool to optimize or inspect class files, as well as a framework to develop optimizations or transformations on Java bytecode."

Soot is capable of different source code representations (Baf, Jimple, Shimple and Grimp) which are internally converted into a so-called unit graph format which is then used as the basis for analysis and possible optimization of a given Java class. A unit (node) contained in these graphs is used for each of the statements of a method's body. Thus, one unit graph represents the control flow graph of a method.

More details on how Soot works and how it can be used via its API specification can be found on the Soot website and the API for Unit Graphs.

The soot2jabc tool takes a given Java class as its input file, lets Soot create the unitgraph representation of it and transforms this unitgraph into a JavaABC SIBGraph which e.g. allows for automatic verification of the resulting control flow graph via the GEAR model checker.


jETI integration

The integration of the converter with the jETI tool server is currently realized via remote usage of the command line interface. There is a page detailing the necessary steps to get the Unitgraph to SIBGraph converter working on a jETI tool server.


Support

The Unitgraph to SIBGraph Converter (soot2jabc) is maintained by Marco Bakera.