Introduction to Static Analysis: An Abstract Interpretation Perspective (The MIT Press)

We are grateful to the many people who helped bring this book to fruition. First and foremost, we thank all the great researchers and professors who contributed to the emergence and development of the static analysis field. In particular, Patrick Cousot and Radhia Cousot have built a very robust, powerful, and general framework for designing static analysis and more generally for reasoning about program semantics. Since these foundational works have been achieved, many research scientists, developers, engineers, and pioneer end users have contributed to the development and adoption of static analysis and have greatly advanced the state of the art. We would like to thank them all here. Many colleagues have contributed directly or indirectly in the genesis of this book with discussions, ideas, and encouragement, and we thank them all, even though we cannot gather an exhaustive list. We especially thank Copyright 4 Preface 10 1 Program Analysis 17 1.1 Understanding Software Behavior 17 1.2 Program Analysis Applications and Challenges 18 1.3 Concepts in Program Analysis 21 1.3.1 What to Analyze 21 1.3.2 Static versus Dynamic 23 1.3.3 A Hard Limit: Uncomputability 24 1.3.4 Automation and Scalability 26 1.3.5 Approximation: Soundness and Completeness 27 1.4 Families of Program Analysis Techniques 30 1.4.1 Testing: Checking a Set of Finite Executions 30 1.4.2 Assisted Proof: Relying on User-Supplied Invariants 32 1.4.3 Model Checking: Exhaustive Exploration of Finite Systems 33 1.4.4 Conservative Static Analysis: Automatic, Sound, and Incomplete Approach 34 1.4.5 Bug Finding: Error Search, Automatic, Unsound, Incomplete, Based on Heuristics 35 1.4.6 Summary 36 1.5 Roadmap 37 2 A Gentle Introduction to Static Analysis 38 2.1 Semantics and Analysis Goal: A Reachability Problem 38 2.2 Abstraction 44 2.3 A Computable Abstract Semantics: Compositional Style 55 2.3.1 Abstraction of Initialization 55 2.3.2 Abstraction of Post-Conditions 56 2.3.3 Abstraction of Non-Deterministic Choice 61 2.3.4 Abstraction of Non-Deterministic Iteration 62 2.3.5 Verification of the Property of Interest 70 2.4 A Computable Abstract Semantics: Transitional Style 71 2.4.1 Semantics as State Transitions 72 2.4.2 Abstraction of States 76 2.4.3 Abstraction of State Transitions 77 2.4.4 Analysis by Global Iterations 80 2.5 Core Principles of a Static Analysis 86 3 A General Static Analysis Framework Based on a Compositional Semantics 90 3.1 Semantics 91 3.1.1 A Simple Programming Language 91 3.1.2 Concrete Semantics 92 3.2 Abstractions 99 3.2.1 The Concept of Abstraction 99 3.2.2 Non-Relational Abstraction 104 3.2.3 Relational Abstraction 108 3.3 Computable Abstract Semantics 110 3.3.1 Abstract Interpretation of Assignment 113 3.3.2 Abstract Interpretation of Conditional Branching 117 3.3.3 Abstract Interpretation of Loops 121 3.3.4 Putting Everything Together 131 3.4 The Design of an Abstract Interpreter 133 4 A General Static Analysis Framework Based on a Transitional Semantics 137 4.1 Semantics as State Transitions 138 4.1.1 Concrete Semantics 139 4.1.2 Recipe for Defining a Concrete Transitional Semantics 144 4.2 Abstract Semantics as Abstract State Transitions 145 4.2.1 Abstraction of the Semantic Domain 145 4.2.2 Abstraction of Semantic Functions 150 4.2.3 Recipe for Defining an Abstract Transition Semantics 152 4.3 Analysis Algorithms Based on Global Iterations 155 4.3.1 Basic Algorithms 155 4.3.2 Worklist Algorithm 157 4.4 Use Example of the Framework 159 4.4.1 Simple Imperative Language 159 4.4.2 Concrete State Transition Semantics 162 4.4.3 Abstract State 163 4.4.4 Abstract State Transition Semantics 164 5 Advanced Static Analysis Techniques 167 5.1 Construction of Abstract Domains 168 5.1.1 Abstraction of Boolean-Numerical Properties 169 5.1.2 Describing Conjunctive Properties 171 5.1.3 Describing Properties Involving Case Splits 176 5.1.4 Construction of an Abstract Domain 180 5.2 Advanced Iteration Techniques 182 5.2.1 Loop Unrolling 183 5.2.2 Fixpoint Approximation with More Precise Widening Iteration 186 5.2.3 Refinement of an Abstract Approximation of a Least Fixpoint 188 5.3 Sparse Analysis 190 5.3.1 Exploiting Spatial Sparsity 193 5.3.2 Exploiting Temporal Sparsity 194 5.3.3 Precision-Preserving Def-Use Chain by Pre-Analysis 196 5.4 Modular Analysis 198 5.4.1 Parameterization, Summary, and Scalability 199 5.4.2 Case Study 200 5.5 Backward Analysis 202 5.5.1 Forward Semantics and Backward Semantics 202 5.5.2 Backward Analysis and Applications 204 5.5.3 Precision Refinement by Combined Forward and Backward Analysis 207 6 Practical Use of Static Analysis Tools 211 6.1 Analysis Assumptions and Goals 211 6.2 Setting Up the Static Analysis of a Program 220 6.2.1 Definition of the Source Code and Proof Goals 220 6.2.2 Parameters to Guide the Analysis 225 6.3 Inspecting Analysis Results 229 6.4 Deployment of a Static Analysis Tool 235 7 Static Analysis Tool Implementation 238 7.1 Concrete Semantics and Concrete Interpreter 239 7.2 Abstract Domain Implementation 247 7.3 Static Analysis of Expressions and Conditions 252 7.4 Static Analysis Based on a Compositional Semantics 255 7.5 Static Analysis Based on a Transitional Semantics 260 8 Static Analysis for Advanced Programming Features 266 8.1 For a Language with Pointers and Dynamic Memory Allocations 267 8.1.1 Language and Concrete Semantics 268 8.1.2 An Abstract Semantics 270 8.2 For a Language with Functions and Recursive Calls 275 8.2.1 Language and Concrete Semantics 275 8.2.2 An Abstract Semantics 279 8.3 Abstractions for Data Structures 286 8.3.1 Arrays 286 8.3.2 Buffers and Strings 293 8.3.3 Pointers 296 8.3.4 Dynamic Heap Allocation 301 8.4 Abstraction for Control Flow Structures 309 8.4.1 Functions and Procedures 310 8.4.2 Parallelism 319 9 Classes of Semantic Properties and Verification by Static Analysis 326 9.1 Trace Properties 327 9.1.1 Safety 328 9.1.2 Liveness 332 9.1.3 General Trace Properties 335 9.2 Beyond Trace Properties: Information Flows and Other Properties 337 10 Specialized Static Analysis Frameworks 345 10.1 Static Analysis by Equations 346 10.1.1 Data-Flow Analysis 346 10.2 Static Analysis by Monotonic Closure 351 10.2.1 Pointer Analysis 352 10.2.2 Higher-Order Control-Flow Analysis 355 10.3 Static Analysis by Proof Construction 359 10.3.1 Type Inference 359 11 Summary and Perspectives 367 A Reference for Mathematical Notions and Notations 370 A.1 Sets 370 A.2 Logical Connectives 371 A.3 Definitions and Proofs by Induction 371 A.4 Functions 371 A.5 Order Relations and Ordered Sets 372 A.6 Operators over Ordered Structures and Fixpoints 373 B Proofs of Soundness 375 B.1 Properties of Galois Connections 375 B.2 Proofs of Soundness for Chapter 376 B.2.1 Soundness of the Abstract Interpretation of Expressions 376 B.2.2 Soundness of the Abstract Interpretation of Conditions 377 B.2.3 Soundness of the Abstract Join Operator 378 B.2.4 Abstract Iterates with Widening 378 B.2.5 Soundness of the Abstract Interpretation of Commands 380 B.3 Proofs of Soundness for Chapter 381 B.3.1 Transitional-Style Static Analysis over Finite-Height Domains 381 B.3.2 Transitional-Style Static Analysis with Widening 383 B.3.3 Use Example of the Transitional-Style Static Analysis 384 Bibliography 386 Index 394 A self-contained introduction to abstract interpretation-based static analysis, an essential resource for students, developers, and users. Static program analysis, or static analysis, aims to discover semantic properties of programs without running them. It plays an important role in all phases of development, including verification of specifications and programs, the synthesis of optimized code, and the refactoring and maintenance of software applications. This book offers a self-contained introduction to static analysis, covering the basics of both theoretical foundations and practical considerations in the use of static analysis tools. By offering a quick and comprehensive introduction for nonspecialists, the book fills a notable gap in the literature, which until now has consisted largely of scientific articles on advanced topics. The text covers the mathematical foundations of static analysis, including semantics, semantic abstraction, and computation of program invariants; more advanced notions and techniques, including techniques for enhancing the cost-accuracy balance of analysis and abstractions for advanced programming features and answering a wide range of semantic questions ; and techniques for implementing and using static analysis tools. It begins with background information and an intuitive and informal introduction to the main static analysis principles and techniques. It then formalizes the scientific foundations of program analysis techniques, considers practical aspects of implementation, and presents more advanced applications. The book can be used as a textbook in advanced undergraduate and graduate courses in static analysis and program verification, and as a reference for users, developers, and experts. "The book introduces static analysis. It covers both the basic theoretical foundations and the basic practical consideration underlying the design, implementation, and the use of static analysis tools. It is hard to find good references that could provide a quick and comprehensive introduction for non-experts. The scientific literature on static analysis is huge, and may seem hard for students or working engineers to get started quickly. Indeed, while we can recommend great scientific articles on many specific topics, these are often too advanced for a general audience. The purpose of this book is precisely to provide such a general introduction, that effectively provides the basic key concepts (both in the theory and in the practical point of view), gives the gist of the state of the art in program static analysis, and that can be read rather quickly and easily. More precisely, we cover the mathematical foundations of general static analysis frameworks (semantics, semantic abstraction, computation of program invariants), more advanced notions and techniques (abstractions for advanced programming features, and to answer a wide range of semantic questions), and techniques to implement and use static analysis tools"-- Provided by publisher