Principles of Software System Construction Jonathan ...

1 Static AnalysisPrinciples of Software System ConstructionJonathan AldrichSome slides from Ciera JaspanFind the Bug!disable interruptsSource: Engler et al., checking System Rules Using System -Specific, Programmer-Written Compiler Extensions, OSDI November 201115"214: Principles of Software System Construction2disable interruptsre"enable interruptsERROR: returningwith interrupts disabledLimits of Inspection People ..are very high cost ..make mistakes ..have a memory limitSo, let s automate inspection!29 November 2011315"214: Principles of Software System ConstructionMetal Interrupt Analysisis_enableddisableenableenable =>err(double enable)Source: Engler et al., checking System Rules Using System -Specific, Programmer-Written Compiler Extensions, OSDI =>err(double disable)end path =>err(end pathwith/intrdisabled)29 November 2011415"214: Principles of Software System ConstructionApplying the Analysisinitial state is_enabledSource: Engler et al.

2 , checking System Rules Using System -Specific, Programmer-Written Compiler Extensions, OSDI November 201115"214: Principles of Software System Construction5transition to is_disabledtransition to is_enabledfinal state is_enabled is OKfinal state is_disabled: ERROR!Empirical Results on Static Analysis InfoSys study [Chaturvedi 2005] 5 projects Average 700 function points each Compare inspection with and without static analysisAdapted from [Chaturvedi 2005] Conclusions Fewer defects Higher productivity29 November 2011615"214: Principles of Software System ConstructionStatic Analysis Finds Mechanical Errors Defects that result from inconsistently following simple, mechanical design rules Security vulnerabilities Buffer overruns, unvalidated Memory errors Null dereference, uninitialized Resource leaks Memory, OS Memory, OS Violations of API or framework rules Windows device drivers; real time libraries.

3 GUI frameworks Exceptions Arithmetic/library/user-defined Encapsulation violations Accessing internal data, calling private Race conditions Two threads access the same data without synchronization29 November 201115"214: Principles of Software System Construction7 Outline Why static analysis? Automated Can find some errors faster than people Can provide guarantees that some errors are found How does it work? What are the hard problems? What are the hard problems? How do we use real tools in an organization?29 November 2011815"214: Principles of Software System ConstructionOutline Why static analysis? How does it work? Systematic exploration of program abstraction Many kinds of analysis AST walker Control-flow and data-flow Control-flow and data-flow Type systems model checking Specifications frequently used for more information What are the hard problems? How do we use real tools in an organization?

4 29 November 2011915"214: Principles of Software System ConstructionAbstract Interpretation Static program analysis is the systematic examinationof an abstraction of a program s state space Abstraction Don t track everything! (That s normal interpretation) Track an important abstraction Systematic Systematic Ensure everything is checked in the same way Let s start November 20111015"214: Principles of Software System ConstructionA Performance AnalysisWhat s the performance problem?public foo() {= ( We have + conn + connections. );}public foo() {=if ( ()) { ( We have + conn + connections. );}Seems minor=but if this performance gain on 1000 servers means we need 1 less machine,we could be saving a a lot of ( We have + conn + connections. );}}29 November 20111115"214: Principles of Software System ConstructionA Performance Analysis Check that we don t create strings outside of a check Abstraction Look for a call to () Make sure it s surrounded by an if ( ()) Systematic Systematic Check all the code Known as an AST walker Treats the code as a text file Ignores control flow, variable values, and the heap Code style checkers work the same way you should never be checking code style by hand Simplest static analysis: grep29 November 20111215"214: Principles of Software System ConstructionAn interrupt checker Check for the interrupt problem Abstraction 2 states.

5 Enabled and disabled Program counter Systematic Check all paths through a function Check all paths through a function Error when we hit the end of the function with interrupts disabled Known as a control flow analysis More powerful than reading it as a raw text file Considers the program state and paths29 November 20111315"214: Principles of Software System ConstructionAdding branching When we get to a branch, what should we do? 1: explore each path separately Most exact information for each path Leads to an exponential state explosion 2: join paths back together Less exact But no state explosion Not just conditionals! Loops, switch, and exceptions too!29 November 20111415"214: Principles of Software System ConstructionExample: Bad1. int foo() {2. unsigned long flags;3. int rv;4. save_flags(flags);5. cli();6. rv = dont_interrupt();7. if (rv > 0) { ();Abstraction (before statement)2-4: enabled5: enabled6: disabled7: disabled8: disabled9: (); ();10.}}

6 } else {11. handle_error_case();12. }13. return rv;14. }9: disabled11: disabled13: unknownError: did not reenable interrupts on some path29 November 20111515"214: Principles of Software System ConstructionA null pointer checker Prevent accessing a null value Abstraction Program counter 3 states for each variable: null, not-null, and maybe-null Systematic Explore all paths in the program (as opposed to all paths in the Explore all paths in the program (as opposed to all paths in the method) Known as a data-flowanalysis Tracking how data moves through the program Very powerful, many analyses work this way Compiler optimizations were the first29 November 20111615"214: Principles of Software System ConstructionExample: Bad1. int foo() { x = new Integer(6); y = bar(); z; (y != null) = () + ();Abstraction (before statement)3: x not-null4: x not-null, y maybe-null5: x not-null, y maybe-null6: x not-null, y { = (); = x;10.)

7 X = null;11. }12. return z + ();13. }6: x not-null, y not-null8: x not-null, y null9: x not-null, y null10: x not-null, y not-null12: x maybe-null, y not-nullError: may have null pointer on line 1229 November 20111715"214: Principles of Software System ConstructionExample: Method calls1. int foo() { x = bar(); y = baz(); z = noNullsAllowed(x, y); ();6. }Two options:1. Global analysis7. Integer noNullsAllowed(8. Integer x, Integer y) { z;10. z = () + ();11. return new Integer(z);12. }1. Global analysis2. Modular analysis with specifications29 November 20111815"214: Principles of Software System ConstructionGlobal Analysis Dive into every method call Like branching, exponential Can t use joining trick Some path in the program has an error? Still requires developer to determine which method has the faultfault Who should check for null? The caller or the callee?

8 29 November 20111915"214: Principles of Software System ConstructionModular Analysis w/ Specifications Analyze each module separately Piece them together with specifications Pre-conditionand post-condition When analyzing a method Assume the method s precondition Check that it generates the postcondition Check that it generates the postcondition When the analysis hits a method call Check that the precondition is satisfied Assume the call results in the specified postcondition29 November 20112015"214: Principles of Software System ConstructionExample: Method calls1. int foo() { x = bar(); y = baz(); z = noNullsAllowed(x, y); ();6. }7.@Nonnull Integer noNullsAllowed(7.@Nonnull Integer noNullsAllowed(8. @Nonnull Integer x, @Nonnull Integer y) { z;10. z = () + ();11. return new Integer(z);12. }13. @Nonnull Integer bar();14. @Nullable Integer baz();29 November 20112115"214: Principles of Software System ConstructionClass invariants Is always true outside a class s methods Can be broken inside, but must always be put back together againpublic class Buffer {boolean isOpen;int available;/*@ invariant isOpen <==> available > 0 @*/public void open() {isOpen = true;//invariant is brokenavailable = loadBuffer();}}Java Modeling Language (JML)allows these kind of specs29 November 20112215"214: Principles of Software System ConstructionOther kinds of specifications Loop invariants What is always true inside a loop?)

9 Lock invariant What lock must you have to use this object? Protocols What order can you call methods in? What order can you call methods in? Good: Open, Write, Read,Close Bad: Open, Write, Close, Read29 November 20112315"214: Principles of Software System ConstructionTypechecking Another static analysis! In No typechecking at all! In ML, no annotations required Global typechecking In Java, we annotate with typesfoo() {a = 5;b = 3;bar( A , B ); In Java, we annotate with types Modular typechecking Types are a specification! In C#, no annotations for local variables Required for parameters and return values Best of bothbar( A , B );print(5 / 3); }bar(x, y) {print(x / y);} 29 November 20112415"214: Principles of Software System ConstructionStatic Analysis for Race Conditions Race conditiondefined:[From Savage et al., Eraser: A Dynamic Data Race Detector for Multithreaded Programs] Two threads access the same variable At least one access is a write No explicit mechanism prevents the accesses from being simultaneous Abstraction Abstraction Program counter of each thread, state of each lock Abstract away heap and program variables Systematic Examine all possible interleavings of all threads Flag error if no synchronization between accesses Exploration is exhaustive, since abstract state abstracts all concrete program state Known as model Checking29 November 201115"214: Principles of Software System Construction25 model checking for Race Conditionsthread1() {read x;}thread2() {lock();write x;Thread 1 Thread 2read xlockwrite xunlockwrite x;unlock();}Interleaving 1: OK29 November 20112615"214: Principles of Software System ConstructionModel checking for Race Conditionsthread1() {read x;}thread2() {lock();write x.}

10 Thread 1 Thread 2read xlockwrite xunlockwrite x;unlock();}Interleaving 1: OKInterleaving 2: OK29 November 20112715"214: Principles of Software System ConstructionModel checking for Race Conditionsthread1() {read x;}thread2() {lock();write x;Thread 1 Thread 2read xlockwrite xunlockwrite x;unlock();}Interleaving 1: OKInterleaving 2: OKInterleaving 3: Race29 November 20112815"214: Principles of Software System ConstructionModel checking for Race Conditionsthread1() {read x;}thread2() {lock();write x;Thread 1 Thread 2read xlockwrite xunlockwrite x;unlock();}Interleaving 1: OKInterleaving 2: OKInterleaving 3: RaceInterleaving 4: Race29 November 20112915"214: Principles of Software System ConstructionOutline Why static analysis? How does it work? What are the important properties? Side effects Modularity Aliases Aliases Termination Precision How do we use real tools in an organization?29 November 20113015"214: Principles of Software System ConstructionHard problems Side-effects Often difficult to specify precisely In practice: ignore (unsafe) or approximate (loses accuracy) Modularity Specifications Not just performance issue Not just performance issue Don t have to analyze all the code Reduces interactions between people Aliasing and pointer arithmetic Termination Precision29 November 20113115"214: Principles of Software System ConstructionAliasing Two variables point to the same object A variable might change underneath you during a seemingly unrelated call Multi-threaded: change at any time!