5/23/20111Path-Based Static AnalysisLecture 18CS 295Prof. Aiken CS 295 Lecture 18 1Overview• So far we have looked at summary-basedstatic analysis– For each function f, compute description of the effect of f– Mapping of inputs to outputs• Example ala Saturn:(flag, *file1, Closed) -> (true, *file1, Open)“if flag is true and file1 is closed on function entry, then file1 is open on function exit”Prof. Aiken CS 295 Lecture 18 2Discussion• Summaries can be hard to compute• Must account for all paths through the function• Summary language generally must be quite expressiveProf. Aiken CS 295 Lecture 18 3Another Approach• An alternative to summaries is to peformpath-basedanalysis•Analyze just one path at a timeAnalyze just one path at a time• Conceptually simpler– And often simpler to implementProf. Aiken CS 295 Lecture 18 4Checking PathsProf. Aiken CS 295 Lecture 18 5Issues• There can be a lot of paths–Nconditionals -> up to 2Npaths•There can be a lotof pathsp– Loops, recursive functions• Leave these issues aside for nowProf. Aiken CS 295 Lecture 18 65/23/20112Finite State Properties (Again)• For specifications, use FSMs• For this lecture, files–Two states: Open, Closed–An Open file can be Closed–A Closed file can be Open– Other transitions are errorsProf. Aiken CS 295 Lecture 18 7A First AlgorithmFor each path track the state of each fileFor each path, track the state of each fileProf. Aiken CS 295 Lecture 18 8Applying the Simple AlgorithmAssume file is initially in Open stateProf. Aiken CS 295 Lecture 18 9What Went Wrong?• Some of these paths are invalid– no execution can follow these “paths”Prof. Aiken CS 295 Lecture 18 10An Invalid PathProf. Aiken CS 295 Lecture 18 11A Second Algorithm• Keep track of branch decisions on paths– Abstract state is now a pair(predicate, file state)• Predicate is a conjunction of branch conditions– If predicate is false, path is infeasible• File state is as beforeProf. Aiken CS 295 Lecture 18 125/23/20113Tracking PredicatesProf. Aiken CS 295 Lecture 18 13Discussion•This works– Modulo unresolved issues with loops/recursion•Requiresq– A theorem prover• Something that can deduce whether a predicate is false– A way of accurately modeling branch predicates• A hard problem in general– Branch predicates can be arbitrary code• But many predicates are easy in practiceProf. Aiken CS 295 Lecture 18 14The Problem• The main problem is there are too many paths• In practice, this approach has not proven to be scalablebe scalable– Exponential blow-up in number of paths is real– Can’t extend this approach to large programsProf. Aiken CS 295 Lecture 18 15An Observation• Some of the paths in our example are irrelevant to the property of interest•Consider the test on pConsider the test on pProf. Aiken CS 295 Lecture 18 16Irrelevant PredicatesProf. Aiken CS 295 Lecture 18 17Discussion• We want something in between the naïve approach with no predicates and modeling all predicates• Just want to model predicates relevant to the propertyProf. Aiken CS 295 Lecture 18 185/23/20114The Idea• Give up on analyzing paths completely independently– Now analyze all paths in a function simultaneously• At points where paths join–joinall abstract states where the information for the file is the same– Note: number of possible abstract states is now limited by the number of FSM statesProf. Aiken CS 295 Lecture 18 19The Join Operation• The join operation is special• New abstract states:(p1p2 p S)(p1p2… pn, S)• First component is a list of predicates– Implicitly conjoinedProf. Aiken CS 295 Lecture 18 20The Join Operation (Cont.)• Idea: Join drops any predicates not in common•Example:Join[(p1p2p3 S) (p1p4p3 S)] =Join[(p1p2p3, S),(p1p4p3, S)] =(p1 p3, S)Prof. Aiken CS 295 Lecture 18 21ExampleProf. Aiken CS 295 Lecture 18 22Discussion• Key to path-sensitive analysis is maintaining correlations– Between branches and the property of interest• The pattern involving dump is very common– As are more elaborate variations • But not all correlations are useful– Some turn out to have no useful information at all– ESP tries to locally infer the useful correlationsProf. Aiken CS 295 Lecture 18 23What is Lost?Prof. Aiken CS 295 Lecture 18 245/23/20115What is Lost?• If a correlation is established– Before the property state is affected– And ultimately does affect the property state• ESP will not track it and will lose informationProf. Aiken CS 295 Lecture 18 25Another ExampleProf. Aiken CS 295 Lecture 18 26Back to Recursion• Consider the following examplefoo(x,y) {if (x == 0) return;if (x == 0) return;open(y);close(y);foo(x-1, y)}Prof. Aiken CS 295 Lecture 18 27Comments• Like any static analysis, recursion/looping introduces recursive constraints•Need an initial estimate for the solution, Need an initial estimate for the solution, which can then be iteratively improved– convergence is guaranteed for ESP as there are only finitely many possibilities altogether– either one of them is a solution or there is no solutionProf. Aiken CS 295 Lecture 18 28Comments• ESP uses “summary edges” to capture recursive constraints•Essentially, break cycle by assigning some Essentially, break cycle by assigning some initial value to the result of a recursive function– Iterate to find true valueProf. Aiken CS 295 Lecture 18 29Aliasing• Tricky aliasing is a problem in real code•Example:tmp= foo field;tmp foo.field;f = tmp->file;open(tmp->file);…close(tmp->file);if (foo.field->file == NULL) …Prof. Aiken CS 295 Lecture 18 305/23/20116Aliasing (Cont.)• Like all sound analysis systems, ESP incorporates alias analysis– Context sensitive– Flow-insensitive• Property checking must be done for every expression in an alias equivalence classProf. Aiken CS 295 Lecture 18 31What About Multiple Values?• What if a program, say, opens 3 files?•ESP is run 3 times–Once for each fileOnce for each file– Or rather, each alias equivalence class with a file• Allows branches that affect other files to be ignored during analysis– Separate analysis of each is more efficient than simultaneous analysis