Scalable Error Detection using Boolean SatisfiabilityYichen Xie∗Alex Aiken∗Computer Science DepartmentStanford UniversityStanford, CA 94305{yxie,aiken}@cs.stanford.eduABSTRACTWe describe a software error-detection tool that exploits re-cent advances in boolean satisfiability (SAT) solvers. Ouranalysis is path sensitive, precise down to the bit level, andmodels pointers and heap data. Our approach is also highlyscalable, which we achieve using two techniques. First, foreach program function, several optimizations compress thesize of the boolean formulas that model the control- anddata-flow and the heap locations accessed by a function.Second, summaries in the spirit of type signatures are com-puted for each function, allowing inter-procedural analysiswithout a dramatic increase in the size of the boolean con-straints to be solved.We demonstrate the effectiveness of our approach by con-structing a lock interface inference and checking tool. Inan interprocedural analysis of more than 23,000 lock relatedfunctions in the latest Linux kernel, the checker generated300 warnings, of which 179 were unique locking errors, afalse positive rate of only 40%.Categories and Subject DescriptorsD.2.4 [Software Engineering]: Software/Program Verifi-cation; D.2.3 [Software Engineering]: Coding Tools andTechniques; D.2.5 [Software Engineering]: Testing andDebuggingGeneral TermsAlgorithms, Experimentation, Languages, Verification.KeywordsProgram analysis, error detection, boolean satisfiability.∗Supported by NFS grant CCF-0430378.Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies arenot made or distributed for profit or commercial advantage and that copiesbear this notice and the full citation on the first page. To copy otherwise, torepublish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee.POPL’05, January 12–14, 2005, Long Beach, California, USA.Copyright 2005 ACM 1-58113-830-X/05/0001 ...$5.00.1. INTRODUCTIONThis paper presents Saturn1, a software error-detectiontool based on exploiting recent advances in solving booleansatisfiability (SAT) constraints. Rapid improvements in al-gorithms for SAT have led to its use in a variety of applica-tions, including recently in program verification [16, 17, 19,7, 11]. The contributions of our approach are:• We give a translation from a realistic programminglanguage to SAT that is substantially more efficientthan previous approaches (Section 2). While we modeleach bit path sensitively as in [19, 8, 24], several tech-niques achieve a substantial reduction in the size of theSAT formulas Saturn must solve.• We describe how to compute a summary, similar to atype signature, for each analyzed function (Section 4),thereby enabling interprocedural analysis. Comput-ing concise summaries enables Saturn to analyze muchlarger programs than previous error checking systemsbased on SAT, and in fact, the scaling behavior ofSaturn is at least competitive with, if not better than,other, non-SAT approaches to bug finding and verifi-cation. In addition, Saturn is able to infer and applysummaries that encode a form of interprocedural pathsensitivity via input and output predicates, lending it-self well to checking complex value-dependent programbehaviors (Section 5.2).• We present an interface for defining temporal safetyproperties for Saturn to check, and we show one suchspecification in detail: checking that a single threadcorrectly manages locks—i.e., does not perform twolock or unlock operations in a row on any lock (Sec-tion 5.5).• We present a significant experiment in which we per-form an interprocedural analysis of the entire Linuxkernel for locking errors (Section 6). In analyzing 4.8million lines of code, Saturn generated 300 warnings,of which 179 were unique locking errors, for a false pos-itive rate of only 40% (i.e., more than half of the warn-ings were genuine bugs). For comparison, two previousstudies of the same locking properties using MC [13]and CQual [12] found 31 and 18 locking errors respec-tively, with higher false positive rates (above 80% forboth MC and CQual—i.e., fewer than 1 in 5 warningsis a genuine bug) [2, 10, 12].1SATisfiability-based failURe aNalysis.351• We have built a database of all the inferred lockingsignatures of functions in the Linux kernel. We re-port some interesting statistics, showing that lockingbehavior in Linux is quite complex and that much ofthe kernel relies either directly or indirectly on correctlocking behavior (Section 6.2).It is worth noting that Saturn can do more than analyz-ing locks, although we do not report on additional checkershere. Locking analysis has become a standard test case forbug finding/verification tools, because in practice analyzinglocking requires accurate modeling of many features: lock-ing is always a flow sensitive and sometimes a path sensitiveproperty, programmers store locks in data structures, passlocks as arguments, use complex tests to decide when andwhere to acquire and release locks, and so on.One thing that Saturn is not, at least in its current form,is a verification tool. Tools such as CQual are capable ofverification (proving the absence of bugs, or at least as closeas one can reasonably come to that goal for C programs).Saturn is a bug finding tool in the spirit of MC, which meansit is designed to find as many bugs as possible with a lowfalse positive rate, potentially at the cost of missing somebugs. In particular, Saturn currently is unsound in its anal-ysis of loops (see Section 2) because it is not possible inmost cases to construct a finite boolean formula represent-ing a fully unrolled loop. This problem is shared by allSAT-based analysis systems (see, e.g., [19, 24]) and we leavefurther investigation as future work.Another source of unsoundness is Saturn’s treatment ofpointers in a function’s environment. In order to reducefalse positives, Saturn makes the assumption that distinctpointers from the environment do not alias each other. Thesame treatment is afforded to pointer values obtained fromaspects of the C language that Saturn does not currentlymodel (e.g., arrays, unions, inline assembly, unsafe casts,and function pointers). A sound alternative is to use a sep-arate global alias analysis to account for potentially missedaliasing relationships. The treatment of external pointers isfurther