---

August 2011

Volume 26 Number 08

Cutting Edge - Static Code Analysis and Code Contracts

By Dino Esposito | August 2011

For many, it’s hard to believe that there was ever a time when you could print the entire source code of an application, read it from top to bottom and catch bugs or possible misbehavior. The complexity of modern software makes this approach impractical for humans—but not for some types of smart software, such as static-analysis tools. 

Static analysis of software consists of inferring the behavior of a piece of code from its instructions. A static-analysis tool conducts its examination of source code by progressively building a base of knowledge that it uses to prove statements and their output right or wrong. Static analysis doesn’t actually execute the code; it just reads lines and figures things out. What kind of things?

In general, static analysis can identify possible bugs in code as well as indicate how closely certain segments of code match expectations and specifications.

It has been known for some time—at least as far back as the great work done by Alan Turing in the 1930s—that there’s no automatic and completely reliable way to decide whether a given program will terminate without errors. In any case, computer science is mostly based on approximation, and being forewarned that you likely have a bug around some lines is a valuable help. Scale this help to the size of a modern project and you can see the real value. A static-analysis tool probably won’t give you absolute certainties but, working in real time as you write your classes, it can give you immediate feedback about what may be wrong in your implementation.

Static Analysis and Testing

There’s a fundamental difference between testing and static analysis. As a developer, you actively write the test but passively endure the static analysis. If your tests don’t actually cover significant conditions, or don’t check them with significant values, the results won’t be meaningful. A tool for static analysis gives you warnings about facts (as the tool understands them) that violate some of the configured internal rules. In general, getting nearly no warnings from static analysis is a good indication of the quality of the software. On the other hand, getting warnings doesn’t automatically mean your software is buggy and will fail at first run. Static analysis will likely detect hard-to-catch, corner-case errors that have the potential to crash your application. As with testing, static analysis can catch defects quite early in the development phase, thus limiting the impact of software errors on the overall project.

Types of Static Analyzers

Static analysis has many facets and a variety of different levels of implementation. A very basic type of static analyzer is the language compiler. The compiler goes through your source code and matches it to the syntax rules of the language. This is the first step of analysis. Modern compilers, however, do a lot more.

The latest C# compiler, for example, detects violations of the Liskov principle when you sum up Code Contracts in derived classes. This compiler can often point out occurrences of unused variables. However, what a compiler detects and classifies as a warning doesn’t necessarily qualify as a bug. Still, the compiler is a distinct step you have to execute. And it may take a while, depending on the project and the environment.

Tools like FxCop or, better yet, the Code Analysis feature in Visual Studio 2010, perform a more specific analysis of the code and can be configured to run either on demand or in each build, as Figure 1 shows.

Figure 1 Code Analysis Settings in a Visual Studio 2010 Project

Moreover, you can declaratively set the rules you want it to employ when processing your code. Figure 2 shows a sample of the long list of warnings you may receive when you enable the All Rules option in the Visual Studio 2010 Code Analysis. Note that some of those warnings are very specific, and very useful for making your code cleaner and more adherent to the Microsoft .NET Framework guidelines.

(click to zoom)

Figure 2 Warnings Received When All Rules Are Enabled

The key point about static analysis is that automatic tools are absolutely honest and give you warnings based strictly on violations of rules. Detected rule violations are not necessarily bugs; but if a violation is a bug, it likely will show in edge cases, and in full accordance with Murphy’s Law—just when it’ll do the most damage.

Besides on-demand tools like compilers and FxCop-like facilities, another category of tools can provide a lot of feedback for you—but they work asynchronously. To this category belongs ReSharper, which provides the same type of handy suggestions as Code Analysis, but dynamically as you type. It also offers to edit the code for you at the cost of a click or two. ReSharper detects, for example, unassigned variables, unreachable code, possible null references and a variety of code smells such as virtual calls in a constructor and access to modified closures in LINQ expressions. More importantly, ReSharper allows you to formalize your own code smells and automatically find and replace them intelligently as you type them. For more information and a detailed step-by-step example of the ReSharper structural search and replace, read the blog post at bit.ly/eCMvCL.

Finally, static analysis in the .NET Framework 4 and Visual Studio 2010 also takes place using the Static Checker tool created by the Code Contracts team.

Static Checker in Action

Along with Code Contracts, Microsoft provides the Static Checker tool, which can go through your code even without you compiling it and highlight Code Contracts not being verified or just impossible to prove right or wrong. You can get the Static Checker only if you have Visual Studio 2010 Premium or Ultimate or Visual Studio Team System 2008. These version requirements are in line with the requirements for the Code Analysis feature—that is, none of these features are available in Visual Studio Professional or Express editions.

Like the Intermediate Language rewriter, the Static Checker is a separate download that enhances Visual Studio 2010. You can get the latest Code Contracts bits from bit.ly/fF3wzl. You’ll need to explicitly enable Static Checking on a per-project configuration basis, as shown in Figure 3.

Figure 3 Enabling Static Checking of Code Contracts in Visual Studio 2010

The Static Checker can run in the background if you like, and can explicitly show squiggles for each warning. Background execution means that the Static Checker is scheduled to run in parallel with the compiler as a build happens and code is changed.

You can have the Static Checker look for implicit as well as explicit contracts. An explicit contract is any contract you declare in a class method, such as a precondition, a postcondition or an invariant. In addition, the Static Checker can also take into account some built-in Code Contracts and check whether array indexes always stay within array bounds, whether any null references are used or if any division by zero will occur. You control implicit Code Contracts through the checkboxes shown in Figure 3. Note that enabling implicit Code Contracts may flood your output window with a ton of messages and warnings. You might not want to do this all the time, and probably not after the beginning. Here’s an example of code that will be caught as a potential error when you have the Implicit Array Bounds Obligations contract on:

var numbers = new int[2];

numbers[3] = 0;

Most of the power of the Static Checker, though, results from using it with explicit contracts, such as preconditions and postconditions.

Explicit Contracts

Suppose you have the following code in one of your methods:

var orderId = GetLatestOrderId(); 

ProcessOrder(orderId);

A variable is obtained from a function call and then passed on to another method for further processing. There’s not much any Static Checker can do to try to prove these statements right or wrong without some explicit contract information. On the other hand, if the GetLatestOrderId method exposes a meaningful postcondition, as in the following code, the Checker might be able to prove whether the successive call is valid:

public int GetLatestOrderId()

{

  Contract.Ensures(Contract.Result<int>() >0);

  ...

  return n;

}

The GetLatestOrderId method explicitly declares it will be returning a value greater than zero. As the Checker makes its pass, it grabs this piece of information and adds it to its knowledgebase. Later on, when it finds that the return value from GetLatestOrderId method is being used as input to another method with an explicit precondition, the Checker can reasonably attempt to see if the operation is consistent with declared contracts. Let’s consider the following precondition contract:

public void ProcessOrder(int orderId)

{

  Contract.Requires<ArgumentException>(orderId >0);

  ...

}

These two explicit contracts provide enough information to the Checker to prove the contract. In this case, you won’t be getting any extra warning. But what if some of these contracts are missing? The Static Checker returns an output similar to what you see in Figure 4. The Checker detects that, say, a method has a Requires contract and receives data from another one that doesn’t say anything about its returned output.

Figure 4 Unproven Contracts

It should be clear by now that, to get the most out of the Static Checker, you must use Code Contracts all throughout your code. The more explicit contracts you bring in, the more reliable the Static Checker can be.

Assume and Assert

Sometimes, however, you have to integrate your new code with legacy code that others have written and that can’t be updated. If the legacy code doesn’t have any contracts, you’re going to get annoying warnings from the Static Checker. The Code Contracts API offers a workaround for this.

Essentially, unproven contract warnings originate from lack of information—the Checker is unable to find the required information. However, as the developer, you can provide more details—specifically, assumptions. Have a look at Figure 5.

Figure 5 A Warning from the Static Checker

You see a tooltip that warns about a possible null reference. Apparently, the variable context is being used without having been assigned. Who’s actually responsible for the tooltip? Is it the Checker or is it something else?

In this case, the tooltip comes from ReSharper, whose analysis engine correctly determines a possible null reference. Why don’t we get an analogous message from the Checker? That’s because of the first line in Figure 5:

Contract.Assume(context != null);

With this instruction, you guarantee to the Checker that the variable context is never null. The Checker just trusts you and adds that piece of information to its knowledgebase. ReSharper doesn’t currently provide full support for .NET Code Contracts, which explains why it still gives you a warning. On the other hand, ReSharper does support its own set of annotations that you can use in much the same way as with assumptions. See bit.ly/lVSnkj for more details.

Optimal Use of Static Analysis

Static analysis is difficult, and it’s probably not even an exact science. It often happens that you fill your code with contract information with the best intentions, just to find out that it significantly slows the build process. There are a couple of approaches to consider to optimize the use of contracts and subsequent analysis.

First, you might want to create a special build configuration and enable static checking only on that. You switch to it periodically, grab the feedback and apply it. When you’re done, you move back to build your solution as usual without the additional burden of static analysis.

Second, you can try using contracts piecemeal. You apply contracts extensively in the code, but then you disable contracts at the assembly level. You can do this by simply adding the following attribute to the properties of the assembly:

[assembly: ContractVerification(false)]

Next, you re-enable contract checking only where you’re currently focusing: class, method or assembly. You use the same attribute with a value of true.

Wrapping Up

Static analysis is a technique that aims to evaluate the correctness of your source code without running it. There are a few tools that do this to various extents. One is simply the compiler; another analysis tool is the Static Checker—an executable that usually integrates with the build process. In the .NET Framework, a special Static Checker tool works by learning facts about your code from Code Contracts. The Checker then evaluates these facts and highlights possible errors and contract violations.

At a time when complexity increases continually and development teams always run short of time, integrated static analysis saves a bit of time in builds and, more importantly, saves you from nasty bugs that hit your software just in corner cases.

---

Dino Esposito is the author of “Programming Microsoft ASP.NET MVC” (Microsoft Press, 2010) and coauthor of “Microsoft .NET: Architecting Applications for the Enterprise” (Microsoft Press, 2008). Based in Italy, Esposito is a frequent speaker at industry events worldwide. Follow him on Twitter at twitter.com/despos.

Thanks to the following technical expert for reviewing this article: Manuel Fahndrich