Applications of Data-Flow Analysis
- optimization
- correctness
Optimization
Brief list of data-flow analyses and their uses - from Tiger book, sav08, papers
Checks:
- initialization analysis
- protocol usage analysis
- array bounds checks
Some optimizations:
- common subexpression elimination using available expression analysis
- avoid recomputing (automatically or manually generated) identical expressions
- constant propagation
- use constants instead of variables if variable value is known
- copy propagation
- use another variable with the same name
- dead code elimination
- remove unnecessary code
- automatically generate code for parallel machines
Consider code:
x = complexComputationF(a.f,b.g); y = complexComputationG(c.f,d.g); z = x + y; c.f = e; u = complexComputationF(a.f,b.g);
Questions:
- can we compute complexComputationF and complexComputationG in parallel?
- does u compute same results as x ?
- what areas of memory do functions
- read
- write
- can a and c both refer to the same object?
- alias analysis
References:
- Tiger book, Chapter 17
- Automatic parallelization of divide and conquer algorithms by Radu Rugina and Martin Rinard
Correctness
ASTREE Analyzer
“In Nov. 2003, ASTRÉE was able to prove completely automatically the absence of any RTE in the primary flight control software of the Airbus A340 fly-by-wire system, a program of 132,000 lines of C analyzed in 1h20 on a 2.8 GHz 32-bit PC using 300 Mb of memory (and 50mn on a 64-bit AMD Athlon™ 64 using 580 Mb of memory).”
Some Commercial Tools
- Modular checking for buffer overflows in the large Brian Hackett, Manuvir Das, Daniel Wang, Zhe Yang
- Coverity Prevent
SAN FRANCISCO - January 8, 2008 - Coverity®, Inc., the leader in improving software quality and security, today announced that as a result of its contract with US Department of Homeland Security (DHS), potential security and quality defects in 11 popular open source software projects were identified and fixed. The 11 projects are Amanda, NTP, OpenPAM, OpenVPN, Overdose, Perl, PHP, Postfix, Python, Samba, and TCL.
- 7 April 2005. AbsInt contributes to guaranteeing the safety of the A380, the world's largest passenger aircraft.
The Analyzer is able to verify the proper response time of the control software of all components by computing the worst-case execution time (WCET) of all tasks in the flight control software. This analysis is performed on the ground as a critical part of the safety certification of the aircraft.