Real-Time Static Analysis in Eclipse
This term, I had the pleasure of working with Elliott Baron on an independent study that focused on implementing static analyses with real-time and real-world constraints. Elliott was an intern at Red Hat during his professional experience year and became familiar with Eclipse and the CDT, so he developed a proof-of-concept static analysis for the Eclipse IDE. He has generated several blog posts about his work and just submitted a proposal for an EclipseCon presentation to share his efforts with the community.
Elliott implemented a variant of property simulation1 to demonstrate that a static analysis could be run within an IDE in near real-time (a few seconds) on C projects as large as Eclipse could handle. Eclipse provided an AST and control-flow graph. However, he needed to add support for control-flow order traversal of the code (to verify temporal properties) and support for merging execution states. The original paper used a theorem prover, but Elliott found that a straightforward boolean minimization and substitution of known values is enough for most real-world code.
Along the way, Elliott ran into several problems that lead to potential future work:
- The control flow generated by multiple returns or statements like break/continue/goto is difficult to support. Eclipse could use a standard set of traversals (control-flow and data-flow at a minimum) that handle these cases cleanly.
- Pointers are, of course, a problem. The analysis framework could use a fast pointer analysis algorithm that could generate (incrementally) rough points-to sets to be shared by all of the analyses in the framework.
- Elliott’s solution of merging execution states could be expanded to handle a wider set of conditions and then extracted to make it available to other analyses.
- Whole-program analysis isn’t always possible, but since Eclipse tracks whole projects, the analysis framework may be able to compute and store function summaries to provide support for context-insensitive whole-program analyses.
That’s a lot of work, but I think it would be well worth it. IDEs are in a fantastic position to provide real-time support (or close) to developer. They already provide suggestions and make local corrections in real-time. Now, with a few extra cores available to maintain the necessary structures (AST, CFG, points-to sets) in the background, static verifiers that aim to identify common errors (like MSR’s prefix and prefast) could be run quickly on demand.
1Das, M., Lerner, S., and Seigle, M. 2002. ESP: path-sensitive program verification in polynomial time. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (Berlin, Germany, June 17 – 19, 2002). PLDI ‘02. ACM, New York, NY, 57-68.
