Dillig1CS157: Computational LogicFall 2007Static Program AnalysisDillig2●Everything I will present is joint work with Isil Dillig. ●Unfortunately, she is sick and cannot present as planned today.Dillig3Motivation●Software is increasingly becoming an inherent part of our every day life.●Software failures can have very significant consequences.●Example 1: The Ariane Rocket–Cost: 7.5 billion dollars●Example 2: Therac-25 –At least 5 patients died.Dillig4How do we prevent software failures?●Traditional Testing–Cannot achieve good 'coverage'–Does not guarantee lack of errors ●Dynamic program analysis–Instrument program execution to identify errors–Achieves better coverage than testing–But still cannot guarantee lack of errors.Dillig5Static Program Analysis●Find errors in the program without actually executing it.●Static analysis tool – A program that takes another program as input and automatically identifies errors in the input program.●'Symbolic execution' => 100% coverage ●Verify lack of errors: 'soundness'–Partial verification: guarantees lack of a certain class of errors, e.g null dereferences, integer overflow etc.Dillig6But what about Rice's Theorem?●Rice's Theorem: –Any non-trivial property of programs is undecidable!●So, what do we mean by 'verification'?●We deal with over-approximations of programs–such that these over-approximations are over a decidable theory (e.g. boolean SAT)–but static analysis tools will report some errors that are not actually errors in the original program● false positivesDillig7How is computational logic relevant to all this?●Computational logic comes up all over the place, but especially in constraint-based static analysis.●Constraint-based analysis–Step 1: Generate constraints–Step 2: Solve these constraints●This is the where the techniques from CS157 are useful!Dillig8Constraint Generation●Example:void foo(bool flag, int b)void foo(bool flag, int b){{int a;int a;if(flag)if(flag)a = 3;a = 3;else if(b != 0)else if(b != 0)a = b;a = b;else a=-1;else a=-1;assert(a>0);assert(a>0);}}● The constraint under which the assertion holds:flag flag |||| (b!=0 & b>0) (b!=0 & b>0)Dillig9Why are constraints useful?●Given a constraint for a program property P, we are often interested in knowing either of the following two:–Is this constraint satisfiable?●If so, then property P MAYMAY hold. –Is this constraint valid?●Then, property P MUSTMUST hold.Dillig10Example: Safety Properties●A safety property is a property stating that 'something bad' never happens:●A null pointer may not be dereferenced.●An unitialized variable may not be used.●A tainted value may not be referenced etc.●Requires satisfiability query–If the constraint under which 'something bad' happens is SAT, then the program may violate the safety property.Dillig11Example: Liveness Properties●A liveness property is a property that specifies that 'something good' eventually happens:●Allocated memory must be freed.●An opened file must be closed etc.●Requires querying validity–If the constraint is not valid, then liveness property may be violated.Dillig12Constraint Resolution●To solve the kinds of constraints that come up in static analysis, we typically make use of two kinds of theorem provers:–SAT solvers –SMT solversDillig13SAT solvers●Boolean Satisfiability–Since every variable is represented as n # of bits in hardware (e.g. n=32), we can model every program variable as n boolean variables.–Constraints expressed in propositional logic!–Many program analysis tools use this trick●E.g. SATURN: http://saturn.stanford.edu/Dillig14Example●Suppose type supershortsupershort has only 4 bits.●Assume:– The variable ii has type supershortsupershort–The first bit of i is modeled by variable a, second bit by b, third bit by c, and last bit by d.Dillig15Example Continued●Then the constraint i=1 & i>1i=1 & i>1 results in the following propositional formula:a & !b & !c & !d & (b | c | d)a & !b & !c & !d & (b | c | d) ●By inspection, this is UNSAT!Dillig16Advantages of SAT●Very efficient SAT solvers already exist!–No need to implement ad-hoc constraint solvers for a specific application.–Even though boolean SAT is NP-hard, modern SAT solvers can often solve 100,000 clauses in under a second!Dillig17Disadvantages of SAT●Translating to boolean formulas involves loss of high level information.–Ex: To prove that the constraint i<1 & i>2i<1 & i>2 unsatisfiable, we need to represent i as 32 (or 64) boolean variables!Dillig18SMT Solvers●SMT stands for satisfiability modulo theories.–Generalization of boolean satisfiability that also incorprates other (decidable) background theories.●Some example background theories:–Theory of integers (Presburger arithmetic)–Theory of uninterpreted functions–Theory of recursive data structuresDillig19SMT Solvers, continued●Advantage:●often much faster (can exploit high-level structure of contraints)●Disadvantage:●tailored for a specific constraint representation●Perfomance is only good if a problem instance has exploitable higher level structures anticipated by SMT developer. ●Most SMT solvers use SAT solvers as a back-up...Dillig20SMT Example●Assume our SMT solver uses linear intervals and conceptually represents each distinct variable in a constraint as an interval on a line.●Then the constraint i=1i=1 & & i>1i>1 results in the following●However, what would happen with i=1i=1&&i*2>1?i*2>1?-∞ ∞ 0 1iDillig21Current ResearchDisclaimer:●From now on, I will talk specifically about my current research●„Sound, Complete and Scalable Path-sensitive Analysis“–I. Dillig, T. Dillig, A. AikenDillig22Recursive Constraints●Unfortunately, so far we only solved constraints from very simple straight-line programs. ●But how can we write the constraint describing the condition under which queryUser returns true/false?bool queryUser(bool featureEnabled){bool queryUser(bool featureEnabled){ if(!featureEnabled) return false;if(!featureEnabled) return false; char userInput = getUserInput();char userInput = getUserInput(); if(userInput == ’y’) return true;if(userInput == ’y’) return true; if(userInput==’n’) return false;if(userInput==’n’) return false; printf("Please try again");printf("Please try again"); return queryUser(featureEnabled);return queryUser(featureEnabled);}}Dillig23Loops and
View Full Document
Unlocking...