Can't get no Boolean satisfaction? -

Can’t get no Boolean satisfaction?


Since its introduction, static source-code analysis has had a mixed reputation with development teams due to long analysis times, excessive noise, or an unacceptable rate of false-positive results. Excessive false-positive results are the main reason why many source-code analysis products quickly become shelfware after a few uses. Despite early shortcomings, the promise of static analysis remained of interest to developers because the technology offers the ability to find bugs before software is run, improving code quality, and dramatically accelerating the availability of new applications. Although static analysis has historically struggled to deliver on this promise, a relatively new use of Boolean satisfiability (SAT) in the field is poised to help static analysis deliver on its potential.

Before the first software application was released, the first software defects had been found and eliminated. Call them bugs, errors, or failures, software defects have existed as long as software itself. As early applications evolved to become more robust and more complex, the remaining defects became more difficult to corral. Simply stated, the more lines of code necessary to create an application, the more defects one would expect to encounter during development.

Consider a theoretical average ratio of one defect per 1000 lines of code (likely a gross underestimate). As a code base expands from thousands of lines, to tens of thousands, to hundreds of thousands, this defect ratio would become overwhelming for developers relying exclusively on manual techniques to control the resulting volume of defects.

With applications assuming more critical functions for business and industry, the consequence of defects in the field now mandates that software meet specific quality standards prior to release. It's at this intersection of opportunity and risk that developers turned to software itself to try and eliminate software defects earlier in the development cycle. Applying static analysis to software, the automated review of code prior to run-time with the intention of identifying defects, was an obvious solution to this fundamental challenge of ensuring code quality.

First-generation static analysis
The first static-analysis tool appeared in the late 1970s. One of the most commonly referred to tools from that era was Lint, which can be regarded as the first generation of commercially viable static analysis. Lint held great promise for developers when it was initially released, because for the first time, it allowed developers to automate the detection of software defects early in the application lifecycle, when they were easiest to correct. The key innovation behind Lint was the use of compilers to do more than simply check compile warnings and errors. By extending the scope of what the compiler looked for in the code, Lint was able to uncover some real defects in software systems, thus enabling it to become the first viable static source-code analysis solution.

In reality, Lint wasn't designed with the goal of identifying defects that cause run-time problems. Rather, its purpose was to flag suspicious or non-portable constructs in the code to help developers code in a more consistent format. By “suspicious code,” I mean code that, while technically correct from the perspective of the source code language (e.g., C, C++), it might be structured so that it could possibly execute in ways not intended by the developer. The problem with flagging suspicious code is that, like compiler warnings, code of this type could, and often would, work correctly. Because of this, and Lint's limited analysis capabilities, noise rates were extremely high, often exceeding a 10:1 ratio between noise and real defects.

Finding the real defects amidst Lint's voluminous reports required developers to conduct time-consuming manual reviews of the results, compounding the exact problem that static analysis was supposed to, in its ideal state, eliminate. Hence, Lint was never widely adopted as a defect detection tool. But as a testament to the quality of Lint's underlying technology, many different versions of the product still remain available.

Second -generation static analysis
For nearly two decades, static analysis remained more fiction than fact as a commercially viable production tool for identifying defects. In early 2000, a second generation of tools (e.g., Stanford Checker) emerged that offered enough value to become commercially viable. By leveraging new technology that expanded the capabilities of first-generation tools past simple pattern matching to also focus on path coverage, second-generation static analysis was able to uncover more defects with real run-time implications. Again, the observation was that the compiler could do more than it was doing by simply turning source code into object files. But this time, the requirement was to try to identify not just suspicious code but rather violations of the many ad-hoc system specific rules that modern day software systems must obey.

These tools could also analyze entire code bases, not just one file. By shifting focus from “suspicious constructs” to “run-time defects,” developers of these new static-analysis technologies recognized the need to understand more of the inter-workings of code bases. This meant combining sophisticated path analysis with inter-procedural analysis to understand what happened when the control flow passed from one function to another within a given software system.

Despite their adoption and use by organizations, second-generation static analysis still had difficulty finding the sweet spot between accuracy and scalability. Some solutions were accurate for a small set of defect types, but couldn't scale to analyze millions of lines of code.

The problem of wrestling with an elusive sweet spot between accuracy and scalability led to a false-positive problem. Like the noise problem preventing first-generation tools from delivering on the promise of static analysis, it slowed second-generation tools from being more rapidly adopted.

Third-generation static analysis
Today, a new generation of static analysis is emerging. The technology is capable of delivering unmatched quality of results from a solution that fits within existing development processes and environments. Leveraging solvers for Boolean satisfiability (SAT) to complement traditional path simulation analysis techniques, third-generation static analysis gives developers results that are both comprehensive and accurate.

For now, let's define SAT as the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to “true.” It's equally important to determine whether no such assignments exist, which would imply that the function expressed by the formula is identically “false” for all possible variable assignments. In this latter case, the formula is unsatisfiable; otherwise, it's satisfiable.

The use of SAT allows static source-code analysis to find the right defects in code without a high rate of distracting false positives. It also provides new capabilities that lay the foundation for further technological advances in static analysis. Before delving into the technology, some background on the use of SAT may provide some helpful context.

Leveraging SAT in IC design
In the field of computer-aided engineering and design, EDA (electronic design automation) tools have been used with tremendous success to eliminate costly design failures in hardware devices. For decades, companies such as Cadence, Mentor Graphics, and Synopsys have used advanced tools to simulate the operations of circuits prior to fabrication to verify their correctness and performance.

The use of SAT was introduced in these tools in the 1980s to create a digital simulation of hardware, allowing developers to test a design's architectural operation and inspect the accuracy of performance at both cycle and interface levels. This visibility accelerated development and improved device quality by allowing EDA developers to more thoroughly simulate their designs prior to fabrication.

Because of its successful history in hardware development, the introduction of SAT to software analysis is unlike previous advancements in static analysis. Leveraging SAT solvers for performing static analysis of hardware designs is a mature, sophisticated technique that incorporates decades of refinement from the hardware tool vendors. Use of this technology lays the groundwork for a new generation of static analysis, where we can analyze code with two complementary analysis techniques (SAT and path simulation) to deliver accurate results.

Today's software development challenges require companies to look for innovative ways to remove the critical performance flaws and security vulnerabilities in software before it gets to the quality assurance lab, or worse, into the field. Fortunately for developers, source-code analysis is now up to the task. By combining techniques in the application of Boolean satisfiability to software with the latest advances in path simulation analysis, the most sophisticated source-code analysis can boast out-of-the-box false positive rates as low as 10% and scalability to tens of millions of lines of C/C++ or Java code.

Software developers can use static analysis to automatically uncover errors that are typically missed by unit testing, system testing, quality assurance, and manual code reviews. By quickly finding and fixing these hard-to-find defects at the earliest stage in the software development life cycle, organizations are saving millions of dollars in associated costs.

Future uses of SAT in static analysis
Potential applications of SAT include false path pruning and the ability to find problems such as string overflows, integer overflows, or deadcode, and the use of static asset checking to identify difficult-to-find logic bugs. While some instances of the defects in these categories can be discovered today, SAT-based analysis builds on the success of existing path simulation analysis to reach new levels of accuracy and precision in static code analysis.

SAT will benefit software developers and architects by fundamentally changing the way they view static analysis of their source code. Going from simple “grep” parsing through code to practical path simulation analysis earlier this decade was a huge eye-opener for many developers (“You mean, it can show me the whole path to get to a real bug?”). Now, leveraging SAT solvers for static analysis can impress anyone who writes software.

Ben Chelf is the CTO of San Francisco-based Coverity. He was a founding member of the Stanford Computer Science Laboratory team that architected and developed Coverity's underlying technology. He is one of the world's leading experts on the commercial use of static source code analysis. Chelf holds BS and MS degrees in Computer Science from Stanford University. He can be reached at

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.