One distinctive feature of my static analysis tool, NStatic, is support for fast interprocedural analysis as demonstrated by this snapshot of the callstack window depicting a stack trace, eleven function calls deep. Note that this is a pre-release product, and anything I mention in this post is subject to change.
Interprocedural analysis is rare among static analysis tools because it can drastically slow down analysis of code; analysis tools that do this may run for days, making it impractical for frequent use. As a result, some tools like ESC/Java and Spec# perform modular analysis, which only examines a single function at a time.
These shortcomings limit the utility of the aforementioned tools. Therefore, I decided that a good solution requires a good treatment of interprocedural calls and took up the challenge.
I divided functions into two categories—simple and complex. Simple functions consist of expressions (including function calls), assignments, and if statements. Complex functions consists of looping constructs, gotos, and switches. I am considering moving switches to the former category. I didn’t based the functions on factors such as size or cyclomatic complexity, because my original criteria seems to work well in practice.
Simple functions are always traversed up to a large user-settable limit (default = 10). Properties, indexers and constructors typically fall into this category. The amount of time required to execute a simple function is probably similar to the amount of time that would transpired had the function call been bypassed.
Complex functions are traversed up to a small user-settable depth (default = 2). Each increment in the depth of the traversal typically doubles the scanning time. In such cases, it is usually better to simply evaluate the pre- and post-conditions of the function and invalidate any variable that could possibly be changed by the function call. Pre- and post- conditions are automatically deduced (or explicitly entered through asserts/specification) from the body of the function and also propagated through nested function calls. Contrast this with ESC/Java which requires the user to manually propagate annotations to each caller of a function.
Whether a function is traversed or bypassed, a full stack trace into and including the bypassed functions can still be built. Bypassing simply makes less information available for finding errors and causes the tool to proceed more conservatively.
In addition to regular methods, there is special handling for iterators, closures and interface/virtual methods. Virtual/interfaces methods and overrides are conceptually combined into one large function with nested if-else statements containing type-checks (ie, obj is type). Closures carry around frame information, and iterators called within foreach loops undergo a transformation in which the body of the foreach loop is passed as a closure to the iterator just as in Ruby.
To complete the story, static and instance constructors and field initializations are executed early, so that class invariants can be deduced and made available for analysis of normal methods. A topological sort of non-constructor methods also ensures condition and modification information of callee functions are available to caller functions, if any callee needs to be bypassed.