WIXLIB

Quick QuizDraw a parse tree for the function below. You can assume that the“for” statement is at the top of the parse tree.void copy bytes(char dest[], char source[], int n) {for (int i 0; i n; i)dest[i] source[i];}2/21/201117-654: Analysis of Software ArtifactsStatic Analysis39Matching AST against Bug Patterns AST Walker Analysis Walk the AST, looking for nodes of a particular typeCheck the immediate neighborhood of the node for a bug patternWarn if the node matches the patternSemantic grep Like grep, looking for simple patternsUnlike grep, consider not just names, but semantic structure ofAST Makes the analysis more preciseCommon architecture based on Visitors 2/21/2011class Visitor has a visitX method for each type of AST node XDefault Visitor code just descends the AST, visiting each nodeTo find a bug in AST element of type X, override visitX17-654: Analysis of Software ArtifactsStatic Analysis4020

Behavioral Patterns: Visitor Applicability Structure with many classes Want to perform operationsthat depend on classes Set of classes is stable Want to define newoperations Consequences Easy to add new operations Groups related behavior inVisitor Adding new elements ishard Visitor can store state Elements must exposeinterface2/21/201117-654: Analysis of Software ArtifactsStatic Analysis41Example: Shifting by more than 31 bitsclass BadShiftAnalysis extends VisitorvisitShiftExpression(ShiftExpression e) {if (type of e’s left operand is int)if (e’s right operand is a constant)if (value of constant 0 or 31)warn(“Shifting by less than 0 or morethan 31 is /201117-654: Analysis of Software ArtifactsStatic Analysis4221

Example: String concatenation in a loopclass StringConcatLoopAnalysis extends Visitorprivate int loopLevel 0;visitStringConcat(StringConcat e) {if (loopLevel 0)warn(“Performance issue: String concatenation in loop (useStringBuffer instead)”)super.visitStringConcat(e);// visits AST children}visitWhile(While e) {loopLevel ;super.visitWhile(e);// visits AST childrenloopLevel--;}// similar for other looping constructs2/21/201117-654: Analysis of Software ArtifactsStatic Analysis43Example Tool: FindBugs Origin: research project at U. Maryland Checks over 250 “bug patterns” Now freely available as open sourceStandalone tool, plugins for Eclipse, etc.Over 100 correctness bugsMany style issues as wellIncludes the two examples just shownFocus on simple, local checks Similar to the patterns we’ve seenBut checks bytecode, not AST Harder to write, but more efficient and doesn’t require 654: Analysis of Software ArtifactsStatic Analysis4422

Example FindBugs Bug Patterns Correct equals()Use of Closing streamsIllegal castsNull pointer dereferenceInfinite loopsEncapsulation problemsInconsistent synchronizationInefficient String useDead store to variable2/21/201117-654: Analysis of Software ArtifactsStatic Analysis45FindBugs Experiences Useful for learning idioms of Java Rules about libraries and interfaces e.g. equals() Customization is important Many warnings may be irrelevant, others may beimportant – depends on domain e.g. embedded system vs. web application Useful for pointing out things to examine 2/21/2011Not all are real defectsTurn off false positive warnings for future analyseson codebase17-654: Analysis of Software ArtifactsStatic Analysis4623

Outline Why static analysis?What is static analysis?How does static analysis work?AST AnalysisDataflow Analysis Control Flow Graph Representation Simple Flow Analysis: Zero/Null Values2/21/201117-654: Analysis of Software ArtifactsStatic Analysis47Motivation: Dataflow Analysis Catch interesting errors Non-local: x is null, x is written to y, y isdereferenced Optimize code Reduce run time, memory usageK Soundness required Safety-critical domain Assure lack of certain errorsCannot optimize unless it is proven safe Correctness comes before performance Automation required 2/21/2011Dramatically decreases costMakes cost/benefit worthwhile for far morepurposes17-654: Analysis of Software ArtifactsStatic Analysis4824

Dataflow analysis Tracks value flow through program Can distinguish order of operations Did you read the file after you closed it?Does this null value flow to that dereference?Differs from AST walker Walker simply collects information or checks patternsTracking flow allows more interesting properties Abstracts values Chooses abstraction particular to property Is a variable null?Is a file open or closed?Could a variable be 0?Where did this value come from?More specialized than Hoare logic 2/21/2011Hoare logic allows any property to be expressedSpecialization allows automation and soundness17-654: Analysis of Software ArtifactsStatic Analysis49Zero Analysis Could variable x be 0? Useful to know if you have an expression y/xIn C, useful for null pointer analysis Program semantics η maps every variable to an integer Semantic abstraction σ maps every variable to non zero (NZ), zero(Z), or maybe zero (MZ)Abstraction function for integers αZI : We may not know if a value is zero or not 2/21/2011αZI(0) ZαZI(n) NZ for all n 0Analysis is always an approximationNeed MZ option, too17-654: Analysis of Software ArtifactsStatic Analysis5025

Zero Analysis Exampleσ []x : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/201117-654: Analysis of Software ArtifactsStatic Analysis51Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x αZI(10)]17-654: Analysis of Software ArtifactsStatic Analysis5226

Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]17-654: Analysis of Software ArtifactsStatic Analysis53Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y σ(x)]17-654: Analysis of Software ArtifactsStatic Analysis5427

Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y NZ]17-654: Analysis of Software ArtifactsStatic Analysis55Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y NZ]σ [x NZ,y NZ,z αZI(0)]17-654: Analysis of Software ArtifactsStatic Analysis5628

Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y NZ]σ [x NZ,y NZ,z Z]17-654: Analysis of Software ArtifactsStatic Analysis57Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y NZ]σ [x NZ,y NZ,z Z]σ [x NZ,y NZ,z Z]17-654: Analysis of Software ArtifactsStatic Analysis5829

Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y NZ]σ [x NZ,y NZ,z Z]σ [x NZ,y NZ,z Z]σ [x NZ,y NZ,z Z]17-654: Analysis of Software ArtifactsStatic Analysis59Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y NZ]σ [x NZ,y NZ,z Z]σ [x NZ,y NZ,z Z]σ [x NZ,y NZ,z Z]σ [x NZ,y MZ,z Z]17-654: Analysis of Software ArtifactsStatic Analysis6030

Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y NZ]σ [x NZ,y NZ,z Z]σ [x NZ,y NZ,z Z]σ [x NZ,y NZ,z Z]σ [x NZ,y MZ,z Z]σ [x NZ,y MZ,z NZ]17-654: Analysis of Software ArtifactsStatic Analysis61Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y NZ]σ [x NZ,y NZ,z Z]σ [x NZ,y MZ,z MZ]σ [x NZ,y NZ,z Z]σ [x NZ,y MZ,z Z]σ [x NZ,y MZ,z NZ]17-654: Analysis of Software ArtifactsStatic Analysis6231

Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y NZ]σ [x NZ,y NZ,z Z]σ [x NZ,y MZ,z MZ]σ [x NZ,y MZ,z MZ]σ [x NZ,y MZ,z Z]σ [x NZ,y MZ,z NZ]17-654: Analysis of Software ArtifactsStatic Analysis63Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;2/21/2011σ []σ [x NZ]σ [x NZ,y NZ]σ [x NZ,y NZ,z Z]σ [x NZ,y MZ,z MZ]σ [x NZ,y MZ,z MZ]σ [x NZ,y MZ,z MZ]σ [x NZ,y MZ,z NZ]17-654: Analysis of Software ArtifactsStatic Analysis6432

Zero Analysis Examplex : 10;y : x;z : 0;while y -1 dox : x / y;y : y-1;z : 5;σ []σ [x NZ]σ [x NZ,y NZ]σ [x NZ,y NZ,z Z]σ [x NZ,y MZ,z MZ]σ [x NZ,y MZ,z MZ]σ [x NZ,y MZ,z MZ]σ [x NZ,y MZ,z NZ]Nothing more happens!2/21/201117-654: Analysis of Software ArtifactsStatic Analysis65Zero Analysis Termination The analysis values will not change, no matter howmany times we execute the loop 2/21/2011Proof: our analysis is deterministicWe run through the loop with the current analysis values,none of them changeTherefore, no matter how many times we run the loop, theresults will remain the sameTherefore, we have computed the dataflow analysis resultsfor any number of loop iterations17-654: Analysis of Software ArtifactsStatic Analysis6633

Zero Analysis Termination The analysis values will not change, no matter howmany times we execute the loop Proof: our analysis is deterministicWe run through the loop with the current analysis values,none of them changeTherefore, no matter how many times we run the loop, theresults will remain the sameTherefore, we have computed the dataflow analysis resultsfor any number of loop iterationsWhy does this work If we simulate the loop, the data values could (in principle)keep changing indefinitely There are an infinite number of data values possibleNot true for 32-bit integers, but might as well be true Counting to 232 is slow, even on today’s processorsDataflow analysis only tracks 2 possibilities!So once we’ve explored them all, nothing more will changeThis is the secret of abstractionWe will make this argument more precise later2/21/201117-654: Analysis of Software ArtifactsStatic Analysis67Using Zero Analysis Visit each division in the programGet the results of zero analysis for the divisorIf the results are definitely zero, report an errorIf the results are possibly zero, report a warning2/21/201117-654: Analysis of Software ArtifactsStatic Analysis6834

Quick Quiz Fill in the table to show how what information zeroanalysis will compute for the function given.Program StatementAnalysis Info after that statement0: beginning of program 1: x : 02: y : 13: if (z 0)4:x : x y5: else y : y – 16: w : y2/21/201117-654: Analysis of Software ArtifactsStatic Analysis69Outline Why static analysis?What is static analysis?How does static analysis work?AST AnalysisDataflow AnalysisFurther Examples and Discussion2/21/201117-654: Analysis of Software ArtifactsStatic Analysis7035

Static Analysis Definition Static program analysis is the systematic examinationof an abstraction of a program’s state space Simple model checking for data races Data Race defined:[From Savage et al., Eraser: A Dynamic Data Race Detector forMultithreaded Programs] Two threads access the same variableAt least one access is a writeNo explicit mechanism prevents the accesses from beingsimultaneousAbstraction Program counter of each thread, state of each lock Abstract away heap and program variablesSystematic Examine all possible interleavings of all threads Flag error if no synchronization between accessesExploration is exhaustive, since abstract state abstracts all concreteprogram state2/21/201117-654: Analysis of Software ArtifactsStatic Analysis71Model Checking for Data Racesthread1() {read x;}thread2() {lock();write x;unlock();}Thread 1Thread 2read xlockwrite xunlockInterleaving 1: OK2/21/201117-654: Analysis of Software ArtifactsStatic Analysis7236

Model Checking for Data Racesthread1() {read x;}thread2() {lock();write x;unlock();}Thread 1Thread 2lockwrite xunlockread xInterleaving 1: OKInterleaving 2: OK2/21/201117-654: Analysis of Software ArtifactsStatic Analysis73Model Checking for Data Racesthread1() {read x;}thread2() {lock();write x;unlock();}Thread 1Thread 2lockread xwrite xunlockInterleaving 1: OKInterleaving 2: OKInterleaving 3: Race2/21/201117-654: Analysis of Software ArtifactsStatic Analysis7437

Model Checking for Data RacesThread 1thread1() {read x;}thread2() {lock();write terleaving2/21/2011Thread 2lockwrite xread xunlock1: OK2: OK3: Race4: Race17-654: Analysis of Software ArtifactsStatic Analysis75Compare Analysis to Testing, Inspection Why might it be hard to test/inspect for: Null pointer errors? Forgetting to re-enable interrupts? Race conditions?2/21/201117-654: Analysis of Software ArtifactsStatic Analysis7638

Compare Analysis to Testing, Inspection Null Pointers, Interrupts Testing Errors typically on uncommon paths or uncommon inputDifficult to exercise these pathsInspection Non-local and thus easy to miss Object allocation vs. dereferenceDisable interrupts vs. return statement Finding Data Races Testing Cannot force all interleavingsInspection Too many interleavings to considerCheck rules like “lock protects x” instead 2/21/2011But checking is non-local and thus easy to miss a case17-654: Analysis of Software ArtifactsStatic Analysis77Sound Analyses A sound analysis never misses an error [of the relevant error category]No false negatives (missed errors)Requires exhaustive exploration of state spaceInductive argument for soundness 2/21/2011Start program with abstract state for all possible initialconcrete statesAt each step, ensure new abstract state covers all concretestates that could result from executing statement on anyconcrete state from previous abstract stateOnce no new abstract states are reachable, by induction allconcrete program executions have been considered17-654: Analysis of Software ArtifactsStatic Analysis7839

Soundness and PrecisionProgram state covered in actual executionunsound(false negative)imprecise(false positive)Program state covered by abstractexecution with analysis2/21/201117-654: Analysis of Software ArtifactsStatic Analysis79Soundness and PrecisionProgram state covered in actual executionunsound(false negative)imprecise(false positive)Program state covered by abstractexecution with analysis2/21/201117-654: Analysis of Software ArtifactsStatic Analysis8040

Abstraction and Soundness Consider “Sound Testing” [testing that finds every bug]Requires executing program on every input (and on all interleavings of threads)Infinite number of inputs for realistic programs Therefore impossible in practice Abstraction 2/21/2011Infinite state space finite set of statesCan achieve soundness by exhaustive exploration17-654: Analysis of Software ArtifactsStatic Analysis81Zero Analysis Precision1.2.3.4.5.void foo(unsigned n) {int x -1;x x 2;int y 10/x;}What will be the result of staticanalysis?Path 1 (after stmt):1: 2: x NZ3: x MZwarning: possible divide by zero atline 4False positive! (not a real error)What went wrong? Before statement 3 we only knowx is nonzero We need to know that x is -12/21/201117-654: Analysis of Software ArtifactsStatic Analysis8241

Regaining Zero Analysis Precision Keep track of exact value of variables Infinite states or 232, close enough Add a -1 state Not general enough Track formula for every variable Undecidable for arbitrary formulas Track restricted formulas Decent solution in practice 2/21/2011Presburger arithmetic17-654: Analysis of Software ArtifactsStatic Analysis83Analysis as an Approximation Analysis must approximate in practice May report errors where there are really none False positives May not report errors that really exist All analysis tools have either false negatives or falsepositives False negatives Approximation strategy Find a pattern P for correct code which is feasible to check (analysis terminates quickly),covers most correct code in practice (low false positives),which implies no errors (no false negatives) Analysis can be pretty good in practice Many tools have low false positive/negative ratesA sound tool has no false negatives 2/21/2011Never misses an error in a category that it checks17-654: Analysis of Software ArtifactsStatic Analysis8442

Attribute-Specific Analysis Analysis is specific to A quality attribute Race conditionBuffer overflow, divide by zeroUse after freeA strategy for verifying that attribute Protect each shared piece of data with a lockPresburger arithmetic decision procedure for arrayindexes, zero analysisOnly one variable points to each memory location Analysis is inappropriate for some attributes Approach to assurance is ad-hoc and follows noclear patternNo known decision procedure for checking anassurance pattern that is followedExamples?2/21/201117-654: Analysis of Software ArtifactsStatic Analysis85Soundness Tradeoffs Sound Analysis Assurance that nobugs are left Of the target errorclass Can focus otherQA resources onother errors May have morefalse positives2/21/2011 Unsound Analysis No assurance thatbugs are gone Must still applyother QAtechniques May have fewerfalse positives17-654: Analysis of Software ArtifactsStatic Analysis8643

Which to Choose? Cost/Benefit tradeoff Benefit: How valuable is the bug? How much does it cost if not found?How expensive to find using testing/inspection?Cost: How much did the analysis cost? Effort spent running analysis, interpreting results –includes false positivesEffort spent finding remaining bugs (for unsound analysis) Rule of thumb For critical bugs that testing/inspection can’t find, asound analysis is worth it As long as false positive rate is acceptableFor other bugs, maximize engineer productivity2/21/201117-654: Analysis of Software ArtifactsStatic Analysis8717-654: Analysis of Software ArtifactsStatic Analysis88Questions?2/21/201144

Additional Slides/Examples2/21/201117-654: Analysis of Software ArtifactsStatic Analysis89Static Analysis Definition Static program analysis is the systemati

Empirical Results on Static Analysis Nortel study [Zheng et al. 2006] 3 C/C projects 3 million LOC total Early generation static analysis tools Conclusions Cost per fault of static analysis 61-72% compared to inspections Effectively finds assignment, checking faults Can be used to find potential security .