This repository collects examples from the Software Analysis lecture in Jupyter notebooks.
PDF Exports of the notebooks will be uploaded to StudIP, and markdown exports are included in the repository. To run the notebooks on your own you will need to install Jupyter.
This chapter describes two very basic analyses of source code at character level, by splitting source code files into lines: The first analysis is to count lines of code, and the second on is a basic code clone detection technique, capable of detecting type 1 clones.
This chapter looks at the process of converting source code into token streams, and applying different types of analyses on these, such as code clone detection or code completion based on language models.
This chapter considers syntactic information on top of the lexical information provided by the tokens. That is, it considers what language constructs the tokens are used in, by looking at the abstract syntax tree. We further look at how we can automatically generate parsers using Antlr, and then use these to translate programs and to create abstract syntax trees. We also use the Abstract Syntax Trees to do some basic linting.
This chapter looks at how to extract information about the flow of control between the statements in a program, and how to represent this in the control flow graph. The control flow graph is the foundation for further control flow analyses, and in particular we consider dominance and post-dominance relations, which in turn are the foundation for control dependence analysis.
This chapter looks at how to track the propagation of data throughout the control flow of the program. We consider some classical data-flow analyses using an iterative analysis framework, and specifically look at how to propagate information about reaching definitions and reachable uses, which then allows us to construct a data-dependence graph.
This chapter continues with dataflow analysis, and refines our iterative dataflow analysis algorithm from chapter 6 to the lattice-theoretic monotone framework. Using this framework, we can then apply abstract interpretation, which is a more general analysis not only of how the program computes (which are all the analyses from chapter 6), but also what the program computes. Since this is more challenging, we need to abstract the values. Our example analysis checks if programs may have division by zero errors.
This chapter continues the zero-analysis example, but considers what happens if you have functions that call other functions. We can either assume a function call can return anything, or we have to make our analysis interprocedural. This causes some challenges, for example if the same method is called from multiple locations. We counter this problem by making our analysis context-sensitive (using cloning in the example).
In this chapter we revisit control dependencies, and look at an alternative way to calculate them using the dominance frontier (a concept used for creating static single assignment form). By combining data and control dependencies, we can create the program dependence graph. This can be used to slice programs, i.e., extract subsets of the program that are relevant for a given target slicing criterion. Since the examples are analysing Java code, the notebook focuses only on static slicing, although the concepts generalise well to dynamic slicing as covered in the lecture.
All previous chapters considered static analysis, now we move on to dynamic analysis. We start analysing Python code, since this can be executed easily within the notebooks. We consider two alternative ways to instrument programs such that we can create execution traces: (1) Modifying ASTs, and (2) using the VM's tracing functionality. Using these instrumentation approaches we implement a range of different example dynamic analyses.
Symbolic execution represents execution paths as symbolic constraints over input variables. This can be used to generate test inputs that cover specific paths, or it can be used to check assertions and other properties of a program. Although recent progress on constraint solvers (SMT solvers in particular) has greatly improved the applicability of symbolic execution, there are fundamental limitations such as having to deal with loops, or black box function calls, which can, however, be overcome dynamically. The combination of dynamic and symbolic execution is known as dynamic symbolic execution, or concolic execution (concrete+symbolic). This chapter is based on Andreas Zeller's excellent Fuzzing Book