Static Program Analysis - Aarhus Universitet

1 Static Program AnalysisAnders M ller and Michael I. SchwartzbachJanuary 3, 2022 Copyright 2008 2021 Anders M ller and Michael I. SchwartzbachDepartment of Computer ScienceAarhus University, DenmarkThis work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives International License. To view a copy of this license, Applications of Static Program Analysis .. Approximative Answers .. Undecidability of Program Correctness ..62 A Tiny Imperative Programming The Syntax of TIP .. Example Programs .. Normalization .. Abstract Syntax Trees .. Control Flow Graphs ..163 Type Types .. Type Constraints .. Solving Constraints with Unification .. Record Types .. Limitations of the Type Analysis .

2 334 Lattice Motivating Example: Sign Analysis .. Lattices .. Constructing Lattices .. Equations, Monotonicity, and Fixed Points ..435 Dataflow Analysis with Monotone Sign Analysis , Revisited .. Constant Propagation Analysis .. Fixed-Point Algorithms .. Live Variables Analysis .. Available Expressions Analysis .. Very Busy Expressions Analysis .. Reaching Definitions Analysis .. Forward, Backward, May, and Must .. Initialized Variables Analysis .. Transfer Functions ..766 Interval Analysis .. Widening and Narrowing ..827 Path Sensitivity and Relational Control Sensitivity using Assertions .. Paths and Relations ..918 Interprocedural Interprocedural Control Flow Graphs.

3 Context Sensitivity .. Context Sensitivity with Call Strings .. Context Sensitivity with the Functional Approach .. 1079 Control Flow Closure Analysis for the -calculus .. The Cubic Algorithm .. TIP with First-Class Function .. Control Flow in Object Oriented Languages .. 12010 Pointer Allocation-Site Abstraction .. Andersen s Algorithm .. Steensgaard s Algorithm .. Interprocedural Pointer Analysis .. Null Pointer Analysis .. Flow-Sensitive Pointer Analysis .. Escape Analysis .. 13711 Abstract A Collecting Semantics for TIP .. Abstraction and Concretization .. Soundness .. Optimality .. Completeness .. Trace Semantics .. 166 Index of Notation171 CONTENTSiiiBibliography173 PrefaceStatic Program Analysis is the art of reasoning about the behavior of computerprograms without actually running them.

4 This is useful not only in optimizingcompilers for producing efficient code but also for automatic error detectionand other tools that can help programmers. A Static Program analyzer is a pro-gram that reasons about the behavior of other programs. For anyone interestedin programming, what can be more fun than writing programs that analyzeprograms?As known from Turing and Rice, all nontrivial properties of the behaviorof programs written in common programming languages are mathematicallyundecidable. This means that automated reasoning of software generally mustinvolve approximation. It is also well known that testing, concretely runningprograms and inspecting the output, may reveal errors but generally cannotshow their absence. In contrast, Static Program Analysis can with the right kindof approximations check all possible executions of the programs and provideguarantees about their properties.

5 One of the key challenges when developingsuch analyses is how to ensure high precision and efficiency to be practicallyuseful. For example, nobody will use an Analysis designed for bug finding ifit reports many false positives or if it is too slow to fit into real-world softwaredevelopment notes present principles and applications of Static Analysis of pro-grams. We cover basic type Analysis , lattice theory, control flow graphs, dataflowanalysis, fixed-point algorithms, widening and narrowing, path sensitivity, rela-tional Analysis , interprocedural Analysis , context sensitivity, control flow Analysis ,several flavors of pointer Analysis , and key concepts of semantics-based abstractinterpretation. A tiny imperative programming language with pointers andfirst-class functions is subjected to numerous different Static analyses illustratingthe techniques that are take aconstraint-based approachto Static Analysis where suitable constraintsystems conceptually divide the Analysis task into a front-end that generatesconstraints from Program code and a back-end that solves the constraints toproduce the Analysis results.

6 This approach enables separating the analysisvviPrefacespecification, which determines its precision, from the algorithmic aspects thatare important for its performance. In practice when implementing analyses, weoften solve the constraints on-the-fly, as they are generated, without representingthem focus on analyses that are fullyautomatic( , not involving Program -mer guidance, for example in the form of loop invariants or type annotations)andconservative(sound but incomplete), and we only consider Turing com-plete languages (like most programming languages used in ordinary softwaredevelopment).The analyses that we cover are expressed using different kinds of constraintsystems, each with their own constraint solvers: term unification constraints, with an almost-linear union-find algorithm, conditional subset constraints, with a cubic-time algorithm, and monotone constraints over lattices, with variations of fixed-point style of presentation is intended to be precise but not overly readers are assumed to be familiar with advanced programming languageconcepts and the basics of compiler construction and computability notes are accompanied by a web site that provides lecture slides, animplementation (in Scala) of most of the algorithms we cover, and additionalexercises.

7 Amoeller/spa/Chapter1 IntroductionStatic Program Analysis aims to automatically answer questions about the possi-ble behaviors of programs. In this chapter, we explain why this can be usefuland interesting, and we discuss the basic characteristics of Analysis Applications of Static Program AnalysisStatic Program Analysis has been used since the early 1960 s in optimizing com-pilers. More recently, it has proven useful also for bug finding and verificationtools, and in IDEs to support Program development. In the following, we givesome examples of the kinds of questions about Program behavior that arise inthese different for Program optimizationOptimizing compilers (including just-in-time compilers in interpreters) need to know many different properties of theprogram being compiled, in order to generate efficient code.

8 A few examples ofsuch properties are: Does the Program contain dead code, or more specifically, is functionfunreachable frommain? If so, the code size can be reduced. Is the value of some expression inside a loop the same in every iteration?If so, the expression can be moved outside the loop to avoid redundantcomputations. Does the value of variablexdepend on the Program input? If not, it couldbe precomputed at compile time. What are the lower and upper bounds of the integer variablex? The answermay guide the choice of runtime representation of the variable. Dopandqpoint to disjoint data structures in memory? That may enableparallel INTRODUCTIONA nalysis for Program correctnessThe most successful Analysis tools that havebeen designed to detect errors (or verify absence of errors) target generic cor-rectness properties that apply to most or all programs written in specific pro-gramming languages.

9 In unsafe languages like C, such errors sometimes lead tocritical security vulnerabilities. In more safe languages like Java, such errors aretypically less severe, but they can still cause Program crashes. Examples of suchproperties are: Does there exist an input that leads to a null pointer dereference, division-by-zero, or arithmetic overflow? Are all variables initialized before they are read? Are arrays always accessed within their bounds? Can there be dangling references, , use of pointers to memory that hasbeen freed? Does the Program terminate on every input? Even in reactive systems suchas operating systems, the individual software components, for exampledevice driver routines, are expected to always correctness properties depend on specifications provided by the Program -mer for the individual programs (or libraries), for example: Are all assertions guaranteed to succeed?

10 Assertions express programspecific correctness properties that are supposed to hold in all executions. Is functionhasNextalways called before functionnext, and isopenalwayscalled beforeread? Many libraries have such so-calledtypestatecorrectnessproperties. Does the Program throw anActivityNotFoundExceptionor aSQLiteExceptionfor some input?With web and mobile software, information flow correctness properties havebecome extremely important: Can input values from untrusted users flow unchecked to file systemoperations? This would be a violation ofintegrity. Can secret information become publicly observable? Such situations areviolations increased use of concurrency (parallel or distributed computing) and event-driven execution models gives rise to more questions about Program behavior: Are data races possible?