Xavier Rival - Introduction to static analysis an abstract interpretation perspective

Introduction to Static Analysis

2020 Massachusetts Institute of Technology

All rights reserved. No part of this book may be reproduced in any form or by any electronic or mechanical means (including photocopying, recording, or information storage and retrieval) without permission in writing from the publisher.

Library of Congress Cataloging-in-Publication Data

Names: Rival, Xavier, author. | Yi, Kwangkeun, author.

Title: Introduction to static analysis : an abstract interpretation perspective / Xavier Rival and Kwangkeun Yi.

Description: Cambridge, MA : The MIT Press, [2020] | Includes bibliographical references and index.

Identifiers: LCCN 2019010151 | ISBN 9780262356657

Subjects: LCSH: Statics.

Classification: LCC TA351 .R58 2020 | DDC 620.1/03dc23 LC record available at https://lccn.loc.gov/2019010151

Author names are in alphabetical order. Both authors share equal authorship.

d_r0

To our parents

Static program analysis or, for short, static analysis aims at discovering semantic properties of programs without running them. Initially, it was introduced in the seventies to enable compiler optimizations and guide the synthesis of efficient machine code. Since then, the interest in static analysis has grown considerably, as it plays an important role in all phases of program development, including the verification of specifications, the verification of programs, the synthesis of optimized code, and the refactoring and maintenance of software applications. It is commonly used to certify critical software. It also helps improve the quality of general-purpose software and enables aggressive code optimizations. Consequently, static analysis is now relevant not only to computer scientists who study the foundations of programming but also to many working engineers and developers who can use it for their everyday work.

The purpose of this book is to provide an introduction to static analysis and to cover the basics of both theoretical foundations and practical considerations underlying the implementation and use of static analysis tools. 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; thus, it is harder to find good references that could provide a quick and comprehensive introduction for nonexperts. The aim of this book is precisely to provide such a general introduction, which explains the key basic concepts (both in the theory and from a practical point of view), gives the gist of the state of the art in static program analysis, and can be read rather quickly and easily. More precisely, we cover the mathematical foundations of static analysis (semantics, semantic abstraction, computation of program invariants), more advanced notions and techniques (abstractions for advanced programming features and for answering a wide range of semantic questions), and techniques to implement and use static analysis tools.

On the other hand, it is not possible to provide an exhaustive description of the state of the art, simply because the sheer number of scientific reports and articles published every year on the topic far exceeds what a single person can assimilate or will even need. A huge number of practical techniques and fundamental constructions could be studied, yet they may be useful to only a small group of readers. Therefore, we believe that exhaustivity should not be the purpose of this book, and it is likely that most readers will have to complement it with additional material that covers their personal interest. However, we hope that this book will help all readers quickly reach the point where they master the foundational principles of static analysis, and help them acquire additional knowledge more easily when they need it. To better achieve this, we try to present, in an intuitive manner, some ideas and principles that often take years of research and practical experience to fully understand and learn.

We divide our material into chapters that can often be skipped or omitted in the first reading, depending on the motivations of the reader. Furthermore, we distinguish several reader profiles, which we consider part of the target audience of this book and for whom we can provide specific advice on where to start and how to handle each chapter:

• Students (abbreviated as [S] in the introduction to each chapter) who follow a course on programming languages, compilers, program analysis, or program verification will find here material to construct a theoretical and practical knowledge of static analysis; we expect advanced students (e.g., graduate students specializing in program analysis or verification) to read most of the chapters and complement them with additional readings, whereas more junior students can focus on the first chapters.
• Developers ([D]) of programming tools (e.g., compilers and program verifiers) who need to implement static analysis techniques to solve practical problems will find both the technical basics that they need and practical examples with actual code to learn about common approaches to implementing static analyzers.
• Users ([U]) of static analysis tools need to know about the general principles underlying static analyzers and how to set up an analysis; they will find not only general notions on static analysis but also a chapter devoted specifically to the use of static analysis tools, including their configuration and the exploitation of the analysis results.

Structure of the Book presents an intuitive graphical introduction to the abstraction of program semantics and to the static analysis of programs. These two chapters are fundamental for all readers.

in a first reading, returning to it when needed.

The following two chapters focus on the practical implementation and use of static analysis techniques. reviews the implementation of a simple static analyzer, provides source code, and discusses implementation choices. It was written for readers who intend to develop static analyzers, although other readers may also find it useful for gaining deeper understanding of how a static analyzer works. Readers who are mainly interested in the foundations may skip these two chapters, at least in the first reading.

The next two chapters consider more advanced applications. , yet take advantage of specific programming language features or properties of interest to build efficient static analyses. These chapters often focus on the high-level ideas and main abstractions to solve a class of problems. We expect readers interested in these issues to pursue reading of additional material.

Finally, summarizes the main concepts of static analysis, several routes for further studies, and a few challenges for the future.

For reference, appendix A recalls standard mathematical notations used throughout the book (to make it accessible even without a background in discrete mathematics and logics), and appendix B collects the proofs of the theorems presented in the core of the formal chapters.

Acknowledgments

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.