1Prof. Aiken CS295 Lecture 10 1Introduction to Static AnalysisCS295Lecture 10Prof. Aiken CS295 Lecture 10 2Definitions• Program analysisDiscovering facts about programs.• Dynamic analysisProgram analysis using program executions.• Static analysisProgram analysis without running the program.Prof. Aiken CS295 Lecture 10 3History• Static analysis is nearly as old as programming.• First used in compilers– For program optimization– Starting with FORTRAN (1954)• Use for software quality nearly as old– Type systemsProf. Aiken CS295 Lecture 10 4So What?• It’s a big field– With different approaches– And applications– And lots of terms• This lecture aims to sketch basic– concepts– techniques– terminologyProf. Aiken CS295 Lecture 10 5Laundry List Outline• Analysis paradigms– Type systems– Dataflow analysis– Model checking• Terminology– Abstract values– Flow insensitive– Flow sensitive– Path sensitive– Local vs. global analysis– Verification vs. bug-finding– Soundness– False positives and false negatives– . . .Prof. Aiken CS295 Lecture 10 6Type SystemsA Notation for Describing Static Analyses2Prof. Aiken CS295 Lecture 10 7Type Systems• Types are the most widely used static analysis• Part of nearly all mainstream languages– Widely recognized as important for quality• Type notation is useful for discussing concepts– We use type notation to discuss type checking, dataflow analysis, and model checkingProf. Aiken CS295 Lecture 10 8What is a Type?• Consensus– A set of values• Examples– Int is the set of all integers– Float is the set of all floats– Bool is the set {true, false}Prof. Aiken CS295 Lecture 10 9More Examples• List(Int) is the set of all lists of integers– List is a type constructor– A function from types to types• Foo, in Java, is the set of all objects of class Foo• Int  Int is the set of functions mapping an integer to an integer– E.g., increment, decrement, and many othersProf. Aiken CS295 Lecture 10 10What is a Type?• Consensus– A set of values• A type is an example of an abstractvalue– Represents a set of concretevalues– Every static analysis has abstract values• In type systems, – Every concrete value is an element of some abstract value– i.e., every concrete value has a typeProf. Aiken CS295 Lecture 10 11Abstraction• All static analyses use abstraction– Represent sets of values as abstract values• Why?– Because we can’t reason directly about the infinite set of possible concrete values– For performance (even just termination), must make such approximations• In type systems, the approximations are called typesProf. Aiken CS295 Lecture 10 12The Next Step• Now we need to compute with types– Actually analyze programs• Type systems have a well-developed notation for expressing such computations3Prof. Aiken CS295 Lecture 10 13Rules of Inference• Inference rules have the formIf Hypothesis is true, then Conclusion is true• Type checking computes via reasoningIf E1and E2 have certain types, then E3has a certain type• Rules of inference are a compact notation for “If-Then” statementsProf. Aiken CS295 Lecture 10 14From English to an Inference Rule• Start with a simplified system and gradually add features• Building blocks– Symbol  is “and”– Symbol is “if-then”– x:T is “x has type T”Prof. Aiken CS295 Lecture 10 15From English to an Inference Rule (2)If e1has type Int and e2has type Int, then e1+ e2has type Int(e1has type Int  e2has type Int) e1+ e2has type Int(e1: Int  e2: Int)  e1+ e2: IntProf. Aiken CS295 Lecture 10 16From English to an Inference Rule (3)The statement (e1: Int  e2: Int)  e1+ e2: Intis a special case of Hypothesis1 . . .  Hypothesisn ConclusionThis is an inference rule.Prof. Aiken CS295 Lecture 10 17Notation for Inference Rules• By tradition inference rules are written Hypothesis1. . .  Hypothesisn Conclusion• Type rules have hypotheses and conclusions e : T• means “it is provable that . . .”Prof. Aiken CS295 Lecture 10 18Two Rules[Int][Add]i is an integer i : Int e1: Int e2: Int  e1 + e2: Int4Prof. Aiken CS295 Lecture 10 19Two Rules (Cont.)• These rules give templates describing how to type integers and + expressions• By filling in the templates, we can produce complete typings for expressions• Note that– Hypotheses prove facts about subexpressions– Conclusions prove facts about the entire expressionProf. Aiken CS295 Lecture 10 20Example: 1 + 21 is an integer 1: Int2 is an integer 2: Int 1 + 2: IntProf. Aiken CS295 Lecture 10 21A Problem• What is the type of a variable reference?• The rule does not carry enough information to give x a type.[Var] x: ?x is a variableProf. Aiken CS295 Lecture 10 22A Solution• Put more information in the rules!• Anenvironmentgives types for freevariables– An environment is a function from variables to types– For other static analyses the environment may map variables to other abstract values– A variable is free in an expression if it is not defined within the expressionProf. Aiken CS295 Lecture 10 23Type EnvironmentsLet A be a function from Variables to TypesThe sentence A  e : T is read: Under the assumption that variables have the types given by A, it is provable that the expression e has the type TProf. Aiken CS295 Lecture 10 24Modified RulesThe type environment is added to all rules:[Add]A  e1 : IntA  e2 : IntA  e1 + e2 : Int5Prof. Aiken CS295 Lecture 10 25New RulesAnd we can write new rules:[Var]A  x: TA(x) = TProf. Aiken CS295 Lecture 10 26SummaryDescribe static analyses using logics of the form:A’  e’ : T’A’’  e’’ : T’’A  e : TThe program (or program fragment) to be analyzed.Assumptions needed for aspects of e that are determined by e’s environment.The abstract value computed for e.Analysis of expression is recursively defined using analysis of subexpressions.Prof. Aiken CS295 Lecture 10 27An ExampleProf. Aiken CS295 Lecture 10 28The Rule of Signs• We want to estimate a computation’s sign• Example: -3 * 4 = -12• Abstraction: - * + = -Prof. Aiken CS295 Lecture 10 29Abstract Values• + = {set of positive integers}• 0 = { 0 }• - = {set of negative integers}• Environment: Variables -> {+, 0, - }Prof. Aiken CS295