SATIrE: Static Analysis Tool Integration Engine

SATIrE integrates components of different program analysis tools and offers an infrastructure for building new code analysis tools. The design of SATIrE allows to build arbitrary tool chains with the integrated tools and to add user-defined components. In its present release, it integrates

the Program Analyzer Generator (PAG) from AbsInt,
components of the LLNL-ROSE source-to-source infrastructure (e.g. the EDG C/C++ Front End),
Termite, a TERM Iteration and Transformation Environment,
and the SATIrE Term-Representation components for exporting and importing the SATIrE intermediate representation.

As a result of our effort in SATIrE the user only needs to provide as input:

A high-level specification of the analysis

to compile the analyzer. The generated SATIrE-analyzer uses the EDG Front End for parsing the C/C++ program and with the additional SATIrE modules the user has a number of command line options available to control the output of the analyzer and access program information available in the ROSE-IR. The output (after running the compiled analyzer on some C/C++ input file) can be:

A visualization of the interprocedural control flow graph with analysis results at nodes and edges (PAG output)
The analysis results added as comments to the original source code (by using ROSE's source-to-source transformation capabilities)
For debugging an analysis, a step-by-step animation of the analysis (PAG output)

For the advanced user the analysis results are available such that they can be used for building new analysis tools:

The analysis results are accessible as AST attributes (ROSE AST). A traversal is available for traversing the AST and accessing the pre- and post-info for each statement node in the ROSE AST.
The decorated AST can be printed into a PDF file where each thumbnail is one node in the AST (the tree structure showing the AST), and the values of the attributes are printed on each page.
SATIrE also provides mapping functions that allow to map label and expression information from the normalized AST, on which the analyzer operates on, back to the original ROSE-AST.
Multiple analyses can be combined by accessing AST attributes that have been computed by previous analyses (not necessarily performed by a PAG analyzer) from an analysis specification [under development, not all support modules are finished yet]

FAQ

An FAQ can be found here.

Authors

The authors of SATIrE Core Components are: Markus Schordan(2004+), Gergo Barany(2004+), Adrian Prantl(2007+), Viktor Pavlu(2007+).

Contributors of analyses, integrations, and auxiliary components are: Dietmar Schreiner (2009+), Mihai Ghete (2008), Christoph Bonitz (2006).

Download

Release Date	Version	ROSE	PAG	Comment on major SATIrE changes and extensions
2012-Mar-12	SATIrE 0.9.1	0.9.5a-18777+	9.0.0.92248	Integrated SATIrE into ROSE. SATIrE is now available as part of the ROSE distribution. Some small fixes to comply with the ROSE policies and supporting different GNU compiler versions and improvements of the configuration system; SATIrE can be accessed in ROSE in the src/projects/SATIrE directory; the README file explains how to configure SATIrE inside ROSE.
2012-Jan-11	SATIrE 0.9.0	0.9.5a	9.0.0.92248	Added 100+ pages documentation (manual.pdf (72 pages), termite.pdf (30 pages)); all major functionality is now accessible for exploration through the new satire_driver (64 command line options); new options for DOT visualization; Integrated Termite and TuBound Analyzers (see tools/loopbounds); provided are now a number of SATIrE analyzers (pointsto, interval, constprop,sl2rd); additional information about inteprocedural PAG contexts has been added (=readable representation of callstrings). All SATIrE components have been upgraded to ROSE 0.9.5a; new build system using libtool to create dynamic libraries.
2008-Nov-22	SATIrE 0.8.5	0.9.3a	9.0.0.92248	Experimental points-to/alias analysis: new options are --run-pointsto-analysis, --resolve-funcptr-calls (currently restricted to C); improved PAG analyzer integration architecture (analyzers are encapsulated as C++ objects now); using new features provided by PAG 9.0.0.92248, SATIrE's attributes, types, and auxiliary functions are now declared automatically; improved float/double support in Termite integration; experimental support for clang Frontend integration.
2008-Sep-26	SATIrE 0.8.4	0.9.3a	8.7.6.17	upgraded to ROSE 0.9.3a (build 1593), parallel builds with -j are fully supported now, improved handling of switch statements in ICFG (in particular Duff's device). Note: this version requires ROSE 0.9.3a.
2008-Aug-14	SATIrE 0.8.3	0.9.1a	8.7.6.17	Improved support for combined analyzers, the resolution of calls to static functions, and the resolution of static file-scope variables and their initializers. Added TypeId as abstract type identifier. Total ordering on each Id type. Improved scheme for temporary variables handling function calls and function returns. Added PAG specific command line options for tuning memory consumption of analyzers.
2008-May-30	SATIrE 0.8.2	0.9.1a	8.2.3.34	Added VariableId and ExpressionId. Extended annotation format and visualization to display VariableId, ExpressionId, and ICFG-ASTs. Replaced single ExternalCall node by ExternalCall/ExternalReturn pair. Performance improvements in SATIrE library speeding up analyzers.
2008-Apr-11	SATIrE 0.8.1	0.9.1a	7.7.5.50	tuned computation of expression and type sets - the ICFG builder is now roughly 5 to 10 times faster; added analyzer command line flag --no-number-expressions; added generation of GNUplot histograms for testsuite.
2008-Mar-11	SATIrE 0.8.0	0.9.0b	7.7.5.50	Changed and added command line options, added support for multiple input/output files, improved support for initializers, improved ICFG generation, added new tests.
2008-Feb-08	SATIrE 0.7.9	0.9.0b	7.3.8.55	Upgrade to ROSE 0.9.0b and PAG 7.3.8.55.
2008-Jan-24	SATIrE 0.7.8	0.8.10e	6.1.6.96	Added visualization of shape graphs and support for global variables.
2007-Nov-12	SATIrE 0.7.7	0.8.10e	6.1.6.96	Added shape analyses. Added option --wholeprogram to generated analyzer. Added option '-u' to command newanalysis.
2007-Oct-24	SATIrE 0.7.6	0.8.10e	6.1.6.96	Added the function expression and the parameter list to the ExternalCall constructor. Improved ICFG construction for logical expressions.
2007-Oct-16	SATIrE 0.7.5	0.8.10e	6.1.6.96	established use of GNU autotools for entire build process. Added Termite and option --termoutput to generated analyzer.
2007-Jul-15	SATIrE 0.7.4	0.8.10e	6.1.6.96	Upgraded SATIrE-ROSE interface from ROSE 0.8.8a to ROSE 0.8.10e; Removed ExpressionRoot in SATIrE-IR.
2007-May-22	SATIrE 0.7.3	0.8.8a	0.9.7.843d	Added command line options for generated analyzer: --language c++, --language c99
2007-May-10	SATIrE 0.7.2	0.8.8a	0.9.7.843d	Added support for syntactic lists in PAG specifications.
2007-Mar-20	SATIrE 0.7.1	0.8.8a	0.9.7.843d	Introduced command newanalysis for use with example analyses such that all support files are generated now.
2007-Mar-09	SATIrE 0.7.0	0.8.8a	0.9.7.843d	initial release