Skip to content

Real-Time Static Analysis in Eclipse

December 22, 2009

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:

  1. 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.
  2. 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.
  3. 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.
  4. 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.

No comments yet

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: