A System and Language for Building System-Specific,Static AnalysesSeth Hallem, Benjamin Chelf, Yichen Xie, and Dawson EnglerStanford UniversityABSTRACTThis paper presents a novel approach to bug-finding anal-ysis and an implementation of that approach. Our goal isto find as many serious bugs as possible. To do so, we de-signed a flexible, easy-to-use extension language for speci-fying analyses and an efficent algorithm for executing theseextensions. The language, metal, allows the users of oursystem to specify a broad class of analyses in terms that re-semble the intuitive description of the rules that they check.The system, xgcc, executes these analyses efficiently using acontext-sensitive, interprocedural analysis.Our prior work has shown that the approach describedin this paper is effective: it has successfully found thousandsof bugs in real systems code. This paper describes the un-derlying system used to achieve these results. We believethat our system is an effective framework for deploying newbug-finding analyses quickly and easily.KeywordsExtensible compilation, error detection.General TermsReliability, Security, Verification.Categories and Subject DescriptorsSoftware [Software Engineering]: Coding Tools andTechniques1. INTRODUCTIONThis paper describes the implementation of an unusualapproach to finding bugs that we call metacompilation(MC). The focus of our approach is pragmatism: we wantto find as many serious bugs as possible. We do so usingprogrammer-written compiler extensions (checkers). Thispaper presents a language, metal, for implementing theseextensions, and an analysis engine, xgcc, that executes ex-tensions using a context-sensitive, interprocedural analysis.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.PLDI’02, June 17-19, 2002, Berlin, Germany.Copyright 2002 ACM 1-58113-463-0/02/0006 ...$5.00.The main barrier to finding bugs is simply knowing thecorrectness rules that code must obey. The more rules youcan check, the more bugs you will find. Thus, we designedmetal to be (1) easy to use and (2) flexible enough to ex-press a broad range of rules within a unified framework.Metal must be easy to use since many rules are known onlyto programmers; if they cannot write extensions, we can-not check these rules. Thus, metal is designed for systemimplementers, not compiler writers. Metal must be flexiblebecause we want to check arbitrary rules. We do not wanta system that is limited to checking a specific set of proper-ties (e.g., synchronization constraints; temporal rules) or aspecific underlying assumption (e.g., “the analysis must beconservative”).Metal is easy to use because it provides the state ma-chine (SM) as a fundamental abstraction. State machinesare an easy abstraction because they are a familiar conceptin systems programming. Metal is flexible because it allowsthe extension writer to enhance the SM abstraction in near-arbitrary ways with general-purpose code. Metal’s flexibilityallows extensions to make the analysis rule-specific withoutmodifying the language or the underlying system.Our prior work has shown that metal works well. Itrequires little investment to get results: a day’s work canproduce an extension that finds tens or even hundreds of se-rious errors in actual code. Further, extensions are small —usually between 10 and 200 lines of code, depending mostlyon the amount of error reporting that they do. Metal’sflexibility is demonstrated by the fact that we were able towrite over fifty checkers that express significantly differenttypes of analyses including: (1) finding violations of knowncorrectness rules [1, 9] and (2) automatically inferring suchrules from source code [10]. We describe metal in Sections 2through 4.We have three main requirements for xgcc; it must: (1)provide the analysis needed to find bugs, (2) not significantlyrestrict what metal extensions can do, and (3) scale to largeprograms. Our ideal division of labor is that extensions en-code only the property to check, leaving the details of howto check the rule to xgcc. The second and third requirementsare important since the more rules we check and the morecode we analyze, the more bugs we will find. The main re-striction that xgcc places on extensions is determinism; theycan otherwise perform arbitrary computations internally. Inthis paper, we present the analysis algorithm, implementedin xgcc, that executes our extensions. We describe xgcc inSections 5 and 6.In Section 7, we discuss the approximations that our691: state decl any_pointer v;2:3: start: { kfree(v) } ==> v.freed;4:5: v.freed: { *v } ==> v.stop,6: { err("using %s after free!", mc_identifier(v)); }7: | { kfree(v) } ==> v.stop,8: { err("double free of %s!", mc_identifier(v)); }9: ;Figure 1: Free Checkeranalyses make and their implications. Section 8 discussesseveral analysis techniques for handling false positives in-cluding a simple, path-sensitive analysis for eliminatingnonexecutable paths. Section 9 continues the false positivediscussion by presenting the ways in which xgcc ranks er-ror reports. Finally, Section 10 discusses related work andSection 11 concludes.2. OVERVIEWOur extensions are written in metal, a language for ex-pressing a broad class of customized, static, bug-findinganalyses. The common thread among these analyses is thatthey all exploit the fact that many abstract program restric-tions map clearly to source code actions [9]. While metal ex-tensions are executed much like a traditional dataflow anal-ysis, they can easily be augmented in ways outside the scopeof traditional approaches, such as using statistical analysisto discover rules [10].To check a rule, an extension does two things: (1) recog-nizes interesting source code actions relevant to a given ruleand (2) checks that these actions satisfy some rule-specificconstraint. Metal organizes extensions around a state ma-chine (SM) abstraction. State machines are a concise way torepresent many program properties. Note that the SM ab-straction provides sugar for common operations, it does notlimit extensions to checking finite-state properties.